-- | Backchaining procedure for Horn clauses, and toy Prolog implementation. {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wall #-} module Data.Logic.ATP.Prolog where import Data.List as List (map) import Data.Logic.ATP.Apply (HasApply(TermOf)) import Data.Logic.ATP.FOL (var, lsubst) import Data.Logic.ATP.Formulas (IsFormula(AtomOf)) -- import Data.Logic.ATP.Lib (deepen) import Data.Logic.ATP.Lit (IsLiteral, JustLiteral) import Data.Logic.ATP.Term (IsTerm(TVarOf), vt) import Data.Map.Strict as Map import Data.Set as Set import Data.String (fromString) import Test.HUnit data PrologRule lit = Prolog (Set lit) lit deriving (PrologRule lit -> PrologRule lit -> Bool (PrologRule lit -> PrologRule lit -> Bool) -> (PrologRule lit -> PrologRule lit -> Bool) -> Eq (PrologRule lit) forall lit. Eq lit => PrologRule lit -> PrologRule lit -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a $c== :: forall lit. Eq lit => PrologRule lit -> PrologRule lit -> Bool == :: PrologRule lit -> PrologRule lit -> Bool $c/= :: forall lit. Eq lit => PrologRule lit -> PrologRule lit -> Bool /= :: PrologRule lit -> PrologRule lit -> Bool Eq, Eq (PrologRule lit) Eq (PrologRule lit) => (PrologRule lit -> PrologRule lit -> Ordering) -> (PrologRule lit -> PrologRule lit -> Bool) -> (PrologRule lit -> PrologRule lit -> Bool) -> (PrologRule lit -> PrologRule lit -> Bool) -> (PrologRule lit -> PrologRule lit -> Bool) -> (PrologRule lit -> PrologRule lit -> PrologRule lit) -> (PrologRule lit -> PrologRule lit -> PrologRule lit) -> Ord (PrologRule lit) PrologRule lit -> PrologRule lit -> Bool PrologRule lit -> PrologRule lit -> Ordering PrologRule lit -> PrologRule lit -> PrologRule lit forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a forall lit. Ord lit => Eq (PrologRule lit) forall lit. Ord lit => PrologRule lit -> PrologRule lit -> Bool forall lit. Ord lit => PrologRule lit -> PrologRule lit -> Ordering forall lit. Ord lit => PrologRule lit -> PrologRule lit -> PrologRule lit $ccompare :: forall lit. Ord lit => PrologRule lit -> PrologRule lit -> Ordering compare :: PrologRule lit -> PrologRule lit -> Ordering $c< :: forall lit. Ord lit => PrologRule lit -> PrologRule lit -> Bool < :: PrologRule lit -> PrologRule lit -> Bool $c<= :: forall lit. Ord lit => PrologRule lit -> PrologRule lit -> Bool <= :: PrologRule lit -> PrologRule lit -> Bool $c> :: forall lit. Ord lit => PrologRule lit -> PrologRule lit -> Bool > :: PrologRule lit -> PrologRule lit -> Bool $c>= :: forall lit. Ord lit => PrologRule lit -> PrologRule lit -> Bool >= :: PrologRule lit -> PrologRule lit -> Bool $cmax :: forall lit. Ord lit => PrologRule lit -> PrologRule lit -> PrologRule lit max :: PrologRule lit -> PrologRule lit -> PrologRule lit $cmin :: forall lit. Ord lit => PrologRule lit -> PrologRule lit -> PrologRule lit min :: PrologRule lit -> PrologRule lit -> PrologRule lit Ord) -- ------------------------------------------------------------------------- -- Rename a rule. -- ------------------------------------------------------------------------- renamerule :: forall lit atom term v. (IsLiteral lit, JustLiteral lit, Ord lit, HasApply atom, IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Int -> PrologRule lit -> (PrologRule lit, Int) renamerule :: forall lit atom term v. (IsLiteral lit, JustLiteral lit, Ord lit, HasApply atom, IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Int -> PrologRule lit -> (PrologRule lit, Int) renamerule Int k (Prolog Set lit asm lit c) = (Set lit -> lit -> PrologRule lit forall lit. Set lit -> lit -> PrologRule lit Prolog ((lit -> lit) -> Set lit -> Set lit forall b a. Ord b => (a -> b) -> Set a -> Set b Set.map lit -> lit inst Set lit asm) (lit -> lit inst lit c), Int k Int -> Int -> Int forall a. Num a => a -> a -> a + Set v -> Int forall a. Set a -> Int Set.size Set v fvs) where fvs :: Set v fvs = (lit -> Set v -> Set v) -> Set v -> Set lit -> Set v forall a b. (a -> b -> b) -> b -> Set a -> b Set.fold (Set v -> Set v -> Set v forall a. Ord a => Set a -> Set a -> Set a Set.union (Set v -> Set v -> Set v) -> (lit -> Set v) -> lit -> Set v -> Set v forall b c a. (b -> c) -> (a -> b) -> a -> c . lit -> Set v forall formula atom term v. (IsFormula formula, HasApply atom, atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) => formula -> Set v var) (Set v forall a. Set a Set.empty :: Set v) (lit -> Set lit -> Set lit forall a. Ord a => a -> Set a -> Set a Set.insert lit c Set lit asm) vvs :: Map v term vvs = [(v, term)] -> Map v term forall k a. Ord k => [(k, a)] -> Map k a Map.fromList (((v, Int) -> (v, term)) -> [(v, Int)] -> [(v, term)] forall a b. (a -> b) -> [a] -> [b] List.map (\(v v, Int i) -> (v v, TVarOf term -> term forall term. IsTerm term => TVarOf term -> term vt (String -> TVarOf term forall a. IsString a => String -> a fromString (String "_" String -> String -> String forall a. [a] -> [a] -> [a] ++ Int -> String forall a. Show a => a -> String show Int i)))) ([v] -> [Int] -> [(v, Int)] forall a b. [a] -> [b] -> [(a, b)] zip (Set v -> [v] forall a. Set a -> [a] Set.toList Set v fvs) [Int k..])) inst :: lit -> lit inst = Map v term -> lit -> lit forall lit atom term v. (JustLiteral lit, HasApply atom, IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> lit -> lit lsubst Map v term vvs {- (* ------------------------------------------------------------------------- *) (* 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' = renamerule 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 (simpcnf(skolemize(Not(generalize fm)))) in deepen (fun n -> backchain rules n 0 undefined [False],n) 0;; (* ------------------------------------------------------------------------- *) (* A Horn example. *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; 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))>>;; (* ------------------------------------------------------------------------- *) (* A non-Horn example. *) (* ------------------------------------------------------------------------- *) (**************** hornprove <<(p \/ q) /\ (~p \/ q) /\ (p \/ ~q) ==> ~(~q \/ ~q)>>;; **********) END_INTERACTIVE;; (* ------------------------------------------------------------------------- *) (* Parsing rules in a Prolog-like syntax. *) (* ------------------------------------------------------------------------- *) let parserule s = let c,rest = parse_formula (parse_infix_atom,parse_atom) [] (lex(explode s)) in let asm,rest1 = if rest <> [] & hd rest = ":-" then parse_list "," (parse_formula (parse_infix_atom,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];; (* ------------------------------------------------------------------------- *) (* Ordering example. *) (* ------------------------------------------------------------------------- *) START_INTERACTIVE;; let lerules = ["0 <= X"; "S(X) <= S(Y) :- X <= Y"];; simpleprolog lerules "S(S(0)) <= S(S(S(0)))";; (*** simpleprolog lerules "S(S(0)) <= 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)";; (* ------------------------------------------------------------------------- *) (* However this way round doesn't work. *) (* ------------------------------------------------------------------------- *) (*** *** prolog appendrules "append(X,3::4::nil,X)";; ***) (* ------------------------------------------------------------------------- *) (* 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(S(S(S(0))))::S(0)::0::S(S(0))::S(0)::nil,X)";; (* ------------------------------------------------------------------------- *) (* Yet with a simple swap of the first two predicates... *) (* ------------------------------------------------------------------------- *) let badrules = ["sort(X,Y) :- sorted(Y), perm(X,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"];; (*** This no longer works prolog badrules "sort(S(S(S(S(0))))::S(0)::0::S(S(0))::S(0)::nil,X)";; ***) END_INTERACTIVE;; -} testProlog :: Test testProlog :: Test testProlog = String -> Test -> Test TestLabel String "Prolog" ([Test] -> Test TestList [])