Evaluation of Proposition AST in OCaml Example

In OCaml, using the following definitions, implement a function evaluate : valuation -> proposition -> bool such that evaluate v p is true if the logic proposition p is true when using the valuation v. Avoid short-circuiting evaluation of the conjunction and disjunction operations, and ensure that an exception is raised if p contains a variable that cannot be found in v.

ocaml

module StringMap = Map.Make (String)

type variable = string
type valuation = bool StringMap.t

type proposition =
  | Variable of variable                       (* x *)
  | Conjunction of proposition * proposition   (* p ∧ q *)
  | Disjunction of proposition * proposition   (* p ∨ q *)
  | Negation of proposition                    (* ¬ p *)
  | Top                                        (* ⊤ *)
  | Bottom                                     (* ⊥ *)

Solution

Following the definition of propositional logic, we implement evaluate as a recursive function that traverses the abstract syntax tree of the input proposition. In the case where the proposition is a variable, we need to lookup the valuation table for the truth value assigned to the variable. In the logical conjunction and disjunction cases, to avoid OCaml's short-circuiting evaluation of the boolean operators (&&) and (||), we need to fully evaluate the operands before computing the operation. The negation and constants cases are straigthforward.

ocaml

let rec evaluate : valuation -> proposition -> bool =
  fun valuation proposition ->
    match proposition with
    | Variable x -> StringMap.find x valuation
    | Conjunction (p, q) ->
        let vp = evaluate valuation p in
        let vq = evaluate valuation q in
        vp && vq
    | Disjunction (p, q) ->
        let vp = evaluate valuation p in
        let vq = evaluate valuation q in
        vp || vq
    | Negation p ->
        let vp = evaluate valuation p in
        Bool.not vp
    | Top -> true
    | Bottom -> false