Re: Intended meaning

From: Michael Hanus <mh_at_informatik.uni-kiel.de>
Date: Fri, 02 Nov 2007 12:53:27 +0100

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

This archive was generated by hypermail 2.3.0 : Do Feb 01 2024 - 07:15:08 CET