[Termtools] higher-order union beta category in the TPDB

[Cynthia Kop]

Hello all!

With the termination competition approaching, I would like to come back 
to a topic that we debated briefly last year, but which then went 
nowhere. I realise that this is very late -- probably too late to be 
actionable for the current competition -- but figured we still need to 
talk about this to avoid some of the chaos of last year from repeating. 
Also, I would like to see the problems with the TPDB resolved 
eventually. If not for this year, then at least for the next!

/*Item 1: the explanation of the category:*/

Last year there was some confusion regarding the semantics of the 
"higher-order union beta" category, which also lead to conflicts. At the 
time, it was noted that the explanation on 
http://www.termination-portal.org/wiki/Higher_Order_Rewriting is kind of 
minimal. Johannes asked whether the participants could propose 
amendments, and I wrote the following (which I think is what we 
originally intended when designing the formalism):

*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).

However, there has not been any further discussion on this. Can we agree 
that this is the intended format (or propose amendments), and if so, put 
it on the website?

/*Item 2: the current TPDB:*/

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 
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.  An 
example of this is Mixed_HO_10/deriv.xml . However, presumably due to 
the same miscommunication that caused the conflict last year, /all/ the 
Hamana_17 and Hamana_Kikuchi_18 benchmarks do this (except for the ones 
that have no higher-order matching at all, like 
Hamana_17/Blanqui_15/02Ackermann.xml). This gives the wrong impression 
of the format, and forces new tools to deal with a very artificial input 
problem or immediately lose half the database.

Would it be possible to adapt these benchmarks to use plain matching? In 
most cases the choice of replacement is easy -- for example, most of 
them only have higher-order rules of a form like:

         map (λx.F x) (cons Y Z) => cons (F Y) (map (λx.F x) Z)

Which is trivially turned into AFS format by replacing the λx.F x on 
both sides by F.

For this, I look to Makoto Hamana. My guess is that these benchmarks are 
generated, because no one likes to write dozens of XML-files by hand. 
Would it be possible to regenerate them to use plain matching?

(Again, I am not asking to do it for /this/ competition -- let's spare 
Akihisa the last-minute stress. But I think it would be good to set this 
in motion.)

/*Item 3: other problems in the current TPDB:*/

Unrelated to questions of format, I think that the move to StarExec has 
caused a new problem for the competition in that large benchmark sets 
now dominate small categories.

To illustrate this, I would like to point to an addition of my own: in 
2011, I took all the applicative first-order benchmarks that could be 
automatically typed and whose typing had higher-order aspects, uncurried 
them and turned them into higher-order benchmarks. That's 110 benchmarks 
added in one go, most of which are very boring: many of them are just 
instances of map/filter/both with a bunch of first-order rules.

At the time, the competition was run on a /selection/ of benchmarks, and 
the selection mechanism meant that there would not too many benchmarks 
from any particular category. But since we moved to StarExec, the 
competition is run on /all/ the benchmarks. So now suddenly, those 110 
benchmarks dominate the competition. And unfortunately, many of the 2018 
benchmarks have the same "first-order plus one or two higher-order 
rules" format (except now in eta-expanded curried form). Consequently, 
about half the benchmarks now do little more than test the strength of 
the first-order back-end that some higher-order tools use. That should 
not be what the higher-order category is about.

If there are no plans to go back to the old selection mechanism in the 
future, then I would propose pruning the database. Since I added them in 
the first place, I would be happy to cut down the number of 
Uncurried_Applicative benchmarks by removing most of the really boring 
ones (or perhaps move them to a sub-directory that is included for 
reference, but not tested, if that is possible?). Would this be 
acceptable? And could we perhaps do the same with the 2018 benchmarks?

Cynthia.

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