Wolfgang,
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.
Cheers,
Sergio
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on So Nov 11 2007 - 22:28:03 CET