A Note On Square-free Sequences and Anti-unification Type
David M. Cerna
TL;DR
The paper tackles whether a minimal complete set of $E$-generalizations exists for AI anti-unification. It demonstrates Nullarity by constructing an infinite chain of generalizations using square-free sequences over a ternary alphabet. The approach defines $(x,C)$-simple words and uses containment arguments to refute the existence of a finite $mcsg_E(s,t)$ in the AI setting. The result clarifies limits on inductive inference in equational theories with AI properties and offers a method that could extend to related theories.
Abstract
Error: Peer-review process exposed an error in Theorem 1 that, unfourtunately, is not repairable. Idempotent semigroups are always finite. See Green and Rees [1952], Siekmann and Szabó [1981] for details Anti-unification is a fundamental operation used for inductive inference. It is abstractly defined as a process deriving from a set of symbolic expressions a new symbolic expression possessing certain commonalities shared between its members. We consider anti-unification over term algebras where some function symbols are interpreted as associative-idempotent $(f (x, f (y, z)) = f (f (x, y), z)$ and $f (x, x) = x$, respectively) and show that there exists generalization problems for which a minimal complete set of solutions does not exist (Nullary), that is every complete set must contain comparable elements with respect to the generality relation. In contrast to earlier techniques for showing the nullarity of a generalization problem, we exploit combinatorial properties of complete sets of solutions to show that comparable elements are not avoidable. We show that every complete set of solutions contains an infinite chain of comparable generalizations whose structure is isomorphic to a subsequence of an infinite square-free sequence over three symbols.