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

From: Wolfgang Lux <wlux_at_uni-muenster.de>

Date: Wed, 26 Oct 2005 13:11:53 +0200

Michael Hanus wrote:

*> You are right that a suspended search goal cannot be resumed
*

*> in the proposed framework. However, I think that the Suspend
*

*> case is useful for the programmer to distinguish finite failure
*

*> and suspension of a computation. For instance, if all branches
*

*> in the search tree are finite and end with a fail, you are
*

*> sure that your initial goal or expression is not provable
*

*> or has no value. Thus, under a closed world assumption,
*

*> you might assume the negation (and this is sometimes used
*

*> to implement negation-as-failure). However, if you consider
*

*> suspension as a failure, this reasoning is no longer true.
*

Good point. But then I would say that the implementation of

allValuesOf is, errr, broken. Most users probably will implement

negation-as-failure via

naf x = allValuesOf x >>= return . null

which falls short in the light of this reasoning. In fact,

returning the list [0] for

allValuesOf (0 ? let X free in ensureNotFree X)

looks somewhat dubious to me.

So I modify my complaints about Bernd's proposal such that

allValuesD and allValuesB should treat the Suspend case

differently. There seem to be two choices how to do that:

1) Report an error when Suspend is encountered.

This can be achieved in at least three different ways:

- omit the Suspend case from the definition,

- use an explicit call to prelude.error, or

- use let X free in ensureNotFree X or an equivalent

expression to make the evaluation of the solutions

suspend like the search goal itself.

2) Change the result types of allValuesD and allValuesB

from SearchTree a -> [a] into SearchTree a -> [Maybe a]

and the implementation of allValuesD would become

allValuesD (Value x) = [Just x]

allValuesD Fail = []

allValuesD Suspend = [Nothing]

allValuesD (Or xs) = concatMap allValuesD xs

Note that the user can easily extract the results of

the terminated computations with Maybe.catMaybes.

Regards

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Mi Okt 26 2005 - 13:45:47 CEST

Date: Wed, 26 Oct 2005 13:11:53 +0200

Michael Hanus wrote:

Good point. But then I would say that the implementation of

allValuesOf is, errr, broken. Most users probably will implement

negation-as-failure via

naf x = allValuesOf x >>= return . null

which falls short in the light of this reasoning. In fact,

returning the list [0] for

allValuesOf (0 ? let X free in ensureNotFree X)

looks somewhat dubious to me.

So I modify my complaints about Bernd's proposal such that

allValuesD and allValuesB should treat the Suspend case

differently. There seem to be two choices how to do that:

1) Report an error when Suspend is encountered.

This can be achieved in at least three different ways:

- omit the Suspend case from the definition,

- use an explicit call to prelude.error, or

- use let X free in ensureNotFree X or an equivalent

expression to make the evaluation of the solutions

suspend like the search goal itself.

2) Change the result types of allValuesD and allValuesB

from SearchTree a -> [a] into SearchTree a -> [Maybe a]

and the implementation of allValuesD would become

allValuesD (Value x) = [Just x]

allValuesD Fail = []

allValuesD Suspend = [Nothing]

allValuesD (Or xs) = concatMap allValuesD xs

Note that the user can easily extract the results of

the terminated computations with Maybe.catMaybes.

Regards

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry

Received on Mi Okt 26 2005 - 13:45:47 CEST

*
This archive was generated by hypermail 2.3.0
: Do Jan 21 2021 - 07:15:03 CET
*