MPI-I-98-2-008
AE-Equational theory of context unification is Co-RE-Hard
Vorobyov, Sergei
April 1998, 20 pages.
.
Status: available - back from printing
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.
Note:
Revised and abridged version to appear in the Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS'98), Springer Lecture Notes in Computer
Science. Brno, Czech Republic, August 24-28.
-
- Attachement: MPI-I-98-2-008.ps (253 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1998-2-008
BibTeX
@TECHREPORT{Vorobyov98-2-008,
AUTHOR = {Vorobyov, Sergei},
TITLE = {AE-Equational theory of context unification is Co-RE-Hard},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-98-2-008},
MONTH = {April},
YEAR = {1998},
ISSN = {0946-011X},
NOTE = {Revised and abridged version to appear in the Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS'98), Springer Lecture Notes in Computer
Science. Brno, Czech Republic, August 24-28.},
}