[Termtools] semantics of higher order rewriting/termination?

[Cynthia Kop]

 > and propose amendments if needed?

Well...

*History.* When the higher-order category for the termination 
competition was introduced, we had a long debate about the various 
formalisms and their fundamental differences, and concluded that we'd 
probably need 4-6 formalisms to make everyone happy. However, at the 
time there were only two people who were actively building a tool, and 
both of us were working on slight variations of the formalism that I 
(following Femke van Raamsdonk) call AFS. Thus, we agreed that we'd 
start with only this formalism, and then we could look into spreading 
out to other formalisms -- particularly HRSs -- as more people started 
building tools. However, projects ended and priorities shifted, and that 
never ended up happening... until now, it seems. :)

*The format.* The rules for the XML format in the "higher-order 
rewriting union beta" category are very liberal:

* Types are simple: base types and the arrow constructor, polymorphism 
is not allowed.; notationally, the arrow constructor is right-associative
* Terms are built from typed variables x : sigma and function symbols 
which carry a type declaration f : [sigma_1 x ... x sigma_n] => tau as 
follows:
   - if x : sigma is a variable then x is a term of type sigma;
   - if f : [sigma_1 , ... , sigma_n] => tau is a function symbol and 
s_1,...,s_n terms of type sigma_1,...,sigma_n respectively, then 
f(s_1,...,s_n) is a term of type tau -- and here, tau does not have to 
be a base type;
   - if x is a symbol that hasn't been declared as a variable or 
function symbol and s a term of type tau then lambda x:sigma.s is a term 
of type sigma => tau;
   - if s and t are terms of type sigma -> tau and sigma respectively, 
then s * t is a term of type tau (in the printable format this is 
indicated with a space, but I use a * here for clarity)
* Rules are a pair of terms (l,r) of the same type, such that FV(r) ⊆ 
FV(l) and l is not a variable. That's it -- there are no other sanity 
restrictions on the rules. Matching is plain, and ->_beta is a separate 
rule. That is, s ->_R t if either s ->_beta t or there are a context C, 
a rule (l,r) in R and a substitution gamma such that s = C[l gamma] and 
t = C[r gamma].
* There is no implicit eta rule, although lambda x:sigma.F * x -> F 
would be a valid rule to write down (if F : sigma => tau is a variable).


For term formation, note in particular that this allows both for 
entirely applicative notation ( f * 0 * 0 if f : () --> nat -> nat -> 
nat ), entirely functional notation ( f(0,0) if f : (nat * nat) --> nat 
) and intermediate notation ( f(0) * 0 if f : (nat) --> nat -> nat. This 
difference is significant because if f has a type declaration f : (nat) 
--> nat -> nat, it essentially has a /minimal arity/: you are not 
allowed to use f without giving it at least that one argument. For rule 
formation, note that it is perfectly allowed to have a rule f(λx.F * x) 
-> F * but that this will not match a term f(λx.g(x)). It is also 
allowed to have non-beta-normal left-hand sides, or a left-hand side 
where the head symbol is not a function symbol (e.g., F * x -> x).

*Discussion.* Most benchmarks in the database do not take advantage of 
these allowances, not even to define an eta rule. There have always been 
a few (two or three?) examples in the TPDB that apply a free variable to 
bound variables, but in most cases they seem to be misplaced -- given 
the suggestive naming of symbols in these benchmarks, it looks like HRS 
matching is intended, and these examples cannot really be represented 
with plain matching. However (and I'm sorry for not catching this last 
year, when the first batch was added), the new Hamana examples violate 
this unwritten rule, as they are presented in an eta-long form that does 
not make much sense when using plain matching. Since we are now adding a 
new category for HRSs, I would propose moving these examples there, and 
perhaps make it explicit that applying a variable on the left-hand side 
of a rule really has a different meaning between the two categories.

Cynthia.


On 07/13/2018 04:12 PM, Johannes Waldmann wrote:
> Hi Cynthia,
>
>> I can imagine that this will give some debate > if the definition of the input format is not> written down anywhere.
> then it should be written down. The canonical place is
> http://www.termination-portal.org/wiki/Higher_Order_Rewriting
>
> Can the participants of this category check whether that's enough,
> and propose amendments if needed?
> And/Or refer to a standard publication.
>
> - Johannes.
> _______________________________________________
> Termtools mailing list
> Termtools at lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20180713/e9b08da2/attachment.html>