Item

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.