On the implementation of
for non-free
Frédéri

onstru tion fun tions

on rete data types

1
2
3
Blanqui , Thérèse Hardin , and Pierre Weis

INRIA & LORIA, BP 239, 54506 Villers-lès-Nan y Cedex, Fran e
2
UPMC, LIP6, 104, Av. du Pr. Kennedy, 75016 Paris, Fran e
INRIA, Domaine de Volu eau, BP 105, 78153 Le Chesnay Cedex, Fran e

arXiv:cs/0701031v1 [cs.LO] 5 Jan 2007

1

3

Abstra t. Many algorithms use on rete data types with some additional invariants. The set of values satisfying the invariants is often a set
of representatives for the equivalen e lasses of some equational theory.
For instan e, a sorted list is a parti ular representative wrt ommutativity. Theories like asso iativity, neutral element, idempoten e, et . are
also very ommon. Now, when one wants to ombine various invariants,
it may be di ult to nd the suitable representatives and to e iently
implement the invariants. The preservation of invariants throughout the
whole program is even more di ult and error prone. Classi ally, the
programmer solves this problem using a ombination of two te hniques:
the denition of appropriate onstru tion fun tions for the representatives and the onsistent usage of these fun tions ensured via ompiler
veri ations. The ommon way of ensuring onsisten y is to use an abstra t data type for the representatives; unfortunately, pattern mat hing
on representatives is lost. A more appealing alternative is to dene a
on rete data type with private onstru tors so that both ompiler veri ation and pattern mat hing on representatives are granted. In this
paper, we detail the notion of private data type and study the existen e
of onstru tion fun tions. We also des ribe a prototype, alled Mo a,
that addresses the entire problem of dening on rete data types with
invariants: it generates e ient onstru tion fun tions for the ombination of ommon invariants and builds representatives that belong to a
on rete data type with private onstru tors.

1 Introdu tion
Many algorithms use data types with some additional invariants. Every fun tion
reating a new value from old ones must be dened so that the newly

reated

value satisfy the invariants whenever the old ones so do.
One way to easily maintain invariants is to use abstra t data types (ADT):
the implementation of an ADT is hidden and
tions are provided. A value of an ADT

onstru tion and observation fun -

an only be obtained by re ursively using

the

onstru tion fun tions. Hen e, an invariant an be ensured by using appropri-

ate

onstru tion fun tions. Unfortunately, abstra t data types pre lude pattern

mat hing, a very useful feature of modern programming languages [10, 11, 16,
15℄. There have been various attempts to

ombine both features in some way.

In [23℄, P. Wadler proposed the me hanisms of

views.

A view on an ADT

α is given by providing a on rete data type (CDT) γ and two fun tions in :
α → γ and out : γ → α su h that in ◦ out = idγ and out ◦ in = idα . Then,
a fun tion on α an be dened by mat hing on γ (by impli itly using in) and
the values of type γ obtained by mat hing an be inje ted ba k into α (by
impli itly using out). However, by leaving the appli ations of in and out impli it,
we an easily get in onsisten ies whenever in and out are not inverses of ea h
other. Sin e it may be di ult to satisfy this
translations between

artesian and polar

ondition ( onsider for instan e the

oordinates), these views have never

been implemented. Following the suggestion of W. Burton and R. Cameron
to use the

in

fun tion only [3℄, some propositions have been made for various

programming languages but none has been implemented yet [4, 17℄.
In [3℄, W. Burton and R. Cameron proposed another very interesting idea
whi h seems to have attra ted very little attention. An ADT must provide

on-

stru tion and observation fun tions. When an ADT is implemented by a CDT,
they propose to also export the

onstru tors of the CDT but only for using

them as patterns in pattern mat hing
underlying CDT
only the

lauses. Hen e, the

onstru tors of the

an be used for pattern mat hing but not for building values:

onstru tion fun tions

an be used for that purpose. Therefore, one

an

both ensure some invariants and oer pattern mat hing. These types have been
introdu ed in OCaml by the third author [24℄ under the name of

type with private onstru tors, or private data type (PDT)
Now, many invariants on

on rete data types

tional theory. Take for instan e the type of
Given some elements

v1 ..vn ,

an be related to some equa-

with the

onstru tors

the sorted list whi h elements are

ular representative of the equivalen e

x::y ::l=y ::x::l.

list

lass of

on rete data

for short.

v1 ::..::vn ::[]

v1 ..vn

[]

and

::.

is a parti -

modulo the equation

Requiring that, in addition, the list does not

ontain the same

x::x::l=x::l.
empty , singleton and

element twi e is a parti ular representative modulo the equation
Consider now the type of join lists with the onstru tors

append,

for whi h

on atenation is of

to asso iativity and

append

is

empty

stru ture of

onstant

ommutativity of

append.

orresponds to neutrality of

omplexity. Sorting

orresponds

Requiring that no argument of

empty

wrt

append.

We have a

ommutative monoid.

More generally, given some equational theory on a

on rete data type, one

may wonder whether there exists a representative for ea h equivalen e
if so, whether a representative of
that

t1 . . . t n

C(t1 . . . tn )

an be e iently

lass and,

omputed knowing

are themselves representatives.

In [21, 22℄, S. Thompson des ribes a me hanism introdu ed in the Miranda
fun tional programming language for implementing su h non-free

on rete data

types without pre luding pattern mat hing. The idea is to provide
rewrite rules,
newly

alled

laws, that are impli

reated value. This

tion fun tions (primed

onditional

itly applied as long as possible on every

an also be a hieved by using a PDT whi h

onstru -

onstru tors in [21℄) apply as long as possible ea h of

the laws. Then, S. Thompson studies how to prove the
dened by pattern mat hing on su h

lawful types.

orre tness of fun tions

However, few hints are given

on how to

he k whether the laws indeed implement the invariants one has in

mind. For this reason and be ause reasoning on lawful types is di ult, the law
me hanism was removed from Miranda.
In this paper, we propose to spe ify the invariants by unoriented equations
(instead of rules). We will

all su h a type a

relational data type

(RDT). Se -

tions 2 and 3 introdu e private and relational data types. Then, we study when
an RDT

an be implemented by a PDT, that is, when there exist

fun tions

omputing some representative for ea h equivalen e

onstru tion

lass. Se tion 4

provides some general existen e theorem based on rewriting theory. But rewriting may be ine ient. Se tion 5 provides, for some

ommon equational theories,

onstru tion fun tions more e ient than the ones based on rewriting. Se tion
6 presents Mo a, an extension of OCaml with relational data types whose

on-

stru tion fun tions are automati ally generated. Finally, Se tion 7 dis usses some
possible extensions.

2 Con rete data types with private onstru tors
We rst re all the denition of a rst-order term algebra. It will be useful for
dening the values of

on rete and private data types.

Denition 1 (First-order term algebra)

A

sorted term algebra denition is

S is a non-empty set of sorts, C is a non-empty
+
set of onstru tor symbols and Σ : C → S
is a signature mapping a non-empty
sequen e of sorts to every onstru tor symbol. We write C : σ1 . . . σn σn+1 ∈ Σ
to denote the fa t that Σ(C) = σ1 . . . σn σn+1 . Let X = (Xσ )σ∈S be a family
of pairwise disjoint sets of variables. The sets Tσ (A, X ) of terms of sort σ are

a triplet

A = (S, C, Σ)

where

indu tively dened as follows:

x ∈ Xσ , then x ∈ Tσ (A, X ).
C : σ1 . . . σn+1 ∈ Σ and ti ∈ Tσi (A, X ), then C(t1 , . . . , tn ) ∈ Tσn+1 (A, X ).
Tσ (A) be the set of terms of sort σ ontaining no variable.

 If

 If
Let

S0 of primitive types like int, string,
C0 of primitive onstants 0, 1, "foo", . . . Let Σ0 be the orresponding
(Σ0 (0) = int, . . . ).

In the following, we assume given a set
. . . and a set
signature

all on rete data type (CDT)
onstru tors. More formally:

In this paper, we
dened by a set of

Denition 2 (Con rete data type)

A

an indu tive type

à la

ML

on rete data type denition is a triplet

Γ = (γ, C, Σ) where γ is a sort, C is a non-empty set of onstru tor symbols and
Σ : C → (S0 ∪ {γ})+ is a signature su h that, for all C ∈ C , Σ(C) = σ1 ..σn γ .
The set V al(γ) of values of type γ is the set of terms Tγ (AΓ ) where AΓ =
(S0 ∪ {γ}, C0 ∪ C, Σ0 ∪ Σ).
This denition of CDTs

orresponds to a small but very useful subset of all

the possible types denable in ML-like programming languages. For the purpose
of this paper, it is not ne essary to use a more

omplex denition.

Example 1

4

The following type

onstru tors of sort

type

exp =

exp and

exp

is a CDT denition with two

a binary operator of sort

Zero | One | Opp of

exp | Plus of

onstant

exp exp exp.

exp *

exp

Now, a private data type denition is like a CDT denition together with
onstru tion fun tions as in abstra t data types. Constru tors
patterns as in

(ex ept in the denition of
use

annot

on rete data types but they

an be used as

be used for value

reation

onstru tion fun tions). For building values, one must

onstru tion fun tions as in abstra t data types. Formally:

Denition 3 (Private data type)

A

private data type denition

is a pair

Γ = (π, C, Σ) is a CDT denition and F is a family of onstru tion fun tions (fC )C∈C su h that, for all C : σ1 ..σn π ∈ Σ , fC : Tσ1 (AΓ ) ×
. . . × Tσn (AΓ ) → Tπ (AΓ ). Let V al(π) be the set of the values of type π , that

Π = (Γ, F )

where

is, the set of terms that one

an build by using the

f : Tπ (AΓ ) → Tπ (AΓ ) su h that,
ti ∈ Tσi (AΓ ), f (C(t1 ..tn )) = fC (f (t1 )..f (tn )), is
tion asso iated to F .
The fun tion

onstru tion fun tions only.

for all

C : σ1 ..σn π ∈ Σ

alled the

and

normalization fun -

This is quite immediate to see that:

Lemma 1.

V al(π) is the image of f .

PDTs have been implemented in OCaml by the third author [24℄. Extending a
programming language with PDTs is not very di ult: one only needs to modify
the

ompiler to parse the PDT denitions and

use of

he k that the

onditions on the

onstru tors are fullled.

Note that

onstru tion fun tions have no

onstraint in general: the full power

of the underlying programming language is available to dene them.
It should also be noted that, be ause the set of values of type
of the set of values of the underlying CDT

γ,

a fun tion on

π

π

is a subset

dened by pattern

mat hing may be a total fun tion even though it is not dened on all the possible
ases of

γ.

Dening a fun tion with patterns that mat h no value of type

not harm sin e the

orresponding

π

does

ode will never be run. It however reveals that

the developer is not aware of the distin tion between the values of the PDT and
those of the underlying CDT, and thus

an be

onsidered as a programming

error. To avoid this kind of errors, it is important that a PDT

omes with a

lear identi ation of its set of possible values. To go one step further, one
provide a tool for he king the
into a

ount the invariants, when it is possible. We leave this for future work.

Example 2

Let us now start our running example with the type

operations on arithmeti

4

ould

ompleteness and usefulness of patterns that takes

exp des

ribing

expressions.

Examples are written with OCaml [10℄, they an be readily translated in any programming language oering pattern-mat hing with textual priority, as Haskell, SML,
et .

type exp = private Zero | One | Opp of exp | Plus of exp * exp

exp is indeed a PDT built upon the CDT exp. Prompted by the
private, the OCaml ompiler forbids the use of exp onstru tors (outside the module my_exp.ml ontaining the denition of exp) ex ept in patterns.
If Zero is supposed to be neutral by the writer of my_exp.ml, then he/she will
This type

keyword

provide

onstru tion fun tions as follows:

let re zero = Zero and one = One and opp x = Opp x
and plus = fun tion
| (Zero,y) -> y
| (y,Zero) -> y
| (x,y) -> Plus(x,y)

3 Relational data types
We mentioned in the introdu tion that, often, the invariants upon

on rete data

types are su h that the set of values satisfying them is indeed a set of representatives for the equivalen e

lasses of some equational theory. We therefore propose

to spe ify invariants by a set of unoriented equations and study to whi h extent
su h a spe i ation

an be realized with an abstra t or private data type. In

ase of a private data type however, it is important to be able to des ribe the
set of possible values.

Denition 4 (Relational data type)
tion

A

relational data type (RDT) deni-

(Γ, E) where Γ = (π, C, Σ) is a CDT denition and E is a nite
set of equations on Tπ (AΓ , X ). Let =E be the smallest ongruen e relation ontaining E . Su h an RDT is implementable by a PDT (Γ, F ) if the family of
onstru tion fun tions F = (fC )C∈C is valid wrt E :
is a pair

(Corre tness) For all C : σ1 ..σn π and vi ∈ V al(σi ), fC (v1 ..vn ) =E C(v1 ..vn ).
(Completeness) For all C : σ1 ..σn σ, vi ∈ V al(σi ), D : τ1 ..τp σ ∈ Σ and
wi ∈ V al(τi ), fC (v1 ..vn ) = fD (w1 ..wp )

whenever

C(v1 ..vn ) =E D(w1 ..wp ).

We are going to see that the existen e of a valid family of

onstru tion fun -

tions is equivalent to the existen e of a valid normalization fun tion:

Denition 5 (Valid normalization fun tion)
is a

A map

valid normalization fun tion for an RDT (Γ, E)

with

f : Tπ (AΓ ) → Tπ (AΓ )
Γ = (π, C, Σ) if:

(Corre tness) For all t ∈ Tπ (AΓ ), f (t) =E t.
(Completeness) For all t, u ∈ Tπ (AΓ ), f (t) = f (u) whenever t =E u.
◦ f = f ) and
λxy.f (x) = f (y)).

Note that a valid normalization fun tion is idempotent (f
provides a de ision pro edure for

Theorem 6

=E

(the boolean fun tion

The normalization fun tion asso iated to a valid family is a valid

normalization fun tion.

Proof.
t ∈ Tπ . We have C :
σ1 ..σn π ∈ Σ and ti su h that t = C(t1 ..tn ). By denition, f (t) = fC (f (t1 )..
f (tn )). By indu tion hypothesis, f (ti ) =E ti . Sin e the family is valid and
f (t1 )..f (tn ) are values, fC (f (t1 )..f (tn )) =E C(f (t1 )..f (tn )). Thus, f (t) =E t.
Completeness. Let t, u ∈ Tπ su h that t =E u. We have t = C(t1 ..tn ) and u =
D(u1 ..up ). By denition, f (t) = fC (f (t1 )..f (tn )) and f (u) = fD (f (u1 )..f (up )).
By orre tness, f (ti ) =E ti and f (uj ) =E uj . Hen e, C(f (t1 )..f (tn )) =E
D(f (u1 )..f (up )). Sin e the family is valid and f (t1 )..f (tn ) are values, fC (f (t1 )
..f (tn )) = fD (f (t1 )..f (tn )). Thus, f (t) = f (u).


 Corre tness. We pro eed by indu tion on the size of



Conversely, given

f : Tπ (AΓ ) → Tπ (AΓ ), one an easily dene a family of
f is a valid normalization fun tion.

onstru tion fun tions that is valid whenever

Denition 7 (Asso iated family of onstr. fun tions)

Given a CDT Γ =
f : Tπ (AΓ ) → Tπ (AΓ ), the family of onstru tion fun tions asso iated to f is the family (fC )C∈C su h that, for all C : σ1 ..σn π ∈ Σ
and ti ∈ Tσ1 (AΓ ), fC (t1 , . . . , tn ) = f (C(t1 , . . . , tn )).

(π, C, Σ)

and a fun tion

Theorem 8

The family of

onstru tion fun tions asso iated to a valid normal-

ization fun tion is valid.

Example 3
Zero = x}
family of

We

an

hoose

exp

as the underlying CDT and

to dene a RDT implementable by the PDT

onstru tion fun tions

zero, one, opp, plus.

exp,

E = { Plus x
with the valid

4 On the existen e of onstru tion fun tions
In this se tion, we provide a general theorem for the existen e of valid families
of

onstru tion fun tions based on rewriting theory. We re all the notions of

rewriting and

ompletion. The interested reader may nd more details in [8℄.

Standard rewriting. A rewrite rule is an ordered pair of terms (l, r) written

l → r.

A rule is

left-linear if no variable o urs twi e in its left hand side l.
Pos(t) of positions in t is dened as a set of words on positive

As usual, the set

p ∈ Pos(t), let t|p be the subterm of t at position p and t[u]p be
t|p repla ed by u.
Given a nite set R of rewrite rules, the rewriting relation is dened as
follows: t →R u i there are p ∈ Pos(t), l → r ∈ R and a substitution θ su h
that t|p = lθ and u = t[rθ]p . A term t is an R-normal form if there is no u su h
that t →R u. Let =R be the symmetri , reexive and transitive losure of →R .
A redu tion ordering ≻ is a well-founded ordering (there is no innitely dereasing sequen e t0 ≻ t1 ≻ . . .) stable by ontext (C(..t..) ≻ C(..u..) whenever
t ≻ u) and substitution (tθ ≻ uθ whenever t ≻ u). If R is in luded in a redu tion
ordering, then →R is well-founded (terminating, strongly normalizing).
integers. Given

the term

t

with

→R is onuent if, for all terms t, u, v su h that u ←∗R t →∗R v ,
∗
∗
there exists a term w su h that u →R w ←R v . This means that the relation
∗
∗
∗
∗
←R →R is in luded in the relation →R ←R ( omposition of relations is written
We say that

by juxtaposition).
If

→R

is

onuent, then every term has at most one normal form. If

well-founded, then every term has at least one normal form. Therefore, if

→R
→R

is
is

onuent and terminating, then every term has a unique normal form.

Standard ompletion. Given

a nite set

≻, the standard Knuth-Bendix
set R of rewrite rules su h that:

dering
nite

• R is in luded in ≻,
• →R is onuent,
• R and E have same
Note that

E

of equations and a redu tion or-

ompletion pro edure [2℄ tries to nd a

=E = =R .

theory:

ompletion may fail or not terminate but, in

R-normalization provides a de
R-normal forms of t and u are synta

ase of su

termination,

ision pro edure for

i the

ti ally equal.

However, sin e permutation theories like

=E

essful

sin e

t =E u

ommutativity or asso iativity and

ommutativity together (written AC for short) are in luded in no redu tion
ordering, dealing with them requires to
modulo these theories and

onsider rewriting with pattern mat hing

ompletion modulo these theories. In this paper, we

restri t our attention to AC.

Denition 9 (Asso iative- ommutative equations)
C(x, y) = C(y, x). Then, let EAC

Com be the set of
E ontains an
be the subset of E made of

ommutativity and asso iativity equations for the

ommutative onstru tors,

ommutative

onstru tors,

equation of the form
the

=AC

be the smallest

i.e. the set of

ongruen e relation

onstru tors

ontaining

C

Let

su h that

EAC

and

E¬AC = E \ EAC .

Rewriting modulo AC. Given a set R of rewrite rules, rewriting with pattern

mat hing modulo AC

is dened as follows: t →R,AC u i there are p ∈ Pos(t),
l → r ∈ R and a substitution θ su h that t|p =AC lθ and u = t[rθ]p . A redu tion
′
′
′
ordering ≻ is AC - ompatible if, for all terms t, t , u, u su h that t =AC t and
′
′
′
u =AC u , t ≻ u i t ≻ u. The relation →R,AC is onuent modulo AC if
(←∗R,AC =AC →∗R,AC ) ⊆ (→∗R,AC =AC ←∗R,AC ).

Completion modulo AC.

Given a nite set

ompatible redu tion ordering
nite set

R

≻,

E

of equations and an

ompletion modulo

AC

AC -

[18℄ tries to nd a

of rules su h that:

• R is in luded in ≻,
• →R,AC is onuent modulo AC ,
• E and R ∪ EAC have same theory: =E = =R∪EAC .

Denition 10

A theory

E

has a

omplete presentation

patible redu tion ordering for whi h the
terminates.

AC -

if there is an AC- om-

ompletion of

E¬AC

su

essfully

Many interesting systems have a

omplete presentation: ( ommutative) mo-

noids, (abelian) groups, rings, et . See [13, 5℄ for a
automated tools implementing

atalog. Moreover, there are

ompletion modulo AC. See for instan e [6, 12℄.

R, AC -normal forms but, by
AC -equivalent and one an easily

A term may have distin t

AC ,

all normal forms are

normal form for

AC -equivalent

terms [13℄:

Denition 11 (AC -normal form)
C , C -left- ombs

stru tor

(resp.

onuen e modulo
dene a notion of

Given an asso iative and ommutative on-

C -right- ombs)

and their

leaves

are indu tively

dened as follows:
 If

t is not headed by C , then t is both a C -left-

omb and a

leaves of t is the one-element list leaves(t) = [t].

C -right-

omb. The

t is not headed by C and u is a C -right- omb, then C(t, u) is a C -right- omb.
leaves of C(t, u) is the list t :: leaves(u).
If t is not headed by C and u is a C -left- omb, then C(u, t) is a C -left- omb.
The leaves of C(u, t) is the list leaves(u)@[t], where @ is the on atenation.

 If

The


orient

Let

be a fun tion asso iating a kind of

ombs (left or right) to every AC-

≤ be a total ordering on terms. Then, a term t is in AC -normal
form wrt orient and ≤ if:
onstru tor. Let

 Every subterm of

t

headed by an AC- onstru tor

≤.
C(u, v)

C

is an

orient (C)-

omb

whose leaves are in in reasing order wrt

t of
u ≤ v.

 For every subterm of
asso iative, we have

As it is well-known, one

Theorem 12
t

has an

the form

with

AC -normal

an put any term in

form

t ↓AC

wrt

orient (C)
orient (C)

→A

is a

form:

orient and the ordering ≤ are, every term
orient and ≤, and t =AC t ↓AC .

Proof. Let A be the set of rules obtained by
 If

ommutative but non-

Whatever the fun tion

AC -normal

asso iativity equations of
 If

C

EAC

a

is left, then take

ording to

hoosing an orientation for the

orient :

C(x, C(y, z)) → C(C(x, y), z).
C(C(x, y), z) → C(x, C(y, z)).

is right, then take

onuent and terminating relation putting every subterm headed by

an AC- onstru tor into a
omputing the
the leaves of

A-normal

omb form a

ording to

ombs and the arguments of

ommutative but non-asso iative

≤.

Then, the fun tion

form of any term and

sort (comb(t)) =AC

stru tors to put them in in reasing order wrt
omputes the

AC -normal

orient . Let comb be a fun tion
sort be a fun tion permuting

form of a term. Let now

on-

sort ◦ comb
t.


AC -equivalen e: the fun λxy.sort (comb(x)) = sort (comb(y)). It follows that R, AC -normalization
together with AC -normalization provides a valid normalization fun tion, hen e
This naturally provides a de ision pro edure for

tion

the existen e of a valid family of

onstru tion fun tions:

Theorem 13
of

If

E

has a

omplete presentation, then there exists a valid family

onstru tion fun tions.

Proof. Assume that

E

has a

omplete presentation

R.

We dene the

om-

putation of normal forms as it is generally implemented in rewriting tools. Let

R, AC -rewrite step if there is one, or failing if the
norm be the fun tion applying step until a normal
form is rea hed. Sin e R is a omplete presentation of E , by denition of the
ompletion pro edure, sort ◦comb ◦norm is a valid normalization fun tion. Thus,

by Theorem 8, the asso iated family of onstru tion fun tions is valid.
step

be a fun tion making an

term is in normal form. Let

The

onstru tion fun tions des ribed in the proof are not very e ient sin e

they are based on rewriting with pattern mat hing modulo AC, whi h is NPomplete [1℄, and do not take advantage of the fa t that, by denition of PDTs,
they are only applied to terms already in normal form. We
whether they

an be dened in a more e ient way for some

an therefore wonder
ommon equational

theories like the ones of Figure 1.

Fig. 1. Some
Name
Abbrev

ommon equations on binary onstru tors

Denition

Example

asso iativity Assoc(C) C(C(x, y), z) = C(x, C(y, z)) (x + y) + z = x + (y + z)
ommutativity Com(C)
C(x, y) = C(y, x)
x+y = y+x
neutrality
N eu(C, E)
C(x, E) = x
x+0=x
inverse
Inv(C, I, E)
C(x, I(x)) = E
x + (−x) = 0
idempoten e Idem(C)
C(x, x) = x
x∧x=x
nilpoten e
N il(C, A)
C(x, x) = A
x ⊕ x = ⊥ (ex lusive or)

Rewriting provides also a way to

Theorem 14

he k the validity of

onstru tion fun tions:

has a omplete presentation R and F = (fC )C∈C is a family
C : σ1 ..σn π ∈ Σ and terms vi ∈ V al(σi ), fC (v1 ..vn ) is an
form of C(v1 ..vn ) in AC -normal form, then F is valid.

If

E

su h that, for all

R, AC -normal

Proof.
C : σ1 ..σn π ∈ Σ and vi ∈ V al(σi ). Sin e fC (v1 ..vn ) is an
C(v1 ..vn ), we learly have fC (v1 ..vn ) =E C(v1 ..vn ).
Completeness. Let C : σ1 ..σn π ∈ Σ , vi ∈ V alF (σi ), D : τ1 ..τp π ∈ Σ , and
wi ∈ V alF (τi ) su h that C(v1 ..vn ) =E D(w1 ..wp ). Sin e R is a omplete presentation of E , norm(C(v1 ..vn )) =AC norm(D(w1 ..wp )). Thus, fC (v1 ..vn ) =
fD (w1 ..wp ).


 Corre tness. Let

R, AC -normal



form of

It follows that rewriting provides a natural way to explain what are the
possible values of an RDT: values are
side of a rule of

R.

AC -normal

forms mat hing no left hand

5 Towards e ient onstru tion fun tions
When there is no

ommutative symbol,

onstru tion fun tions

an be easily

implemented by simulating innermost rewriting as follows:

Denition 15 (Linearization)

Let VPos(t) be the set of positions p ∈ Pos(t)
t|p is a variable x ∈ X . Let ρ : VPos(t) → X be an inje tive mapping
and lin(t) be the term obtained by repla ing in t every subterm at position
p ∈ VPos(t) by ρ(p). Let now Eq(t) be the onjun tion of true and of the
equations ρ(p) = ρ(q) su h that t|p = t|q and p, q ∈ VPos(t).
su h that

Denition 16

Given a set

stru tion fun tions

•

(fC )C∈C

R

of rewrite rules, let

F (R)

be the family of

on-

dened as follows:

l → r ∈ R with l = C(l1 , . . . , ln ), add to the denition of
\ , where b
fC the lause lin(l1 ), . . . , lin(ln ) when Eq(l) -> lin(r)
t is the term
obtained by repla ing in t every o urren e of a onstru tor C by a all to its
onstru tion fun tion fC .
• Terminate the denition of fC by the default lause x -> C(x).
For every rule

Theorem 17
Then,

F (R)

We now

Assume that

is valid wrt

E

onsider the

EAC = ∅

ase of

a modular way of dening the
example, with the type
ommutative only. The

and

E

has a

omplete presentation

(whatever the order of the non-default

R.

lauses is).

ommutative symbols. We are going to des ribe
onstru tion fun tions by pursuing our running

exp. Assume that Plus is de
onstru tion fun tions

lared to be asso iative and

an then be dened as follows:

let zero = Zero and one = One and opp x = Opp x
and plus = fun tion
| Plus(x,y), z -> plus (x, plus (y,z))
| x, y -> insert_plus x y
and insert_plus x = fun tion
| Plus(y,_) as u when x <= y -> Plus(x,u)
| Plus(y,t) -> Plus (y, insert_plus x t)
| u when x > u -> Plus(u,x)
| u -> Plus(x,u)
One

an easily see that

plus

sort ◦ comb
A-normalization

does the same job as the fun tion

used in Theorem 12 but in a slightly more e ient way sin e
and sorting are interleaved.

Zero is neutral. The AC- ompletion of { Plus(Zero, x)
{ Plus(Zero, x) → x}. Hen e, if x and y are terms in normal form,
Plus(x, y) an be rewritten modulo AC only if x = Zero or y = Zero.

Assume moreover that

= x}
then

gives

Thus, the fun tion

plus needs

to be extended with two new

lauses only:

and plus = fun tion
| Zero, y -> y
| x, Zero -> x
| Plus(x,y), z -> plus (x, plus (y,z))
| x, y -> insert_plus x y

Plus is de lared to have Opp as inverse. Then, the om{ Plus(Zero, x) = x, Plus(Opp(x), x) = Zero} gives
the following well known rules for abelian groups [13℄: { Plus(Zero, x) → x,
Plus(Opp(x), x) → Zero, Plus(Plus(Opp(x), x), y) → y , Opp(Zero) →Zero,
Opp(Opp(x)) → x, Opp(Plus(x, y)) → Plus(Opp(y),Opp(x)) }.
The rules for Opp are easily translated as follows:
Assume now that

pletion modulo AC of

and opp = fun tion
| Zero -> Zero
| Opp(x) -> x
| Plus(x,y) -> plus (opp y, opp x)
| _ -> Opp(x)
The third rule of abelian groups is
sin e it is obtained by rst adding the

alled an
ontext

extension

P lus([], y)

of the se ond one

on both sides of this

x and y in
(x, y) mat hes none of the three lauses previously
dening plus, that is, x and y are distin t from Zero, and x is not of the form
Plus(x1 , x2 ). To get the normal form of Plus(x, y), we need to he k that x and
the normal form of its opposite Opp(x) do not o ur in y . The last lause dening
se ond rule,then normalizing the right hand side. Take now two terms

normal form and assume that

plus needs

therefore to be modied as follows:

and plus = fun tion
| Zero, y -> y
| x, Zero -> x
| Plus(x,y), z -> plus (x, plus (y,z))
| x, y -> insert_opp_plus (opp x) y
and insert_opp_plus x y =
try delete_plus x y
with Not_found -> insert_plus (opp x) y
and delete_plus x = fun tion
| Plus(y,_) when x < y -> raise Not_found
| Plus(y,t) when x = y -> t
| Plus(y,t) -> Plus (y, delete_plus x t)
| y when y = x -> Zero
| _ -> raise Not_found
Forgetting about
tive,

Zero

and

Opp,

fun tion is modied as follows:

Plus is de lared asso iaplus is kept but the insert

suppose now that

ommutative and idempotent. The fun tion

and insert_plus x = fun tion
| Plus(y,_) as u when x = y -> u
| Plus(y,_) as u when x < y -> Plus(x,u)
| Plus(y,t) -> Plus (y,insert_plus x t)
| u when x > u -> Plus(u,x)
| u when x = u -> u
| u -> Plus(x,u)
Nilpoten e
In

an be dealt with in a similar way.

on lusion, for various

dene in a ni e modular way

ombinations of the equations of Figure 1, we

an

onstru tion fun tions that are more e ient than

the ones based on rewriting modulo AC. We summarize this as follows:

Denition 18

A set of equations E is a theory of type:
EAC = ∅ and E has a omplete presentation,
if E is the union of {Assoc(C), Com(C)} with either {N eu(C, E), Inv(C, I, E)},
{Idem(C)}, {N eu(C, E), Idem(C)} {N il(C, A)} or {N eu(C, E), N il(C, A)}.

(1) if
(2)

Two theories are disjoint if they share no symbol.
Let us give s hemes for
is generated only if the
These

onstru tion fun tions for theories of type 2. A
onditions

Neu(C,E), Inv(C,I,E),

onditions are not part of the generated

ode.

let f_C = fun tion
| E, x when Neu(C,E) -> x
| x, E when Neu(C,E) -> x
| C(x,y), z when Asso (C) -> f_C(x,f_C(y,z))
| x, y when Inv(C,I,E) -> insert_inv_C (f_I x) y
| x, y -> insert_C x y
and f_I = fun tion
| E -> E
| I(x) -> x
| C(x,y) -> f_C(f_I y, f_I x)
| x -> I x
and insert_inv_C x y =
try delete_C x y
with Not_found -> insert_C (f_I x) y
and delete_C x = fun tion
| Plus(y,_) when x < y -> raise Not_found
| Plus(y,t) when x = y -> t
| Plus(y,t) -> C(y, delete_C x t)
| y when y = x -> E
| _ -> raise Not_found

lause

et . are satised.

and insert_C x = fun tion
| C(y,_) as u when x = y & idem -> u
| C(y,t) when x = y & nil -> f_C(A,t)
| C(y,_) as u when x <= y & om -> C(x,u)
| C(y,t) when Com(C) -> C(y, insert_C x t)
| u when x > u & Com(C) -> C(u,x)
| u when x = u & Idem(C) -> u
| u when x = u & Nil(C,A) -> A
| u -> C(x,u)

Theorem 19

Let

E

Assume that, for all
Denition 16 if

be the union of pairwise disjoint theories of type 1 or 2.

C

onstru tor

k = 1,

Proof. Assume that E =

k , fC is dened as
(fC )C∈C is valid wrt E .

whi h theory is of type

and as above if

k = 2.

Then,

in

Sn

i=1 Ei where E1 , . . . , En are pairwise disjoint theories of type 1 or 2. Whatever the type of Ei is, we saw that Ei has a omplete

Ri . Therefore, sin e E1 , . . . , En share no symbol, by denition
of
Sn
AC - ompletion of E su essfully terminates with R = i=1 Ri .
Thus, →R,AC is terminating and AC - onuent. Sin e F = (fC )C∈C omputes
R, AC -normal forms in AC -normal forms, by Theorem 14, F is valid.


presentation

ompletion, the

The

onstru tion fun tions of type 2

an be easily extended to deal with ring

or latti e stru tures (distributivity and absorban e equations).
More general results
modularity of

an be expe ted by using or extending results on the

ompleteness for the

pleteness of hierar hi al

ombination of rewrite systems. The

om-

ombinations of non-AC -rewrite systems is studied in

[19℄. Note however that the modularity of

onuen e for

AC -rewrite systems has

been formally established only re ently in [14℄.
Note that the
same results with

onstru tion fun tion denitions of type 1 or 2 provide the
all-by-value,

The detailed study of the

all-by-name or lazy evaluation strategy.

omplexity of theses denitions ( ompared to AC-

rewriting) is left for future work.

6 The Mo a system
We now des ribe the Mo a prototype, a program generator that implements an
extension of OCaml with RDTs. Mo a parses a spe ial .mlm le

ontaining the

RDT denition and produ es a regular OCaml module (interfa e and implementation) whi h provides the

onstru tion fun tions for the RDT. Mo a provides

a set of keywords for spe ifying the equations des ribed in Figure 1.
For instan e, the RDT

exp

an be dened in Mo a as follows:

type exp = private Zero | One | Opp of exp | Plus of exp * exp
begin asso iative ommutative neutral(Zero) opposite(Opp) end
Mo a also features user's arbitrary rules with the

-> pattern.

These rules add extra

tions generated by Mo a: the LHS

onstru tion:

lauses in the denitions of

pattern

is

rule pattern

onstru tion fun -

opied verbatim as the pattern of

a

lause whi h returns the RHS

stru tors are repla ed by

pattern

alls to the

onsidered as an expression where

orresponding

ourse, in the presen e of su h arbitrary rules, we
tion or

ompleteness of the generated

for expert users that

ing set of rules. That way, the programmer
those whi h

annot guarantee the termina-

ode. This

an prove termination and

on-

onstru tion fun tions. Of

onstru tion is thus provided

ompleteness of the

an des ribe

orrespond-

omplex RDTs, even

annot be des ribed with the set of predened equational invariants.

Mo a also a

epts polymorphi RDTs and RDTs mutually dened with re ord

types (but equations between re ord elds are not yet available).
The equations of Figure 1 also support n-ary
unary

onstru tors of type

ment of type
instead of
ments: in a

exp list.

t list -> t.

In this

onstru tor, implemented as
ase,

Plus

Normal forms are modied a

gets a single argu-

ordingly and use lists

ombs. For instan e, asso iative normal forms get at lists of arguPlus(l) expression, no element of l is a Plus(l′) expression. The

orresponding data stru ture is widely used in rewriting.
Finally, Mo a oers an important additional feature: it

an generate onstru -

tion fun tions that provide maximally shared representatives. To re maximal
sharing, just add the

sharing

option when

ompiling the .mlm le. In this

ase, the generated type is slightly modied, sin e every fun tional
gets an extra argument to keep the hash

onstru tor

ode of the term. Maximally shared rep-

resentatives have a lot of good properties: not only data size is minimal and user's
memoized fun tions
is turned from a

an be light speed, but

omplex re ursive term

omparison between representatives

omparison to a pointer

omparison 

a single ma hine instru tion. Mo a heavily uses this property for the generation
of

onstru tion fun tions: when dealing with non-linear equations, the maximal

sharing property allows Mo a to repla e term equality by pointer equality.

7 Future work
We plan to integrate Mo a to the development environment Fo al [20℄. Fo al
units

ontain de larations and denitions of fun tions, statements and proofs

as rst- lass

itizens. Their

ompilation produ es both a le

theorem prover Coq [7℄ and a OCaml sour e
Coq or via the automati
it su

he kable by the

ode. Proofs are done either within

theorem prover Zenon [9℄, whi h issues a Coq le when

esses. Every Fo al unit has a spe ial eld, giving the type of the data ma-

nipulated in this unit. Thus, it would be very interesting to do a full integration
of private/relational data types in Fo al, the proof of

orre tness of

onstru tion

fun tions being done with Zenon or Coq and then re orded as a theorem to be
used for further proofs. This should be

ompleted by the integration of a tool

on rewriting and equational theories able to
to generate and prove the

omplete equational presentations,

orresponding lemmas and to show some termination

properties. Some experiments already done within Fo al on
and Zenon give a serious hope of su

A knowledgments. The authors thank Claude Kir

on a previous version of the paper.

oupling CiME [6℄

ess.

hner for his

omments

Referen es
1. D. Benanav, D. Kapur, and P. Narendran. Complexity of mat hing problems. J.
of Symboli Computation, 3(1-2):203216, 1987.
2. P. Bendix and D. Knuth. Computational problems in abstra t algebra, hapter
Simple word problems in universal algebra. Pergamon Press, 1970.
3. F. Burton and R. Cameron. Pattern mat hing with abstra t data types. J. of
Fun tional Programming, 3(2):171190, 1993.
4. W. Burton, E. Meijer, P. Sansom, S. Thompson, and P. Wadler. Views: An extension to Haskell pattern mat hing. http://www.haskell.org/extensions/views.
html, 1996.
5. P. Le Chenade . Canoni al forms in nitely presented algebras. Resear h notes in
theoreti al omputer s ien e. Pitman, 1986.
6. E. Contejean, C. Mar hé, B. Monate, and X. Urbain. CiME version 2.02. LRI,
CNRS UMR 8623, Université Paris-Sud, Fran e, 2004. http:// ime.lri.fr/.
7. Coq Development Team. The Coq Proof Assistant Referen e Manual, Version 8.0.
INRIA, Fran e, 2006. http:// oq.inria.fr/.
8. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor,
Handbook of Theoreti al Computer S ien e, volume B, hapter 6. North Holland,
1990.
9. D. Doligez. Zenon, version 0.4.1. http://fo al.inria.fr/zenon/, 2006.
10. D. Doligez, J. Garrigue, X. Leroy, D. Rémy, and J. Vouillon. The Obje tive Caml
system release 3.09, Do umentation and user's manual. INRIA, Fran e, 2005.
http:// aml.inria.fr/.
11. S. P. Jones (editor). Haskell 98 Language and Libraries, The revised report. Cambridge University Press, 2003.
12. J.-M. Gaillourdet, T. Hillenbrand, B. Lö hner, and H. Spies. The new Waldmeister
loop at work. In Pro . of CADE'03, LNCS 2741. http://www.waldmeister.org/.
13. J.-M. Hullot. Compilation de formes anoniques dans les théories équationnelles.
PhD thesis, Université Paris 11, Fran e, 1980.
14. J.-P. Jouannaud. Modular hur h-rosser modulo. In Pro . of RTA'06, LNCS 4098.
15. P.-E. Moreau, E. Balland, P. Brauner, R. Kopetz, and A. Reilles. Tom Manual
version 2.3. INRIA & LORIA, Nan y, Fran e, 2006. http://tom.loria.fr/.
16. P.-E. Moreau, C. Ringeissen, and M. Vittek. A pattern mat hing ompiler for
multiple target languages. In Pro . of CC'03, LNCS 2622.
17. C. Okasaki. Views for standard ML. In Pro . of ML'98.
18. G. Peterson and M. Sti kel. Complete sets of redu tions for some equational
theories. J. of the ACM, 28(2):233264, 1981.
19. K. Rao. Completeness of hierar hi al ombinations of term rewriting systems. In
Pro . of FSTTCS'93, LNCS 761.
20. R. Rioboo, D. Doligez, T. Hardin, and all. FoCal Referen e Manual, version 0.3.1.
Université Paris 6, CNAM & INRIA, 2005. http://fo al.inria.fr/.
21. S. Thompson. Laws in Miranda. In Pro . of LFP'86.
22. S. Thompson. Lawful fun tions and program veri ation in Miranda. S ien e of
Computer Programming, 13(2-3):181218, 1990.
23. P. Wadler. Views: a way for pattern mat hing to ohabit with data abstra tion.
In Pro . of POPL'87.
24. P. Weis. Private onstru tors in OCaml. http://alan.petitepomme.net/ wn/
2003.07.01.html#5, 2003.

