kanren: Relational Programming in Python

A Goal is a function that takes a substitution and returns a stream (generator) of substitutions.

Users typically do not write goals directly; instead, they use Goal Constructors (like membero or eq) to build them. When you call a goal constructor, it returns a goal that, when executed with a substitution, yields all possible ways to satisfy that logical constraint.

# Creating a goal using a constructor
g = membero(x, (1, 2, 3))

# Executing the goal with an empty substitution
for s in g({}):
    print(s)  # Yields {~x: 1}, {~x: 2}, {~x: 3}

In miniKanren, a Term is the fundamental data unit. Terms can be:

• Any standard Python object (e.g., 1, [1, 2], 'cat').
• A logic variable created using var().
• A combination of the two (e.g., a tuple containing constants and variables like (1, x, 'cat')).

Think of terms as trees where the leaves are either constants or logic variables.

In kanren, you can combine multiple goals to create complex relations:

• Conjunction (lall): All goals must be satisfied (logical AND). This is often used implicitly when passing multiple goals to run.
• Disjunction (lany): At least one of the goals must be satisfied (logical OR).

Example of finding values that satisfy multiple membership constraints:

from kanren import run, membero, var

x = var()
# Find x such that x is in (1, 2, 3) AND x is in (2, 3, 4)
results = run(0, x, membero(x, (1, 2, 3)), membero(x, (2, 3, 4)))
print(results)  # (2, 3)

You can define your own relations by writing functions that return goal combinations (typically using lall). This allows you to build complex logic on top of existing relations.

from kanren import Relation, facts, run, var, lall

parent = Relation()
facts(parent, ("Homer", "Bart"), ("Homer", "Lisa"), ("Abe", "Homer"))

def grandparent(x, z):
    y = var()
    return lall(parent(x, y), parent(y, z))

x = var()
# Who is Bart's grandparent?
print(run(1, x, grandparent(x, 'Bart')))  # ('Abe',)

When performing expansions, you can use kanren.goals.conso to constrain the structure of the resulting terms. For example, you can force the expanded_term to have a specific operator (like log) or ensure it is not a nullary function by constraining its cdr (the operand part).

from kanren.goals import conso
from kanren import run, var

expanded_term = var()
reduced_term = var()
exp_term_cdr = var()

# Constraint: expanded_term must start with 'log' AND have a non-empty operand
res = run(10, [expanded_term, reduced_term],
          conso(log, exp_term_cdr, expanded_term),
          conso(var(), var(), exp_term_cdr),
          term_walko(math_reduceo, expanded_term, reduced_term))

You can install kanren (the Python implementation of miniKanren) using pip or conda.

# Using pip
pip install miniKanren

# Using conda
conda install -c conda-forge miniKanren

To perform logic programming, you use var() to create logic variables and run() to execute queries. The eq(a, b) goal constructor is used for unification (checking if a and b can be made equal).

from kanren import run, eq, var

x = var()
# Find values of x such that x == 5
results = run(1, x, eq(x, 5))
print(results)  # (5,)

To reduce a specific term to its simplest form, define the expanded_term (the starting expression) and a reduced_term (a logic variable to hold the result). Use run with term_walko and your reduction relation.

Example: Reducing add(add(3, 3), exp(log(exp(5)))) using a custom math_reduceo relation.

from kanren import run, var

# The term to reduce
expanded_term = etuple(add, etuple(add, 3, 3), etuple(exp, etuple(log, etuple(exp, 5))))
# Logic variable for the result
reduced_term = var()

# Execute reduction
res = run(3, reduced_term, term_walko(math_reduceo, expanded_term, reduced_term))

Because kanren is relational, you can perform 'expansion' by providing a grounded reduced_term and an ungrounded expanded_term (a logic variable). This asks the engine: "What expressions would reduce to this result?"

Note: Since there can be infinitely many expansions, use a finite number in run to limit results.

expanded_term = var()
reduced_term = etuple(mul, 2, 5)

# Ask for 10 possible expansions of mul(2, 5)
res = run(10, expanded_term, term_walko(math_reduceo, expanded_term, reduced_term))