hide
Free keywords:
-
Abstract:
Context unification is a particular case of second-order
unification, where all second-order variables are *unary* and
only *linear* functions are sought for as solutions. Its
decidability is an open problem. We present the simplest (currently
known) undecidable quantified fragment of the theory of context
unification by showing that for every signature containing a
non-unary function symbol there exists a one-parametric context
equation such that the universal-existential closure of this equation
forms a co-r.e. hard set, as the parameter runs over the set of
finite words of a binary alphabet.
Moreover, the universal prefix contains one first-order, and the
existential prefix contains just 5 context and 3 first-order variables.
It follows, in particular, that the AE-equational
theory of context unification is undecidable.
