Hi Wolfgang,
I dropped this issue, but it keeps coming back, so I'll try one
more time.
> I'm sorry Sergio, but I do not understand you problem here.
My fault. I should have explained it better. Sorry if this
message is long. First I change a bit your program to work only
with algebraic types, the usual integers are not defined by a
finite data declaration (but Brassel et al. showed that they could
be "declared").
t = let x free in (f x ? g x)
f True = success
g False = success
I also assume that both f and g are flexible or narrow their
argument.
Let (a/x) denote the substitution that maps x to a. t(True/x)
evaluates to success and so t(False/x). A complete strategy
evaluates t to success with computer answer (True/x) and likewise
(False/x).
t has 3 narrexes (4 steps). I think you disagreed with this
statement in the past, but I insist.
1. t -> let x free in f x
2. t -> let x free in g x
3. t -> success ? g (True ? False)
4. t -> f (True ? False) ? success
In the narrowing step, I bound the free variable x to (True ?
False) rather than only True or only False, because variables may
be shared (indeed x is shared in this case).
Each of these steps can be extended to a derivation that computes
an intended result. All this is good. In particular, the order
of evaluation does not affect the results of t. The last
statement is subtle, because depending on the first step some
computed expressions are not longer reachable, but the concept can
be satisfatorily formalized.
Now, here comes the twist.
Suppose that g is rigid or residuates on its argument. What are
the intended results of t? If t is equal to
(let x free in f x) ? (let x free in g x)
the the only result is success with (True/x). Then the
independence of the order of evaluation argued above is lost. The
derivations starting with steps 1 and 2 give the intended meaning,
step 4 is never computed, which is OK, but step 3 gives a wrong
result. Incompleteness problems with the order of evaluation are
not new, e.g., consider backtracking or see
http://www.informatik.uni-kiel.de/~pakcs/pitfalls.html. This is
the first case I know of unsoundness. Furthermore, the problem
originates from parallelism rather than lack of parallelism.
Are there simple, good solutions? Fixing the order of evaluation
is very bad. Banning residuation may be difficult because of
builtin types. Giving a declarative semantics for which the
variable x in (let x free in (f x ? g x)) is not shared seems
difficult as well. The only solution that I see at this time is
that the variable x in (let x free in (f x ? g x)) is indeed
shared. If this is not what the programmer intends, he can
simply code ((let x free in f x) ? (let x free in g x)).
Cheers,
Sergio
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Do Nov 08 2007 - 23:27:25 CET