Schematic Unification
David M. Cerna
TL;DR
This work presents a generalization of first-order unification to a term algebra where variable indexing is part of the object language and provides a terminating and sound algorithm.
Abstract
We present a generalization of first-order unification to a term algebra where variable indexing is part of the object language. We exploit variable indexing by associating some sequences of variables ($X_0,\ X_1,\ X_2,\dots$) with a mapping $σ$ whose domain is the variable sequence and whose range consist of terms that may contain variables from the sequence. From a given term $t$, an infinite sequence of terms may be produced by iterative application of $σ$. Given a unification problem $U$ and mapping $σ$, the \textit{schematic unification problem} asks whether all unification problems $U$, $σ(U)$, $σ(σ(U))$, $\dots$ are unifiable. We provide a terminating and sound algorithm. Our algorithm is \textit{complete} if we further restrict ourselves to so-called $\infty$-stable problems. We conjecture that this additional requirement is unnecessary for completeness. Schematic unification is related to methods of inductive proof transformation by resolution and inductive reasoning.