Citation
Term rewriting systems

Material Information

Title:
Term rewriting systems
Creator:
Sunshine, Todd Allan
Publication Date:
Language:
English
Physical Description:
iv, 96 leaves : illustrations ; 29 cm

Subjects

Subjects / Keywords:
Rewriting systems (Computer science) ( lcsh )
Rewriting systems (Computer science) ( fast )
Genre:
bibliography ( marcgt )
theses ( marcgt )
non-fiction ( marcgt )

Notes

Bibliography:
Includes bibliographical references (leaves 94-96).
General Note:
Submitted in partial fulfillment of the requirements for the degree, Master of Science, Computer Science.
General Note:
Department of Computer Science and Engineering
Statement of Responsibility:
by Todd Allan Sunshine.

Record Information

Source Institution:
|University of Colorado Denver
Holding Location:
|Auraria Library
Rights Management:
All applicable rights reserved by the source institution and holding location.
Resource Identifier:
34088538 ( OCLC )
ocm34088538
Classification:
LD1190.E52 1995m .S86 ( lcc )

Full Text
TERM REWRITING SYSTEMS
by
Todd Allan Sunshine
B.A., Cornell University, 1984
B.S., Cornell University, 1984
A thesis submitted to the
Faculty of the Graduate School of the
University of Colorado at Denver
in partial fulfillment
of the requirements for the degree of
Master of Science
Computer Science
1995


This thesis for the Master of Science
degree by
Todd Allan Sunshine
has been approved for the
Graduate School
by


Sunshine, Todd Allan (M.S., Computer Science)
Term Rewriting Systems
Thesis directed by Professor Jay Rothman
ABSTRACT
This thesis aims to provide an introduction to the concepts essential to a clear
understanding of term rewriting systems. The thesis is composed of two primary
elements; an introduction to the fundamental concepts underlying term rewriting
systems as well as an actual implementation of a term rewriting system. The basis
for understanding term rewriting systems is presented through a review of the
fundamentals of binary relations and abstract reduction systems. Then, in the
setting of abstract reduction systems, a detailed account of the Knuth-Bendix
completion procedure is given. Relevant concepts pertaining to rewriting systems
such as first-order unification, critical pairs, superposition, and term ordering are
also discussed. Also presented is an introduction to recent developments in the
arena of abstract completion. Based on the concepts introduced in the thesis a
fully functional term rewriting system is then presented. The complete source
listings of the term rewriting implementation are included. Of specific interest are
the algorithms used to perform unification, superposition, normalization, and
completion. Details of the programs use are demonstrated through annotated
examples showing both the users input and resulting output.
This abstract accurately represents the content of the candidates thesis. I
recommend its publication.
Signed
Jay Rothman
111


CONTENTS
Chapter
1. Introduction ............................................................ 1
2. Relations ............................................................... 2
2.1 Properties of Relations............................................. 3
2.2 Equivalence Relations............................................... 3
2.3 Closure of Relations ............................................... 4
2.4 Partial Orders...................................................... 4
3. Abstract Reduction Systems .............................................. 5
3.1 Terminating Reductions.............................................. 5
3.2 Confluence and the Church-Rosser Property........................... 6
3.3 Complete Reductions................................................. 8
3.4 Local Confluence ................................................... 9
3.5 Completion ........................................................ 11
4. Term Rewriting Systems.................................................. 12
4.1 Terms.............................................................. 12
4.2 Confluence of Term Rewriting Systems............................... 13
4.2.1 Unification................................................... 14
4.2.1.1 Syntactic Unification .................................. 14
4.2.1.2 Semantic Unification ................................... 16
4.2.2 Critical Pairs................................................ 18
4.2.2.1 Critical Pairs Completion .............................. 19
4.2.3 Knuth-Bendix Algorithm ....................................... 24
4.3 Termination of Term Rewriting Systems ............................. 26
4.3.1 Knuth-Bendix Ordering ..................................... 28
5. Abstract Completion .................................................... 30
6. Implementation of a TRS................................................. 33
6.1 Data Structures.................................................... 33
6.2 Unification........................................................ 34
6.3 Completion Procedure............................................... 35
6.4 Samples............................................................ 35
7. Conclusion.............................................................. 48
Appendix A................................................................. 49
References................................................................ 94
iv


1. Introduction
When equations are interpreted as programs, they are used in one direction
only, to rewrite an expression to a simpler one. A rewrite system is a set of such
one-way rules. Equational programs based on rewrite systems are usually
considered to be nondeterministic: an expression can be rewritten by any equation
whose left-hand side matches any subterm of the expression.
Knuth and Bendix [1970] proposed a procedure that attempts to construct a
convergent rewrite system from a finite axiomatization of an equational theory. In
their paper, they modestly state:
The formal development in this paper is primarily a precise statement of
what hundreds of mathematicians have been doing for many decades, so no
great claims of originality are intended for most of the concepts or methods
used. [p. 264]
However, the overall viewpoint was indeed revolutionary, as it formalized the
notion of a completion procedure in a concrete theoretical setting.
Many rewrite systems satisfy the Church-Rosser, or "confluence," property:
whenever two terms are equivalent, they can be rewritten to a common form. This
guarantees that the "normal forms" (unrewritable terms) computed by a program
are unique. Another important property is "termination": there are no infinite
sequences of rewrites. Termination ensures that there is at least one normal form
for every term. A system with both these properties is called "complete." A finite
convergent system is a decision procedure for the free word problem of the
underlying equational theory: an identity holds if and only if both its sides can be
rewritten to the identical normal form.
This "completion" procedure must be supplied with an ordering that is used to
determine in which direction a derived equation s = t is to be oriented into a one-
way rule, s - t or t > s. It deduces new equations by a process (involving
unification) called "superposition". When the left-hand side of an instance of a
rule can be rewritten by another rule, the two possible results of rewriting the left-
hand side instance form what is called a "critical pair."
These concepts will be presented formally, with precise definitions, as they
arise. This paper is organized from the "ground up", such that each section is
based on the preceding ones. In Section 2, a review of the basic properties of
relations are reviewed. In Section 3, the relevant properties common to all
reduction systems are introduced. In Section 4, the process of term rewriting as
presented by Knuth and Bendix is formalized. In Section 5, recent developments
in abstract completion are introduced. And finally, in Section 6, the concepts
introduced in the paper are synthesized into a fully functional term rewriting
system with samples of its execution.
1


2. Relations
Before attempting to present the essential features of rewriting systems, it will
first be necessary to review some fundamental background material. Therefore, in
this section some more or less well-known properties of relations are summarized.
First, let us recall some basic notions. A binary relation R on two sets A and
B is a subset of the Cartesian product A x B. That is, a binary relation is a set of
pairs. The first component of each pair is chosen from a set called the domain,
and the second component of each pair is chosen from a (possibly different) set
called the range. If R is a given binary relation, we shall often write xRy, instead
of (x, y) e R, to indicate that an element jc is related via R to an element y.
When we say that R is a binary relation on set A, we mean that R is a subset of
A x A (that is, the domain and range are the same set A).
There is the following possibility to picture a (finite) relation R on a set A.
Each element of A is represented by a point and two points corresponding to
elements x and y are connected by an arrow, x > y, whenever xRy holds. For
example, if A = {w, x, y, z) and R = {(x, y), (x, w), (y, x), (z, y)}, then R is
depicted in Figure 1.
Because of this graphical representation, the preferred notation for an arbitrary
relation is the arrow itself.
2


2.1 Properties of Relations
We say a relation R on a set A is:
(1) reflexive if, for all x e A, xRx.
(2) symmetric if, for all x,y e A, xRy implies yRx.
(3) transitive if, for all x,y,z e A, xRy and yRz imply xRz.
(4) irreflexive if, for all x e A, xRx is false.
(5) asymmetric if, for all x,y e A, xRy implies that yRx is false.
(6) antisymmetric if, for all x,y e A, xRy and yRx imply x = y.
Note that any asymmetric relation must also be irreflexive.
2.2 Equivalence Relations
Mathematical abstractions are based on equivalence relations. If we want to
ignore some inessential attributes of the objects in a certain set, then all objects
with the same essential attributes have to be identified. Such an identification is a
reflexive, symmetric, and transitive relation. This motivates the following
definition.
Definition 2.1 A relation R that is reflexive, symmetric, and transitive is
said to be an equivalence relation.
The following notation will be adopted. If R is an equivalence relation on a set A,
then instead of xRy we will write x ~ y. When x ~ y, x is said to be equivalent to
y modulo R.
In order to formalize the abstraction processes mentioned above we have to
decompose a given set into subsets. Let A be a set. A set P of pairwise disjoint
nonempty subsets of A is called a partition of A whenever A uP. Obviously,
each element of A belongs to exactly one subset.
We may say that abstraction on a set A is formalized by the concept of
partition. There is a one-to-one correspondence between partitions and equivalence
relations. If P is a partition on A, an equivalence ~ is defined by the rule: x ~ y if
and only if x and y are in the same class of the partition. Conversely, any
equivalence relation on A induces a partition on A consisting of its equivalence
classes. Hence, abstraction is based on equivalence relations.
3


2.3 Closure of Relations
Suppose P is a set of properties of relations. The P-closure of a relation > is
the smallest relation that includes all the pairs of and possesses the
properties in P. Therefore, for an arbitrary relation -> on a set, let:
= be the reflexive closure of -
<-> be the symmetric closure of
>+ be the transitive closure of -
<->= be the reflexive and symmetric closure of >
-V be the reflexive and transitive closure of -
-+ be the symmetric and transitive closure of >
<->* be the reflexive, symmetric, and transitive closure of
2.4 Partial Orders
Partial orders, especially in regard to the ordering of terms, plays an important
role in term rewriting systems. Therefore, while on the topic of relations let us
review some basic definitions that we will need later.
Definition 2.2 A reflexive, transitive, and antisymmetric relation on a set A
is called a partial order on A.
An example of a partial order is given by the set inclusion relation c over a
collection of sets.
A relation R on a set A is a total order if it is a partial order and for all
x,y A, either xRy or yRx. A total order is often called a linear order because
the elements of A can be laid out on a straight line such that x is to the left of y if
and only if xRy. The integers under the relation < form a total order, as do the
reals.
Definition 2.3 A reflexive and transitive relation on a set A is called a
preorder.
4


3. Abstract Reduction Systems
It is frequently the case that when mathematical concepts are involved, it is
easier to understand a concept in an abstract setting rather than a specific concrete
setting. This is precisely the case when considering reduction systems. We
therefore present the basic notions of reduction and replacement in an abstract
theoretic sense. We introduce reduction systems in this setting in order to develop
as far as possible the properties common to all reduction systems. Specifically, we
consider reduction and replacement in terms of a set of objects and binary relations
on that set.
A pair (A, >) consisting of a set A and a relation on it is called an abstract
reduction system. We say that a reduction system (A, ->) has a property (e.g., it
is terminating, confluent, etc.) if the relation -> has the property. In this context,
is called a reduction relation.
3.1 Terminating Reductions
Termination is one of the basic concepts in theoretical computer science, which
expresses in a certain way a finiteness condition. It should be intuitively clear that
such conditions are necessary for any constructive proof method.
To introduce terminating relations we need some more notions. Let > be an
arbitrary relation on a set A. Given elements x and y of A, we say that x is
reduced to y in one step if x - y, and y is called an (immediate) reduct of x. An
element x of A is called reducible if x has any reduct. Otherwise, jc is called
irreducible. Furthermore, we say that an element x of A has a terminating
reduction if there are elements x^xxm e A such that x, - xi+I for
i = 0,l,...,m-l and xm is irreducible. This will be written:
X = x0 -> X, ... xm
We say that an element x of A has a nonterminating reduction if there is an
infinite sequence x^x,,... e A such that xj xi+I for all i > 0, which will be
written:
X = X0 > X, x2 > ...
Which leads to the following definition:
Definition 3.1 A relation - on a set A is called terminating if every
element of A has only terminating reductions. That is, is
5


terminating if there is no infinite sequence x^x,,... e A such
that Xj -> xj+I for all i > 0.
Observe that a terminating relation - on a set A is necessarily acyclic, i.e., there
is no element x of A such that x ->* x holds. Hence the relation:
is not terminating since it is not acyclic. Even though every element of the
relation depicted in Figure 2 has a terminating reduction, the relation itself is not
terminating since it is not acyclic.
3.2 Confluence and the Church-Rosser Property
One of the fundamental computing paradigms is that of reduction. Computing
can be done by reducing an expression to a simpler one. Let (2 + 3) x (1 + 1) be
a term to compute. A reduction of this term is
(2 + 3) x (1 + 1) -> 5 x (1 + 1) 5 x 2 -> 10.
Other reductions are possible, as in
(2 + 3)x(l + l)->2x(l + l) + 3x(l + l)-2x2 + 3x2->4 + 6-10,
which ends with the same term. This confluence of all the reductions flowing out
of the same term is an essential property of this form of computing, as it
guarantees the same result regardless of the reduction strategy. Formally,
6


Definition 3.2 A reduction system (A, ->) is confluent if for all
w, x, y e A, w x and w ->* y imply that there exists a
z e A, such that x -> z and y >* z.
Confluence is depicted in Figure 3,
where a complete line indicates a hypothesis (if...) and a dashed line indicates a
conclusion (there exists
Confluence says that no matter how one diverges from a common ancestor,
there are paths joining at a common descendent. The implication is that
confluence is a fundamental property of every model of computation using
reduction, as it guarantees the independence of the result of a computation from the
reductions taken.
If -> is a reduction relation, then its generated equivalence <->* is called a
convertibility relation.
Definition 3.3 A reduction system (A, ) has the Church-Rosser Property
if for all x, y e A, if jc <-* y, there exists az e A, such that
x -* z and y * z.
The Church-Rosser property is depicted in Figure 4.
7


Tigure 4
The conversion relation turns out to mean reducing to the same term: this is called
the Church-Rosser property.
Theorem 3.1 (Church-Rosser Theorem) A relation has the Church-Rosser
property if and only if it is confluent [Church and Rosser,
1936]
If a reduction system satisfies the Church-Rosser, or confluence, property, then
whenever two terms are equivalent, they can be rewritten to a common form. This
guarantees that the "normal forms" (unrewritable terms) computed by a program
are unique.
3.3 Complete Reductions
Now that we have defined both terminating and confluent reduction systems we
are prepared for the following definition:
Definition 3.4 A confluent and terminating reduction system is called
complete.
Consider the reduction system (A, ) given by A = {jc, y, z) and - as depicted in
Figure 5. Then (A, >) is certainly terminating but is not confluent.
8


We are now going to characterize complete reduction systems. Let (A, >) be
an arbitrary reduction system. An element x of A admits a normal form if there is
an irreducible element, say y, in A such that x -* y. In Figure 5, y and z are
normal forms of x.
If (A, ) is a confluent reduction system, each element of A has at most one
normal form. When (A, -) is a terminating reduction system, each element of A
has at least one normal form. Hence, in a complete reduction system every
element has exactly one normal form, often called the canonical normal form.
The Church-Rosser Theorem is the basis of the confluence method explained
below. Let - be a confluent and terminating relation on a set A. Given an
element x of A, any reduction starting from x terminates after finitely many steps
with an element, say x'. By the confluence of x' is uniquely determined. For
if x were reducible to two irreducible elements y and z, then these elements would
be convergent and, hence, equal. So x is always reducible to a unique element x',
the canonical normal form of x
3.4 Local Confluence
Related to the property of confluent reduction systems is the concept of locally
confluent reduction systems.
Definition 3.5 A reduction system (A, ->) is locally confluent if for all
w, x, y e A, w > x and w > y imply that there exists a
z e A, such that x -* z and y -* z.
Local confluence is visualized in Figure 6.
9


Clearly, every confluent reduction system is locally confluent. The converse,
however, is not true, as the following example indicates. The reduction system
depicted in Figure 7 is locally confluent, but not confluent.
Observe that the reduction system is not terminating.
10


3.5 Completion
A completion procedure is aimed at constructing a confluent and terminating
reduction system from a given reduction system. Unfortunately, both properties
are undecidable in general. However, if the reduction itself is terminating, then
there is a necessary and sufficient condition that is quite useful in building a
completion procedure.
Theorem 3.2 (Newmans Lemma) A terminating reduction system is
confluent if and only if it is locally confluent [Newman,
1942].
As a corollary we get an important criterion for completeness.
Corollary A reduction system is complete if and only if it is locally
confluent and terminating.
Given a reduction system (A, >), any equivalent complete reduction system is
called a completion of (A, ->). Our main goal is an algorithmic construction of
such a completion when it is possible.
The idea of a possible algorithmic construction of a completion procedure is
based on Theorem 3.2. Given a terminating reduction system (A, -) we try to
construct a completion (A, =>) by locating all situations in which local confluence
is injured. This suggests the following procedure. Start with the relation - and
compute the set CP() of "critical pairs" of where (x, y) e A x A is called
critical if there is an element z of A such that z -> x and z y, but jc and y are
not convergent. If CP(-) is empty, the reduction relation > is locally confluent
and hence confluent, which means that (A, -) is already complete. In case there
exists at least one critical pair (x, y) we remedy the violation of local confluence
by allowing that either x is reducible to y or, vice versa, y is reducible to x
depending on the analysis where adjoining (x, y) or (y, x) to the reduction relation
leaves the termination property untouched. When both possibilities destroy the
termination property the procedure stops with "failure". After adjoining a critical
pair to - we get a new relation. Again its critical pairs are computed and
eventually added. If the procedure terminates with a relation =>, then there is no
critical pair left. Consequently, (A, =>) is a completion of (A, ->). By
construction, (A, =>) is a complete reduction system. But, it should also be clear
that (A, =>) and (A, -) are equivalent.
11


4. Term Rewriting Systems
Now that the groundwork has been laid, we can apply the general ideas derived
in the framework of reduction systems to term reduction systems. But, first, we
must establish some notational conventions.
4.1 Terms
In this section we are concerned with the syntactic generation which yields the
notion of a term.
A signature is a set 2, whose elements are called operation symbols, together
with a mapping arity: 2 - N, called the arity function, assigning to each
operation symbol its finite arity. If/ e 2 and arityif) = n, / is of arity n, or / is
n-ary. If n > 1,/is a functional symbol, and if n = 0, it is a constant symbol.
Definition 4.1 Let 2 be a signature and V be a set of variables. The set of
(first-order) terms over V is T£(F) and is defined inductively
as:
(1) Ifv e V, then v e T£(F).
(2) If/e 2, and t...,tn e TZ(F) (n > 0), then
e T£(F).
For convenience, we shall always assume that 2 and V are disjoint.
Following convention, we shall agree to use the most readable notation for
terms. This permits us to represent terms on an extended alphabet with parentheses
and commas, which is closer to standard mathematical practice. Therefore, a term
is either a variable symbol, a constant symbol, or a function symbol followed by a
series of terms, separated by commas, and enclosed in parentheses.
The finite set Var(t) of variables occurring in a term t is defined as follows:
(1) Var(v) = {v}, if v e V.
(2) Var= Var(/,) u...u Var(0, if/e 2 and if g T£(F).
We say that a term t is a ground term if Var(t) = 0. That is, a term that is
variable-free is a ground term. The set of all ground terms is denoted by Tz and it
is clear that Tz = Tz(0).
12


4.2 Confluence of Term Rewriting Systems
Equational proofs of equational theorems are not easy to deduce. It is difficult
to find a strategy for selecting and orienting axioms. A simple idea is always to
apply the equalities in the same direction. Such a directed equality is called a
rewrite rule, denoted by replacing the equal sign =, by an arrow Formally, if
an equation is a pair (s, t) of terms s,t e TX(F) denoted by s = t, then s t is its
associated rewrite rule.
Definition 4.2 A term rewriting system (hereafter abbreviated TRS) is a
set of reduction rules.
Rewriting a term with a rewrite system R consists in replacing a subterm which
matches a left-hand side of a rewrite rule by the right-hand side whose variables
are bound to values computed by the matching algorithm. This relation is denoted
by R. Iterating this process is called reducing. If two terms can be reduced to
the same one, a special equational proof is obtained, called a rewrite proof. A
term which cannot be rewritten is said to be in normal form.
A property required for a rewrite system is the uniqueness of the normal form
for any term. This is crucial for any application where computing normal forms
must be independent of the strategy of rule application. Uniqueness of the normal
form is implied by the property of confluence. A rewrite system is confluent when
two rewrite sequences beginning from the same term can always be extended to
end with the same term. Confluence, which has been shown to be an abstract
property of relations, gives us a relation between equational proofs and rewrite
proofs: given a confluent rewrite system, every equational theorem has a rewrite
proof.
Theorem 4.1 A rewriting system is locally confluent if and only if every
critical pair is confluent.
Combining Newmans lemma with the preceding theorem yields the key theorem
from the Knuth-Bendix paper.
Theorem 4.2 A terminating rewriting system is confluent if and only if
every critical pair is confluent.
The importance of Theorem 4.2 is that it shows that to test for local confluence it
is sufficient to consider only the critical pairs. However, computing critical pairs
is an application of unification. Therefore, before expounding further on how
critical pairs are used to show confluence, we must digress into a somewhat
detailed explanation of unification.
13


4.2.1 Unification
In its essence, the unification problem in first-order logic can be expressed as
follows: Given two terms containing some variables, find, if it exists, the simplest
substitution (i.e., an assignment of some term to every variable) that will make the
two terms identical. The nature of such unifying substitutions, as well as the
means of computing them, makes up the study of unification.
4.2.1.1 Syntactic Unification
A substitution is a function a: V - T£(F), which is the identity function almost
everywhere, i.e., except for a finite subset of V. Substitutions can be represented
by a set of variable-term pairs ct = {jc; <- t ..., x < t} with x, tf. A
substitution or in which ct(x) is g(h(a), a) and c(y) is h(a) would be written as:
a = {x A substitution is also a function a: TZ(F) TZ(V); that is, a function that maps
terms to terms. The application of a substitution a to a term t is also written and denotes the term in which each variable x, in t is replaced by afo).
Substitutions can be composed: ct0(/) denotes the term t after the application of
the substitutions of 0 followed by the application of the substitutions of ct. The
substitution ct0 is a new substitution built from old substitutions ct and 0 by (1)
modifying 0 by applying a to its terms, then (2) adding variable-term pairs in ct
not found in 0. Composition of substitutions is associative, that is,
(a0)x(j) = ct(0x)(.s) but is not in general commutative, that is, ct0(^) Q Definition 4.3 Two terms s and t are said to match if there exists a
substitution ct such that a(s) = t.
If a term t can be formed from another term s by making substitutions for the
variables of s, then we say that t is an instance of s or that s subsumes t. This
forms the basis of a relation on terms called the subsumption ordering, written
s < t. The subsumption relation is closely related to the ability to match one term
to another: for only if there exists a substitution ct such that a(s) = t does it imply
that sit. For example,/fx) 3 f(g(c)), since the substitution {x < g(c)} when
applied to f(x) yields f(g(c)).
If, for two terms s and t, s < t and t < s, then s is called a variant of t, written
s ~ t (where ~ is the equivalence relation associated with *). It is easily shown
that if s ~ t, then s and t can differ only by the names of their variables. Therefore
14


the equivalence relation ~ equates terms which are equal up to the renaming of
variables. Thus the subsumption relation is in fact a preorder relation (i.e., it is a
reflexive and transitive binary relation). However, the subsumption relation is not
antisymmetric, so it is not an order relation. Consider, for example, if x and y are
distinct variables, then x < y and y 3 x, but x y. In other words, the subsumption
relation is only antisymmetric up to the renaming of variables.
If neither s < t nor t 1 s, then s and t cannot be matched and are said to be
unrelated.
Let t* represent the set of all instances of a term t. In general, t* is an infinite
set and can be represented diagrammatically as in Figure 8.
The two sets of instances s* and t*, of terms s and t, respectively, may
intersect as represented in Figure 9. Although s and t may themselves be
unrelated, there will often be instances of each that are related. The set of terms
that are instances of both s and t lie in the region s* n t*.
15


The unification of s and t is the process of finding elements of s* r\ t*. If s
and t share variables, then their set of unified forms is, in general, a subset of, and
not identical to, s* n t*. As an example of this, consider the two terms f(x, 2) and
f(3, x): an instance of both is f(3, 2), but this is not a unified form.
Definition 4.4 Two terms s and t are called unifiable if there exists a
substitution c such that o(s) = a(t). In such a case, a is
called a unifier of s and t, and g(s) is called a unification of
s and t.
As an example consider the two terms f(x, yj and f(g(y, a), h(a)). They are
said to be unifiable, since the application of the substitution
a = {x <- g(h(a), a), y 4- h(a)}
will change both terms to f(g(h(a), a), h(a)).
In his famous paper on the resolution principle for a machine-oriented logic,
J.A. Robinson [1965] gave an algorithm to compute a substitution that unifies two
terms. Furthermore, Robinson proved that if the unification of two first-order
terms is possible, there exists a single, most general unified form, unique up to
variable renaming. This most general unified form is the one that subsumes all
other unified forms, and is the term r in Figure 9.
Definition 4.5 A unifier a of terms s and t is called a most general unifier
(MGU) of s and t if for any other unifier 0, there is a
substitution x such that tct = 0.
Consider, for example, the two terms f(x) and f(g(y)). The MGU is
{x 4- g(y)}, but there are many non-MGU unifiers such as {x 4- g(a), y <- a).
Intuitively, the MGU of two terms is the simplest of all their unifiers.
4.2.1.2 Semantic Unification
In the previous section we presented the concepts involved in solving an
equation s = t syntactically; this is a particular case of the problem of solving
equations semantically, i.e. modulo some equational theory E (for this reason
semantic unification is also called ^-unification). More precisely, in the presence
of an equational theory E, and given an equation s = t, we want to find substitution
a such that g(s) =e v(f). Therefore, syntactic unification is ^-unification with
empty E.
16


A substitution ct is a solution in E to an equation s = t if a(X) =E a(t), in
which case we say that ct is an ^-unifier of s and t; we say that t ^'-matches s if
there exists a substitution ct such that ct(j) =e t.
When more than one solution may exist for a theory E, we define a solution ct
of s =Et to be more general than solution p if ct ordering variables x in s and t, but not vice versa. An .E-unifier is most general if no more
general unifier exists. Note that there are decidable theories with infinite sets of
most general unifiers, and there are some for which there are solutions, but no
most general one, as we shall see.
Consider the two first order terms s and t
s =f(x, g(a, b)) t =f(g(y, b), x)
The decision problem for syntactic unification is whether or not there exist terms
which can be substituted for the variables x and y in s and t so that the two terms
thus obtained are identical. In this example g(a, b) and a are two such terms and
we write
8 = {x <- g(a, b), y <- a}
to represent this unifying substitution. We say that 8 is a unifier for s and t, since
m = 8(0 =f(g(a, b), g(a, b)).
Consider a variation of the above problem in the presence of an equational
theory, which arises when we assume that the function /is commutative:
(C) f(x, y) =f(y, x)
Now 8 is still a unifier for s and t. However, ct = {y and t, since
ctCO =f(x, g(a, b)) =c f(g(a, b), x) = ct(0
But ct is more general than 8, or put another way 8 is an instance of ct, since it is
obtained as the composition of the substitutions 0ct where 0 = {x <- g(a, b)}.
Hence a unification algorithm only needs to compute ct.
Unlike syntactic unification, where there is at most one general unifying
substitution, semantic unification can yield a number of most general unifiers.
Under commutativity, for example, there are pairs of terms which have more than
one most general unifier, but they always have at most finitely many.
17


The problem becomes entirely different if we assume that the function / is
associative:
(A) f(x, f(y, z)) =f(f(x, y), z)
In this case 6 is still a unifying substitution, but t = {x f(g(a, b), g(a, b)),
y <- a} is also a unifier, since
=f(f(g(a, b), g(a, b)), g(a, b)) =A f(g(a, b), f(g(a, b), g(a, b))) = x{t)
But t' = {x <- f(g(a, b), f(g(a, b), g(a, b))), y <-_a} is again a unifying substitution
and it is not difficult to see, by an iteration of this process, that there are infinitely
many unifiers, all of which are most general.
Finally, if we assume that both axioms (A) and (C) hold for f, the situation
changes yet again and for any pair of terms there are at most finitely many most
general unifiers under (AC).
4.2.2 Critical Pairs
We have shown that assuming termination, confluence is equivalent to local
confluence, itself equivalent to the convergence of critical pairs. Yet it remains for
us to formally construct the notion of critical pairs.
In order to define critical pairs a few more notions are required. First, by t|p,
we denote the subterm of t rooted at position p. Furthermore, reasoning with
equations requires replacing subterms by other terms. Therefore, let the term t
with its subterm 11 p replaced by a term s be denoted by t[s]p.
Definition 4.6 Let s - s' and t > t' be two reduction rules of a given TRS
R. We assume that the variables are renamed appropriately
so that s and t share no variables. If p is the position of a
nonvariable subterm of s and there exists a substitution a
such that
<*(s|p) = (0
then ct(j') along with a(s|/']p) is called a critical pair in R.
Both components of a critical pair (a(sr), cr(.s|/']p)) are the two outcomes of
reducing a(j) by s - s' and t - t\ respectively.
18


For example, consider the following reduction rules
f(g(x), f(x, z)) z
f(x, f(y, g(f(x, y)))) c
Let us rename the variables of the first reduction rule so that we have
-y =f(g(x), fix', z)) and t =f(x, f(y, g(f(x, y)))). Then,
(1) j|p =f(x', z) is a nonvariable subterm of s; and
(2) j|p and t are unifiable with a mgu a = {*' <- x, z < f(y, g(f(x, y)))}.
Now we obtain
<*(*') = a(z) =f(y, g(f(x, y)))
cj(j[^p) = Thus, f(y, g(f(x, y))) and f(g(x), c) is a critical pair.
The critical pairs can be found by unifying each nonvariable subterm of the
left-hand side of a rewrite rule with the left-hand side of another rule. This
process is called the superposition algorithm.
4.2.2.1 Critical Pairs Completion
We will now explain the essential features of the completion algorithm first by
an informal, intuition-guided, completion of the equational specification of groups.
Consider the group signature consisting of a binary operation Mult, a unary
operation Inv, and a nullary operation e. We start by giving the axioms for groups
a "sensible" orientation:
(1) Mult(e, x) - x
(2) Mult(Inv(x), x) > e
(3) Mult(Mult(x, y), z) Mult(x, Mult(y, z))
Note that the TRS defined by these three reduction rules is terminating but not
confluent. Termination will not be discussed here, but will be studied in the next
section. Confluence is violated, as can be seen by the superposition of rules (2)
19


and (3), with result Mult(Mult(Inv(x), x), z). In a sense, Mult(Mult(Inv(x), x), z) is
the most general term subject to the two possible reductions:
Mult(Mult(Inv(x), x), z) >3 Mult(Inv(x), Mult(x, z))
Mult(Mult(Inv(x), x), z) 2 Mult(e, z)
which yields the critical pair Mult(Inv(x), Mult(x, z)) and Mult(e, z). After
applying the reduction Mult(e, x) - jc we have the problematic pair of terms
Mult(Inv(x), Mult(x, z)) and z; problematic because their equality is derivable from
the group axioms, but they are not convergent with respect to the reduction rules
available so far. Therefore, we adopt the new reduction rule:
(4) Mult(Inv(x), Mult(x, z)) z
Continuing in this manner, we find that the superposition of rules (1) and (4):
Mult(Inv(e), Mult(e, x)) Mult(Inv(e), x)
Mult(Inv(e), Mult(e, x)) >4 x
yields the critical pair Mult(Inv(e), x) and x. Therefore, adopt the reduction rule:
(5) Mult(Inv(e), x) > x
Superposition of rules (2) and (4):
Mult(Inv(Inv(x)), Mult(Inv(x), x)) -2 Mult(Inv(Inv(x)), e)
Mult(Inv(Inv(x)), Mult(Inv(x), x)) ->4 x
yields the critical pair Mult(Inv(Inv(x)), e) and x. Therefore, adopt the new
reduction rule:
(6) Mult(Inv(Inv(x)), e) - x
Superposition of rules (3) and (6):
Mult(Mult(Inv(Inv(x)), e), y) >3 Mult(Inv(Inv(x)), Mult(e, y))
Mult(Mult(Inv(Inv(x)), e), y) 6 Mult(x, y)
yields the critical pair Mult(Inv(Inv(x)), Mult(e, y)) and Mult(x, y). Therefore, after
normalizing adopt the new reduction rule:
(7) Mult(Inv(Inv(x)), y) -> Mult(x, y)
20


Superposition of rules (6) and (7):
Mult(Inv(Inv(x)), e) 7 Mult(x, e)
Mult(Inv(Inv(x)), e) 6 x
yields the critical pair Mult(x, e) and x. Therefore, adopt the new reduction rule:
(8) Mult(x, e) x
Superposition of rules (6) and (8):
Mult(Inv(Inv(x)), e) g Inv(Inv(x))
Mult(Inv(Inv(x)), e) ->6 jc
yields the critical pair Inv(Inv(x)) and x. Therefore, adopt the new reduction rule:
(9) Inv(Inv(x)) - x
Notice that reduction rule (6) can be deleted due to rules (8) and (9) because:
Mult(Inv(Inv(x)), e) ->6 x
Mult(Inv(Inv(x)), e) -9 Mult(x, e) 8 x
are convergent. Likewise reduction rule (7) can be deleted due to rule (9) because:
Mult(Inv(Inv(x)), y) -7 Mult(x, y)
Mult(Inv(Inv(x)), y) ->9 Mult(x, y)
are convergent. Superposition of rules (5) and (8):
Mult(Inv(e), e) -8 Inv(e)
Mult(Inv(e), e) -5 e
yields the critical pair Inv(e) and e. Therefore, adopt the new reduction rule:
(10) Inv(e) e
Notice that reduction rule (5) can be deleted due to rules (1) and (10) because:
Mult(Inv(e), x) -5 x
Mult(Inv(e), x) 10 Mult(e, x) x
21


are convergent. Superposition Rules (2) and (9):
Mult(Inv(Inv(x)), Inv(x)) 9 Mult(x, Inv(x))
Mult(Inv(Inv(x)), Inv(x)) -2 e
yields the critical pair Mult(x, Inv(x)) and e. Therefore, adopt the new reduction
rule:
(11) Mult(x, Inv(x)) e
Superposition Rules (4) and (9):
Mult(Inv(Inv(x)), Mult(Inv(x), z)) 9 Mult(x, Mult(Inv(x), z))
Mult(Inv(Inv(x)), Mult(Im(x), z)) >4 z
yields the critical pair Mult(x, Mult(Inv(x), z)) and z. Therefore, adopt the new
reduction rule:
(12) Mult(x, Mult(Inv(x), z)) -> z
Superposition Rules (3) and (11):
Mult(Mult(x, y), Inv(Mult(x, y))) -3 Mult(x, Mult(y, Inv(Mult(x, y))))
Mult(Mult(x, y), Inv(Mult(x, y))) e
yields the critical pair Mult(x, Mult(y, Inv(Mult(x, y)))) and e. Therefore, adopt the
new reduction rule:
(13) Mult(x, Mult(y, Inv(Mult(x, y)))) > e
Superposition Rules (12) and (13):
Mult(Inv(x), Mult(x, Mult(y, Inv(Mult(x, y))))) ->12 Mult(y, lnv(Mult(x, y)))
Mult(Inv(x), Mult(x, Mult(y, Inv(Mult(x, y))))) 13 Mult(Inv(x), e)
yields the critical pair Mult(y, Inv(Mult(x, y))) and Mult(Inv(x), e). Therefore, after
normalizing adopt the new reduction rule:
(14) Mult(y, Inv(Mult(x, y))) > Inv(x)
Notice that reduction rule (13) can be deleted due to rules (11) and (14) because:
22


Mult(x, Mult(y, Inv(Mult(x, y)))) >13 e
Mult(x, Mult(y, Inv(Mult(x, y)))) 14 Mult(x, Inv(x)) ->n e
are convergent. Superposition Rules (4) and (14):
Mult(Inv(y), Mult(y, Inv(Mult(x, y)))) 4 Inv(Mult(x, y))
Mult(Inv(y), Mult(y, Inv(Mult(x, y)))) ->14 Mult(Inv(y), Inv(x))
yields the critical pair Im(Mult(x, y)) and Mult(Inv(y), Inv(x)). Therefore, adopt
the new reduction rule:
(15) Inv(Mult(x, y)) Mult(Inv(y), Inv(x))
Notice that reduction rule (14) can be deleted due to rules (12) and (15) because:
Mult(y, Inv(Mult(x, y))) -14 Inv(x) and
Multfy, Inv(Mult(x, y))) ->I5 Multfy, Mult(Inv(y), Inv(x))) 12 Inv(x)
are convergent. The TRS is now complete, and is composed of the following
rewrite rules:
(1) Mult(e, x) - x
(2) Mult(Inv(x), x) -* e
(3) Mult(Mult(x, y), z) - Mult(x, Multfy, z))
(4) Multflnvfx), Multfx, z)) -> z
(5) Multfx, e) -> x
(6) Invflnvfx)) > x
(7) Invfe) -> e
(8) Multfx, Invfx)) e
(9) Multfx, Multflnvfx), z)) -> z
(10) InvfMultfx, y)) > Multflnvfy), Invfx))
23


4.2.3 Knuth-Bendix Algorithm
A completion procedure is aimed at building a confluent and terminating
rewrite system from a set of equalities. In what follows we shall explain a
completion procedure based on Theorem 4.2 called the Knuth-Bendix Completion
Procedure. The Knuth-Bendix procedure can be outlined roughly as follows:
Input: An equational specification (E, E) and a reduction ordering > on
TZ(F) (i.e., a program which computes >).
Output: A complete TRS R.
Method: A sequence (U J n e N) of finite TRSs is computed iteratively, if
possible, as follows:
R := 0;
while (E t* 0)
{
Select an equation (s = t) e E;
E := E {s = t};
Reduce s and t to respective normal forms s' and t1 with respect to R;
if (s' t')
{
if (s' > t')
a := s'; p = t';
else if (t1 > s')
a := t'; P = s';
else
failure
CP := {P = Q | is a critical pair between the rules in R
and a -> P};
R := R u {a - P);
E := E u CP;
}
}
success___________________________________________________________________________
Cnuth-Bendix Completion Procedure
24


This procedure may have several possible outcomes:
(1) It terminates successfully, in which case we will have a complete TRS.
(2) It terminates unsuccessfully, i.e., aborts, and does not find a complete
TRS. In other words, the procedure found a critical pair whose two
terms are not comparable (under the current termination ordering). This
may be due to an inadequate choice of termination ordering, and by
changing the ordering the terms may become comparable. However,
there are also cases where the terms are intrinsically incomparable.
(3) It loops forever, generating more and more critical pairs.
In the case where a finite confluent set of rules can be generated, the
importance to equational reasoning is clear. A decision procedure is found for
solving the identity problem. A two-part strategy for proving theorems is possible.
(1) The given axioms are compiled into a confluent set of rewrite rules
using the Knuth-Bendix completion procedure. If this succeeds, then:
(2) Equations are shown to be theorems by reducing both sides to normal
form. If the normal forms are the same, the theorem is shown to be a
consequence of the given axioms; if different, the theorem is proven
false.
The complete set of rules derived in the previous section can be used to prove,
for instance, that:
Inv(Mult(Mult(Inv(y), y), Mult(x, Inv(x)))) = Mult(x, Mult(Inv(Mult(y, x)), y))
The rewrite rules are used to find the normal forms of both terms:
Inv(Mult(Mult(Inv(y), y), Mult(x, Inv(x)))) -10 Mult(Inv(Mult(x, Inv(x))),
Inv(Mult(Inv(y), y))) 8 Mult(Inv(e), Inv(Mult(Inv(y), y))) 2
Mult(Inv(e), Inv(e)) -7 Mult(e, Inv(e)) 8 e.
Mult(x, Mult(Inv(Mult(y, x)), y)) 10 Mult(x, Mult(Mult(Inv(x), Inv(y)), y)) >3
Mult(x, Mult(Inv(x), Mult(lnv(y), y))) -9 Mult(Inv(y), y) 2 e.
Since the normal forms are the same, the theorem has been shown to be a
consequence of the given axioms. Note that, due to confluence, the same normal
forms are found regardless of the order of rule application.
25


4.3 Termination of Term Rewriting Systems
Termination is a fundamental property of term rewriting systems. Specifically,
the successful use of the Knuth-Bendix procedure depends upon our ability to
prove the termination of the term rewriting systems that are generated during the
process of completion. In general, as already noted, termination is an undecidable
property. Therefore various termination proof methods have been developed to
show that special systems terminate. In this section, we only briefly sketch the
problem and its solution; a good and complete survey can be found in Dershowitz
[1987].
The Knuth-Bendix procedure computes a sequence (Rn | n e N) of finite sets of
reduction rules so that the following conditions are satisfied:
(1) Rn is terminating and equivalent to R; and
(2) Any critical pair in R is convergent in Rn+I.
Preserving termination is the crucial point in that construction. A critical pair in R
becomes convergent in Rn+1 only if the corresponding reduction rules preserve
termination.
Various methods exist for proving the termination of TRS. Most of these are
based on reduction orderings which are well founded, compatible with the structure
of terms and stable with respect to substitutions. The notion of reduction orderings
leads to the following description of termination of rewriting systems: A TRS R
terminates if, and only if, there exists a reduction ordering > such that s > t for
each rule s - / of R. That is, for each pair of terms s and t, it is decidable
whether s > t holds or not. But there is an obstacle to be mentioned. When a
critical pair arises during the completion process such that its two components are
incomparable with respect to >, the Knuth-Bendix procedure aborts with an error
message, which indicates that > fails to prove termination.
A rewrite system is said to be terminating if the relation -R is well founded.
Termination is in general undecidable and sufficient conditions for ensuring it have
been developed. Classical methods are based on orderings on the term algebra.
The key idea is to show that a specific well-founded partial ordering contains the
intended rewrite relation. If such an ordering exists, clearly the rewrite relation
terminates. However, instead of proving the inclusion on the whole rewriting
relation, one usually localizes the proof, by proving that only the well-founded
relation contains the rewrite rules. By means of some stability properties, this is
extended to a termination proof of the whole rewriting relation. Basically, a "good
candidate" has to satisfy two properties: stability by substitution of terms to
variables (also called full invariance) and stability by the operations of the term
algebra (also called replacement property).
26


Such a well-founded ordering is called a reduction ordering. Simplification
orderings form an important family of reduction orderings. They are such that
any subterm of a term is smaller than the whole term. This property and stability
by substitutions and operators are enough for ensuring the well-foundedness of the
ordering.
There are essentially two types of reduction orderings on terms for proving
termination. The first one, called syntactical, provides the ordering via a careful
analysis of the structure of the terms. Among these orderings are the recursive
path ordering, the lexicographic path ordering, and the recursive decomposition
ordering. These orderings are convenient since they are based on a concept of
precedence which is somewhat natural, especially in the context of abstract data
types. In addition they enjoy a property called incrementality that enables one to
build the proof of termination step by step, in the case of an incremental set of
rewrite rules. Another family contains the semantical orderings, that interpret the
terms in another structure where a well-founded ordering is known. For such a
purpose, two common, well-ordered sets are the natural numbers and the terms
ordered by a syntactical ordering. The first choice enables one to consider
functions over natural numbers which are stable by substitutions. The most
frequently used are polynomials. If the set of terms ordered by a syntactical
ordering is chosen as a target for the "semantics," one transforms the rewrite
system into another one. The Knuth-Beridix ordering presented with the
completion procedure in the original paper combines a semantical ordering
(polynomial interpretation of degree 1) and a syntactical ordering.
27


4.3.1 Knuth-Bendix Ordering
In their pioneering paper [Knuth and Bendix, 1970], Knuth and Bendix first
presented a simple but powerful term ordering. In this ordering, non-negative
integer weights are assigned to each function symbol, and then to each term by
adding up the weights of the function symbols it contains. Two terms are
compared by comparing their weights and, if the weights are the same, by
comparing their subterms in the same way. What follows, is a precise definition of
what has come to be known as the Knuth-Bendix ordering.
Let 2 be an arbitrary signature with at least one nullary operation symbol. We
assume that 2 is equipped with a total order > and an associated weight function,
w: 2 N, assigning a non-negative integer, or weight, w(/), to each operator
/ e 2, satisfying the following two conditions:
(a) The weight of every nullary operation symbol is positive. That is, if
arity(/) = 0 then w(f) > 0.
(b) If the weight of a unary operation symbol /is zero, then/is the greatest
element in 2. That is, if arity(/) = 1 and w(f) = 0 then / > g for all
operators g. In other words, every unary operation symbol has positive
weight, with the possible exception of the greatest element provided it is
unary.
The weight function can be extended to a mapping w from TZ(F) to N by the rules:
w(v) = min (w(c) | c e 20) for all variables v e V; and
w(f(t...,tj) = w(/) + w (t}) + ... + w (t)
for every n-ary operation/of 2 and all terms tt in TZ(F). Thus, the weight of
any variable is the smallest weight of any constant and the weight of a term is just
the sum of the weights of all the symbols appearing in it.
Before giving a formal definition of the Knuth-Bendix ordering one further
notation convention is required: let us write n(a, t) for the number of occurrences
of the symbol a in term t.
Definition 4.7 Let 2 be a signature. If > is a total order on 2 and
w: TZ(F) - N is a weight function, then the induced Knuth-
Bendix order ^ on TZ(F) is defined as follows. For any
two terms s and t, s >KB t if and only if either
28


(1) w(j) > w(/) and n(v, s) > n(v, t) for all variables v e V; or
(2) w(s) = w(0 and n(v, s) = n(v, t) for all variables v e V and either
(2a) s -f"(v) and t = v for some n > 1; or
(2b) j =f(s...,sj and t = g(tl,...,tj and either
(i) / g; or
(ii) /= g and s, = th sk_, = tM and sk >KB tk for some k with
1 < k < n, and n = m.
As an example, consider the group signature with precedence Inv > Mult > e
and weights: w(e) = 1, w(Inv) = 0, and w(Mult) = 1. Then, for instance,
Mult(Mult(x, y), z) >KB Multfx, Mult(y, z))
by condition (2b) subcase (ii) since Mult(x, y) >KB x; or
Inv(Mult(x, y)) >KB Mult(Inv(y), Inv(x))
by condition (2b) subcase (i) because Inv t Mult; or
Inv(Inv(x)) >KB x
by condition (2a).
The Knuth-Bendix ordering is very flexible; the choice of weights means that
there may be infinitely many Knuth-Bendix orderings on a given set of terms.
However, there are two significant problems with this ordering. First, the number
of occurrences of a variable must not increase when passing from a larger to a
smaller term. Thus, no Knuth-Bendix ordering can order the distributive law:
f(x, g(y, z)) = g(f(x, y), f(x, z))
since x occurs twice on the right and once on the left. The second problem is that
it is very difficult to know what weights to choose! If the Knuth-Bendix ordering
fails to order our rules with one choice of weights we can try another, but without
some help we may fail again and indeed it may be that no Knuth-Bendix ordering
can order them.
29


5. Abstract Completion
There are many completion algorithms such as the Knuth-Bendix procedure,
differing in order of execution or ways of optimization. The question is, how to
prove that these algorithms are correct, i.e. deliver upon successful termination a
TRS R with the same equality as the one generated by the original set of equations
E. As there is a whole family of completion algorithms, one needs to extract the
abstract principles of such algorithms; and this has been done [Bachmair et al.,
1987].
Specifically, completion has been reformulated as an equational inference
system in which new equations and new rewrite rules are derived, while old ones
are simplified and/or deleted. The application of completion to a set of equations
is viewed as a process of proof simplification, the goal of which is the derivation
of rewrite proofs.
What distinguishes completion from ordinary logical inference is the
incorporation of rules for removing redundant items from the set of inferred
equations. In this context, an inference rule is a binary relation between pairs
(E; R), where E is a set of (unordered) equations and R is a set of (orientated)
rewrite rules. A rule that adds a consequence to a set is called an expansion rule;
one that deletes a redundancy is called a contraction rule. The method for proving
correctness of completion algorithms starts with the introduction of a derivation
system where the objects are pairs (E; R); each derivation step from (E; R) to
(E'; R') preserves equality (i.e., =EuR coincides with =EuR.).
Let > be a reduction ordering on terms. The inference system known as
standard completion contains six rules operating on (E; R) as follows:
The first inference rule is used to expand the set of equations with critical pairs
obtained by rewriting an instance of a left-hand side of a rule in two different
ways:
E ; R
Deduction: ------------- if (s = t) e CP(R)
Eu{s = t};R
Equations may be eliminated from nonnormal proofs by turning them into one-
way rewrite rules. Equations are oriented according to the given reduction order >
to ensure that rewrite systems derived by completion are terminating:
Eu{s = t};R
Orientation: ------------- if s >-1
E;Ru {s - t}
A simple contraction rule deletes trivial equations:
30


Eu{s = s};R
Deletion: --------------
E ; R
Another contraction rule, uses rules to simplify deduced equations:
Eu{s = t};R
Simplification: -------------- if t -R u
Eu{s = u};R
This inference is also a combination of expansion (adding s = u), followed by
contraction (removal of the now redundant s = t).
For efficiency reasons, implementations of completion procedures usually
include further simplification mechanisms which can be described by the following
two inference rules:
E;Ru {s -> t}
Composition: -------------- if t -R u
E ; R u {s - u}
E ; R u {s - t}
Collapse: -------------- if s R u by 1 - r
Eu{u = t};R with s - t > 1 r
The symbol > denotes the encompassment ordering; s > v if some subterm of 5
is an instance of v, but not vice versa. Composition allows simplification of right-
hand sides of rewrite rules; collapsing simplifies left-hand sides. Although
composition produces another rewrite rule, the equation obtained by collapsing a
rule need not necessarily be orientable.
Definition 5.1 A standard completion procedure is any program that takes
a finite set E0 of equations and reduction ordering >, and uses
the above rules to generate a sequence of inferences from
(Eo, 0).
When success occurs after a finite number of steps, the resultant system R* is a
decision procedure for E0. But completion may "loop", producing an infinitely
large set of persisting rules. A simple example [Ardis, 1980] of looping is
provided by the equation f(g(f(x))) = g(f(x)). Oriented the only way possible, the
rule f(g(f(x))) -> g(f(x)) overlaps itself, generating the critical pair g(f(g(f(x)))) =
f(g(g(f(x)))), which simplifies to g(g(f(x))) = f(g(g(f(x)))). Continuing in the same
manner, an infinite set of rules {f(g!(f(x))) -> g!(f(x)) | i > 1} is produced.
31


The following version of completion [Dershowitz, 1982] takes as input a set of
equations E0 and a well-founded ordering >-. It generates all new critical pairs at
once; more practical versions (notably the one in [Huet, 1981]) do this
incrementally.
Let E be E0 and R be the empty set. Then repeat the following six steps as
long as equations are left in E; if none remain, terminate successfully:
(1) Remove an equation from E such that s > t. If none exists, terminate
with failure.
(2) Add the rule s - t to R.
(3) Use R to reduce the right-hand sides of existing rules.
(4) Add to E all critical pairs formed using the new rule.
(5) (Optional) Remove all old rules from R whose left-hand side contains
an instance of s.
(6) Use R to reduce both sides of equations in E to normal forms. Remove
any equation whose reduced sides are identical
This procedure is an example of standard completion. Step (2) represents an
application of orientation; step (3), repeated application of composition; step (4),
repeated deduction; step (6), repeated simplification and deletion. Step (4), in
combination with step (5), implicitly uses collapse, for whenever a rule s - t can
be collapsed to u = t, then u = t is a critical pair in CP(i?). In the above
procedure, the equation u = t is first deduced in step (4), but may be deleted in
step (5). Fairness of the procedure, that is, fairness of all its derivations, depends
on the order in which, in step (1), equations are removed from E.
32


6. Implementation of a TRS
The following is a brief account of the significant decisions that were made in
implementing a term rewriting system. A complete account of the resulting term
rewriting system is presented in Appendix A.
6.1 Data Structures
A completion procedure operates exclusively on equations and rewrite rules
which are both composed of a pair of terms. Therefore, to implement a
completion procedure the most important decision to be made is the choice of the
internal representation of a term. This decision affects not only the complexity of
all of the routines operating on terms, but also has a fundamental effect on
performance.
The obvious representational candidates for a term include any data structure
that supports the notion of a rooted tree with a variable number of sub-trees.
Typically, completion procedures select one of the standard tree representations
based on tree nodes containing pointers to other nodes. Such a representation has
the advantage of making term substitutions as simple as a single pointer affectation.
However, with this representation the cost of almost every other operation
performed on a term (constructing, copying, deleting, traversing, etc.) is quite
significant.
In my completion procedure, I selected a representation for terms that is to my
knowledge the single most efficient and effective that one could choose. The
structure is a simple array of pointer/weight pairs. Each pointer is to a shared copy
of either a function, constant, or variable descriptor, while each weight represents
the total number of subterms for that term (including itself). The subterms are
ordered in the array in a pre-order fashion. This weighted pre-order representation
has the following advantages:
(1) Traversing a tree in pre-order amounts to sequentially walking the term
array. Since pre-order traversals account for a significant portion of the
time spent processing terms the manner in which terms are traversed is
important. The array of terms representation is ideally suited to this
operation, being trivial to implement, as fast as possible, and recursion
free.
(2) Traversing a tree in level-order amounts to adding to the pointer of the
given term its own weight. Therefore, to traverse from one term to its
next sequential sibling is a trivial operation.
33


(3) Copying a term is trivial; allocate a single memory new memory block
and copy the contents of the source term into it.
(4) Deleting a term is trivial; free the terms single memory block.
(5) Performing a lexical comparisons of two terms is trivial; perform a
comparison of the two memory blocks.
(6) Memory consumption is held to a minimum.
The only disadvantage to this representation is that performing a term substitution
is more costly than changing a single pointer. But in light of all of the obvious
benefits to this representation this single disadvantage is worth bearing.
6.2 Unification
Any attempt to write a term rewriting system must, at some point, come to
terms with the issue of unification. The decision concerning which unification
algorithm to select should not be taken lightly; the computing of critical pairs,
which has been shown to be an application of unification, is the very heart of any
completion procedure.
There are a number of well documented algorithms that handle first-order
unification. Robinsons [1965] original algorithm was inefficient, requiring
exponential time and space. Since then, a great deal of effort has gone into
improving the efficiency of unification. Boyer and Moore [1972], for example,
gave a unification algorithm that shares structure; it was efficient in its use of
space but was still exponential in time complexity. Venturini-Zilli [1975]
introduced a marking scheme that reduced the complexity of Robinsons algorithm
to quadratic time. Huets [1976] work led to an improved time bound. His
algorithm is based on maintaining equivalence classes of subterms and is an almost
linear algorithm. Paterson and Wegman [1978] gave a truly linear algorithm for
unification, but is, reportedly, very complex to implement. Martelli and Montanari
[1982], gave a thorough description of an efficient unification algorithm. This
algorithm, although it is not truly linear, is probably the most widely used in
practice. It too is based on equivalence classes and is in practice quite efficient.
For my implementation, I chose to implement the algorithm presented in
Escalada-Imaz and Ghallab [1988], I chose this algorithm because it is an efficient
unification algorithm for first-order terms. It relies on the known theoretical
framework of homogeneous and valid equivalence relations on terms and it makes
use of a union-find algorithmic schema, thus keeping an almost linear worst-case
complexity. Its advantages over similar algorithms are a very low overhead and
34


practical efficiency, even for small terms, that are due to simple data structures and
careful design tradeoffs.
6.3 Completion Procedure
My first attempt at writing a completion procedure began with a basic
implementation of the Knuth-Bendix completion procedure. However, it soon
became apparent that, for efficiency reasons, the implementation should include all
of the simplification mechanisms found in abstract completion procedures.
Specifically, the inference rules of Composition and Collapse were needed to keep
the resulting set of rewrite rules in a minimal, non-redundant state. Adding these
inference rules to the basic Knuth-Bendix procedure was quite easy and resulted in
a huge increase in performance. Furthermore, tracking and debugging the TRS
was made significantly easier.
As far as choosing a reduction ordering to use, I selected to implement the
Knuth-Bendix ordering. As has been noted, the Knuth-Bendix ordering is very
flexible and easily implemented. The drawbacks concerning its inability to deal
with certain types of axioms were considered unfortunate. However, it was not at
all clear from the literature that choosing any other reduction ordering would have
significantly increasing the range of axioms the system could effectively deal with.
The particular method an algorithm uses in regard to selecting the next axiom
to be consider is called its selection strategy. For Knuth-Bendix completion to
work correctly, its selection strategy must satisfy the following fairness constraint:
every axiom must eventually be considered as a rule (i.e., no axiom can be ignored
indefinitely). In the given implementation the strategy used to select an axiom is
by size; the shortest axiom in the current axiom set is selected first. This strategy
is fair and nearly always leads to convergence in fewer iterations than selection on
a first-come first-served basis.
6.4 Samples
The following samples illustrate the input and output obtained by executing the
term rewriting system constructed for this thesis. Input to the program is denoted
by a > in column one. It should be noted that the language used to construct a
signature contains sorts. The intent was to be able to extend the system at a later
time to include order-sorted unification and perform order-sorted completion.
35


The first example shows the completion process in action on the, now familiar,
group signature:
> declare sorts
> group;
>
> declare constants
> e : group;
>
> declare variables
> x, y, z : group;
>
> declare functions
> Inverse : group -> group,
> Mult : group, group group;
>
> declare equations
> Mult(Mult(x, y), z) = Mult(x, Mult(y, z)),
> Mult(Inverse(x), x) = e, // left inverse
> Mult(e, x) = x; // left identity
>
> KnuthBendix e(l) Mult(O) Inverse(O);
We noted earlier that a completion procedure using the Knuth-Bendix ordering
requires a total order and an associated weight function. In my implementation
these pieces of information are supplied, to the procedure via the syntax displayed
on the last line of the preceding figure. The weights are specified in parentheses.
36


The completion procedure attempts to construct a confluent and terminating rewrite
system from the given set of axioms. The following is a depiction of the process
as new rules are added to the set of rewrite rules. Note that some of the rules in R
are collapsed, which causes both their removal from R and their addition to E for
further consideration.
Add rule: Mult(e, x) -> x
Add rule: Mult(Inverse(x), x) - e
Add rule: Mult(Mult(x, y), z) Mult(x, Mult(y, z))
Add rule: Mult(Inverse(x), Mult(x, z)) - z
Add rule: Mult(Inverse(e), x) -> x
Add rule: Mult(Inverse(Inverse(e)), x) x
Collapse: Mult(Inverse(Inverse(e)), x) - x
To: Mult(e, x) = x
Collapse: Mult(Inverse(e), x) - x
To: Mult(e, x) = x
Add rule: Inverse(e) -> e
Add rule: Mult(Inverse(Inverse(x)), e) - x
Add rule: Mult(Inverse(Inverse(Inverse(x))), x) -> e
Collapse: Mult(Inverse(Inverse(Inverse(x))), x) -> e
To: Mult(Inverse(x), x) = e
Collapse: Mult(Inverse(Inverse(x)), e) - x
To: Mult(x, e) = x
Add rule: Inverse(Inverse(x)) -> x
Add rule: Mult(x, e) - x
Add rule: Mult(x, Inverse(x)) e
Add rule: Mult(x, Mult(Inverse(x), z)) -> z
Add rule: Mult(x, Mult(y, Inverse(Mult(x, y)))) - e
Collapse: Mult(x, Mult(y, Inverse(Mult(x, y)))) e
To: Mult(x, Inverse(x)) = e
Add rule: Mult(y, Inverse(Mult(x, y))) -> Inverse(x)
Collapse: Mult(y, Inverse(Mult(x, y))) -> Inverse(x)
To: Mult(y, Mult(Inverse(y), Inverse(x))) = Inverse(x)
Add rule: Inverse(Mult(x, y)) -> Mult(Inverse(y), Inverse(x))
37


Upon successful completion, the final set of rewrite rules is displayed:
(1) Inverse(Mult(x, y)) - Mult(Inverse(y), Inverse(x))
(2) Mult(x, Mult(Inverse(x), z)) - z
(3) Mult(x, Inverse(x)) -> e
(4) Mult(x, e) - x
(5) Inverse(Inverse(x)) -> x
(6) Inverse(e) - e
(7) Mult(Inverse(x), Mult(x, z)) z
(8) Mult(Mult(x, y), z) Mult(x, Mult(y, z))
(9) Mult(Inverse(x), x) -> e
(10) Mult(e, x) -> x
Using the resulting rewrite system we can than prove the following two theorems:
> Prove Mult(Mult(Inverse(x), x), Mult(e, x)) =
Mult(Mult(Inverse(x), Mult(e, x)), x)
1st term normalized: x
2nd term normalized: x
>
>
> Prove Inverse(Mult(Mult(Inverse(y), y), Mult(x, Inverse(x)))) =
> Mult(x, Mult(Inverse(Mult(y, x)), y))
1st term normalized: e
2nd term normalized: e
Note that the process of proving theorems via a TRS amounts to reducing the two
sides of the given equation to normal form and checking for equality. In the given
implementation, the checking for equality is left to the user. A more rigorous
approach would completely automate this last step. This could be accomplished by
matching the normalized terms and verifying that only trivial substitutions (i.e., a
variable is mapped only to another variable) result.
38


It is interesting to ask what happens if we modify the axioms of group theory
slightly, postulating a left identity element and a right inverse. This leads to an
algebraic system which apparently was first discussed by A.H. Clifford. H.B.
Mann independently discussed this question, and called the systems "(1, r) systems".
They are also called "left groups".
> declare sorts
> group;
> declare constants
> e : group;
>
> declare variables
> x, y, z : group;
>
>
> declare functions
> Inverse : group - group,
> Mult : group, group -> group;
>
> declare equations
> Mult(Mult(x, y), z) = Mult(x, Mult(y, z)),
> Mult(x, Inverse(x)) = e,
> Mult(e, x) = x;
// right inverse
// left identity
>
> KnuthBendix e(l) Mult(O) Inverse(O)
39


The process of computing a complete TRS for the (l, r) systems signature follows:
Add rule: Mult(e, x) -> x
Add rule: Mult(x, Inverse(x)) - e
Add rule: Inverse(e) e
Add rule: Mult(Mult(x, y), z) -> Mult(x, Mult(y, z))
Add rule: Mult(x, Mult(Inverse(x), z)) -> z
Add rule: Mult(x, e) - Inverse(Inverse(x))
Add rule: Mult(x, Inverse(Inverse(Inverse(x)))) > e
Add rule: Inverse(Inverse(Inverse(Inverse(x)))) Inverse(Inverse(x))
Add rule: Mult(Inverse(Inverse(x)), z) - Mult(x, z)
Add rule: Mult(Inverse(x), Mult(x, z)) z
Collapse: Inverse(Inverse(Inverse(Inverse(x)))) - Inverse(Inverse(x))
To: Inverse(Inverse(x)) = Inverse(Inverse(x))
Collapse: Mult(x, Inverse(Inverse(Inverse(x)))) -> e
To: Mult(x, Inverse(x)) = e
Add rule: Inverse(Inverse(Inverse(x))) - Inverse(x)
Add rule: Mult(x, Mult(y, Inverse(Mult(x, y)))) -> e
Add rule: Inverse(Mult(Inverse(y), y)) -> e
Add rule: Mult(y, Inverse(Mult(Inverse(x), y))) Inverse(Inverse(x))
Collapse: Mult(y, Inverse(Mult(Inverse(x), y))) -> Inverse(Inverse(x))
To: Inverse(Inverse(x)) = Inverse(Inverse(x))
Collapse: Mult(x, Mult(y, Inverse(Mult(x, y)))) > e
To: Mult(x, Inverse(x)) = e
Add rule: Mult(z, Inverse(Mult(x, z))) - Inverse(x)
Collapse: Mult(z, Inverse(Mult(x, z))) -> Inverse(x)
To: Mult(z, Mult(Inverse(z), Inverse(x))) = Inverse(x)
Collapse: Inverse(Mult(Inverse(y), y)) -> e
To: Mult(Inverse(y), Inverse(Inverse(y))) = e
Add rule: Inverse(Mult(x, z)) Mult(Inverse(z), Inverse(x))
40


Upon successful completion, the final set of rewrite rules is again displayed. It is
interesting to note the differences in the rules generated between this example and
the previous example.
(1) Inverse(Mult(x, z)) - Mult(Inverse(z), Inverse(x))
(2) Inverse(Inverse(Inverse(x))) - Inverse(x)
(3) Mult(Inverse(x), Mult(x, z)) -> z
(4) Mult(Inverse(Inverse(x)), z) - Mult(x, z)
(5) Mult(x, e) Inverse(Inverse(x))
(6) Mult(x, Mult(Inverse(x), z)) -> z
(7) Mult(Mult(x, y), z) - Mult(x, Mult(y, z))
(8) Inverse(e) -> e
(9) Mult(x, Inverse(x)) -> e
(10) Mult(e, x) x
Using this rewrite system we can prove the following theorems:
> Prove Mult (Mult(Inverse(Inverse(x)), Mult(x, Mult(Inverse(x), y))), z) =
> Mult(Mult(x, y), Mult(e, Mult(Inverse(x), Mult(x, z))))
1st term normalized: Mult(x, Mult(y, z))
2nd term normalized: Mult(x, Mult(y, z))
>
>
> Prove Mult(y, Mult(Mult(x, Inverse(x)), Inverse(Inverse(Inverse(x))))) =
> Mult(y, Mult(Inverse(Inverse(e)), Inverse(Mult(e, x))))
1st term normalized: Mult(y, Inverse(x))
2nd term normalized: Mult(y, Inverse(x))
>
>
> Prove Mult(Mult(z, Mult(Inverse(z), x)), Mult(Inverse(e), y)) =
> Mult(Inverse(Inverse(Mult(e, x))), Mult(Inverse(x), Mult(x, y)))
1st term normalized: Mult(x, y)
2nd term normalized: Mult(x, y)
It should be apparent that if the normalized forms are not equivalent then the
equation is not a theorem of the given algebraic system.
41


If we introduce two left identity elements and two corresponding right inverse
operators, we have the following five axioms:
> declare sorts
> group;
>
> declare constants
> e, f: group;
>
> declare variables
> x, y, z : group;
>
> declare functions
> Inverse, Inverse2 : group -> group,
> Mult : group, group - group;
>
> declare equations
> Mult(Mult(x, y), z) = Mult(x, Mult(y, z)),
> Mult(x, Inverse(x)) = e, // right inverse
> Mult(e, x) = x, // left identity
> Mult(f, x) = x, // left identify (2nd)
> Mult(x, Inverse2(x)) = f; // right inverse (2nd)
>
> KnuthBendix e(l) f(l) Mult(O) Inverse(O) Inverse2(0);
The process of computing a complete TRS for this signature is a lengthy
proposition:
Add rule: Mult(f, x) - x
Add rule: Mult(e, x) x
Add rule: Mult(x, Inverse2(x)) - f
Add rule: Inverse2(f) -> f
Add rule: Inverse2(e) > f
Add rule: Mult(x, Inverse(x)) -> e
Add rule: Inverse(f) -> e
Add rule: Inverse(e) -> e
Add rule: Mult(Mult(x, y), z) > Mult(x, Mult(y, z)) continued
42


Add rule: Mult(x, Mult(Inverse2(x), z)) z
Add rule: Mult(x, f) - Inverse2(Inverse2(x))
Add rule: Mult(x, e) - Inverse(Inverse2(x))
Add rule: Mult(x, Inverse(Inverse2(Inverse2(x)))) - e
Add rule: Mult(x, Inverse2(Inverse2(Inverse2(x)))) -> f
Add rule: Inverse2(Inverse2(Inverse2(Inverse2(x)))) - Inverse2(Inverse2(x))
Add rule: Inverse(Inverse2(Inverse2(Inverse2(x)))) > Inverse(Inverse2(x))
Add rule: Mult(Inverse2(Inverse2(x)), z) - Mult(x, z)
Add rule: Mult(Inverse2(x), Mult(x, z)) - z
Collapse: Inverse(Inverse2(Inverse2(Inverse2(x)))) - Inverse(Inverse2(x))
To: Inverse(Inverse2(x)) = Inverse(Inverse2(x))
Collapse: Inverse2(Inverse2(Inverse2(Inverse2(x)))) Inverse2(Inverse2(x))
To: Inverse2(Inverse2(x)) = Inverse2(Inverse2(x))
Collapse: Mult(x, Inverse2(Inverse2(Inverse2(x)))) f
To: Mult(x, Inverse2(x)) = f
Add rule: Inverse2(Inverse2(Inverse2(x))) -> Inverse2(x)
Collapse: Mult(x, Inverse(Inverse2(Inverse2(x)))) -> e
To: Mult(x, Inverse(x)) = e
Add rule: Inverse(Inverse2(Inverse2(x))) -> Inverse(x)
Add rule: Mult(x, Mult(y, Inverse2(Mult(x, y)))) -> f
Add rule: Inverse2(Mult(Inverse2(y), y)) -> f
Add rule: Mult(x, Inverse2(Inverse(Inverse2(x)))) > f
Add rule: Mult(Inverse2(x), Inverse2(Inverse(x))) f
Collapse: Inverse(Inverse2(Inverse2(x))) -> Inverse(x)
To: Inverse(Inverse2(Inverse(x))) = Inverse(x)
Collapse: Inverse2(Inverse2(Inverse2(x))) -> Inverse2(x)
To: Inverse2(Inverse(Inverse2(x))) = Inverse2(x)
Collapse: Mult(Inverse2(Inverse2(x)), z) - Mult(x, z)
To: Mult(Inverse2(Inverse(x)), z) = Mult(x, z)
Add rule: Inverse2(Inverse2(x)) -> Inverse2(Inverse(x))
Compose: Mult(x, f) -> Inverse2(Inverse2(x))
To: Mult(x, f) -> Inverse2(Inverse(x))
Collapse: Mult(x, Inverse2(Inverse(Inverse2(x)))) - f
To: Mult(x, Inverse2(x)) = f
Add rule: Inverse2(Inverse(Inverse2(x))) -> Inverse2(x)
Add rule: Inverse(Inverse2(Inverse(x))) -> Inverse(x)
Add rule: Mult(Inverse2(Inverse(x)), Inverse(x)) -> e
Add rule: Mult(Inverse(Inverse2(x)), Inverse2(x)) f
Add rule: Mult(Inverse2(Inverse(x)), Inverse2(x)) -> f continued
43


Add rule: Inverse2(Inverse(Inverse(x))) Inverse2(x)
Collapse: Mult(Inverse(Inverse2(x)), Inverse2(x)) f
To: Mult(Inverse(Inverse(x)), Inverse2(x)) = f
Collapse: Inverse(Inverse2(Inverse(x))) Inverse(x)
To: Inverse(Inverse(Inverse(x))) = Inverse(x)
Collapse: Inverse2(Inverse(Inverse2(x))) Inverse2(x)
To: Inverse2(Inverse(Inverse(x))) = Inverse2(x)
Add rule: Inverse(Inverse2(x)) Inverse(Inverse(x))
Compose: Mult(x, e) - Inverse(Inverse2(x))
To: Mult(x, e) -> Inverse(Inverse(x))
Add rule: Inverse(Inverse(Inverse(x))) -> Inverse(x)
Add rule: Mult(Inverse(Inverse(x)), Inverse(x)) - e
Add rule: Mult(Inverse2(x), Inverse(Inverse(x))) -> e
Add rule: Mult(Inverse(Inverse(x)), Inverse2(x)) -> f
Add rule: Inverse(Inverse(Mult(Inverse2(y), y))) -> e
Collapse: Inverse(Inverse(Mult(Inverse2(y), y))) -> e
To: Inverse(e) = e
Add rule: Inverse(Mult(Inverse2(y), y)) - e
Collapse: Mult(Inverse2(Inverse(x)), Inverse2(x)) -> f
To: Mult(x, Inverse2(x)) = f
Collapse: Mult(Inverse2(Inverse(x)), Inverse(x)) - e
To: Mult(x, Inverse(x)) = e
Add rule: Mult(Inverse2(Inverse(x)), z) -> Mult(x, z)
Add rule: Mult(Inverse(x), Mult(x, z)) -> z
Add rule: Inverse2(Mult(Inverse(x), x)) -> f
Add rule: Inverse2(Inverse(Mult(Inverse(x), x))) -> f
Add rule: Mult(x, Mult(Inverse(x), z)) -> z
Collapse: Mult(Inverse(Inverse(x)), Inverse2(x)) - f
To: Mult(x, Inverse2(x)) = f
Collapse: Mult(Inverse(Inverse(x)), Inverse(x)) -> e
To: Mult(x, Inverse(x)) = e
Add rule: Mult(Inverse(Inverse(x)), z) -> Mult(x, z)
Collapse: Mult(Inverse2(Inverse(x)), z) Mult(x, z)
To: Mult(Inverse(Inverse(x)), z) = Mult(x, z)
Collapse: Inverse(Mult(Inverse2(y), y)) > e
To: Inverse(Mult(Inverse(y), y)) = e
Collapse: Mult(Inverse2(x), Inverse(Inverse(x))) -> e
To: Mult(Inverse(x), Inverse(Inverse(x))) = e
Collapse: Mult(Inverse2(x), Inverse2(Inverse(x))) -> f
continued
44


To: Mult(Inverse(x), Inverse2(Inverse(x))) = f
Collapse: Inverse2(Mult(Inverse2(y), y)) - f
To: Inverse2(Mult(Inverse(y), y)) = f
Collapse: Mult(Inverse2(x), Mult(x, z)) -> z
To: Mult(Inverse(x), Mult(x, z)) = z
Collapse: Mult(x, Mult(Inverse2(x), z)) -> z
To: Mult(x, Mult(Inverse(x), z)) = z
Add rule: Mult(Inverse2(x), z) -> Mult(Inverse(x), z)
Collapse: Inverse2(Inverse(Mult(Inverse(x), x))) -> f
To: Inverse2(e) = f
Add rule: Inverse(Mult(Inverse(y), y)) - e
Add rule: Mult(x, Mult(y, Inverse(Mult(x, y)))) -> e
Collapse: Mult(x, Mult(y, Inverse(Mult(x, y)))) e
To: Mult(x, Inverse(x)) = e
Add rule: Mult(y, Inverse(Mult(x, y))) Inverse(x)
Collapse: Mult(y, Inverse(Mult(x, y))) > Inverse(x)
To: Mult(y, Mult(Inverse(y), Inverse(x))) = Inverse(x)
Collapse: Inverse(Mult(Inverse(y), y)) -> e
To: Mult(Inverse(y), Inverse(Inverse(y))) = e
Add rule: Inverse(Mult(x, y)) -> Mult(Inverse(y), Inverse(x))
Add rule: Mult(y, Inverse2(Mult(Inverse(x), y))) -> Inverse2(Inverse(x))
Collapse: Mult(y, Inverse2(Mult(Inverse(x), y))) -> Inverse2(Inverse(x))
To: Inverse2(Inverse(x)) = Inverse2(Inverse(x))
Collapse: Mult(x, Mult(y, Inverse2(Mult(x, y)))) > f
To: Mult(x, Inverse2(x)) = f
Add rule: Mult(z, Inverse2(Mult(x, z))) -> Inverse2(x)
Collapse: Mult(z, Inverse2(Mult(x, z))) -> Inverse2(x)
To: Mult(z, Mult(Inverse(z), Inverse2(x))) = Inverse2(x)
Collapse: Inverse2(Mult(Inverse(x), x)) -> f
To: Mult(Inverse(x), Inverse2(Inverse(x))) = f
Add rule: Inverse2(Mult(x, z)) > Mult(Inverse(z), Inverse2(x))
45


Upon successful completion, the final set of rewrite rules is displayed:
(1) Inverse2(Mult(x, z)) -> Mult(Inverse(z), Inverse2(x))
(2) Inverse(Mult(x, y)) - Mult(Inverse(y), Inverse(x))
(3) Mult(Inverse2(x), z) - Mult(Inverse(x), z)
(4) Mult(Inverse(Inverse(x)), z) > Mult(x, z)
(5) Mult(x, Mult(Inverse(x), z)) -> z
(6) Mult(Inverse(x), Mult(x, z)) z
(7) Inverse(Inverse(Inverse(x))) -> Inverse(x)
(8) Inverse(Inverse2(x)) -> Inverse(Inverse(x))
(9) Inverse2(Inverse(Inverse(x))) > Inverse2(x)
(10) Inverse2(Inverse2(x)) -> Inverse2(Inverse(x))
(11) Mult(x, e) - Inverse(Inverse(x))
(12) Mult(x, f) - Inverse2(Inverse(x))
(13) Mult(Mult(x, y), z) - Mult(x, Mult(y, z))
(14) Inverse(e) - e
(15) Inverse(f) - e
(16) Mult(x, Inverse(x)) -> e
(17) Inverse2(e) - f
(18) Inverse2(f) f
(19) Mult(x, Inverse2(x)) -> f
(20) Mult(e, x) -> x
(21) Mult(f, x) > x
Using the resulting rewrite system we can prove the following two theorems:
> Prove Mult(Inverse(e), Inverse(Mult(Inverse(y), Mult(y, x)))) =
> Mult(Inverse(Mult(x, Inverse2(x))), Inverse(x))
1st term normalized: Inverse(x)
2nd term normalized: Inverse(x)
>
>
> Prove Mult(Mult(e, x), Inverse2(Mult(Inverse2(Inverse(Inverse(f))), x))) =
> Mult(x, Inverse2(Mult(Inverse(f), Mult(Inverse(z), Mult(z, x)))))
1st term normalized: f
2nd term normalized: f
46


The next example also illustrates the input and output of a sample run of the
given term rewriting system:
> declare sorts
> loops;
>
> declare constants
> e : loops;
>
> declare variables
> x : loops;
>
> declare functions
> f, g : loops loops;
>
> declare equations
> f(g(f(x))) = g(f(x));
>
> KnuthBendix e(l) g(0) f(0)
Unlike the previous examples, however, this one does not find a complete TRS,
but generates an infinite number of critical pairs:
Add rule: f(g(f(x))) g(f(x))
Add rule: f(g(g(f(x)))) - g(g(f(x)))
Add rule: f(g(g(g(f(x)))))g(g(g(f(x))))
Add rule: f(g(g(g(g(f(x)))))) g(g(g(g(f(x)))))
Add rule: f(g(g(g(g(g(f(x))))) g(g(g(g(g(f(x))))))
Add rule: f(g(g(g(g(g(g(f(x)))))))) -> g(g(g(g(g(g(f(x)))))))
Add rule: f(g(g(g(g(g(g(g(f(x))))))))) -> g(g(g(g(g(g(g(f(x))))))))
Add rule: f(g(g(g(g(g(g(g(g(f(x)))))))))) g(g(g(g(g(g(g(g(f(x)))))))))
Add rule: f(g(g(g(g(g(g(g(g(g(f(x))))))))))) -> g(g(g(g(g(g(g(g(g(f(x))))))))))
The term rewriting system continued in this fashion until it aborted due to a lack
of memory. However, it is clear that if the system had not run out of memory it
would have continued to generate more and more critical pairs of the same form.
47


7. Conclusion
Reasoning about equality has been one of the most challenging problems in
automated deduction. In the past thirty years, a number of methods have been
proposed. In this survey, an overview has been given on one of the more
successful approaches, the term rewriting method.
Term rewriting was originally proposed for generating canonical term rewriting
systems which can be used as decision procedures for proving the validity of
equalities in certain equational theories. With the emergence of equationally
specified abstract data types in the late 1970s, term rewriting has gained
considerable popularity also as a bridge between programming language theory and
program verification. Its application to theorem proving has also been extended to
different domains.
The term rewriting approach to theorem proving is unique in several aspects. It
is one of the few methods which can be applied to a variety of problem domains.
In addition to the validity problem of equational logic, it has also been applied to
inductive theorem proving, first-order theorem proving, unification theory, and
even geometry theorem proving. From the operational point of view, term
rewriting is a forward chaining method. In other words, its main inference
mechanism deduces new lemmas from known theorems, rather than reducing the
intended problem into subproblems and trying to solve them separately. Forward
chaining methods are usually not efficient due to the large number of theorems
produced which makes the search space unmanageable. As a tradeoff, forward
chaining methods usually do not require backtracking, which is necessary in most
backchaining methods. In fact, term rewriting is one of the very few successful
forward chaining methods. The problem of space explosion is handled in term
rewriting through two techniques: a notion of critical pairs, which tries to find only
"useful" lemmas, and more importantly, a notion of "simplification." Basically
simplification replaces existing data by those which are logically equivalent but
"smaller" according to some well-founded ordering. Since the ordering is well-
founded, simplification cannot go on indefinitely.
48


Appendix A
#include
File: t_except.h
/****************************************************************************/
/* Exceptions */
/****************************************************************************/
typedef enum {
#define SystemException(m) m,
#include "t_errors.h"
EXCEPTION_COUNT
} EXCEPTION;
/****************************************************************************/
/* Traps */
/****************************************************************************/
typedef struct exception_trap {
jmp_buf Jump_Buffer;
struct exception_trap *next;
} EXCEPTION_TRAP, *PEXCEPTION_TRAP;
jmp_buf *ExceptionTry (PEXCEPTION_TRAP pException_Trap)
int ExceptionCatch (void);
void ExceptionEnd (PEXCEPTION_TRAP pException_Trap);
void ExceptionThrow (EXCEPTION Exception, int iLine, char *pcFile);
void ExceptionRethrow (void);
const char *ExceptionLiteral (void);
const char ExceptionFile (void);
int ExceptionLine (void);
EXCEPTION ExceptionValue (void);
#define TRY \
{ \
EXCEPTION_TRAP Exception_Trap; \
if (setjmp (*ExceptionTry (&Exception_Trap)) == 0)
#define CATCH else if (ExceptionCatch0)
#define END_TRY_CATCH ExceptionEnd (&Exception_Trap) }
#define THROW(Exception) ExceptionThrow ((Exception), ___LINE__, __FILE___)
/*
A macro to rethrow the exception being handled. This macro may appear only
in a handler or in a function directly or indirectly called from a handler.
*/
#define RETHROW ExceptionRethrowO
#ifdef NDEBUG
(define assert (p) ((void)0)
#else
define assert (p) ((p) ? ((void)0) : THROW (ASSERTION_FAIL))
#endif
File: t_except.c
include "t_except.h"
49


/ft***************************************************************************/
/* Exception Literals */
/a-***************************************************************************/
static const char *Exception_Text[] = {
ttdefine SystemException(m) #m,
#include "t_errors.h"
0
};
int
char
EXCEPTION
PEXCEPTION TRAP
Current_Exception_Line ;
*Current_Exception_File;
Current_Except ion;
pException_Stack = 0;
jmp_buf *ExceptionTry (PEXCEPTION_TRAP pException_Trap)
Current_Exception = NULL_EXCEPTION;
pException_Trap->next = pException_Stack;
pException_Stack = pException_Trap;
return (&pException_Trap->Jump_Buffer) ,-
int ExceptionCatch (void)
if (pException_Stack)
pException_Stack = pException_Stack->next;
return (1);
}
void ExceptionEnd (PEXCEPTION_TRAP pException_Trap)
if (pException_Stack == pException_Trap)
/****************************************************************y
/* Not specifying a handler for a try-block is equivalent to */
/* specifying CATCH RETHROW; That is, the search for a handler */
/* continues in a dynmaically surrounding try-block. */
/****************************************************************/
ExceptionCatch();
ExceptionRethrow();
else
{
Current_Exception = NULL_EXCEPTION;
/****************************************************************************/
/* When an exception is thrown, control is transferred to the handler whose */
/* try-block was most recently entered by the thread of control and not yet */
/* exited. ~ */
void ExceptionThrow (EXCEPTION Exception, int iLine, char *pcFile)
/****************************************************************/
/* longjmp cannot pass the value 0; if 0 is passed in as the */
/* value of Exception, longjmp will substitute the value 1. */
/* Therefore, define a throw of the value 0 to be a no-op. */
/ft***************************************************************/
if (Exception == NULL_EXCEPTION)
return;
50


}
if (pException Stack)
{
Current_Exception = Exception;
Current_Exception_Line = iLine;
Current_Exception_File = pcFile;
longjmp (pException_Stack->Jump_Buffer, Exception);
void ExceptionRethrow (void)
{
ExceptionThrow (Current_Exception,
Current_Exception_Line,
Current~Exception_File);
/*
Given an Exception, return the Exception as a literal character string.
*/
const char *ExceptionLiteral (void)
return Exception_Text[Current_Exception];
const char ExceptionFile (void)
return (Current_Exception == NULL_EXCEPTION) ? "" : Current_Exception_File
int ExceptionLine (void)
return (Current_Exception == NULL_EXCEPTION) ? 0 : Current_Exception_Line;
EXCEPTION ExceptionValue (void)
return (Current_Exception);
File: t_parse.h
/* Global Prototypes */
/it***************************************************************************/
void Parse (void);
#include
#include
ttinclude
#include
#include
#include
ttinclude
#include
#include
#include




"t_except.h"
"t_lex.hn
nt_memory.h"
"t_normal.h"
"t_output.h"
"t_parse.h"
File: tparse.c
/Needed only for memcpy prototype */
BOOLEAN gbCtrl_C_Hit;
extern long Token_Value;
ttinclude nt_algebr.h"
51


/****************************************************************************/
/* Local Function Prototypes */
/tic************************************-
static void ParseProcess (char
static void ParseLoop (PLEX
static void Parselnclude (PLEX
static void ParseSignature (PLEX
static void ParseDeclarations (PLEX
static void ParseSorts (PLEX
static void ParseConstants (PLEX
static void ParseFunctions (PLEX
static void ParseVariables (PLEX
static void ParseEquations (PLEX
PPEQUATION E);
r*************************************/
filename);
pLex);
pLex);
pLex, PALGEBRA pAlgebra);
pLex, PALGEBRA pAlgebra);
pLex, PSYMBOLJTABLE pSymbolTable);
pLex, PSYMBOLJTABLE pSymbolTable);
pLex, PSYMBOLJTABLE pSymbolTable);
pLex, PSYMBOLJTABLE pSymbolTable) ;
pLex, PSYMBOL_TABLE pSymbolTable,
static PSORT ParseMatchSort
static PTERM ParseTerm
static SUBTERMS ParseTerms
t);
(PLEX pLex,
(PLEX pLex,
(PLEX pLex,
PSYMBOLJTABLE pSymbolTable);
PSYMBOL_TABLE pSymbolTable);
PSYMBOLJTABLE pSymbolTable, PTERM
static void
static void
static void
static void
pSymbolTable);
static void
pSymbolTable);
static void
ParseMatch
ParseUnify
ParseKB
ParseUseTrs
ParseProve
ParseKBTotalOrder
(PLEX pLex, PSYMBOLJTABLE pSymbolTable);
(PLEX pLex, PSYMBOL_TABLE pSymbolTable);
(PLEX pLex, PALGEBRA pAlgebra);
(PLEX pLex, PREWRITE R, PSYMBOLJTABLE
(PLEX pLex, PREWRITE R, PSYMBOLJTABLE
(PLEX pLex, PALGEBRA pAlgebra);
static void SetVariableWeights (PEQUATION E, WEIGHT Weight);
extern IDENTIFIER Token_Identifier[];
#define MatchToken(Token) LexMatchToken (pLex, Token)
void Parse (void)
{
/********************************************************************/
/* Install a signal handler to modify the behavior of CTRL-C. */
/********************************************************************/
gbCtrl_C_Hit = FALSE;
if (signal (SIGINT, CtrlCHandler) == SIG_ERR)
THROW (INTERNAL_CHECK);
ParseProcess (NOLL) ,-
1
static void ParseProcess (char filename)
{
LEX Lex;
Lexlnitiate (&Lex, filename);
TRY
{
ParseLoop (&Lex);
CATCH
{
LexTerminate (&Lex);
RETHROW;
}
END_TRY_CATCH
LexTerminate (&Lex);
}
52


static void ParseLoop (PLEX pLex)
PALGEBRA pAlgebra = NULL_PALGEBRA;
MemAlloc ((PPTR)fcpAlgebra, sizeof(ALGEBRA));
pAlgebra->pSymbolTable = SymbolTableCreate (31);
while (!(MatchToken (TOKEN_EOF) |j MatchToken (TOKEN_QUIT)))
switch (MatchToken (TOKEN UNKNOWN))
{
case TOKEN_INCLUDE: Parselnclude (pLex); break;
case TOKEN_UNIFÂ¥: ParseUnify (pLex, pAlgebra->pSymbolTable); break;
case TOKEN_MATCH: ParseMatch (pLex, pAlgebra->pSymbolTable); break;
case TOKEN_DECLARE: ParseDeclarations (pLex, pAlgebra); break;
case TOKEN_KNUTH_BENDIX: ParseKB (pLex, pAlgebra); break;
default: THROW (ASSERTION_FAIL);
SymbolTableDestroy (pAlgebra->pSymbolTable);
MemFree ((PPTR) SpAlgebra);
static void Parselnclude (PLEX pLex)
char buf[100];
if (!MatchToken (TOKEN_IDENTIFIER))
THROW (TRS______MISSING_INCLUDE);
strcpy (buf, Token_Identifier);
strcat (buf, ".trs");
ParseProcess (buf) ,-
}
static void ParseSignature (PLEX pLex, PALGEBRA pAlgebra)
if (!MatchToken (TOKEN_IDENTIFIER))
THROW (TRS__MISSING_SIGNATURE);
MemStrDup ((PPTR)&pAlgebra->pSignature, Token_Identifier);
if (!MatchToken (TOKEN_EQUALS))
THROW (TRS MISSING EQUALS);
} _
static void ParseDeclarations (PLEX pLex, PALGEBRA pAlgebra)
PSYMBOLJIABLE pSymbolTable = pAlgebra->pSytnbolTable;
switch (MatchToken (TOKEN UNKNOWN))
{
}
case TOKEN_SORTS:
case TOKEN_CONSTANTS
case TOKEN_FUNCTIONS
case TOKEN_VARIABLES
case TOKEN_EQUATIONS
default:
ParseSorts (pLex, pSymbolTable); break;
ParseConstants (pLex, pSymbolTable); break;
ParseFunctions (pLex, pSymbolTable); break;
ParseVariables (pLex, pSymbolTable); break;
ParseEquations (pLex, pSymbolTable, &pAlgebra->E) ,-
break;
THROW (TRS DECLARE_WHAT);
}
if ([MatchToken (TOKEN_SEMI_COLON))
THROW (TRS______MISSING_SEMI_COLON);
53


static void ParseSorts (PLEX pLex, PSYMBOL_TABLE pSymbolTable)
do {
if (IMatchToken (TOKEN_IDENTIFIER))
THROW (TRS__MISSING_SORT);
Symbollnsert (pSymbolTable, Token_Identifier, Sort);
} while (MatchToken (TOKEN COMMA));
}
static void ParseConstants (PLEX pLex, PSYMBOL_TABLE pSymbolTable)
int i;
PSORT Range;
PCONSTANT Array[100];
do {
i = 0;
do {
if (IMatchToken (TOKEN_IDENTIFIER))
THROW (TRS___MISSING_CONSTANT) ;
Array[i++] = (PCONSTANT) Symbollnsert (pSymbolTable,
Token_Identifier,
Constant);
} while (MatchToken (TOKEN_COMMA));
if (IMatchToken (TOKEN_COLON))
THROW (TRS___MISSING_COLON);
if ((Range = ParseMatchSort (pLex, pSymbolTable)) == NULL_PSORT)
THROW (TRS_______MISSING_RANGE);
while (i--)
Array[i]->Range = Range;
} while (MatchToken (TOKEN_COMMA));
static void ParseFunctions (PLEX pLex, PSYMBOL_TABLE pSymbolTable)
int i;
ARITY Arity;
PSORT pSort, Range, Domain[100];
PFUNCTION pFunction;
PFONCTION Array[100];
do {
i = 0;
do {
if (IMatchToken (TOKEN IDENTIFIER))
THROW (TRS__MISSING_FUNCTION);
Array[i++] = (PFONCTION) Symbollnsert (pSymbolTable,
Token_Identifier,
Function);
} while (MatchToken (TOKEN_COMMA));
54


if (IMatchToken (TOKEN_COLON))
THROW (TRS__MISSING_COLON);
Arity = 0;
while ((pSort = ParseMatchSort (pLex, pSymbolTable)) != NULL_PSORT)
Domain[Arity++] = pSort;
if (IMatchToken (TOKEN_COMMA))
break;
}
if (IMatchToken (TOKEN_ARROW))
THROW (TRS__MISSING_ARROW);
if ((Range = ParseMatchSort (pLex, pSymbolTable)) == NtJLL_PSORT)
THROW (TRS______MISSING_RANGE);
while (i)
{
pFunction = Array [i];
pFunction->Arity = Arity;
pFunction->Range = Range;
MemAlloc ((PPTR)&pFunction->Domain, Arity sizeof(PSORT));
memcpy (pFunction->Domain, Domain, Arity sizeof(PSORT));
} while (MatchToken (TOKEN_COMMA));
static void ParseVariables (PLEX pLex, PSYMBOL_TABLE pSymbolTable)
int i;
PSORT pSort;
PVARIABLE pVariablel, pVariable2;
PVARIABLE Array[100];
do {
i = 0;
do {
if (IMatchToken (TOKEN_IDENTIFIER))
THROW (TRS__MISSING_VARIABLE);
pVariablel = (PVARIABLE) Symbollnsert (pSymbolTable,
Token_Ident i f i er,
Variable);
strcat (Token_Identifier, "'");
pVariable2 = TPVARIABLE) Symbollnsert (pSymbolTable,
Token_Identifier,
Variable);
pVariablel->Rename = pVariable2;
pVariable2->Rename = pVariablel;
Array[i++] = pVariablel;
Array[i++] = pVariable2;
} while (MatchToken (TOKEN_COMMA));
if (IMatchToken (TOKEN_COLON))
THROW (TRS__MISSING_C0L0N);
if ((pSort = ParseMatchSort (pLex, pSymbolTable)) == NULL_PSORT)
THROW (TRS_VARIABLE_SORT) ;
while (i)
Array[i]->pSort = pSort;
} while (MatchToken (TOKEN_COMMA));
55


static PSORT ParseMatchSort (PLEX pLex, PSYMBOL_TABLE pSymbolTable)
PSYMBOL pSymbol;
if (MatChToken (TOKEN IDENTIFIER))
{
pSymbol = SymbolLocate (pSymbolTable, Token_Identifier);
if ((pSymbol != NDLL_PSYMBOL) && (pSymbol->Type == Sort))
return ((PSORT)pSymbol);
return (NULL PSORT);
}
static void ParseEquations (PLEX pLex, PSYMBOL_TABLE pSymbolTable, PPEQUATION E)
PTERM Lbs, Rhs;
do {
Lhs = ParseTerm (pLex, pSymbolTable) ,-
if (!MatChToken (TOKEN_EQUALS))
THROW (TRS__MISSING_EQUALS);
Rhs = ParseTerm (pLex, pSymbolTable);
RuleAdd (E, RuleMake (Lhs, Rhs)),-
} while (MatChToken (TOKEN_COMMA));
/*
Parenthesized Prefix Notation
*/
static PTERM ParseTerm (PLEX pLex, PSYMBOL_TABLE pSymbolTable)
TERM V[MAX__TERMS];
ParseTerms (pLex,.pSymbolTable, v);
return (TermCopy (v));
static SUBTERMS ParseTerms (PLEX pLex, PSYMBOL_TABLE pSymbolTable, PTERM t)
ARITY i;
if (!MatChToken (TOKEN_IDENTIFIER))
THROW (TRS__MISSING_IDENTIFIER);
t->pSymbol = SymbolLocate (pSymbolTable, Token_Identifier);
t->SubTerms = 1;
if (t->pSymbol == NULL_PSYMBOL)
THROW (TRS_UNKNOWN_IDENTIFIER) ;
if (IsFunction (t))
{
if ([MatChToken (TOKEN_LP))
THROW (TRS__MISSING_LP);
for (i = 1; i <= Arity (t),- i++)
t->SubTerms += ParseTerms (pLex, pSymbolTable, TermSkip (t));
56


if ((i < Arity (t)) && IMatchToken (TOKEN_COMMA))
THROW (TRS MISSING COMMA);
}
if (IMatchToken (TOKEN_RP))
THROW (TRS MISSING RP);
}
return (t->SubTerms);
}
static void ParseMatch (PLEX pLex, PSYMBOL_TABLE pSymbolTable)
PTERM S, t;
BOOLEAN bSuccess;
s = ParseTerm (pLex, pSymbolTable);
if (IMatchToken (TOKEN_AND))
THROW (TRS__MISSING_AND),-
t = ParseTerm (pLex, pSymbolTable);
if (IMatchToken (TOKEN_EXPECTING))
THROW (TRS__MISSING_EXPECTING);
switch (MatchToken (TOKEN UNKNOWN))
{
case TOKEN_FAILURE: bSuccess = FALSE; break;
case TOKEN_SUCCESS: bSuccess = TRUE; break;
default: THROW (TRS___EXPECTING_STATUS);
TermMatchVerify (s, t, bSuccess);
TermFree (s);
TermFree (t);
}
static void ParseUnify (PLEX pLex, PSYMBOL_TABLE pSymbolTable)
PTERM s, t, u;
s = ParseTerm (pLex, pSymbolTable);
if (IMatchToken (TOKEN_AND))
THROW (TRS__MISSING_AND);
t = ParseTerm (pLex, pSymbolTable);
if (IMatchToken (TOKEN_EXPECTING))
THROW (TRS__MISSING_EXPECTING);
if (MatchToken (TOKEN_FAILURE))
U = NULL_PTERM;
else
u = ParseTerm (pLex, pSymbolTable);
TermUnifyVerify (s, t, u);
TermFree (s);
TermFree (t);
TermFree (u);
57


static void ParseKB (PLEX pLex, PALGEBRA pAlgebra)
PREWRITE R;
ParseKBTotalOrder (pLex, pAlgebra)
MatchToken (TOKEN_SEMI_COLON);
R = TermKnuthBendix (&pAlgebra->E);
RuleDisplay (stdout, R, "Rewrite", "->"),-
ParseUseTrs (pLex, R, pAlgebra->pSymbolTable);
RuleClose (&R);
}
static void ParseUseTrs (PLEX pLex, PREWRITE R, PSYMBOL_TABLE pSymbolTable)
while (1)
{
if (MatchToken (TOKEN PROVE))
{
ParseProve (pLex, R, pSymbolTable);
MatchToken (TOKEN SEMI COLON);
} '
else
return,-
static void ParseProve (PLEX pLex, PREWRITE R, PSYMBOL_TABLE pSymbolTable)
PTERM s, t, sp, tp;
s = ParseTerm (pLex, pSymbolTable);
if (!MatchToken (TOKEN_EQUALS))
THROW (TRS__MISSING_EQUALS);
t = ParseTerm (pLex, pSymbolTable);
sp = TermNormalize (s, R);
tp = TermNormalize (t, R);
TrsPrintf (stdout, "1st term normalized: "),-
TermDisplay (stdout, sp); TrsPrintf (stdout, "\n"),-
TrsPrintf (stdout, "2nd term normalized: ");
TermDisplay (stdout, tp);TrsPrintf (stdout, "\n");
TermFree (s) ,-
TermFree (t);
TermFree (sp);
TermFree (tp);
static void ParseKBTotalOrder (PLEX pLex, PALGEBRA pAlgebra)
TOTAL_ORDER TotalOrder = 0;
PSYMBOL pSymbol;
WEIGHT Weight = 0X7FFF;
PSYMBOL_TABLE pSymbolTable = pAlgebra->pSymbolTable;
do {
if (IMatchToken (TOKENJEDENTIFIER))
THROW (TRS______MISSING_IDENTIFIER);
58


pSymbol = SymbolLocate (pSymbolTable, Token_Identifier);
if (pSymbol == NULL_PSYMBOL)
THROW (TRS__UNKNOWN_IDENTIFIER);
if (pSymbol->Type == Constant)
((PCONSTANT)(pSymbol))->TotalOrder = TotalOrder++;
else if (pSymbol->Type == Function)
((PFUNCTION)(pSymbol))->TotalOrder = TotalOrder++;
else
THROW (TRS__INVALID_IDENTIFIER);
if (IMatchToken (TOKEN_LP))
THROW (TRS__MISSING_LP);
if (IMatchToken (TOKEN_NUMBER))
THROW (TRS__MISSING_NUMBER);
pSymbol->Weight = (WEIGHT)Token_Value;
if (pSymbol->Type == Constant)
if (pSymbol->Weight < Weight)
Weight = pSymbol->Weight;
if (IMatchToken (TOKEN_RP))
THROW (TRS__MISSING_RP);
} while (MatchToken (TOKEN_TOTAL_ORDER));
SetVariableWeights (pAlgebra->E, Weight);
static void SetVariableWeights (PEQUATION E, WEIGHT Weight)
CPTERM Z;
PTERM t;
PRULE Rule;
For_Every_Rule (Rule, E)
t = Rule->Rhs;
for (z = TermSkip (t); t != z; TermNext (t))
if (IsVariable(t))
Weight(t) = Weight;
t = Rule->Lhs;
for (z = TermSkip (t); t != z; TermNext (t))
{
if (IsVariable(t))
Weight(t) = Weight;
File: t_main.c
#include "t_except.h"
ttinclude nt_memory.h"
((include nt_output.h"
ttinclude "t_parse.h"
59


void main (void)
TrsPrintf (stdout, "*** Welcome ***\n");
TRY
{
Memlnitiate ();
TRY
Parse () ;
CATCH
TrsException ();
END_TRY_CATCH
MemTerminate ();
}
CATCH
{
TrsException ();
END_TRY_CATCH
TrsPrintf (stdout, "*** Farewell ***\n");
#include "t_except.h"
#include "t_normal.h"
# inc lude 11 t_output. h "
File: t match.c
/****************************************************************************i
/* Wrapper for TermMatchO, with consistency check build in. */
/* If a subsitution a exits such that a(s) = t, */
/* then let u = cr(s) and insist that u = t. */
^*******************************************r*****************************#***^
void TermMatchVerify (CPTERM s, CPTERM t, BOOLEAN bSuccess)
PTERM U;
SUBST Sigma;
if (Sigma = TermMatch (s, t))
{
if (bSuccess == FALSE)
{
TrsPrintf (stderr, "Error:.did not expect a successful match.\n");
return;
u = TermSubstitute (Sigma, s);
. if (TermCompare (t, u) != 0)
TrsPrintf (stderr, "Error: the term substitution failed.\n");
TrsPrintf (stderr, " => );
TermDisplay (stderr, u);
TrsPrintf (stderr, "\n"j;
TermFree (u);
}
else
{
if (bSuccess == TRUE)
TrsPrintf (stderr, "Error: did not match given terms.\n"),-
60


/A***************************************************************************/
/* Find, if it exists, a subsitution a such that a(s) = t. */
^/Hr******************************'*******-************************************^
SUBST TermMatch (CPTERM s, CPTERM t)
{
CPTERM Z;
SUBST Sigma = TermNextSigma () ,
for (z = TermSkip (s); s != z; TermNext (s))
if (IsVariable (s))
{
if (Sigma (s) == Sigma)
if (TermCompare (S(s), t) != 0)
return (0);
}
else
{
S(s) = t;
Sigma(s) = Sigma;
t = TermSkip (t);
else
{
if (!IdenticalSymbols (s, t))
return (0) ,-
TermNext (t);
return (Sigma);
}
File: t_memory.h
typedef void *PTR, **PPTR;
/* Global Function Prototypes */
/****************************************************************************/
void Memlnitiate (void);
void MemTerminate (void) ,-
void MemAlloc (PPTR pPtr, unsigned int uisize);
void MemRealloc (PPTR pPtr, unsigned int uisize);
void MemStrDup (PPTR pPtr, const PTR Ptr);
void MemFree (PPTR pPtr) ,-
File: t_memory.c
((include
#include
#include "t_except.h"
#include "t_memory.h"
long glAllocations,-
ttdefine NULL_PTR ((PTR)O)
void Memlnitiate (void)
{
glAllocations = 0L;
}
61


void MemTerminate (void)
{
if (glAllocations != OL)
THROW (MEM TERMINATE);
, 1
void MemAlloc (PPTR pPtr, unsigned int uiSize)
if (uiSize == 0) /* A zero length allocation should */
{ /* result in a NULL_PTR, rather than */
pPtr = NULL_PTR; /* a pointer to a zero-length item. */
else
{
if ((*pPtr = (PTR) calloc (1, uiSize)) == NULL_PTR)
THROW (MEM_ALLOCATE) ;
glAllocations++;
void MemRealloc (PPTR pPtr, unsigned int uiSize)
{
if (uiSize == 0)
{
/* See relevant comment in MemAlloc. */
}
else
{
if (*pPtr != NULL_PTR)
MemFree (pPtr);
if (*pPtr != NULL_PTR)
glAllocations--;
if ((*pPtr = (PTR) realloc (*pPtr, uiSize)) == NULL_PTR)
THROW (MEM_REALLOCATE) ;
glAllocations++;
void MemStrDup (PPTR pPtr, const PTR Ptr)
unsigned int uiSize;
uiSize = strlen(Ptr) + 1;
MemAlloc (pPtr, uiSize);
memcpy (*pPtr, Ptr, uiSize);
void MemFree (PPTR pPtr)
if (*pPtr == NULL_PTR)
THROW (MEM FREE);
free (*pPtr);
*pPtr = NULL_PTR;
glAllocations--;
62


File: t normal.h
#include nt rules.h"
/****************************************************************************/
/* Global Function Prototypes */
^*********************************************************************^
PTERM TermNormalize
SOBST TermMatch
void TermMatchVerify
SUBST TermNextSigma
PTERM TermSubstitute
SUBST TermUnify
void TerraUnifyVerify
void TermSuperPosition
PREWRITE TermKnuthBendix
(CPTERM t, CPREWRITE R) ;
(CPTERM s, CPTERM t) ;
(CPTERM S, CPTERM t, BOOLEAN bSuccess);
(void) ;
(SUBST Sigma, CPTERM t);
(CPTERM S, CPTERM t) ;
(CPTERM S, CPTERM t, CPTERM u) ;
(PPEQUATION E, CPREWRITE R, CPRULE Rule_s);
(PPEQUATION E);
#include "t normal.h"
File: t normal.c

/* Normalize the given term with respect to the given rewrite system. */
/* */
/* "Normalizing" a term with a rewrite system R consists in replacing a */
/* subterm which matches a left-hand side of a rewrite rule by the right- */
/* hand side whose variables are bound to values computed by the matching */
/* algorithm. This relation is denoted by ->R. Iterating this process */
/* is called "reducing". A term which cannot be rewritten is said to be */
/* in "normal form". */
/*****4r**#********************************#*************'*****************#***^/
PTERM TermNormalize (CPTERM t, CPREWRITE R)
{
CPRULE Rule;
CPTERM Z;
PTERM q, r, S, U;
SUBST Sigma;
r = TermCopy (t);
RESTART:
for (s = r, z = TermSkip (s); s != z; TermNext (s))
For Every Rule (Rule, R)
{ "
if (HsVariable (Rule->Lhs))
{
if (Sigma = TermMatch (Rule->Lhs, s))
u = TermSubstitute (Sigma, Rule->Rhs);
q = TermReplace (r, s, u);
TermFree (r) ,-
TermFree (u);
r = q;
goto RESTART;
return (r);
63


#include
File: t_output.h
/ irkitlckltlt ***** it ************* * +************ ************** ** ****************** /
/* Global Function Prototypes */
/****************************************************************************/
void TrsException (void),-
void TrsPrintf (FILE Stream, const char Format, ...);
File: t_output.c
#include
#include
ftinclude "t_except.h
#include t_output. h"
FILE *Log_Stream;
void TrsException (void)
TrsPrintf (stderr, "Exception %s on line %d of file %s.\n",
ExceptionLiteral(), ExceptionLine(), ExceptionFile());
void TrsPrintf (FILE Stream, const char Format, _____)
{
va_list marker;
va_start (marker. Format);
vfprintf (Stream, Format, marker);
va end (marker) ,-
}
File: t_rules.h
#include "t terms.h"
typedef struct _RULE {
struct _RULE Next;
struct RULE Prev;
PTERM LhS;
PTERM Rhs;
} RULE, PRULE, PPRULE;
typedef const RULE CPRULE;
typedef PRULE PEQUATION, PREWRITE;
typedef PPRULE PPEQUATION, PPREWRITE;
typedef CPRULE CPEQUATION, CPREWRITE;
#define For_Every_Rule(Rule, R) for (Rule = R; Rule; Rule = Rule->Next)
/***************************************************************************/
/* Global Function Prototypes */
/a***************************************************************************/
PRULE RuleMake (PTERM LhS, PTERM Rhs);
void RuleAdd (PPRULE R, PRULE Rule);
void RuleRemove (PRULE Rule);
void RuleFree (PRULE Rule) ,-
void RuleClose (PPRULE R);
void RuleDisplay (FILE Stream, PRULE Rule, unsigned char pName, unsigned char
*pSep) ,-
64


File: t rules.c
((include "t_memory.h"
((include "t_output.h"
#include "t rules.h"
PRULE RuleMake (PTERM Lhs, PTERM Rhs)
{
PROLE Rule;
MemAlloc ((PPTR)tRule, sizeof(RULE));
Rule->Lhs = Lhs;
Rule->Rhs = Rhs;
return (Rule);
void RuleAdd (PPROLE R, PROLE Rule)
{
PROLE Temp;
Temp = *R;
*R = Rule;
Rule->Prev = R;
Rule->Next = Temp;
if (Temp)
Temp->Prev = &Rule->Next;
void RuleRemove (PROLE Rule)
{
if (*(Rule->Prev) = Rule->Next)
Rule->Next->Prev = Rule->Prev;
Rule->Next = 0;
Rule->Prev =0;
void RuleFree (PROLE Rule)
{
if { (Rule)
TermFree (Rule->Lhs);
TermFree (Rule->Rhs);
} MemFree ((PPTR)&Rule)
void RuleClose (PPROLE R)
{
PROLE Rule, Next;
for (Rule = *R; Rule; Rule = Next)
{
Next = Rule->Next;
RuleFree (Rule);
void RuleDisplay (FILE Stream, PROLE Rule, unsigned char pName, unsigned char
*pSep)
65


int i = 1;
TrsPrintf (Stream, "%s Rules:\n", pName),
while (Rule)
{
TrsPrintf (Stream, "(%d) ", i++);
TermDisplay (Stream, Rule->Lhs);
TrsPrintf (Stream, %s ", pSep);
TermDisplay (Stream, Rule->Rhs);
TrsPrintf (Stream, "\n");
Rule = Rule->Next,-
File: t_subst.c
#include /* Needed only for memcpy prototype */
#include "t normal.h"
SUBST TermNextSigma (void)
static SUBST Sigma = 0,-
++Sigma;
return (Sigma);
/Hr***************************************************************************/
/* Apply the given substitution to the given term (s = a(t)). */
PTERM TermSubstitute (SUBST Sigma, CPTERM t)
TERM u[MAX__TERMS];
CPTERM z;
PTERM S = U;
for (z = TermSkip (t) ,- t != z; TermNext (t))
if ((IsVariable (t)) && /* t is a variable */
(Sigma(t) == Sigma) && /* {t <- r} in Sigma */
(!IdenticalSymbols (t, S(t)))) /* Don't apply {x <- x} */
memcpy (s, S(t), TermSize (S(t)));
s += S(t)->SubTerms;
}
else
{
*S++ = *t;
TermFixUp (u);
return (TermCopy (u));
ttinclude "t normal.h"
File: t_super.c
^*****************************r***********************************************^
/* Local Function Prototypes */
/Jr***************************************************************************/
66


static void Superposition (PPEQUATION E, CPRULE Rule_s, CPRULE Rule_t, CPTERM u);
static PRDLE RenameVariables (CPROLE Rule);
static void RenameBack (PTERM t);
^Jr*************************************************************************^
/* Superpose the new rule on all existing rules (including itself) and */
/* introduce each critical pair into the axiom set. */
ye***************************************************************************/
void TermSuperPosition (PPEQUATION E, CPREWRITE R, CPRULE Rule_s)
CPTERM u, z;
PRULE Renamed_Rule_s;
CPRULE Rule_t;
Renamed_Rule_s = RenameVariables (Rule_s);
For_Every_Rule (Rule_t, R)
u = Renamed_Rule_s->Lhs;
for (z = TermSkip (u)u != z; TermNext (u))
Superposition (E, Renamed_Rule_s, Rule_t, u);
u = Rule_t->Lhs;
for (z = TermSkip (u), TermNext (u); u != z; TermNext (u))
Superposition (E, Rule_t, Renamed_Rule_s, u) ,
RuleFree (Renamed Rule s);
} "
static void Superposition (PPEQUATION E, CPRULE Rule_s, CPRULE Rule_t, CPTERM u)
PTERM r, m, n;
SUBST Sigma;
if (HsVariable (u))
{
if (Sigma = TermUnify (u, Rule_t->Lhs))
m = TermSubstitute (Sigma, Rule_s->Rhs);
RenameBack (m);
r = TermReplace (Rule_s->Lhs, u, Rule_t->Rhs);
n = TermSubstitute (Sigma, r);
RenameBack (n);
TermFree (r);
RuleAdd (E, RuleMake (m, n));
static PRULE RenameVariables (CPRULE Rule)
{
CPTERM z;
PTERM t, Lhs, Rhs;
t = Lhs = TermCopy (Rule->Lhs);
for (z = TermSkip (t); t 1= z; TermNext (t))
if (IsVariable (t))
t->pSymbol = (PSYMBOL)Rename(t);
t = Rhs = TermCopy (Rule->Rhs);
for (z = TermSkip (t); t != z; TermNext (t))
67


if (IsVariable (t))
t >pSymbol = (PSYMBOL) Rename (t);
return (RuleMake (Lhs, Rhs));
}
#include
static void RenameBack (PTERM t)
{
CPTERM Z;
unsigned char *p;
for (z = TermSkip (t); t != z; TermNext (t))
if (IsVariable (t))
{
p = Identifier (t),-
if (p[strlen(p) 1] == 'V')
t->pSymbol = (PSYMBOL)Rename(t);
#include "t terms.h"
File: t table.h
/* Entry */
^****************************Tfr***********************************************y
typedef struct _ENTRY_ {
struct _ENTRY_ *NextEntry;
struct _ENTRY_ **PrevEntry;
SYMBOL Symbol;
} ENTRY, *PENTRY, **PPENTRY;
ttdefine NULL_PENTRY ((PENTRY)0)
#define NULL_PPENTRY ((PPENTRY)0)
/****************************************************************************/
/* Symbol Table */
/it***************************************************************************/
typedef struct {
unsigned int uiSize,-
unsigned int uiSymbols;
PENTRY Table[1];
} SYMBOL_TABLE, PSYMBOL_TABLE;
#define NOLL_PSYMBOL_TABLE ((PSYMBOL_TABLE)0)
y****************************************************************************^
/* Global Function Prototypes */
/*******************************************************^
PSYMBOL_TABLE SymbolTableCreate (unsigned int uisize);
void SymbolTcibleDestroy (PSYMBOL_TABLE pSymbolTable);
PSYMBOL Symbollnsert (PSYMBOL_TABLE pSymbolTable, PIDENTIFIER pldentifier, TYPE
Type);
void SymbolRemove (PSYMBOL_TABLE pSymbolTable, PIDENTIFIER pldentifier);
PSYMBOL SymbolLocate (PSYMBOL_TABLE pSymbolTable, PIDENTIFIER pldentifier);
68


#include
#include "t_except.h"
((include "t_memory.h"
((include "t table.h"
File: t_table.c
/* needed only for strcmpO prototype! */
/****************************************************************************/
/* Local Function Prototypes */
/***********************************'***************** ^
static PENTRY SymbolAllocate (PIDENTIFIER pldentifier, TYPE Type);
static int SymbolHash (PIDENTIFIER pldentifier);
static void EntryFree (PENTRY pEntry);
static PENTRY EntryLocate (PSYMBOL_TABLE pSymbolTable, PIDENTIFIER pldentifier);
#define GET_PENTRY(pht, ident) (pht->Table)[SymbolHash(ident) % pht->uisize]
/****************************************************************************^/
/* Make a hash table the size specified in uisize. The hash table is a */
/* data structure that the manager uses to organize the database entries. */
/* It contains a "hash table" array along with various other housekeeping */
/* variables. The uisize argument controls the size of the array portion */
/* of the data structure, but any number of symbols can be put into the */
/* table, regardless of the table size. Different table sizes will affect */
/* the speed with which a symbol can be accessed, however. If the table */
/* is too small, the search time will be unnecessarily long. Ideally the */
/* table should be about the same size as the expected number of symbols. */
/* There is no benefit in making the table too large. It's a good idea */
/* to make uisize a prime number. Some useful sizes are: 47, 61, 89, */
/* 113, 127, 157, 193, 211, 257, 293, 337, 367, 401. */
y****************************************************************************y
PSYMBOL_TABLE SymbolTableCreate (unsigned int uisize)
int iTable_Size;
PSYMBOL_TABLE pSymbolTable;
iTable_Size = ((uisize + 1) sizeof(PSYMBOL)) + sizeof(SYMBOL_TABLE);
MemAlloc ((PPTR) SpSymbolTable, iTable_Size) ,
memset (pSymbolTable, 0, iTable_Size) ,-
pSymbolTable->uiSize = uisize;
pSymbolTable->uiSymbols = 0;
return (pSymbolTable);
void SymbolTableDestroy (PSYMBOL_TABLE pSymbolTable)
PENTRY pEntry, pNextEntry;
PPENTRY ppEntryHead;
assert (pSymbolTable != NULL_PSYMBOL_TABLE);
for (ppEntryHead = pSymbolTable->Table; pSymbolTable->uiSize--;
ppEntryHead++)
for (pEntry = *ppEntryHead; pEntry; pEntry = pNextEntry)
pNextEntry = pEntry- >NextEntry,-
if (pEntry->Symbol.Type == Function)
MemFree ((PPTR)&((PFONCTION)(&pEntry->Symbol))->Domain);
EntryFree (pEntry);
69


MemFree ((PPTR)tpSymbolTable);
PSYMBOL Symbollnsert (PSYMBOL_TABLE pSymbolTable, PIDENTIFIER pldentifier, TYPE
Type)
PENTRY pEntry, pEntryFirst;
PPENTRY ppEntryHead;
assert (pSymbolTable != NULL_PSYMBOL_TABLE);
assert (pldentifier != NULL_PIDENTIFIER);
if (EntryLocate (pSymbolTable, pldentifier) != NULL_PENTRY)
THROW (TRS_DUPLICATE_SYMBOL) ;
pEntry = SymbolAllocate (pldentifier, Type) ;
/************************************************************************/
/* Add 'pEntry' to the front of the doubly-linked list at ppSymbolHead */
/************************************************************************/
ppEntryHead = &GET_PENTRY(pSymbolTable, pldentifier);
pEntryFirst = ppEntryHead;
ppEntryHead = pEntry;
pEntry->PrevEntry = ppEntryHead;
pEntry->NextEntry = pEntryFirst;
if (pEntryFirst != NULL_PENTRY)
pEntryFirst->PrevEntry = kpEntry->NextEntry;
pSymbolTable->uiSymbols++;
return (&pEntry->Symbol);
void SymbolRemove (PSYMBOL_TABLE pSymbolTeible, PIDENTIFIER pldentifier)
PENTRY pEntry;
assert (pSymbolTable != NDLL_PSYMBOL_TABLE);
assert (pldentifier != NULL_PIDENTIFIER);
if ((pEntry = EntryLocate (pSymbolTable, pldentifier)) != NULL_PENTRY)
if ((*(pEntry->PrevEntry) = pEntry->NextEntry) != NULL_PENTRY)
pEntry->NextEntry->PrevEntry = pEntry->PrevEntry;
pSymbolTable->uiSymbols--;
EntryFree (pEntry);
PSYMBOL SymbolLocate (PSYMBOL_TABLE pSymbolTable, PIDENTIFIER pldentifier)
PENTRY pEntry;
pEntry = EntryLocate (pSymbolTable, pldentifier);
return (pEntry ? fcpEntry->Symbol : NULL_PSYMBOL);
static PENTRY EntryLocate (PSYMBOL_TABLE pSymbolTable, PIDENTIFIER pldentifier)
PENTRY pEntry;
70


assert (pSymbolTable != NULL_PSYMBOL_TABLE);
assert (pldentifier != NULL_PIDENTIFIER);
for (pEntry = GET_PENTRY(pSymbolTable, pldentifier);
pEntry != NULL_PENTRY;
pEntry = pEntry->NextEntry)
if (strcmp (pldentifier, pEntry->Symbol.pldentifier) == 0)
break;
}
return (pEntry) ,-
static PENTRY SymbolAllocate (PIDENTIFIER pldentifier, TYPE Type)
unsigned int uiSize;
PENTRY pEntry;
uiSize = sizeof(ENTRY) sizeof(SYMBOL) ;
switch (Type)
case Sort:
case Constant:
case Function:
case Variable
}
uiSize += sizeof(SORT);
uiSize += sizeof(CONSTANT)
uiSize += sizeof(FUNCTION)
uiSize += sizeof(VARIABLE)
break
break
break
break
MemAlloc ((PPTR)kpEntry, uiSize),-
memset (pEntry, 0, uiSize);
MemStrDup ((PPTR) &pEntry-^Symbol.pldentifier, pldentifier);
pEntry->Symbol.Type = Type;
return (pEntry);
static void EntryFree (PENTRY pEntry)
if (pEntry != NULL PENTRY)
{
if (pEntry->Symbol.pldentifier != NULL_PIDENTIFIER)
MemFree ((PPTR)fcpEntry->Symbol.pldentifier);
MemFree ((PPTR) tpEntry) ,-
#define NBITS_IN_INT ( sizeof(int) 3 )
#define SEVENTY_FIVE_PERCENT ((int)( NBITS_IN_INT .75 ))
ttdefine TWELVE_PERCENT ((int)( NBITS_IN_INT .125 ))
#define HIGH_BITS ( -( (unsigned int)(-0) >> TWELVE_PERCENT ) )
static int SymbolHash (PIDENTIFIER pldentifier)
int g, h = 0;
for (; pldentifier; ++pldentifier)
h = (h TWELVE_PERCENT) + pldentifier,-
if ((g = h & HIGH_BITS) > 0)
h = (h A (g SEVENTY FIVE PERCENT)) & -HIGH_BITS;
return (h);
}
71


File: t_terms.h
tt include "t_output.h"
#include "t_system.h"
y*******************************************it**************'******************y
/* Data Types */
y****************************************************************************^
typedef unsigned int ARITY;
typedef unsigned int SUBTERMS;
typedef unsigned int TOTAL_ORDER
typedef long SUBST;
#define MAX__TERMS 200
y****************************************************************************y
/* Type */
y****************************************************************************y
typedef enum {
Constant,
Function,
Variable,
Sort
} TYPE, *PTYPE, **PPTYPE;
ttdefine NULL PTYPE ((PTYPE)O)
typedef int WEIGHT;
typedef struct {
TYPE Type;
PIDENTIFIER pldentifier;
WEIGHT Weight; /* Knuth-Bendix ordering weight */
} SYMBOL, *PSYMBOL;
#define NULL_PSYMBOL ((PSYMBOL)O)
y****************************************************************************y
/* Term */
y***************************************************************'*************y
typedef struct {
PSYMBOL pSymbol;
SUBTERMS SubTerms;
} TERM, *PTERM;
typedef const TERM *CPTERM;
ttdefine NULL_PTERM ((PTERM)0)
#define NULL_CPTERM ((CPTERM)O)
#include nt_symbol.h"
#define TO_PSYMBOL(t)
idefine TO_PCONSTANT(t)
#define TO_PFUNCTION(t)
ttdefine TO_PVARIABLE(t)
#define R(t)
ttdefine Sigma(t)
ttdefine Path(t)
ttdefine S(t)
ttdefine Rename(t)
ttdefine Identifier(t)
ttdefine Weight(t)
((t)->pSymbol)
((PCONSTANT)TO_PSYMBOL(t))
((PFUNCTION)TO_PSYMBOL(t))
((PVARIABLE)TO_PSYMBOL(t))
TO_PVARIABLE(t)->r
TO_PVARIABLE(t)->Sigma
TO_PVARIABLE(t)->path
TO_PVARIABLE(t)->s
TO_PVARIABLE (t) >Rename
TO_PSYMBOL(t)->pldentifier
TO_PSYMBOL(t)->Weight
72


/****************************************************************************/
/* ^**********,*********r************* ((define TermType(t) Term Macros */ ********************************************/ (TO_PSYMBOL(t)->Type)
((define ((define ((define IsConstant(t) isFunction(t) IsVariable(t) (TermType(t) == Constant) (TermType(t) == Function) (TermType(t) == Variable)
((define ((define ((define ((define IdenticalSymbols(t, s) identicalConstants(t, s) IdenticalFunctions(t, s) IdenticalVariables(t, s) (TO_PSYMBOL(t) == TO_PSYMBOL(S)) (IsConstant(t) && IdenticalSymbols(t, (IsFunction(t) && IdenticalSymbols(t, (IsVariable(t) && IdenticalSymbols(t, s)) s)) s))
((define Arity(t) (IsFunction(t) ? TO_PFUNCTION(t)->Arity : 0)
#define ((define ((define TermSkip(t) TermNext(tj TermSize(t) ((t) + (t)->SubTerms) (SubTerms sizeof(TERM))
/ft***************************************************************************/
/* Global Function Prototypes */
/A***************************************************************************/
PTERM TermCopy (CPTERM t);
int TermCompare (CPTERM s, CPTERM t);
SUBTERMS TermDisplay (FILE Stream, CPTERM t);
void TermFree (PTERM t);
SUBTERMS TermFixUp (PTERM t);
PTERM TermReplace (CPTERM t, CPTERM s, CPTERM u) ;
TOTAL_ORDER TotalOrder (PTERM t);
File: t_terms.c
((include
((include nt_memory.h"
((include "t_output.h"
#include nt terms.h"
/AT***************************************************************************/
/* Local Function Prototypes */
/ft***************************************************************************/
static void AncestorPatch (PTERM t, PTERM v, int n);
/*******************************************************^
/* Construct and return an identical copy of the given term. */
y****************************************************************************^
PTERM TermCopy (CPTERM t)
unsigned int uiBytes;
PTERM S;
uiBytes = TermSize (t);
MemAlloc ((PPTRJ&s, uiBytes);
memcpy (s, t, uiBytes);
return (s);
}
/A************************************************************************/
/* If the two terms are identical return zero; otherwise, return non-zero. */
/****************************************************************************/
int TermCompare (CPTERM s, CPTERM t)
return memcmp (s, t, TermSize (t));
73


/Jr***************************************************************************/
/* Display the given term. */
/****************************************************************************/
SUBTERMS TermDisplay (FILE *Stream, CPTERM t)
SUBTERMS j;
ARITY i;
TrsPrintf (Stream, "%s", Identifier(t));
if (IsFunction (t))
{
TrsPrintf (Stream, "("),-
for (j = 1, i = 1; i <= Arity(t); i++)
j += TermDisplay (Stream, t + j);
if (i != Arity(t))
TrsPrintf (Stream, ", ");
}
TrsPrintf (Stream,
}
return (t->SubTerms) ;
}
void TermFree (PTERM t)
{
if (t != NULL PTERM)
{
memset (t, 0, TermSize (t));
MemFree ((PPTR) &t),-
^***************************r**********ilr**************************************^
/* */
/A***************************************************************************/
SUBTERMS TermFixUp (PTERM t)
ARITY i;
t->SubTerms = l;
if (IsFunction (t))
{
for (l = 1; i <= Arity (t); i++)
t->SubTerms += TermFixUp (TermSkip (t));
return (t->SubTerms);
}
/it***************************************************************************/
/* In term 't' replace the subterm 's' with term 'u' (i.e., return t[u]s). */
PTERM TermReplace (CPTERM t, CPTERM s, CPTERM u)
PTERM s_prime, t_prime;
int iDelta_Terms = (int)(u->SubTerms s->SubTerms);
MemAlloc ((PPTR)&t_prime, (t->SubTerms + iDelta_Terms) sizeof(TERM));
s_prime = t_prime + (s t);
memcpy (t_prime, t, (s t) sizeof (TERM) ),-
74


raemcpy (s_prime, u, TermSize (u)) ;
s += s->SubTerms;
memcpy (TermSkip (s_prime), s, (t->SubTerms (s t)) sizeof(TERM));
if (iDelta_Terms != 0)
AncestorPatch (t_prime, s_prime, iDelta_Terms);
return (t_prime);
static void AncestorPatch (PTERM t, PTERM v, int n)
{
while (t < v)
{
if (TermSkip (t) > v)
{ /* At this point: t is an ancestor of v */
t->SubTerms += n;
TermNext (t);
}
else
{
t = TermSkip (t);
TOTAL ORDER TotalOrder (PTERM t)
{ "
if (IsConstant (t))
return TO_PCONSTANT (t) >TotalOrder ;
if (IsFunction (t))
return TO_PFUNCTION(t)->TotalOrder;
return (0);
}
#include "t_except.h"
#include "t_output.h"
#include "t_normal.h"
iinclude "t terms.h"
File: t_unify.c
typedef CPTERM PATH;
ttdefine NIL NULL_PTERM
#define DONE ((PTERM)1)
#define LOOP ((PTERM)2)
#define AddPath(p, v) Path(v) = p; p = v
^*************************************************************************'***/
/* Local Function Prototypes */
/****************************************************************************^
static void Init
static void Term
static void HERE
static void VAR_HERE
static CPTERM VERE
Static CPTERM TERM_VERE
static PATH Source
static BOOLEAN OnPath
static void Collapse
static void RECUR HERE
(CPTERM S, CPTERM t);
(CPTERM S, CPTERM t, SUBST Sigma);
(CPTERM s, CPTERM t);
(CPTERM u, CPTERM t);
(CPTERM U, SUBST Sigma);
(CPTERM t, SUBST Sigma);
(CPTERM X, CPTERM *v);
(PATH path, CPTERM v);
(PATH path, CPTERM v);
(CPTERM V, CPTERM y, CPTERM t);
75


/it***************************************************************************/
/* Find, if it exists, a subsitution a such that ct(s) = a(t). */
/***************************************************************************/
SUBST TermUnify (CPTERM s, CPTERM t)
SUBST Sigma = TermNextSigma ();
TRY
{
Init (s. t);
HERE (s, t) ;
Term (s, t,
}
CATCH
{
if (ExceptionValue() != UNIFY_FAILURE)
RETHROW;
Sigma = 0;
}
END_TRY_CATCH
return (Sigma) ;
static void Init (CPTERM s, CPTERM t)
{
CPTERM Z;
for (z = TermSkip (s); s != z,- TermNext (s))
{
}
if (IsVariable (s))
R(s) = S(s) = NIL;
for (z = TermSkip (t); t != z; TermNext (t))
{
if (IsVariable (t))
R(t) = S(t) = NIL;
}
static void Term (CPTERM s, CPTERM t, SUBST Sigma)
CPTERM z;
for (z = TermSkip (s); s != z; TermNext (s))
if (IsVariable (s) && (S(s) == NIL))
VERE (s, Sigma);
for (z = TermSkip (t); t != z; TermNext (t))
{
if (IsVariable (t) && (S(t) == NIL))
VERE (t, Sigma);
}
/*
Definition: A "homogeneous equivalence relation" is such that:
(1) a variable may be equivalent to any term t;
(2) two non-variable terms t and s are equivalent iff:
- they correspond to the same constant or function symbol
(homo-geneity condition); and
- their ith subterms are pairwise equivalent.
76


Static void HERE (CPTERM S, CPTERM t)
{
CPTERM Z;
if (!(IdenticalVariables (t, s) II IdenticalConstants (t, s)))
{
if (IsVariable (t))
VAR_HERE (t, S);
else if (IsVariable (s))
VAR_HERE (s, t);
else
{
if (!IdenticalFunctions (t, s))
THROW (ONI FY_FAILURE) ,-
for (z = TermSkip (t), TermNext (t), TermNext (s),-
t = z;
t = TermSkip (t), s = TermSkip (s))
HERE (t, S);
static void VAR HERE (CPTERM u, CPTERM t)
{
PATH path, path2;
CPTERM V, w, Z;
if (R (u) == NIL)
R (u) = t;
else
{
if (!IsVariable (t))
{
path = Source (u, tv)
Collapse (path, v);
if (R(v) == NIL)
R(v) = t;
else
RECUR HERE (v, R(v), t)
}
else
{
if (R (t) == NIL)
R (t) = U;
else
{
path = Source (u, &v);
if ((R (v) == NIL) II (R (v) == DONE) )
{
AddPath (path, v);
Collapse (path, t) ,-
else
{
path2 = Source (t, &w);
if (IdenticalSymbols (v, w))
Collapse (path, v) ,-
Collapse (path2, v);
else
{
Z = R(w) ;
Collapse (path, v);
AddPath (path2, w);
Collapse (path2, v);
if ((z != NIL) && (z != DONE))
77


}
RECUR_HERE (v, R(v), z) ;
static void RECUR HERE (CPTERM V, CPTERM y, CPTERM t)
{
R(v) = LOOP;
HERE (y, t);
R(v) = y;
^ft******************************#*******************************************!^
/* Source(x) traverses the path up from x, to the last variable v in this */
/* path if it is loop-free, or up to the first variable to appear twice on */
/* the path. Variables along the path are put in a list and marked "done" */
/* using their r-pointers. Notice that for a loop-free path the source */
/* variable v is not marked, thus preserving R(v). */
/**************************************************************************** j
Static PATH source (CPTERM x, CPTERM *v)
{
CPTERM Z;
PATH path;
Path(x) = NIL;
path = x;
while ((R(x) != DONE) && (R(x) != LOOP) && (R(x) != NIL) && IsVariable
(R(x)))
{
Z = R (x) ;
R(x) = DONE;
if (OnPath (path, z))
break;
AddPath (path, z);
x = z;
}
*v = path;
path = Path(path);
return (path);
static BOOLEAN OnPath (PATH path, CPTERM v)
for (; path; path = Path(path))
if (IdenticalSymbols (path, v))
return (TRUE) ,-
}
return (FALSE);
}
/ft***************************************************************************/
/* Collapse directs the r-pointers of all variables in the given path to a */
/* source variable v. */
/***************************************************************************/
static void Collapse (PATH path, CPTERM v)
for (; path; path = Path(path))
R(path) = v;
78


static CPTERM VERE (CPTERM u, SUBST Sigma)
CPTERM V, y, z;
PATH path, p,-
path = Source (u, &v) ;
if (R(v) == NIL) /*
Z = V/ / *
R(v) = DONE; - /*
else if (R(v) == DONE) /*
{
if (S(v) == LOOP)
THROW (UNIFY_FAILURE);
Z = (S (v) == NIL) ? V : S (v) ;
}
else
{
switch (TermType (R(v)))
case Constant: /*
S (v) = z = R (v) ; /*
Sigma(v) = Sigma; R(v) = DONE; /*
break;
case Function: /*
y = R (V) ;
Case 1. u -> ... -> w -> v -> nil */
v is a common substitution to all */
variables in the path. */
Case 4. u ..-> w -> v -> done */
Case 2. u w -> v -> constant */
R(v) is a common substitution to all */
variables in the path. */
> w -> v -> f(. ..) */
Case 3. u >. .
R(v) = DONE;
S(v) = LOOP;
for (p = path; p; p = Path(p))
S(p) = LOOP;
S(v) = z = TERM_VERE (y, Sigma);
Sigma(v) = Sigma;
break;
default:
TrsPrintf (stderr, "Error This should never happen\n");
THROW (ONIFY_FAILURE);
break;
for (p = path; p; p = Path(p))
S(p) = z;
Sigma(p) = Sigma;
return (z);
}
static CPTERM TERM VERE (CPTERM t, STJBST Sigma)
{
CPTERM r, S, Z;
S = t;
for (z = TermSkip (t), TermNext (t); t != z; t = TermSkip (t))
r = NULL_PTERM;
if (IsVariable(t))
{
if (R(t) == DONE)
79


{
}
if (S(t) == LOOP)
THROW (UNIFY_FAILURE);
else
r = S (t); // Replace subterm ti by S(ti)
else if (R(t) != NIL)
r = VERE (t, Sigma); // Replace subterm ti by VERE(ti)
else if (IsFunction(t))
r = TERM_VERE (t, Sigma); // Replace subterm ti by TERM_VERE(ti)
if (r != NOLL PTERM)
{
r = TermReplace (s, t, r);
z = TermSkip (r);
t = r + (t s) ;
s = r;
}
return (s);
}
void TermUnifyVerify (CPTERM s, CPTERM t, CPTERM u)
PTERM sp, tp;
SUBST Sigma;
if (Sigma = TermUnify (s, t))
if (u == NULL_CPTERM)
TrsPrintf (stderr, "Error: did not expect unification.\n");
return
}
sp = TermSubstitute (Sigma, s);
if (TermCompare (sp, u) != 0)
TermFree (sp);
TrsPrintf (stderr, "Error: the term substitution failed.\n") ,-
return,-
}
tp = TermSubstitute (Sigma, t);
if (TermCompare (tp, u) != 0)
TermFree (sp);
TermFree (tp);
TrsPrintf (stderr, "Error: the term substitution failed.\n") ,-
return;
}
if (TermCompare (sp, tp) != 0)
TermFree (sp);
TermFree (tp);
TrsPrintf (stderr, "Error: the term substitution failed.\n");
return;
}
TermFree (sp);
TermFree (tp);
TrsPrintf (stdout, "As expected, terms were successfully unified.\n");
80


else
{
Xf (u != NULL_CPTERM)
TrsPrintf (stderr, "Error: did not succeed in unifying terms.\n");
else
TrsPrintf (stdout, "As expected, the terms were not unified.\n");
File: t_lex.h
iinclude
#include "t_system.h"
typedef enum {
TOKEN_NULL,
TOKEN_UNKNOWN,
TOKEN_DECLARE,
TOKEN_EQUATIONS,
TOKEN_CONSTANTS,
TOKEN_FUNCTIONS,
TOKEN_VARIABLES,
TOKEN_SORTS,
TOKEN_QUIT,
TOKEN_INCLUDE,
TOKEN_AND,
TOKEN_MATCH,
T0KEN_EXPECT1NG,
TOKEN_FAILURE,
TOKEN_SUCCESS,
TOKEN_UNIFY,
TOKEN_KNUTH_BENDIX,
TOKEN_PROVE,
TOKEN_NORMALIZE,
TOKEN_IDENTIFIER,
TOKEN_NUMBER,
TOKEN_EQUALS,
TOKEN_COMMA,
TOKEN_COLON,
TOKEN_SEMI_COLON,
TOKEN_LP,
TOKEN_RP,
TOKEN_ARROW,
TOKEN_TOTAL ORDER,
TOKEN_EOF
} TOKEN;
^************************************************************************Hf***/
/* */
^**********r***:***'**************r**********************************************y
typedef struct {
char *pCurrent; /* Pointer to the current byte within the buffer */
char pBuffer,- /* Pointer to the first byte in the buffer */
FILE *stream;
} LEX, *PLEX;
#define NULL_PLEX ((PLEX)O)
#define LEX_BUFFER_SIZE 256
#define MAX IDENTIFIER 32
/* Global Function Prototypes */
81


void Lexlnitiate (PLEX pLex, char filename);
void LexTerminate (PLEX pLex);
TOKEN LexMatchToken (PLEX pLex, TOKEN Token);
#include
#include
#include
include
include
#include
#include
#include
#include





"t_except.h"
"t_lex.h"
nt_memory.h"
"t_output.h"
File: t lex.c
define isalpha_(c)
#define isalnum_(c)
#define Advance
(define Current
(isalpha(c) ] I (c =
(isalnum(c) | | (c =
*(pLex)->pCurrent++
(pLex)->pCurrent
'))
'))
static TOKEN LexNumber (PLEX pLex)
static void LexComment (PLEX pLex)
static TOKEN LexKeyword (PLEX pLex)
static void LexGetLine (PLEX pLex)
y4r**4,*****4r*,*##**4r*<*****4r*4r*********4r*********************4l4r4r*4rik********#tfr***y
/* Keywords */
/ft***************************************************************************/
static const struct KEYWORD {
PIDENTIFIER pldentifier;
TOKEN Token;
} Keyword!] = {
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
(PIDENTIFIER)
}<
"declare",
"equations",
"constants",
"functions",
"variables",
"sorts",
"quit",
"include",
"and",
"match",
"expecting",
"failure",
"success",
"unify",
"knuthbendix",
"prove",
"normalize",
TOKEN
TOKEN"
token"
token"
TOKEN"
token"
token"
token"
token"
token"
token"
token"
token"
token"
token"
token"
token"
DECLARE
EQUATIONS
CONSTANTS
'FUNCTIONS
VARIABLES
SORTS
QUIT
INCLUDE
'AND
'match
'EXPECTING
'failure
'success
'unify
'knuth_bendix
'prove
NORMALIZE
define KEYWORDS ( sizeof(Keyword) / sizeof(struct KEYWORD) )
TOKEN Token;
IDENTIFIER Token_Identifier[MAX_IDENTIFIER + 1];
long Token_Value,-
TOKEN LexMatchToken (PLEX pLex, TOKEN Match Token)
{
TOKEN TempToken;
82


while (Token == TOKEN NULL)
{
switch (Current)
{
case * .
case '\t;:
case ' \r': Advance break
case ' \n' : LexGetLine (pLex) break
case /_/ , Token = TOKEN EQUALS; Advance break
case / $ t Token = TOKEN COMMA; Advance break
case 1 . Token = TOKEN COLON; Advance break
case ! . / Token = TOKEN-SEMI COLON; Advance break
case ' (' : Token = TOKEN LP; Advance break
case ')' : Token = TOKEN RP; Advance break
case '\0' : Token = TOKEN EOF; break
case '< : Token = TOKEN TOTAL ORDER; Advance
if (Current != '<')
THROW (LEX___INVALID_TOKEN);
Advance;
break;
case Token = TOKEN_ARROW; Advance;
if (Current != '>')
THROW (LEX__INVALID_TOKEN);
Advance; ~
break;
case LexComment (pLex); break;
default: if (isalpha (Current))
Token = LexKeyword (pLex);
else if (isdigit (Current))
Token = LexNumber (pLex);
else if (iscntrl (Current))
Advance; /* Ignore if present */
break;
if ((Match_Token == Token) || (Match_Token == TOKEN_UNKNOWN))
TempToken = Token;
Token = TOKEN NULL;
}
else
{
TempToken = TOKEN_NULL;
return (TempToken);
static TOKEN LexNumber (PLEX pLex)
{
char EndPtr;
Token_Value = strtol (Current, fcEndPtr, 10);
if (Current != EndPtr)
{
Current = EndPtr;
return (TOKEN NUMBER);
}
Advance;
return (TOKEN_UNKNOWN);
static void LexComment (PLEX pLex)
{
Advance;
83


if (Current == '/')
{
}
else if (Current == '*')
LexGetLine (pLex);
{
}
else
Advance;
do {
while (Current != '*')
if (Current == '\n')
LexGetLine (pLex);
else
if (Current == '\0')
THROW (LEX___COMMENT_EOF);
Advance,-
.
Advance;
} while (Current != '/');
Advance;
THROW (LEX INVALID TOKEN);
static TOKEN LexKeyword (FLEX pLex)
unsigned int i, k;
char *p;
if (isalpha_ (Current))
p = Current;
for (i = 0; isalnum_ (*p); i++, p++)
if (i == MAX_IDENTIFIER)
THROW (LEX MAX IDENTIFIER);
} ~ "
for (k = 0; k < KEYWORDS; k++)
{
if (i != strlen (Keyword[k].pldentifier))
continue;
if (stmicmp (Current, Keyword[k] .pldentifier, i) != 0)
continue;
}
Current = p;
return (Keyword[k].Token);
memcpy (Token_Identifier, Current, i);
Token_Identifier[i] = '\0';
Current = p;
return (TOKEN IDENTIFIER);
}
else
THROW (LEX___INVALIDJTOKEN);
return (Token);
void Lexlnitiate (PLEX pLex, char filename)
{
/* Initialize file buffer pointers */
84


MemAlloc ((PPTR)&pLex->pBuffer, LEX____BUFFER_SIZE);
if (filename)
{
if ((pLex->Stream = fopen (filename, "r")) == NULL)
THROW (LEX FILE OPEN);
} ~
else
pLex->Stream = stdin;
LexGetLine (pLex);
Token = TOKEN NULL;
}
void LexTerminate (PLEX pLex)
if (pLex 1= NULL_PLEX)
if (pLex->pBuffer)
MemFree ((PPTR)&pLex->pBuffer); /* * Free file contents buffer. */
if (pLex->Stream != stdin)
fclose (pLex->Stream);
static void LexGetLine (PLEX pLex)
{
int ch;
int iCount;
char *p;
p = Current = pLex->pBuffer,-
if (!feof (pLex->Stream))
TrsPrintf (stdout, "> ");
for (iCount =1; iCount < LEX BUFFER SIZE; iCount++)
{
if ((ch = getc (pLex->Stream)) == EOF)
ch = '\n';
if ((*p++ = ch) == '\n')
break;
*p = '\0';
if (pLex->Stream != stdin)
TrsPrintf (stdout, "%'s", Current);
#include "t_except.h"
#include "t_normal.h"
#include "t_output.h"
File: t_kbproc.c
/* Local Function Prototypes */
/************************************************************************* j
static PRULE SelectEquation (PPEQUATION E);
Static PRULE Orient (PTERM s, PTERM t);
static void KnuthBendixCompose (PREWRITE R);
85


static void KnuthBendixCollapse (PPEQUATION E, PREWRITE R, CPRULE Rule);
PREWRITE TermKnuthBendix (PPEQUATION E)
{
PTERM S, t;
PRULE Rule;
PREWRITE R = 0;
while (*E)
{
Rule = SelectEquation (E);
s = TermNormalize (Rule->Lhs, R);
t = TermNormalize (Rule->Rhs, R);
RuleFree (Rule);
if (TermCompare (s, t) == 0)
TermFree (s);
TermFree (t) ;
continue;
}
Rule = Orient (s, t);
KnuthBendixCollapse (E, R, Rule);
RuleAdd (&R, Rule);
TrsPrintf (stdout, "Add rule: ");
TermDisplay (stdout, Rule->Lhs);
TrsPrintf (stdout, -> ");
TermDisplay (stdout, Rule->Rhs);
TrsPrintf (stdout, "\n");
KnuthBendixCompose (R);
TermSuperPosition (E, R, Rule);
/* Delete */
/* Orient */
/* Collapse */
/* Compose */
/* Deduce */
return (R);
}
^******************,************************'**************************il<:*******y
/* The strategy used to select an axiom is by size; the shortest axiom in */
/* the current axiom set is selected first. This strategy is fair and */
/* nearly always leads to convergence in fewer iterations than selection */
/* on a first-come first-served basis. */
/ft***************************************************************************/
static PRULE SelectEquation (PPEQUATION E)
PRULE Rule, Shortest;
SUBTERMS Rule_Length, Shortest_Length;
Shortest_Length = OxFFFF;
For_Every_Rule (Rule, *E)
Rule_Length = Rule->Lhs->SubTerms + Rule->Rhs->SubTerms;
if (Rule_Length < Shortest_Length)
Shortest = Rule;
Shortest_Length = Rule_Length;
RuleRemove (Shortest) ,-
86


return (Shortest);
}
typedef enum {
LT,
LE,
EQ,
GE,
GT,
NO
} RELATION;
static RELATION KnuthBendixOrient (PTERM s, PTERM t);
Static WEIGHT w (CPTERM t);
static RELATION NumVariables (CPTERM s, CPTERM t);
static unsigned int VarOccurrences (CPTERM v, CPTERM t);
Static RELATION TWOB (PTERM S, PTERM t);
static PRULE Orient (PTERM s, PTERM t)
{
switch (KnuthBendixOrient (s, t))
case GT: return RuleMake (s, t); /* s > t, implies s -> t */
case LT: return RuleMake (t, s)/* s < t, implies t -> s */
default: THROW (ASSERTION_FAIL);
static RELATION KnuthBendixOrient (PTERM s, PTERM t)
{
RELATION n;
WEIGHT W_s, w_t ;
n = NumVariables (s, t);
w_s = w(s) ;
W_t = w(t);
if (w_s > w_t)
if (n == GE || n == EQ)
return (GT);
}
else if (w_s < w_t)
if (n == LE || n == EQ)
return (LT);
else /* w_s == w_t */
if (n == EQ)
{
return (TWOB (s, t));
return (NO);
}
87


y****************************************************************************^
/* The weight of a term is the sum of the weights of the term's symbols. */
/***************************************************************/
Static WEIGHT w (CPTERM t)
{
CPTERM Z;
WEIGHT Weight = Of
for (z = TermSkip (t); t != z; TermNext (t))
Weight += Weight(t);
return (Weight);
static RELATION NumVariables (CPTERM s, CPTERM t)
{
CPTERM V, Z;
RELATION Relation = EQ;
unsigned int VinS, VinT;
v = t;
for (z = TermSkip (v) ; v != z; TermNext (v))
{
if (IsVariable (v))
VinT = VarOccurrences (v, t) ;
VinS = VarOccurrences (v, s);
if (VinS < VinT)
{
if (Relation == GE)
return (NO) ;
Relation = LE;
}
else if (VinS > VinT)
{
if (Relation == LE)
return (NO) ;
Relation = GE;
v = s;
for (z = TermSkip (v); v != z; TermNext (v))
if (IsVariable (v))
{
VinT = VarOccurrences (v, t);
VinS = VarOccurrences (v, s);
if (VinS < VinT)
{
if (Relation == GE)
return (NO);
Relation = LE;
}
else if (VinS > VinT)
{
if (Relation == LE)
return (NO);
Relation = GE;
return (Relation);
}
88


/it***************************************************************************/
/* Return the number of occurrences of the variable v in term t. */
^******************************'***************************,**'************Tir****/
static unsigned int VarOccurrences (CPTERM v, CPTERM t)
CPTERM Z;
unsigned int uiOccurrences = 0;
for (z = TermSkip (t); t != z; TermNext (t))
if (IdenticalVariables(t, v))
uiOccurrences++;
}
return (uiOccurrences);
Static RELATION TWOB (PTERM s, PTERM t)
{
CPTERM Z;
RELATION Relation;
if (IsVariable (s))
{
}
/* Case 2a
if (!IsVariable (t) && XYZ (t, s, u))
return (LT);
else if (IsVariable (t))
{
if (XYZ (s, t, u))
return (GT)
}
else
{
if ('IdenticalSymbols (s, t))
/* Case 2b (i) */
}
else
{
if (TotalOrder (s) > TotalOrder (t))
return (GT);
else
return (LT);
/* Case 2b (ii) */
for (z = TermSkip (t), TermNext (t), TermNext (s);
t I = z ;
t = TermSkip (t), s = TermSkip (s))
{
Relation = KnuthBendixOrient (s, t);
if (Relation != EQ)
return (Relation);
}
return (EQ);
BOOLEAN XYZ (PTERM S, PTERM t, PTERM u)
CPTERM Z;
for (z = TermSkip (s); s 1= z; TermNext (s))
if (!IdenticalSymbols (s, u))
if (IdenticalVariables (s, t))
return (TRUE);
89


}
break;
return (FALSE):
}
static void KnuthBendixCompose (PREWRITE R)
{
PTERM U;
PRULE Rule;
For_Every_Ru1e (Rule, R)
u = TermNormalize (Rule->Rhs, R);
if (TermCompare (Rule->Rhs, u) != 0)
TrsPrintf (stdout, "Compose: ");
TermDisplay (stdout, Rule->Lhs);
TrsPrintf (stdout, -> ");
TermDisplay (stdout, Rule->Rhs);
TrsPrintf (stdout, "\n");
TrsPrintf (stdout, To: ");
TermDisplay (stdout, Rule->Lhs);
TrsPrintf (stdout, -> "),-
TermDisplay (stdout, u);
TrsPrintf (stdout, "\n");
}
TermFree (Rule->Rhs);
Rule->Rhs = u;
static void KnuthBendixCollapse (PPEQUATION E, PREWRITE R, CPRULE Rule)
PTERM U;
PRDLE Next;
while (R)
{
assert ((Rule->Next == 0) £& (Rule->Prev == 0));
u = TermNormalize (R->Lhs, Rule);
if (TermCompare (R->Lhs, u) != 0)
TrsPrintf (stdout, "Collapse: ");
TermDisplay (stdout, R->Lhs) ,-
TrsPrintf (stdout, -> ");
TermDisplay (stdout, R->Rhs);
TrsPrintf (stdout, "\n");
TrsPrintf (stdout, " To: ");
TermDisplay (stdout, u);
TrsPrintf (stdout, = ");
TermDisplay (stdout, R->Rhs);
TrsPrintf (stdout, "\n");
Next = R->Next;
RuleRemove (R);
TermFree (R->Lhs);
R->Lhs = U;
RuleAdd (E, R);
R = Next;
}
else
{
TermFree (u) ,-
90


}
R = R->Next;
File: t_algebr.h
#include "t_rules.h"
#include "t table.h"
^***************************************************************************^
ALGEBRA;

pOl^llClLtUlU LP rn imri'iTTi
pSymbol_Table
E
^ h* * ** * * * * * * ** * * * * * * * * * * * * * * * * * * * * ** *** * j
typedef struct {
unsigned char *pSignature;
PSYMBOL_TABLE pSymbolTable;
PEQUATION E;
} ALGEBRA, *PALGEBRA;
#define NOLL PALGEBRA ((PALGEBRA)0)
File: t_symbol.h
/****************************************************************************\
SORT:
Type

1 1 1 1 1 1 1 1 1 1 1 1 1
\it it 4( h 1t it it 1t h ii it -k it it it it it it 1t h it it -k 1r it it it it 1t it ic 1t 1t it it 1t h it it ir it * 1t 1r ** ie 1r it * it 1t ic it it ir it it it * /
typedef struct {
SYMBOL Symbol;
} SORT, *PSORT, **PPSORT;
idefine NOLL_PSORT ((PSORT)O)
#define NULL PPSORT ((PPSORT)O)
/****************************************************************************\
CONSTANT:
Type

rmrmiim


typedef struct {
SYMBOL Symbol;
91


PSORT Range;
TOTAL_ORDER TotalOrder;
} CONSTANT, *PCONSTANT;
ttdefine NOLL PCONSTANT ((PCONSTANT)0)
/****************************************************************************\
FUNCTION:
\* ***************************************************************************/
typedef struct {
SYMBOL
ARITY
PPSORT
PSORT
TOTAL ORDER
} FUNCTION, PFUNCTION;
Symbol ,-
Arity;
Domain;
Range;
TotalOrder;
#define NULL PFUNCTION ((PFUNCTION)0)
/****************************************************************************\
VARIABLE:
\****************************************************************************y
typedef struct VRBL {
SYMBOL Symbol;
PSORT pSort;
CPTERM r; // Needed for unification
CPTERM s; // Needed for unification
CPTERM path;
SUBST Sigma;
struct VRBL Rename;
} VARIABLE, PVARIABLE;
#define NULL PVARIABLE ((PVARIABLE)0)
File: t_system.h
typedef unsigned int BOOLEAN;
#define FALSE ((BOOLEAN)0)
#define TRUE ((BOOLEAN)1)
typedef unsigned char IDENTIFIER, PIDENTIFIER;
#define NULL PIDENTIFIER ((PIDENTIFIER)0)
92


File: t_errors.h
^**********************************************1t************tlr****************/
/* Exception foundation file: make changes here and source files will adapt */
/it***************************************************************************/
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemExcept ion
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
Sys temExcept ion
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
SystemException
(NULL EXCEPTION)
(ASSERTION_FAIL)
(INTERNAL_CHECK)
(MEM__ALLOCATE)
(MEM_REALLOCATE)
(MEM_FREE)
(MEM__TERMINATE)
(LEX__INVALID_TOKEN)
(LEX__COMMENT_EOF)
(LEX_MAX_IDENTIFIER)
(LEX__FILEJDPEN)
(TRS__MISSING_DECLARE)
(TRS__DECLARE_WHAT)
(TRS__MISSING_SIGNATURE)
(TRS__MISSING_EQUALS)
(TRS__MISSING_SORT)
(TRS__MISSING_CONSTANT)
(TRS__MISSING_FUNCTION)
(TRS__MISSING_VARIABLE)
(TRS__MISSING_COLON)
(TRS__MISSING_SEMI_COLON)
(TRS__MISSING_ARROW)
(TRS__MISSING_RANGE)
(TRS__OPNS_NAME)
(TRS_VARIABLE_SORT)
(TRS__DUPLICATE_SYMBOL)
(TRS__MISSING_IDENTIFIER)
(TRS__UNKNOWN_IDENTIFIER)
(TRS__INVALID_IDENTIFIER)
(TRS__MISSING_LP)
(TRS__MISSING_COMMA)
(TRS__MISSING_RP)
(TRS__MISSING_AND)
(TRS__MISSING_EXPECTING)
(TRS__MISSING_NUMBER)
(TRS__MISSING_INCLUDE)
(TRS__EXPECTING_STATUS)
(VAR_DUPLICATE)
(UNIFY FAILURE)
/* Must be 1st exception listed */
/* Debug only: assertion failed */
/* Should never happen not!!! */
#undef SystemException
/* Allow re-definition to occur */
93


References
Ardis, M.A., 1980. Data abstraction transformations. Ph.D. Thesis, Report TR-
925, Dept, of Computer Science, University of Maryland.
Bachmair, Leo, and Dershowitz, Nachum, 1987. Inference rules for rewrite-based
first-order theorem proving. In Proceedings of the 2nd Symposium on Logic in
Computer Science, Ithaca, New York, pp. 331-337.
Bachmair, Leo, and Dershowitz, Nachum, 1988. Critical pair criteria for
completion. Journal of Symbolic Computation 6, pp. 1-18.
Bachmair, Leo, and Dershowitz, Nachum, 1994. Equational inference, canonical
proofs, and proof orderings. Journal of the ACM 41, 2, pp. 236-276.
Boyer, R.S., and Moore, J.S., 1972. The sharing of structure in theorem-proving
programs. Machine Intelligence, 7, pp. 101-116.
Buntine, W.L., and Burckert, H.J., 1994. On solving equations and disequations.
Journal of the ACM 41, 4, pp. 591-629.
Church, A., and Rosser, J.B., 1936. Some properties of conversion. Trans. Amer.
Math. Soc 39, pp. 472-482.
Dershowitz, N., 1982. Applications of the Knuth-Bendix completion procedure.
Proceedings of the Seminaire dlnformatique Theorique, Paris, France, pp. 95-111.
Dershowitz, N., 1987. Termination of rewriting. Journal of Symbolic
Computation 3, 1, pp. 69-116.
Dershowitz, N., and Jouannaud, J.P., 1990. Rewrite systems. In Handbook of
Theoretical Computer Science B: Formal Methods and Semantics, North-Holland,
Amsterdam, chapter 6, pp. 243-320.
Dick, A.J.J, 1991. An introduction to Knuth-Bendix completion. The Computer
Journal 34, 1, pp. 2-15.
Dick, Jeremy, Kalmus, John, and Martin, Ursula, 1990. Automating the Knuth-
Bendix ordering. Acta Informatica 28, pp. 95-119.
94


Epstein, D.B.A., Holt, D.F., and Rees, S.E., 1991. The use of Knuth-Bendix
methods to solve the word problem in automatic groups. Journal of Symbolic
Computation 12, pp. 397-414.
Escalada-Imaz, Gonzalo, and Ghallab, Malik, 1988. A practically efficient and
almost linear unification algorithm. Artificial Intelligence 36, pp. 249-263.
Goguen, Joseph A., 1988. Modular algebraic specification of some basic
geometrical constructions. Artificial Intelligence 37, pp. 123-153.
Hoffmann, Christoph M., and ODonnell, Michael J., 1982. Pattern matching in
trees. Journal of the ACM 29, 1, pp. 68-95.
Hopcroft, J.E., and Ullman, J.D., 1979. Introduction to Automata Theory,
Languages and Computation. Addison-Wesley, New York.
Hsiang, Jieh, 1985. Refutational theorem proving using term-rewriting systems.
Artificial Intelligence 25, pp. 255-300.
Hsiang, Jieh, Kirchner, Helene, Lescanne, Pierre, and Rusinowitch, Michael, 1992.
The term rewriting approach to automated theorem proving. Journal of Logic
Programming 14, pp. 71-99.
Huet, G., 1976. Resolution dequations dans les langages dordre 1, 2, ..., co.
Ph.D. dissertation. University of Paris VII, France.
Huet, G., 1980. Confluent reductions: abstract properties and applications to term
rewriting systems. Journal of the ACM 27, 4, pp. 797-821.
Huet, G., 1981. A complete proof of correctness of the Knuth and Bendix
completion algorithm. Journal of Computer and System Sciences 25, pp. 11-21.
Huet, G., and Oppen, D.C., 1980. Equations and rewrite rules: A survey in. In
Formal Languages; Perspective and Open Problems. R. Book, ed. Academic
Press, Orlando, Florida.
Hussmann, Heinrich, 1992. Nondeterministic algebraic specifications and
nonconfluent term rewriting. Journal of Logic Programming 12, pp. 237-255.
Klop, J.W., 1980. Combinatory Reduction Systems. PhD thesis, Mathematishch
Centrum Amsterdam.
95


Klop, J.W., 1987. Term rewriting systems: a tutorial. Bull. European Assoc.
Theoret. Computer. Science 32, pp. 143-183.
Knight, Kevin, 1989. Unification: a multidisciplinary survey. ACM Computing
Surveys 21, 1, pp. 93-124.
Knuth, Donald E., and Bendix, Peter B., 1970. Simple word problems in universal
algebras. In Computational Problems in Abstract Algebra, J. Leech, ed., Pergamon
Press, Oxford, U.K., pp. 263-297.
Lalement, R., 1993. Computation as Logic. Prentice Hall, Englewood Cliffs, N.J.
Lescanne, Pierre, 1990. On the recursive decomposition ordering with
lexicographical status and other related orderings. Journal of Automated Reasoning
6, pp. 39-49.
Martelli, A., and Montanari, U., 1982. An efficient unification algorithm. ACM
Trans. Program Languages and Systems 4, 2, pp. 258-282.
Meseguer, J., Goguen, J.A., and Smolka, G., 1989. Order-sorted unification.
Journal of Symbolic Computation 8, 4, pp. 383-414.
Newman, M.H.A., 1942. On theories with a combinatorial definition of
equivalence. Ann. Math. 43, 2, pp. 223-243.
ODonnell, Michael J., 1985. Equational Logic as a Programming Language. MIT
Press, Cambridge, MA.
Paterson, M.S., and Wegman, M.N., 1978. Linear unification. Journal of
Computer Sciences 16, pp. 158-167.
Robinson, J.A., 1965. A machine-oriented logic based on the resolution principle.
Journal of the ACM 12, pp. 23-41.
Siekmann, J., 1989. Unification Theory. Journal of Symbolic Computation 7, 3/4,
pp. 207-274.
Steinbach, Joachim, 1993. Simplification orderings: putting them to the test.
Journal of Automated Reasoning 10, pp. 389-397.
Venturini-Zilli, M., 1975. Complexity of the unification algorithm for first-order
expressions. Calcolo 12, 4, pp. 361-372.
96