# Prolog Proof search trees

Somewhere I read that writing programs is much like writing mathematical proofs.
Let’s try to understand what’s meant by that, by playing with Prolog.

Consider the following Prolog facts, that is, given definitions:

`bigger(cat, mouse).bigger(mouse, bug).`

Now, we can ask Prolog what’s smaller than a cat?

`?- bigger(cat, X).X = mouse.`

It of course responds that a mouse is smaller than a cat.
But what about a bug? Why didn’t it report that a bug is smaller than a cat?
This is so because Prolog doesn’t know much about this relation. Other than what is supplied to it, it assumes everything else is untrue. So, for instance, if we did:

`?- bigger(cat, bug).false.`

We would get a negative answer.

To fix this, we need to implement a transitive relation of bigger. What this means is that if we have that A·B and B·C, then A·C holds as well, that is, ∀a, b, c ∈ X : (a·b ∧ b·c) ⇒ a·c. Do you see the mathematical similarity here?

In this case, · would be bigger. Let’s call this relation is_bigger.

This is how it looks:

`is_bigger(A, B) :- bigger(A, B).is_bigger(A, B) :- bigger(A, C), is_bigger(C, B).`

Doing a couple of tests:

`?- is_bigger(cat, mouse).true .?- is_bigger(mouse, bug).true .?- is_bigger(cat, bug).true .`

It seems to be working fine!

Now let’s try to explain the definition.

The :- operator here is like mathematical if, that is, if we did a :- b, and then ask for the truth value of a, it would report true if b were true as well. So by is_bigger :- bigger, we say that the former is true if the latter.

When you define multiple definitions in Prolog, it tries to find which one of them is true. In this case, it’s acting kind of an OR, it tries the first definition, then the second, and if all of them fail the result would be false, but even one of them succeeds and the result is true. Note that, we could also rewrite the definition like:

`is_bigger(A, B) :- bigger(A, B); bigger(A, C), is_bigger(C, B).`

That is, rewrite it using the ; operator as an OR. This is also valid, but much less readable.

In contrast, when you do a, b, c. in Prolog (i.e. comma operator), it does an AND, i.e. it first tries to prove a, then b, then c. If one of them fails, the result is false. Otherwise, it’s true.

One could easily notice that this definition is a recursive one, and the first one should be the base case of the recursion. This is correct.

So, calling is_bigger(cat, bug) would fail for the first definition, and then proceeds to the second (recursive) one to see if it can find a true match. So it tries to prove bigger(A, C), is_bigger(C, B), that is, it tries to find a C such that these 2 terms are logically true. But does there exist such C? Let’s try to further expand.

is_bigger(C, B) would first attempt to prove bigger(C, B), that is, bigger(C, bug). C in this case (according to the given facts) would be mouse. This is a possible match. Let’s return to bigger(A, C) and see if we can also fit mouse to it, i.e. is it true that bigger(cat, mouse)? Of course, this is also in the definitions. So for C = mouse, we can prove that bigger(A, C), bigger(C, B) is true. From this, it follows also that is_bigger(cat, bug) is true.

Would you agree that we’ve just written a mathematical proof? Given a few definitions, using transitivity we were able to deduce some fact, using Prolog.

The gap between Prolog and Mathematics is too small, in contrast to other languages, say Python and Mathematics. This is why notation is important. It makes you think in a different way for tasks you likely already solved using other languages.

So, let’s turn to our everyday languages for a while. What we have to deal with is some trees, some equality checking and we should be able to easily implement this in another language. Let’s try Python.

We’re going to write a program that attempts to prove a given search tree, just what Prolog did. With this, I think we will be able to see how writing programs is actually much like writing mathematical proofs.

I won’t go through the details, but here’s how it could look:

`class node(object):    def __init__(self, value, children = []):        self.value = value        self.children = children    def contains(self, value):        for x in self.children:            if x.value == value:                return True        return False    def __repr__(self, level=0):        ret = "  "*level+repr(self.value)+"\n"        for child in self.children:            ret += child.__repr__(level+1)        return ret# The relation tree to work withtree = node("bigger", [    node("cat", [node("mouse"), node("bug")]),    node("mouse", [node("bug")]),])# This function would attempt to find a correct proof for the given task# It parses the treedef find_proof(tree, A, B):    if tree.value == A and tree.contains(B):        return True    for node in tree.children:        if find_proof(node, A, B):            return True    return False# Try to find proofprint(find_proof(tree, 'cat', 'mouse'))print(find_proof(tree, 'mouse', 'bug'))print(find_proof(tree, 'cat', 'bug'))`

It returns:

`TrueTrueTrue`

What would be more interesting is to write a function that would generate the proof tree instead of us manually supplying it 🙂