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

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

Negativ set constraints: an easy proof of decidability

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

Charatonik,  Witold
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45153

Pacholski,  Leszek
Programming Logics, MPI for Informatics, Max Planck Society;

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

MPI-I-93-265.pdf
(beliebiger Volltext), 109KB

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

Charatonik, W., & Pacholski, L.(1993). Negativ set constraints: an easy proof of decidability (MPI-I-93-265). Saarbrücken: Max-Planck-Institut für Informatik.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0014-B4C2-3
Zusammenfassung
Systems of set constraints describe relations between sets of ground terms. They have been successfuly used in program analysis and type inference. So far two proofs of decidability of mixed set constraints have been given: by R.~Gilleron, S.~Tison and M.~Tommasi [12] and A.~Aiken, D.~Kozen, and E.L.~Wimmers [3], but both these proofs are very long, involved and difficult to follow. We first give a new, simple proof of decidability of systems of mixed positive and negative set constraints. We explicitely describe a very simple algorithm working in NEXPTIME and we give in all detail a relatively easy proof of its correctness. Then we sketch how our technique can be applied to get various extensions of this result. In particular we prove that the problem of consistency of mixed set constraints with restricted projections and unrestricted diagonalization is decidable. Diagonalization here represents a decidable part of equality. It is known that the equality of terms can not be directly included in the language of set constraints. Our approach is based on a reduction of set constraints to the monadic class given in a recent paper by L.~Bachmair, H.~Ganzinger, and U.~Waldmann [7]. To save space we assume that the reader is familiar with the main ideas of the method introduced in [7] of using the monadic class to study set constraints. We shall drop this assumption in the full paper.