(* ========================================================================= *)
(* Backchaining procedure for Horn clauses, and toy Prolog implementation. *)
(* *)
(* Copyright (c) 2003, John Harrison. (See "LICENSE.txt" for details.) *)
(* ========================================================================= *)
(* ------------------------------------------------------------------------- *)
(* Rename a rule. *)
(* ------------------------------------------------------------------------- *)
let renamer k (asm,c) =
let fvs = fv(list_conj(c::asm)) in
let n = length fvs in
let vvs = map (fun i -> "_" ^ string_of_int i) (k -- (k+n-1)) in
let inst = formsubst(instantiate fvs (map (fun x -> Var x) vvs)) in
(map inst asm,inst c),k+n;;
(* ------------------------------------------------------------------------- *)
(* Basic prover for Horn clauses based on backchaining with unification. *)
(* ------------------------------------------------------------------------- *)
let rec backchain rules n k env goals =
match goals with
[] -> env
| g::gs ->
if n = 0 then failwith "Too deep" else
tryfind (fun rule ->
let (a,c),k' = renamer k rule in
backchain rules (n - 1) k' (unify_literals env (c,g)) (a @ gs))
rules;;
let hornify cls =
let pos,neg = partition positive cls in
if length pos > 1 then failwith "non-Horn clause"
else (map negate neg,if pos = [] then False else hd pos);;
let hornprove fm =
let rules = map hornify (clausal(skolemize(Not(generalize fm)))) in
deepen (fun n -> backchain rules n 0 undefined [False],n) 0;;
(* ------------------------------------------------------------------------- *)
(* Some Horn examples. *)
(* ------------------------------------------------------------------------- *)
START_INTERACTIVE;;
let p1 = hornprove
<
q <=> ~q ==> ~p>>;;
let p18 = hornprove
< P(x)>>;;
let p32 = hornprove
<<(forall x. P(x) /\ (G(x) \/ H(x)) ==> Q(x)) /\
(forall x. Q(x) /\ H(x) ==> J(x)) /\
(forall x. R(x) ==> H(x)) ==>
(forall x. P(x) /\ R(x) ==> J(x))>>;;
END_INTERACTIVE;;
(* ------------------------------------------------------------------------- *)
(* Parsing rules in a Prolog-like syntax. *)
(* ------------------------------------------------------------------------- *)
let parserule s =
let c,rest = parse_formula parse_atom [] (lex(explode s)) in
let asm,rest1 =
if rest <> [] & hd rest = ":-"
then parse_list "," (parse_formula parse_atom []) (tl rest)
else [],rest in
if rest1 = [] then (asm,c) else failwith "Extra material after rule";;
(* ------------------------------------------------------------------------- *)
(* Prolog interpreter: just use depth-first search not iterative deepening. *)
(* ------------------------------------------------------------------------- *)
let simpleprolog rules gl =
backchain (map parserule rules) (-1) 0 undefined [parse gl];;
(* ------------------------------------------------------------------------- *)
(* ML version of the first Prolog example. *)
(* ------------------------------------------------------------------------- *)
type numeral = Z | S of numeral;;
let rec less_or_equal =
function (Z,x) -> true
| (S(x),S(y)) -> less_or_equal (x,y);;
(* ------------------------------------------------------------------------- *)
(* Ordering example. *)
(* ------------------------------------------------------------------------- *)
START_INTERACTIVE;;
let lerules = ["0 <= X"; "S(X) <= S(Y) :- X <= Y"];;
simpleprolog lerules "S(S(0)) <= S(S(S(0)))";;
let env = simpleprolog lerules "S(S(0)) <= X";;
apply env "X";;
END_INTERACTIVE;;
(* ------------------------------------------------------------------------- *)
(* With instantiation collection to produce a more readable result. *)
(* ------------------------------------------------------------------------- *)
let prolog rules gl =
let i = solve(simpleprolog rules gl) in
mapfilter (fun x -> Atom(R("=",[Var x; apply i x]))) (fv(parse gl));;
(* ------------------------------------------------------------------------- *)
(* Example again. *)
(* ------------------------------------------------------------------------- *)
START_INTERACTIVE;;
prolog lerules "S(S(0)) <= X";;
(* ------------------------------------------------------------------------- *)
(* Append example, showing symmetry between inputs and outputs. *)
(* ------------------------------------------------------------------------- *)
let appendrules =
["append(nil,L,L)"; "append(H::T,L,H::A) :- append(T,L,A)"];;
prolog appendrules "append(1::2::nil,3::4::nil,Z)";;
prolog appendrules "append(1::2::nil,Y,1::2::3::4::nil)";;
prolog appendrules "append(X,3::4::nil,1::2::3::4::nil)";;
prolog appendrules "append(X,Y,1::2::3::4::nil)";;
(* ------------------------------------------------------------------------- *)
(* A sorting example (from Lloyd's "Foundations of Logic Programming"). *)
(* ------------------------------------------------------------------------- *)
let sortrules =
["sort(X,Y) :- perm(X,Y),sorted(Y)";
"sorted(nil)";
"sorted(X::nil)";
"sorted(X::Y::Z) :- X <= Y, sorted(Y::Z)";
"perm(nil,nil)";
"perm(X::Y,U::V) :- delete(U,X::Y,Z), perm(Z,V)";
"delete(X,X::Y,Y)";
"delete(X,Y::Z,Y::W) :- delete(X,Z,W)";
"0 <= X";
"S(X) <= S(Y) :- X <= Y"];;
prolog sortrules "sort(S(0)::0::nil,X)";;
prolog sortrules "sort(S(0)::S(S(0))::0::nil,X)";;
prolog sortrules
"sort(S(S(S(S(0))))::S(0)::0::S(S(0))::S(0)::nil,X)";;
END_INTERACTIVE;;