(* ========================================================================= *)
(* Simple implementation of Stalmarck's algorithm. *)
(* *)
(* NB! This algorithm is patented for commercial use (not that a toy version *)
(* like this would actually be useful in practice). See US patent 5 276 897, *)
(* Swedish patent 467 076 and European patent 0403 454 for example. *)
(* *)
(* Copyright (c) 2003, John Harrison. (See "LICENSE.txt" for details.) *)
(* ========================================================================= *)
(* ------------------------------------------------------------------------- *)
(* Triplet transformation, using functions defined earlier. *)
(* ------------------------------------------------------------------------- *)
let triplicate fm =
let fm' = nenf(psimplify fm) in
let n = Int 1 +/ overatoms (max_varindex "p_" ** pname) fm' (Int 0) in
let (p,defs,_) = maincnf false (fm',undefined,n) in
p,map (snd ** snd) (funset defs);;
(* ------------------------------------------------------------------------- *)
(* Automatically generate triggering rules to save writing them out. *)
(* ------------------------------------------------------------------------- *)
let atom lit = if negative lit then negate lit else lit;;
let rec align (p,q) =
if atom p < atom q then align(q,p) else
if negative p then (negate p,negate q) else (p,q);;
let equate2 (p,q) eqv = equate (negate p,negate q) (equate (p,q) eqv);;
let rec irredundant rel eqs =
match eqs with
[] -> []
| (p,q)::oth ->
if canonize rel p = canonize rel q then irredundant rel oth
else insert (p,q) (irredundant (equate2 (p,q) rel) oth);;
let consequences peq fm eqs =
let pq = (fun (p,q) -> Iff(p,q)) peq in
let raw = filter
(fun (r,s) -> tautology(Imp(And(pq,fm),Iff(r,s)))) eqs in
irredundant (equate2 peq unequal) raw;;
let triggers fm =
let poslits = insert True (map (fun p -> Atom p) (atoms fm)) in
let lits = union poslits (map (fun p -> Not p) poslits) in
let pairs = allpairs (fun p q -> p,q) lits lits in
let npairs = filter (fun (p,q) -> atom p <> atom q) pairs in
let eqs = setify(map align npairs) in
let raw = map (fun p -> p,consequences p fm eqs) eqs in
filter (fun (p,c) -> c <> []) raw;;
(* ------------------------------------------------------------------------- *)
(* An example. *)
(* ------------------------------------------------------------------------- *)
START_INTERACTIVE;;
triggers <
(q /\ r)>>;;
END_INTERACTIVE;;
(* ------------------------------------------------------------------------- *)
(* Precompute and instantiate triggers for standard triplets. *)
(* ------------------------------------------------------------------------- *)
let ddnegate fm = match fm with Not(Not p) -> p | _ -> fm;;
let trigger =
let [trig_and; trig_or; trig_imp; trig_iff] =
map triggers
[<
q /\ r>>; <
q \/ r>>;
<
(q ==> r)>>; <
(q <=> r)>>]
and p = <
> and q = <> and r = <> in
let inst_fn [x;y;z] =
let subfn = fpf [P"p" |-> x; P"q" |-> y; P"r" |-> z] in
ddnegate ** propsubst subfn in
let inst2_fn i (p,q) = align(inst_fn i p,inst_fn i q) in
let instn_fn i (a,c) = inst2_fn i a,map (inst2_fn i) c in
let inst_trigger = map ** instn_fn in
function (Iff(x,And(y,z))) -> inst_trigger [x;y;z] trig_and
| (Iff(x,Or(y,z))) -> inst_trigger [x;y;z] trig_or
| (Iff(x,Imp(y,z))) -> inst_trigger [x;y;z] trig_imp
| (Iff(x,Iff(y,z))) -> inst_trigger [x;y;z] trig_iff;;
(* ------------------------------------------------------------------------- *)
(* Finding variables in triggers, prioritized by fecundity estimate. *)
(* ------------------------------------------------------------------------- *)
let rec fecundity ((p,q),conseqs) f =
let vars = union (atoms p) (atoms q) in
let n = (if atom q = True then 2 else 1) * length conseqs in
itlist (fun x -> (x |-> n + tryapplyd f x 0)) vars f;;
let variable_list trigs =
let fec = itlist fecundity trigs undefined in
let repcounts = funset fec in
map (fun (p,q) -> Atom p)
(sort (fun (_,n) (_,m) -> m <= n) repcounts);;
(* ------------------------------------------------------------------------- *)
(* Compute a function mapping each variable/true to relevant triggers. *)
(* ------------------------------------------------------------------------- *)
let insert_relevant p trg f = (p |-> insert trg (tryapplyl f p)) f;;
let insert_relevant2 ((p,q),_ as trg) f =
insert_relevant p trg (insert_relevant q trg f);;
let relevance trigs =
let vars = variable_list trigs
and rfn = itlist insert_relevant2 trigs undefined in
vars,rfn;;
(* ------------------------------------------------------------------------- *)
(* Merging of equiv classes and relevancies. *)
(* ------------------------------------------------------------------------- *)
let equatecons (p0,q0) (eqv,rfn as erf) =
let p = canonize eqv p0
and q = canonize eqv q0 in
if p = q then [],erf else
let p' = canonize eqv (negate p0)
and q' = canonize eqv (negate q0) in
let eqv' = equate2(p,q) eqv
and sp_pos = tryapplyl rfn p
and sp_neg = tryapplyl rfn p'
and sq_pos = tryapplyl rfn q
and sq_neg = tryapplyl rfn q' in
let rfn' = itlist identity
[canonize eqv' p |-> union sp_pos sq_pos;
canonize eqv' p' |-> union sp_neg sq_neg] rfn in
let nw = union (intersect sp_pos sq_pos) (intersect sp_neg sq_neg) in
itlist (union ** snd) nw [],(eqv',rfn');;
(* ------------------------------------------------------------------------- *)
(* Zero-saturation given an equivalence/relevance and new assignments. *)
(* ------------------------------------------------------------------------- *)
let rec zero_saturate erf assigs =
match assigs with
[] -> erf
| (p,q)::ts ->
let news,erf' = equatecons (p,q) erf in
zero_saturate erf' (union ts news);;
(* ------------------------------------------------------------------------- *)
(* Zero-saturate then check for contradictoriness. *)
(* ------------------------------------------------------------------------- *)
let contraeq pfn =
let vars = filter positive (equated pfn) in
exists (fun x -> canonize pfn x = canonize pfn (Not x)) vars;;
let zero_saturate_and_check erf trigs =
let (eqv',rfn' as erf') = zero_saturate erf trigs in
if contraeq eqv' then snd(equatecons (True,Not True) erf') else erf';;
(* ------------------------------------------------------------------------- *)
(* Iterated equivalening over a set. *)
(* ------------------------------------------------------------------------- *)
let rec equateset s0 eqfn =
match s0 with
a::(b::s2 as s1) ->
equateset s1 (snd(equatecons (a,b) eqfn))
| _ -> eqfn;;
(* ------------------------------------------------------------------------- *)
(* Intersection operation on equivalence classes and relevancies. *)
(* ------------------------------------------------------------------------- *)
let rec inter els (eq1,_ as erf1) (eq2,_ as erf2) rev1 rev2 erf =
match els with
[] -> erf
| x::xs ->
let (b1,n1) = tryterminus eq1 x
and (b2,n2) = tryterminus eq2 x in
let s1 = apply rev1 b1 and s2 = apply rev2 b2 in
let s = intersect s1 s2 in
inter (subtract xs s) erf1 erf2 rev1 rev2
(if s = [x] then erf else equateset s erf);;
(* ------------------------------------------------------------------------- *)
(* Reverse the equivalence mappings. *)
(* ------------------------------------------------------------------------- *)
let reverseq domain eqv =
let al = map (fun x -> x,canonize eqv x) domain in
itlist (fun (y,x) f -> (x |-> insert y (tryapplyl f x)) f)
al undefined;;
(* ------------------------------------------------------------------------- *)
(* Special intersection taking contradictoriness into account. *)
(* ------------------------------------------------------------------------- *)
let truefalse pfn = canonize pfn (Not True) = canonize pfn True;;
let stal_intersect (eq1,_ as erf1) (eq2,_ as erf2) erf =
if truefalse eq1 then erf2
else if truefalse eq2 then erf1 else
let dom1 = equated eq1 and dom2 = equated eq2 in
let comdom = intersect dom1 dom2 in
let rev1 = reverseq dom1 eq1 and rev2 = reverseq dom2 eq2 in
inter comdom erf1 erf2 rev1 rev2 erf;;
(* ------------------------------------------------------------------------- *)
(* General n-saturation for n >= 1 *)
(* ------------------------------------------------------------------------- *)
let saturate allvars =
let rec saturate n erf assigs =
let (eqv',_ as erf') = zero_saturate_and_check erf assigs in
if n = 0 or truefalse eqv' then erf' else
let (eqv'',_ as erf'') = splits n erf' allvars in
if eqv'' = eqv' then erf''
else saturate n erf'' []
and splits n (eqv,_ as erf) vars =
match vars with
[] -> erf
| p::ovars ->
if canonize eqv p <> p then splits n erf ovars else
let erf0 = saturate (n - 1) erf [p,Not True]
and erf1 = saturate (n - 1) erf [p,True] in
let (eqv',_ as erf') = stal_intersect erf0 erf1 erf in
if truefalse eqv' then erf'
else splits n erf' ovars in
saturate;;
(* ------------------------------------------------------------------------- *)
(* Cleaning up the triggers to represent the equivalence relation. *)
(* ------------------------------------------------------------------------- *)
let minatom fms =
match fms with
fm::ofms ->
itlist (fun x y -> if atom x < atom y then x else y) ofms fm
| _ -> failwith "minatom: empty list";;
let realcanon eqv =
let domain = equated eqv in
let rev = reverseq domain eqv in
itlist (fun x -> (x |-> minatom(apply rev (canonize eqv x)))) domain
undefined;;
let substitute eqv =
let cfn = tryapply(realcanon eqv) in
fun (p,q) -> align(cfn p,cfn q);;
let rec cleanup subfn trigs =
match trigs with
[] -> []
| ((p,q),conseqs)::otr ->
let (p',q') = subfn (p,q) in
if p' = q' or p = negate q' then cleanup subfn otr else
let conseqs' = map subfn conseqs in
let useful,triv =
partition (fun (p,q) -> atom p <> atom q) conseqs' in
let news =
if exists (fun (p,q) -> p = negate q) triv
then (p',q'),[align(True,Not True)]
else (p',q'),useful in
insert news (cleanup subfn otr);;
(* ------------------------------------------------------------------------- *)
(* Saturate up to a limit. *)
(* ------------------------------------------------------------------------- *)
let rec saturate_upto n m trigs assigs =
if n > m then
(print_string("%%% Too deep for "^(string_of_int m)^"-saturation");
print_newline();
false)
else
(print_string("*** Starting "^(string_of_int n)^"-saturation");
print_newline();
let vars,rfn = relevance trigs in
let (eqv',rfn') = saturate vars n (unequal,rfn) assigs in
if truefalse eqv' then true else
let trigs' = cleanup (substitute eqv') trigs in
saturate_upto (n + 1) m trigs' []);;
(* ------------------------------------------------------------------------- *)
(* Overall function. *)
(* ------------------------------------------------------------------------- *)
let include_trigger (eq,conseqs) f =
(eq |-> union conseqs (tryapplyl f eq)) f;;
let stalmarck fm =
let fm' = psimplify(Not fm) in
if fm' = False then true else if fm' = True then false else
let p,triplets = triplicate fm' in
let trigfn = itlist (itlist include_trigger ** trigger)
triplets undefined in
saturate_upto 0 2 (funset trigfn) [p,True];;
(* ------------------------------------------------------------------------- *)
(* Try the primality examples. *)
(* ------------------------------------------------------------------------- *)
START_INTERACTIVE;;
do_list (time stalmarck)
[prime 5;
prime 13;
prime 23;
prime 43;
prime 97];;
END_INTERACTIVE;;
(* ------------------------------------------------------------------------- *)
(* Artifical example of Urquhart formulas. *)
(* ------------------------------------------------------------------------- *)
let urquhart n =
let pvs = map (fun n -> Atom(P("p_"^(string_of_int n)))) (1 -- n) in
end_itlist (fun p q -> Iff(p,q)) (pvs @ pvs);;
START_INTERACTIVE;;
map (time stalmarck ** urquhart) [1;2;4;8;16];;
END_INTERACTIVE;;