# Re: Confused Students

From: Sebastian Fischer <sebf_at_informatik.uni-kiel.de>
Date: Wed, 20 Jun 2007 09:18:57 +0200

>> 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

This archive was generated by hypermail 2.3.0 : So Jan 26 2020 - 07:15:09 CET