Combinators for logic programming

gistfile1.fs

// 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