Re: Intended meaning

From: Sergio Antoy <>
Date: Sat, 10 Nov 2007 06:09:35 -0800 (PST)


Thanks for the new interesting example:

> Thank you for this clarification. So the problem can be boiled
> down to this one. Given the functions
> f False = 1 + failed
> g False = success
> there is a reduction of
> const (f x) (g x)
> to success even if g is rigid, namely with the following steps
> const (f x) (g x)
> ~~> {x=False} const (1 + failed) (g False) -- narrowing (f x)
> ~~> {x=False} const (1 + failed) success -- reducing (g False)
> ~~> {x=False} succeess -- reducing const ...
> and this result cannot be computed with either an outer-most strategy
> (assuming g is rigid) nor an inner-most strategy (because 1+failed
> has no solution).

I think your const is non-standard (swapped arguments?) and you do
not really need 1+, but you certainly expose the problem. It is
known (and acceptable) that residuation is a source of
incompleteness for narrowing computations. After all, it prevents
some steps that would otherwise be pssible, such as reducing (g
False). It is not convenient to make it also a source of
unsoundness. The conclusion is that success should be a result
of the above computation (with your definition of const). If the
result is not found because of residuation, than this is another
example of incompleteness.

curry mailing list
Received on So Nov 11 2007 - 22:28:03 CET

This archive was generated by hypermail 2.3.0 : Do Jun 20 2024 - 07:15:09 CEST