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

Item

ITEM ACTIONSEXPORT

Released

Report

Negativ set constraints: an easy proof of decidability

MPS-Authors
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;

Locator
There are no locators available
Fulltext (public)

MPI-I-93-265.pdf
(Any fulltext), 109KB

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

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.


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