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=,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=}
{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=}
{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