Module `Single_value_abstraction.Quadrivalent`

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.

type boolean = Lattices.Quadrivalent.boolean =

| Bottom
| True
| False
| Top

val name : string

module Boolean_Forward : 
  Operator.BOOLEAN_FORWARD
    with module Arity := Operator.Forward_Arity
     and type boolean := boolean

module Boolean_Backward : 
  Operator.BOOLEAN_BACKWARD
    with module Arity := Operator.Backward_Arity
     and type boolean := boolean

module Boolean_Lattice : Lattices.Sig.BOOLEAN_LATTICE with type t = boolean

val of_bools : may_be_false:bool -> may_be_true:bool -> boolean

The result of of_bools may_be_false may_be_false:

May be false (i.e. False or Top) if may_be_false is true, and must not be otherwise (i.e. True or Bottom)

May be true (i.e. True of Top) if may_be_true is true, and must not be otherwise (i.e. False or Bottom)

val refine : older:boolean -> newer:boolean -> boolean option

It attempts to refine the abstract value older with the information provided by newer.

Module Single_value_abstraction.Quadrivalent

Module `Single_value_abstraction.Quadrivalent`