logic.ml

type property = string

(** Logic subsumption type: p |= q *)
type t = (property → property → bool)

(** Converts a property to a string representation. *)
let string_of_property p = p


(** Propositional logic formula type. *)
type 'a formula = 

  (* `⊤`: True value formula. *)
  | True

  (* `⊥`: False value formula. *)
  | False

  (* `p, q, ...`: Logical variable. *)
  | Variable of 'a

  (* `¬`: Formula negation. *)
  | Negation of 'a formula

  (* `∧`: Logical conjunction. *)
  | Conjunction of 'a formula * 'a formula  

  (* `∨`: Logical disjunction. *)
  | Disjunction of 'a formula * 'a formula

  (* `⇒`: Material implication. *)
  | Implication of 'a formula * 'a formula

  (* `⇔`: Material equivalence. *)
  | Equivalence of 'a formula * 'a formula


(* DSL Constructor Functions *)
module Lang = struct
  let var : 'a → 'a formula =
    λ x → Variable x

  let (¬) : 'a formula → 'a formula =
    λ x → Negation x

  let (∨) : 'a formula → 'a formula → 'a formula =
    λ p q → Disjunction (p, q)

  let (∧) : 'a formula → 'a formula → 'a formula =
    λ p q → Conjunction (p, q)

  let (⇒) : 'a formula → 'a formula → 'a formula =
    λ p q → Implication (p, q)

  let (⇔) : 'a formula → 'a formula → 'a formula =
    λ p q → Equivalence (p, q)
end


(** Converts a formulta to a string representation. *)
let rec string_of_formula : 'a formula → string = λ
  | True → "⊤"
  | False → "⊥"
  | Variable v → string_of_property v
  | Negation f → "¬" ^ (string_of_formula f)
  | Conjunction (a, b) → "(" ^ (string_of_formula a) ^ " ∧ "
                             ^ (string_of_formula b) ^ ")"
  | Disjunction (a, b) → "(" ^ (string_of_formula a) ^ " ∨ "
                             ^ (string_of_formula b) ^ ")"
  | Implication (a, b) → "(" ^ (string_of_formula a) ^ " ⇒ "
                             ^ (string_of_formula b) ^ ")"
  | Equivalence (a, b) → "(" ^ (string_of_formula a) ^ " ⇔ "
                             ^ (string_of_formula b) ^ ")"


(** Evaluates the truth value of a formula in a given environment. *)
let rec eval : ('a → bool) → 'a formula → bool = λ env → λ
  | True → true
  | False → false
  | Variable x → env x
  | Negation f → not (eval env f)
  | Conjunction (a, b) → (eval env a) && (eval env b)
  | Disjunction (a, b) → (eval env a) || (eval env b)
  | Implication (a, b) → not (eval env a) || (eval env b)
  | Equivalence (a, b) → (eval env a) = (eval env b)

(** Applies a function to all formula variables perserving the structure. *)
let rec map : ('a → 'b formula) → 'a formula → 'b formula = λ f → λ
  | True | False as truth → truth
  | Variable x → f x
  | Negation a → Negation (map f a)
  | Conjunction (a, b) → Conjunction (map f a, map f b)
  | Disjunction (a, b) → Disjunction (map f a, map f b)
  | Implication (a, b) → Implication (map f a, map f b)
  | Equivalence (a, b) → Equivalence (map f a, map f b)


(** Applies a function to all formula variables ignoring the results. *)
let rec iter: ('a → unit) → 'a formula → unit = λ f → λ
  | True | False → ()
  | Variable x → f x
  | Negation a → iter f a
  | Conjunction (a, b) → iter f a; iter f b
  | Disjunction (a, b) → iter f a; iter f b
  | Implication (a, b) → iter f a; iter f b
  | Equivalence (a, b) → iter f a; iter f b


(* TODO: Group the results. *)
let rec properties : 'a formula → property list = λ
  | True | False -> []
  | Variable x → [x]
  | Negation f → properties f
  | Conjunction (p, q) | Disjunction (p, q) | Implication (p, q)
  | Equivalence (p, q) → (properties p) @ (properties q)

(* is_contradiction(f:Formula) = ! any(values(f)) *)
(* is_contingent(f::Formula) = ! (is_tautology(f) || is_contingent(f)) *)