Solving Equations Involving Sequence Variables and Sequence Functions - Artificial Intelligence and Symbolic Computation - page 165

iff Ψ is. Indeed, replacing each variable binding x → s 1 ,...,s n in a unifier of

Φ with x Ψ → seq ( s 1 ,...,s n ) yields a unifier of Ψ ,andviceversa.

We can consider Ψ as an elementary unification problem in the combined
theory E 1 ∪

E 2 ,where E 1 is a flat equational theory over { seq } and V Ind ,and E 2

is a free equational theory over V Ind . E 1 -unification problems are,

in fact, word equations, while E 2 -unification is Robinson unification. Using the
Baader-Schulz combination method [2], we can prove the following theorem:

F ix ( Ψ )and

Theorem 5. F -unifiability of Ψ is decidable.

Hence, unifiability of general syntactic sequence unification problem is decid-
able.
As for the unification type, in Example 8 we have seen that mcu ∅ ( Γ )is
infinite for Γ =

?
∅

. It implies that the syntactic sequence uni-
fication is at least infinitary. To show that it is not nullary, by Proposition 1,
it is sucient to prove existence of an almost minimal set of unifiers for every
syntactic sequence unification problem. We do it in the standard way, by proving
that for any Γ , every strictly decreasing chain σ 1 X,Q
∅

{ f ( a, x ) ≈ f ( x, a ) }

σ 2 X,Q
∅

··· of substitu-

tions in U ∅ ( Γ ) is finite, where X = V ar ( Γ )and Q = SF un ( Γ ). Hence, syntactic

sequence unification is infinitary.

4 Relation with Order-Sorted Higher-Order Unification

Syntactic sequence unification can be considered as a special case of order-sorted
higher-order E -unification. Here we show the corresponding encoding in the
framework described in [9]. We consider simply typed λ -calculus with the types
i and o . The set of base sorts consists of ind , seq , seqc , o such that the type of
o is o and the type of the other sorts is i . We will treat individual and sequence
variables as first order variables, sequence functions as second order variables and
define a context Γ such that Γ( x )= ind for all x

∈V Ind ,Γ( x )= seq for all x ∈

V Seq ,Γ( f )= seq → seqc for each f ∈F

Seq ,andΓ( f )= ind →···→ ind

Flex

→

n times

Fix

seqc for each f

r ( f )= n . Individual function symbols are treated
as constants. We assign to each f

∈F

Seq with

A

Flex
Ind

∈F a functional sort seq → ind and

Fix

to each f ∈F

Ind with

A r ( f )= n a functional sort ind →···→ ind → ind .

n times

We assume equality constants ≈ s for every sort s .Inaddition,wehavetwo

function symbols: binary of the sort seq → seq → seq and a constant [] of

the sort seq . Sorts are partially ordered as [ ind ≤ seqc ]and[ seqc ≤ seq ]. The
equational theory is an AU-theory, asserting associativity of with [] as left

and right unit. We consider unification problems for terms of the sort ind where
terms are in βη -normal form containing no bound variables, and terms whose
head is

are flattened. For a given unification problem Γ in this theory, we
are looking for unifiers that obey the following restrictions: If a unifier σ binds a
second order variable f of the sort seq → seqc ,then fσ = λx. g 1 ( x ) ,...,g m ( x )

and if σ binds a second order variable f of the sort ind →···→ ind → seqc ,

n times