09 June 2011

Digging in my hard drive found this piece of code from my functional programming studies that implements the logic unification algorithm described in the article â€˜Combinators for logic programmingâ€™ by Michael Spivey and Silvija Seres.

Here are some samples of what kind of problems it can solve.

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

``````

returns:

```{x=Nil,y=[1, 2, 3, 4, 5]}
{x=[1],y=[2, 3, 4, 5]}
{x=[1, 2],y=[3, 4, 5]}
{x=[1, 2, 3],y=[4, 5]}
{x=[1, 2, 3, 4],y=[5]}
{x=[1, 2, 3, 4, 5],y=Nil}
```

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

``````

returns:

```{s=[0]}
{s=[1, 0, 0]}
{s=[1, 0, 1, 0, 0]}
{s=[1, 1, 0, 0, 0]}
{s=[1, 0, 1, 0, 1, 0, 0]}
{s=[1, 1, 0, 0, 1, 0, 0]}
{s=[1, 1, 0, 1, 0, 0, 0]}
{s=[1, 0, 1, 1, 0, 0, 0]}
{s=[1, 1, 0, 0, 1, 0, 1, 0, 0]}
{s=[1, 1, 0, 1, 0, 0, 1, 0, 0]}
```

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

``````

returns:

```{q=[the, cat, scares, the, cat]}
{q=[the, cat, scares, the, mouse]}
{q=[the, mouse, scares, the, cat]}
{q=[the, cat, hates, the, cat]}
{q=[the, mouse, scares, the, mouse]}
{q=[a, cat, scares, the, cat]}
{q=[the, cat, scares, a, cat]}
{q=[the, mouse, hates, the, cat]}
{q=[a, cat, scares, the, mouse]}
{q=[a, mouse, scares, the, cat]}
{q=[the, cat, hates, the, mouse]}
{q=[the, mouse, scares, a, cat]}
{q=[a, cat, hates, the, cat]}
{q=[a, mouse, scares, the, mouse]}
{q=[the, cat, scares, a, mouse]}
{q=[the, mouse, hates, the, mouse]}
{q=[a, cat, scares, a, cat]}
{q=[a, mouse, hates, the, cat]}
{q=[the, cat, hates, a, cat]}
{q=[the, mouse, scares, a, mouse]}
{q=[a, cat, hates, the, mouse]}
{q=[a, mouse, scares, a, cat]}
{q=[the, cat, hates, a, mouse]}
{q=[the, mouse, hates, a, cat]}
{q=[a, cat, scares, a, mouse]}
{q=[a, mouse, hates, the, mouse]}
{q=[the, mouse, hates, a, mouse]}
{q=[a, cat, hates, a, cat]}
{q=[a, mouse, scares, a, mouse]}
{q=[a, cat, hates, a, mouse]}
{q=[a, mouse, hates, a, cat]}
{q=[a, mouse, hates, a, mouse]}
```

The code is here