非表示:
キーワード:
-
要旨:
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.
