Re: Local pattern declarations in Curry

From: Herbert Kuchen <kuchen_at_uni-muenster.de>
Date: Thu, 12 Nov 1998 10:30:59 +0000

> Michael Hanus wrote:
>
> I would be happier if you provide a set of general transformation
> rules instead of explaining the transformation of individual examples.

Well, I was hoping that the general scheme was clear from theexamples and
the corresponding general remarks.
Below, I will try to explain it again.

> For instance, how do you transform the following example:
>
> coin = 0
> coin = 1
> f x = g xs where xs = (x,coin):xs
> xs = []

This would be translated to:

coin = 0
coin = 1
f x = h x
h x = g (xs1 x)
h x = g (xs2 x)
xs1 x = (x,coin):(xs1 x)
xs2 x = []

(assuming (according to our proposal) that the value of a
nullary function like coin is re-used
at all occurrences, i.e. coin is always 0 or always 1. (As I mentioned:
if you would like to have another behaviour, coin could be replaced
by a unary function with a dummy argument.)
Another translation without the above assumption (that the values
of nullary functions are re-used) is straightfoward.)


> Let me mention a final point. A weakness of your proposal
> is that syntactically identical global and local declarations
> 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

> Therefore, I think it is essential to explain the meaning of
> local declarations as syntactic sugar for something else
> (using some simple transformations), otherwise it might be
> too difficult to understand.

That is what the proposal was all about!I think the proposed semantics
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.)

This semantics can be implemented in different ways, e.g. by
1) translating the source program (as sketched above) in
  such a way that nested nullary functions are eliminated, and
2) by relying on the fact that the semantics
  of an unnnested program has property (*). (If this
  assumption should be avoided, a slightly modified scheme
  can be used)

Let me now try to explain the general translation scheme
in more detail (and hopefully clearer this time).
The very general scheme is a bit complicated and
rarely necessary in practice since mutually recursive
non-deterministic nullary
functions will hardly occur. Thus, I would like to start with
a scheme that handles the case of only one (possibly recursive)
non-deterministic nullary function. Let's assume the following
situation:

f ps = e where y = rhs_1
               ...
               y = rhs_n
               Rest (not containing y)

(where ps might be a sequence p1 ... p_k of patterns
containing variables x1 ... x_k. The sequence of these
variables is abbreviated by xs.)

this is translated to:

f ps = h xs
h xs = e[y/ y1 xs] where Rest
...
h xs = e[y/ y_n xs] where Rest
y1 xs = rhs_1[y/ y1 xs] where Rest
...
y_n xs = rhs_n[y/ y_n xs] where Rest


The (more) general case gets rather technical.

f ps = e where y_1 = rhs_1,1
               ...
               y_1 = rhs_1,n_1
               ...
               y_k = rhs_k,1
               ...
               y_k = rhs_k,n_k
               Rest (not containing y_i, i=1,...,k)

this is translated to:


f ps = h xs
h xs = e[y_1/ y_1,(1,...,1) xs, ..., y_k/ y_k,(1,...,1)] where Rest
...
h xs = e[y_1/ y_1,(n_1,...,n_k) xs, ..., y_k/ y_k,(n_1,...,n_k)] where
Rest

...
y_i,(j_1,...,j_k) = rhs_i,j_i[ y_1/ y_1,(j_1,...,j_k) xs, ..., y_k/
y_k,(j_1,...,j_k)]
                    where Rest
...

This should be sufficient to be able to understand the scheme.
In order to apply it to real programs, a few more things have to
be taken into account, like e.g. non-deterministic nullary
functions on different levels of nesting. They could be elimated
level by level.
Moreover, some y_i might occur on the right hand side in the
definition of a non-nullary function

g zs = rhs

in Rest. In this case, several versions

g_(j_1,...,j_k) = rhs[ y_1/ y_1,(j_1,...,j_k) xs, ..., y_k/
y_k,(j_1,...,j_k)]

are necessary. The generalization of the above scheme is straightforward.

I will not go into the details here.

Cheers,

Herbert
Received on Do Nov 12 1998 - 10:38:00 CET