Help Privacy Policy Disclaimer
  Advanced SearchBrowse





Negative set constraints: an easy proof of decidability


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


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

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

(Any fulltext), 109KB

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

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

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