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

denote single formulae. Since in every such unification problem no sequence
meta-variable occurs more that once, and all of them occur only on the top
level, , in fact, deals with a finitary case of sequence unification.

Word equations [1, 8] and associative unification [15] can be modelled by
syntactic sequence unification using constants, sequence variables and one flex-
ible arity function symbol. In the similar way we can imitate the unification
algorithm for path logics closed under right identity and associativity [17].
The

Isabelle

prover [4] has a construct called vector of (Skolem) functions
that resembles our sequence functions. However, unification does not allow to
split vectors of functions between variables: such a vector of functions either
entirely unifies with a variable, or with another vector of functions.
The programming language of Mathematica uses pattern matching that
supports sequence variables (represented as identifiers with “triple blanks”, e.g.,
x ) and flexible arity function symbols. Our procedure (without sequence func-
tion symbols) can imitate the behavior of

Set-Var

Mathematica matching algorithm.

system [6] to
Skolemize quantified sequence variables. In the equational prover of

Buchberger introduced sequence functions in the Theorema

Theorema
[11] we implemented a special case of unification with sequence variables and
sequence functions: sequence variables occurring only in the last argument po-
sitions in terms. It makes unification unitary. Similar restriction is imposed on
sequence variables in the RelFun system [5] that integrates extensions of logic

and functional programming. allows multiple-valued functions as well.

In [10] we described unification procedures for free, flat, restricted flat and
orderless theories with sequence variables, but without sequence functions.
Under certain restrictions sequence unification problems have at most finitely
many solutions: sequence variables in the last argument positions, unification
problems with at least one ground side (matching as a particular instance), all
sequence variables on the top level with maximum one occurrence. It would be
interesting to identify more cases with finite or finitely representable solution
sets.

RelFun

Acknowledgements

I thank Bruno Buchberger and Mircea Marin for interesting discussions on the
topic.

References

1. H. Abdulrab and J.-P. Pecuchet. Solving word equations. J. Symbolic Computation ,
8(5):499-522, 1990.
2. F. Baader and K. U. Schulz. Unification in the union of disjoint equational theories:
Combining decision procedures. J. Symbolic Computation , 21(2):211-244, 1996.
3. F. Baader and W. Snyder. Unification theory. In A. Robinson and A. Voronkov,
editors, Handbook of Automated Reasoning , volume I, chapter 8, pages 445-532.
Elsevier Science, 2001.