Unification in Order-Sorted Signatures

Uwe Waldmann

Forschungsbericht Nr. 298, 1989 (Revised version, 1990 )

Uwe Waldmann Lehrstuhl Informatik V Universität Dortmund Postfach 50 05 00 4600 Dortmund 50 West Germany E-Mail: uwe@unidoi5.ls5.informatik.uni-dortmund.de

Abstract

Unification in an order-sorted signature differs substantially from many-sorted unification. If the signature is finite and regular, unification is finitary, but the size of a minimal complete set of unifiers may grow exponentially with the number of variables in the terms to be unified; besides the unifiability problem is in general NP-complete. We give a decidable necessary and sufficient criterion for unitary unifiability, i.e., for the existence of a most general unifier. Furthermore we prove that if this criterion is satisfied, the sort decreasingness of a term rewrite rule can be efficiently decided as well.

1 Introduction

Order-sorted signatures differ from many-sorted signatures in that sorts are related by a subsort ordering and that operator symbols may be overloaded. They simplify the presentation of partially defined functions and allow a more elegant formulation of error recovery and error propagation in algebraic specifications [Gog83, Gog86, SNGM87].

Unfortunately, unification in an order-sorted signature is more complicated that manysorted unification. Even if the signature is finite and regular, unification is in general not unitary, and the size of a minimal complete set of unifiers may grow exponentially with the number of variables in the terms to be unified; besides the unifiability problem is NP-complete in certain signatures [SS88].

In this paper we develop a criterion for unitary unifiability in order-sorted signatures.

2 Basic Notations

We use the standard symbols ∈, ∩, ∪, \, and × for the membership relation and the set theoretic operations intersection, union, set difference, and cartesian product. The subset relation is denoted by ⊆. The symbol ∅ represents the empty set, the set of natural numbers (including 0) is abbreviated by N. The expression A^{n} denotes the set of all tuples or strings over A with length n, the letter ε symbolizes the empty tuple or empty string. Finally A∗ and A^{+} are defined by A∗ := ⋃_{n≥0} A^{n} and A^{+} := ⋃_{n≥1} A^{n}.

A function f with domain A and range B is written f : A → B; for some A′ ⊆ A the set f(A′) := { f(x) | x ∈ A′ } is the image of A′ under f and f|_{A′} is the restriction of f to A′. The symbol id_{A} means the identity function from A to A. Given two functions f : A → B and g : B → C the composition (g ∘ f) : A → C of f and g is the function that maps every x ∈ A to g(f(x)) ∈ C; this will be denoted by x ↦ g(f(x)). For functions f : A_{1} → B and g : A_{2} → B where A_{1} ∩ A_{2} = ∅ the function (f ∪ g) : (A_{1} ∪ A_{2}) → B is defined by (f ∪ g)(x) := f(x) for x ∈ A_{1} and (f ∪ g)(x) := g(x) for x ∈ A_{2}.

A binary relation ≤ over A that is reflexive and transitive is a quasi-ordering; if it is also antisymmetric, it is called a partial ordering. An antireflexive, transitive, and antisymmetric relation is called a strict ordering. Let (A, ≤) be a partially ordered set. An element a ∈ A is maximal iff a ≤ b implies a = b for every b ∈ A. We say that a is the greatest element of A iff b ≤ a holds for every b ∈ A. Analogously we define “minimal” and “least” elements. A strict ordering < over A is said to be noetherian iff there is no infinite sequence (a_{1}, a_{2}, …) such that a_{i+1} < a_{i} for all i ∈ N.

Given strict orderings <_{1}, …, <_{n} on the sets A_{1}, …, A_{n}, respectively, the lexicographic combination < of the orderings <_{1}, …, <_{n} on A_{1} × ⋯ × A_{n} is defined as follows: We have (a_{1}, …, a_{n}) < (b_{1}, …, b_{n}) if and only if there is a j ∈ {1, …, n} so that a_{i} = b_{i} for 1 ≤ i < j and a_{j} <_{j} b_{j}. If the orderings <_{1}, …, <_{n} are noetherian, their lexicographic combination is noetherian, too.

A multiset M over a set A is a function from A to N. We can interpret M as an unordered collection of elements of A, in which elements may occur multiply; M(a) = n should then be read as “a occurs n times in M”. In general we shall use similar notations for multisets as for sets. Given a strict ordering <_{A} over A, the multiset extension < of <_{A} over the set of all finite multisets over A is defined as the least transitive relation such that M ∪ {b_{1}, …, b_{n}} < M ∪ {a} if n ≥ 0 and b_{i} <_{A} a for all i ∈ {1, …, n}. If the ordering <_{A} is noetherian, its multiset extension < is noetherian, too.

3 Signatures and Algebras

We shall first summarize some basic results about order-sorted signatures, algebras, and deduction, following [SNGM87].

Definition 3.1 An order-sorted signature is a triple (S, ≤, Σ), where S is a set of sorts, ≤ a partial ordering over S, and Σ a family { Σ_{w,s} | w ∈ S∗, s ∈ S } of (not necessarily disjoint) sets of operator symbols.

The ordering ≤ is extended componentwise to strings s_{1} … s_{n} ∈ S∗ and to pairs (w, s) ∈ S∗ × S, so we have s_{1} … s_{n} ≤ s′_{1} … s′_{n} iff s_{i} ≤ s′_{i} for 1 ≤ i ≤ n, and analogously (w, s) ≤ (w′, s′) iff w ≤ w′ and s ≤ s′.

In order to make the notation simpler and more intuitive we shall often write f : w → s instead of f ∈ Σ_{w,s} and f : → s instead of f ∈ Σ_{ε,s}. We shall also use Σ as an abbreviation for both (S, ≤, Σ) and ⋃_{w,s} Σ_{w,s}.

Definition 3.2 The set T_{Σ,s} of ground terms over Σ with sort s is the least set with the following properties:

(i) f ∈ T_{Σ,s} if f : → s_{0} and s_{0} ≤ s.

(ii) f(t_{1}, …, t_{n}) ∈ T_{Σ,s} if f : s_{1} … s_{n} → s_{0} such that s_{0} ≤ s and t_{i} ∈ T_{Σ,s_{i}} for every i ∈ {1, …, n}.

T_{Σ} := ⋃_{s∈S} T_{Σ,s} denotes the set of all ground terms over Σ.

Definition 3.3 The depth of a term t ∈ T_{Σ} is defined as follows:

(i) If t = f, then depth(t) = 0.

(ii) If t = f(t_{1}, …, t_{n}), then depth(t) = 1 + max({ depth(t_{i}) | 1 ≤ i ≤ n }).

Definition 3.4 Let (S, ≤, Σ) be an order-sorted signature. A (S, ≤, Σ)-algebra A consists of a family { A_{s} | s ∈ S } of sets and a function A_{f} : D_{f}^{A} → C_{A} for every f ∈ Σ such that the following conditions are fulfilled:

(i) A_{s} ⊆ A_{s′}, if s ≤ s′.

(ii) D_{f}^{A} is a subset of (C_{A})∗ where C_{A} := ⋃_{s∈S} A_{s}.

(iii) If f ∈ Σ_{w,s}, then A_{w} ⊆ D_{f}^{A} and A_{f}(A_{w}) ⊆ A_{s}.

We use A_{s_{1}...s_{n}} as an abbreviation for A_{s_{1}} × ⋯ × A_{s_{n}}, A_{ε} is some one-point set. (A function with domain A_{ε} may be considered as a constant.)

Obviously we can make T_{Σ} (which we shall abbreviate by T) a Σ-algebra by

T_{s} := T_{Σ,s}.

For f ∈ Σ we define D_{f}^{T} and T_{f} by

D_{f}^{T} := ⋃_{f:w→s} T_{w}

and

\begin{aligned}T_{f} & : & D_{f}^{T} & → & C_{T} \\ & & (t_{1}, …, t_{n}) & ↦ & f(t_{1}, …, t_{n}). \end{aligned}

Definition 3.5 Let A and B be two (S, ≤, Σ)-algebras. An (S, ≤, Σ)-homomorphism h : A → B is a function h : C_{A} → C_{B} such that:

(i) h(A_{s}) ⊆ B_{s} for each s ∈ S.

(ii) h(D_{f}^{A}) ⊆ D_{f}^{B} and h(A_{f}(a_{1}, …, a_{n})) = B_{f} (h(a_{1}), …, h(a_{n})) for all f ∈ Σ and (a_{1}, …, a_{n}) ∈ D_{f}^{A}.

A homomorphism h : A → B is called an isomorphism, iff a homomorphism h′ : B → A exists satisfying h′ ∘ h = id_{A} and h ∘ h′ = id_{B}.

For every fixed signature (S, ≤, Σ) the Σ-algebras and Σ-homomorphisms make up the category OSA_{Σ}.

As in the unsorted case, we have:

Theorem 3.6 The term algebra T_{Σ} is the initial Σ-algebra, it is determined uniquely (up to isomorphism).

4 Variables

Definition 4.1 An S-sorted variable set is a family V = { V_{s} | s ∈ S } of disjoint sets.

A variable x ∈ V_{s} is written x : s. We shall use V as an abbreviation for ⋃_{s∈S} V_{s}. Let (S, ≤, Σ) be an order-sorted signature and V be a variable set disjoint from Σ.

By componentwise union of Σ and V we get a new signature (S, ≤, Σ ∪ V) defined by (Σ ∪ V)_{ε,s} := Σ_{ε,s} ∪ V_{s} and (Σ ∪ V)_{w,s} := Σ_{w,s} for w ≠ ε. Now we can regard the term algebra T_{Σ∪V} as a (S, ≤, Σ)-algebra, which will be denoted by T_{Σ}(V).

The set of all variables in a term t ∈ T_{Σ}(V) is abbreviated by Var(t).

Definition 4.2 An assignment ν from a variable set V into a Σ-algebra A is a set of functions { ν_{s} : V_{s} → A_{s} | s ∈ S }.

Theorem 4.3 The algebra T_{Σ}(V) is the free Σ-algebra generated by V, i.e., for every Σ-algebra A and every assignment ν from V to A there is exactly one homomorphism ν∗ : T_{Σ}(V) → A that extends ν.

Definition 4.4 A substitution σ is an assignment from a variable set Y into the term algebra T_{Σ}(X). In general the uniquely determined extension σ∗ : T_{Σ}(Y) → T_{Σ}(X) of σ will also be denoted by σ.

A substitution σ : {x_{1}, …, x_{n}} → T_{Σ}(X) that maps the variables x_{1}, …, x_{n} to the terms t_{1}, …, t_{n}, respectively, is written σ = (x_{1} ← t_{1}, …, x_{n} ← t_{n}).

Definition 4.5 A substitution σ : X → T_{Σ}(Y) is called a renaming, if it is injective and if it maps every variable x : s from X to a variable of the same sort s.

Definition 4.6 A substitution σ : X → T_{Σ}(Y) is called a specialization, if it is injective and if it maps every variable x : s from X to a variable (of the same or of a smaller sort).

5 Equations

Definition 5.1 A Σ-equation is a triple (X, t, t′), where X is a variable set and t and t′ are terms from T_{Σ}(X).

We shall usually write (∀X)t = t′ instead of (X, t, t′); if X = Var(t) ∪ Var(t′), we may omit the variable set.

Definition 5.2 A pair (Σ, E), where Σ is a signature and E is a set of Σ-equations, is called a specification.

Definition 5.3 Let (∀X)t = t′ be an equation and A be a Σ-algebra. If ν∗(t) = ν∗(t′) holds for every assignment ν : X → A, we say that A satisfies the equation (∀X)t = t′, which is abbreviated by

A ⊧ (∀X)t = t′.

A Σ-algebra A satisfies a set E of equations, iff it satisfies every equation from E; such an algebra A is called a (Σ, E)-algebra. Provided that every (Σ, E)-algebra A satisfies the equation (∀X)t = t′, we write

E ⊧ (∀X)t = t′.

Whether an equation (∀X)t = t′ is satisfied by an algebra or not may depend on the variable set X. Obviously it is always possible to rename the variables in an equation. The following lemma yields a criterion under which circumstances it is even possible to add or to delete a variable.

Lemma 5.4 Let Σ be a signature and (∀X)l = r be a Σ-equation. If there is a ground term t ∈ T_{Σ,s}, or if X contains a variable of the sort s, then for every Σ-algebra A:

A ⊧ (∀(X ∪ {y : s}))l = r ⟺ A ⊧ (∀X)l = r.

Inference System 5.5 Let Σ be a signature and E be a set of Σ-equations. Using the following rules new equations can be derived from E.

(E1) Reflexivity  (∀X)t = t
(E2) Symmetry  \frac{(∀X)t = t′}{(∀X)t′ = t}
(E3) Transitivity  \frac{(∀X)t = t′, (∀X)t′ = t′′}{(∀X)t = t′′}
(E4) Congruence  \frac{(∀X)t_{1} = t′_{1}, …, (∀X)t_{n} = t′_{n}}{(∀X)f(t_{1}, …, t_{n}) = f(t′_{1}, …, t′_{n})}

if both f(t_{1}, …, t_{n}) and f(t′_{1}, …, t′_{n}) are well-formed terms

(E5) Substitutivity (∀X)ν∗(t) = ν∗(t′)

if (∀Y)t = t′ is an element of the initial set of equations E and if ν : Y → T_{Σ}(X) is a substitution

If an equation (∀X)t = t′ can be derived from E using the rules (E1)–(E5), this is denoted by

E ⊢ (∀X)t = t′

or

t ≡_{E}^{X} t′.

Definition 5.6 Let Σ be a signature, X a variable set, and E a set of Σ-equations. The Σ-algebra T_{Σ,E}(X) (abbreviated by T) is defined as follows:

T_{s} := { [t] | t ∈ T_{Σ}(X)_{s} },

where [t] := { t′ ∈ T_{Σ}(X) | E ⊢ (∀X)t = t′ } denotes the equivalence class of t. For f ∈ Σ let D_{f}^{T} and T_{f} be defined by

D_{f}^{T} := ⋃_{f:w→s} T_{w}

and

T_{f} :  D_{f}^{T}  → C_{T}
([t_{1}], …, [t_{n}]) ↦ [f(t_{1}, …, t_{n})]
for representatives t_{1}, …, t_{n} such that t_{i} ∈ T_{Σ}(X)_{s_{i}} and f : s_{1} … s_{n} → s.

Theorem 5.7 Let Σ be a signature and E be a set of Σ-equations. Then the following properties are equivalent:

(i) E ⊢ (∀X)t = t′.

(ii) Every (Σ, E)-algebra A satisfies the equation (∀X)t = t′.

(iii) The algebra T_{Σ,E}(X) satisfies the equation (∀X)t = t′.

Theorem 5.8 The algebra T_{Σ,E}(X) is the free (Σ, E)-algebra generated by X, i.e., for every (Σ, E)-algebra A and every assignment ν : X → A there is exactly one homomorphism ν̃ : T_{Σ,E}(X) → A such that ν(x) = ν̃_{s}([x]) for all x ∈ X_{s}.

Corollary 5.9 The algebra T_{Σ,E} := T_{Σ,E}(∅) is initial in the set of all (Σ, E)-algebras, i.e., for every (Σ, E)-algebra A there is exactly one homomorphism h : T_{Σ,E} → A.

6 Unifiers and Weakenings

From now on we shall always assume that (S, ≤, Σ) is a signature such that there is a ground term t ∈ T_{Σ,s} for every sort s ∈ S.

Definition 6.1 Let t ∈ T_{Σ}(Y), t′ ∈ T_{Σ}(Y′). We say that t′ is an instance of t (abbreviated by t′ ≥ t), iff there is a substitution θ : Y → T_{Σ}(Y′) such that t′ = θ(t). Given a set E of equations, t′ is called an E-instance of t (abbreviated by t′ ≥_{E} t), iff there is a substitution θ : Y → T_{Σ}(Y′) such that t′ ≡_{E} θ(t).

The notions instance and E-instance may be extended to substitutions:

Definition 6.2 Let σ : X → T_{Σ}(Y) and σ′ : X → T_{Σ}(Y′) be two substitutions. We say that σ′ is an instance of σ (abbreviated by σ′ ≥ σ), iff there exists a substitution θ : Y → T_{Σ}(Y′) such that σ′ = θ ∘ σ. Similarly σ′ is called an E-instance of σ (abbreviated by σ′ ≥_{E} σ), iff there is a substitution θ : Y → T_{Σ}(Y′) such that σ′ ≡_{E} θ ∘ σ, i.e., σ′(x) ≡_{E} θ(σ(x)) for each x ∈ X.

The quasi-ordering ≥ is called subsumption ordering. We write t > t′, iff t ≥ t′ and t′ ≱ t hold (analogously for substitutions), the relation > is called strict subsumption ordering.

Definition 6.3 An equation system over T_{Σ}(X) is a finite multiset of equations t ≐ t′, where t, t′ ∈ T_{Σ}(X).

Definition 6.4 Let Γ be an equation system over T_{Σ}(X). A substitution σ : X → T_{Σ}(Y) is said to be a unifier of Γ, iff σ(t) = σ(t′) holds for all equations t ≐ t′ ∈ Γ. A substitution σ : X → T_{Σ}(Y) is called an E-unifier of Γ, iff σ(t) ≡_{E} σ(t′) holds for all equations t ≐ t′ ∈ Γ. The set of all unifiers of Γ is denoted by SU(Γ), SU_{E}(Γ) represents the set of all E-unifiers of Γ.

A unifier σ of an equation system {t ≐ t′} is also called a unifier of t and t′.

Definition 6.5 Let Γ be an equation system over T_{Σ}(X). A subset U ⊆ SU(Γ) is called complete, iff for every unifier σ′ : X → T_{Σ}(Y′) there exists a σ : X → T_{Σ}(Y) from U such that σ′ is an instance of σ. Analogously a subset U ⊆ SU_{E}(Γ) is called complete, iff for every E-unifier σ′ : X → T_{Σ}(Y′) there exists a σ : X → T_{Σ}(Y) from U such that σ′ is an E-instance of σ.

Definition 6.6 A complete set U of unifiers or E-unifiers of Γ is said to be minimal, iff it does not contain two different substitutions σ, σ′ ∈ U so that σ′ ≥ σ or σ′ ≥_{E} σ, respectively.

A complete set of unifiers of Γ is called a CSU, a minimal and complete set of unifiers of Γ is called a μCSU (and similarly CSU_{E} or μCSU_{E} for E-unifiers).

Definition 6.7 A specification (Σ, E) is said to be unitary unifying, if for all terms t, t′ ∈ T_{Σ}(X) there is a μCSU_{E} containing at most one element; it is called finitary unifying, if it is not unitary unifying and if there exists a finite μCSU_{E} for all terms t, t′ ∈ T_{Σ}(X). Provided that the specification (Σ, E) is not unitary or finitary unifying and that there is a μCSU_{E} for all terms t, t′ ∈ T_{Σ}(X), it is called infinitary unifying. If there are terms t, t′ ∈ T_{Σ}(X) having no μCSU_{E}, a specification is said to be of type zero.

Fages and Huet [FH83] have shown that (in the unsorted case) there are specifications (Σ, E) such that certain equations t ≐ t′ do not have a μCSU_{E}. In order-sorted signatures such a situation can be encountered even if the set of equations E is empty [Wal86]. If minimal and complete sets of E-unifiers exist, however, we have: If U_{1} and U_{2} are two μCSU_{E} of an equation system, then there is a bijection η : U_{1} → U_{2} such that σ ≥_{E} η(σ) and η(σ) ≥_{E} σ for each σ ∈ U_{1}.

Definition 6.8 Let (S, ≤, Σ) be a signature, t a term in T_{Σ}(X), and s a sort in S. A substitution σ : X → T_{Σ}(Y) is called a weakening from t to s, iff σ(t) ∈ T_{Σ}(Y)_{s}. The set of all weakenings from t to s is denoted by SW(t, s).

Definition 6.9 Let t be a term over Σ and s a sort in S. A subset W ⊆ SW(t, s) is said to be complete, iff for each weakening σ′ : X → T_{Σ}(Y′) in SW(t, s) there exists a σ : X → T_{Σ}(Y) in W such that σ′ is an instance of σ.

Definition 6.10 A complete set of weakenings W from t to s is called minimal, iff it does not contain two distinct substitutions σ, σ′ ∈ W so that σ′ ≥ σ.

We write CSW as an abbreviation for a complete set of weakenings and μCSW for a minimal and complete set of weakenings.

Definition 6.11 Let S′ be a subset of (S, ≤). The set lbd(S′) of the lower bounds of S′ is defined by

lbd(S′) := { s ∈ S | s ≤ s′ for each s′ ∈ S′ }.

7 Regularity

We will at first consider the unification modulo the empty set of equations E. The following example demonstrates that order-sorted unification may be infinitary even if the signature is finite [SNGM87].

Example 7.1

\begin{aligned}(S, ≤) & = & \{ s_{1} ≤ s_{0}, s′_{1} ≤ s_{0} \} \\ Σ & = & \begin{aligned}\{ a & : & → s_{0}, \\ a & : & → s_{1}, \\ a & : & → s′_{1}, \\ f & : & s_{0} → s_{0}, \\ f & : & s_{1} → s_{1}, \\ f & : & s′_{1} → s′_{1} \} \end{aligned} \end{aligned}

Consider the equation x : s_{1} ≐ x′ : s′_{1}. For each n ∈ N we define the substitution σ_{n} by σ_{n} := (x : s_{1} ← f^{n}(a), x′ : s′_{1} ← f^{n}(a)). Every σ_{n} is a unifier of the equation and the set of all σ_{n} is complete and minimal, yet infinite. Hence x ≐ x′ cannot have a finite μCSU.

In order to avoid the problems arising from infinite μCSUs we have to restrict the class of signatures to be considered.

Definition 7.2 A signature Σ is called regular, if every term t ∈ T_{Σ}(V) has a least sort, which is denoted by LS(t). (We assume that V contains at least one variable of every sort.)

The following lemma [Smo86] shows that the regularity of a finite signature is decidable.

Lemma 7.3 A signature Σ is regular if and only if for every operator symbol f ∈ Σ and every w ∈ S∗ the set { s′ | f : w′ → s′, w ≤ w′ } is either empty or has a least element.

Proof Let Σ be a regular signature, f ∈ Σ an operator symbol, and w = s_{1} … s_{n} a word over S such that the set { s′ | f : w′ → s′, w ≤ w′ } is not empty. Given variables x_{1} : s_{1}, …, x_{n} : s_{n}, the term f(x_{1}, …, x_{n}) is well-formed. By hypothesis it has a least sort, so the set of all declarations f : w′ → s′ where w ≤ w′ must contain a declaration with a least s′, which is the least sort of f(x_{1}, …, x_{n}).

In order to prove the inverse direction let Σ be a signature such that for every operator symbol f ∈ Σ and every w ∈ S∗ the set { s′ | f : w′ → s′, w ≤ w′ } is either empty or has a least element. Now define a function sort : T_{Σ}(V) → S as follows:

sort(x : s) = s
sort(f(t_{1}, …, t_{n})) = min({ s | s_{i} := sort(t_{i}), f : w → s, s_{1} … s_{n} ≤ w })

It is easy to prove that sort(t) ≤ s holds if and only if t ∈ T_{Σ}(V)_{s} holds, thus we have sort(t) = LS(t). □

Lemma 7.4 If (S, ≤, Σ) is a finite and regular signature, then for every term t ∈ T_{Σ}(X) and every sort s ∈ S there is a finite complete set of weakenings from t to s such that each of these weakenings is a specialization.

Proof Suppose that the substitution σ is a weakening from t to s. The sort s_{x} being defined by s_{x} := LS(σx) for x ∈ Var(t) and s_{x} := LS(x) for x ∈ X \ Var(t), let ρ be the specialization ρ := (x ← y_{x} : s_{x} | x ∈ X). Obviously σ is an instance of ρ, besides an easy inductive proof shows that LS(ρt) = LS(σt), hence ρ is a weakening from t to s, too. The set of all specializations ρ so that LS(ρt) ≤ s and LS(ρx) = LS(x) for x ∉ Var(t) is a CSW from t to s. Since the set S of all sorts and the variable set Var(t) are finite, there exist only finitely many of these specializations modulo renaming, thus a finite CSW can be computed by systematic testing. □

A CSW can also be determined using a recursive algorithm. The following procedure is due to Schmidt-Schauß [SS86].

Let t ∈ T_{Σ}(X) and s ∈ S. If LS(t) ≤ s, we have

CSW(t, s) = {id_{X}},

otherwise we get depending on the form of t:

CSW(x : s′, s) = { id_{X\{x}} ∪ (x ← y : s′′) | s′′ maximal in lbd({s, s′}) },
CSW(f, s) = ∅,
CSW(f(t_{1}, …, t_{n}), s)
= { ( x ← y_{x} : s_{x} | x ∈ X) |

∃f : s_{1} … s_{n} → s̃ where s̃ ≤ s, lbd({LS(t_{i}), s_{i}}) ≠ ∅, s_{1} … s_{n} maximal,

∃σ_{1} ∈ CSW(t_{1}, s_{1}), …, σ_{n} ∈ CSW(t_{n}, s_{n}):
s_{x} maximal in lbd({ LS(σ_{i}x) | 1 ≤ i ≤ n }) for all x ∈ X }.

8 Computation of a CSU

The unification algorithm that will now be demonstrated is split into three passes. The first pass, which is described by the following inference system, makes no use of the sorts of the terms to be unified, thus it does not differ from an unsorted unification algorithm.

Inference System 8.1 The following rules transform an equation system over T_{Σ}(X) into a new equation system.

(U1) Decomposition \frac{Γ ∪ \{f(t_{1}, …, t_{n}) ≐ f(t′_{1}, …, t′_{n})\}}{Γ ∪ \{t_{1} ≐ t′_{1}, …, t_{n} ≐ t′_{n}\}}
(U2) Merging  \frac{Γ ∪ \{x ≐ t, x ≐ t′\}}{Γ ∪ \{x ≐ t, t ≐ t′\}}
if depth(t) ≤ depth(t′) and v(t) < v(x).
(U3) Commutation \frac{Γ ∪ \{t ≐ x\}}{Γ ∪ \{x ≐ t\}}
if v(t) < v(x).
(U4) Deletion  \frac{Γ ∪ \{t ≐ t\}}{Γ}

Without loss of generality let X = {x_{1}, x_{2}, … }; the function v is defined by v(x_{i}) := i and v(t) := 0 for t ∉ X.

Lemma 8.2 If an equation system Γ_{i} is transformed into an equation system Γ_{i+1} using one of the inference rules (U1)–(U4), then Γ_{i} and Γ_{i+1} have the same set of unifiers. The inference system terminates, i.e., starting with an arbitrary equation system Γ_{0} it yields after finitely many steps an equation system Γ_{k}, to which no rule can be applied. Provided that Γ_{k} does not contain an equation of the form f(t_{1}, …, t_{n}) ≐ g(t′_{1}, …, t′_{m}) where f ≠ g or n ≠ m, then all equations in Γ_{k} have the form x ≐ t where v(t) < v(x), and every variable occurs at most once on the left hand side of an equation.

Proof Obviously the rules (U1)–(U4) are correct. In order to prove that the inference system terminates, the complexity of an equation t ≐ t′ is defined to be the triple (max(depth(t), depth(t′)), v(t′), v(t)); the complexity of an equation system is the multiset of the complexities of its equations. Since the lexicographic ordering on triples of natural numbers and its extension to multisets are noetherian orderings, it is sufficient to show that every inference step decreases the complexity of the equation system.

If rule (U1) has been applied, each newly added equation has a complexity whose first component is smaller than the complexity of f(t_{1}, …, t_{n}) ≐ f(t′_{1}, …, t′_{n}). Using rule (U2) the first and the second component of the complexity remain unchanged, whereas the third component becomes smaller. If rule (U3) is used, the second component of the complexity of the new equation decreases and the first component is not modified, rule (U4) is trivial.

Suppose that the final equation system does not contain an equation f(t_{1}, …, t_{n}) ≐ g(t′_{1}, …, t′_{m}) where f ≠ g or n ≠ m. Consider a remaining equation t ≐ t′. We know that t or t′ is a variable, otherwise rule (U1) or (U4) could be applied.

If t were not a variable, t′ would be a variable and rule (U3) would be applicable, furthermore, because of rule (U3) and (U4) no equation y ≐ x where v(x) ≥ v(y) can remain.

Assume that two equations x ≐ t and x ≐ t′ remain. Without loss of generality we may suppose that depth(t) ≤ depth(t′). Because of rule (U2) we know that v(t) ≥ v(x) holds, but then t would have to be a variable and rule (U3) or (U4) could be applied to the equation x ≐ t. This contradicts our assumption. □

In the unsorted case an equation x ≐ t where x ≠ t is unifiable if and only if x does not occur in t, the most general unifier is σ = (x ← t). In order-sorted signatures it may happen that LS(t) ≰ LS(x) holds (thus the substitution (x ← t) would not be wellformed), on the other hand there may exist instances of t having a sort that is less or equal to LS(x). In such cases it is therefore necessary to compute a CSW from t to LS(x).

Lemma 8.3 Let Σ be a finite regular signature and let Γ = {y_{1} ≐ t_{1}, …, y_{m} ≐ t_{m}} be an equation system such that y_{j} does not occur in t_{i} for j ≤ i. Then a CSU of Γ can be effectively computed.

Proof For i ≤ m we recursively determine sets U_{i} of substitutions as follows:

U_{0} := { id_{X} }
U_{i} := { (σ|_{Y \{y′_{i}}} ∪ (y′_{i} ← σt′_{i})) ∘ θ | θ : X → T_{Σ}(Y) ∈ U_{i−1}, y′_{i} := θy_{i},

t′_{i} := θt_{i}, σ : Y → Y′ ∈ CSW(t′_{i}, LS(y′_{i})) },

where CSW(t, s) denotes a fixed complete set of weakenings from t to s consisting only of specializations.

At first we show that U_{i} is well-defined and that τ|_{X\{y_{1},...,y_{i}}} is a specialization for each τ ∈ U_{i}. This is obvious for i = 0, so let i > 0 and τ = (σ|_{Y \{y′_{i}}} ∪ (y′_{i} ← σt′_{i})) ∘ θ where θ : X → T_{Σ}(Y) ∈ U_{i−1}, y′_{i} = θy_{i}, t′_{i} = θt_{i} and σ : Y → Y′ ∈ CSW(t′_{i}, LS(y′_{i})). By the induction hypothesis θ|_{X\{y_{1},...,y_{i−1}}} is an injective function from X \ {y_{1}, …, y_{i−1}} to Y. Note especially that y′_{i} = θy_{i} is a variable. Since Var(t_{i}) ⊆ X \ {y_{1}, …, y_{i}}, we know that y′_{i} does not occur in t′_{i}. As σ is a weakening from t′_{i} to LS(y′_{i}) the substitution (y′_{i} ← σt′_{i}) is well-defined. Besides, the restriction of (σ|_{Y \{y′_{i}}} ∪ (y′_{i} ← σt′_{i})) to Y \ {y′_{i}} is an injective function from Y \ {y′_{i}} to Y′, thus τ|_{X\{y_{1},...,y_{i}}} is a specialization, too.

Next we prove that every τ ∈ U_{i} is a unifier for the equations 1 through i. (This equation system will be denoted by Γ_{i}.) Let i > 0 and τ = (σ|_{Y \{y′_{i}}} ∪ (y′_{i} ← σt′_{i})) ∘ θ where θ : X → T_{Σ}(Y) ∈ U_{i−1}, y′_{i} = θy_{i}, t′_{i} = θt_{i} and σ : Y → Y′ ∈ CSW(t′_{i}, LS(y′_{i})). By the induction hypothesis θ is a unifier for Γ_{i−1}. As τ is an instance of θ, we know that τ is also a unifier of Γ_{i−1}, so it is sufficient to show that τy_{i} = τt_{i} holds. We obtain

τy_{i} = ((σ|_{Y \{y′_{i}}} ∪ (y′_{i} ← σt′_{i})) ∘ θ)y_{i}
= (σ|_{Y \{y′_{i}}} ∪ (y′_{i} ← σt′_{i}))y′_{i}
= σt′_{i}
τt_{i} = ((σ|_{Y \{y′_{i}}} ∪ (y′_{i} ← σt′_{i})) ∘ θ)t_{i}
= (σ|_{Y \{y′_{i}}} ∪ (y′_{i} ← σt′_{i}))t′_{i}
= σt′_{i}

To prove that U_{i} is a complete set of unifiers of Γ_{i}, consider an arbitrary unifier τ′ of Γ_{i}. Note that τ′ is also a unifier of Γ_{i−1}, thus by the induction hypothesis it is an instance of some substitution θ ∈ U_{i−1}. Suppose that τ′ = ρ′ ∘ θ. As τ′y_{i} = τ′t_{i}, we get ρ′θy_{i} = ρ′θt_{i}. The restriction of θ to X \ {y_{1}, …, y_{i−1}} is a specialization, hence y′_{i} := θy_{i} is a variable that does nor occur in t′_{i} := θt_{i}, and we obtain ρ′y′_{i} = ρ′t′_{i}. Since LS(ρ′t′_{i}) ≤ LS(y′_{i}), there exists a weakening σ ∈ CSW(t′_{i}, LS(y′_{i})) such that ρ′ = μ ∘ σ. We define ρ := (σ|_{Y \{y′_{i}}} ∪ (y′_{i} ← σt′_{i})). Now it suffices to prove that ρ′ = μ ∘ ρ. Two cases have to be distinguished: If x ∈ Y \ {y′_{i}}, we have ρ′x = μσx = (μ ∘ ρ)x, otherwise (i.e., for x = y′_{i}) we obtain ρ′y′_{i} = ρ′t′_{i} = μσt′_{i} = (μ ∘ ρ)y′_{i}; this yields τ′ = ρ′ ∘ θ = μ ∘ ρ ∘ θ where ρ ∘ θ ∈ U_{i}. □

The subsequent theorem originates from Schmidt-Schauß [SS85].

Theorem 8.4 Given a finite regular signature (S, ≤, Σ) for every equation system Γ over T_{Σ}(X) a finite CSU is effectively computable.

Proof By Lemma 8.2 every equation system Γ over T_{Σ}(X) can be transformed into an equivalent equation system Γ′ such that either Γ′ contains an equation f(t_{1}, …, t_{n}) ≐ g(t′_{1}, …, t′_{m}) where f ≠ g or n ≠ m, or all equations in Γ′ have the form x ≐ t where v(t) < v(x) and every variable occurs not more than once on the left hand side of an equation. In the first case, Γ′ (and thus Γ) does not have a unifier, in the second case we use topological sorting [Knu73] and try to obtain an equation system {y_{1} ≐ t_{1}, …, y_{m} ≐ t_{m}} where y_{j} does not occur in t_{i} for j ≤ i. (Note that the numbering of the variables does not agree with the numbering that was used in the inference system.) If the topological sorting is successful, Lemma 8.3 may be applied to the sorted equation system, yielding a CSU of Γ. Otherwise there exist equations x_{i_{1}} ≐ t_{i_{1}}, …, x_{i_{l}} ≐ t_{i_{l}} such that x_{i_{l}} ∈ Var(t_{i_{1}}) and x_{i_{j}} ∈ Var(t_{i_{j+1}}) for 1 ≤ j ≤ l − 1. Since all equations x ≐ t satisfy the condition v(t) < v(x), not all t_{i_{j}} can be variables, so SU(Γ) is empty. □

9 Downward Uniqueness

In finite regular signatures unification is finitary. But unfortunately in certain signatures the problem to determine whether two terms are unifiable is NP-complete, just as the problem to determine whether there is a weakening from a term to a sort. Even if there are only two sorts (then the weakening problem is solvable in linear time), the size of a μCSU or μCSW can grow exponentially with the number of variables in the terms [SS88]. We shall now give a criterion, under which circumstances the unification in a signature is unitary.

Definition 9.1 A set of sorts (S, ≤) is called downward complete, iff for all s_{1}, s_{2} ∈ S the set lbd({s_{1}, s_{2}}) is either empty or contains a greatest element.

Lemma 9.2 The set (S, ≤) is downward complete if and only if for every finite nonempty subset S′ ⊆ S the set lbd(S′) is empty or has a greatest element.

Proof Let S be downward complete. We use induction on the cardinality of S′. If S′ = {s_{1}}, then lbd(S′) = { s ∈ S | s ≤ s_{1} } has the greatest element s_{1}. Otherwise let S′ = {s_{1}, …, s_{n+1}}. We distinguish between two cases.

Case 1: lbd({s_{1}, …, s_{n}}) = ∅, i.e., for each s ∈ S there is an i ∈ {1, …, n} such that s ≰ s_{i}. Then lbd({s_{1}, …, s_{n+1}}) is obviously empty.

Case 2: lbd({s_{1}, …, s_{n}}) has the greatest element s̃, so we have s ≤ s̃ if and only if s ≤ s_{i} for all i ∈ {1, …, n}. Consider the set M := lbd({s̃, s_{n+1}}). If M is empty, for each s ∈ S we obtain

s ≤ s_{i} for all i ∈ {1, …, n} ⟹ s ≤ s̃ ⟹ s ≰ s_{n+1},

hence lbd({s_{1}, …, s_{n+1}}) is also empty. Otherwise let ŝ be the greatest element of lbd({s̃, s_{n+1}}). Now we have

s ≤ ŝ ⟺ s ≤ s̃ and s ≤ s_{n+1}
⟺ s ≤ s_{i} for all i ∈ {1, …, n} and s ≤ s_{n+1}
⟺ s ∈ lbd({s_{1}, …, s_{n+1}}).

Thus ŝ is the greatest element of lbd({s_{1}, …, s_{n+1}}).

The inverse direction of the proof is trivial. □

Definition 9.3 A regular signature (S, ≤, Σ) is called downward unique, if (S, ≤) is downward complete and if for all s ∈ S, w ∈ S∗, f : w^{∘} → s^{∘} where s ≤ s^{∘} and w ≤ w^{∘} the set

{ w′ ∈ S∗ | ∃w̄ ∈ S∗, s̄ ∈ S so that f : w̄ → s̄, s̄ ≤ s, w′ ≤ w, w′ ≤ w̄ }

is empty or contains a greatest element.

Lemma 9.4 Given a regular signature (S, ≤, Σ) the following properties are equivalent:

(i) (S, ≤, Σ) is downward unique.

(ii) For each term t ∈ T_{Σ}(X) and every sort s ∈ S we have: Either there is no weakening from t to s or there exists a substitution σ_{s}^{t} such that LS(σt) ≤ s ⟺ σ ≥ σ_{s}^{t} for all substitutions σ : X → T_{Σ}(Y).

Proof At first we shall show by induction on the depth of t that (i) implies (ii) and that σ_{s}^{t} is a specialization (provided that it exists).

Let t = x ∈ X_{s′}. If lbd({s, s′}) is empty, there exists no substitution σ satisfying LS(σx) ≤ s, since LS(σx) ≤ LS(x) = s′ holds for all substitutions σ. Otherwise let ŝ be the uniquely determined greatest element of lbd({s, s′}). Define the substitution σ_{s}^{t} by σ_{s}^{t} := id_{X\{x}} ∪ (x ← y : ŝ). Now for all substitutions σ we have:

LS(σx) ≤ s ⟺ LS(σx) ≤ ŝ ⟺ σ ≥ σ_{s}^{t}.

Let t = f, s^{∘} := LS(t) and f : → s^{∘}. If s^{∘} ≤ s, let σ_{s}^{t} := id_{X}, otherwise there is no weakening from t to s.

Let t = f(t_{1}, …, t_{n}) with n ≥ 1 and let f : s_{1}^{∘} … s_{n}^{∘} → s^{∘} be a declaration for f such that s^{∘} = LS(t) and s̃_{i} := LS(t_{i}) ≤ s_{i}^{∘} for each i ∈ {1, …, n}, furthermore let w̃ := s̃_{1} … s̃_{n}. We have to distinguish between several cases.

Case 1: lbd({s, s^{∘}}) = ∅. Since LS(σt) ≤ LS(t) = s^{∘} holds for all substitutions σ, no σ satisfies LS(σt) ≤ s.

Case 2: otherwise: Let s̃ be the greatest element of lbd({s, s^{∘}}). For every substitution σ we have LS(σt) ≤ s ⟺ LS(σt) ≤ s̃. Now define the set W ⊆ S^{+} by

W := { w′ ∈ S^{+} | ∃w̄ ∈ S∗, s̄ ∈ S so that f : w̄ → s̄, s̄ ≤ s̃, w′ ≤ w̃, w′ ≤ w̄ }.

Case 2.1: W is empty. Assume there exists a σ such that LS(σt) ≤ s holds.

\begin{aligned}LS(σt) ≤ s & ⟺ & LS(σt) ≤ s̃ \\ & ⟺ & ∃f : s̄_{1} … s̄_{n} → s̄, s̄ ≤ s̃, ∀i ∈ \{1, …, n\}: LS(σt_{i}) ≤ s̄_{i} . \end{aligned}

On the other hand, we know that LS(σt_{i}) ≤ LS(t_{i}) = s̃_{i}, thus s′_{1} … s′_{n} ∈ W where s′_{i} := LS(σt_{i}). Hence our assumption is contradicted and SW(t, s) is empty.

Case 2.2: otherwise: Let ŝ_{1} … ŝ_{n} be the greatest element of W. We shall at first prove the following statement:

LS(σt) ≤ s ⟺ ∀i ∈ {1, …, n}: LS(σt_{i}) ≤ ŝ_{i}.

(⇒): Let LS(σt) ≤ s. Since this implies LS(σt) ≤ s̃, there must exist a declaration f : s̄_{1} … s̄_{n} → s̄ such that s̄ ≤ s̃ and s′_{i} := LS(σt_{i}) ≤ s̄_{i} for each i ∈ {1, …, n}. Besides we have LS(σt_{i}) ≤ LS(t_{i}) = s̃_{i}, so s′_{1} … s′_{n} ∈ W. It follows immediately that

s′_{1} … s′_{n} ≤ ŝ_{1} … ŝ_{n}.

(⇐): Let LS(σt_{i}) ≤ ŝ_{i} for every i. As ŝ_{1} … ŝ_{n} ∈ W, there are s̄_{1}, …, s̄_{n}, s̄ such that f : s̄_{1} … s̄_{n} → s̄, s̄ ≤ s̃ and ŝ_{i} ≤ s̃_{i} and ŝ_{i} ≤ s̄_{i} for each i ∈ {1, …, n}. Since

LS(σt_{i}) ≤ s̄_{i}, we obtain LS(σt) ≤ s̄ ≤ s̃ ≤ s.

This completes the proof of the auxiliary statement.

By the induction hypothesis we have for all i ∈ {1, …, n}: Either there is no weakening from t_{i} to ŝ_{i}, or there is a specialization σt_{i} ; ŝ_{i} such that for all σ:

LS(σt_{i}) ≤ ŝ_{i} ⟺ σ ≥ σt_{i} ; ŝ_{i}.

Case 2.2.1: There exists an i ∈ {1, …, n} such that LS(σt_{i}) ≰ ŝ_{i} holds for all substitutions σ. We can immediately conclude that no σ satisfies LS(σt) ≤ s.

Case 2.2.2: otherwise: We obtain

LS(σt) ≤ s ⟺ ∀i ∈ {1, …, n}: σ ≥ σt_{i} ; ŝ_{i}.

Since σt_{i} ; ŝ_{i} is a specialization, we know that σ ≥ σt_{i} ; ŝ_{i} if and only if LS(σx) ≤ LS(σt_{i} ; ŝ_{i}x) holds for all variables x ∈ X.

Case 2.2.2.1: There is a variable x ∈ X such that the set lbd({ LS(σt_{i} ; ŝ_{i}x) | 1 ≤ i ≤ n }) is empty. Obviously there cannot exist a weakening from t to s.

Case 2.2.2.2: otherwise: Because (S, ≤) is downward complete, for each x ∈ X there is a sort

s_{x} := max lbd({ LS(σt_{i} ; ŝ_{i}x) | 1 ≤ i ≤ n }).

We define σ_{s}^{t} by σ_{s}^{t} := ( x ← y_{x} : s_{x} | x ∈ X) and obtain:

LS(σt) ≤ s ⟺ ∀x ∈ X ∀i ∈ {1, …, n}: LS(σx) ≤ LS(σt_{i} ; ŝ_{i}x)
⟺ ∀x ∈ X: LS(σx) ≤ s_{x}
⟺ σ ≥ σ_{s}^{t}.

Hence the proof of the (i)⇒(ii) part is complete.

To prove the inverse direction we suppose at first that S is not downward complete. Thus there are sorts s_{1}, s_{2} ∈ S such that M := lbd({s_{1}, s_{2}}) is not empty and does not contain a greatest element.

Let t := x : s_{1} and s := s_{2}. For an arbitrary s′ ∈ M define the substitution σ_{s′} by σ_{s′} := (x ← y : s′). Obviously we have LS(σ_{s′}x) = s′ ≤ s_{2}. Assume that there is a substitution σ̃ such that for all substitutions σ:

LS(σx) ≤ s_{2} ⟺ σ ≥ σ̃.

We define σ := σ̃ and obtain s̃ := LS(σ̃x) ≤ s_{2} and s̃ ≤ LS(x) = s_{1}, hence s̃ ∈ M. On the other hand, s̃ is not the greatest element of M, therefore we have s̄ ≰ s̃ for some sort s̄ ∈ M. Now define σ̄ := (x ← ȳ : s̄). As s̄ ∈ M, we know that LS(σ̄x) = s̄ ≤ s_{2}, but σ̄ ≱ σ̃, contradicting our assumption.

Now suppose that S is downward complete but that Σ is not downward unique. Hence there are s′ ∈ S, w′ = s′_{1} … s′_{n} ∈ S∗, f : w^{∘} → s^{∘} where s′ ≤ s^{∘}, w′ ≤ w^{∘} such that the set

M := { w ∈ S∗ | ∃w̄ ∈ S∗, s̄ ∈ S: f : w̄ → s̄, s̄ ≤ s′, w ≤ w′, w ≤ w̄ }

is neither empty nor does it have a greatest element.

Consider t := f(x_{1} : s′_{1}, …, x_{n} : s′_{n}) and s := s′. For w = s_{1} … s_{n} ∈ M let the substitution σ_{w} be defined by

σ_{w} := (x_{1} ← y_{1} : s_{1}, …, x_{n} ← y_{n} : s_{n}).

For every w ∈ M we know that LS(σ_{w}t) = LS(f(y_{1}, …, y_{n})) ≤ s′. Assume there is a substitution σ̃ such that for all σ:

LS(σt) ≤ s′ ⟺ σ ≥ σ̃.

For each i ∈ {1, …, n} set s̃_{i} := LS(σ̃x_{i}) ≤ LS(x_{i}) = s′_{i}; in addition let w̃ := s̃_{1} … s̃_{n} and s̃:= LS(σ̃t).

Case 1: There is a declaration f : s̃_{1} … s̃_{n} → s̃. Inserting w̄ := w̃, s̄ := s̃ into the definition of M we see that w̃ ∈ M. As M does not have a greatest element, we know that ŵ ≰ w̃ for some ŵ = ŝ_{1} … ŝ_{n} ∈ M. Now ŵ ∈ M implies LS(σŵt) ≤ s′, on the other hand there is an i in {1, …, n} such that

LS(σŵx_{i}) = ŝ_{i} ≰ s̃_{i} = LS(σ̃x_{i}).

But then σŵ ≱ σ̃, thus the assumption must have been wrong.

Case 2: There is a declaration f : ŵ → s̃ such that w̃ ≤ ŵ but not w̃ = ŵ. Then we get LS(σŵt) ≤ s̃ ≤ s′ but σŵ ≱ σ̃. Also in this case the assumption is contradicted. □

The (i)⇒(ii) part of the above proof can easily be transformed into an algorithm to compute σ_{s}^{t} that needs O(nm) time, where n is the size of t and m is the size of Var(t). We can obtain O(n log m) time complexity if the resulting specialization is not propagated in a bottom-up manner but accumulated using a global AVL-tree.

Theorem 9.5 Let (S, ≤, Σ) be a regular signature, then the following properties are equivalent:

(i) (S, ≤, Σ) is downward unique.

(ii) For every equation system Γ over T_{Σ}(X) there is a complete set of unifiers having at most one member.

Proof At first we prove that (i) implies (ii). Let (S, ≤, Σ) be a regular and downward unique signature. By Lemma 9.4 for every term t ∈ T_{Σ}(X) and every sort s ∈ S there is a CSW from t to s containing at most one element. Since this implies that in the proof of Lemma 8.3 all sets U_{i} contain at most one element, the proof is complete.

To prove the inverse direction suppose that the signature (S, ≤, Σ) is not downward unique. Hence there is a term t ∈ T_{Σ}(X) and a sort s ∈ S such that the set W of all weakenings from t to s is not empty and does not contain a least element with respect to the subsumption ordering. Let Y := X ∪ {y : s}, where the variable y is not contained in X. Consider the equation t ≐ y : s. We choose an arbitrary θ ∈ W, then the substitution θ ∪ (y ← θ(t)) is a unifier of t ≐ y. Assume there is a most general unifier σ of this equation. Obviously we have LS(σ|_{X}t) = LS(σt) ≤ LS(y) = s and thus σ|_{X} ∈ W. Since W does not have a least element, there is a θ ∈ W satisfying θ ≱ σ|_{X}. Now define ρ := θ ∪ (y ← θt), this yields ρt = θt = ρy. Since ρ is a unifier of t ≐ y, it should be an instance of σ, however, we have ρ|_{X} = θ ≱ σ|_{X}. □

10 Overloaded vs. Non-Overloaded Unification

A number of more or less different descriptions of order-sorted algebras have been presented in the literature.

Our definition of order-sorted algebras is oriented chiefly towards [SNGM87]; however, we allow that an operator symbol has more than one arity. Similar descriptions can be found in [Obe62, Gog83, Gog86, SS85, SS88, Smo86, Kir88]. In all these papers an operator symbol in the signature is always interpreted by a single function of the algebra, no matter how many declarations there are for this operator. This approach is often called “non-overloaded”.

In other papers it is permitted that an operator symbol is interpreted by a family of functions (which can not always be considered as restrictions of a single function); often homomorphisms are considered as families of functions as well [GM85, GJM85, GM87, MGS87, Gan88, GKK88, KKM88]. This so-called “overloaded” approach makes certain prerequisite conditions (i.e., coherence and strong consistency) necessary for the term algebra to be initial [Wld89]. (GJM-regularity as defined in [GJM85] implies both strong consistency and regularity, but is in general an unnecessarily strong restriction.) Note that overloaded algebras induce a slightly different notion of equality on the set of terms, such that in the overloaded case, rule (E4) of Inference System 5.5 must be replaced by:

(E4) Congruence \frac{(∀X)t_{1} = t′_{1}, …, (∀X)t_{n} = t′_{n}}{(∀X)f(t_{1}, …, t_{n}) = f(t′_{1}, …, t′_{n})}
if t_{i}, t′_{i} ∈ T_{Σ}(X)_{s_{i}} and f : s_{1} … s_{n} → s_{0}

In both the overloaded and the non-overloaded worlds two terms are equal with respect to the empty set of equations, if and only if they are syntactically equal. If the set of equations E is not empty, but if all equations are sort preserving, overloaded and nonoverloaded E-equality are still the same [Wld89]. So all our results concerning syntactical unification and the results of Meseguer, Goguen, and Smolka [MGS87], and C. Kirchner [Kir88], who consider only sort preserving equational theories, are valid in both the overloaded and the non-overloaded case.

If E is not sort preserving, however, overloaded and non-overloaded E-equality may differ and overloaded and non-overloaded unifiers are not necessarily identical.

Example 10.1 Let (S, ≤, Σ) and E be defined by

\begin{aligned}(S, ≤) & = & \{ s_{1} ≤ s_{0}, s_{2} ≤ s_{0} \} \\ Σ & = & \begin{aligned}\{ a & : & → s_{1}, \\ b & : & → s_{2}, \\ f & : & s_{1} → s_{1}, \\ f & : & s_{2} → s_{2} \} \end{aligned} \\ E & = & \{ a = b \} \end{aligned}

Using the non-overloaded semantics the equation x_{1} : s_{1} ≐ x_{2} : s_{2} has the infinite μCSU_{E} { (x_{1} ← f^{n}(a), x_{2} ← f^{n}(b)) | n ∈ N }. In the overloaded case, however, the E-unification in this signature is unitary. (Note that the equation f(a) = f(b) is not valid in the overloaded semantics of E.)

11 Sort Decreasingness

Definition 11.1 Given a regular signature (S, ≤, Σ) a rewrite rule (∀Y)l → r is called sort decreasing, iff for all substitutions σ : Y → T_{Σ}(X) we have:

LS(σl) ≥ LS(σr).

An equation (∀Y)l = r is called sort preserving, iff for all substitutions σ : Y → T_{Σ}(X) we have:

LS(σl) = LS(σr).

Sort decreasingness is a very useful property in order-sorted rewriting. For sort decreasing rewrite rules confluence and Church-Rosser property are equivalent and the critical pair lemma holds as in the unsorted case. Unfortunately, there are regular and finite signatures, in which the problem to determine whether a rewrite rule is not sort decreasing is NP-complete. In downward unique signatures, however, an efficient decision procedure is possible.

Theorem 11.2 If the signature (S, ≤, Σ) is regular and downward unique, then a rewrite rule (∀X)l → r is sort decreasing, if and only if we have for all sorts s ∈ S: Either there is no weakening from l to s, or LS(σ_{s}^{l}r) ≤ s holds.

Proof We shall at first assume that the rule (∀X)l → r is sort decreasing. For regular signatures this is equivalent to

∀σ : X → T_{Σ}(Y): LS(σl) ≥ LS(σr),

this implies

∀s ∈ S ∀σ : X → T_{Σ}(Y): (LS(σl) ≤ s ⟹ LS(σr) ≤ LS(σl) ≤ s)

If there is a substitution σ such that LS(σl) ≤ s, then let σ := σ_{s}^{l}. We obtain

∀s ∈ S: (/ ∃σ : X → T_{Σ}(Y): LS(σl) ≤ s) ∨ LS(σ_{s}^{l}r) ≤ s.

To prove the inverse direction suppose that we have for all sorts s ∈ S: Either there is no weakening from l to s, or LS(σ_{s}^{l}r) ≤ s holds. In the second case we have in particular LS(σr) ≤ s for all instances σ of σ_{s}^{l}, hence

∀s ∈ S: (/ ∃σ : X → T_{Σ}(Y): LS(σl) ≤ s) ∨ (∀σ ≥ σ_{s}^{l}: LS(σr) ≤ s).

By the definition of σ_{s}^{l} this implies

∀s ∈ S: ((/ ∃σ: LS(σl) ≤ s) ∨ ∀σ: (LS(σl) ≤ s ⟹ LS(σr) ≤ s)).

Since the right hand side of the disjunction is trivially satisfied, if no σ satisfies LS(σl) ≤ s, we obtain

∀s ∈ S ∀σ: (LS(σl) ≤ s ⟹ LS(σr) ≤ s).

Now let s := LS(σl), this yields

∀σ: LS(σr) ≤ LS(σl),

hence l → r is sort decreasing. □

Corollary 11.3 If the signature (S, ≤, Σ) is regular and downward unique, then an equation (∀X)l = r is sort preserving, if and only if we have for all sorts s ∈ S: Either there is no weakening from l to s or from r to s, or both σ_{s}^{l} and σ_{s}^{r} exist and are equal modulo renaming of variables.

Proof The equation l = r is sort preserving, iff both the rewrite rules l → r and r → l are sort decreasing. As demonstrated above, this is equivalent to:

∀s ∈ S: ((/ ∃σ: LS(σl) ≤ s) ∨ LS(σ_{s}^{l}r) ≤ s)
∧ ((/ ∃σ: LS(σr) ≤ s) ∨ LS(σ_{s}^{r}l) ≤ s).

Choose any s ∈ S. By applying the distributive law and deleting those terms that are not satisfiable we obtain:

((/ ∃σ: LS(σl) ≤ s) ∧ (/ ∃σ: LS(σr) ≤ s))
∨ (LS(σ_{s}^{l}r) ≤ s ∧ LS(σ_{s}^{r}l) ≤ s)
⟺ (/ ∃σ: LS(σl) ≤ s ∨ LS(σr) ≤ s)
∨ (σ_{s}^{l} ≥ σ_{s}^{r} ∧ σ_{s}^{r} ≥ σ_{s}^{l})
⟺ (/ ∃σ: LS(σl) ≤ s ∨ LS(σr) ≤ s)
∨ σ_{s}^{l} equals σ_{s}^{r} modulo renaming of variables.

Since s could be chosen freely, the proof is complete. □

12 Remarks

Meseguer, Goguen, and Smolka have shown [MGS87], that unification in an order-sorted signature is unitary, provided that (S, ≤) is downward complete and that for all f ∈ Σ, s ∈ S ∪ {max}, and n ∈ N the set { s_{1} … s_{n} ∈ S∗ | f : s_{1} … s_{n} → s̃, s̃ ≤ s } is either empty or contains a greatest element, where s ≤ max holds for each s ∈ S. This criterion is sufficient, however, it is necessary only if untyped variables are permitted in the terms that are to be unified, and at least one of the terms to be unified is not an unsorted variable. This situation is demonstrated by the following example.

Example 12.1 Let (S, ≤, Σ) be defined by

\begin{aligned}(S, ≤) & = & \{ s_{2} ≤ s_{1}, s′_{2} ≤ s′_{1} \} \\ Σ & = & \begin{aligned}\{ f & : & s_{1} → s_{1}, \\ f & : & s′_{1} → s_{1}, \\ f & : & s_{2} → s_{2}, \\ f & : & s′_{2} → s_{2} \} \end{aligned} \end{aligned}

The equation f(x : untyped) ≐ x̃ : s_{2} has the minimal complete set of unifiers {(x ← y : s_{2}, x̃ ← f(y)), (x ← y′ : s′_{2}, x̃ ← f(y′))}. We can never encounter such a situation, however, if the variable x has a sort: If x has the sort s_{1} or s_{2}, it cannot be mapped to a variable with the sort s′_{2}, hence only the first substitution remains, similarly the first substitution must be excluded, if x has the sort s′_{1} or s′_{2}.

If only well-formed terms have to be unified (this implies in particular that untyped variables are not permitted), an algorithm that determines a weakening σ from f(t_{1}, …, t_{n}) to s can always make use of the fact that LS(σt_{i}) ≤ LS(t_{i}) holds. In this way the procedure that has been presented in Section 7 decreases the size of the search space and obtains (not in every signature, however) a higher efficiency in comparison with the IP-algorithm from [KKM88]. In general terms that are not well-formed do not offer this possibility.

13 Acknowledgements

I am grateful to Harald Ganzinger and Michael Hanus for finding a number of bugs in previous versions of this paper and I want to thank all members of the Lehrstuhl Informatik V for their support.

References

[FH83] F. Fages and G. Huet. Complete sets of unifiers and matchers in equational theories. In G. Ausiello and M. Protasi, editors, Proceedings of the 8th Colloquium on Trees in Algebra and Programming, LNCS 159, pages 205–220. Springer-Verlag, 1983.

[Gan88] H. Ganzinger. Order-sorted completion: The many-sorted way. Forschungsbericht 274, Universität Dortmund, Fachbereich Informatik, 1988.

[GJM85] J. A. Goguen, J.-P. Jouannaud, and J. Meseguer. Operational semantics for order-sorted algebra. In W. Brauer, editor, Proceedings of the 12th International Colloquium on Automata, Languages and Programming, pages 221–231, 1985.

[GKK88] I. Gnaedig, C. Kirchner, and H. Kirchner. Equational completion in ordersorted algebras (extended abstract). In M. Dauchet and M. Nivat, editors, Proceedings of the 13th Colloquium on Trees in Algebra and Programming, Nancy, LNCS 299, pages 165–184. Springer-Verlag, 1988.

[GM85] J. A. Goguen and J. Meseguer. Order-sorted algebra I: Partial and overloaded operators, errors and inheritance. Draft, SRI International and Center for the Study of Language and Information, 1985.

[GM87] J. A. Goguen and J. Meseguer. Order-sorted algebra solves the constructorselector, multiple representation and coercion problems. In Proceedings of the Second Symposium on Logic in Computer Science, 1987.

[Gog83] M. Gogolla. Algebraic specifications with partially ordered sorts and declarations. Forschungsbericht 169, Universität Dortmund, Abteilung Informatik, 1983.

[Gog86] M. Gogolla. Über partiell geordnete Sortenmengen und deren Anwendung zur Fehlerbehandlung in abstrakten Datentypen. Dissertation, Universität Braunschweig, Naturwissenschaftliche Fakultät, 1986.

[Kir88] C. Kirchner. Order-sorted equational unification. Draft, Centre de Recherche en Informatique de Nancy, 1988.

[KKM88] C. Kirchner, H. Kirchner, and J. Meseguer. Operational semantics of OBJ-3 (extended abstract). In T. Lepistö and A. Salomaa, editors, Proceedings of the 15th International Colloquium on Automata, Languages and Programming, LNCS 317, pages 287–301. Springer-Verlag, 1988.

[Knu73] D. E. Knuth. The Art of Computer Programming, Volume 1: Fundamental Algorithms, pages 258–265. Addison-Wesley, 2nd edition, 1973.

[MGS87] J. Meseguer, J. A. Goguen, and G. Smolka. Order-sorted unification. Technical Report CSLI-87-86, Center for the Study of Language and Information, 1987.

[Obe62] A. Oberschelp. Untersuchungen zur mehrsortigen Quantorenlogik. Mathematische Annalen, 145:297–333, 1962.

[Smo86] G. Smolka. Order-sorted Horn logic: Semantics and deduction. Draft, Universität Kaiserslautern, Fachbereich Informatik, 1986.

[SNGM87] G. Smolka, W. Nutt, J. A. Goguen, and J. Meseguer. Order-sorted equational computation. SEKI-Report SR-87-14, Universität Kaiserslautern, 1987.

[SS85] M. Schmidt-Schauß. A many-sorted calculus with polymorphic functions based on resolution and paramodulation. In A. Joshi, editor, Proceedings of the 9th International Joint Conference on Artificial Intelligence, Los Angeles, pages 1162–1168, 1985.

[SS86] M. Schmidt-Schauß. Unification in many-sorted equational theories. In J. H. Siekmann, editor, Proceedings of the 8th Conference on Automated Deduction, Oxford, pages 538–552, 1986.

[SS88] M. Schmidt-Schauß. Computational Aspects of an Order-Sorted Logic with Term Declarations. Dissertation, Universität Kaiserslautern, Fachbereich Informatik, 1988.

[Wal86] C. Walther. A classification of many-sorted unification problems. In J. H. Siekmann, editor, Proceedings of the 8th Conference on Automated Deduction, Oxford, pages 525–537, 1986.

[Wld89] U. Waldmann. Semantics of order-sorted specifications. Forschungsbericht 297, Universität Dortmund, Fachbereich Informatik, 1989.

Contents

1 Introduction 1 2 Basic Notations 1 3 Signatures and Algebras 2 4 Variables 3 5 Equations 4 6 Unifiers and Weakenings 6 7 Regularity 8 8 Computation of a CSU 9 9 Downward Uniqueness 12 10 Overloaded vs. Non-Overloaded Unification 16 11 Sort Decreasingness 17 12 Remarks 19 13 Acknowledgements 20