5.2 Constructive Disjunction

The operational semantics of some propagators is based on constructive disjunction which allows to lift common information from clauses of a disjunction.

In Oz, constructive disjunction is available through a syntax like the one for nondistributable disjunction or ... end which uses the keyword condis instead or or.

Constructive disjunction adopts the operational semantics of the nondistributable disjunction concerning entailment and failure of clauses. It enriches the semantics as follows.

Assume a disjunction with n clauses and let S be the constraint store of the computation space in which it resides. Let S_1,\ldots,S_n denote the local stores of the n clauses. Then the strongest constraint C consisting of basic constraints X\in D with S_i\models C for 1\leq i \leq n is lifted and added to S.

As an example consider the store X, Y\in\{0,\ldots,10\} and

condis X + 9 =<: Y
[] Y + 9 =<: X
end

Constructive disjunction narrows the domains of X and Y to \{0,1,9,10\}.


Denys Duchier, Leif Kornstaedt, Tobias Müller, Christian Schulte and Peter Van Roy
Version 1.0.1 (19990218)