アイテム詳細

要旨

Testing satisfaction of guards is the essential operation of
concurrent constraint programming ({\footnotesize CCP}) systems. We
present and prove correct, for the first time, an incremental
algorithm for the simultaneous tests of entailment and disentailment
of rational tree constraints to be used in {\footnotesize CCP}
systems with deep guards (\eg, in {\footnotesize AKL} or in Oz).
The algorithm is presented as the {\em simplification\/} of the
constraints which form the (possibly deep) guards and which are {\em
situated\/} at different nodes in a tree (of arbitrary depth). The
nodes correspond to local computation spaces. In this algorithm,
a variable may have multiple bindings (which each represent a
constraint on that same variable in a different node). These may be
realized in various ways. We give a simple fixed-point algorithm
and use it for proving that the tests implemented by another,
practical algorithm are correct and complete for entailment and
disentailment. We formulate the results in this paper for rational
tree constraints; they can be adapted to finite and feature trees.