Re: Intended meaning

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

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 Sun Nov 11 2007 - 22:28:03 CET

This archive was generated by hypermail 2.3.0 : Mon Sep 23 2019 - 07:15:07 CEST