thanks for your replies!
>> This is similar and related to the
>> following: u = x?y implies f u = f (x?y) holds for term rewriting,
>> but not for Curry programs. Here is an example:
>>
>> test = (not u, not u)
>> where u = x?y
>> x = True
>> y = False
This example demonstrates that in Curry it is not valid to replace
variables with their bindings in the presence of non-determinism.
> The other question is of course the precise meaning of ``=''...
In the mentioned distributive property the equal sign denotes
"preservation of the set of results".
> But even if you set
>
> test v = (not v, not v)
> u = x ? y
>
> , you still have
>
> test u = test (x?y)
and even more:
test (x?y) = test x ? test y
I'll try to sum up the situation:
The semantics of Curry differs from standard term rewriting in the
presence of non-determinism. In term rewriting, we can safely replace
variables by their bindings, even if the variables are shared and the
bindings induce a non-deterministic branching. In Curry we are not
allowed to do so because of the call-time choice semantics. On the
other hand, the distributive properties
f (x?y) = f x ? f y
(f?g) x = f x ? g x
hold for Curry programs (without encapsulation) but not for term
rewriting! Consider
pair x = (x,x)
In Curry it is true that the expression
pair (True?False)
has the same results as
pair True ? pair False
namely (True,True) and (False,False). However, in term rewriting, the
first expression could evaluate to (True,False) and (False,True)
also. Distributivity does not hold here!
Cheers,
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Mi Jun 20 2007 - 09:36:25 CEST