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

From: Wolfgang Lux <lux_at_wi.uni-muenster.de>

Date: Wed, 09 Jan 2002 19:15:17 +0100

Hello Sergio,

*> > coin = 0
*

*> > coin = 1
*

*> >
*

*> > main = findall (\x -> x=:=y) where y = coin
*

*> >
*

*> > where findall computes and unpacks all solutions of a search
*

*> > goal with a depth first strategy. In a system based on pure term
*

*> > rewriting, evaluating the goal main would yield the list [0,1].
*

*>
*

*> How would you define findall with "pure term rewriting"?
*

sorry for being imprecise here. I did not mean that I wanted to defined

findall (and thus the encapsulated search) in pure term rewriting but was

referring to the model used to evaluate Curry expressions. In this case I

could always replace the lambda abstraction \x -> x=:=y by \x -> x=:=coin and

now the effect of findall would be to return the list [0,1].

*> This is what you should get. Intuitively, if you evaluate "coin"
*

*> in a program, you should get either 0 or 1, but not both.
*

*> Thus findall should give you either [0] or [1].
*

Yes, but if I were using the goal

main2 = findall (\x -> x=:=coin)

the result will be the list [0,1].

*> > main' = filter (/= y) (findall (\x -> x=:=y)) where y = coin
*

*> >
*

*> > The only sensible solution I can think of is two times the empty list.
*

*>
*

*> I would prefer once (one time) only. This come from
*

*>
*

*> main' = filter (/= y) (findall (\x -> x=:=y)) where y = 0
*

*>
*

*> and likewise for 1.
*

Yes, this was what I meant by -- loosely -- saying two times the empty list.

Once for y=0 and once for y=1.

*>
*

*> > Maybe this was already obvious to you, but the report is totally ignorant
*

*> > about this. IMHO it should at least include a comment about this (writing
*

*> > down a semantics seems quite tricky and is impossible in the framework
*

*> > used by appendix D as there is no explicit notion of sharing).
*

*> >
*

*> > This problem can also creep in if you are used to higher-order programming.
*

*>
*

*> > For instance the following program will not compute a list of all solutions
*

*>
*

*> > for the function coin but -- like the initial example -- compute both
*

*> > solutions non-deterministically (except if you expect the compiler to
*

*> > perform some global sharing analysis and detect that the first argument of
*

*> > the function same is never going to be shared).
*

*> >
*

*> > coin = 0
*

*> > coin = 1
*

*> >
*

*> > main = findall (same coin)
*

*>
*

*> Here I lost you. How (or where) do you define "same"?
*

Hmmm, this was due to some incomplete change of the example. The lacking

definition was

same x y = x =:= y

But the problem is not related to this particular definition of same. In

fact, an binary (constraint) function which uses its first argument will work

(errr, not work as expected :-).

*> I think that some difficulty would be eliminated by considering
*

*> two findalls, the usual one and another for non-deterministic
*

*> computations, say nd-findall. Thus
*

*>
*

*> findall (\x -> x=:=y) where y = coin
*

*>
*

*> evaluates, non-deterministically, to either [0] or [1], whereas
*

*>
*

*> nd-findall (\x -> x=:=y) where y = coin
*

*>
*

*> evaluates, deterministically, to [0,1]
*

I don't think this will help. In fact, my point is that nd-findall cannot be

reasonably defined in Curry at all (but I forget to give you the explanation).

I'm going to elaborate a little bit more on the main' example in order to

show that the result of the evaluation would depend on the evaluation order.

f y = filter (/= y) (nd-findall (\x -> x=:=y))

main | z =:= f y & y =:= x = z where x,z free; y = coin

Admittedly, this is a little bit contrived. The idea is that y=coin can

either be evaluated in right conjunct, i.e. y=:=x. In this case the

non-determinism is occurring already outside of the encapsulated search and

nd-findall is called only with \x -> x=:=0 or \x -> x=:=1. In both cases the

findall result of f (and therefore main) is the empty list.

On the other hand, if the left conjunct is evaluated nd-findall

is going to evaluate the application of coin and returning the list [0,1]

(but without binding y outside the encapsulated search!). As the evaluation of

y was local to the encapsulated search, we have to evaluate y in the global

space again. And this time we get for y=0 the result [1] and for y=1 the

result [0].

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on Do Jan 10 2002 - 09:01:57 CET

Date: Wed, 09 Jan 2002 19:15:17 +0100

Hello Sergio,

sorry for being imprecise here. I did not mean that I wanted to defined

findall (and thus the encapsulated search) in pure term rewriting but was

referring to the model used to evaluate Curry expressions. In this case I

could always replace the lambda abstraction \x -> x=:=y by \x -> x=:=coin and

now the effect of findall would be to return the list [0,1].

Yes, but if I were using the goal

main2 = findall (\x -> x=:=coin)

the result will be the list [0,1].

Yes, this was what I meant by -- loosely -- saying two times the empty list.

Once for y=0 and once for y=1.

Hmmm, this was due to some incomplete change of the example. The lacking

definition was

same x y = x =:= y

But the problem is not related to this particular definition of same. In

fact, an binary (constraint) function which uses its first argument will work

(errr, not work as expected :-).

I don't think this will help. In fact, my point is that nd-findall cannot be

reasonably defined in Curry at all (but I forget to give you the explanation).

I'm going to elaborate a little bit more on the main' example in order to

show that the result of the evaluation would depend on the evaluation order.

f y = filter (/= y) (nd-findall (\x -> x=:=y))

main | z =:= f y & y =:= x = z where x,z free; y = coin

Admittedly, this is a little bit contrived. The idea is that y=coin can

either be evaluated in right conjunct, i.e. y=:=x. In this case the

non-determinism is occurring already outside of the encapsulated search and

nd-findall is called only with \x -> x=:=0 or \x -> x=:=1. In both cases the

findall result of f (and therefore main) is the empty list.

On the other hand, if the left conjunct is evaluated nd-findall

is going to evaluate the application of coin and returning the list [0,1]

(but without binding y outside the encapsulated search!). As the evaluation of

y was local to the encapsulated search, we have to evaluate y in the global

space again. And this time we get for y=0 the result [1] and for y=1 the

result [0].

Wolfgang

_______________________________________________

curry mailing list

curry_at_lists.RWTH-Aachen.DE

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

Received on Do Jan 10 2002 - 09:01:57 CET

*
This archive was generated by hypermail 2.3.0
: Mi Mai 25 2022 - 07:15:02 CEST
*