- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

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

Date: Wed, 20 Jun 2007 13:13:40 +0000

Michael Hanus <mh_at_informatik.uni-kiel.de> wrote:

:-)

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

*
This archive was generated by hypermail 2.3.0
: Sa Okt 16 2021 - 07:15:04 CEST
*