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

From: Sergio Antoy <antoy_at_cs.pdx.edu>

Date: Thu, 19 Dec 1996 21:00:54 -0800

This is a proposal to amend the December 5, 1996, definition of

Curry, Section 2.2, point 1.

Section 2.2 reads

To ensure that functions are well defined by a set of equations, a

valid Curry program must satisfy the following restrictions:

1. For each rule

f t1 ... tn := e if C

the left-hand side f t1 ... tn does not contain multiple

occurrences of a variable, and each variable occurring in the

right-hand side e must also occur in the left-hand side.

My proposal concerns the second and last part of this restriction,

"each variable occurring in the right-hand side e must also occur

in the left-hand side." Without this restriction, some equations

could define things that do not look like functions. The following

example

f := x if g(x)

g(a) := true

g(b) := true

shows that f evaluates to both a and b.

However, some programs that violate this restriction appear to be

well-behaved. Here is an example adapted from Bird & Wadler,

p. 34.

roots (a,b,c) := (r1,r2)

if r1 = (-b+r)/(2*a)

and r2 = (-b-r)/(2*a)

and d = b^2-4*a*c

and d >= 0

and r = sqrt d

Here, r1 and r2 are variables of the right-hand side that do not

appear in the left-hand side. The intuitive reason why this

program should be legal is that it is equivalent to the following

one where all the variables of the right-hand side appear in the

left-hand side.

roots (a,b,c) := ((-b+sqrt (b^2-4*a*c))/(2*a),

(-b-sqrt (b^2-4*a*c))/(2*a))

if b^2-4*a*c >= 0

What is the precise meaning of "functions are well defined?" Here

is my guess.

Functions are well defined if (legal) normal forms are unique.

More precisely, for every ground term t there exists at most one

data term d such that t is reducible to d.

Ground confluence is a sufficient condition for "functions are

well defined."

The restrictions on defining equations discussed next are based on

the following reference

Taro Suzuki, Aart Middeldorp, and Tetsuo Ida, Level-Confluence of

Conditional Rewrite Systems with Extra Variables in Right-Hand

Sides, Proceedings of the 6th International Conference on

Rewriting Techniques and Applications, Kaiserslautern, Lecture

Notes in Computer Science 914, pp. 179-193, 1995.

Initially, we will assume that the condition C of a rule is of the

form

s1=t1 and s2=t2 and ... and sn=tn

where s1, ..., sn are data terms. Conditions in this form are

said to be normal. Observe that the condition in the defining

equation of roots is not normal (due to the fourth conjunct).

Later, we will discuss how to transform this condition into an

equivalent normal condition.

Let

l := r if s1=t1 and ... and sn=tn (*)

be a defining equation such that some variable in r is not in l

and the condition, say C, is normal.

Every variable in r must be in l and/or C. R1

Equation (*) is said to be properly oriented if for all i in

1,...n

Var (ti) is contained in Var (l) union Var (sj),

for j in 1,...,i-1 R2

Observe that the defining equation of roots is not properly

oriented, e.g., t2 (i.e., (-b-r)/(2*a)) contains variable r that

is neither in l nor in s1.

In a properly oriented defining equation, the extra variables in

any conjunct of the condition are not really extra, since they

"are determined" by a previous conjunct. That is, one can replace

every extra variable in the defining equation right-hand side with

an equivalent term without extra variables (requires an induction

and possibly some new functions.)

More precisely, restrictions R1 and R2 (plus all the other that we

impose to Curry) ensure that a rewrite system is confluent and

thus imply that functions are well defined.

These restrictions are less restrictive than the current one, and

are rather easy to understand and check. Unfortunately, some

legal Haskell programs are still excluded, e.g.

f () = u

where u = h v

v = h u

h _ = 0

On the other hand, Haskell compiles and executes the following

program which does not make too much sense because of extra

variables.

f () = u

where u = h v

v = h u

h z = z

I think that further work to enable Curry to accept every

Haskell program (and perhaps more) is within reach.

Thus, I propose that for the time being, pending further study of

this issue, every program whose equations satisfy R1 and R2 is

legal. Furthermore, every program that can be transformed into a

legal program by means of a semantics preserving transformation is

legal, too.

There are some simple semantics preserving transformations,

intended to be performed by a compiler, that enlarge the set of

legal programs, e.g.,

(1) a conjunct g of a condition which is not an equation, is

interpreted as

true = g

(2) the conjuncts of a condition can be permuted

(3) a condition with two disjuncts can be split into two rules,

i.e.,

l := r if c1 or c2

is equivalent to

l := r if c1

l := r if c2

With these tranformations, the defining equation of roots becomes

legal, since it can be transformed into

roots (a,b,c) := (r1,r2)

if d = b^2-4*a*c

and true = d >= 0

and r = sqrt d

and r1 = (-b+r)/(2*a)

and r2 = (-b-r)/(2*a)

which satisfies R1 and R2

--------------------------------

Sergio Antoy

Dept. of Computer Science

Portland State University

P.O.Box 751

Portland, OR 97207

voice +1 (503) 725-3009

fax +1 (503) 725-3211

internet antoy_at_cs.pdx.edu

WWW http://www.cs.pdx.edu/~antoy

--------------------------------

Received on Fr Dez 20 1996 - 08:06:47 CET

Date: Thu, 19 Dec 1996 21:00:54 -0800

This is a proposal to amend the December 5, 1996, definition of

Curry, Section 2.2, point 1.

Section 2.2 reads

To ensure that functions are well defined by a set of equations, a

valid Curry program must satisfy the following restrictions:

1. For each rule

f t1 ... tn := e if C

the left-hand side f t1 ... tn does not contain multiple

occurrences of a variable, and each variable occurring in the

right-hand side e must also occur in the left-hand side.

My proposal concerns the second and last part of this restriction,

"each variable occurring in the right-hand side e must also occur

in the left-hand side." Without this restriction, some equations

could define things that do not look like functions. The following

example

f := x if g(x)

g(a) := true

g(b) := true

shows that f evaluates to both a and b.

However, some programs that violate this restriction appear to be

well-behaved. Here is an example adapted from Bird & Wadler,

p. 34.

roots (a,b,c) := (r1,r2)

if r1 = (-b+r)/(2*a)

and r2 = (-b-r)/(2*a)

and d = b^2-4*a*c

and d >= 0

and r = sqrt d

Here, r1 and r2 are variables of the right-hand side that do not

appear in the left-hand side. The intuitive reason why this

program should be legal is that it is equivalent to the following

one where all the variables of the right-hand side appear in the

left-hand side.

roots (a,b,c) := ((-b+sqrt (b^2-4*a*c))/(2*a),

(-b-sqrt (b^2-4*a*c))/(2*a))

if b^2-4*a*c >= 0

What is the precise meaning of "functions are well defined?" Here

is my guess.

Functions are well defined if (legal) normal forms are unique.

More precisely, for every ground term t there exists at most one

data term d such that t is reducible to d.

Ground confluence is a sufficient condition for "functions are

well defined."

The restrictions on defining equations discussed next are based on

the following reference

Taro Suzuki, Aart Middeldorp, and Tetsuo Ida, Level-Confluence of

Conditional Rewrite Systems with Extra Variables in Right-Hand

Sides, Proceedings of the 6th International Conference on

Rewriting Techniques and Applications, Kaiserslautern, Lecture

Notes in Computer Science 914, pp. 179-193, 1995.

Initially, we will assume that the condition C of a rule is of the

form

s1=t1 and s2=t2 and ... and sn=tn

where s1, ..., sn are data terms. Conditions in this form are

said to be normal. Observe that the condition in the defining

equation of roots is not normal (due to the fourth conjunct).

Later, we will discuss how to transform this condition into an

equivalent normal condition.

Let

l := r if s1=t1 and ... and sn=tn (*)

be a defining equation such that some variable in r is not in l

and the condition, say C, is normal.

Every variable in r must be in l and/or C. R1

Equation (*) is said to be properly oriented if for all i in

1,...n

Var (ti) is contained in Var (l) union Var (sj),

for j in 1,...,i-1 R2

Observe that the defining equation of roots is not properly

oriented, e.g., t2 (i.e., (-b-r)/(2*a)) contains variable r that

is neither in l nor in s1.

In a properly oriented defining equation, the extra variables in

any conjunct of the condition are not really extra, since they

"are determined" by a previous conjunct. That is, one can replace

every extra variable in the defining equation right-hand side with

an equivalent term without extra variables (requires an induction

and possibly some new functions.)

More precisely, restrictions R1 and R2 (plus all the other that we

impose to Curry) ensure that a rewrite system is confluent and

thus imply that functions are well defined.

These restrictions are less restrictive than the current one, and

are rather easy to understand and check. Unfortunately, some

legal Haskell programs are still excluded, e.g.

f () = u

where u = h v

v = h u

h _ = 0

On the other hand, Haskell compiles and executes the following

program which does not make too much sense because of extra

variables.

f () = u

where u = h v

v = h u

h z = z

I think that further work to enable Curry to accept every

Haskell program (and perhaps more) is within reach.

Thus, I propose that for the time being, pending further study of

this issue, every program whose equations satisfy R1 and R2 is

legal. Furthermore, every program that can be transformed into a

legal program by means of a semantics preserving transformation is

legal, too.

There are some simple semantics preserving transformations,

intended to be performed by a compiler, that enlarge the set of

legal programs, e.g.,

(1) a conjunct g of a condition which is not an equation, is

interpreted as

true = g

(2) the conjuncts of a condition can be permuted

(3) a condition with two disjuncts can be split into two rules,

i.e.,

l := r if c1 or c2

is equivalent to

l := r if c1

l := r if c2

With these tranformations, the defining equation of roots becomes

legal, since it can be transformed into

roots (a,b,c) := (r1,r2)

if d = b^2-4*a*c

and true = d >= 0

and r = sqrt d

and r1 = (-b+r)/(2*a)

and r2 = (-b-r)/(2*a)

which satisfies R1 and R2

--------------------------------

Sergio Antoy

Dept. of Computer Science

Portland State University

P.O.Box 751

Portland, OR 97207

voice +1 (503) 725-3009

fax +1 (503) 725-3211

internet antoy_at_cs.pdx.edu

WWW http://www.cs.pdx.edu/~antoy

--------------------------------

Received on Fr Dez 20 1996 - 08:06:47 CET

*
This archive was generated by hypermail 2.3.0
: Fr Okt 23 2020 - 07:15:02 CEST
*