Syntactic Theories and the Algebra of Record Terms

Recently, many type systems for records have been proposed. For most of them, the types cannot be described as the terms of an algebra. In this case, type checking, or type inference in the case of first order type systems, cannot be derived from existing algorithms.

We define record terms as the terms of an equational algebra. We prove decidability of the unification problem for records terms by showing that its equational theory is syntactic. We derive a complete algorithm and prove its termination. We define a notion of canonical terms and approximations of record terms by canonical terms, and show that approximations commute with unification. We also study generic record terms, which extend record terms to model a form of sharing between terms. We prove that the equational theory of generic record terms and that the corresponding unification algorithm always terminates.

Théories syntaxiques et Algébres d’enregistrements

De nombreux systèmes de types pour les enregistrements ont été proposés récemment. Pour la plupart d’entre eux les types ne peuvent pas être décrits comme les termes d’une algèbre. La vérification de types, ou la synthèse de type dans le cas des systèmes de types d’ordre un, ne peuvent alors plus être déduits d’algorithmes connus.

Nous définissons les termes à enregistrements comme les termes d’une algèbre équationnelle. Nous prouvons la décidabilité du problème d’unification pour les termes d’enregistrements en montrant que sa théorie est syntaxique. Nous en déduisons un algorithme complet et prouvons sa terminaison. Nous définissons une notion de termes canoniques et l’approximation d’un terme d’enregistrement par des formes canoniques, et nous montrons que les approximations commutent avec l’unification. Nous étudions les termes d’enregistrements génériques qui étendent les termes d’enregistrements pour modéliser une forme de partage entre les termes. Nous montrons que la théorie équationnelle des termes d’enregistrements générique est syntaxique ainsi que la terminaison de l’algorithme correspondant.

Introduction

Type systems for records have been studied extensively in recent years. For most of them the types of records are no longer terms of an algebra. Consequently, results about unification, which yield, for example, algorithms for type inference in the case of first order languages, cannot be reused, and the problems have to be studied again from the beginning. Type inference for ML can be decomposed into two steps. The first step decomposes ML programs into unification constraints; it needs to know very little about the structure of types, as opposed to the second step which resolves the unification constrains. The author described a type system for polymorphic extensible records that uses terms of an algebra modulo equations for its types [Rém93]. Type inference for ML with sorted equational theory on types has been studied in [Rém92a]. The construction of the record algebra and its properties have been studied in [Rém90] but had not been published in English yet. Here, the results of [Rém90] are reviewed and their presentation is improved — the study is also extended to generic record terms.

Here, record terms are studied for themselves, independently any particular use. However, we motivate some of the constructions by their use as the types of a functional language with record objects. In this context we temporarily call them “record types”. They enable a natural extension of functional languages with records. One interest of extending functional languages with records is to have functions that can operate polymorphically on records with different sets of fields. Records are products of variable size with labeled components. The key idea is that types must reflect the structure of values and therefore record types must be products of different sizes with named components. Types of records carry information on all labels, but only a finite number of labels have different types, so type information can be finitely represented. More motivation can be found in [Rém93]. Types of records are often defined by constructing all fields at once. This requires the introduction of a collection of symbols {a_{1} : ; … a_{p} : } for all subsets of the set of labels (labels form a countable set). Record types with different sets of labels are completely incompatible types, which makes their unification quite difficult. On the contrary, record types are introduced with a symbol Π( ) and built field by field with symbols (a : ; ) , ending with constant symbol abs when there are no more fields to define. Two records types with some common set of fields, for instance (a : τ ; (b : σ ; α)) , and (a : τ ; abs ) can share some structure, namely the skeleton Π (a : ; ) . The fields of record types may be defined in any order, and commutativity equations are used to re-order fields. Some other kind of equations are also be needed to expand rows, for instance abs into (b : abs ; abs ) , so that the two record types may be unified.

Record types are thus types of an algebra taken modulo equations. Type inference in ML reduces to unification problems. Unification in the empty theory is well known, but there is no general algorithm for unification in an arbitrary equational theory. For some theories, there may not even exist such algorithm, or the algorithm may be inherently inefficient. Section 1 recalls definitions and a few results about equational theories. Since the basic problem is rewriting proofs of equality between terms to proofs of a certain shape, we introduce a notation of equality relation that allows the manipulation of sets of proofs that share the same pattern.

Fortunately, there is a class of equational theories, called syntactic theories, for which there exists a unification algorithm quite similar to the free unification algorithm of Martelli-Montanari [MM82]. There is no known algorithm to decide whether a theory is syntactic. The usual methods for proving syntacticness do not apply either. Section 2 briefly introduces syntacticness, and develops a framework for studying syntacticness properties of equational theories. The main result of this section is theorem 1; it gives a sufficient condition for syntacticness and is used in section 3 to prove that the theory of record terms is syntactic.

The theory of record terms is described in section 3. It is shown to be syntactic; this automatically provides a complete unification semi-algorithm, and we prove its termination. In fact record terms have more structure than required by their use as types of record objects. In section 4 we introduce canonical forms and show that record terms can be approximated by canonical forms. Approximations commute with unification. In section 5 we study an extension of record terms with more structure, the generic record terms, which are used as the types of projections in the language Projective ML [Rém92b].

The main results of this article are theorem 6 in section 3 and theorem 11 in section 5, which states the decidability of unification in the theories of record terms and generic record terms, respectively. A secondary result is the existence of principal approximations for record terms and their commutation with unification, stated by theorem 9. The method used for proving theorem 1 and lemma 35 is also interesting and can probably be reused in other situations.

1 Equational theories

This section introduces the main definitions and some known results about unification in equational theories.

1.1 Sorted Free Algebras

We are given a set K of atomic sorts, written ι. Signatures are non-empty tuples of sorts, written ι for a one-element signature or ι_{1} ⊗ … ι_{p} ⇒ ι_{0} for longer ones. The integer p (zero for a one element signature) is the arity of the signature. We are given a set of symbols C and a mapping S from C to the set of signatures. The arity of a symbol f is the arity of its signature, written ϱ(f). The sort of a symbol is the right-most sort of its signature. Finally, we are given a set of variables V with infinitely many variables of every sort (V^{ι})_{ι∈K}. The set of terms is the sorted free algebra T (V, S). The mapping S is also called the signature of the algebra. Variables are written with the letters α, β, γ, and δ, and terms with the letters τ, σ, and ρ.

The set of variables appearing in a term τ is written V(τ). We implicitly coerce a term τ into the set of its variables V(τ) when a set of variables is required. For instance, two terms are said to be disjoint if their sets of variables are disjoint. The top symbol of a non-variable term τ, written Top (τ), is the symbol at the empty occurrence in τ. For any symbol f of arity p, we write f(T^{p}) for the set of terms whose top symbol is f. The sort of a term is the sort of its top symbol. Two terms of the same sorts are said homogeneous.

Substitutions are sort-respecting mappings of finite domains from the set of variables to the set of terms. They naturally extend to mappings from terms to terms by compatibility with the structure of algebra. Substitutions are written with the letters μ, ν, and ξ. The domain of a substitution μ, written dom (μ), is the set of variables that are not their own images and the range of μ, written im (μ), is μ(dom (μ)). We say that a set of variables is disjoint from a substitution if it is disjoint from both the domain and the range of the substitution. We write μ |` W for the restriction of substitution μ to the set W, and μ \ W for the restriction of μ to the set V \ W.

1.2 Equational theories

It is important to distinguish between the presentation of an equational theory and the theory generated by the presentation. A presentation presentation of an equational theory is a set E of homogeneous pairs of terms called axioms. A congruence is an equivalence that is compatible with the structure of algebra. The E-equality on T generated by the presentation E, written =_{E}, is the smallest congruence containing all possible substitutions of the axioms. The equational theory equational theory T /E is the quotient of T by E. Several presentations may define the same equational theory (for instance, if one presentation extends the other with a pair of terms that can be proved equal in the equational theory the first).

We write q for an arbitrary axiom and q^{l} and q^{r} for its first and second projection, respectively. We often assume that presentations are closed under symmetry, and we write q^{−1} for the axiom (q^{r}, q^{l}).

1.3 Equality relations

The basic notion in studying equational theories, and in particular syntacticness, is the transformation of proofs. Equality relations are a formal way of manipulation proofs matching a certain pattern. The correctness of a proof transformation can be formalized by the assertion that one equality relation is a sub-relation of another.

We write τ_{/u} for the sub-term of τ at the occurrence u. We write τ[σ/u] for the term obtained from τ by replacing the subterm at the occurrence u by σ. Two terms τ and σ can be proved equal in one step if there exists an axiom q, an occurrence u, and a substitution μ such that τ_{/u} is μ(q^{l}) and σ_{/u} is μ(q^{r}). In this case, we write τ ⟶ σ. When more information is needed, we may write τ ⟶_{q/u} σ. The former relation is symmetric, but the latter is not.

We formalize and extend this notation below, so that it can be rigorously used in proofs.

An equality step equality step is any sub-relation of ⟶. Arbitrary equality steps are written ⟶_{X}, ⟶_{Y}, and ⟶_{Z}. An Equality relation is any composition of equality steps. They are sub-relations of =_{E}. Arbitrary equality relations are written X, Y and Z.

We write for Δ the identity relation. We write X^{δ} and δ ; ⟶ ; X for equality steps, the union of the relation X with the identity relation Δ. The composition composition equality relations of two equality relations X and Y, written X Y, relates any two terms τ and σ such that there exists a term ρ satisfying τ X ρ ∧ ρ Y σ. The union of two equality relations relates any two terms that can be proved equal by either of the relations.

If K is a totally ordered set and (X_{k})_{k∈K} is a sequence of equality relations equal to the identity after some rank N, we write

(X_{k})^{k∈K}  and  k ∈ K ; ⟶ ; X_{k}  for equality steps,

the composition of all relations taken in the increasing order. When X does not depend on

k we write X^{K} (or K ; ⟶ ; X) for short. We also write

X^{∗}  for  ⋃_{q∈IN} X^{q}  and  ∗ ; ⟶ ; X  for equality steps.

The E-equality is just \underrightarrow{∗}. For all terms τ and σ that are E-equal, there exists a sequence of relations

i ∈ [1, p] ; ⟶ ; X_{i}

and a sequence of terms (ρ_{i})_{i∈[1,p−1]} such that

τ ⟶_{X_{1}} ρ_{1} … ⟶_{X_{i}} ρ_{i} … ⟶_{X_{p−1}} ρ_{p−1} ⟶_{X_{p}} σ

Exhibiting these relations and these terms realizes a proof of τ =_{E} σ. We say that the proof

matches the relation i ∈ [1, p] ; ⟶ ; X_{i}.

Given two equality relations X and Y, we write X ⊂Y whenever X is a sub-relation of Y. Being a sub-relation can also be understood as set inclusion, viewing relations as their graphs, as we often do.

1.4 Paths

Occurrences are not enough precise. They define a subterm of a term, but are unable to tell anything about the symbols encountered on the way from the root to the subterm. A direction direction is a pair (f, x), also written f_{x}, of a symbol f and an integer x. A path path is a finite sequence of directions. We say that a path u equal to (f_{i}, x_{i})_{i∈[1,p]} is a path in τ, or that τ contains the path u, if

1. the occurrence (x_{i})_{i∈[1,p]} is an occurrence in τ, and

2. for all k in [1, p], the symbol f^{p} is at the occurrence (x_{i})_{i∈[1,p−1]}.

We write τ_{/u} for the subterm of τ at the occurrence (x_{i})_{i∈[1,p]}. We write ϵ for the empty path. Two paths are disjoint disjoint if neither is a prefix of the other. For instance, the sequence (f, 1)(g, 2) is a path, abbreviated as f_{1}g_{2}. The associated occurrence is the sequence 12 of length 2.

If q is the axiom (q^{l}, q^{r}) and u is a path, we write ⟶_{q/u} for the equality step that proves

τ[μ(q^{l})/u] =_{E} τ[μ(q^{r})/u]

for any term τ containing u and any substitution μ. If u is a path and τ ⟶_{q/u} σ a one step

proof, we get a proof τ_{/u} ⟶_{q/ϵ} σ_{/u}, called the sub-proof at path u.

Paths are much more precise than occurrences; sometimes they are too precise. An occurrence u can be considered as the set of all paths whose occurrences are u. The union of two equality steps ⟶_{q/u} and ⟶_{q/v} is an equality step. We write it ⟶_{q/u∪v}. More generally, we

write ⟶_{q/U} for

⋃_{u∈U} ⟶_{q/u}

when U is a set of paths. By default, U is the set of all paths and can be omitted.

Proposition 1 For any disjoint sets of paths U and V, the two equality steps ⟶_{U} and ⟶_{V} commute in T , that is

⟶_{U}⟶_{V} = ⟶_{V}⟶_{U}

The following notations help in manipulating sets of paths:

- We identify a path u with the singleton {u}.

- For any symbol f of non-zero arity p, we write for \underline{f} for the set of paths \{(f, x) | x ∈ [1, ϱ(f)]}.

- For any integer p, we write \underline{p} for the set of paths \{(f, p) | f ∈ C ∧ ϱ(f) ≥ p\}. For large values of p, this set may be empty.

- We write •• path for the path of length 1 composed of the set of all directions.

- If U and V are sets of paths, we write UV for the concatenation of U and V, composed of all the concatenations of any path of U with any path of V.

- We write U^{δ}δ path set for the union (ϵ ∪ U).

- If K is a totally ordered set and (U_{k})_{k∈K} is a sequence of path sets equal to ϵ after some rank N, we write (U_{k})^{k∈K} for the concatenation of all path sets (distinct from ϵ) and taken in the increasing order. When U does not depend on k and K is finite, we write U^{K} for short. We write U^{∗} for the union ⋃_{k∈IN} U^{k} and ∞ for (•^{∗}).

For instance, (•∞) denotes the set of all paths of length strictly greater than one. The union of the equality steps ⟶_{q/u} and ⟶_{s/u} is an equality step; it is written ⟶_{q∪s/u}.

That is, axioms are replaced by sets of axioms: If R is a subset of E, we write ⟶_{R/u} for the

equality step

⋃_{q∈R} ( ⟶_{q/u} )

By default, R is E and can be omitted. For example, the expression ∗ ; ⟶ ; •^{k}∞ δ ; ⟶ ; • relates any

two terms that are provably equal with any number of steps at a path of length at least k followed eventually by one step at the empty path.

The expression ⟶_{δ} ∗ ; ⟶ ; •∞⟶_{2∞} relates any two terms that are provably equal with one step at the empty path followed by any number of steps at non-empty paths and one step in the second direct subterm.

1.5 Restriction of equality relations

In the following, we will be interested in transforming proofs inside a subset of T . This is formalized by restriction of equality relations. The restriction of the equality step restriction equality step ⟶_{X} to a subset H of T , noted ⟶_{X|` H} is the relation ⟶_{X} ∩H^{2} in H. The restriction of the equality relation restriction equality relation X to a subset H of T , noted X |` H, is the equality relation X ∩ ∗ ; ⟶ ; |` H in H; it always relates terms that can be proved equal in H. If H is a subset of T , if τ and σ are in T , and if all auxiliary terms are in H, we say that the proof is a proof in Hproof in H.

The restriction to a set of terms H that is not closed under E-equality might be dangerous, in the sense that certain obvious properties in T might not hold in H. The reason is that restriction of an equality relation as we defined it is not the restriction of the relation in the usual meaning. If the set H is closed under E-equality, then the two notions coincide.

Definition 1 A subset H of T is closed closed if it contains all its subterms and satisfies

∀τ, σ ∈ H, ∀u ∈ dom (τ), (τ_{/u} ⟶ σ) ⟹ τ[σ/u] ∈ H.

In the rest of the article, we only allow the restriction of relations by closed subsets of T .

This does not imply that H is closed by E-equality (if τ is not in H, then σ[τ_{/u}] may not be in H), but at least it has two interesting properties:

• A subproof of a proof in H at a defined occurrence is a proof in H.

• Two steps at disjoint paths commute.

These properties are highly desirable before any serious surgery on proofs can be done.

We write X ⊂_{H} Y for X |` H ⊂ Y |` H and we say that X is a sub-relation of Y in H. The relation ⊂_{H} is reflexive and transitive.

1.6 Sorts and equational theories

Sorting terms is a common way of restricting the set of admissible terms. The addition of sorts to an equational theory can have two effects on unification:

• Since fewer terms can meet, difficult cases may sometimes disappear.

• There are fewer proofs, which can be either helpful or harmful. In some particular cases, all proofs between valid terms are valid proofs.

The first situation is unavoidable, because sorts are aimed at restricting the set of terms. It can only make unification easier. The second situation may have no effect, if all proofs between homogeneous terms are still permitted.

Let T be a set of terms, S a sort signature, and E an equational theory. We note T |` S the restriction of T by the signature S. In general, axioms of E may violate the sorts. We say that an axiom has sort ι if both left and right hand sides of the axiom have sort ι. We write E |` S the set of well-sorted axioms for S.

We are interesting in the comparison of equality in the two theories (T |` S)/(E |` S) and (T /E)|` S, that is, the comparison of the equality relations (⟶ ∩(T |` S)^{2})^{∗} and \underrightarrow{∗} ∩(T |` S)^{2}. In particular, when these relations are equal, any unification algorithm for T /E also solves unification in (T |` S)/(E |` S).

Definition 2 We say that a signature Σ and a presentation E are compatible compatible if, for all axioms q and all sorts ι,

Σ ⊢ q^{l} :: ι ⟺ Σ ⊢ q^{r} :: ι.

Proposition 2 If the presentation E is regular and compatible with the signature Σ, then the algebras (T /E) |` Σ and (T |` Σ)/(E |` Σ) are isomorphic.

\underline{Proof}: We show that (⟶ ∩(T |` Σ)^{2})^{∗} and \underrightarrow{∗} ∩ (T |` Σ)^{2} are equal. That is, any proof in T of equality between two terms in T |` Σ has all intermediate subterms in T |` Σ, which is a straight-forward consequence of the property

∀τ ∈ T |` Σ, ∀σ ∈ T , τ ⟶ σ ⟹ σ ∈ T |` Σ

For some axiom q and some occurrence u, τ/u matches q^{l}, that is, there exists some substitution μ such that τ_{/u} is equal to μ(q^{l}). Since τ is in T |` Σ, both q^{l} and the restriction of substitution μ to V(q^{l}) are well sorted. The restriction of μ to V(q^{r}) is identical to its restriction to V(q^{l}) because the theory is regular. Because of compatibility, q^{r} has the same sort as q^{l}. Thus τ[μ(q^{r})/u], that is, σ is well sorted.

The property is often used in one of the following two cases:

• The presentation E is well-sorted.

• The signature removes symbols in a way that is compatible with E.

2 Syntactic theories

Syntactic theories were introduced by C. Kirchner [Kir85].

Assumption In the rest of this article, we assume that the theory is collapse free, that is, there is no axiom composed of a variable on one side.

For any presentation E and any symbols f and g of respective arities p and q, we write E(f, g) the set E ∩ f(T^{p}) × g(T^{q}) of axioms whose top symbols are f and g, respectively.

Definition 3 A pair of symbols (f, g) is syntactic for the presentation E if, for all equal pairs of terms of f(T ) × g(T ), there is a proof of their equality that uses at most one axiom at the empty path. A presentation is syntactic if all pairs of symbols are. A theory is syntactic syntactic if there exists a syntactic presentation of this theory such that all sets E(f, g) are finite for all pairs of symbols (f, g).

For a presentation to be syntactic is equivalent to

\underrightarrow{∗} ⊂ ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞ .

Let H be a closed subset of T . We say that a presentation is syntactic in Hsyntactic in H if

\underrightarrow{∗} ⊂_{H} ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞ .

We write Synt (H) when the presentation is syntactic in H.

The presentation {f =_{E} g, g =_{E} h} is not syntactic, since the pair (f, h) is not (but the pair (f, g) is). However, the theory generated by the presentation is syntactic since the addition of the axiom f =_{E} h does not modify the theory and makes all pairs of symbols syntactic. The empty theory and the theory {f(g(α)) =_{E} g(α)} are syntactic, but the theory {f(g(α)) =_{E} f(α)} is not. Many examples can be found in [Kir85] and [KK89].

Some interesting questions are:

• Is a presentation syntactic?

• Is a theory syntactic?

• How to find a syntactic presentation of a syntactic theory.

• Minimalizing the set of axioms of a syntactic presentation.

The definition of syntactic theories is purely “syntactic,” but a semantic characterization was later found by C. Kirchner and F. Klay [KK89]. T. Nipkow showed that some proof transformations by rewriting techniques were closely related to syntactic presentations [Nip89]. All these studies help in understanding the second problem. A common instance of the third problem is the completion of a presentation into one that is syntactic; it has been thoroughly addressed by C. Kirchner. Our interest is only the first problem.

2.1 Sufficient conditions for commutativity

Proving that a presentation is syntactic usually requires some rearrangement of equality relations. The most frequent one is the commutation of two equality steps. The sufficient conditions fiven in section 2.2 require commutativity of consecutive equality steps of a certain shape. In general, two equality steps at disjoint paths commute. Here, we study the case when one occurrence is prefix of the other below.

Lemma 3 Let H be a closed subset of T . Let q be an axiom such that there is a variable α appearing exactly once in q^{r} at the occurrence u and appearing k times in q^{l} at occurrences (u_{j})_{j∈[1,k]}. Then for any axiom s and any occurrence v,

⟶_{q/ϵ}⟶_{s/uv} ⊂_{H} j ∈ [1, k] ; ⟶ ; s/u_{j}v⟶_{q/ϵ} .

\underline{Proof}: A proof matching ⟶_{q/ϵ}⟶_{s/uv} is of the form

μ(q^{l}) ⟶_{q/ϵ} μ(q^{r}) ⟶_{s/uv} μ(q^{r})[τ/uv].

Let α be q^{r}_{/u}. From the proof

μ(q^{r}) ⟶_{s/uv} μ(q^{r})[τ/uv],

we can extract the proof at u,

μ(α) ⟶_{s/v} μ(α)[τ/v],

and apply it to all disjoint occurrences (u_{j})_{j∈[1,q]} of α in q^{l}. Abbreviating μ(α)[τ/v] by σ,

μ(q^{l}) j ∈ [1, k] ; ⟶ ; s/u_{j}v μ(q^{l})[σ/u_{j}]_{j∈[1,k]}.

The right hand side of the above proof is equal to (μ \ {α} + (α ↦ σ))(q^{l}). Applying axiom q at occurrence ϵ gives (μ \ {α} + (α ↦ σ))(q^{r}), which is (μ \ {α})(q^{r})[τ/u] since u is the only occurrence of α in q^{r} (the linearity condition of q^{r} in α is needed here). By expansion of σ, this simplifies into μ(q^{r})[τ/uv].

Corollary 4 Let H be a closed subset of T . If q is a collapse-free axiom ^{1} such that there exists one variable appearing exactly once in q^{r} at the occurrence u, then for any axiom s,

⟶_{q/ϵ}⟶_{s/u∞} ⊂_{H} ∗ ; ⟶ ; s/•∞⟶_{q/ϵ}

\underline{Proof}: It suffices to notice that the occurrences (u_{j})_{j∈[1,q]} cannot be empty.

Corollary 5 Let H be a closed subset of T . If the presentation is collapse-free and all axioms are linear (regular and such that a variable occurs at most once in each side of axioms) of depth less or equal to n, then

⟶_{q/ϵ}⟶_{s/•^{n}∞} ⊂_{H} ⟶_{s/•∞}⟶_{q/ϵ} .

2.2 Sufficient conditions for syntacticness

Lemma 6 The property Synt (H) is equivalent to

⟶_{ϵ} ∗ ; ⟶ ; •∞⟶_{ϵ} ⊂_{H} ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞ .

1This condition is important here. Though it is assumed to be true throughout this section, it was not needed for the preceding lemma.

\underline{Proof}: The above condition is needed, since it is an instance of the condition Synt . We now assume the condition and prove Synt (H), that is,

\underrightarrow{∗} ⊂ ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞ .

The equality relation \underrightarrow{∗} can be decomposed into

⋃_{k∈IN} ( ∗ ; ⟶ ; •∞ (⟶_{ϵ} ∗ ; ⟶ ; •∞)^{k}) .

The inclusion

∗ ; ⟶ ; •∞ (⟶_{ϵ} ∗ ; ⟶ ; •∞)^{k} ⊂ ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞

is shown for all k by an easy induction on k.

Proposition 7 A sufficient condition for syntacticness in H is

∧ \{ \begin{matrix}⟶_{ϵ}⟶_{ϵ} ⊂_{H} ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞, \\ ⟶_{ϵ}⟶_{•∞} ⊂_{H} ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ . \end{matrix}

This condition was named ϵ-confluence by Claude Kirchner and proved in [Kir85]. The proof is very simple.

\underline{Proof}: Under the given assumptions, the inclusion

⟶_{ϵ} k ; ⟶ ; •∞⟶_{ϵ} ⊂_{H} ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞

for all k is easily shown by induction on k. By taking the union over all integers, we get

⋃_{k∈IN} ⟶_{ϵ} k ; ⟶ ; •∞⟶_{ϵ} ⊂_{H} ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞

That is,

⟶_{ϵ} ∗ ; ⟶ ; •∞⟶_{ϵ} ⊂_{H} ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞

We conclude by the lemma 6.

This proposition is composed of two conditions. The first is usually checked for all possible coverings of axioms. The second is commutativity, and might be deduced from lemma 3. However, the lemma only applies if axioms are of depth at most one. For instance, if one member of an axiom is of depth two, commutativity might not hold when one occurrence is prefix of the other. If axioms are collapse-free, linear, and of depth at most two, then the commutation

⟶_{ϵ}⟶_{••∞} ⊂ ∗ ; ⟶ ; ••∞ δ ; ⟶ ; ϵ

holds. Theorem 1 below generalizes proposition 7 to this case.

Remark 1 For any increasing sequence (H_{n})_{n∈IN} of closed subsets of T ,

(∀n ∈ IN, X ⊂_{H_{n}} Y)  implies  X ⊂_{H} Y  where  H = ⋃_{n∈IN} H_{n}

In particular this applies to the property Synt .

Definition 4 Let H be a closed subset of T . An ordering < is compatible with the equality relation on H if,

• for any term τ in H and any subterm σ of τ we have σ < τ,

• for all terms τ, σ, τ′ and σ′ in H, we have

(τ \underrightarrow{δ} τ′ ∧ σ \underrightarrow{δ} σ′ ∧ τ < σ) ⟹ τ′ < σ′.

An equational theory is strict if a term is never E-equal to one of its subterms. If there exists a compatible ordering, the theory is necessarily strict. The last condition is in fact equivalent to

(τ =_{E} τ′ ∧ σ =_{E} σ′) ⟹ (τ < σ ⇔ τ; < σ′)

In the following, we will always define compatible orderings by the means of a function from terms to an ordered set, namely IN; these functions will always be constant on E-equality classes.

Theorem 1 Let H be a closed subset of T with a well founded compatible ordering, and such that

⟶_{ϵ}⟶_{••∞} ⊂_{H} ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ  (h_{1})

⟶_{ϵ} ( δ ; ⟶ ; k)^{k∈D} ⟶_{ϵ} ⊂_{H} ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞  (h_{2})

Then Synt (H).

\underline{Proof}: For any integer n, let H_{n} be the subset of H composed of all terms that do not start any decreasing sequence of length greater than n. All these sets are closed under ⟶_{|` H}. In

particular, they are closed subsets of T , so properties (h_{1}) and (h_{2}) are valid in any (H_{n}). Any term smaller than a term in H_{n+1} is in H_{n}. The sequence is increasing and its limit is H, thus Synt (H) holds if Synt (H_{n}) holds for any n. We show Synt (H_{n}) by induction on n;

in fact, by lemma 6, it is enough to show that ⟶_{ϵ} ∗ ; ⟶ ; •∞⟶_{ϵ} ⊂_{H_{n}} ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞ holds.

The set H_{0} is composed of variables and constant symbols. Thus, the only instance of the premise is ⟶_{ϵ}⟶_{ϵ}, for which the inclusion is satisfied by the hypothesis (h_{2}).

Let us assume the property Synt (H_{n}) and prove Synt (H_{n+1}). Let D be the set of all directions. A relation ∗ ; ⟶ ; •∞ in H_{n+1} can be written as the composition

( ∗ ; ⟶ ; k∞)^{k∈D}

since disjoint occurrences commute. For each direction k in D, the subproof at k is in H_{n}. Since Synt (H_{n}), it can be rewritten in H_{n} so that it matches

∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞ .

Re-assembling all subproofs, we get a proof matching

( ∗ ; ⟶ ; k•∞ δ ; ⟶ ; kϵ ∗ ; ⟶ ; k•∞) ,^{k∈D}

which is a proof in H_{n+1}. It can be reordered as

( ∗ ; ⟶ ; k•∞)^{k∈D} ( δ ; ⟶ ; k)^{k∈D} ( ∗ ; ⟶ ; k•∞) .^{k∈D}

We have shown that

∗ ; ⟶ ; •∞ ⊂_{H_{n+1}} ( ∗ ; ⟶ ; k•∞)^{k∈D} ( δ ; ⟶ ; k)^{k∈D} ( ∗ ; ⟶ ; k•∞) .^{k∈D}

That is,

∗ ; ⟶ ; •∞ ⊂_{H_{n+1}} ( ∗ ; ⟶ ; ••∞) ( δ ; ⟶ ; k)^{k∈D} ( ∗ ; ⟶ ; ••∞) .

Composing the step at the root on both sides, and then using (h_{1}) and its symmetric image, we get

⟶_{ϵ} ∗ ; ⟶ ; •∞⟶_{ϵ} ⊂_{H_{n+1}} ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ( δ ; ⟶ ; k)^{k∈D} δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞

We conclude by a simple case analysis, using (h_{2}).

Proposition 7 and theorem 1 have two conditions. The first is a commutativity condition, and in general could be deduced from corollary 4. The second has to be proved by hand. However if the number of axioms is finite, the number of possible combinations of equality steps matching the premise is also finite. Thus it is possible to study each of them separately.

2.3 Example

The theory Cg where the only axiom is left commutativity is well known to be syntactic. We give a very short proof below. The axiom is:

x @ (y @ z) = y @ (x @ z)

The size of terms is unchanged by E-equality, which also defines a compatible ordering on T . The condition h_{1} is satisfied since the axiom is linear and the occurrence of non-variable terms is at most 1 (corollary 5). Two successive applications of the axiom at the empty occurrence annihilate each other. Since ⟶_{ϵ}⟶_{1} ⊂ ⟶_{21}⟶_{ϵ}, the only remaining case to consider in order to show (h_{2}) is ⟶_{ϵ}⟶_{2}⟶_{ϵ}, which is equal to ⟶_{2}⟶_{ϵ}⟶_{2}. The proof schema for this relation and its reduction is shown by the diagram below (any cycle is a subset of the identity relation).

β @ (α @ (γ @ δ)) −2−β @ (γ @ (α @ δ))
[figure: ϵ; ϵ]
α @ (β @ (γ @ δ))  γ @ (β @ (α @ δ))
[figure: 2; 2]
α @ (γ @ (β @ δ)) \begin{matrix} \\ − \\ − \\ − \\ ϵ \end{matrix}\begin{matrix}− \\ − \\ − \end{matrix} γ @ (α @ (β @ δ))

2.4 Unification in equational theories

In this section we describe how unification can be solved in syntactic theories. The problem of unification is, given a set of terms, to find a most general substitution that identifies all terms of the set. In fact, it is simpler to manipulate multi-sets of terms, called multi-equations. Since the satisfiability of a multi-equation is often reduced to the satisfiability of several multi-equations, it is also convenient to generalize unification problems to conjunctions of multi-equations called unificands.

Unificands are either multi-equations or conjunction or disjunction of unificands. They are written with letters U and V. Conjunction and disjunction of unificands are written U ∧V and U ∨ V, respectively. The set of solutions of a conjunction (respectively disjunction) of unificands is the intersection (respectively union) of the sets of solutions of the unificands. Thus it is possible to consider unificands equal modulo associativity and commutativity of ∧ and ∨ and modulo distributivity of one over the other. Then unificands can always be written as disjunctions of conjunctions of multi-equations.

It is also very convenient to restrict the set of solutions of a unificand U by some set of variables W. We write ∃ W · U for the unificand composed of these restrictions. The ∃ acts as a binder, and we consider unificands equal modulo renaming of variables bound by ∃’s, exchange of consecutive ∃’s, and removal of vacuous ∃’s. It is convenient to add a unificand ⊥ that has no solution and which is used to represent failure. Unificands were first introduced by C Kirchner [Kir85] and existential unificands were used later by J.-P. Jouannaud and C. Kirchner [KJ90]. A more abstract presentation of unificands can be found in [Rém92b].

A complete set of unifiers for a unificand U is a set S of solutions of U such that any other solution is an instance of at least one solution of S. An equational theory is unitary unifying if any solvable conjunction of multi-equations admits a complete set of solutions composed of a unique substitution. A general method for finding complete set of unifiers of a unificand U is to transform U into a simpler unificand that has exactly the same solutions. Thus, solving a unification problem is done by building a chain of equivalent unificands, each being obtained by rewriting the preceding one with a very simple rule.

Unification in the empty theory may be described by the rules of figure 1. Fusion merges

α ˙= e ∧ α ˙= e′ ; ------------------------------------------------------------------------------------------------------------------------------------------ ≻ ; α ˙= e ˙= e′ (Fuse) f(τ_{1}, … τ_{p}) ˙= f(β_{1}, … β_{p}) ˙= e ; --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- ≻ ; τ_{1} ˙= β_{1} ∧ … τ_{p} ˙= β_{p} ∧ f(β_{1}, … β_{p}) ˙= e (Decompose)

f(τ_{1}, … τ_{p}) ˙= g(σ_{1}, … σ_{q}) ˙= e ; ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- ≻ ; ⊥ (Fail) if f ≠ g,

(α ↦ τ)(e) ; ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- ≻ ; ∃ α · (e ∧ α ˙= τ) (Generalize) if α ∈ V(e) \ e \ V(τ) ∧ τ ∉ V,

Figure 1: Rules for unification in the empty theory

two multi-equations that share a common term variable into a single multi-equation. Collision reduces a multi-equation that contains two terms with different top symbols to the empty unificand ⊥. Decomposition splits a multi-equation that contains two non-variable terms with the same top symbol into a the conjunction of multi-equations composed of equations between the corresponding subterms. Generalization replaces a non-empty occurrence of a non-variable term τ in e by a variable α and adds the equation α ˙= τ. Generalization is used to reduce the height of terms in a unificand and prevent duplication of terms by other rules. For instance, if the right terms premise in rule Decompose were not variables, the conclusion would duplicate terms, which could prevent termination. It would be also possible to factor rules Decompose and Generalize into a single rule that would not require any term of the premise to be small. Below, we use an unrestricted form of generalization where τ may be a variable, called U-Generalize.

The four rules above applied in any order reduce any system of multi-equation to a completely decomposed one. A completely decomposed unificand is one for which no multiequation has more than one non-variable term. An equational theory is strict if a term can never be a sub-term of an E-equal term. In a strict theory, it is immediate to write an algorithm that tells whether a completely decomposed unificand is solvable, and that returns a principal unifier if one exists. See [Rém92b] for more details or [Kir85, Rém90] for a more thorough but slightly different presentation.

In equational theories, decomposition only fires for some pairs of symbols, called decomposable symbols. Collision fires only when the top symbols are incompatible. To be complete, there must be other transformations, called mutations, that together with previous rules reduce any unificand into a completely decomposed unificand. Mutation may not exist if there is no complete set of rules that can be added to fusion and decomposition and that terminate on any input with a completely decomposed system. Mutation often introduces disjunction of unificands.

Syntactic theories have a very simple mutation that, moreover, can be automatically deduced from a syntactic presentation of the theory. Multi-equations can always be reduced by looking at the top symbol of terms, which leads to efficient algorithms that are similar to the Martelli-Montanari unification algorithm in the empty theory [MM82].

Mutation in syntactic theories

In syntactic theories, the mutation is a generalization of decomposition and is derived from the form of the axioms.

Definition 5 Let E be a syntactic theory. Let τ and σ be two non-variable terms. We define decomposition of the equation τ ˙= σ to be the following system, written Dec (τ ˙= σ):

⋀_{i∈[1,p]} (τ_{/i} ˙= σ_{/i})

We define generalization of the equation τ ˙= σ to be the disjunction of systems

⋁_{q∈E(f,g)} (∃ V(q) · ⋀ \{ \begin{matrix}τ_{i} ˙= q^{l}_{/i} & i ∈ [1, p] \\ σ_{i} ˙= q^{r}_{/j} & j ∈ [1, q] \end{matrix} )

written Gen (τ ˙= σ), where the axioms of E(f, g) have been renamed so that they do not share any variable with the terms τ and σ. We define mutation of the equation τ ˙= σ to be the disjunction of systems

∨ \{ \begin{matrix}Gen (τ ˙= σ) ∨ Dec (τ ˙= σ) & if Top (τ) = Top (σ) \\ Gen (τ ˙= σ) & otherwise \end{matrix}

This system is written Mut (τ ˙= σ).

Theorem 2 If E is a syntactic presentation and τ and σ are two non variable terms, then

τ ˙= σ ; ------------------------------------------------------------ ≻ ; Mut (τ ˙= σ)

\underline{Proof}: The following is proved is [Kir85]. We first show that the reduction is correct. Let τ and σ be two terms and μ a solution of the equation τ ˙= σ. We show that μ satisfies Mut (τ ˙= σ). We use the following remark

∀τ, σ ∈ T , τ ∗ ; ⟶ ; •∞ σ ⟹ ⋀ \{ \begin{matrix}Top (τ) = Top (σ) \\ ∀i ∈ [1, ϱ(Top (τ))], τ_{/i} =_{E} σ_{/i} \end{matrix}

Since the theory is syntactic, there exists a proof of the form

τμ ∗ ; ⟶ ; •∞ τ′ δ ; ⟶ ; ϵ σ′ ∗ ; ⟶ ; •∞ σμ.

If there is no step at the empty occurrence, then the top symbols of τ and σ must be equal, and the system Dec (τ ˙= σ) is satisfied by μ. If one axiom q is used at the empty occurrence, it must be in E(Top (τ′), Top (σ′)), and there must be a substitution ν of domain V(q) for which

τ′ = ν(q^{l})  and  σ′ = ν(q^{r})

The substitution μ |` V(q) + ν is a solution of the system

⋀ \{ \begin{matrix}τ_{i} ˙= q^{l}_{/i} & i ∈ [1, p] \\ σ_{i} ˙= q^{r}_{/j} & j ∈ [1, q] \end{matrix}

It follows from the remark that q is in E(Top (τ), Top (σ)) and μ is a solution of Gen (τ ˙= σ).

Conversely, let us assume that μ is a solution of Mut (τ ˙= σ). If it is a solution of Gen (τ ˙= σ), then there is an axiom q of E(Top (τ), Top (σ)) and a substitution ν such that the substitution μ |` V(q) + ν is a solution of the system

⋀ \begin{cases}τ_{i} ˙= q^{l}_{/i} & i ∈ [1, p] \\ σ_{i} ˙= q^{r}_{/j} & j ∈ [1, q] \end{cases}

By composing the proofs of these equalities we get

\begin{matrix}(μ |` V(q) + ν)(τ) \underrightarrow{∗} (μ |` V(q) + ν)(q^{l}) \\ (μ |` V(q) + ν)(σ) \underrightarrow{∗} (μ |` V(q) + ν)(q^{r}) \end{matrix}

which simplifies to

μ(τ) \underrightarrow{∗} ν(q^{l})  and  μ(σ) \underrightarrow{∗} ν(q^{r})

Thus μ(τ) \underrightarrow{∗} μ(σ). The case where the top symbols are equal and μ is a solution of Dec (τ ˙= σ) is immediate.

To get an algorithm for solving unification, the existence of mutation is not sufficient; the termination of mutation together with the other rules must also be proved.

Remark 2 The presentation of left commutativity in the previous section is syntactic, but the corresponding mutation does not provide a unification algorithm since the mutation itself might not terminate. A solution is proposed in [Kir85].

3 Record terms

Record terms, used as types of record objects, enable a natural extension of functional languages with records. Records are products of variable size with labeled components. The key idea is that types must reflect the structure of values and therefore record types must be products of different sizes with named components. We first study a simplification of record terms obtained by forgetting labels and accessing components by position instead of by name: these structures are infinitary tuples.

3.1 Infinitary tuples

Let C be a set of symbols given with their arities (C_{n})_{n∈IN}. Let K be composed of

• a sort Type and

• a countable collection of sorts (Row(n))_{n∈IN}.

Let Σ be the signature composed of the following symbols, given with their sorts:

Σ ⊢ Π :: Row(0) ⇒ Type

Σ ⊢ f^{ι} :: ι^{ϱ(f)} ⇒ ι  f ∈ C, ι ∈ K
Σ ⊢ @^{n} :: Type ⊗ Row(n + 1) ⇒ Row(n)  n ∈ IN

Let E be the set of axioms

f^{Row(n)}(α_{1} @^{n} β_{1}, … α_{p} @^{n} β_{p}) = fType(α_{1}, … α_{p}) @^{n} f^{Row(n+1)(β_{1},...β_{p})}  (f ▷ n)

All axioms are collapse-free, regular and linear.

Let V be a denumerable set of variables with infinitely many variables of every sort.

Definition 6 The algebra of infinitary tuples is the equational theory T (Σ, V)/E.

The following two infinitary tuples are E-equal

Π |

@^{0}

[figure]
fType  g^{Row(1)} |  |
|
α  @^{1}
[figure]
β  γ

Π |

@^{0}

[figure]
fType  @^{1}

| [figure: |]

α gType  g^{Row(1)} |  |
|
β  γ

Theorem 3 The presentation E is syntactic.

\underline{Proof}: Lemma 7 is not sufficient because the commutativity condition is not satisfied; for instance the proof

fType(α_{i})_{I} @^{n} f^{Row(n)} ((β_{i})_{I} @^{n+1} (γ_{i})_{I})
[figure: ϵ; 2]
f^{Row(n+1)} (α_{i} @^{n} (β_{i} @^{n+1} γ_{i}))_{I}  fType(α_{i})_{I} @^{n} (fType(β_{i})_{I} @^{n+1} f^{Row(n+1)}(γ_{i})_{I})

where indexing expression _{i∈I} is written _{I} for short, cannot start with a step at the empty occurrence.

Of course, this proof is subsumed by the proof below for record terms. In particular, theorem 1 can be used, leading to a shorter proof, but it would require controlling terms with an ordering (as in the next section). In fact there would be no instance of the relation

⟶_{ϵ} ( δ ; ⟶ ; k)^{k∈IN} ⟶_{ϵ}

We give a direct proof. In fact we show that

⟶_{ϵ} n ; ⟶ ; •∞⟶_{ϵ} ⊂ n ; ⟶ ; •∞

by induction on n. We will use the following remarks, which are immediate consequences of the form of the axioms.

• Two successive steps at the empty occurrence must be inverse and they annihilate each other. This solves the initial case (n is zero).

• Two applications of axioms at disjoint occurrences, or at occurrences such that one is prefix of the other but at least too directions shorter, commute.

• A proof between two terms with the same top symbol cannot have exactly one step at the empty occurrence.

Let us assume that the property is true for n and consider a proof matching

⟶_{ϵ} n + 1 ; ⟶ ; •∞⟶_{ϵ}

We consider the subproof of n + 1 ; ⟶ ; •∞ at a direction i.

If it does not start or end with an application of an axiom at the empty occurrence, then this equality step commutes with one of the equality steps at the empty occurrence in the original proof. Thus the original proof is of the form ⟶_{ϵ} n ; ⟶ ; •∞⟶_{ϵ} 1 ; ⟶ ; •∞, and by induction

hypothesis it is also of the form n ; ⟶ ; •∞ 1 ; ⟶ ; •∞.

Otherwise, the subproof at occurrence i has at least two steps at the empty occurrence; thus it matches

⟶_{ϵ} p ; ⟶ ; •∞⟶_{ϵ} q ; ⟶ ; ∞

for some p and q whose sum is strictly smaller than n. By the induction hypothesis, this relation is a sub-relation of

p ; ⟶ ; •∞⟶_{ϵ} q ; ⟶ ; ∞

Re-composing this with the original proof, the problem reduces to previous case.

The mutation for the infinitary tuple algebra:

f^{Row(n)}(σ_{i})_{i∈[1,p]} ˙= (α @^{n} γ) ˙= e ; ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- ≻

∃ (α_{i}, γ_{i})_{i∈[1,p]} · ⋀ \{ \begin{matrix}(α @^{n} γ) ˙= e \\ α ˙= fType(α_{i})_{i∈[1,p]} \\ γ ˙= f^{Row(n+1)}(γ_{i})_{i∈[1,p]} \\ σ_{i} ˙= α_{i} @^{n} γ_{i}  for  i ∈ [1, p] \end{matrix}

Mutate

For all other pairs of terms (τ, σ), if they have identical top symbols, they are decomposable, otherwise they produce a collision. Mutation rules can be generalized as shown above.

Theorem 4 Unification in the infinitary tuple algebra is decidable and unitary unifying.

\underline{Proof}: The theory is strict (we can find a compatible ordering as we will do below for record terms). Therefore, the rules of mutation, decomposition, collision, fusion and generalization applied any order form a complete semi-algorithm for unification. It is unitary since mutation does not introduce any disjunction. It remains to prove termination.

Let T^{n} be the subsets of T restricted to the sorts Type and Row(k) for k smaller or equal to n. Generalized decompositions and fusion are stable on the sets T^{n}, and for a system of unificands they decrease in the following lexicographic ordering:

• the number of symbols f^{Row(n)} in the lexicographic order of increasing n,

• the number of all other symbols,

• the sum of heights of terms of the unificand,

• the number of multi-equations.

This guarantees the termination of the rewritting process.

Remark 3 The introduction of an infinite collection of copies of the original set of symbols C might be considered luxurious, while two copies Type and Row would seem sufficient. The main symbol @ would have signature Type ⊗ Row ⇒ Row. The axioms would be

fRow (α_{1} @^{n} β_{1}, … α_{p} @^{n} β_{p}) = fType(α_{1}, … α_{p}) @ f^{Row(β_{1},...β_{p})}

But even if the presentation remained syntactic, termination could not be guaranteed as above.

Remark 4 We can consider the set of raw terms, that is, the algebra T′ built from the all symbols C extended with a binary symbol @ and a unary symbol Π. To any term τ in T there corresponds a raw term obtained from τ by removing all superscripts of symbols. Conversely, for any raw term τ′ and any sort ι, there is at most one term of sort ι whose erasure is τ′. This allows us to define a term of T by giving its erasure and its sort.

3.2 Record terms

We generalize the theory of infinitary tuples to the theory of record terms, where components are named. We describe the theory and show that it is syntactic and that unification is decidable.

The algebra of record terms is define relatively to a collection of symbols given with their arities (C_{n})_{n∈IN}. Let L be a countable set of labels. Labels are written a, b, c and ℓ, finite subset of L are written L and K the set of all of them is written P_{f}(L). We also write a.L for {a} ∪ L.

Let K be the set composed of

• a sort Type, and

• a finite collection of sorts (Row(L)_{L∈P_{f} (L)}.

Let Σ be the signature composed of the following symbols given with their sorts:

Σ ⊢ Π :: Row(∅) ⇒ Type

Σ ⊢ f^{ι} :: ι^{ϱ(f)} ⇒ ι  f ∈ C, ι ∈ K
Σ ⊢ (ℓ^{L} : ; ) :: Type ⊗ Row(ℓ.L) ⇒ Row(L)  ℓ ∈ L, L ∈ P_{f}(L \ {ℓ})

We define projection symbols to be all symbols (ℓ^{L} : ; ). We write D for the new set of symbols.

Let E be the set of axioms composed of:

• Left commutativity axioms. For any labels a and b and any finite subset of labels L that do not contain them,

a^{L} : α ; (b^{a.L} : β ; γ) = b^{L} : β ; (a^{b.L} : α ; γ)  (a ▷ b, L)

• Distributivity axioms. For any symbol f, any label a and any finite subset of labels L that do not contain a,

f^{Row(L)}(a^{L} : α_{1} ; β_{1}, … a^{L} : α_{p} ; β_{p}) = a^{L} : fType(α_{1}, … α_{p}) ; f^{Row(a.L)}(β_{1}, … β_{p})

(f ▷ a, L)

All axioms are collapse-free, regular and linear.

Let V be a denumerable set of variables with infinitely many variables of every sort.

Definition 7 The algebra of record terms (also called the record algebra) is the equational theory T (Σ, V)/E.

Below are two E-equal record terms:

Π |

(a^{∅})

[figure]
fType  g^{Row({a})} |  |
|
α  (b^{{a}})
[figure]
β  γ

Π |

(a^{∅})

[figure]
fType  (b^{{a}})

| [figure: |]

α gType  g^{Row({a})} |  |
|
β  γ

Theorem 5 The presentation E is syntactic.

\underline{Proof}: Let T^{n} be the subset of terms that use only the sorts Type or Row(L), where Card (L) is at most n. The sequence of these sets is increasing and its union is T . Thus it is enough to show Synt (T_{n}) for any integer n. Let n be an integer. We show Synt (T^{n}) using theorem 1.

Let Θ_{n} be the usual size (sum of weights of symbols) where symbols are weighted as follows. Symbols f^{Row(L)} of arity q have a weigh of 2 ∗ (n − Card L) + q. Symbols fType weigh their arity q augmented by 1, and all other symbols weight 1. The size of a term is strictly larger than the size of any of its subterms; the size is constant on E-equality classes. Thus it defines a compatible ordering in T^{n} by τ < σ if Θ_{n}(τ) < Θ_{n}(σ).

The condition (h_{1}) is always satisfied: left commutativity axioms are of depth greater than two, and so are distributivity axioms for symbols of non zero arity. Left distributivity axioms for constant symbols f are such that the equality relations ⟶_{f▷a,L/ϵ}⟶_{••∞} are empty.

The condition (h_{2}) is

⟶_{ϵ} ( δ ; ⟶ ; k)^{k∈D} ⟶_{ϵ} ⊂_{H} ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞

We show it for all instances of the premise:

⟶_{q/ϵ} ( δ ; ⟶ ; s_{k}/k)^{k∈D} ⟶_{t/ϵ}

We write Z for the intermediate relation

( δ ; ⟶ ; s_{k}/k)^{k∈D}

Case Z is empty: The axioms q and t must be inverse and annihilate each other, that is, the equality relation is included in the identity relation Δ.

Case q is (f ▷ a, L): If f were of arity zero, S would be empty (first case). The occurrence 1 in s is not possible, and s_{2} must be another axiom (f ▷ b, a.L), where b is distinct from a. Then t must be the axiom (a ▷ b, L). We conclude with:

\overrightarrow{f ▷ a, L/ϵ}\overrightarrow{f ▷ b, a.L/2}\overrightarrow{a ▷ b, L/ϵ} ⊂ i ∈ [1, ϱ(f)] ; ⟶ ; a ▷ b, L/i\overrightarrow{f ▷ b, L/ϵ}\overrightarrow{f ▷ a, b.L/2}

Case q is (a ▷ f, L): Then t must be (f ▷ b, L). If a and b were equal, Z would be the identity (first case). At least one application of an axiom (a ▷ b, L) at each occurrence i between 1 and the arity of f is needed to change the symbols (a^{L} : ; ) into (b^{L} : ; ). We conclude with:

\overrightarrow{a ▷ f, L/ϵ} i ∈ [1, ϱ(f)] ; ⟶ ; a ▷ b, L/i\overrightarrow{f ▷ b, L/ϵ} ⊂ \overrightarrow{f ▷ b, L/2}\overrightarrow{a ▷ b, L/ϵ}\overrightarrow{a ▷ f, L/2}

Case q is (a ▷ b, L): If t is a distributivity axiom, then by symmetry we fall into one of the preceding case; otherwise it is an axiom (c ▷ b, L). Since 1 is a variable occurrence of q, the rule ⟶_{s_{1},1} commutes with q, and we ignore this case. If c and a were equal, the sequence Z

would be the identity (first case). So t must be the axiom (a ▷ c, b.L). We conclude with:

\overrightarrow{a ▷ b, L/ϵ}\overrightarrow{a ▷ c, b.L/2}\overrightarrow{b ▷ c, L/ϵ} ⊂ \overrightarrow{b ▷ c, a.L/2}\overrightarrow{a ▷ c, L/ϵ}\overrightarrow{a ▷ b, c.L/2}

Note that the two first inclusions can be deduced from the following cycle (any composition of six of these rules is a subset of the identity relation):

− a ▷ b, L, ϵ −

[figure: f ▷ b, a.L, 2; a ▷ f, b.L, 2]

[figure: f ▷ a, L, ϵ; b ▷ f, L, ϵ]

− \begin{matrix}i ∈ [1, ϱ(f)] \\ b ▷ a, L, i \end{matrix} \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}

The last inclusion rule forms the cycle:

− a ▷ c, b.L, 2 −

[figure: a ▷ b, L, ϵ; b ▷ c, L, ϵ]

[figure: c ▷ b, a.L, 2; b ▷ a, c.L, 2]

− \begin{matrix}i ∈ [1, ϱ(f)] \\ c ▷ a, L, ϵ \end{matrix} \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}

Since the theory is syntactic, we automatically derive the mutation rule in the record term algebra:

f^{Row(L)}(σ_{i})_{i∈[1,p]} ˙= a^{L} : α ; β ˙= e ; ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- ≻

∃ (α_{i}, β_{i})_{i∈[1,p]} · ⋀ \{ \begin{matrix}a^{L} : α ; β ˙= e \\ α ˙= fType(α_{i})_{i∈[1,p]} \\ β ˙= f^{Row(a.L)}(β_{i})_{i∈[1,p]} \\ σ_{i} ˙= a^{L} : α_{i} ; β_{i}  for  i ∈ [1, p] \end{matrix}

Mutate(a ▷ f)

a^{L} : τ ; σ ˙= b^{L} : α ; β ˙= e ; --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- ≻ ; ∃ γ · ⋀ \{ \begin{matrix}b^{L} : α ; β ˙= e \\ σ ˙= b^{a.L} : α ; γ \\ β ˙= a^{b.L} : τ ; γ \end{matrix}  Mutate(a ▷ b)

Theorem 6 Unification in the record algebra is decidable and unitary unifying.

\underline{Proof}: The theory is strict (we exhibited a compatible ordering). Therefore, the rules for mutation, decomposition, collision, fusion and generalization applied any order a complete semi-algorithm for unification. The algorithm is unitary since mutation does not introduce any disjunction. It remains to prove termination.

All transformations are stable in the sets T^{n} and decrease in the following lexicographic ordering:

• the number of symbols f^{Row(L)} in the lexicographic order of decreasing Card (L) (that is, bigger sets count less: mutate (a ▷ f)),

• the number of symbols a^{L} : ; counted in the lexicographic order of decreasing Card (L) (mutate (a ▷ b)),

• the number of other symbols (other mutations and decomposition),

• the sum of heights of terms (generalization),

• the number of multi-equations (fusion).

This guarantees the termination of the process.

3.3 Raw terms

Let C′ be the set of symbols C extended with a symbol Π and the collection of symbols (a : ; )_{a∈L}. Terms of the algebra T (C′, V) are called raw terms. To any record term, we associate the raw term obtained by erasing all superscripts of symbols. Conversely, for any raw term τ′ and any sort ι, there is at most one record term whose erasure is τ′. Thus any record term τ of sort ι is completely defined by its erasure τ′ and the sort ι. In the rest of the paper we will mostly use this notation and often drop the sort whenever it is implicit from the context.

Projection symbols associate to the right; that is, (a : τ ; b : σ ; ρ) stands for (a : τ; b : σ ; ρ). In formulas we sometimes write ((a_{i} : τ_{i})_{i∈[1,p]} ; σ) for (a_{1} : τ_{1} ; … a_{p} : τ_{p} ; σ).

3.4 Examples of Record terms

When record terms are used as types of records in ML, the types of fields must first say whether the field is absent or present and in the last case whether it is an arrow type or some other structured type. For instance, a type could be α → Π (a : pre (α → α) ; β) . However, types that would tell their structure before telling that the field is defined must be forbidden: α → Πa : α → α; β is should not be a correct type. These constrains are, of course, realized using sorts. The properties of the section 1 allow record terms to be restricted by a signature compatible with its equations, and still use the same unification algorithm.

We give two examples of restricted record terms used as types in ML with records. The first instance distinguishes a constant symbol abs and a unary symbol pre in C. The signature Σ′ on the two sorts type and field is:

Σ′ ⊢ Π :: field ⇒ type

Σ′ ⊢ abs^{ι} :: field  ι ∈ K

Σ′ ⊢ pre :: type ⇒ field

Σ′ ⊢ fType :: type^{ϱ(f)} ⇒ type  f ∈ C \ {abs , pre }
Σ′ ⊢ (ℓ^{L} : ; ) :: field ⊗ field ⇒ field ℓ ∈ L, L ∈ P_{f}(L \ {ℓ})

The signature Σ′ is compatible with the equations of the record algebra. We define simple record terms as record terms that are well sorted for Σ′. They have a very simple record structure. Terms of the sort Row(L) are either of depth 0 (reduced to a variable or a symbol) or are of the form (a : τ ; ρ). By induction, they are always of the form

(a_{1} : τ_{1} ; … a_{p} : τ_{p} ; σ)

where σ is either abs or a variable, including the case where p is zero and the term is reduced to σ.

The generality of record term algebras is better justified by complex records terms. The problem with simple record terms is the inability to merge two records defined on different fields. For instance, the two record types Π (a : pre (α) ; b : pre (σ) ; abs ) and Π(a : pre (τ); abs ) cannot be unified, since on field b this would require pre (σ) be unifiable with abs . A solution is to separate the access information from the structure information in fields. The two records could be typed with Π (a : pre .α ; b : pre .σ ; abs .β) and Π (a : pre .τ ; abs .β) . They do not yet unify. But if we write instead Π (a : γ_{a}.α ; b : γ_{b}.σ ; abs .β) and Π (a : γ′_{a}.τ ; abs .β′) , then they are unified by the substitution:

γ_{a} ↦ γ′_{a}  α ↦ τ  γ_{b} ↦ abs  β′ ↦ b : β_{b} ; β

Generic record terms are well sorted records terms for the following signature Σ′′. Distinguishing two constant symbols pre and abs and a binary symbol “.” in C, the signature Σ′′ is defined on the three sorts type , flag , and field by:

Σ′′ ⊢ Π :: field ⇒ type

Σ′′ ⊢ abs^{ι} :: flag  ι ∈ K
Σ′′ ⊢ pre^{ι} :: flag  ι ∈ K
Σ′′ ⊢ .^{ι} :: flag ⊗ type ⇒ field  ι ∈ K
Σ′′ ⊢ fType :: type^{ϱ(f)} ⇒ type  f ∈ C \ {abs , pre , .}
Σ′′ ⊢ (ℓ^{L} : ; ) :: field ⊗ field ⇒ field ℓ ∈ L, L ∈ P_{f}(L \ {ℓ})

The signature is still compatible with the equations. Terms of the sort Row(L) can now have a more complex structure such as

(a : τ ; ρ).(b : σ ; ρ′)

If a and b were equal, this would simplify into

(a : τ.σ ; ρ.ρ′)

We say that the latter is a canonical form but the former is not. In the next section we study canonical forms of record terms in general.

4 Approximations of terms

The complex record type Π (a : pre .τ ; σ) can intuitively be understood as the type of some record whose field a is present with type τ and whose presence of other fields is defined by σ. However, it is harder to understand the objects that would have the record type τ equal to Π (a : pre .τ ; (b : pre ; σ).γ) . Substituting γ by (b : γ′ ; γ′′) would lead to the E-equal record type Π (a : pre .τ ; b : pre .γ′ ; σ.γ′′) , which is less general but has a more intuitive meaning. The substitution γ ↦ (b : γ′ ; γ′′) does not impose any more structure on the type of τ. It just “reads” information form τ in the sense that any non-variable instance of γ is necessarily an instance of (b : γ′ ; γ′′) .

Canonical terms are record types in which a symbol (a : ; ) can only occur below some other symbol but (b : ; ) or the symbol Π, and E-canonical terms are those that are Eequal to canonical terms. There are terms that are not E-canonical. For instance, the term τ above is not. We first define a class of “reversible” substitutions called expansions. Then we show that any term can be transformed by expansion into a term that is E-canonical. There exist least E-canonical expansions; however, expansions do not commute with unification. Allowing the reverse of expansions, called contractions, leads to E-canonical approximations, which commute with unification.

4.1 Expansions

Definition 8 An elementary substitution of W is a substitution of the following form:

• α ↦ a : β ; γ is an elementary expansion of W if α is in W and β and γ are not in W.

• α ↦ β is an elementary renaming of W if α is in W and β is outside of W.

• α ↦ β is an elementary fusion of W if α and β are in W.

• α ↦ f(β_{i})_{i∈[1,p]} is an elementary structuration of W if α is in W and β_{i} are all outside of W.

A perfect composition of W is any composition μ_{1} ∘ … μ_{p} such that there exists a sequence (W_{i})_{i∈[0,p]} of sets of variables satisfying:

1. W_{0} = W;

2. μ_{i} is an elementary substitution of W_{i};

3. W_{i} is equal to V(μ(W_{i−1})).

An expansion is a perfect composition of elementary expansions. An α-expansion is a perfect composition of elementary expansions and renamings.

Notation

We write expansions with letters φ, ψ, and χ. We indicate elementary substitutions by a “ˆ ” accent: φ̂, μ̂. The notation

μ : V −T

is not well adapted to describe perfect compositions. We write

V −μ− W

for a perfect composition μ of V such that W is the set of variables of the image of V. We can compose them as follows:

[figure: V; −μ; −; −; W; −ν; −; −; W′]

We also draw diagrams with the convention that continuous lines are universally quantified while dashed lines are existentially quantified. For instance

V − μ− W |  \begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix}
[figure: φ; |; ·; ·; ·; ·; ·; ψ]
W′ ····ν······ .

is read “For any substitution μ from V to W and any expansion from V to W′, there exist a substitution ν of W′ and an expansion ψ of W such that ν ∘ φ and ψ ∘ μ are E-equal.” All diagrams commutes modulo E-equality, except if explicitly mentioned otherwise.

Lemma 8 Any substitution whose domain is in W can be written as a perfect composition of elementary substitutions of W.

\underline{Proof}: The lemma is first shown for the substitution of a variable by a term, by induction on the size of the term. The general case is then shown by induction on the size of the domain of the substitution.

Lemma 9 A substitution μ is an expansion of W if and only if:

• all symbols of the image of μ are projection symbols;

• all variables of the image of μ are outside of W; and

• all terms of μ(W) are linear (a variable does notoccur twice) and disjoint (no variable is shared between two terms).

Concretely, an expansion φ is sum ⊕_{α∈dom (φ)}(φ_{α}) where φ_{α} are

α ↦ a_{1} : α_{1} ; … a_{p_{α}} : α_{p_{α}} ; β_{α}

and expansions φ_{α} are pairwise disjoint.

\underline{Proof}: Any such substitution is trivially an expansion. Conversely, the set of such substitutions contains elementary expansions and is closed by composition with elementary expansions.

Remark 5 The set of expansions is closed by E-equality. Proving the E-equality of two expansions can always be done using left commutativity axioms only.

Lemma 10 If θ is a renaming of W and φ is an expansion of θ(W), then there exists an expansion ψ of W and a renaming of ψ(W) such that θ∘φ and η∘ψ are equal, and conversely, inverting the roles of renamings and expansions.

[figure: W; −θ; −; −; −; .; _{\begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix}  |}; ψ; ·; ·; ·; ·; ·; |; |; φ; .; ·····η; ·; ·; ·; ·; ·; ·; .; W; ····η; ·; ·; ·; ·; ·; ·; .; _{|  \begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix}}; φ; |; |; ·; ·; ·; ·; ·; ψ; .; \begin{matrix}− \\ − \\ − \\ θ \end{matrix}; −; −; −; .]

\underline{Proof}: For the first diagram, the renaming θ can be decomposed into the sum of two renamings θ′ equal to θ |` W′ and θ′′ equal to θ \ W′ where W′ is θ^{−1}(dom (φ)). Take θ′′ + ω^{−1} for η, and ω ∘φ∘θ′ for ψ where ω renames variables of im (φ) away from all other variable involved.

For the second diagram, the renaming θ can be decomposed into the sum of two renamings θ′ equal to θ |` W′ and θ′′ equal to θ \ W′, where W′ is im (φ). Take (θ′ ∘ φ) + ω^{−1} for ψ and ω ∘ θ′′ for η, where ω renames variables of im (ω′′) away form all other variables involved.

In both cases, it is easy to prove that ψ is an expansion, and so the diagram commutes, as required.

Lemma 11 If a perfect composition of elementary substitutions is an α-expansion, then all elementary substitutions are renamings or expansions.

\underline{Proof}: Let μ be the perfect composition of W_{0}.

[figure: W_{0}; − μ̂_{1}; −; −; W_{1}; ⋯; − μ̂_{p}; −; −; W_{p}]

If the sequence contains a structuration α ↦ f(α_{i})_{i∈[1,p]}, then im (μ) contains the symbol f. Otherwise it contains a fusion (α ↦ β), where α and β are in some W_{i}. If α and β are the images of distinct variables α′ and β′ of W_{0}, then the images by μ of α′ and β′ will not be disjoint. Otherwise, α and β are in the image of a common variable α′ and μ_{1} ∘ … μ_{i} will not be linear. In all cases, μ cannot be an α-expansion.

Corollary 12 Two substitutions that perfectly compose into an α-expansion are αexpansions.

Lemma 13 For any set of variables W, any elementary substitution μ̂ of W, and any expansion φ of W, there exists an expansion ψ of μ̂(W) and a substitution ν such that ψ ∘ μ̂ and ν ∘ φ are E-equal on W, that is, the diagram on the right commutes modulo E-equality.

[figure: W; −μ̂; −; −; −; .; _{| \begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix}}; φ; |; |; ·; ·; ·; ·; ·; ψ; .; ·····ν; ·; ·; ·; ·; ·; ·; .]

\underline{Proof}: It is enough to show the lemma for substitutions with disjoint images φ(W) and μ̂(W). The lemma then follows by introducing a renaming θ of the image of φ outside of the image of μ̂, applying the lemma to θ ∘ φ instead of φ, and replacing the resulting substitution ν by ν ∘ θ^{−1}. Similarly, the images can be assumed disjoint from the domains without loss of generality.

We first show the lemma for an expansion φ of the form

α ↦ a_{1} : α_{1} ; … a_{p} : α_{p} ; α_{0}

If the domain of μ̂ is not reduced to α, then the two substitutions commute, and ν is μ̂, and ψ is φ. Otherwise we reason by cases on μ̂:

• If μ̂ is a renaming (α ↦ β), then φ ∘ μ̂ for ψ and the identity for ν.

• If μ̂ is a fusion (α ↦ β), then take β ↦ φ(α) for both ν and ψ. Otherwise the image of μ̂ is outside of W.

• If μ̂ is an expansion (α ↦ a_{j} : β_{j}; β_{0}) for j in [1, p_{i}], take the renaming β_{j} ↦ α_{j} for ν and the expansion β ↦ (a_{k} : α_{k})_{k∈K} ; α_{0} where K is [1, p_{i}] \ {j} for ψ.

• If μ̂ is an expansion (α ↦ b : β_{b}; β_{0}), then take (β_{0} ↦ (a_{k} : α_{k})_{k∈[1,p_{i}]} ; γ_{0}) for ψ and the expansion (α_{0} ↦ b : β_{b}; γ_{0}) for ν, where γ_{0} is a variable distinct from all others.

• If μ̂ is a structuration (α ↦ f(β_{j})_{j∈[1,q]}), then take the expansion

(β_{j} ↦ (a_{k} : γ_{k})_{k∈[1,p_{i}]} ; γ_{0})_{j∈[1,q]}

for ψ and the structuration

(α_{k} ↦ f(γ_{k})_{i∈[1,p]})_{k∈[0,p_{i}]}

for ν, where all variables γ_{k} are distinct and distinct from all others.

A general expansion φ is the disjoint sum ⊕_{i∈[1,p]}(φ_{i}) of simple expansions. If it is not disjoint from μ̂, there exists one expansion (φ_{1} for instance) that has the same domain as μ̂. Applying the lemma with φ_{1} gives ψ_{1} and ν. Take ψ_{1} + ⊕_{i∈[2,p]}(φ_{i}) for ψ.

Remark 6 If μ̂ is an expansion, then ν̂ is an α-expansion.

Proposition 14 For any substitution μ of W and any expansion φ of W, there exists an expansion ψ of μ(W) and a substitution ν of φ(W) such that ψ ∘ μ and ν ∘ φ are E-equal on W, that is, the diagram on the right commutes modulo E-equality.

[figure: W; −μ; −; −; −; .; _{| \begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix}}; φ; |; |; ·; ·; ·; ·; ·; ψ; .; ·····ν; ·; ·; ·; ·; ·; ·; .]

\underline{Proof}: By induction on the number of elementary substitutions that compose μ, we obtain the following diagram:

[figure: W; − μ̂_{1}; −; −; −; −; .; ···· ·; ·····; .; − μ̂_{n}; −; −; −; −; .] |  \begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix}  \begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix}  \begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix}
[figure: φ_{0}; |; |; ·; ·; ·; ·; ·; φ_{1}; ·; ·; ·; ·; ·; φ_{n−1}; ·; ·; ·; ·; ·; φ_{n}]
[figure: .; ······ ν_{1}; ·; ·; ·; ·; ·; ·; ·; .; ···· ·; ·····; .; ········ ν_{n}; ·; ·; ·; ·; ·; ·; ·; .]

Corollary 15 If a unificand U admits a solution μ outside of V(U), and φ is an expansion of U, then there exists a solution ν of φ(U) and an expansion ψ of μ(U) such that ψ ∘ μ and ν ∘ φ are E-equal.

Corollary 16 For any expansions φ and ψ of W, there exist two expansions φ′ of φ(W) and ψ′ of ψ(W) and a renaming θ such that θ ∘ φ′ ∘ φ and ψ′ ∘ ψ are E-equal on W, that is, the adjoining diagram commutes modulo E-equality.

\underline{Proof}: By proposition 14, where μ is an expansion, and then by corollary 12, ν must be an α-expansion.

[figure: W; − ψ; −; −; −; −; −; −; −; −; −; −; .; _{| \begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix}}; φ; |; |; ·; ·; ·; ·; ·; ψ′; .; ····· φ′; ·; ·; ·; ·; ·; ·; ·; ·; ·; .; ········θ; ·; ·; ·; ·; ·; ·; .]

Theorem 7 Let U be a unificand and φ an expansion of U into V. If μ and ν are principal unifiers of U and V, then there exists an α-expansion η ∘ ψ of μ(U) into ν(V) such that ν ∘ φ and η ∘ ψ ∘ μ are equal, that is, the adjoining diagram commutes modulo E-equality.

[figure: U; −μ; −; −; −; −; −; .; _{| \begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix}}; φ; |; ·; ·; ·; ·; ·; η ∘ ψ; V; \begin{matrix}− \\ − \\ ν \end{matrix}; −; −; −; −; −; .]

\underline{Proof}: The proof is sketched in the adjoining diagram, taken modulo E-equality. The existence of ξ and ψ follows from corollary 15. Since ν ∘ φ is a solution of U and μ is the principal solution of U, the substitution ξ′ must exist. Finally, the existence of ξ′′ is a consequence of the fact that ξ is a solution of V, since ξ(V) is equal to ψ ∘ ν(U), which is satisfied, while ν is a principal solution of V. Since ξ′′ ∘ ξ′ is an expansion, ξ′′ and, in particular ξ′′ are α-expansions.

[figure: U; − μ; −; −; −; −; −; −; −; −; .; _{| \begin{matrix}· \\ · \\ · \\ · \\ · \\ · \\ · \\ · \\ · \\ · \\ · \\ · \end{matrix}}; (1); ·····; ψ; ^{·····}; φ; |; |; |; |; .; (2); ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ξ′; ·····; ξ; ^{·····}; (3); ^{·····}; ξ′′; ·····; V; \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \\ − \\ ν \end{matrix}; −; −; −; −; −; −; −; −; .]

4.2 Canonical terms

In this section we define canonical terms and show that any term can be expanded into a canonical term. We assume we are given an ordering on L that extends naturally to projection symbols.

Definition 9 A record term τ is canonical if projection symbols can only occur below a symbol Π or some other smaller projection symbol.

∀ux ∈ dom (τ), Top (τ_{/ux}) = (a : ; ) ⟹ Top (τ_{/u}) ∈ {Π} ∪ {(a : ; ) | a < b}

A term is E-canonical canonical E if it is E-equal to a canonical term.

A canonical expansion of τ is a canonical term obtained by an expansion of τ.

For instance, the term (a : Π (a : α ; α′) ; b : β′ ; γ) is canonical, but the term

f((a : α ; α′) , (a : β ; b : β′ ; γ))

is not. The term (a : τ ; ρ) . (b : σ ; ρ′) of section 3.4 is canonical.

Notation

In general if Q is a set of terms (respectively a set of symbols) and ι is a sort, we write Q^{ι} for the subset of Q of terms (respectively symbols) of the sort ι.

If L is a finite subset of labels, we write V_{L} for the union VType ∪ V^{Row(L)} and V_{⊂L} for the union of all V_{K} for all subsets K of L, C_{⊂L} for the union of CType and all C^{Row(K)} for all subsets K of L, and Σ_{⊂L} for the restriction of the signature Σ |` C_{⊂L}. We write T_{L} for the algebra T_{L}(V_{L}, Σ_{⊂L}) and T_{⊂L} the algebra T (V_{⊂L}, Σ_{⊂L}).

For instance, the term τ equal to {a : α ; α′} is in T_{{a}}. The term σ equal to (b : β ; β′) is in T′_{{b}}, and the term τ → σ is in T_{⊂{a,b}}.

Definition 10 For any finite set of labels L we write E⃗_{L} for the rewriting system obtained by orienting the equations (a ▷ b, K) if a and b are ordered and (f ▷ a, K) for all subsets K of L.

Lemma 17 For any finite set of labels L, the rewriting system E⃗_{L} is stable and terminates in the set T_{⊂L}.

\underline{Proof}: We extend the total order on projection symbols to a partial order on all symbols by placing projection symbols before all other symbols. An ordered element in τ is a pair (u, v) of two non-variable occurrences of τ such that u is a prefix of v and the symbol at the occurrence u is smaller than the symbol at occurrence v. Any step increases the number of ordered elements. The size Θ_{Card (L)} is constant, which provides a bound on the number of occurrences of symbols of the term, and thus on the number of pairs of non-variable prefix occurrences.

Remark 7 The rewriting system E⃗_{∞} would not terminate, since constant symbols could be rewritten forever in terms of T_{L} for increasing L.

Lemma 18 For any finite set of labels L, all terms of E⃗_{L}(T_{L}) are canonical.

\underline{Proof}: A term of E⃗_{L}(T_{L}) reduces by E⃗_{L} to some term where non-projection symbols can only have sorts Row(L). Such terms are trivially canonical.

Corollary 19 For any finite set of labels L, all terms of T_{L} are E-canonical.

This gives us a means of computing the canonical form of a term in T_{L}.

Definition 11 Let τ be a term, and L be the smallest K such that τ is in T_{⊂K}. If φ is an expansion of row variables of τ into T_{L}, then φ(τ) is called a canonical expansion of τ. Let μ be a substitution and L the smallest K such that im (μ) is in T_{⊂K}. If φ is an expansion of variables of im (μ) into T_{L}, then φ ∘ μ is called a canonical expansion of μ.

It is clear that canonical expansions are E-canonical. They are defined modulo a renaming of variables that are introduced by the expansion. In general, they are not the smallest Ecanonical expansions, even for a single term τ of T′. For instance, if τ is in T_{L}, α is in V_{L}(τ), and the label a is not in L, then the canonical expansion of (α ↦ a : f ; f)(τ) is in T_{a.L}, but there the E-canonical term (α ↦ f)(τ) in T_{L} obtained by the empty expansion.

The existence of E-canonical forms is not enough. As computed above, canonical forms may be very large. Are there smallest E-canonical forms? Do they commute with unification? That is, given a unificand W, an α-expansion φ that maps W to a the smallest canonical form W′, and two principal unifiers μ and μ′ of W and W′, are the smallest α-expansions ψ(μ(W)) and sx1′(μ′(W′)) E-equal modulo renaming?

[figure: W; −μ; −; −; −; .; − ψ; −; −; −; −; .] |  \begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix}
φ|  \begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix}θ?
[figure: W′; −ν; −; −; −; .; − χ; −; −; −; −; .]

The following example shows that this cannot be the case.

Example 8

f((a : g ; α) , β) ˙= f(g, β)− \begin{matrix}(α ↦ g) \\ T′_{∅} \end{matrix} −f(g, β) ˙= f(g, β)
|  \begin{matrix}· \\ · \\ · \\ · \\ · \\ · \\ · \end{matrix}
(β ↦ (a : γ ; δ) )\begin{matrix}| \\ | \\  \end{matrix}T′_{\{a\}}  \begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix} θ̸
f((a : g ; α) , (a : γ ; δ) ) ˙= f(g, (a : γ ; δ) ) − \begin{matrix}(α ↦ g) \\ T′_{\{a\}} \end{matrix} −f(g, (a : γ ; δ) ) ˙= f(g, (a : γ ; δ) )

This counterexample removed any hope of providing the set of E-canonical forms with a “sup” operation that extends the “sup” in T . The preceding diagrams can be easily extended to show that this operation would not be associative. The problem comes from axioms (f ▷ a, K) for constant symbols f. One solution to is to allow contraction — the reverse of expansion — while computing canonical forms. These more general canonical forms are called approximations and are studied in the rest of this section.

Definition 12 An approximation of a substitution μ (respectively of a term τ) is an Ecanonical substitution ν (respectively an E-canonical term σ) such that there exist two expansions φ and ψ such that ψ ∘ ν = φ ∘ μ (respectively φ(τ) = ψ(σ)).

Approximations are called contractions when φ is the identity.

We first show that computing approximations in T can be reduced to computing approximations in T′.

4.3 Approximations in T

Recall that a substitution μ is p-potent if μ^{p} is equal to μ. It is potent if it is potent for some p. Its composition for high enough powers is written μ^{∞}. A 1-potent substitution is also said idempotent. An idempotent substitution is characterized by having disjoint domain and image. We say that μ is potent on W if the restriction of μ to W is potent.

A substitution μ is linear in a variable α if α appears at most once in the image of at most one variable of the domain of μ. By extension a substitution is linear in a set of variables W if it is linear in all variables of W.

Definition 13 A decomposition of a substitution μ is a pair, written dec W · ν, of a set of variables W disjoint from μ and a substitution ν potent on W such that (ν |` W)^{∞} ∘ (ν \ W) is equal to μ. A Π-decomposition of μ is a decomposition dec W · ν such that ν sends W to Π(T′) and V \ W to T′. It is linear if ν is linear on W. If ν is potent on W, we also write dec W · ν for the substitution (ν |` W)^{∞} ∘ (ν \ W) itself.

4.3 Approximations in T 29

For instance, the substitution α ↦ {a : {b : α ; β} ; abs } → {b : α ; β} can be decomposed into

dec γ, δ · ∧ \{ \begin{matrix}α ↦ γ → δ \\ γ ↦ \{a : δ ; abs \} \\ δ ↦ \{b : α ; β\} \end{matrix}  or  dec γ, δ, δ′ · ∧ \{ \begin{matrix}α ↦ γ → δ \\ γ ↦ \{a : δ′ ; abs \} \\ δ ↦ \{b : α ; β\} \\ δ′ ↦ \{b : α ; β\} \end{matrix}

and the latter decomposition is linear.

Lemma 20 Each term has a linear Π-decomposition.

\underline{Proof}: We can build a linear Π-decomposition for any term by induction on the number of Π symbols. If μ has no Π symbol, then ν is μ and W is empty. Otherwise there exists a variable α in the domain of μ whose image is τ[Π(σ)/β], where σ has no Π symbol and the variable β is taken out of μ and appears exactly once in τ. By induction, the substitution μ′ equal to μ \ {α} + α ↦ τ has a linear Π-decomposition dec W′ · ν′. Then dec W ∪ {β} · ν′ + β ↦ σ is a linear Π-decomposition of μ.

The decomposition dec W · ν can be represented by annotating all occurrences of Π symbols in the image of μ with distinct variables of W.

Lemma 21 If μ has a Π-decomposition then it has a linear one.

\underline{Proof}: Let dec W · ν be a Π-decomposition of μ.

• If ν sends two variables α and β two terms τ and σ that share a variable γ of W, then dec W ∪ {γ′} · ν \ {β} + β ↦ σ[γ′/γ], where γ′ is disjoint from ν, is a decomposition of μ.

• If ν sends a variable α to a term τ that contains two occurrences u and v of the same variable β in W, then dec W ∪ {β′} · ν \ {α} + α ↦ σ[β′/v] where β′ is disjoint from ν is a decomposition of μ.

Each transformation increases the number of variables in W, which is bound by the number of Π symbols in μ. When no more transformations are possible, the decomposition is linear.

Lemma 22 Let dec W · ν and dec W′ · ν′ be two Π-decompositions of μ, and μ′. If there exists a renaming θ of W into W′ and if ν′ and θ ∘ ν ∘ θ^{−1} are E-equal, then μ′ and μ are E-equal.

\underline{Proof}: For a high enough p, the substitution μ′ is (ν′ |` W′)^{p} ∘ (ν \ W′), that is

(θ ∘ ν ∘ θ^{−1} |` θ(W))^{p} ∘ (θ ∘ ν ∘ θ^{−1} \ θ(W))  or  (θ ∘ (ν |` W) ∘ θ^{−1})^{p} ∘ (θ ∘ (ν \ W) ∘ θ^{−1})

After removing intermediate θ^{−1} and θ, we get θ ∘ (ν |` W)^{p} ∘ (ν \ W) ∘ θ^{−1} which is θ ∘ μ ∘ θ^{−1}. Since μ is disjoint from μ, it is equal to μ.

The converse is not true in general. But it is true if the decompositions are linear. Thus, all linear Π-decompositions are equal up to renaming of intermediate variables.

Lemma 23 Let dec W · ν and dec W′ · ν′ be two linear Π-decompositions of μ and μ′. If μ′ and μ are E-equal, then there exists a renaming θ of W into W′ such that ν′ and θ ∘ ν ∘ θ^{−1} are E-equal.

\underline{Proof}: We reason by induction on the number of Π-symbols in μ. If μ contains no Π symbol, then neither does μ′ and both W and W′ are empty; consequently ν′ and ν are E-equal.

Otherwise, there exists a variable α in the domain of μ whose image by μ is τ[Π(σ_{i})/β_{i}], where τ has no Π symbol and variables β_{i} are taken away from μ and appear exactly once in τ. The term μ′(α) is of the form τ′[Π(σ′_{i})/β_{i}], where τ and τ′ on one hand and σ_{i} and σ′_{i} on the other hand are E-equal. The substitutions μ \ {α} + β_{i} ↦ σ_{i} and μ′ \ {α} + β_{i} ↦ σ′_{i} are E-equal. We name them respectively μ_{α} and μ′_{α}. For each i there must be a variable in W whose image under ν is Π(σ_{i}). We can assume that it is β_{i} without lost of generality. It is easy to check that dec W \ {β_{i}} · ν \ {α} is a decomposition of μ_{α}. Similarly for each i there is a variable β′_{i} in W′ whose image under ν′ is σ′_{i}, and such that dec W′ \ {β′_{i}} · ν \ {α} is a decomposition of μ′_{α}. By the induction hypothesis, there exists a substitution θ_{0} such that the substitutions ν \ {α} and θ_{0} ∘ (ν′ \ {α}) ∘ θ_{0}^{−1} are E-equal. The substitution θ equal to θ + (β ↦ β_{i}) satisfies the lemma.

Lemma 24 For any linear Π-decomposition dec W · ν of a substitution μ, μ is E-canonical if and only if ν is.

\underline{Proof}: For any substitution ν and any substitution ξ of into Π(T′), then ξ ∘ ν is E-canonical if and only if ν and ξ are E-canonical, since S(ξ ∘ ν) and S(ξ) ∪ S(ν) are equal, where S(μ_{0}) is the set of all pairs (f, (a : ; ) ) such that (a : ; ) occurs directly below some occurrence of f in μ_{0}. This shows the lemma for canonicity instead of E-canonicity. The general case follows from lemmas 22 and 23.

Definition 14 The composition of two Π-decompositions dec W_{1}· ν_{1} and dec W_{2}· ν_{2} such that W_{1} is disjoint from ν_{2} and W_{2} is disjoint from ν_{1} is the Π-decomposition dec W_{1}, W_{2} · ν_{1} ∘ ν_{2}.

Lemma 25 The composition of the Π-decompositions of two substitutions is a Π-decomposi-tion of their composition.

\underline{Proof}: We must check that for some high enough p,

(μ |` U)^{p} ∘ (μ \ U) ∘ (ν |` V)^{p} ∘ (ν \ V) = (μ ∘ ν |` U ∪ V)^{p} ∘ \underline{(μ ∘ ν \ U \ V)}

where μ is disjoint from V and ν is disjoint from U. Since im (ν) is disjoint from U, the substitution μ ∘ ν \ U \ V is equal to (μ \ U) ∘ (ν \ V) and we are left with:

(μ |` U)^{p} ∘ \underline{(μ \ U) ∘ (ν |` V)^{p}} = (μ ∘ ν |` U ∪ V)^{p} ∘ (μ \ U)

Since dom (μ \ U) is disjoint from dom (ν |` V), the substitution (μ \ U) ∘ (ν |` V) is equal to (μ \ U) + ((μ \ U) ∘ (ν |` V)) |` V, that is, (μ ∘ ν |` V) ∘ (μ \ U). By induction, we find that the substitution (μ \ U) ∘ (ν |` V)^{p} is E-equal to (μ ∘ ν |` V)^{p} ∘ (μ \ U). Thus, we are left with:

(μ |` U)^{p} ∘ (μ ∘ ν |` V)^{p} = (μ ∘ ν |` U ∪ V)^{p}

which holds since μ ∘ ν |` U ∪ V is equal to (μ ∘ ν |` V) + (μ |` U).

The lemma is true even for non-linear Π-decompositions. The composition of linear Πdecompositions may not be linear. If dec W · ν is a linear expansion of μ and φ is an expansion disjoint form W, then dec W · φ ∘ ν is a linear Π-decomposition of φ ∘ μ.

Lemma 26 Let dec W · ν be a linear Π-decomposition of μ. A substitution μ′ is an approximation of μ if and only if there exists a linear Π-decomposition of dec W · ν′ of μ′ such that ν′ is an approximation of ν.

4.4 Approximations in T′ 31

\underline{Proof}: Assume that there exists a Π-decomposition dec W · ν′ of μ′ such that ν′ is an approximation of ν. There exist two substitutions φ and φ′ such that φ ∘ ν and φ′ ∘ ν′ are E-equal. The substitution φ ∘ μ is equal to φ ∘ (ν |` W)^{p} ∘ (ν \ W). By sort considerations, the substitution φ is necessarily disjoint from W, and it is potent. Thus the above substitution is also ((φ ∘ ν) |` W)^{p} ∘ ((φ ∘ ν) \ W). We get an E-equal substitution replacing φ ∘ ν by φ′ ∘ ν′ which is E-equal to φ′ ∘ μ′ by the same reasoning.

Conversely, assume that μ′ is an approximation of μ. Then there exists a linear approximation dec W · ν′ of μ′. A similar calculus to the one above shows that substitution dec W · φ ∘ ν is a linear Π-decomposition of φ ∘ μ and similarly dec W · φ′ ∘ ν′ is a linear Π-decomposition of φ′ ∘ μ′. The E-equality of φ ∘ μ and φ′ ∘ μ′ and lemma 23 show that φ ∘ ν and φ′ ∘ ν′ are E-equal. Thus, φ′ is an approximation of φ.

The lemma is not true if the decompositions are not linear. For instance, take

dec α_{1}, β_{2} · \{ \begin{matrix}α ↦ α_{1} → α_{2} \\ α_{1} ↦ Π (a : β ; γ_{1}) \\ α_{2} ↦ Π (γ_{2}) \end{matrix}  and  dec α_{1} · \{ \begin{matrix}α ↦ α_{1} → α_{1} \\ α_{1} ↦ Π (a : β ; γ_{1}) \end{matrix}

for μ and μ′.

We are led to study approximations for substitutions in T′ ∪ Π(T′).

4.4 Approximations in T′

For simplicity of exposition, we study approximations of substitutions into T′, but all results straightforwardly extend to approximations of substitutions into T′ ∪ Π(T′).

Definition 15 The connexe components of a substitution μ in T′ is the partition of the domain of μ by the smallest equivalence ∼_{μ} that contains all pairs α ∼_{μ} β such that images of α and β by μ share at least one row variable, i.e. V(μ(α)) ∩ V(μ(β)) \ VType ≠ ∅.

A substitution is said to be connexe if ∼_{μ} has only one connexe component

The connexe components of a substitution are preserved by expansion. Let (W_{i})_{i∈[1,p]} be the connexe components of μ. We write μ_{i} the restrictions of μ to W_{i}. Then μ is equal to ⊕_{i∈[1,p]}μ_{i}. If μ is idempotent, it is also the composition μ_{1} ∘ … μ_{p} in any order. If φ is an expansion of μ, then φ ∘ μ has the same connexe components as μ and the substitution φ_{i} perfectly composes with μ_{i}, where φ_{i} is the restriction φ to im (μ_{i}). Conversely, if φ_{i} are expansions that perfectly compose with μ_{i} and are disjoint, then ⊕_{i∈[1,p]}φ_{i} is an expansion that perfectly composes with μ.

Lemma 27 Let μ and ν be two substitutions in T′. The substitution ν is an approximation of μ if and only if they have the same connexe components and μ |` W is an approximation of ν |` W on each connexe component W.

\underline{Proof}: We first assume the existence of two expansions φ and ψ such that φ ∘ μ and ψ ∘ ν are equal and ν is E-canonical. Since expansion does not change connexe components, both μ and ν have the same connexe components (W_{i})_{i∈[1,p]}. The substitution ν_{i} is of course Ecanonical since the restriction of a E-canonical substitution and such that ψ |` μ(W_{i}) ∘ μ |` W_{i} and φ |` ν(W_{i}) ∘ ν |` (W_{i}) are E-equal for each connexe component W_{i}.

Conversely, we assume that μ and ν have the same components (W_{i})_{i∈[1,p]}, and that ν |` W_{i} is an approximation of μ |` W_{i} on each connexe component W_{i}. Therefore, there exists expansions φ_{i} and ψ_{i} such that ψ_{i} ∘ ν |` W_{i} and φ_{i} ∘ μ |` W_{i} are E-equal. We can always choose them such that they are disjoint form each other and from the common domain of μ and ν. Then their respective sums φ and ψ perfectly composes. The substitution ψ ∘ ν and φ ∘ μ are E-equal.

We are left with the computation of approximations on connexe components.

4.5 Approximations on connexe components in T′

By corollary 19, we know that substitutions in T′_{L} are E-canonical. Conversely, a connexe E-canonical substitution μ in T′ is in fact always in a set T′_{L} for some L. Connectivity is preserved by expansion. Therefore, any approximation ν of μ is also a connexe E-canonical substitution, say ν. It can be looked for among the substitutions whose range is in T′_{L′} for some L′. When the approximation ν is a contraction of μ, there exist an expansion φ that sends variables of V^{Row(L′)} to terms of T_{L}. The set L′ is a subset of L. The smallest contractions are contractions on a contraction on label when L′ is L \ {a} for some label a. We show that any contraction of a connexe E-canonical substitution can be obtained by successive contractions on labels, independently of the order in which labels are chosen. The process will end with a minimal approximation.

Definition 16 If a term of T′ is E-equal to (a : τ ; σ) we define its projection on a and its residual on a as the terms τ and σ written τ_{/a} and τ_{\a}, respectively. We recursively define the template of a term τ, written τ_{/∞}, as (τ_{\a})_{/∞} if τ is equal to (a : σ ; ρ) and τ otherwise.

The projection (respectively residual, template) of a substitution are raw substitutions of the same domain that maps variables to the projection (respectively residual, template) of their substitution, when defined.

Lemma 28 Let μ be a connexe substitution into T_{L}. It contracts on label a if and only if μ_{/a} is defined and is raw-isomorphic to μ_{/∞}.

Let ϱ be a raw-renaming from V^{Row(L)}(im (μ)) to V^{Row(L\{a})}. The contraction of μ (up to renaming and E-equality) is the substitution ϱ^{−1} ∘ (μ_{\a}), which is equal to μ by the expansion (a : ϱ_{a} ∘ ϱ^{−1} ; ϱ^{−1}), where ϱ_{a} is a raw-renaming that maps μ_{/∞} to μ_{/a} disjoint from μ.

\underline{Proof}: Both sides are immediate.

Corollary 29 Let μ be a connexe E-canonical substitution. If it contracts on label a and on label b separately, then its contraction on a contracts on b and its contraction on b contracts on a, both ways ending with the same substitution, up to renaming and E-equality.

\underline{Proof}: The proof follows immediately from the fact that μ_{\a}_{\b} and μ_{\b}_{\a} are defined simultaneously and then are equal.

[figure: Z; ν; ^{·········}; ξ′; ·········; μ; W′; ······· θ ∘ φ′_{b}; ·; ·; ·; ·; ·; ·; ·; ·; U; \begin{matrix}· \\ · \\ · \\ · \\ · \\ · \\ · \\ · \\ · \end{matrix}  |; ·; ·; ·; ·; ·; ·; ψ′_{a}; ξ; |; |; φ_{a}; V; \begin{matrix}− \\ − \\ − \\ − \\ ψ_{b} \end{matrix}; −; −; −; −; W]

4.6 Minimal approximations in T 33

Corollary 30 Let ξ be an connexe E-canonical substitution. If μ and ν are two contractions of ξ, then there is an approximation ξ′ and two expansions φ′ and ψ′ such that μ is E-equal to φ′ ∘ ξ′ and ν is E-equal to ψ′ ∘ ξ′.

\underline{Proof}: By lemma 9, any contraction is composed of contractions on labels. Then repeatedly apply the previous lemma.

[figure: Z; ν; ^{·········}; ξ′; ·········; μ; W′; ······· θ ∘ φ′; ·; ·; ·; ·; ·; ·; ·; ·; U; \begin{matrix}· \\ · \\ · \\ · \\ · \\ · \\ · \\ · \\ · \end{matrix}  |; ·; ·; ·; ·; ·; ·; ψ′; ξ; |; |; φ; V; \begin{matrix}− \\ − \\ − \\ − \\ ψ \end{matrix}; −; −; −; −; W]

Corollary 31 Any connexe E-canonical substitution has a minimal contraction.

Lemma 32 Any connexe substitution has a minimal approximation, which is the minimal contraction of a E-canonical expansion.

\underline{Proof}: If a substitution has two approximations, there exist expansions of the two approximations that are E-equal up to renaming. Thus both expansions are contraction of a same connexe E-canonical form, and are thus E-equal up to renaming.

4.6 Minimal approximations in T

Theorem 8 Any substitution μ has a minimal approximation μ′ in T , which can be computed as follows:

1. Find a linear Π-decomposition dec W · ν of a μ.

2. Decompose μ into connexe components, ⊕_{i∈[1,p]}μ |` W_{i}.

3. For each connexe component:

(a) find an E-canonical expansion ξ_{i} of μ |` W_{i},

(b) find a minimal contraction ν_{i} of ξ_{i}, by contracting on all labels for which the projection of ξ_{i} is raw-isomorphic to the template of ξ_{i}.

Take the substitution dec W · ⊕_{i∈[1,p]}(ν_{i}) for μ′.

\underline{Proof}: The algorithm and the theorem is a combination of lemmas 32, 27, and 26.

In fact in step 1, the Π-decomposition dec W · ν of μ need not be linear. In this case, the approximations of μ do not correspond to approximations of ν, but it can be shown that minimal approximations do.

Finding a Π-decomposition and the connexe components can always be done in linear time. The expensive part of the algorithm is step 3b, which looks for possible isomorphisms. This is inherent to contraction. Removing this step (that is, taking ν_{i} for ν_{i}) will compute a good approximation of μ (it is a small canonical expansion of μ). This is sufficient in practice.

4.7 Minimal approximations and unification

The following theorem shows that unification commutes with approximations. Therefore unification can be done modulo approximations.

Theorem 9 If U′ is a minimal approximation of a unificand U and μ is a principal unifier of U, then U′ has a principal unifier μ′ and μ and μ′ have the same minimal approximation modulo renaming and E-equality.

\underline{Proof}: The following diagram commutes: the existence of μ′′ follows from corollary 15. Then the existence of μ′ follows from the unifier μ′′ ∘ φ′ of U′. Theorem 7 is applied twice to get the existence of ψ and ψ′. The renamings can in fact be included in the principal unifiers μ′ and μ′′. The unificand V′′ and V′ may not be E-canonical. However, V and V′ have an identical Ecanonical form, and thus they have the same principal E-canonical approximation modulo renaming.

[figure: U; −μ; −; −; −; −; −; −; −; −; −; V; _{| \begin{matrix}· \\ · \\ · \\ · \\ · \end{matrix}}; |; |; |; |; |; |; φ; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ψ; U′; ·······μ′; ······; ······; ·; ·; ·; ·; V′; φ′; ·····; ψ′; ^{·····}; U′′; ·········· μ′′; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; ·; V′′]

There are cases where the structure of unificands ensures that the principal unifier is E-canonical. For instance, with the signature of record terms Σ′ of section 3.4, all terms are always E-canonical. This is no longer the case with the signature Σ′′, as shown by the examples at the beginning of this section. However, for some input unificands to the type inference algorithm, it is guaranteed that the output unificands will be in canonical form. Obviously, it is not sufficient that the input unificand is E-canonical.

Definition 17 A unificand is separated if it can be written (by rearranging the multiequations) in the form ∃ W · U ∧ V such that

1. all multi-equations of U are of the sort T ype and those of V are of a row sort,

2. all row subterms of U and all type subterms of V are variables and their union is W,

3. row variables of W are only variable terms in V,

4. any pair of terms of V have disjoint or equal sets of row variables, and

5. all terms are E-canonical.

A unificand is separable if it is equivalent to a separated unificand using only the U-Generalize rule.

Lemma 33 (Separate) Let ∃ W · U ∧∃ V(e)· (e∧V) be a separated canonical unificand and let μ be a principal E-unifier of e such that its image is outside all bound or free variables of the input unificand. Then, ∃ W · μ(U) ∧ μ(V) is an equivalent unificand in separated E-canonical form, up to reordering the multi-equations.

\underline{Proof}: We first show that μ(e) is E-canonical. Each term σ of E is in some set T_{L_{σ}} for some set of labels L_{σ}. Let L be the union of all sets L_{σ}. It is enough to show that μ(e) is in T_{L}. Let α be a variable of μ(e). For each σ, the variable α is in μ(σ); thus there exists a variable α_{σ} such that α is in μ(α_{σ}). Since there is no Π symbol in e, the variable α_{σ} is of sort L_{σ}; therefore α has a sort Row(L) for some L greater than L_{σ}. The set L contains L_{σ}, for any σ. We know that there is a solution of the multi-equation in T_{⊂L}; thus L cannot be greater than L, otherwise μ would not be principal.

Each term τ of V either shares no row variable with e or has exactly the same row variables as one term of e. In the former case the image by μ is unchanged. In the latter case, the term μ(τ) has exactly the same row variables as μ(e), i.e., it is in T_{⊂L} and is thus E-canonical. The equivalence of the two unificands is obvious.

Corollary 34 (Separate-bis) Let ∃ W, α · U ∧ ∃ V(e) · (α = e ∧ V) be a separated canonical unificand and let μ be a principal E-unifier of e such that its image is outside all bound or free variables of the input unificand. Then ∃ W · μ(U) ∧ (α = μ(e) ∧ μ(V)) is an equivalent unificand in separated E-canonical form.

\underline{Proof}: Generalize the unificand into ∃ W, α · U ∧ ∃ β, V(e) · (β = e ∧ α = β ∧ U) and apply the previous lemma.

Theorem 10 A completely decomposed form of a separable solvable unificand is separable.

\underline{Proof}: Let U be the input unificand and V a completely decomposed form. Let U′ be a separated unificand equivalent to U. Let V′ be a separated, completely decomposed unificand obtained by the algorithm we describe below. The unificands V and V′ are equivalent and completely decomposed. They are necessarily equal modulo unrestricted generalization.

To obtain an algorithm that solves separated unificands, we restrict the rule Separate-Bis to the case where e contains more than one term. Applying Decompose for symbols of the sort Type and rules Separate, Separate-Bis, Generalize and Fuse is stable on separated unificands and terminates. Each rule decrease in the following lexicographic order:

1. The number of symbols of the sort Type (decomposition).

2. The sum of heights of row terms (generalization).

3. The number of multi-equations (fusion and first transformation).

4. The number of terms in row multi-equations (last transformation).

This guarantees the termination. Stability of separation rules is proved above. Stability is obvious for all other rules.

For instance, with the signature of record terms Σ′ of section 3.4, all terms are always E-canonical. This is no longer the case with the signature Σ′′, as shown by examples at the beginning of the section. However, the type inference algorithm will only generate Ecanonical unificands in disjoint form.

Of course, E-canonical unificands can be approximated by smaller unificands, but this has less interest in this case, since the completely decomposed forms are automatically Ecanonical if the input unificands are always separable. The type systems for languages with records presented in [Rém93] are based on signatures Σ′ and Σ′′, and the unificands generated by the type system are always separable, which prevents us from computing E-canonical forms at the end of typechecking.

5 Generic record terms

In record terms, row variables can always be substituted by rows with independent fields; the expansion “duplicates” row variables. For instance, in record types of the form Π(a : τ; pre(α)), it is always possible to substitute α by b : α_{b} ; c : α_{c} ; α′. In some cases, it is useful to express the fact that some part of a row must be shared on all fields. Those parts need to be of the sort type, and consequently we need a new symbol ∂ to inject types into rows. For instance, let σ be α → Π (a : τ ; ∂(α)) . The variable α cannot be replaced by a row defined on b, but σ is equal to α → Π (a : τ ; b : α ; ∂(α)) , which is realized by non-linear idempotent axioms asserting that ∂(τ) is equal to b : α ; ∂(α).

This formalizes the algebra of generic record terms. We can show that it is a decidable syntactic theory, and derive a unitary unifying unification algorithm. Generic record terms provide a type system for a very raw view of records [Rém92b]. They also illustrate the treatment of generic variables in ML, which they generalizes to a degenerate form of intersection types [Pie91].

5.1 Presentation of generic Record Terms

As for record terms, we first define the unsorted generic record terms, and restrict them later by a compatible signature. We assume given a collection of symbols with their arities (C_{n})_{n∈IN}. Let L be a denumerable set of labels. Let K be composed of

• a sort Type and

• a finite collection of sorts (Row(L)_{L∈P_{f} (L)}.

Let Σ be the signature composed of the following symbols, given with their sorts:

Σ ⊢ Π :: Row(∅) ⇒ Type

Σ ⊢ f^{ι} :: ι^{ϱ(f)} ⇒ ι  f ∈ C, ι ∈ K, ϱ(f) ≠ 0
Σ ⊢ ∂^{L} :: Type ⇒ Row(L)  L ∈ P_{f}(L)
Σ ⊢ (ℓ^{L} : ; ) :: Type ⊗ Row(ℓ.L) ⇒ Row(L)  ℓ ∈ L, L ∈ P_{f}(L \ {ℓ})

We write D for the new set of symbols. Let E be the following set of axioms:

• Left commutativity. For any labels a and b and any finite subset of labels L that contains neither a nor b,

a^{L} : α ; b^{a.L} : β ; γ = b^{L} : β ; a^{b.L} : α ; γ  (a ▷ b, L)

• Distributivity. For any symbol f, any label a and any finite subset of labels L that do not contain a,

f^{Row(L)}(a^{L} : α_{1} ; β_{1}, … a^{L} : α_{p} ; β_{p}) = a^{L} : fType(α_{1}, … α_{p}) ; f^{Row(a.L)}(β_{1}, … β_{p})

(f ▷ a, L)

• Idempotence.

∂^{L}α = a^{L} : α ; ∂^{a.L}α  (∂ ▷ a, L)

• Distributivity.

∂^{L} (f^{Row(L)}(α_{1}, … α_{p})) = f^{Row(L)}(∂^{L}α_{1}, … ∂^{L}α_{p})  (∂ ▷ f, L)

All axioms are collapse-free and regular. The last axiom is not linear, but it is right-linear. For instance, the following are two E-equal record terms:

f^{Row(∅)}
[figure]
(b)^{∅}  ∂^{∅}

| [figure]

β  g^{Row({b})} hType
[figure]
α  β

(b)^{∅}
[figure]
fType  f^{Row({b})}
[figure]
β  hType  g^{Row({b})}  ∂^{{b}}

| [figure]

α  β  hType
[figure]
α  β

Let θ be a decreasing function on positive integers. Let Θ be the size function defined on terms by:

Θ(a^{L} : τ ; σ) = sup (Θ(τ) + θ(Card (L)), Θ(σ) + θ(Card (L)) − θ(Card (a.L)))
Θ(f^{K}(τ_{1}, … τ_{p})) = sup_{i∈[1,p]}(τ_{i}) + 1
Θ(∂^{L}(τ)) = Θ(τ) + θ(Card (L))

The size Θ is constant on E-equality classes and defines a compatible ordering on terms. However, the ordering is not well-founded on T . Let T^{n} be the subset of terms that uses only the sorts Type and Row(L), where Card (L) is at most n. The previous ordering is compatible and well-founded on all subsets T^{n}.

5.2 Sufficient condition for syntacticness with non-linear axioms

The sufficient condition for syntacticness given by of theorem 1 does not apply, since the axioms (∂ ▷ a, L) are not linear and therefore the condition (h_{1}) is not always true. For instance, the adjoining proof, matching ⟶_{ϵ} ∗ ; ⟶ ; ••, cannot be rewritten into a proof match-

ing ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ. However, it is still possible to show directly that the theory of generic record terms is syntactic, following the structure of the demonstration of theorem 1.

[figure: \underline{∂ (Π (f) )}; |; ϵ; \overline{a : \underline{Π (f)} ; ∂ (Π (f) )}; |; 2; a : \overline{Π (b ; f : f)} ; ∂f]

Lemma 35 The theory of generic record terms is syntactic.

\underline{Proof}: The proof follows the proof of theorem 1 until the use of conditions (h_{1}) and (h_{2}). Then it resembles the proof of theorem 5, and using a tedious case analysis as we did for proving condition (h_{2}) of theorem 1.

The sequence of sets (T^{k})_{k∈IN} is increasing and its union is T . Thus it is enough to show Synt (T^{k}) on all T^{k}. Let H be one of them.

For any integer n, let H_{n} be the subset of H composed of all the terms that do not start any decreasing sequence of length n. All these sets are closed under ∗ ; ⟶ ; |` H. In particular, they are closed subsets of T . Any term smaller than a term in H_{n+1} is in H_{n}. The sequence is increasing, and its limit is H. We show Synt (H_{n}) by induction on n. In fact, it is enough to show that

⟶_{ϵ} ∗ ; ⟶ ; •∞⟶_{ϵ} ⊂_{H_{n}} ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞

holds.

The set H_{0} is composed of variables and constant symbols. Thus, the only instance of the premise is ⟶_{ϵ}⟶_{ϵ}, for which the inclusion is satisfied, since the two axioms must be inverses and annihilate each other.

Let us assume the property Synt (H_{n}) and show Synt (H_{n+1}). Let D be the set of all directions. A relation ∗ ; ⟶ ; •∞ in H_{n+1} can be written as the composition

( ∗ ; ⟶ ; k∞)^{k∈D}

since disjoint occurrences commute. For each direction k, the subproof at k is in H_{n}. Since Synt (H_{n}), it can be rewritten in H_{n} so that it matches

∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞

Re-assembling all subproofs, we get a proof matching

( ∗ ; ⟶ ; k•∞ δ ; ⟶ ; k ∗ ; ⟶ ; k•∞)^{k∈D}

which is a proof in H_{n+1} since H_{n+1} is closed. It can be reordered as

( ∗ ; ⟶ ; k•∞)^{k∈D} ( δ ; ⟶ ; k)^{k∈D} ( ∗ ; ⟶ ; k•∞)^{k∈D}

We have shown

∗ ; ⟶ ; •∞ ⊂_{H_{n+1}} ( ∗ ; ⟶ ; k•∞)^{k∈D} ( δ ; ⟶ ; k)^{k∈D} ( ∗ ; ⟶ ; k•∞)^{k∈D}

Composing the step at the root on both sides, we get

⟶_{ϵ} ∗ ; ⟶ ; •∞⟶_{ϵ} ⊂_{H_{n+1}} ⟶_{ϵ} ( ∗ ; ⟶ ; k•∞)^{k∈D} ( δ ; ⟶ ; k)^{k∈D} ( ∗ ; ⟶ ; k•∞)^{k∈D} ⟶_{ϵ}

and we are left with proving

⟶_{r,ϵ} ( ∗ ; ⟶ ; k•∞)^{k∈D} ( δ ; ⟶ ; k)^{k∈D} ( ∗ ; ⟶ ; k•∞)^{k∈D} ⟶_{s,ϵ} ⊂_{H_{n+1}} ∗ ; ⟶ ; •∞ δ ; ⟶ ; ϵ ∗ ; ⟶ ; •∞

We show this inclusion condition by cases on the outermost axioms r and s. We omit the superscripts of symbols.

Case r is (∂ ▷ a): The axiom s must be of the form (a ▷ X), since a : ; is the top symbol of the term before the last step.

Subcase X is ∂: The proof is of the form:

∂(τ) ⟶_{ϵ} a : τ ; ∂(τ) ∗ ; ⟶ ; 1∞ a : σ ; ∂(τ) ∗ ; ⟶ ; 2∞ a : σ ; ∂(σ) ⟶_{ϵ} ∂(σ)

A shorter proof is the subproof at occurrence 1 applied to ∂(τ).

Subcase X is b: The label b must be distinct from a. The proof is of the form:

∂(τ) ⟶_{ϵ} a : τ ; ∂(τ) ∗ ; ⟶ ; R,1∞ a : τ′ ; ∂(τ) ∗ ; ⟶ ; S,2∞ a : τ′ ; b : τ′′ ; σ ⟶_{ϵ} b : τ′′ ; a : τ′ ; σ

The subproof

∂(τ) ∗ ; ⟶ ; S,∞ b : τ′′ ; σ

at the occurrence 2 is in H_{n−1}. Thus, it can be rewritten into a proof of the form

∂(τ) ∗ ; ⟶ ; T, 1∞ ∂(ρ) \overrightarrow{ϵ} b : ρ ; ∂(ρ) ∗ ; ⟶ ; P, 1∗ ∗ ; ⟶ ; Q, 2∗ b : τ′′ ; σ

Putting the pieces together, there is a proof matching

\begin{matrix}∂(τ) ∗ ; ⟶ ; 1∞ ∂(ρ) \overrightarrow{ϵ} b : ρ ; ∂(ρ) ∗ ; ⟶ ; P^{−1}, 1∞ b : τ′′ ; ∂(ρ) \overrightarrow{22} b : τ′′ ; a : ρ ; ∂(ρ) ∗ ; ⟶ ; T^{−1}, 21 \\ b : τ′′ ; a : τ ; ∂(ρ) & ∗ ; ⟶ ; R, 21 & b : τ′′ ; a : τ′ ; ∂(ρ) & ∗ ; ⟶ ; Q, 22 & b : τ′′ ; a : τ′ ; σ \end{matrix}

Subcase X is f: Then first term must be of the form f(τ_{1}, … τ_{p}). The proof is of the form

∂ (f(τ_{1}, … τ_{p})) \overrightarrow{ϵ} a : f(τ_{1}, … τ_{p}) ; ∂ (f(τ_{1}, … τ_{p})) ∗ ; ⟶ ; R, 1∞

a : f(σ_{1}, … σ_{p}) ; ∂ (f(τ_{1}, … τ_{p})) ∗ ; ⟶ ; S, 12∞ a : f(σ_{1}, … σ_{p}) ; f(ρ_{1}, … ρ_{p}) \overrightarrow{ϵ}
f(a : σ_{1} ; ρ_{1}, … a : σ_{p} ; ρ_{p})

The subproof using axioms S at occurrence 1 is H_{n}, and can be rewritten into a proof matching

∂ (f(τ_{1}, … τ_{p})) ∗ ; ⟶ ; T, 1∞ ∂ (f(τ′_{1}, … τ′_{p})) \overrightarrow{ϵ} f(∂(τ′_{1}), … ∂(τ′_{p})) ( ∗ ; ⟶ ; P, •∞) f(ρ_{1}, … ρ_{p})

Again, the subproof using axioms R at occurrence 1 and the subproof using axioms T at the occurrence 1 are in H_{n}, and cannot have exactly one axiom at the empty occurrence. Therefore they are composed of a succession of proofs in all directions. Then we can prove:

∂ (f(τ_{1}, … τ_{p})) \overrightarrow{ϵ} f(∂(τ_{1}), … ∂(τ_{p})) ∗ ; ⟶ ; 2 f(a : τ_{1} ; ∂(τ_{1}), … a : τ_{p} ; ∂(τ_{p})) ∗ ; ⟶ ; T, •21∞

f(a : τ_{1} ; ∂(τ′_{1}), … a : τ_{p} ; ∂(τ′_{p})) ∗ ; ⟶ ; P, •21∞ f(a : τ_{1} ; ∂(ρ_{1}), … a : τ_{p} ; ∂(ρ_{p})) ∗ ; ⟶ ; R, •1∞
f(a : σ_{1} ; ∂(ρ_{1}), … a : σ_{p} ; ∂(ρ_{p}))

Case r is (∂ ▷ f): Then s must be an axiom (f ▷ X).

Subcase X is ∂: The proof is of the form:

∂(f(τ)) ⟶_{ϵ} f(∂(τ_{1}), … ∂(τ_{p})) ∗ ; ⟶ ; •1∞ f(∂(σ_{1}), … ∂(σ_{p})) ⟶_{ϵ} ∂(f(σ))

A shorter proof is the composition of subproofs at occurrences i1 applied at occurrences 1i to ∂(f(τ)).

Subcase X is a: The proof is of the form

∂(f(τ_{1}, … τ_{p})) \overrightarrow{ϵ} f(∂(τ_{1}), … ∂(τ_{p})) ∗ ; ⟶ ; R, •1∞ f(∂(τ′_{1}), … ∂(τ′_{p})) ∗ ; ⟶ ; ∂ ▷ a, •

f(a : τ′_{1} ; ∂(τ′_{1}), … a : τ′_{p} ; ∂(τ′_{p})) ∗ ; ⟶ ; S, •1∞ f(a : σ_{1} ; ∂(τ′_{1}), … a : σ_{p} ; ∂(τ′_{p})) ∗ ; ⟶ ; T, •21∞

f(a : σ_{1} ; ∂(ρ_{1}), … a : σ_{p} ; ∂(ρ_{p})) \overrightarrow{ϵ} a : f(σ_{1}, … σ_{p}) ; f(∂(ρ)_{1}, … ∂(ρ)_{p})

Then, we can prove

\begin{matrix}∂(f(τ_{1}, … τ_{p})) \overrightarrow{ϵ} a : f(τ_{1}, … τ_{p}) ; f(∂(τ), … ∂(τ)) ∗ ; ⟶ ; R ∪ S, 1•∞ \\ a : f(σ_{1}, … σ_{p}) ; f(∂(τ), … ∂(τ)) & ∗ ; ⟶ ; R ∪ T, 2•∞ & a : f(τ_{1}, … τ_{p}) ; f(∂(ρ), … ∂(ρ)) \end{matrix}

Subcase X is g: is not possible.

Case s is (a ▷ ∂): This case is symmetric to the case r where is (∂ ▷ a).

Case neither r is (∂ ▷ X), nor is s (∂ ▷ X): Then the axioms r and s are linear on the right and left, respectively and commutes with their right and left neighbors, so we get a proof matching:

( ∗ ; ⟶ ; k•∞)^{k∈D} ⟶_{r,ϵ} ( δ ; ⟶ ; k)^{k∈D} ⟶_{ϵ} ( ∗ ; ⟶ ; k•∞)^{k∈D}

We show that the inclusion

⟶_{r,ϵ} ( δ ; ⟶ ; k)^{k∈D} ⟶_{s,ϵ} ⊂_{H_{n}} ∗ ; ⟶ ; •∞ δ ; ⟶ ; s,ϵ ∗ ; ⟶ ; •∞

by cases on r and s.

Case r is (X ▷ ∂) or s is ∂ ▷ X: The middle equality must be empty. The two axioms r and s must be inverse and annihilate each other.

Other cases: In the remaining cases, neither r nor s are ∂ axioms. The middle axiom cannot be a ∂ axiom. The remaining cases are then exactly those of the record term algebra.

We derive the mutation in the record term algebra (figure 2): For all other pairs of terms (τ, σ), if they have identical top symbols, they are decomposable; otherwise they produce a collision.

Theorem 11 Unification in the generic record algebra is decidable and unitary unifying.

\underline{Proof}: The theory is strict (we exhibited a compatible ordering). Therefore, the rules mutation, decomposition, collision, fusion and generalization applied any order form a complete semi-algorithm for unification. It is unitary since mutation does not introduce any disjunction.

All transformations are stable in the sets T^{n} and decrease in the following lexicographic ordering:

1. the number of symbols f^{Row(L)} in the lexicographic order of decreasing Card (L) (that is, bigger sets count less: mutate (a ▷ f)),

2. the number of symbols a^{L} : ; counted in the lexicographic order of decreasing Card (L) (mutate (a ▷ b)),

f^{Row(L)}(σ_{i})_{i∈[1,p]} ˙= a^{L} : α ; γ ˙= e ; ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- ≻

∃ α_{i}, γ_{i}_{i∈[1,p]} · ⋀ \{ \begin{matrix}a^{L} : α ; γ ˙= e \\ α ˙= fType(α_{1}, … α_{p}) \\ γ ˙= f^{Row(a.L)}(γ_{1}, … γ_{p}) \\ σ_{i} ˙= a^{L} : α_{i} ; γ_{i} i ∈ [1, p] \end{matrix}

Mutate(a ▷ f)

a^{L} : τ ; σ ˙= b^{L} : α ; β ˙= e ; --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- ≻ ; ∃ γ · ⋀ \{ \begin{matrix}b^{L} : α ; β ˙= e \\ σ ˙= b^{a.L} : α ; γ \\ β ˙= a^{b.L} : τ ; γ \end{matrix}  Mutate(a ▷ b)

a^{L} : τ ; ρ ˙= ∂^{L}(α) ˙= e ; ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- ≻ ; ∂^{L}(α) ˙= e ∧ τ ˙= α ∧ ρ ˙= ∂^{a.L}(α)  Mutate(∂ ▷ b)

f^{Row(L)}(σ_{1}, … σ_{p}) ˙= ∂^{L}(α) ˙= e ; -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- ≻ ; ∃ (α)_{i∈[1,p]} · ⋀ \{ \begin{matrix}∂^{L}(α) ˙= e \\ α ˙= fType(α_{1}, … α_{p}) \\ σ_{i} ˙= ∂^{L}(α_{i}) & i ∈ [1, p] \end{matrix} Mutate(f ▷ ∂)

Figure 2: Mutation in the generic algebra of record terms

3. the number of other symbols (other mutations and decomposition),

4. the sum of heights of terms (generalization),

5. the number of multi-equations (fusion).

Thus, applying the rules in any order always terminates.

6 Comparison with other work

In our approach, records are terms of a sorted algebra modulo regular equations. We have infinitely many equations (indexed by labels), but all equations act locally on terms, since the axioms are of depth at most 2.

In record calculi, it is possible to define a record s by adding a field (a = x) to the record r whether r already defines field a or not. It is tempting to reflect the structure of record objects into record types and assign the type (a : τ ; σ) to s provided s has type σ. In the case, where r already defines field a, it has a type of the form (a : τ′ ; ρ) ; then s has type (a : τ ; (a : τ′ ; ρ)) . The type component of r on field a is meaningless in the type of s, since the field of s is x. This can be realized by adding a non-regular absorption axiom

a : α ; a : α′ ; γ = a : α ; γ

Such an axiom much be treated carefully. This approach has been taken in two recent proposals for record terms, one by A. Hense and G. Smolka [HS92], the other by B. Berthomieu [Ber93]. Both approaches also restrict terms to the equivalent of our canonical terms. The notion of expansion is not based on distributivity equations; instead, it is incorporated in the substitutions themselves, using more complex sorts to control substitution.

For instance, the record term a : τ ; abs is coded as a : τ ; αabs in Berthomieu’s system; the sort abs assigned to α restricts any substitution to be at least of the form α ↦ ℓ : abs ; βabs . The following E-equality in record terms

a : τ ; abs = a : τ ; (b : abs ; abs )

is not an equality in Berthomieu’s system [Ber93]; the two equivalent terms are only in the instance relation

a : τ ; αabs < a : τ ; (b : abs ; α^{′abs} )

The right hand side is equal to the substitution of variable α of sort abs by b : abs ; α^{′abs} in the left hand side. This is the smallest possible substitution for α as a result of its sort constraint. Berthomieu’s approach is more complex in the case of simple record algebras, but it seems to simplify the treatment of generic record algebras: the generic record term

a : τ ; β → ∂(α)

would be represented in Berthomiue’s system as

a : τ ; γ^{∀ β· β→α}

using the explicit quantifiers in sorts. Then, the variable γ can be replaced by ℓ : ρ ; γ^{′∀ β· β→α} provided ρ is an instance of the type scheme ∀ β · β → α, that is, of the form σ → α. The sorts are terms and can also be instantiated during unification. This is an additional difficulty but also a gain of expressiveness.

We find the approach of Berthomieu quite interesting for the extension to generic record algebras, but we prefer our approach for simple record terms, since it fits nicely in a known framework.

Conclusion

We introduced a framework in which syntacticness of an equational presentation can be studied more easily. We defined record algebras over an initial set of symbols as the quotient of a free sorted algebras by left commutativity and distributivity axioms. We showed that it is syntactic and decidable and we deduced an efficient, unitary unifying algorithm for unification. Many variants of record algebras can be obtained by restricting the terms by a signature that is compatible with the equations. Different instances have already been used to provide type systems for languages with records.

The extension of record algebras to recursive types has not been addressed here. In practice, the algorithm that we described also works with non-strict systems of multi-equations, which represent recursive terms. However, the notion of regular trees modulo equations has to be defined before any correspondence between these and non-strict systems of multi-equations can be studied. It seems that the algebra of record terms is sufficiently constrained by the sorts that there would be a close correspondence between the two, which cannot be expected in general.

The extension of record algebras to generic record algebras is a difficult step. Even if it can be extended to higher order genericity, it seems too difficult to be the right notion. Making a closer connection with the record terms of Berthomieu is a promising approach. The generality of record algebras suggests that there should be other useful applications.

[Ber93] Bernard Berthomieu. Tagged types, a theory of order sorted types for tagged expressions. Research Report 93083, LAAS, 7, Avenue du Colonnel Roche, 31077 Toulouse, France, March 1993.

[HS92] Andreas V. Hense and Gert Smolka. A verification of extensible record types. In Zhongzhi Shi, editor, Proceedings of the IFIP TC12/WG12.3 International Workshop on Advances in Automated Reasoning, pages 13–16, Beijing, P.R. China, July 1992. International Federation for Information Processing, Elsevier, North-Holland, Excerpta Medica. to appear.

[Kir85] Claude Kirchner. Méthodes et outils de conception systématique d’algorithmes d’unification dans les théories équationnelles. Thèse de doctorat d’état en informatique, Université de Nancy 1, 1985.

[KJ90] Claude Kirchner and Jean-Pierre Jouannaud. Solving equations in abstract algebras: a rule-based survey of unification. Research Report 561, Université de Paris Sud, Orsay, France, April 1990.

[KK89] Claude Kirchner and François Klay. Syntactic theories and unification. CRIN & INRIA-Loraine, Nancy (France), 1989.

[MM82] Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258–282, 1982.

[Nip89] Tobias Nipkow. Proof transformations for equational theories. Technical Report 181, University of Cambridge, Computer laboratory, 1989.

[Pie91] Benjamin C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, Pittsburg, Pensylvania, February 1991.

[Rém90] Didier Rémy. Algèbres Touffues. Application au Typage Polymorphe des Objets Enregistrements dans les Langages Fonctionnels. Thèse de doctorat, Université de Paris 7, 1990.

[Rém92a] Didier Rémy. Extending ML type system with a sorted equational theory. Research Report 1766, Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, 1992.

[Rém92b] Didier Rémy. Projective ML. In 1992 ACM Conference on Lisp and Functional Programming, pages 66–75, New-York, 1992. ACM press.

[Rém93] Didier Rémy. Type inference for records in a natural extension of ML. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design. MIT Press, 1993.