Re: Confused Students

From: Sebastian Fischer <>
Date: Wed, 20 Jun 2007 09:18:57 +0200

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!


curry mailing list
Received on Mi Jun 20 2007 - 09:36:25 CEST

This archive was generated by hypermail 2.3.0 : Do Dez 03 2020 - 07:15:03 CET