A Unification Algorithm for GP 2 (Long Version)
Ivaylo Hristakiev∗ and Detlef Plump

arXiv:1705.02171v1 [cs.LO] 5 May 2017

The University of York, UK

Abstract: The graph programming language GP 2 allows to apply sets of rule
schemata (or “attributed” rules) non-deterministically. To analyse conflicts of programs statically, graphs labelled with expressions are overlayed to construct critical
pairs of rule applications. Each overlay induces a system of equations whose solutions represent different conflicts. We present a rule-based unification algorithm for
GP expressions that is terminating, sound and complete. For every input equation,
the algorithm generates a finite set of substitutions. Soundness means that each of
these substitutions solves the input equation. Since GP labels are lists constructed by
concatenation, unification modulo associativity and unit law is required. This problem, which is also known as word unification, is infinitary in general but becomes
finitary due to GP’s rule schema syntax and the assumption that rule schemata are
left-linear. Our unification algorithm is complete in that every solution of an input
equation is an instance of some substitution in the generated set.
Keywords: graph programs, word unification, critical pair analysis

1 Introduction
A common programming pattern in the graph programming language GP 2 [Plu12, BFPR15] is to
apply a set of graph transformation rules as long as possible. To execute such a loop {r1 , . . . , rn }!
on a host graph, in each iteration an applicable rule ri is selected and applied. As rule selection
and rule matching are non-deterministic, different graphs may result from the loop. Thus, if the
programmer wants the loop to implement a function, a static analysis that establishes or refutes
functional behaviour would be desirable.
The above loop is guaranteed to produce a unique result if the rule set {r1 , . . . , rn } is terminating and confluent. However, conventional confluence analysis via critical pairs [Plu05]
assumes rules with constant labels whereas GP employs rule schemata (or “attributed” rules)
whose graphs are labelled with expressions. Confluence of attributed graph transformation rules
has been considered in [HKT02, EEPT06, GLEO12], but we are not aware of algorithms that
check confluence over non-trivial attribute algebras such as GP’s which includes list concatenation and Peano arithmetic. The problem is that one cannot use syntactic unification (as in logic
programming) when constructing critical pairs and checking their joinability, but has to take into
account all equations valid in the attribute algebra.
For example, [HKT02] presents a method of constructing critical pairs in the case where the
equational theory of the attribute algebra is represented by a confluent and terminating term
∗ This author’s work is supported by a PhD scholarship of the UK Engineering and Physical Sciences Research
Council (EPSRC)

1 INTRODUCTION

2

rewriting system. The algorithm first computes normal forms of the attributes of overlayed nodes
and subsequently constructs the most general (syntactic) unifier of the normal forms. This has
been shown to be incomplete [EEPT06, p.198] in that the constructed set of critical pairs need not
represent all possible conflicts. For, the most general unifier produces identical attributes—but it
is necessary to find all substitutions that make attributes equivalent in the algebra’s theory.
Graphs in GP rule schemata are labelled with lists of integer and string expressions, where lists
are constructed by concatenation. In host graphs, list entries must be constant values. Integers
and strings are subtypes of lists in that they represent lists of length one.
As a simple example, consider the program in Figure 1 for calculating shortest distances. The
program expects input graphs with non-negative integers as edge labels, and arbitrary lists as
node labels. There must be a unique marked node (drawn shaded) whose shortest distance to
each reachable node has to be calculated. The rule schemata init and add append distances
main = init; {add, reduce}!
init(x : list)
x
1

⇒

add(x, y : list; m, n : int)
x:0

x:m

1

1

n

y

⇒

2

x:m

n

1

y:m+n
2

reduce(x, y : list; m, n, p : int)
x:m

n

1

y:p
2

⇒

x:m

n

1

y:m+n
2

where m + n < p
Figure 1: A program calculating shortest distances
to the labels of nodes that have not been visited before, while reduce decreases the distance of
nodes that can be reached by a path that is shorter than the current distance.
To construct the conflicts of the rule schemata add and reduce, their left-hand sides are
overlayed. For example, the structure of the left-hand graph of reduce can match the following
structure in two different ways:

Consider a copy of reduce in which the variables have been renamed to x′ , m′ , etc. To match
reduce and its copy differently requires solving the system of equations hx:m =? y′ :p′ , y:p =?
x′ :m′ i. Solutions to these equations should be as general as possible to represent all potential
conflicts resulting from the above overlay. In this simple example, it is clear that the substitution

σ = {x′ 7→ y, m′ 7→ p, y′ 7→ x, p′ 7→ m}
is a most general solution. It gives rise to the following critical pair:1
1

For simplicity, we ignore the condition of reduce.

3
n
x:p+n′
1

n
y:p

n′

2

⇐

1

n
y:p

x:m
n′

⇒

y:m+n

x:m

2

1

n′

2

In general though, equations can arise that have several independent solutions. For example,
the equation hn:x =? y:2i (with n of type int and x,y of type list) has the minimal solutions

σ1 = {x, y 7→ empty, n 7→ 2} and σ2 = {x 7→ z:2, y 7→ n:z}
where empty represents the empty list and z is a list variable.
Seen algebraically, we need to solve equations modulo the associativity and unit laws
AU = {x : (y : z) = (x : y) : z, empty : x = x, x : empty = x}.
This problem is similar to word unification [BS01], which attempts to solve equations modulo
associativity. (Some authors consider AU -unification as word unification, e.g. [Jaf90]). Solvability of word unification is decidable, albeit in PSPACE [Pla99], but there is not always a finite
complete set of solutions. The same holds for AU-unification (see Section 3). Fortunately, GP’s
syntax for left-hand sides of rule schemata forbids labels with more than one list variable. It
turns out that by additionally forbidding shared list variables between different left-hand labels
of a rule, rule overlays induce equation systems possessing finite complete sets of solutions.
This paper is the first step towards a static confluence analysis for GP programs. In Section 3,
we present a rule-based unification algorithm for equations between left-hand expressions of
rule schemata. We show that the algorithm always terminates and that it is sound in that each
substitution generated by the algorithm is an AU-unifier of the input equation. Moreover, the
algorithm is complete in that every unifier of the input equation is an instance of some unifier in
the computed set of solutions.
This paper is an extended version of the workshop paper [HP15].

2 GP Rule Schemata
We refer to [Plu12, BFPR15] for the definition of GP and more example programs. In this section, we define (unconditional) rule schemata which are the “building blocks” of graph programs.
A graph over a label set C is a system G = (V, E, s,t, l, m), where V and E are finite sets of
nodes (or vertices) and edges, s,t : E → V are the source and target functions for edges, l : V → C
is the node labelling function and m : E → C is the edge labelling function. We write G (C ) for
the class of all graphs over C .
Figure 2 shows an example for the declaration of a rule schema. The types int and string
represent integers and character strings. Type atom is the union of int and string, and list
represents lists of atoms. Given lists l1 and l2 , we write l1 : l2 for the concatenation of l1 and l2 .
The empty list is denoted by empty. In pictures of graphs, nodes or edges without label (such as
the dashed edge in Figure 2) are implicitly labelled with the empty list. We equate lists of length
one with their entry to obtain the syntactic and semantic subtype relationships shown in Figure 3.
For example, all labels in Figure 2 are list expressions.
Figure 4 gives a grammar in Extended Backus-Naur Form defining the abstract syntax of
labels. The function length return the length of a variable, while indeg and outdeg access
the indegree resp. outdegree of a left-hand node in the host graph.

2 GP RULE SCHEMATA

4
bridge(x, y : list; a : atom; n : int; s, t : string)

a:x

s

t

n

1

y

2

3

⇒

s

a

x:n

1

t

2

n∗n
3

Figure 2: Declaration of a GP rule schema

Figure 4 defines four syntactic categories of expressions: Integer, String, Atom and List, where
Integer and String are subsets of Atom which in turn is a subset of List. Category Node is the
set of node identifiers used in rule schemata. Moreover, IVar, SVar, AVar and LVar are the sets of
variables of type int, string, atom and list. We assume that these sets are disjoint and define
Var = IVar ∪ SVar ∪ AVar ∪ LVar. The mark components of labels are represented graphically
rather than textually.
Each expression l has a unique smallest type, denoted by type(l), which can be read off the
(Z ∪ Char∗ )∗

⊆

⊆

list
atom

Z ∪ Char∗

⊆

⊆

⊇

⊇

Char∗
⊆

Z

⊆

string

int

char

Char

Figure 3: Subtype hierarchy for labels
Integer

::=

ArithOp
String
Atom
List
Label
Mark

::=
::=
::=
::=
::=
::=

Digit {Digit} | IVar
| ‘−’ Integer | Integer ArithOp Integer
| length ‘(’ LVar | AVar | SVar ‘)’
| (indeg | outdeg) ‘(’ Node ‘)’
‘+’ | ‘-’ | ‘∗’ | ‘/’
‘ “ ’ {Char} ‘ ” ’ | SVar | String ‘.’ String
Integer | String | AVar
empty | Atom | LVar | List ‘:’ List
List [Mark]
red | green | blue | grey | dashed | any

Figure 4: Abstract syntax of rule schema labels

5
hierarchy in Figure 3 after l has been normalised with the rewrite rules shown at the beginning of
Subsection 3.2. We write type(l1 ) < type(l2 ) or type(l1 ) ≤ type(l2 ) to compare types according
to the subtype hierarchy. If the types of l1 and l2 are incomparable, we write type(l1 ) k type(l2 ).
The values of rule schema variables at execution time are determined by graph matching. To
ensure that matches induce unique “actual parameters”, expressions in the left graph of a rule
schema must have a simple shape.
Definition 1 (Simple expression) A simple expression contains no arithmetic operators, no
length or degree operators, no string concatenation, and at most one occurrence of a list variable.
In other words, simple expressions contain no unary or binary operators except list concatenation, and at most one occurrence of a list variable. For example, given the variable declarations
of Figure 2, a:x and y:n:n are simple expressions whereas n ∗ 2 or x:y are not simple.
Our definition of simple expressions is more restrictive than that in [Plu12] because we exclude
string concatenation and the unary minus. These operations (especially string concatenation)
would considerably inflate the unification algorithm and its completeness proof, without posing
a substantial challenge.
Definition 2 (Rule schema) A rule schema hL, R, Ii consists of graphs L, R in G (Label) and
a set I, the interface, such that I = VL ∩ VR . All labels in L must be simple and all variables
occurring in R must also occur in L.
When a rule schema is graphically declared, as in Figure 2, the interface I is represented by
the node numbers in L and R. Nodes without numbers in L are to be deleted and nodes without
numbers in R are to be created. All variables in R have to occur in L so that for a given match of
L in a host graph, applying the rule schema produces a graph that is unique up to isomorphism.
Assumption 1 (Left-linearity). We assume that rule schemata hL, R, Ii are left-linear, that is, the
labels of different nodes or edges in L do not contain the same list variable.
This assumption is necessary to ensure that the solutions of the equations resulting from overlaying two rule schemata can be represented by a finite set of unifiers. For example, without
this assumption it is easy to construct two rule schemata that induce the system of equations
hx : 1 =? y, y =? 1 : xi. This system has solutions {x 7→ empty, y 7→ 1}, {x 7→ 1, y 7→ 1 : 1},
{x 7→ 1 : 1, y 7→ 1 : 1 : 1}, . . . which form a infnite, minimal and compete set of solutions (See
Definition 5 below).

3 Unification
We start with introducing some technical notions such as substitutions, unification problems and
complete sets of unifiers. Then, in Subsection 3.2, we present our unification algorithm. In
Subsection 3.3, we prove that the algorithm terminates and is sound.

3 UNIFICATION

6

3.1 Preliminaries
A substitution is a family of mappings σ = (σX )X∈{I,S,A,L} where σI : IVar → Integer, σS : SVar →
String, σA : AVar → Atom, σL : LVar → List. Here Integer, String, Atom and List are the sets of
expressions defined by the GP label grammar of Figure 4. For example, if z ∈ LVar, x ∈ IVar
and y ∈ SVar, then we write σ = {x 7→ x + 1, z 7→ y : −x : y} for the substitution that maps x to
x + 1, z to y : −x : y and every other variable to itself.
Applying a substitution σ to an expression t, denoted by t σ , means to replace every variable
x in t by σ (x) simultaneously. In the above example, (z : −x)σ = y : −x : y : −(x + 1).
By Dom(σ ) we denote the set {x ∈ Var | σ (x) 6= x} and by VRan(σ ) the set of variables occurring in the expressions {σ (x) | x ∈ Var}. A substitution σ is idempotent (
if Dom(σ ) ∩ VRan(σ ) = 0.
/
(xσ )θ if x ∈ Dom(σ )
The composition of two substitutions σ and θ , is defined as x(σ ◦ θ ) =
otherwise
xθ
and is an associative operation.
Definition 3 (Unification problem)
tution

A unification problem is a pair of an equation and a substi-

P = hs =? t, σP i
where s and t are simple list expressions without common variables.
The symbol =? signifies that the equation must be solved rather than having to hold for all
values of variables. The purpose of σP is for the unification algorithm (Section 3.2) to record a
partial solution. An illustration of this concept will be seen in Figure 8.
In Section 2, we already assumed that GP rule schemata need to be left-linear. Now, the problem of solving a system of equations {s1 = t1 , s2 = t2 } can be broken down to solving individual
equations and combining the answers - if σ1 and σ2 are solutions to each individual equation,
then σ1 ∪ σ2 is a solution to the combined problem as σ1 and σ2 do not share variables.
Consider the equational axioms for associativity and unity,
AU = {x : (y : z) = (x : y) : z, empty : x = x, x : empty = x}
where x, y, z are variables of type list, and let =AU be the equivalence relation on expressions
generated by these axioms.
Definition 4 (Unifier)
tution θ such that

Given a unification problem P = hs =? t, σP i a unifier of P a is a substi-

sθ =AU t θ and xi θ =AU ti θ
for each binding {xi 7→ ti } in σP .
The set of all unifiers of P is denoted by U (P). We say that P is unifiable if U (P) 6= 0.
/
The special unification problem fail represents failure and has no unifiers. A problem
P = hs =? t, ∅i is initial and P = h∅, σP i is solved.

3.2 Unification Algorithm

7

A substitution σ is more general on a set of variables X than a substitution θ if there exists a
substitution λ such that xθ =AU xσ λ for all x ∈ X . In this case we write σ ≦X θ and say that
θ is an instance of σ on X . Substitutions σ and θ are equivalent on X , denoted by σ =X θ , if
σ ≦X θ and θ ≦X σ .
Definition 5 (Complete set of unifiers [Plo72]) A set C of substitutions is a complete set of
unifiers of a unification problem P if
1. (Soundness) C ⊆ U (P), that is, each substitution in C is a unifier of P, and
2. (Completeness) for each θ ∈ U (P) there exists σ ∈ C such that σ ≦X θ , where X = Var(P)
is the set of variables occurring in P.
Set C is also minimal if each pair of distinct unifiers in C are incomparable with respect to ≦X .
If a unification problem P is not unifiable, then the empty set ∅ is a minimal complete set of
unifiers of P.
For simplicity, we replace =? with = in unification problems from now on.
Example 1 The minimal complete set of unifiers of the problem ha : x = y : 2i (where a is an
atom variable and x,y are list variables) is {σ1 , σ2 } with

σ1 = {a 7→ 2, x 7→ empty, y 7→ empty} and σ2 = {x 7→ z : 2, y 7→ a : z}.
We have σ1 (a : x) = 2 : empty =AU 2 =AU empty : 2 = σ1 (y : 2) and σ2 (a : x) = a : z : 2 =
σ2 (y : 2). Other unifiers such as σ3 = {x 7→ 2, y 7→ a} are instances of σ2 .

3.2 Unification Algorithm
We start with some notational conventions for the rest of this section:
• L, M stand for simple expressions,
• x, y, z stand for variables of any type (unless otherwise specified),
• a, b stand for
(i) simple string or integer expressions, or
(ii) string, integer or atom variables
• s, t stand for
(i) simple string or integer expressions, or
(ii) variables of any type

3 UNIFICATION

8

Preprocessing. Given a unification problem P = hs =? t, σ i, we rewrite the terms in s and t
using the reduction rules
L : empty → L and

empty : L → L

where L ranges over list expressions. These reduction rules are applied exhaustively before any
of the transformation rules. For example,
x : empty : 1 : empty → x : 1 : empty → x : 1.
We call this process normalization. In addition, the rules are applied to each instance of a transformation rule (that is, once the formal parameters have been replaced with actual parameters)
before it is applied, and also after each transformation rule application.
Transformation rules. Figure 5 shows the transformation rules, the essence of our approach,
in an inference system style where each rule consists of a premise and a conclusion.
Remove:
Decomp1:
Decomp1’:
Decomp2/2’:
Decomp3:
Decomp4:
Subst1:
Subst2:
Subst3:
Orient1/2:
Orient3:
Orient4:

deletes trivial equations
syntactically equates a list variable with an atom expression or
list variable
syntactically equates an atom variable with an expression of
lesser type
assigns a list variable to start with another list variable
removes identical symbols from the head
solves an atom variable
solves a variable
assigns empty to a list variable
assigns an atom prefix to a list variable
moves variables to left-hand side
moves variables of larger type to left-hand side
moves a list variable to the left-hand side

The rules induce a transformation relation ⇒ on unification problems. In order to apply any
of the rules to a problem P, the problem part of its premise needs to be matched onto P. Subsequently, the boolean condition of the premise is checked and the rule instance is normalized so
that its premise is identical to P.
For example, the rule Orient3 can be matched to P = ha : 2 = m, σ i (where a and m are variables
of type atom and list, respectively) by setting y 7→ a, x 7→ m, M 7→ 2, and L 7→ empty. The rule
instance and its normal form are then
ha : 2 = m : empty, σ i
hm : empty = a : 2, σ i

and

ha : 2 = m, σ i
hm = a : 2, σ i

where the conclusion of the normal form is the result of applying Orient3 to P.

3.2 Unification Algorithm

9

hL = L, σ i
Remove
h∅, σ i
hx : L = s : M, σ i L 6= empty type(x) = list
Decomp1
hL = M, σ ◦ {x 7→ s}i
hx : L = a : M, σ i L 6= empty type(a) ≤ type(x) ≤ atom
Decomp1′
h(L = M){x 7→ a}, σ ◦ {x 7→ a}i
hx : L = y : M, σ i L 6= empty type(x) = list type(y) = list x′ is a fresh list variable
Decomp2
hx′ : L = M, σ ◦ {x 7→ y : x′ }i
hx : L = y : M, σ i L 6= empty type(x) = list type(y) = list y′ is a fresh list variable
Decomp2′
hL = y′ : M, σ ◦ {y 7→ x : y′ }i

hs : L = s : M, σ i
Decomp3
hL = M, σ i

hx = a : y, σ i type(x) = atom type(y) = list
Decomp4
hempty = y, σ ◦ {x 7→ a}i

/ Var(L) type(x) ≥ type(L)
hx = L, σ i x ∈
Subst1
h∅, σ ◦ {x 7→ L}i
hx : L = M, σ i L 6= empty type(x) = list
Subst2
hL = M, σ ◦ {x 7→ empty}i
hx : L = a : M}, σ i L 6= empty x′ is a fresh list variable
hx′ : L = M, σ ◦ {x 7→ a : x′ }i

type(x) = list

Subst3

ha : M = x : L, σ i a is not a variable
Orient1
hx : L = a : M, σ i
hx : L = y, σ i L 6= empty type(x) = type(y)
Orient2
hy = x : L, σ i

hy : M = x : L, σ i type(y) < type(x)
Orient3
hx : L = y : M, σ i

hempty = x : L, σ i type(x) = list
Orient4
hx : L = empty, σ i

Figure 5: Transformation rules

3 UNIFICATION

10

hx = L, σ i x ∈ Var(L)

x 6= L
fail

type(x) = list

Occur

ha : L = b : M, σ i a 6= b Var(a) = 0/ = Var(b)
Clash1
fail

ha : L = empty, σ i
Clash2
fail
hempty = a : L, σ i
Clash3
fail

hx = L, σ i type(x) k type(L)
Clash4
fail
Figure 6: Failure rules

Showing that a unification problem has no solution can be a lengthy affair because we need
to compute all normal forms with respect to ⇒. Instead, the rules Occur and Clash1 to Clash4,
shown in Figure 6, introduce failure. Failure cuts off parts of the search tree for a given problem
P. This is because if P ⇒ fail, then P has no unifiers and it is not necessary to compute another
normal form. Effectively, the failure rules have precedence over the other rules. They are justified
by the following lemmata.
Lemma 1 A normalised equation x = L with x 6= L has no solution if L is a simple expression,
x ∈ Var(L) and type(x) = list.
Proof. Since x ∈ Var(L) and x 6= L, L is of the form s1 : s2 : . . . : sn with n ≥ 2 and x ∈ Var(si )
for some 1 ≤ i ≤ n. As L is normalised, none of the terms si contains the constant empty.
Also, since L is simple, it contains no list variables other than x and x is not repeated. It follows
σ (x) 6=AU σ (L) for every substitution σ .
Lemma 2 Equations of the form a : L = empty or empty = a : L have no solution if a is an
atom expression.
Lemma 3 An equation a : L = b : M with a 6= b has no solution if a and b are atom expressions
without variables.
The algorithm. The unification algorithm in Figure 7 starts by normalizing the input equation,
as explained above. It uses a queue of unification problems to search the derivation tree of P
with respect to ⇒ in a breadth-first manner. The first step is to put the normalized problem P on
the queue.
The variable next holds the head of the queue. If next is in the form h∅, σ i, then σ is a
unifier of the original problem and is added to the set U of solutions. Otherwise, the next step is
to construct all problems P′ such that next ⇒ P′ . If P′ is fail, then the derivation tree below
next is ignored, otherwise P′ gets normalized and enqueued.

3.3 Termination and Soundness
Unify(P) :

11

U := 0/
create empty queue Q of unification problems
normalize P
Q.enqueue(hP, ∅i)
while Q is not empty
next := Q.dequeue()
if next is in the form h∅, σ i
U := U ∪ {σ }
else if next ; fail
foreach P′ such that next ⇒ P′
normalize P′
Q.enqueue(P′)
end foreach
end if
end if
end while
return U
Figure 7: Unification algorithm

An example tree traversed by the algorithm is shown in Figure 8. Nodes are labelled with
unification problems and edges represent applications of transformation rules. The root of the
tree is the problem hy : 2 = a : xi to which the rules Decomp1, Subst2 and Subst3 can be applied.
The three resulting problems form the second level of the search tree and are processed in turn.
Eventually, the unifiers

σ1 = {x 7→ 2, y 7→ a}
σ2 = {x 7→ y′ : 2, y 7→ a : y′ }
σ3 = {a →
7 2, x 7→ empty, y 7→ empty}
are found, which represent a complete set of unifiers of the initial problem. Note that the set is
not minimal because σ1 is an instance of σ2 .
The algorithm is similar to the A-unification (word unification) algorithm presented in [Sch92]
which looks at the head of the problem equation. That algorithm terminates for the special case
that the input problem has no repeated variables, and is sound and complete. Our approach can
be seen as an extension from A-unification to AU-unification, to handle the unit equations, and
presented in the rule-based style of [BS01]. In addition, our algorithm deals with GP’s subtype
system.

3.3 Termination and Soundness
We show that the unification algorithm terminates if the input problem contains no repeated list
variables, where termination of the algorithm follows from termination of the relation ⇒.

3 UNIFICATION

12


Decomp1



2=x
y 7→ a



x=2
y 7→ a



Subst2


2=a:x
y 7→ empty

Subst3



Subst1




 ∅
y 7→ a


x 7→ 2
solved



y′ : 2 = x
y 7→ a : y′





Orient1

Orient1



y:2=a:x
∅

′

Decomp2 Decomp2

Orient2

a:x=2
y 7→ empty



Decomp1′



y′

x= :2
y 7→ a : y′





y′′

: 2 = empty
y 7→ a : x : y′′

Subst1


  ∅



x
=
empty


′
y 7→ a : y
y 7→ empty

  x→

7 y′ : 2
a 7→ 2
solved
Subst1


∅



y 7→ empty
a 7→ 2



x 7→ empty
solved









Figure 8: Unification example



Subst2



2 = empty
y 7→ a : x



Clash2
fail






 2 = x′
′
y 7→ a : y


x 7→ y′ : x′
Orient1

 ′

 x =2
y 7→ a : y′


x 7→ y′ : x′
Subst1




 ∅
y 7→ a : y′


x 7→ y′ : 2
solved

3.3 Termination and Soundness

13

Theorem 1 (Termination) If P is a unification problem without repeated list variables, then
there is no infinite sequence P ⇒ P1 ⇒ P2 ⇒ . . .
Proof. Define the size |L| of an expression L by
• 0 if L = empty,
• 1 if L is an expression of category Atom (see Figure 4) or a list variable,
• |M| + |N| + 1 if L = M : N.
We define a lexicographic termination order by assigning to a unification problem P = hL =
M, σ i the tuple (n1 , n2 , n3 , n4 ), where
• n1 is the size of P, that is, n1 = |L| + |M|;
(
0 if L starts with a variable
• n2 =
1 otherwise
(
1 if type(x) > type(y)
• n3 =
0 otherwise
where x and y are the starting symbols of L and M
• n4 = |L|
The table in Figure 9 shows that for each transformation step P ⇒ P′ , the tuple associated with
P′ is strictly smaller than the tuple associated with P in the lexicographic order induced by the
components n1 to n4 .
Subst1 − 3
Decomp1 − 4
Remove
Orient1
Orient4
Orient3
Orient2

n1 n2 n3 n4
>
>
>
= >
= >
= = >
= = = >

Figure 9: Lexicographic termination order

For most rules, the table entries are easy to check. All the rules except for Orient decrease the
size of the input equation s =? t. The Orient rules keep the size equal, but move variables and
expressions of a bigger type to the left-hand side.

3 UNIFICATION

14
Lemma 4

If P ⇒ P′ , then U (P) ⊇ U (P′ ) .

Proof. We show that for each transformation rule, a unifier θ of the conclusion unifies the
premise.
Note that for Remove, Decomp3 and Orient1-4, we have that σP′ = σP .
• Remove
θ ∈ U (h∅, σP′ i)

⇐⇒
⇐⇒
⇐⇒

θ ∈ U (h∅, σP i)
θ ∈ U (h∅, σP i) ∧ Lθ = Lθ
θ ∈ U (hL = L, σP i)

• Decomp3

θ ∈ U (hL = M, σP′ i)

⇐⇒
⇐⇒
⇐⇒

θ ∈ U (hL = M, σP i)
θ ∈ U (hL = M, σP i) ∧ sθ = sθ
θ ∈ U (hs : L = s : M, σP i)

• Decomp1 - We have xθ = sθ and Lθ = M θ .
Then (x : L)θ = (s : L)θ = (s : M)θ as required.
• Decomp1’ - We have xθ = aθ and Lθ = M θ .
Then (x : L)θ = (a : L)θ = (a : M)θ as required.
• Decomp2 - We have xθ = (y : x′ )θ and (x′ : L)θ = M θ .
Then (x : L)θ = (y : x′ : L)θ = (y : M)θ as required.
• Decomp2’ - We have yθ = (x : y′ )θ and Lθ = (y′ : M)θ .
Then (y : M)θ = (x : y′ : M)θ = (x : L)θ as required.
• Decomp4 - We have xθ = aθ and yθ = (empty)θ = empty.
Then (a : y)θ = (x : y)θ = (x : empty)θ = xθ as required.
• Subst1 - We have xθ = Lθ
θ ∈ U (h∅, σS′ i) ⇐⇒ θ ∈ U (h∅, σS ◦ (x 7→ L)i)
⇐⇒ θ ∈ U (h∅, σS ◦ (x 7→ L)i) ∧ xθ = Lθ
⇐⇒ θ ∈ U (hx = L, σS i)
• Subst2 - We have xθ = (empty)θ and Lθ = M θ .
Then (x : L)θ = (empty : L)θ = Lθ = M θ as required.
• Subst3 - We have xθ = (a : x′ )θ and (x′ : L)θ = M θ .
Then (x : L)θ = (a : x′ : L)θ = (a : M)θ as required.
• Orient1-4 - Since =AU is an equivalence relation and hence symmetric, a unifier of the
conclusion is also a unifier of the premise.

3.4 Completeness

Theorem 2 (Soundness)
P.

15

If P ⇒+ P′ with P′ = h∅, σP′ i in solved form, then σP′ is a unifier of

Proof. We have that σP′ is a unifier of P′ by definition. A simple induction with Lemma 4 shows
that σP′ must be a unifier of P.

3.4 Completeness
In order to prove that our algorithm is complete, by Definition 5 we have to show that for any
unifier δ , there is a unifier in our solution set that is more general.
Our proof involves using a selector algorithm that takes a unification problem hs =? ti together
with an arbitrary unifier δ , and outputs a path of the unification tree associated with a more
general unifier than δ . This is very similar to [Sie78] where completeness of a A-unification
algorithm is shown via such selector.
Lemma 5 (Selector Lemma) There exists an algorithm Select(δ , s =? t) that takes an equation
s =? t and a unifier δ as input and produces a sequence of selections B = (b1 , . . . , bk ) such that:
• Unify(s =? t) has a path specified by B .
• For all selections b ∈ B: if σ is the substitution corresponding to b, then there exists an
instantiation λ such that σ ◦ λ ≤ δ .
For the selector algorithm and proof see Section 4.
For example, consider the unification problem hy : 2 = a : xi and δ = (x 7→ 1 : 2, y 7→ a : 1)
as a unifier. The unification tree was shown in Figure 8. Select(δ , y : 2 = a : x) would produce
selections (Subst3, Decomp2’, Orient1, Subst1), which corresponds to the right-most path in the
tree. The unifier at the end of this path is σ = (x 7→ y′ : 2, y 7→ a : y′ ) which is more general
than δ by instantiation λ = (y′ 7→ 1).
Now we are able to state our completeness result, which follows directly from Lemma 5.
Theorem 3 (Completeness) For every unifier δ of a unification problem hs =? ti, there exist a
unifier σ generated by Unify such that σ ≤ δ .

4 Proving Completeness: The Select Algorithm
As already stated, the Select algorithm takes a unification problem s =? t together with a unifier
δ , and outputs a path of the unification tree associated with a unifier that is at least as general δ .
The algorithm itself is presented below, together with several examples of how it works. Afterwards, we are able to prove the Selector Lemma meaning that Select is correct w.r.t. Unify.
Preprocessing Preprocessing of the problem s = t w.r.t. a unifier δ involves expanding each
variable to the correct number of symbols, i.e. x → x1 : . . . : xn where n = |xδ | .

4 PROVING COMPLETENESS: THE SELECT ALGORITHM

16

Call x the parent symbol of x1 , . . . , xn , and the expanded strings s and t.
Furthermore, for each binding {x 7→ empty} in δ , replace x with xe in s̄ and t̄. When Select
sees such an empty list variable, it will be able to select Subst2.
Also, pad the shorter string with extra empty symbols to make s̄ and t̄ of equal length.
For example, the problem a : x = y : b has unifier δ = (x 7→ acb, y 7→ acb) and the expansion
would transform it into a : x1 : x2 : x3 = y1 : y2 : y3 : b where each ”pseudo”-variable can hold
exactly one symbol.
The expanded s̄ and t̄ can be represented graphically as the diagram below:
m
a

x1

x2

x3 s̄

y2

y3

b

n
y1

t̄

Predicates
• A basic look-ahead is implemented as a predicate L(s, k) that returns the number of adjacent ”pseudo”-variables of sk to the right of sk . If sk has no ”pseudo”-variables or a
constant then L(s, k) = 0.
For example, for the above strings:
L(s, 1) = 0
L(s, 2) = 2
L(s, 3) = 1
L(s, 4) = 0

a is a constant
after x1 there is x2 and x3
after x2 there is x3
after x3 there is no x4

L(t, 1) = 2
L(t, 2) = 1
L(t, 3) = 0
L(t, 4) = 0

after y1 there is y2 and y3
after y2 there is y3
after y3 there is no y4
b is a constant

This predicate is really only useful for list variables.
• Another predicate
Type(< string >, < pos >) → {ListVar, AtomVar, AtomExpr, EmptyListVar, empty}
returns the type of the symbol of < string > at position < pos >.
For example for the string s = a : ”a” : xe : y : empty
Type(s, 1) = AtomVar
Type(s, 2) = AtomExpr
Type(s, 3) = EmptyListVar
Type(s, 4) = ListVar
Type(s, 5) = empty

17
• Another predicate
LookAhead(< string >, < pos >) → {true, f alse}
determines if the word after the given symbol (or sequence of ”pseudo”-variables when
Type(< string >, < pos >) = ListVar) is not the empty constant (or the blank symbol ∆
at the end of the preprocessed string).
For example for the string s = x1 : x2 : a
LookAhead(s, 1) = true
LookAhead(s, 2) = true
LookAhead(s, 3) = f alse

because of a
because of a
because at end of string

The Select Algorithm
The algorithm is essentially a 3-tape TM with look-ahead. The head looks at both input tapes
simultaneously (the ”head” of the current problem) as defined by pointers m and n, and can move
each pointer separately and only to the right.
It starts with preprocessing the input problem as explained above. Depending on the predicate
values at m and n, specific selections are recorded and pointers are updated. This is repeated
until the pointers both reach the end of the input strings.
Select (s,t, δ ) → B :
Preprocess(s,t, δ ) → s,t
m = 1, n = 1 // the head position
B = ”” // initial selection
if m > length(s) and n > length(t) return B
Case analysis on L(s, m) and L(t, n):
Case 1. L(s, m) < L(t, n)
Since L(t, n) > 0, tn must be a list variable
Do subcase analysis on type of sm and look ahead results
Case 1.1. Type(sm ) = ListVar /* x : L = y : M */
/* It cannot be the case that the LookAhead(sm ) returns f alse (i.e. L 6= empty) as tn is not of
type EmptyListVar (L(tn ) > 0) */
select Decomp2’ /* x : L = y : M with L 6= empty */
m = m + 1 + L(sm), n = n + 1 + L(sm ) /* move head to end of shorter substring */
Case 1.2. Type(sm ) = AtomVar /* a : L = y : M */
select Orient3, swap input tapes and pointers
Case 1.3. Type(sm ) = AtomExpr /* a : L = y : M */
select Orient1, swap input tapes and pointers
Case 1.4. Type(sm ) = EmptyListVar /* xe : L = y : M */
/* It cannot be the case that the LookAhead(sm ) returns f alse (i.e. L 6= empty) as tn is not of
type EmptyListVar (L(tn ) > 0) */
select Subst2, m++, no change for n

18

4 PROVING COMPLETENESS: THE SELECT ALGORITHM

Case 1.5. Type(sm ) = empty
/* cannot happen, as tn is not of type EmptyListVar (L(tn ) > 0) and δ is a unifier */
Case 2. L(s, m) > L(t, n)
Since L(s, m) > 0, sm must be a list variable
if LookAhead(sm ) = f alse
then (Case 2.1)
select Subst1 /* x = y : M */
m = m + 1 + L(sm), n = length(t) + 1 /* move head to end of both strings */
else /* L 6= empty */
Case 2.2. Type(tn ) = ListVar
select Decomp2 /* x : L = y : M with L 6= M and x should start with y */
m = m + 1 + L(tn), n = n + 1 + L(tn ) /* move head to end of shorter substring */
Case 2.3. Type(tn ) = AtomVar or AtomExpr
select Subst3 /* x : L = a : M with L 6= M and x should start with a */
m++, n++
Case 2.4. Type(tn ) = EmptyListVar
select Decomp2 /* x : L = ye : M with L 6= M and x should start with y */
m++, n++
Case 2.5. Type(tn ) = empty
/* cannot happen, same reason as 1.5 */
Case 3. L(s, m) = L(t, n)
Case 3.1. L(s, m) = L(t, n) > 0
Both sm and t n must be list variables
if LookAhead(sm ) = f alse
select Subst1 /* x = y : M */
m = m + 1 + L(sm), n = length(t) + 1 /* move head to end of both strings */
else /* L 6= empty */
select Decomp1 /* x : L = y : M */
m = m + 1 + L(sm ), n = n + 1 + L(sm ) /* move head to next pair of unrelated symbols */
Case 3.2. L(s, m) = L(t, n) = 0
/* This is the largest subcase because sm and tn can be of any of the possible types. */
Do case analysis on Type(sm ) and Type(t n ):
3.2.1. (ListVar, ListVar) – same as 3.1
3.2.2. (ListVar, AtomVar) – same as 3.1
3.2.3. (ListVar, AtomExpr) – same as 3.1
3.2.4. (ListVar, EmptyListVar) – same as 2.4
3.2.5. (ListVar, empty) – cannot happen as δ is a unifier
3.2.6. (AtomVar, ListVar) – Orient3 (like 1.2)
3.2.7-8 (AtomVar, AtomVar) or (AtomVar, AtomExpr)

19
if LookAhead(sm ) = f alse
if LookAhead(tn ) = f alse
select Subst1 /* a = b */
m++, n++ /* move head to end of both strings */
else
select Decomp4 /* a = b : y with δ (y) = empty */
m++, n++ /* move head to next pair of unrelated symbols */
else /* L 6= empty */
select Decomp1’ /* a : L = b : M */
m++, n++ /* move head to next pair of unrelated symbols */
3.2.9. (AtomVar, EmptyListVar) – same as 1.2
3.2.10. (AtomVar, empty) /* cannot happen due to failure lemmata */
3.2.11. (AtomExpr, ListVar) – same as 1.3
3.2.12. (AtomExpr, AtomVar) – same as 1.3
3.2.13. (AtomExpr, AtomExpr) –
/* must be the same expression due to not considering the subunification algorithm for StringChar */
select Decomp3, m++, n++
3.2.14. (AtomExpr, EmptyListVar) – same as 1.3
3.2.15. (AtomExpr, empty) – /* cannot happen due to failure lemmata */
3.2.16-18. (EmptyListVar, ListVar) or (EmptyListVar, AtomVar) or (EmptyListVar, AtomExpr)
/* It must be the case that there is something following sm for δ to be a unifier. */
select Subst2, m++ (like 1.4)
3.2.19. (EmptyListVar, EmptyListVar) – same as 3.1
3.2.20. (EmptyListVar, empty) – select Subst1, m++, n = length(tn ) + 1
3.2.21. (empty, ListVar) /* cannot happen as δ is a unifier */
3.2.22 & 3.2.23 (empty, AtomVar) or (empty, AtomExpr) /* cannot happen due to failure
lemmata */
3.2.24. (empty, EmptyListVar) – select Orient4, swap tapes and pointers
3.2.25. (empty, empty) select Remove /* nothing left to solve */

Examples Below are some examples of how the algorithm behaves when presented with a
unification problem and a unifier.
The first two examples are of the problem P = hy : 2 =? a : xi, with its unification tree already
shown in Figure 8. The third example is of the problem P = hn =? y : ni that has a single most
general unifier σ = {y 7→ empty}.
Example 2
P = hy : 2 =? a : xi

δ = {a 7→ 2, x 7→ empty, y 7→ empty}

4 PROVING COMPLETENESS: THE SELECT ALGORITHM

20
m=1

m=2

ye

2

∆

2

∆

→ n=1

n=1
a

ye

s̄

m=1

xe

∆

a

t̄

→
xe

∆

xe

a

s̄

∆

ye

s̄

a

xe

∆

→

n=2

t̄

m=3

m=2

∆

2

select Decomp1’
select Subst2
select Orient1
m++,n++
swap tapes & pointers
m++
(case 3.2.12)
(case 3.2.8)
(case 3.2.17)

t̄

ye

s̄

2

n=3 →
ye

∆

2

xe

a

t̄

select Subst1
m++, n = 3
(case 3.2.20)

end

P = hy : 2 =? a : xi

δ = {x 7→ a : 1, y 7→ 1 : 2}

y1

y2

∆

2

y1

s̄
→

n=1
a

n=3

m=2

x1

x2

∆

y2

2

∆

a

x1

x2

∆

select Decomp2’
m + +, n + +
(case 2.1)

select Subst3
m + +, n + +
(case 2.3)

y2

→

n=2

t̄

y1

s̄

t̄

x1

→

x2

y2

2

select Subst1
m + +, n + +
(case 3.2.3)

a

x1

x2

∆

t̄

select Orient1
swap tapes & pointers
(case 3.2.11)

∆

y1

s̄

y2

2

→
∆

t̄

∆

s̄

n=4
a

x1

end

Example 4
P = hn =? y : ni

→

m=4

n=3
y1

s̄

m=3

m=3
a

∆

2

δ = {y 7→ empty}

x2

∆

s̄

n=3

Example 3

m=1

∆

t̄

∆

t̄

21
m=1
n

m=1
e

∆

ye

n

∆

→ n=1

n=1
ye

s̄

n

∆

t̄

n

m=3

m=2

s̄

ye

n

∆

→ n=1
e

∆

select Subst2
select Orient3
swap tapes & pointers
m++
(case 3.2.9)
(case 3.2.17)

t̄

n

s̄

ye

→
e

∆

select Subst1
m++,n++
(case 3.2.7)

t̄

n

∆

s̄

∆

t̄

n=2
n

e

end

Lemma 5 (Selector Lemma) Let B be the sequence of selections defined by Select(δ , s =? t)
where δ (s) = δ (t)
1) Unify(s =? t) has a path specified by B .
2) For all selections b ∈ B:
• 2.1) the symbols examined by Unify at b are parent symbols of the symbols Select sees at
head position (m, n) for selection b
• 2.2) if σ is the substitution corresponding to selection b, then σ ≤ δ , i.e. exist substitution
λ such that σ ◦ λ ⊆ δ
Proof. By induction on the number of the selections (b1 , b2 , . . .) of B
Base Case The initial selection b1 of Select is based on the first symbols of s and t as this is the
initial head position (m and n are initialized to 1). The transformation rules of Unify also examine
the head of the initial problem. Also, Select does not throw away list variables that should be
removed due to Subst2, so condition 2.1) is trivially satisfied. For 2.2), σ1 = ∅ by definition of
initial unification problem, and let λ1 = ∅. Therefore σ1 ◦ λ1 = ∅ ⊆ δ as required.
Hypothesis Assume the statements of the theorem are true for selection bk with a corresponding node in the unification tree hPk , σk i and let (m, n) be the head position of Select before
outputting selection bk+1 .
2.1) the symbols at the head of the problem Pk (x and y) are parent symbols of sm ,t n
2.1) exists substitution λk such that σk ◦ λk ⊆ δ
Inductive case
from bn ,

There are several possible cases for the selection bn+1 . We have to show that

i Unify can generate selection bk+1 (i.e. the selected rule is applicable) and
ii The symbols at the head of the next unification problem Pk+1 (where Pk ⇒ Pk+1 via the rule
bk+1 ) are parent symbols of smnew and t nnew

22

4 PROVING COMPLETENESS: THE SELECT ALGORITHM

iii exists instantiation λn+1 such that σn+1 ◦ λn+1 ⊆ δ
For all Orient rules, we can notice that:
• they do not change the head of the unification problem nor they generate a supplementary
substitution σk+1 , so conditions ii and iii trivially hold
• they always swap left-hand side with right-hand side; so does Select for each Orient selection
Therefore, we only need to prove condition i for each Orient selection.
We now have to consider all the cases from Pk to Pk+1 in Select via rule bk+1 .
Case 1. L(s, m) < L(t, n)
It must be the case that t n is a list variable because L(t, n) > 0 only for list variables.
Call x and y the parent symbols of sm and tn in s and t.
Case 1.1. Type(sm ) = ListVar
By hypothesis, it follows that x and y are also list variables.
Suppose nothing follows x (i.e. LookAhead(sm ) = f alse). Then the unification problem at
node bk must be of the form x = y : M. However, we have that L(s, m) < L(t, n) which contradicts
that δ is a unifier.
Therefore, there must be something following x. Then the current unification problem must
be of the form x : L = y : M. Then rule Decomp2’ is applicable (condition i satisfied). Because x
has the shorter expansion by δ , t n+L(sm )+1 is a child variable of y and condition ii holds.
For iii, let λk′ = (sn . . . sm+L(sm ) 7→ T ) where T = δ (sm . . . sm+L(sm ) ). For δ to be a unifier, it
must contain term(s) (tn . . .tn+L(sm ) 7→ T ):
δ ⊇ σk ◦ λk ∪ (tn . . .tn+L(sm ) 7→ T )
= σk ◦ λk ∪ ((tn . . .tn+L(sm ) 7→ sm . . . sm+L(sm ) ) ◦ λk′ ) (same as saying y starts with x)
= σk ◦ λk ∪ ((y 7→ x : y′ ) ◦ λk′ )
= σk ◦ (y 7→ x : y′ ) ◦ λk ◦ λk′ (since no repeated list variables)
= σk+1 ◦ λk+1 as required (set λk+1 = λk ◦ λk′ )
Case 1.2. Type(sm ) = AtomVar
It holds by hypothesis that x and y are atom and list variables so rule Orient3 is applicable.
Case 1.3. Type(sm ) = AtomExpr
The argument is the same as above except that x is an atom expression and Orient1 becomes
applicable.
Case 1.4. Type(sm ) = EmptyListVar
Because L(t n ) > L(sm ) = 0, there must be something after sm+L(sm ) (i.e. LookAhead(sm ) =
true) for δ to be a unifier. Also, by hypothesis x must be a list variable since xδ = empty.
Therefore rule Subst2 is applicable (condition i holds). The resulting unification problem is
({L = M}{x 7→ empty}; σk ◦ {x 7→ empty}). Select moves the position m by 1 and keeps n,
therefore condition ii also holds.
For condition iii:

23

δ

⊇
=
=

σk ◦ λk ∪ (x 7→ empty)
σk ◦ (x 7→ empty) ◦ λk (since no repeated list variables)
σk+1 ◦ λk+1 as required (set λk+1 = λk )

Case 1.5. Type(sm ) = empty
As explained, this subcase cannot occur if δ is a unifier.
Case 2. L(s, m) > L(t, n)
As in the previous case, it follows that sm is a list variable with |δ (x)| > 0 for its parent
symbol x. By hypothesis, x is also a list variable.
Case 2.1. Let LookAhead(sm ) = f alse, i.e. nothing follows x
The unification problem at node bk must be of the form x = L so rule Subst1 is applicable
(condition i satisfied). Since the resulting unification problem is h∅, σk ◦ {x 7→ y : M}i and
Select moves the head position to the end of the strings s̄ and t̄, condition ii is satisfied.
For iii, let λk′ = (L 7→ T ) where T = δ (L). For δ to be a unifier, it must contain term(s) (x 7→ T )
δ ⊇ σk ◦ λk ∪ (x 7→ T )
= σk ◦ λk ∪ ((x 7→ L) ◦ λk′ )
= σk ◦ (x 7→ L) ◦ λk ◦ λk′ (since no repeated list variables)
= σk+1 ◦ λk+1 as required (set λk+1 = λk ◦ λk′ )
Now let LookAhead(sm ) = true and the problem is of the form x : L = s : M with L 6= empty.
Case 2.2. Type(tn ) = ListVar
By hypothesis, y must be a list variable. Then rule Decomp2 is applicable (condition i satisfied). Because x has the longer expansion by δ , sm+L(t n )+1 is a child variable of x and condition
ii holds.
For iii, let λk′ = (sn . . . sm+L(t n ) 7→ T ) where T = δ (sm . . . sm+L(t n ) ), and the argument becomes
identical to Case 1.1 (x starts with y, so σk+1 = σk ◦ {x 7→ y : x′ })
Case 2.3. Type(tn ) = AtomVar or Type(tn ) = AtomExpr
By hypothesis, y is an atom variable or atom expression. Then the problem is of the form
x : L = a : M with L 6= empty. So rule Subst3 is applicable (condition i satisfied). Positions are
incremented by 1, so condition ii holds as sm+1 and x′ (in Orient3) must have the same parent
symbol.
For iii, let λk′ = (t n 7→ T ) where T = δ (t n ). It follows that δ must contain term (sm 7→ T ) to be
a unifier.
δ ⊇ σk ◦ λk ∪ (sm 7→ T )
= σk ◦ λk ∪ ((sm 7→ t n ) ◦ λk′ )
= σk ◦ λk ∪ ((x 7→ a : x′ ) ◦ λk′ )
= σk ◦ (x 7→ a : x′ ) ◦ λk ◦ λk′ (since no repeated list variables)
= σk+1 ◦ λk+1 as required (set λk+1 = λk ◦ λk′ )
Case 2.4. Type(tn ) = EmptyListVar
We have that t n is of the form ye where y is a list variable with δ (y) = empty. The unification
problem is then of the form x : L = y : M. Rule Decomp2 becomes applicable
Let λk′ = (y 7→ empty)

4 PROVING COMPLETENESS: THE SELECT ALGORITHM

24

δ

⊇
=
=
=

σk ◦ λk ∪ (y 7→ empty)
σk ◦ λk ∪ ((x 7→ y : x′ ) ◦ λk′ )
σk ◦ (x 7→ y : x′ ) ◦ λk ◦ λk′ (because no repeated list variables)
σk+1 ◦ λk+1 as required (set λk+1 = λk ◦ λk′ )

Case 3. L(s, m) = L(t, n)
Case 3.1. L(s, m) = L(t, n) > 0
It must be the case that sm and t n are list variables because L(sm ) > 0 and L(t, n) > 0 only for
list variables.
By hypothesis, it follows that x and y are also list variables.
If there is nothing after the x (i.e. LookAhead(sm ) = f alse). Then Subst1 is applicable and
the argument is the same as Case 2.1.
Otherwise, it must be that L 6= empty so rule Decomp1 is applicable. Here the problem is of
the form x : L = y : M and the generated substitution is σk+1 = σk ◦ (x 7→ y).
For ii, the argument is similar to Case 2.2 except that now both sm+L(sm )+1 and L, and t n+L(sm )+1
and M must have the same pairs of parent symbols.
Let λk′ = (y 7→ δ (y)). It must be the case that δ also contains term (x 7→ δ (y)) to be a unifier.
δ ⊇ σk ◦ λk ∪ (x 7→ δ (y))
= σk ◦ λk ∪ ((x 7→ y) ◦ λk′ )
= σk ◦ (x 7→ y) ◦ λk ◦ λk′ (because no repeated list variables)
= σk+1 ◦ λk+1 as required (set λk+1 = λk ◦ λk′ )
Case 3.2. L(s, m) = L(t, n) = 0
This is the largest subcase because sm and tn can be of any of the possible types.
3.2.1-3 (ListVar, ListVar) or (ListVar, AtomVar) or (ListVar, AtomExpr)–
Same as 3.1 because the parent symbol of t n can be matched by s in Decomp1.
3.2.4. (ListVar, EmptyListVar) – same as Case 2.4
3.2.5. (ListVar, empty) – cannot happen as δ is a unifier
3.2.6. (AtomVar, ListVar) – same as Case 1.2
3.2.7. (AtomVar, AtomVar) or (AtomVar, AtomExpr)
• LookAhead(sm ) = true, i.e. L 6= empty - then the problem is of the form a : L = b : M
(a and b are also atom variables by hypothesis) and rule Decomp1’ is applicable. Unify
generates σk+1 = σk ◦ {a 7→ b}.
Let λk′ = (sm 7→ δ (sm )) = (a 7→ δ (a)). Then δ must also contain term (t n 7→ δ (sm )) to be
a unifier:
δ ⊇ σk ◦ λk ∪ (t n 7→ δ (sm ))
= σk ◦ λk ∪ ((t n 7→ sm ) ◦ λk′ )
= σk ◦ λk ∪ ((a 7→ b) ◦ λk′ )
= σk ◦ (a 7→ b) ◦ λk ◦ λk′
= σk+1 ◦ λk+1 as required (set λk+1 = λk ◦ λk′ )
• LookAhead(sm ) = f alse, i.e. the problem is a = b : M.

25
– If LookAhead(t n ) = true, then M can only be a single list variable for δ to be a unifier
with δ (y) = empty. This makes rule Decomp4 applicable. For iii, the argument is
the same as in the previous item (with σk+1 = σk ◦ {a 7→ b}).
– If LookAhead(t n ) = f alse, then the problem is of the form a = b, which makes
Subst1 is applicable and the argument is the same as Case 2.1
3.2.9. (AtomVar, EmptyListVar) – same as Case 1.2
3.2.10. (AtomVar, empty) – cannot happen due to failure lemmata
3.2.11. (AtomExpr, ListVar) – same as Case 1.3
3.2.12. (AtomExpr, AtomVar) – same as Case 1.3
3.2.13. (AtomExpr, AtomExpr) – Both symbols must be the same atom expression due to
not considering the subunification algorithm for String-Char. So rule Decomp3 is applicable.
Conditions ii and iii hold trivially.
3.2.14. (AtomExpr, EmptyListVar) – same as 1.3
3.2.16-18. (EmptyListVar, ListVar) or (EmptyListVar, AtomVar) or (EmptyListVar, AtomExpr)
It must be the case that there is something following sm for δ to be a unifier. Proceed proof like
Case 1.4
3.2.19. (EmptyListVar, EmptyListVar) – same as 3.1
3.2.20. (EmptyListVar, empty)
It follows that x (the parent of sm ) is a list variable with δ (x) = empty. Also, since there are
no repeated list variables, for δ to be a unifier there must be nothing following x. So the problem
is of the form x = empty and rule Subst1 is applicable.
For condition iii, proceed as Case 1.4
3.2.21. (empty, ListVar) – cannot happen because δ is a unifier
3.2.22 & 3.2.23 (empty, AtomVar) or (empty, AtomExpr) – cannot happen due to failure
lemmata
3.2.24. (empty, EmptyListVar)
It follows that y (the parent of t n ) is a list variable with δ (y) = empty. So the problem has the
form empty = x : L and rule Orient4 is applicable.
3.2.25. (empty, empty)
It follows that rule Remove is applicable. Conditions ii and iii hold trivially.

5 Conclusion
This paper presents groundwork for a static confluence analysis of GP programs. We have constructed a rule-based unification algorithm for systems of equations with left-hand expressions
of rule schemata, and have shown that the algorithm always terminates and is sound. Moreover,
we have proved completeness in that every unifier of the input problem is an instance of some
unifier in the computed set of solutions.
Future work includes establishing a Critical Pair Lemma in the sense of [Plu05]; this entails
developing a notion of independent rule schema applications, as well as restriction and embed-

BIBLIOGRAPHY

26

ding theorems for derivations with rule schemata. Another topic is to consider critical pairs of
conditional rule schemata (see [EGH+ 12]).
In addition, since critical pairs contain graphs labelled with expressions, checking joinability
of critical pairs will require sufficient conditions under which equivalence of expressions can be
decided. This is because the theory of GP’s label algebra includes the undecidable theory of
Peano arithmetic.
Acknowledgements: We thank the anonymous referees of GCM 2014 for their comments on
previous versions of this paper.

Bibliography
[BFPR15] C. Bak, G. Faulkner, D. Plump, C. Runciman. A Reference Interpreter for the Graph
Programming Language GP 2. In Proc. Graphs as Models (GaM 2015). Electronic
Proceedings in Theoretical Computer Science 181, pp. 48–64. 2015.
doi:10.4204/EPTCS.181
[BS01]

F. Baader, W. Snyder. Unification Theory. In Robinson and Voronkov (eds.), Handbook of Automated Reasoning. Pp. 445–532. Elsevier and MIT Press, 2001.

[EEPT06] H. Ehrig, K. Ehrig, U. Prange, G. Taentzer. Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science. Springer-Verlag, 2006.
[EGH+ 12] H. Ehrig, U. Golas, A. Habel, L. Lambers, F. Orejas. M-Adhesive Transformation
Systems with Nested Application Conditions. Part 2: Embedding, Critical Pairs and
Local Confluence. Fundamenta Informaticae 118(1):35–63, 2012.
[GLEO12] U. Golas, L. Lambers, H. Ehrig, F. Orejas. Attributed Graph Transformation with
Inheritance: Efficient Conflict Detection and Local Confluence Analysis Using Abstract Critical Pairs. Theoretical Computer Science 424:46–68, 2012.
doi:10.1016/j.tcs.2012.01.032
[HKT02]

R. Heckel, J. M. Küster, G. Taentzer. Confluence of Typed Attributed Graph Transformation Systems. In Proc. International Conference on Graph Transformation
(ICGT 2002). Lecture Notes in Computer Science 2505, pp. 161–176. SpringerVerlag, 2002.

[HP15]

I. Hristakiev, D. Plump. A Unification Algorithm for GP 2. In Graph Computation
Models (GCM 2014), Revised Selected Papers. Electronic Communications of the
EASST 71. 2015.

[Jaf90]

J. Jaffar. Minimal and Complete Word Unification. Journal of the ACM 37(1):47–85,
1990.

BIBLIOGRAPHY

27

[Pla99]

W. Plandowski. Satisfiability of Word Equations with Constants is in PSPACE. In
Symposium on Foundations of Computer Science (FOCS 1999). Pp. 495–500. IEEE
Computer Society, 1999.

[Plo72]

G. Plotkin. Building-in Equational Theories. Machine intelligence 7(4):73–90, 1972.

[Plu05]

D. Plump. Confluence of Graph Transformation Revisited. In Middeldorp et al.
(eds.), Processes, Terms and Cycles: Steps on the Road to Infinity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday. Lecture Notes in
Computer Science 3838, pp. 280–308. Springer-Verlag, 2005.
doi:10.1007/11601548

[Plu12]

D. Plump. The Design of GP 2. In Proc. International Workshop on Reduction
Strategies in Rewriting and Programming (WRS 2011). Electronic Proceedings in
Theoretical Computer Science 82, pp. 1–16. 2012.
doi:10.4204/EPTCS.82.1

[Sch92]

K. U. Schulz. Makanin’s Algorithm for Word Equations: Two Improvements and a
Generalization. In Proc. Word Equations and Related Topics (IWWERT ’90). Lecture
Notes in Computer Science 572, pp. 85–150. Springer-Verlag, 1992.

[Sie78]

J. Siekmann. Unification and Matching Problems. PhD thesis, University of Essex,
1978.

