de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

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

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45677

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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)

1998-2-008
(beliebiger Volltext), 11KB

Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


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