Re: Confused Students

From: <kahl_at_cas.mcmaster.ca>
Date: Wed, 20 Jun 2007 13:13:40 +0000

Michael Hanus <mh_at_informatik.uni-kiel.de> wrote:
>
> kahl_at_cas.mcmaster.ca 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,

Wolfram
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Wed Jun 20 2007 - 18:28:14 CEST

This archive was generated by hypermail 2.3.0 : Mon Sep 23 2019 - 07:15:06 CEST