Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Negativ set constraints: an easy proof of decidability

Charatonik, Witold and Pacholski, Leszek

MPI-I-93-265. December 1993, 11 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-93-265.pdfMPI-I-93-265.pdfMPI-I-93-265.dvi - MPI-I-93-265.dvi
56 KBytes; 109 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Charatonik, Witold and Pacholski, Leszek},
  TITLE = {Negativ set constraints: an easy proof of decidability},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-93-265},
  MONTH = {December},
  YEAR = {1993},
  ISSN = {0946-011X},