Re: Confused Students

From: Michael Hanus <mh_at_informatik.uni-kiel.de>
Date: Thu, 21 Jun 2007 10:33:11 +0200

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 Thu Jun 21 2007 - 12:27:30 CEST

This archive was generated by hypermail 2.3.0 : Mon Nov 11 2019 - 07:15:07 CET