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