- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

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

Date: Sat, 10 Nov 2007 06:09:35 -0800 (PST)

Wolfgang,

Thanks for the new interesting example:

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
*