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 Mi Jun 20 2007 - 18:28:14 CEST