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

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 Thu Nov 12 1998 - 10:38:00 CET

Date: Thu, 12 Nov 1998 10:30:59 +0000

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.

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.)

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

our proposed semantics is: 0 | 2

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 Thu Nov 12 1998 - 10:38:00 CET

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