Skip to content

Instantly share code, notes, and snippets.

# ademar/gist:1016874 Created Jun 9, 2011

Combinators for logic programming
 // Based on the article 'Combinators for logic programming' by Michael Spivey and Silvija Seres. let rec inf_seq n = seq { yield n; yield! inf_seq (n+1) } let rec lzw f l1 l2 = LazyList.delayed ( fun () -> match l1,l2 with |LazyList.Nil, _ -> l2 |_, LazyList.Nil -> l1 |LazyList.Cons(p1,tail1),LazyList.Cons(p2,tail2) -> LazyList.consDelayed (f p1 p2) (fun () -> lzw f tail1 tail2)) let rec diag input = LazyList.delayed ( fun () -> match input with |LazyList.Nil -> LazyList.empty |LazyList.Cons(p,tail) -> lzw (LazyList.append) (LazyList.ofSeq (seq {for x in p do yield LazyList.ofList [x]})) (LazyList.consDelayed (LazyList.empty) (fun () -> diag tail))) //-- Diagonal Monad type DiagBuilder () = member b.Return(x) = LazyList.ofList [x] member b.Bind(x, rest) = LazyList.concat (diag (LazyList.map ( rest) x)) member b.Let(p, rest) = rest p member b.Delay(f ) = f () member b.Zero() = LazyList.empty let diagonal = new DiagBuilder () type Variable = |Named of string |Generated of int type Term = | Int of int | Float of float | String of string | Nil | Var of Variable | Cons of Term*Term | Atom of string*Term type Clause = Clause of Term*Term type Program = Program of Clause list type Subst = (Variable*Term) list type Answer = Subst*int type Pred = Answer -> LazyList let var s = Var(Named(s)) let cons x y = Cons(x,y) let int = fun i -> Int(i) let list1 xs = List.foldBack (cons) xs Nil let list2 f xs = list1 (List.map f xs) let list xs = list2 int xs let idsubst = [] let extend (x:Variable) (t:Term) (b) = (x,t)::b let lookup v b = let rec lookup' = function |[] -> None |(x,t)::tail -> if x=v then Some t else lookup' tail lookup' b let rec deref (subst:Subst) (term:Term) : Term = match subst,term with |b,Var(v) -> match (lookup v b) with |Some t -> deref subst t |None -> Var v |_,_ -> term let rec apply s t = match (deref s t) with |Cons(x,xs) -> Cons(apply s x, apply s xs) |t' -> t' let rec occurs s x t = let occurs' s x = function |Nil -> false |Cons(y,ys) -> occurs s x y || occurs s x ys |Int(_) -> false |Float(_) -> false |String(_) -> false |Atom(_,ts) -> occurs s x ts |Var(y) -> (x=y) occurs' s x (deref s t) let rec unify (s:Subst) (t,u) = let univar (x,t) = if t=Var(x) then Some s else if occurs s x t then None else Some (extend x t s) let unify' = function |(Nil,Nil) -> Some s |(Cons(x,xs),Cons(y,ys)) -> Option.bind (fun s' -> unify s' (xs,ys)) (unify s (x,y)) |(Int(n),Int(m)) when n=m -> Some(s) |(Float(n),Float(m)) when n=m -> Some(s) |(String(n),String(m)) when n=m -> Some(s) |Var(x),t -> univar (x,t) |t,Var(x) -> univar (x,t) |_ -> None unify' (deref s t, deref s u) let rec shuffle a b = match a with |LazyList.Nil -> b |LazyList.Cons(x,xs) -> LazyList.consDelayed x (fun () -> shuffle b xs) let alt a b = shuffle a b let initial = (idsubst,0) let run (p:Pred) = p initial let wrap a = a let (==) t u (s,n) = match unify s (t,u) with | Some s' -> diagonal.Return (s',n) | None -> diagonal.Zero() // -- predicate operators let (&&&) (p:Pred) (q:Pred) (s:Answer) = diagonal.Bind(p s,q) let (|||) (p:Pred) (q:Pred) (s:Answer) = alt (p s) (q s) // -- exists introduces a new (semi-anonymous) variable let exists p (s,n) = p (Var (Generated (n))) (s,n+1) let step (p:Pred) (s:Answer) = wrap (p s) let rec append p q r = step (((p == Nil) &&& (q == r)) ||| exists (fun x -> exists (fun a -> exists ( fun b -> (p == (cons x a)) &&& (r == (cons x b)) &&& append a q b)))) // -- print routine let rec print term = match term with |Nil -> "Nil" |Cons(a,b) -> "[" + (print a) + (print_tail b) + "]" |Int(n) -> n.ToString() |Var(Named(s)) -> s |Var(Generated(n)) -> "_g" + n.ToString() |String(o) -> o.ToString() |Float(o) -> o.ToString() |Atom(s,t) -> s + "(" + (print t)+ ")" and print_tail term = match term with |Nil -> "" |Cons(a,b) -> ", " + (print a) + (print_tail b) |t -> "|" + (print t) let rec joinwith sep = function |[] -> "" |[s] -> s |s::ss -> s + sep + joinwith sep ss let isNamed = function |Named(_) -> true; |_ -> false let name = function |Named(x) -> x |Generated(x) -> "_g" + x.ToString() let rec print_subst b = let showb x = x + "=" + (print (apply (b) (Var(Named(x))))) let vars = List.map (fun (x,y) -> name x) (List.filter (fun (t,_) -> isNamed t) b ) "{" + (joinwith "," (List.map showb (List.sort vars))) + "}" let print_answer (s,n) = print_subst s let printSolutions q = for x in q do printf "%s\n" (print_answer x) // Sample #1 - append let X = var "x" let Y = var "y" let problem1 = append X Y (list [1;2;3;4;5]) run problem1 |> printSolutions // Sample #2 - good sequence let rec good s = step( (s == cons (Int 0) Nil) ||| exists (fun t -> exists(fun q -> exists(fun r -> (s == cons (Int 1) t) &&& append q r t &&& (good q) &&& (good r)))) ) let problem2 = good (var "s") run problem2 |> printSolutions // Sample #3 - Difference lists & Grammars let append' (a1,a2) (b1,b2) (c1,c2) = (a1 == c1) &&& (a2 == b1) &&& (b2 == c2) // -- difference list axiom let list3 xs ys = List.foldBack (cons) xs ys let (++) f1 f2 = fun (list1,r) -> exists( fun x -> append' (list1,x) (x,r) (list1,r) &&& f1(list1,x) &&& f2(x,r)) let final s (list,rest) = exists(fun x -> ((list == list3 ([String(s)]) x)) &&& (x == rest)) let or' f g (list,rest) = f (list,rest) ||| g (list,rest) let noun = final "cat" |> or' <| final "mouse" let determiner = final "the" |> or' <| final "a" let verb = final "scares" |> or' <| final "hates" let noun_phrase = determiner ++ noun let verb_phrase = verb ++ noun_phrase let sentence = noun_phrase ++ verb_phrase run ( sentence (var "q", Nil)) |> printSolutions
to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.