💾 Archived View for dcreager.net › papers › Kutsia2007.gmi captured on 2023-11-14 at 08:21:15. Gemini links have been rewritten to link to archived content
⬅️ Previous capture (2023-11-04)
-=-=-=-=-=-=-
Temur Kutsia, Solving equations with sequence variables and sequence functions, Journal of Symbolic Computation, Volume 42, Issue 3, 2007, Pages 352-388, ISSN 0747-7171.
Term equations involving individual and sequence variables and sequence function symbols are studied. Function symbols can have either fixed or flexible arity. A sequence variable can be instantiated by any finite sequence of terms. A sequence function abbreviates a finite sequence of functions all having the same argument lists. It is proved that solvability of systems of equations of this form is decidable. A new unification procedure that enumerates a complete almost minimal set of solutions is presented, together with variations for special cases. The procedure terminates if the solution set is finite. Applications in various areas of artificial intelligence, symbolic computation, and programming are discussed.
This is the primary paper describing sequence unification, which is the unification strategy we use in stack graph path stitching.
§6.3 shows that sequence unification is unitary if “sequence variables occur only in the last argument positions in terms”.