Introduction to logic programming

In logic programming instead of describing how to solve a problem, we declare the rules of the problem.

Here is a simpler logic program in a hypothetical language, very similar to prolog:

parent('John', 'Mary')
parent('John', 'Mike')
parent('George', 'John')
grandparent(A, C): exists B: parent(A, B) and parent(B, C).

And then you have some way of asking the system to solve for a variable:

solve for Q: grandparent(Q, 'Mary')

And it would respond with ‘George’.

In logic programming we describe the rules: Someone is a grandparent of someone else, if he is the parent of his parent. Then we gave some examples of parent-child relationships and asked the system to find Mary’s grandparent.

Contrast this to how we would do it in regular python:

We would probably have some sort of dictionary that describes parents, and a function that returns somebody’s grandparent.

parents = {
    'Mary': 'John',
    'Mike': 'John',
    'John': 'George'
}

def grandparent(x):
    if x not in parents:
        return None
    parent = parents[x]
    return parents[parent] if parent in parents else None

Then we could print Mary’s grandparent with print(grandparent('Mary')).

It’s neat that the logic programming snippet describes the relations between values (the “what”) and not which steps to take to resolve them (the “how”). However, the python version doesn’t seem all that worse than the logic programming solution. So, why bother? Well, when using logic programming rules, you can also ask who are the grandchildren of George, for free.

solve for Q: grandparent('George', Q)

The expected response being ‘Mary’ and ‘Mike’. In python we would have to define a new function grandchildren(x) but which would need to use the previous dictionary inverted, and in such a way that each key has a list of values, or some other custom logic.

Other more complicated problems that can be described with rules are even better suited for such programming, for example solving sudoku.

Okay, now let’s try to build something like this in Python.

Variable representation

We first need a way to represent logical variables.

from dataclasses import dataclass
from typing import Any

@dataclass
class Variable:
    name: str

    def __eq__(self, other: Any) -> bool:
        return isinstance(other, Variable) and self.name == other.name

    def __hash__(self) -> int:
        return hash(self.name)

    def __repr__(self) -> str:
        return self.name

As this is our first python snippet, you will notice I’m using type hints and data classes. In short, the dataclass annotation defines a default constructor that sets the fields of the class to the values passed as arguments. So Variable('x') creates a Variable instance with name set to ‘x’.

Knowledge representation

We can use dictionaries to represent that variables have certain values:

{ x: 1, y: 2 }

But variables may be equal to other variables:

{ x: y, y: 1 }

Since variables can point to other variables, we will use the same variable as key and value to represent variables that have not been assigned yet:

{ x: x, y: y }

We will call such a dictionary, a “binding”:

from typing import Dict

Binding = Dict[Variable, Any]

Now, we also need to say that a variable may have multiple values. We can do that using a list of such bindings:

[ { x: 1 }, { x: 2 } ]

Having a list of bindings allows us to represent that when one variable is this value, then the other variable is that value:

For example, if y is x + 1 and x is 1 or 2, then:

[ { x: 1, y: 2 }, { x: 2, y: 3 } ]

A careful reader will be suspicious of the fact that we have only two levels in this structure, but since one is analogous to boolean “or” (the items of the list) and the other analogous to “and” (the dictionary key-value pairs), we can argue that there is a distributive property here that allows us to “expand” any deeper nested structure into just two levels.

However, instead of usings lists we will use any sort of iterable, which allows us to write generators that produce infinite different bindings.

So, we will call an iterable of bindings, knowledge:

from typing import Iterable

Knowledge = Iterable[Binding]

You can always think of this data structure as list of dictionaries, but which does not allow for accessing a particular element (no “[]” element access operator), and which in order to be printed needs to be translated into a list by calling the list() built-in function (which may cause an infinite loop).

Rules of logic

Ok, now that we can represent knowledge, we need to be able to transform knowledge through rules of logic. A rule is a function that takes a binding and produces knowledge:

from typing import Callable

Rule = Callable[[Binding], Knowledge]

Therefore we can use apply a rule to transform each binding in our existing knowledge to produce new knowledge:

def apply(k: Knowledge, r: Rule) -> Knowledge:
    for binding in k:
         for result in r(binding):
             yield result

Let’s look at simplest rules we can apply. A rule that erases any knowledge we had:

def fail(binding: Binding) -> Knowledge:
    return []

We will say that a rule fails if it not only doesn’t produce new knowledge, but also erases any knowledge we had (for example because a contradiction has been found).

And we will say that a rule succeeds if it produces knowledge. The simplest succeeding rule doesn’t check the existing knowledge and just propagates what we already know:

def succeed(binding: Binding) -> Knowledge:
    return [binding]

We can apply these rules to hypothetical previous knowledge:

>>> x = Variable('x')
>>> list(apply([{x: 1}], fail))
[]
>>> list(apply([{x: 1}], succeed))
[{x: 1}]

list() is used here in order to print the results of the generator.

Applying the result of one rule to the result of the other is equivalent to applying both rules (“and”):

>>> k = [{x: 1}]
>>> list(apply(apply(k, succeed), fail))
[]
>>> list(apply(apply(k, succeed), succeed))
[{x: 1}]

While applying two rules separately to the same input and concatenating the results is equivalent to applying either of the rules (“or”):

>>> k = [{x: 1}]
>>> list(apply(k, fail)) + list(apply(k, fail))
[]
>>> list(apply(k, succeed)) + list(apply(k, fail))
[{x: 1}]

We can leverage this to create “higher level rules”, rules that combine other rules to produce a new rule. Therefore in terms of our python code, these are functions that takes functions as arguments and return new functions.

As we have seen, to create a rule that takes two rules and applies both, we need to pass every result of the first rule to the second:

def both(a: Rule, b: rule) -> Rule:
    def gen(binding: Binding):
        return (b(bind) for bind in a(binding))
    return gen

In order to implement the equivalent of logical “or” we need to append the results of one rule to the results of the other. If knowledge was represented as a list we would simply add the two lists with +. But since they are iterables we can use itertools.chain instead:

def either(a: Rule, b: Rule) -> Rule:
    def gen(binding: Binding):
        return itertools.chain(a(binding), b(binding))
    return gen

We can make a small improvement here that will allow for a list of rules to be passed instead of just two rules:

def either(*rules: List[Rule]) -> Rule:
    def gen(binding: Binding):
        all_knowledge = [rule(binding) for rule in rules]
        return itertools.chain(*all_knowledge)
    return gen

Finding solutions

To solve a rule call it with an initial state where nothing is known (everything is possible):

def solve(rule: Rule) -> Knowledge:
    init = {}
    knowledge = rule(init)
    return list(knowledge)

Let’s test that this works:

>>> solve(fail)
[]
>>> solve(succeed)
[{}]
>>> solve(either(fail, succeed))
[{}]

Unification

Let’s write a fact that asserts that socrates is a man as a python function:

def is_man(x: str) -> Rule:
    def gen(binding):
        if x == 'socrates' or (x in binding and binding[x] == 'socrates'):
            return [binding]
        return []
    return gen

This function works like succeed and fail, but also checks that the argument to the function is 'socrates' or a variable that is bound to it:

>>> apply([{x: 'socrates'}], is_man(x))
[{x: 'socrates'}]
>>> apply([{x: 'lizard'}], is_man(x))
[]

However, we would like it to also solve the problem the other way around:

>>> x = Variable('x')
>>> apply([{x: x}], is_man(x))
[{x: socrates}]
>>>

However, the above would fail and just answer the empty list.

We can change is_man to assign an unassigned variable to the value of 'socrates':

def is_man(x: Any) -> Rule:
    def gen(binding):
        if x == 'socrates':
            return [binding]
        if isinstance(x, Variable):
            if x in binding and binding[x] != 'socrates':
                return []
            binding = copy(binding)
            binding[x] = 'socrates'
            return binding
        return []
    return gen

This seems like a lot of work for just one fact. Ideally, we would just use a function unify(x, 'socrates') that generates a rule that binds x to socrates.

Let’s write that function in the same logic that we used in is_man definition, but making it work with both arguments possibly being logical variables:

def extend(binding: Binding, variable: Variable, value: Any) -> Binding:
    binding = {k: v for (k, v) in binding}
    binding[variable] = value
    return binding

def resolve(binding: Binding, key: Any) -> Any:
    return binding[key] if key in binding else key

def unify(x: Any, y: Any) -> Rule:
    def gen(binding):
        x = resolve(binding, x)
        y = resolve(binding, y)
        if x == y:
            return [binding]
        if isinstance(x, Variable) or isinstance(y, Variable):
            if isinstance(x, Variable):
                binding = extend(binding, x, y)
            if isinstance(y, Variable):
                binding = extend(binding, y, x)
            return [binding]
        return []
    return gen

Let’s test this out:

>>> x = Variable('x')
>>> y = Variable('y')
>>> apply([{}], unify(x, 1))
[{x: 1}]
>>> apply([{y: 1}], either(unify(x, 1), unify(x, 2)))
[{x: 1, y: 1}, {x: 2, y: 1}]
>>> apply([{x: 1}], unify(x, 2))
[]

As seen in the last example, by looking up a variable before doing anything else, we have made sure that when checking if x and y are variables, they are unassigned variables, and therefore unify does not allow for re-assigning the value of a variable. There is however something that our code doesn’t yet handle correctly. The following should not return any bindings, since there is a contradiction:

>>> apply([{x: y, y: 1}], unify(x, 2))
[{x: y, y: 2}]

The reason for this is that resolve function does not properly handle the case of a variable pointing to another variable (which points to a value, or a third variable etc).

Let’s fix that, while being careful not to be trapped in an infinite loop if variables point to a variable we are already trying to resolve (there is a cycle in the assignment graph):

def resolve(binding: Binding, key: Any) -> Any:
    visited = []
    while key in binding and key not in visited:
        visited.append(key)
        key = binding[key]
    return key

Now the previous case returns the expected result:

>>> apply([{x: y, y: 1}], unify(x, 2))
[]

Finally the socrates is man rule can be written much more cleanly:

def is_man(x):
    return unify(x, 'socrates')

Remember, when we say the above what we mean is that socrates is indeed a man, but also that socrates is a solution for x, such that x is a man.

Fresh variables

We can make an improvement to our API to signify the equivalent of “exists” in first-order logic.

Let’s define a function exists that takes as argument a lambda function, and adds to the bindings the variables that the lambda function has as parameters. This will alow us to be explicit about when a variable is spawn into existence.

So we would write something like this:

>>> solve(exists(lambda x: succeed))
[{x: x}]

In order to implement this, we need some python magic to find out which parameters a function expects. For this we will use the inspect module:

def fn_parameters(f: Callable) -> List[Variable]:
    return [Variable(p) for p in inspect.signature(f).parameters.keys()]

Conveniently this method also returns the list of variables as Variable instances. We can use this to write exists:

def exists(f: Rule) -> Rule:
    def gen(binding):
        for param in fn_parameters(f):
            binding = extend(binding, param, param)
        return binding
    return gen

The param, param line has a nice melody to it, something out of the little drammer boy song.

Family relationships in python

So, we can finally define facts and goals in python like we did in the original imaginary logic programming language:

def parent(p, c):
    return either(both(unify(p, 'John'), unify(c, 'Mary')),
                  both(unify(p, 'John'), unify(c, 'Mike')),
                  both(unify(p, 'George'), unify(c, 'John')))

def grandparent(a, c):
    return exists(lambda b: both(parent(a, b), parent(b, c)))

Defining facts like parent above is somewhat cumbersome, improving that is left as an exercise to the reader. But the definition of grandparent rule above is quiet elegant, and solving it for various values is very satisfying:

>>> solve(exists(lambda q: grandparent('John', q)))
[{q: 'Mary', b: 'John'}, {q: 'Mike', b: 'John'}]
>>> solve(exists(lambda q: grandparent(q, 'Mary')))
[{q: 'John'}]

Possible improvements

  • simpler api for fact definition for example:
parent = fact()
parent.assert('John', 'Mary')
parent.assert('John', 'Mike')
parent.assert('George', 'John')
  • unify lists and functions for lists (appendo, membero)
  • not equals, domains
  • constraints
  • interleaving unify

Further reading