kahl_at_cas.mcmaster.ca wrote:
> > 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.
Sorry for the confusion. I sometimes tend to use "operation"
instead of "(defined) function" to avoid the discussion about
whether a nondeterministic function, i.e., one that delivers
more than one reult, should be called "function" or not.
Thus, I sometimes use the more neutral word "operation".
Thus, an operation is an entity defined by some program rule.
> 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.
Yes, this is a much better formulation.
Best regards,
Michael
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Do Jun 21 2007 - 12:27:30 CEST