de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

AE-Equational theory of context unification is Co-RE-Hard

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45677

Vorobyov,  Sergei
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)

MPI-I-98-2-008.pdf
(Any fulltext), 289KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Vorobyov, S.(1998). AE-Equational theory of context unification is Co-RE-Hard (MPI-I-1998-2-008). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-7A87-8
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.