Re: Confused Students

From: <>
Date: Wed, 20 Jun 2007 13:13:40 +0000

Michael Hanus <> wrote:
> wrote:
> > The other question is of course the precise meaning of ``=''...
> >
> >
> > The thing that does definitely not hold in Curry is substitution of equals:
> >
> > u = x?y does not imply t[v \ u] = t[v \ (x?y)].
> Here is again the precise meaning of "=" important.


> If "u = x?y" is a definition of an operation "u",
> then the implication holds, otherwise the substitution rule
> holds only for values or expressions having the same values.

BTW, why do you use the word ``operation'' here?
I just checked the Curry report, which uses the word sporadically,
without definition, and apparently at least occasionally
in a similarly strange way --- is it what in Haskell would be called
``variable bound by a pattern binding''?
In any case, in particular since ``u'' does not have to have
a function type or an explicitly monadic type,
I find the use of the word ``operation'' surprising.

Would you accept the following reformulation?

 | If "u = x?y" is a (desugared) program rule
 | (as opposed to a (derived) semantic equation),
 | then t[v \ u] = t[v \ (x?y)] holds as a semantic equation,
 | otherwise the substitution rule holds only for values,
 | or for expressions having the same SINGLE values.

It tries to make explicit how program rules,
which are used as rewriting rules,
connect the two worlds....

Best regards,

curry mailing list
Received on Mi Jun 20 2007 - 18:28:14 CEST

This archive was generated by hypermail 2.3.0 : Fr Sep 22 2023 - 07:15:08 CEST