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

From: Michael Hanus <hanus_at_informatik.rwth-aachen.de>

Date: Thu, 12 Nov 1998 16:18:11 +0100

Herbert Kuchen wrote:

*> > might have a different meaning. For instance, consider the
*

*> > following definitions:
*

*> >
*

*> > coin = 0
*

*> > coin = 1
*

*> > f = coin
*

*> >
*

*> > Since f is a global function, the expression "f+f" reduces to 0|1|2.
*

*> > Now consider the expression "let f=coin in f+f". Since the local
*

*> > symbol f is a variable according your proposal, this expression
*

*> > reduces to 0|2.
*

*>
*

*> I do not understand this remark. In both examples, thevalue according to
*

*> our proposed semantics is: 0 | 2
*

Now I see what you mean. This was a misunderstanding probably due to the

lack of a set of general transformation rules explaining the precise

semantics. Let me summarize the important points.

We have the following facts for the kernel language:

1. A program is a set of functions defined by (conditional) rules.

2. Occurrences of the same variable in a rule denote the same values.

In particular, there is no notion of variable outside a rule

(I consider the initial goal as the rhs of some dummy rule).

There is a comprehensive theory (ESOP'96 paper by Madrid)

for this framework. Thus, every syntactic extension (like

local declarations) should be mapped into this kernel language.

My initial problem was the classification of locally introduced

symbols of the form "...where x=e...": should e be considered

as a variable or a function?

Firstly, I thought that you proposed to consider it always as a

variable (since there is no other option for the kernel language).

In particular, I thought that global 0-ary functions are still

functions since there is no other possibility. Now I learned

that you are intended to change the semantics even of existing

programs without local declarations to

*> is easy to understand:(*) the (once computed) value of a nullary function
*

*> is
*

*> re-used at every occurrence (within the same scope).
*

*> (It does not matter, whether the nullary function is defined
*

*> on top level or in some let or where clause.)
*

which means that 0-ary functions do not longer exist.

I understand it from an operational point of view, but could

you refer to some theory justifying this view?

Maybe the UC Madrid group can help?

If there is no such theory, we have to explain the meaning of this

view by mapping it into the kernel language. However, if you want to

consider top-level 0-ary functions also as shared, I think the

mapping becomes very complicated since I guess you have to

introduce auxiliary arguments for each 0-ary top-level function

to pass their values. For instance, how to you transform

a program like

coin = 0

coin = 1

...

f xs = ...coin...

g ys = ...coin...

...

and some more occurrences of coin in other rules. Sorry, but this

is not clear to me from your transformation rules.

Since there is no necessity to disallow top-level 0-ary functions

and a transformation is not so easy to understand (at least for me),

I think we should keep the current interpretation of programs

without local declarations as it is but require that in local

declarations the lhs is interpreted as a variable in the 0-ary case.

Of course, this comes with the restriction that these variable occurrences

cannot be recursive (as long as explicit graph structures are

not supported) but such cases can always be handled by

"globalizing" the definition or adding a dummy argument

like in your proposal (which turns them into a recursive function).

Such an interpretation has the advantage that no transformation

is necessary for programs without local declarations. Thus,

I think the semantics is simpler.

Best regards,

Michael

Received on Thu Nov 12 1998 - 19:46:00 CET

Date: Thu, 12 Nov 1998 16:18:11 +0100

Herbert Kuchen wrote:

Now I see what you mean. This was a misunderstanding probably due to the

lack of a set of general transformation rules explaining the precise

semantics. Let me summarize the important points.

We have the following facts for the kernel language:

1. A program is a set of functions defined by (conditional) rules.

2. Occurrences of the same variable in a rule denote the same values.

In particular, there is no notion of variable outside a rule

(I consider the initial goal as the rhs of some dummy rule).

There is a comprehensive theory (ESOP'96 paper by Madrid)

for this framework. Thus, every syntactic extension (like

local declarations) should be mapped into this kernel language.

My initial problem was the classification of locally introduced

symbols of the form "...where x=e...": should e be considered

as a variable or a function?

Firstly, I thought that you proposed to consider it always as a

variable (since there is no other option for the kernel language).

In particular, I thought that global 0-ary functions are still

functions since there is no other possibility. Now I learned

that you are intended to change the semantics even of existing

programs without local declarations to

which means that 0-ary functions do not longer exist.

I understand it from an operational point of view, but could

you refer to some theory justifying this view?

Maybe the UC Madrid group can help?

If there is no such theory, we have to explain the meaning of this

view by mapping it into the kernel language. However, if you want to

consider top-level 0-ary functions also as shared, I think the

mapping becomes very complicated since I guess you have to

introduce auxiliary arguments for each 0-ary top-level function

to pass their values. For instance, how to you transform

a program like

coin = 0

coin = 1

...

f xs = ...coin...

g ys = ...coin...

...

and some more occurrences of coin in other rules. Sorry, but this

is not clear to me from your transformation rules.

Since there is no necessity to disallow top-level 0-ary functions

and a transformation is not so easy to understand (at least for me),

I think we should keep the current interpretation of programs

without local declarations as it is but require that in local

declarations the lhs is interpreted as a variable in the 0-ary case.

Of course, this comes with the restriction that these variable occurrences

cannot be recursive (as long as explicit graph structures are

not supported) but such cases can always be handled by

"globalizing" the definition or adding a dummy argument

like in your proposal (which turns them into a recursive function).

Such an interpretation has the advantage that no transformation

is necessary for programs without local declarations. Thus,

I think the semantics is simpler.

Best regards,

Michael

Received on Thu Nov 12 1998 - 19:46:00 CET

*
This archive was generated by hypermail 2.3.0
: Wed Sep 18 2019 - 07:15:04 CEST
*