Skip to content

Instantly share code, notes, and snippets.

@ademar
Created June 9, 2011 14:49
Show Gist options
  • Save ademar/1016874 to your computer and use it in GitHub Desktop.
Save ademar/1016874 to your computer and use it in GitHub Desktop.
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<Answer>
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment