[Termtools] mail test

[Cynthia Kop]

Looking at the output of both Wanda and Sol, it seems that the tools are 
using a different kind of matching: Wanda says YES because she uses 
/plain/ matching, while SOL appears to be using matching /modulo beta/. 
Plain matching means that in examples such as myfunc (λxy. F x y) -> 
myfunc (λxy. F y z) with F a free variable, the only instances of the 
left-hand side have the form myfunc (λxy. s x y). Matching modulo beta 
means that /any/ term of the form myfunc (λxy.t) matches (also if x or y 
occur in s). Thus, the rules are terminating under the former 
interpretation and non-terminating under the latter.

(Since the category is higher-order rewriting /union/ beta, not /modulo/ 
beta, I would argue that the former interpretation is the right one -- 
it's certainly the one that I remember agreeing on when we set up the 
category, and using from the start. However, I can imagine that this 
will give some debate if the definition of the input format is not 
written down anywhere.)

Aside from conflicts, I must admit that I am quite concerned that Wanda 
seems to be failing a /lot/ of benchmarks -- in the sense of apparently 
not delivering an answer. Many of these are new benchmarks and might 
have been due to a timeout, but this includes benchmarks that were 
around long before and that Wanda can trivially handle. Wanda has not 
been updated in at least two years, so it is strange that this should 
change. Moreover, the prover output does indicate that Wanda is giving 
an answer -- see, e.g., http://54.199.109.250:3000/pairs/381734197 and 
http://54.199.109.250:3000/pairs/381734446 . SizeChangeTool suffers from 
the same problem, being marked in red when the answer was YES in for 
instance http://54.199.109.250:3000/pairs/381734376 . Could it be that 
there is a problem with starexec?

On 07/13/2018 02:16 PM, Aart Middeldorp wrote:
> It is :-) There seems to be a yes/no conflict in the HRS (union beta)
> category (involving Sol and Wanda) -- Aart
>
> On 07/13/2018 09:44 AM, Johannes Waldmann wrote:
>> is this list working? - J.W.
>> _______________________________________________
>> Termtools mailing list
>> Termtools at lri.fr
>> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>>
> _______________________________________________
> 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/1b4c289c/attachment.html>