Module Single_value_abstraction.QuadrivalentSource

The lattice for four-valued boolean logic. It represents the powerset of {true,false}. See Lattices.Quadrivalent.

The transfer functions are implemented naturally following the Galois connection between this lattice and the {true,false} powerset. For instance, A \land^{\#} B = \alpha(\{\, a \land b \mid a \in \gamma(A),\ b \in \gamma(B) \,\}) The operations on True, False and Top correspond to Kleene's strong three-valued logic.

Those on True, False and Bottom correspond to Kleene's weak three-valued logic (= Bochvar three-valued logic).

However, note that this four-valued logic is different Belnap's four-valued logic. It should be seen as a combination of Kleene's strong and weak ternary logics.

Note: For the lattice implementor, it may be sometimes difficult to know whether the answer to a predicate should be Top or Bottom. Implementation should be guided by the Gallois connection to the collecting semantics. For instance, when implementing abstract equality ==^\#: A ==^{\#} B = \gamma( \{ a \in \alpha(A), b \in \alpha(B): a == b \})

Thus ==^\# returns Bottom if either A or B concretize only into the empty set.