Re: Local pattern declarations in Curry

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 Do Nov 12 1998 - 19:46:00 CET