# Beyond unification: A little logic language

In *Unification in Elixir*, I describe in detail how to implement the unification algorithm. Through two small examples, I also hint at how new layers can be added that make it possible to process more complex logical expressions. In this post, I carry these ideas forward to develop a *little logic language* (L3) in Elixir. This language captures core aspects of microKanren, a more complete (but still very small) logic programming language. You don't need to have read the microKanren paper to follow along here, but it would be a good idea to skim *Unification in Elixir *and review the code linked in that post.

## Start at the end

Rather than begin with primitive concepts and build up to L3, I'm going to start by demonstrating the interface I'd like to achieve. There are three logic functions that L3 will support: `equal`

, `both`

, and `either`

, each of which takes two arguments. Before discussing how these functions work and what they return, I want to talk about what they *mean* and how they can be composed to create complex logical expressions.

The simplest of these functions is `equal`

. Like `unify`

, `equal`

takes two terms as arguments and is asserting their equality. For instance, `equal(x, 1)`

asserts that variable `x`

is equal to 1. Another way to say this is that `equal(x, 1)`

returns a *goal* expressing the idea that `x == 1`

. Depending on the current substitution, this goal may or may not succeed. I'll clearly define what a goal is a bit later.

Logical conjunction is expressed with `both`

. Each of the two arguments to `both`

is a goal. Like `equal`

, `both`

is a function that returns a goal. The expression `both(equal(x, y), equal(y, 1))`

declares that `x == y`

and `y == 1`

are jointly true. More complex conjunctions can be constructed through composition:

```
both(
equal(x, y),
both(
equal(y, z),
equal(z, 1)
)
)
```

Ask yourself, *what should the result be if there is no initial knowledge about the variables?*

As you might guess, `either`

expresses the logical disjunction of a pair of goals; it also returns a goal. For example, `either(equal(x, 1), equal(x, 2))`

says that `x == 1`

or `x == 2`

may be separately true. Arguments of `either`

and `both`

can be arbitrarily nested compositions of `equal`

, `both`

, and `either`

.

Code written using `equal`

, `both`

, and `either`

is *declarative*. Even when the implementation details are unknown, the intent is clear when writing something like `both(equal(x, y), equal(y, 1))`

. Declarative code allows one to express intent without procedural distractions. Before addressing the procedural ~~distractions~~ necessities, let's look at more examples.

## Familiar examples

Near the end of *Unification in Elixir**,* I discuss two examples, one a logical join of three lists, and the other a series of binary choices. Let's cast these examples in terms of the functions described above. After the functions are fully implemented, I'll return to these examples to get actual results.

### Three lists united

Equality of `[x, 2, 3]`

and `[1, y, 3]`

is written as `equal([x, 2, 3], [1, y, 3])`

. With the help of `both`

, multiple equalities may be chained together:

```
l1 = [x, 2, 3]
l2 = [1, y, 3]
l3 = [1, 2, z]
both(
equal(l1, l2),
both(
equal(l2, l3),
equal(l1, l3)
)
)
```

This doesn't have a `with`

block or `:ok`

tuples or other arcane symbols; it's a concise declaration of intent.

### A walk divided

For a person that can step either `:left`

or `:right`

, the first step with direction `d1`

is written as

```
either(
equal(d1, :left),
equal(d1, :right)
)
```

For the first two steps:

```
both(
either(
equal(d1, :left),
equal(d1, :right)
),
either(
equal(d2, :left),
equal(d2, :right)
)
)
```

For the first three steps:

```
both(
either(
equal(d1, :left),
equal(d1, :right)
),
both(
either(
equal(d2, :left),
equal(d2, :right)
),
either(
equal(d3, :left),
equal(d3, :right)
)
)
)
```

And so on.

This is much less code and is arguably much more readable than what was presented in *Unification in Elixir**. *That's by design! L3 is a declarative domain-specific language, one whose sole purpose is to clearly express and evaluate logical ideas.

## Goal setting

We're writing code to solve problems. Declarations of intent are not enough. Somewhere, somehow those declarations need to act on data to produce new data. I said earlier that `equal`

, `both`

, and `either`

return goals when provided with arguments. And `both`

and `either`

take goals as arguments. But what is a goal?

An assertion like `equal(x, 1)`

must be evaluated in the context of what is already known. Recall that a single state of knowledge is represented by a substitution, a mapping between variables and their values. Whatever `equal(x, 1)`

returns, it must be able to act on a substitution. A goal is a *function* of a substitution. What does this function produce when called?

When given the empty substitution, `%{}`

(nothing is known), the goal generated by `equal(x, 1)`

should return the updated substitution `%{x => 1}`

. Maybe a goal returns a new substitution? Not so fast!

When the disjunction `either(equal(x, 1), equal(x, 2))`

is given an empty substitution, it should yield `[%{x => 1}, %{x => 2}]`

. A list of substitutions, one that reflects all possible choices, is the most general state of knowledge, at least for our purposes. Even though the goal corresponding to `equal(x, 1)`

doesn't spawn multiple substitutions, it still returns a list to be compatible with `either`

. The same goes for goals generated by `both`

.

A goal is a function that takes a substitution and returns a list of substitutions. To help solidify this idea, here's an elixir type definition:

`@type goal :: (substitution -> [substitution])`

The list may be empty. This happens when the assertion is in conflict with the substitution supplied to the goal. If we know `%{x => 2}`

, then `equal(x, 1)`

is a false assertion, and the goal must return `[]`

.

## A little logic language

The interface to L3 has been described, and the abstract notion of a goal has been defined. It's now time to fully implement the specific goals returned by `equal`

, `both`

, and `either`

.

`equal(term1, term2)`

Recall that `unify`

implements term equality in the context of a substitution. Unsurprisingly, `equal`

is just a lightweight wrapper around `unify`

:

```
@spec equal(uterm, uterm) :: goal
def equal(term1, term2) do
fn sub ->
case unify(sub, term1, term2) do
{:ok, sub} -> [sub]
:error -> []
end
end
end
```

The goal repackages the result of `unify`

so that a list is returned. The result of `equal(x, 1).(%{})`

is `[%{x => 1}]`

, as expected, while `equal(x, 1).(%{x => 2})`

is a conflict and yields `[]`

.

`both(goal1, goal2)`

A conjunction involves a mapping of one goal over the results of another. First, apply `goal1`

to the input substitution to generate a list of new substitutions. Then, for each of these substitutions, apply `goal2`

. The output of these two steps is a nested list of substitutions. Finally, flatten the nested list to return one list of substitutions that represents the combined result. The Elixir function `Enum.flat_map`

does the job nicely:

```
@spec both(goal, goal) :: goal
def both(goal1, goal2) do
fn sub ->
Enum.flat_map(goal1.(sub), goal2)
end
end
```

Here's a diagram that illustrates `both`

:

The circles are substitutions, the boxes with solid borders are functions, and the dashed boxes are lists. Colors indicate a goal or substitutions generated by the goal with matching color. Numbers indicate unique substitutions with a given color. In this illustrative example, I assume that each of the goals generates two substitutions.

You might be wondering if the result of `both`

changes when the order of its arguments is swapped. In a certain technical sense, the result does change. But this change is an artifact of using lists to hold substitutionsâ€“a computational convenience. If the result is cast to a set (in Elixir, a `MapSet`

) and all variables are fully simplified, you'll see that answer is the same before and after the argument swap. (There is a caveat to this when one or both goals can produce an *infinite* number of substitutions, but that's outside the scope of this post.)

`either(goal1, goal2)`

Each goal supplied to `either`

generates a separate list of substitutions. To match the structure of the desired result, these two lists are combined. The simplest way to combine two lists is to concatenate them, as seen here:

```
@spec either(goal, goal) :: goal
def either(goal1, goal2) do
fn sub ->
Enum.concat(goal1.(sub), goal2.(sub))
end
end
```

And here's an illustrative diagram for `either`

:

The order of the arguments to `either`

doesn't have a material effect on the results.

### A little help

It feels clunky to call goals directly. Here's a helper function that takes a goal and a list of variables, and returns simplified values (via `simplify`

):

```
@spec present(goal, [variable]) :: [uterm]
def present(goal, vars) do
%{}
|> goal.()
|> Enum.map(&present_sub(&1, vars))
end
defp present_sub(sub, vars) do
Enum.map(vars, fn v ->
if Map.has_key?(sub, v) do
simplify(sub, v)
else
v
end
end)
end
```

This function calls the goal with an empty substitution and then applies `simplify`

to the variables for each member of the returned list of substitutions. Putting `present`

to use looks like this:

```
both(
either(
equal(x, 1),
equal(x, y)
),
either(
equal(y, 2),
equal(y, 3)
)
)
|> present([x, y])
# returns
[[1, 2], [1, 3], [2, 2], [3, 3]]
```

If a variable given to `present`

isn't a substitution key, then the unresolved variable is included in the output:

```
equal(x, 1)
|> present([x, y])
# returns
[[1, y]]
```

## Revisited examples

Now that the L3 logic functions are implemented, the examples from earlier can be evaluated. For the joint unification of three lists, calling on an empty substitution yields the expected result:

```
both(
equal(l1, l2),
both(
equal(l2, l3),
equal(l1, l3)
)
)
|> present([x, y, z])
# returns
[[1, 2, 3]]
```

In the case of the random walk, the possibilities after two steps are

```
both(
either(
equal(d1, :left),
equal(d1, :right)
),
either(
equal(d2, :left),
equal(d2, :right)
)
)
|> present([d1, d2])
# returns
[
[:left, :left],
[:left, :right],
[:right, :left],
[:right, :right]
]
```

It's incredibly satisfying to see our hard hard work culminate in such a simple and expressive little language.

## The end?

There's so much more we could do with L3, from quality-of-life improvements to deeper applications. I hope to explore some of these ideas in later posts. Until then, if you'd like to play with L3, all the code can be found here:

Have fun!