Basic normalization of propositional logic, in Standard ML

prop.sml

(*
Some basic normal forms for propositional logic.

So far, I have NNF, NENF, DNF, and CNF normalizations.

This is mostly a translation of chapter 2 from John Harrison's _Handbook of Automated Reasoning and Practical Logic_.
*)
datatype 'a Formula = True
       | False
       | Atom of 'a
       | Not of 'a Formula
       | And of ('a Formula)*('a Formula)
       | Or of ('a Formula)*('a Formula)
       | Implies of ('a Formula)*('a Formula)
       | Iff of ('a Formula)*('a Formula)
       | Forall of string * ('a Formula)
       | Exists of string * ('a Formula);

datatype Prop = P of string;

(*
Produces a string representation of a formula such that it could be printed out,
copy/pasted back into the REPL, and you'd obtain a valid Formula.
*)
fun fm_toStr (fm : Prop Formula) =
    case fm of
       (True) => "True"
     | (False) => "False"
     | (Atom (P x)) => x
     | (Not (p)) => "Not ("^(fm_toStr p)^")"
     | (And (p,q)) => "And ("^(fm_toStr p)^", "^(fm_toStr q)^")"
     | (Or (p,q)) => "Or ("^(fm_toStr p)^", "^(fm_toStr q)^")"
     | (Implies (p,q)) => "Implies ("^(fm_toStr p)^", "^(fm_toStr q)^")"
     | (Iff (p,q)) => "Iff ("^(fm_toStr p)^", "^(fm_toStr q)^")"
     | (Forall (x,p)) => "Forall ("^x^", "^(fm_toStr p)^")"
     | (Exists (x,p)) => "Exists ("^x^", "^(fm_toStr p)^")";

fun prop_cmp (P x, P y) = String.compare(x, y);

fun prop_ord (p : Prop) (q : Prop) : int =
    case prop_cmp (p,q) of
        GREATER => 1
      | EQUAL => 0
      | LESS => ~1;

fun prop_eq (p : Prop) (q : Prop) =  (prop_cmp (p,q) = EQUAL);

fun fm_eq True True = true
  | fm_eq False False = false
  | fm_eq ((Atom x) : Prop Formula) ((Atom y) : Prop Formula) =  prop_eq x y
  | fm_eq (And(l1,r1)) (And(l2,r2)) = fm_eq l1 l2 andalso fm_eq r1 r2
  | fm_eq (Or(l1,r1)) (Or(l2,r2)) = fm_eq l1 l2 andalso fm_eq r1 r2
  | fm_eq (Implies(l1,r1)) (Implies(l2,r2)) = fm_eq l1 l2 andalso fm_eq r1 r2
  | fm_eq (Iff(l1,r1)) (Iff(l2,r2)) = fm_eq l1 l2 andalso fm_eq r1 r2
  | fm_eq (Forall(x,p)) (Forall(y,q)) = (x = y) andalso fm_eq p q
  | fm_eq (Exists(x,p)) (Exists(y,q)) = (x = y) andalso fm_eq p q
  | fm_eq _ _ = false;

fun cmp2 cmp (l1,r1) (l2,r2) =
    case cmp l1 l2 of
        LESS => LESS
      | EQUAL => cmp r1 r2
      | GREATER => GREATER;

(* This is a monster, I wish I were smarter and could write a cleaner version.
I stole Haskell's method of generating an order based on the definition's ordering of
constructors, then lexicographically ordering on the constructor's parameters.
*)
fun form_cmp True True = EQUAL
  | form_cmp False False = EQUAL
  | form_cmp True False = GREATER
  | form_cmp False True = LESS
  | form_cmp ((Atom x) : Prop Formula) True = LESS
  | form_cmp True (Atom x) = GREATER
  | form_cmp (Atom x) False = LESS
  | form_cmp False (Atom x) = GREATER
  | form_cmp (Atom x) (Atom y) = prop_cmp(x,y)
  | form_cmp True fm = GREATER
  | form_cmp False fm = GREATER
  | form_cmp (Atom _) fm = GREATER
  | form_cmp (And (p,q)) True = LESS
  | form_cmp (And (p,q)) False = LESS
  | form_cmp (And (p,q)) (Atom _) = LESS
  | form_cmp (And (l1,r1)) (And (l2,r2)) = cmp2 form_cmp (l1,r1) (l2,r2)
  | form_cmp (And _) fm = GREATER
  | form_cmp (Or _) True = LESS
  | form_cmp (Or _) False = LESS
  | form_cmp (Or _) (Atom _) = LESS
  | form_cmp (Or _) (And _) = LESS
  | form_cmp (Or (l1,r1)) (Or (l2,r2)) = cmp2 form_cmp (l1,r1) (l2,r2)
  | form_cmp (Or _) fm = GREATER
  | form_cmp (Implies _) True = LESS
  | form_cmp (Implies _) False = LESS
  | form_cmp (Implies _) (Atom _) = LESS
  | form_cmp (Implies _) (And _) = LESS
  | form_cmp (Implies _) (Or _) = LESS
  | form_cmp (Implies(l1,r1)) (Implies(l2,r2)) = cmp2 form_cmp (l1,r1) (l2,r2)
  | form_cmp (Implies _) fm = GREATER
  | form_cmp (Iff _) True = LESS
  | form_cmp (Iff _) False = LESS
  | form_cmp (Iff _) (Atom _) = LESS
  | form_cmp (Iff _) (And _) = LESS
  | form_cmp (Iff _) (Implies _) = LESS
  | form_cmp (Iff(l1,r1)) (Iff(l2,r2)) = cmp2 form_cmp (l1,r1) (l2,r2)
  | form_cmp (Iff _) fm = GREATER
  | form_cmp (Forall (x,p)) (Forall (y,q)) = if x=y then form_cmp p q
                                             else String.compare(x,y)
  | form_cmp (Forall _) (Exists _) = GREATER
  | form_cmp (Forall _) fm = LESS
  | form_cmp (Exists (x,p)) (Exists (y,q)) = if x=y then form_cmp p q
                                             else String.compare(x,y)
  | form_cmp (Exists _) fm = LESS
  | form_cmp _ _ = LESS;

fun fm_cmp (p,q) = form_cmp p q;

fun fm_ord p q = case form_cmp p q of
                     GREATER => 1
                   | EQUAL => 0
                   | LESS => ~1;

type 'a Valuation = 'a -> bool;

fun onatoms (f : 'a -> 'a Formula) (fm : 'a Formula) : 'a Formula =
    case fm of
        Atom a => f a
      | Not p => Not (onatoms f p)
      | And (p,q) => And (onatoms f p, onatoms f q)
      | Or (p,q) => Or (onatoms f p, onatoms f q)
      | Implies (p,q) => Implies (onatoms f p, onatoms f q)
      | Iff (p,q) => Iff (onatoms f p, onatoms f q);

fun overatoms (f : 'a -> 'b -> 'b) (fm : 'a Formula) (b : 'b) : 'b =
    case fm of
        Atom a => f a b
      | Not p => overatoms f p b
      | And (p,q) => overatoms f p (overatoms f q b)
      | Or (p,q) => overatoms f p (overatoms f q b)
      | Implies (p,q) => overatoms f p (overatoms f q b)
      | Iff (p,q) => overatoms f p (overatoms f q b)
      | Forall (x,p) => overatoms f p b
      | Exists (x,p) => overatoms f p b
      | _ => b;

(* eval : 'a Formula -> 'a Valuation -> bool *)
fun eval (fm : 'a Formula) (v : 'a Valuation) =
    case fm of
        False => false
      | True => true
      | Atom x => v(x)
      | Not p => not (eval p v)
      | And (p,q) => (eval p v) andalso (eval q v)
      | Or (p,q) => (eval p v) orelse (eval q v)
      | Implies (p,q) => not (eval p v) orelse (eval q v)
      | Iff (p,q) => (eval p v) = (eval q v);

fun eval_example () =
    let val p = Atom (P "p")
        val q = Atom (P "q")
        val r = Atom (P "r")
    in eval (Implies (And (p,q), And (q,r))) (fn P "p" => true |
                                              P "q" => false |
                                              P "r" => true |
                                              _ => false)
    end;

(* Default valuation, with everything evaluated to false. *)
val false_v : 'a Valuation = (fn _ => false);

(* Merge sort related functions *)
fun merge cmp ([], ys) = ys
  | merge cmp (xs, []) = xs
  | merge cmp (xs as x::xs', ys as y::ys') =
      case cmp (x, y) of
           GREATER => y :: merge cmp (xs, ys')
         | _       => x :: merge cmp (xs', ys);

fun sort cmp [] = []
  | sort cmp [x] = [x]
  | sort cmp xs =
    let
      val ys = List.take (xs, length xs div 2)
      val zs = List.drop (xs, length xs div 2)
    in
      merge cmp (sort cmp ys, sort cmp zs)
    end;

(* Make a list of unique values. *)
fun uniq (xs: 'a list) (eq : 'a -> 'a -> bool) =
    let fun check [] item = false
          | check (x::xs) item = (eq item x) orelse check xs item
        fun go_through [] = []
          | go_through (x::xs) = if check xs x
                                 then go_through xs
                                 else x :: go_through xs
    in
        go_through xs
    end;

(* In OCaml and F# the comparison is build in to the language. It is not
in SML, so many of the following functions also take an ordering
function as input. *)

(* setify : 'a order -> 'a list -> 'a list; *)
fun setify (ord : 'a -> 'a -> int) (l : 'a list) : 'a list =
    let fun canonical lis =
            case lis of
                x::(rest as y::_) => ord x y < 0 andalso canonical rest
              | _ => true
        fun ord_cmp (x,y) = if ord x y < 0 then LESS
                            else if ord x y > 0 then GREATER
                            else EQUAL
        fun eq x y = (ord x y = 0)
    in
        if canonical l then l
        else uniq (sort ord_cmp l) eq
    end;

fun atom_union (ord : 'b -> 'b -> int) (f : 'a -> 'b list) (fm : 'a Formula) =
    setify ord (overatoms (fn h => fn t => f(h)@t) fm []);

fun atoms (fm : Prop Formula) : Prop list =
    atom_union prop_ord (fn a => [a]) fm;

fun on_all_valuations (subfn : 'a Valuation -> bool) (v : 'a Valuation) eq =
    fn [] => subfn v
  | (p::ps) => let fun v' t q = if eq q p then t else v(q)
               in on_all_valuations subfn (v' false) eq ps andalso
                  on_all_valuations subfn (v' true) eq ps
               end;

val fm1 =
    let val p = Atom (P "p")
        val q = Atom (P "q")
        val r = Atom (P "r")
        val s = Atom (P "s")
    in Iff (Or(And(p,q),s),
            Or(Not p,
               Iff (r,s)))
    end;

fun atoms_test1 () =
    atoms fm1;

(** Satisfiability-related functions **)
fun tautology fm =
    on_all_valuations (eval fm) false_v prop_eq (atoms fm);

fun unsatisfiable fm = tautology (Not fm);
fun satisfiable fm = not (unsatisfiable fm);

val lem_fm =
    let val p = Atom(P"p")
    in
        Or(p, Not(p))
    end;
val fm2 =
    let val p = Atom(P"p")
        val q = Atom(P"q")
    in
        Implies(Or(p,q),p)
    end;
val fm3 =
    let val p = Atom(P"p")
        val q = Atom(P"q")
    in Implies(Or(p,q), Or(q, Iff(p,q)))
    end;
val fm4 =
    let val p = Atom(P"p")
        val q = Atom(P"q")
        val r = Atom(P"r")
    in
        Implies(And(Or(p,q), Not(And(p,q))),
                Iff(Not(p),q))
    end;
val fm5 =
    let val p = Atom(P"p");
        val q = Atom(P"q");
        val r = Atom(P"r");
    in And(Or(p,And(q,r)),
           Or(Not p, Not r))
    end;

(* Partial function application *)
fun tryapplyd (f : 'a -> 'b option) (x : 'a) (v : 'b) : 'b =
    case f x of
        (SOME y) => y
      | NONE => v;

infix 6 |=>;
infix 6 |->;

fun (x |-> y) eq f = (fn x' => if eq x x' then SOME y else f x);
fun (x |=> y) eq = (x |-> y) eq (fn _ => NONE);

(* val psubst : ('a, 'a formula) func -> 'a formula -> 'a formula *)
fun psubst subfn = onatoms (fn p => tryapplyd subfn p (Atom p));

fun psubst_ex () =
    psubst ((P "p" |=> fm1) prop_eq) fm3;

(*** Negation normal form ***)

fun dual False = True
  | dual True = False
  | dual (Atom p) = (Atom p)
  | dual (Not p) = Not (dual p)
  | dual (And (p,q)) = Or(dual p, dual q)
  | dual (Or (p,q)) = And(dual p, dual q)
  | dual _ = raise (Fail "Formula involves connectives ==> or <=>");

(* Recursively simplify a proposition by using tautologies like double negation, etc.
 *)
local
    fun psimplify1 (Not False) = True
      | psimplify1 (Not True) = False
      | psimplify1 (Not (Not p)) = p
      | psimplify1 (And (p, False)) = False
      | psimplify1 (And (False,p)) = False
      | psimplify1 (And (p,True)) = p
      | psimplify1 (And (True,p)) = p
      | psimplify1 (Or (p,False)) = p
      | psimplify1 (Or (False,p)) = p
      | psimplify1 (Or (p,True)) = True
      | psimplify1 (Or (True,p)) = True
      | psimplify1 (Implies (False,p)) = True
      | psimplify1 (Implies (p,True)) = True
      | psimplify1 (Implies (True,p)) = p
      | psimplify1 (Implies (p,False)) = Not p
      | psimplify1 (Iff (p,True)) = p
      | psimplify1 (Iff (True,p)) = p
      | psimplify1 (Iff (False,False)) = True
      | psimplify1 (Iff (p,False)) = Not p
      | psimplify1 (Iff (False,p)) = Not p
      | psimplify1 fm = fm
in
fun psimplify (Not p) = psimplify1 (Not (psimplify p))
  | psimplify (And (p,q)) = psimplify1 (And(psimplify p,psimplify q))
  | psimplify (Or (p,q)) = psimplify1 (Or(psimplify p,psimplify q))
  | psimplify (Implies (p,q)) = psimplify1 (Implies(psimplify p,psimplify q))
  | psimplify (Iff(p,q)) = psimplify1 (Iff(psimplify p,psimplify q))
  | psimplify fm = fm
end;

fun psimp_ex () =
    let val x = Atom (P "x")
        val y = Atom (P "y")
        val z = Atom (P "z")
    in
        [psimplify (Implies (Implies(True, Iff(x,False)),
                             Not(Or(y, And(False,z))))),
         psimplify (Or(Implies(Implies(x,y),True),
                       Not False))]
    end;

(* Tests if a literal is positive or negative. *)
fun negative (Not p) = true
  | negative _ = false;

fun positive (lit : 'a Formula) : bool = not(negative lit);

fun negate (Not p) = p
  | negate p = Not p;

(* Transform a formula into Negation Normal Form. *)
local
    fun nnf1 (And (p,q)) = And(nnf1 p, nnf1 q)
      | nnf1 (Or (p,q)) = Or(nnf1 p, nnf1 q)
      | nnf1 (Implies (p,q)) = Or(nnf1 (Not p),nnf1 q)
      | nnf1 (Iff(p,q)) = Or(And(nnf1 p,nnf1 q),
                             And(nnf1 (Not p), nnf1 (Not q)))
      | nnf1 (Not(Not p)) = nnf1 p
      | nnf1 (Not(And(p,q))) = Or(nnf1 (Not p), nnf1 (Not q))
      | nnf1 (Not(Or(p,q))) = And(nnf1 (Not p), nnf1 (Not q))
      | nnf1 (Not(Implies(p,q))) = And(nnf1 p, nnf1(Not q))
      | nnf1 (Not(Iff(p,q))) = Or(And(nnf1 p,nnf1(Not q)),
                                  And(nnf1(Not p),nnf1 q))
      | nnf1 fm = fm
in
fun nnf fm = nnf1 (psimplify fm)
end;


local
    fun nenf1 (Not(Not p)) = nenf1 p
      | nenf1 (Not(And(p,q))) = Or(nenf1(Not p),nenf1(Not q))
      | nenf1 (Not(Or(p,q))) = And(nenf1(Not p),nenf1(Not q))
      | nenf1 (Not(Implies(p,q))) = And(nenf1 p,nenf1(Not q))
      | nenf1 (Not(Iff(p,q))) = Iff(nenf1 p,nenf1(Not q))
      | nenf1 (And(p,q)) = And(nenf1 p,nenf1 q)
      | nenf1 (Or(p,q)) = Or(nenf1 p,nenf1 q)
      | nenf1 (Implies(p,q)) = Or(nenf1(Not p),nenf1 q)
      | nenf1 (Iff(p,q)) = Iff(nenf1 p,nenf1 q)
      | nenf1 fm = fm
in
fun nenf fm = nenf(psimplify fm)
end;

(*** DNF and CNF ***)
(* We now need to transform a formula into a conjunction of clauses, or
disjunction of...disjuncts...in reality, we will be using lists of literals to encode
clauses or disjuncts. So we need to transform a formula to a list of literals
(or a list of lists of literals), and vice-versa.
*)
fun list_conj [] = True
  | list_conj (l::[]) = l
  | list_conj (l::ls) = foldr And l ls;

fun list_disj [] = False
  | list_disj (l::[]) = l
  | list_disj (l::ls) = foldr Or l ls;

fun mk_lits pvs v =
    list_conj (map (fn p => if eval p v then p else Not p) pvs);

(* Produce a list of valuations satisfying a `subfn : 'a Valuation -> bool`. *)
fun all_sat_valuations subfn v eq [] = if subfn v then [v] else []
  | all_sat_valuations subfn v eq (p::ps) =
    let fun v' t q = if eq q p then t else v(q)
    in (all_sat_valuations subfn (v' false) eq ps) @
       (all_sat_valuations subfn (v' true) eq ps)
    end;

fun dnf fm =
    let val pvs = atoms fm
        val satvals = all_sat_valuations (eval fm) (fn _ => false) prop_eq pvs
    in
        list_disj (map (mk_lits (map (fn p => Atom p) pvs)) satvals)
    end;

fun rawdnf fm =
let
    fun distrib (And(p,Or(q,r))) = Or(distrib(And(p,q)),distrib(And(p,r)))
      | distrib (And(Or(p,q),r)) = Or(distrib(And(p,r)),distrib(And(q,r)))
      | distrib fm = fm
in
    case fm of
        (And(p,q)) => distrib(And(rawdnf p, rawdnf q))
      | (Or(p,q)) => Or(rawdnf p,rawdnf q)
      | _ => fm
end;

fun rawdnf_ex () =
    let val p = Atom (P "p")
        val q = Atom (P "q")
        val r = Atom (P "r")
    in rawdnf (And(Or(p,And(q,r)),
                   Or(Not p, Not r)))
    end;

(* set-based DNF *)
fun union (ord : 'a -> 'a -> int) (l : 'a list) (r : 'a list) : 'a list =
    let fun cmp (x,y) = if ord x y < 0 then LESS
                        else if ord x y > 0 then GREATER
                        else EQUAL
        fun u l [] = l
          | u [] r =  r
          | u (l as h1::t1) (r as h2::t2) = case cmp (h1,h2) of
                                                EQUAL => h1 :: (u t1 t2)
                                              | LESS => h1 :: (u t1 r)
                                              | GREATER => h2 :: (u l t2)
    in u (setify ord l) (setify ord r)
    end;

(* allpairs : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list *)
fun allpairs (f : 'a -> 'b -> 'c) ([] : 'a list) (l2 : 'b list) = []
  | allpairs f (h1::t1) l2 = foldr (fn (x,a) => f h1 x :: a) (allpairs f t1 l2) l2;

fun clause_ord [] r = ~1
  | clause_ord l [] = 1
  | clause_ord (h1::t1 : Prop Formula list) (h2::t2 : Prop Formula list) =
    case form_cmp h1 h2 of
        EQUAL => clause_ord t1 t2
      | LESS => ~1
      | GREATER => 1;

fun pure_distrib (s1 : Prop Formula list list) (s2 : Prop Formula list list)
    : Prop Formula list list
    = setify clause_ord (allpairs (union fm_ord) s1 s2);

fun purednf (fm : Prop Formula) : Prop Formula list list =
    case fm of
        And(p,q) => pure_distrib (purednf p) (purednf q)
      | Or(p,q) => union clause_ord (purednf p) (purednf q)
      | _ => [[fm]];

fun non p x = not(p x);

fun intersect cmp [] l2 = []
  | intersect cmp l1 [] = []
  | intersect cmp l r =
    let fun inter (l1 as h1::t1) (l2 as h2::t2) =
            (case cmp(h1,h2) of
                EQUAL => h1::(intersect cmp t1 t2)
              | LESS => intersect cmp t1 l2
              | GREATER => intersect cmp l1 t2)
        fun ord x y =
            (case cmp(x,y) of
               EQUAL => 0
             | GREATER => 1
             | LESS => ~1)
    in inter (setify ord l) (setify ord r)
    end;

fun trivial (lits : Prop Formula list) : bool =
    let val (pos,neg) = List.partition positive lits
    in not (null (intersect fm_cmp pos (map negate neg)))
    end;

fun pure_dnf_ex () =
    let val p = Atom (P "p")
        val q = Atom (P "q")
        val r = Atom (P "r")
    in purednf (And (Or (p, And(q,r)),
                     (Or(Not p, Not r))))
    end;

fun isSubset (ord : 'a -> 'a -> int) (xs1 : 'a list) (xs2 : 'a list) : bool =
    case (xs1,xs2) of
        ([], l2) => true
      | (l1,[]) => false
      | (h1::t1,h2::t2) =>
        (let val r = ord h1 h2
         in if r = 0 then isSubset ord t1 t2
            else if r < 0 then false
            else isSubset ord xs1 t2
         end);

fun isProperSubset (ord : 'a -> 'a -> int) (xs1 : 'a list) (xs2 : 'a list) : bool =
    let fun isProp [] l2 = false
          | isProp l1 [] = true
          | isProp (l1 as h1::t1) (h2::t2) =
            (let val r = ord h1 h2
             in if r = 0 then isProp t1 t2
                else if r < 0 then false
                else isSubset ord l1 t2
             end)
    in isProp (setify ord xs1) (setify ord xs2)
    end;

fun simp_dnf False = []
  | simp_dnf True = [[]]
  | simp_dnf fm =
    let val djs = List.filter (non trivial) (purednf (nnf fm))
    in List.filter (fn d => not(List.exists (fn d' => isProperSubset fm_ord d' d) djs))
              djs
    end;

fun dnf fm = list_disj (map list_conj (simp_dnf fm));


fun dnf_ex () =
    let val p = Atom (P "p")
        val q = Atom (P "q")
        val r = Atom (P "r")
    in dnf (And (Or (p, And(q,r)),
                 (Or(Not p, Not r))))
    end;

fun pure_cnf fm = map (map negate) (purednf (nnf (Not fm)));

fun simpcnf False = [[]]
  | simpcnf True = []
  | simpcnf fm =
    let val cjs = List.filter (non trivial) (pure_cnf fm)
    in List.filter (fn c => not(List.exists (fn c' => isProperSubset fm_ord c' c)
                                            cjs))
                   cjs
    end;

fun cnf fm = list_conj(map list_disj (simpcnf fm));

val fm6 =
    let val p = Atom (P "p")
        val q = Atom (P "q")
        val r = Atom (P "r")
    in And (Or (p, And(q,r)),
            (Or(Not p, Not r)))
    end;

val fm7 =
    let val p = Atom (P "p")
        val q = Atom (P "q")
        val r = Atom (P "r")
        val s = Atom (P "s")
    in And (Or (p, And(q,Not r)),
            s)
    end;

fun cnf_ex () =
    let val p = Atom (P "p")
        val q = Atom (P "q")
        val r = Atom (P "r")
    in cnf (And (Or (p, And(q,r)),
                 (Or(Not p, Not r))))
    end;