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