Wolfgang Lux schrieb:
> Upon a second thought, I should correct myself. The only reasonable
> alternative to a rigid evaluation of non-local variables with a resumption
> of encapsulated search (as done in MCC), is a hyper-rigid getSearchTree
> primitive, which suspends until all free variables in its arguments are
> instantiated. Otherwise, the result of my example would depend on the
> order of evaluation in the conjuction
> y =:= head (tail solns) & lim =:= S (S Z)
> If evaluated from left to right this would fail because the non-local
> variable lim is uninstantiated and if evaluated from right to left the
> it would succeed and bind y to S Z because there no longer is a free
> variable in the search goal.
Okay, let's see how your example works within the framework proposed in
the WFLP-Paper. Maybe it is another reasonable alternative:
data Nat = Z | S Nat
le Z _ = success
le (S m) (S n) = le m n
notAbove n | m `le` n = m where m free
main =
do
let lim free
t <- getSearchTree (notAbove lim)
let solns = allValuesD t
x,y free
doSolve (x =:= head solns)
print x
doSolve (y =:= head (tail solns) & lim =:= S (S Z))
print y
As the evaluation of (notAbove lim) works on a local copy, there is no
problem in binding lim locally. Because of that, t in the above example
corresponds to
Or [Value Z, Or [Value (S Z), Or [Value (S (S Z)), Or [...]]]]
Therefore solns denotes [Z,S Z,S (S Z),...
and consequentially,
Z
S Z
is printed.
If you would continue main like this:
...
print y
t' <- getSearchTree (notAbove lim)
print t'
You would get another search tree, namely
Or [Value Z,Or [Value (S Z),Or [Value (S (S Z)),Fail]]]
Thus, the searchTree is conceptually defined in that moment in which
getSearchTree is called and cannot be changed "back in time". Thus,
nothing depends on the order of evaluation in the doSolve expressions
Is this so unreasonable? Apparantly not, judging form the last message:
>> Actually, this is what the mentioned paper describes. You can bind
>> non-local variables, but this binding is then only local. Conceptually,
>> strong encapsulation means making a copy of the whole evaluation state.
>
>
> Ah, I see. Somehow I have missed the point that fresh variables are
> used in the local search space. It's probably because there was never
> a disagreement about the handling of non-local variables with respect
> to the try primitive. I guess, I should fix MCC's implementation of
> getSearchTree.
But message exchange on this mailing list is a bit fast lately...
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Okt 14 2005 - 16:07:14 CEST