Sergio Antoy wrote:
> Now consider:
>
> 1+x ? zero x
>
> where x is free and zero 0 = 0. There are only to narrexes: the
> whole term and zero x. They are non-overlapping. These are two
> complete computations.
>
> 1+x ? zero x -> 1+x
> 1+x ? zero x -> 1+0 ? 0 -> 1+0 -> 1
Similarly to Wolfgang, I don't see why the second reduction
should be allowed. One has to be careful to narrow
non-outermost (or non-demanded) narrexes because this problem
is already present in confluent TRS. For instance, consider
the rules
f True _ = True
g False = False
and the expression (f x (g x)). If you reduce the narrex (g x),
you cannot obtain the normal form True.
Best regards,
Michael
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Nov 02 2007 - 12:55:04 CET