max planck institut
informatik
informatik
MPI-I-98-2-008. April 1998, 20 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry
Abstract in LaTeX format:
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.
Acknowledgement:
References to related material:
| To download this research report, please select the type of document that fits best your needs. | Attachement Size(s): |
|---|---|
| 253 KBytes | |
| Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView | |
BibTeX