# A `core.logic`

primer

This notebook is an interactive version of the page with the same name in the `core.logic`

wiki with minor fixes.

Thanks to the original authors.

`{:deps {org.clojure/core.logic {:mvn/version "1.0.0"}}}`

`(use clojure.core.logic)`

## Introduction

This is a top-down introduction to `core.logic`

which attempts to lead you to that elusive AHA! moment of understanding what logic programming is about.

We begin with a high level overview of the purpose and basic syntax of core.logic and then show a small example of the sort of questions logic programming attempts to answer. With that understanding in hand we build up from the basic logic operators to simple programs.

This is (hopefully) the first of a series of articles that will further explore `core.logic`

's capabilities.

## Logic Programming

A logic program consists of a logic expression(s) and a solution engine or solver. A logic expression is a set of logic variables and constraints upon those variables. The logic expression is input to the logic engine which returns all assignments to the logic variables that satisfy the constraints in the expression.

Generally speaking you write the logic expression, and the solver is provided (`core.logic`

is the solver).

This setup is similar to SQL programming, which is a relational statement that is input to a relational engine which returns all data in the database consistent with that statement.

`core.logic`

syntax

A `core.logic`

program is written

`(run* [logic-variable]`

` &logic-expressions)`

This means: take the set of logic-expressions, run them through the solver and return all the values of logic-variable that satisfy the logic-expression.

### Logic Expression

A logic expression comprises a set of logic variables and a set of constraints upon the values that those logic variables can assume.

#### Logic Variables

A logic variable, or `lvar`

, is a variable that contains an ambiguous value. That is, the variable can take several values, but only one at a time. Precisely how this is done is beyond the scope of this introduction.

#### Constraints

Constraints are expressions that limit the values the `lvars`

may assume.

##### Motivating Example

An example is useful here. The `core.logic`

program

` (run* [q]`

` (membero q [1 2 3])`

` (membero q [2 3 4]))`

is read: run the logic engine and return all values of q such that q is a member of the vector `[1 2 3]`

and a member of the vector `[2 3 4]`

. It will thus return `(2 3)`

, indicating that q can be either `2`

or `3`

and satisfy the constraints. The return value of `run*`

is a list where each element is one of the possible values of `q`

.

This is what logic programming is all about:

declaring logic variables;

defining constraints on them;

having a logic engine figure out what values of the variables satisfy the constraints.

#### Note on naming conventions

Many functions that we'll discuss that are used with `core.logic`

(such as `membero`

) are somewhat special - in fact they have little meaning outside of `run`

/`run*`

. In order to differentiate these special functions (relations) from regular Clojure functions, we often append an "o", "e", "u", or "a".

These may seem strange at first- but rest assured, as you delve further into `core.logic`

you'll find that it's convenient to mix functional programming with logic programming and the naming convention simplifies reading more sophisticated `core.logic`

programs.

## How it's done

We now explore each of these concepts further to develop a better understanding.

### More on Logic Variables

Logic variables are similar to locals in Clojure. You can declare their value, they are lexically scoped, and not assignable. Most of the similarities end there.

For example, sometimes a logic variable may never actually take on a specific value(s). A special value for `lvars`

is `_.N`

, where `N`

is some number. This means "anything", much as `*`

means "anything" in a shell.

This means that the `lvar`

can take on any value and still satisfy the constraints. Sometimes the variable is said to be *nonground*. We'll refer to *nonground* variables as being "fresh".

Furthermore, if you have two variables that can be anything they will have values like `_.0`

and `_.1`

, meaning that each can be anything and they can be distinct from another. If they were both `_.0`

, it would mean they can be anything but must be equal to another.

Logic variables are introduced into a program in two ways.

The first is the main query variable introduced in

`(run* [query-variable]`

` ...)`

whose values will be the return value of the `(run* ...) `

expression. There can only be one such main query variable, and we use q for query variable. Feel free to use a more descriptive name for your own logic programs.

The other method of introducing logic variables is using the '`fresh`

' operator, much like 'let' in normal Clojure. For instance the snippet

`(fresh [a b c] &logic-expressions)`

introduces three logic variables `a`

, `b`

and `c`

, that may be used within the logic-expressions.

### More on Constraints

Logic expressions constrain the values of logic variables. All expressions directly beneath run* are combined in a logical AND (sometimes referred to as conjunction). So in

`(run* [q]`

` (constraint-1)`

` (constraint-2)`

` (constraint-3))`

each expression constrains q in some way, and `run*`

will return the values of `q`

that satisfies all three constraints in the expression.

### Goals

`core.logic`

is based upon miniKanren. miniKanren dictates that we define our constraints in a particular way. Each is a goal that either succeeds or fails.

The logic engine explores the possible values of all the `lvars`

and returns the value of q in each case where the logic expression, as a whole, succeeds. In the example above all the goals are conjunction, hence the expression succeeds if and only if all the goals succeed.

### The `core.logic`

operators

miniKanren and hence `core.logic`

are based upon three core operators: `fresh`

, `==`

and `conde`

.

`fresh`

We have already seen fresh, which introduces new lvars, in the fresh state, into the logic program.

`unify`

, or `==`

The most fundamental operator is ==, or unify:

`(== lvar1 lvar2)`

which serves to constrain each `lvar`

to have the same set of possible values. It is a goal that succeeds if `lvar1`

can be made equal to `lvar2`

, otherwise it fails.

##### Unification of a single `lvar`

with a literal

In the simplest case you can use Clojure literals for `lvar1`

or `lvar2`

. For example the expression:

`(run* [q]`

` (== q 1))`

succeeds if q can be made to have the value of 1. As run* introduces q in the fresh state, this is possible. Hence the unify goal succeeds, hence run* returns the list of successful values of q, that is (1). This means that the set of possible values that q can assume, under this constraint is only the integer 1. The mental shortcut is to view unify as constraining q to be equal to 1.

You unify more complex datatypes too:

`(run* [q]`

` (== q {:a 1 :b 2}))`

evaluates to: `({:a 1, :b 2})`

.

Similarly

`(run* [q]`

` (== {:a q :b 2} {:a 1 :b 2}))`

returns `(1)`

, which is rather exciting.

Finally, the order of the arguments to `==`

is irrelevant,

`(run* [q]`

` (== 1 q))`

is also `(1)`

.

**Gotcha**: Now although when printed an `lvar`

looks like a list, this is not the literal syntax for an `lvar`

(the reader will not read it); there is not in fact a literal syntax for an `lvar`

. So the program

`(run* [q]`

` (== q (1 2 3)))`

evaluates to `((1 2 3))`

, not `(1 2 3)`

.

That is, `q`

can only take the value of the list `(1 2 3)`

, not either 1 or 2 or 3, which is what you might have expected.

As stated above `run*`

finds the solutions that satisfy all the constraints. This is because `run*`

composes the goals in logical conjunction. Thus,

`(run* [q]`

` (== q 1)`

` (== q 2))`

returns `()`

: there are no values of `q`

that satisfy all the constraints. That is, it's impossible for `q`

to equal 1 AND for `q`

to equal 2 at the same time.

##### Unification of two `lvars`

When you unify two `lvars`

, the operation constrains each `lvar`

to have the same set of possible values. A mental shortcut is to consider unification to be the intersection of the two sets `lvar`

values.

To demonstrate this we have to cheat and go out of order a bit. As mentioned there is no literal syntax for an `lvar`

, so to constrain `lvar1`

to have value `(1, 2, 3)`

, we have to introduce a goal, `membero`

:

`(membero x l)`

For now, and this is true but not the full story, think of it as constraining `x`

to be an element of the list `l`

. So the program

`(run* [q]`

` (membero q [1 2 3]))`

evaluates to `(1, 2, 3)`

, meaning that `q`

can be either 1 or 2 or 3, as we wanted. Now we have our full demonstration:

`(run* [q]`

` (membero q [1 2 3])`

` (membero q [3 4 5]))`

First we use

`run*`

and ask it to return the value of the`lvar`

under a set of constraints.In the first we constrain

`q`

to have the value`(1, 2, 3)`

, that is,`q`

can be either 1 or 2 or 3.Then we constrain the same

`lvar`

,`q`

, to have the value`(3, 4, 5)`

, that is,`q`

can be 3 or 4 or 5.In order to satisfy both constraints

`q`

can only be 3, hence`run*`

returns`(3)`

.

Another way to write the same thing, with unification is

`(run* [q]`

` (fresh [a]`

` (membero a [1 2 3])`

` (membero q [3 4 5])`

` (== a q)))`

Here we introduce an additional `lvar`

, `a`

, with fresh and constrain it to being either 1 or 2 or 3. Then we constrain `q`

to being either 3 or 4 or 5. Finally we unify `a`

and q` `

leaving both with the value of their intersection: `(3)`

.

`core.logic`

is Declarative

Now some magic: the order of constraints does not matter as far as the value of the (run* ...) expression is concerned. So the programs:

`(run* [q]`

` (fresh [a]`

` (membero q [1 2 3])`

` (membero a [3 4 5])`

` (== q a)))`

` (run* [q]`

` (fresh [a]`

` (membero a [3 4 5])`

` (== q a)`

` (membero q [1 2 3])))`

` (run* [q]`

` (fresh [a]`

` (== q a)`

` (membero a [3 4 5])`

` (membero q [1 2 3])))`

all evaluate to `(3)`

.

#### The final operator, `conde`

We have introduced `run*`

, `fresh`

and `==`

, and there is only one more operator: `conde`

. Unsurprisingly `conde`

behaves a lot like `cond`

, and is **logical disjunction** (OR). Its syntax is

`(conde &clauses)`

where each clause is a series of at least one goal composed in conjunction. `conde`

succeeds for each clause that succeeds, independently. You can read a `conde`

goal:

`(run* [q]`

` (conde`

` [goal1 goal2 ...]`

` ...))`

a bit like this:

`(run* [q]`

` (OR`

` [goal1 AND goal2 AND ...]`

` ...))`

Some further examples may help:

`(run* [q]`

` (conde`

` [succeed]))`

returns `(_.0)`

. `conde`

succeeds because `succeed`

succeeds, however `q`

is not involved and hence can take on any value.

There can be any number of goals in the clause

`(run* [q]`

` (conde`

` [succeed succeed succeed succeed]))`

also returns `(_.0)`

and each term in the clause for `conde`

succeeds, and they are combined in logical conjunction, hence succeeding. However,

`(run* [q]`

` (conde`

` [succeed succeed fail succeed]))`

returns `()`

, as `conde`

failed because of the fail in the clause, which due to the conjunction causes the entire clause to fail. Thus there are no values of `q`

that can cause the expression to succeed.

Furthermore, `conde`

succeeds or fails for each clause independently

`(run* [q]`

` (conde`

` [succeed]`

` [succeed]))`

returns `(_.0 _.0)`

. There are two values here because `conde`

succeeds twice, once for each clause.

`(run* [q]`

` (conde`

` [succeed]`

` [fail]))`

returns `(_.0)`

because `conde`

succeeds only for the first clause.

The above examples show the logical structure, but let's see some output.

`(run* [q]`

` (conde`

` [succeed (== q 1)]))`

returns `(1)`

. This is because `succeed`

and `(== q 1)`

only both succeed if `q`

can be made equal to 1. Having two elements in the `conde`

clause is the usual structure as it reminds us of `cond`

, but don't be misled:

`(run* [q]`

` (conde`

` [(== q 2) (== q 1)]))`

returns `()`

. If you expect `conde`

to produce the same results as `cond`

, your thought process might incorrectly lead you to assume that this will return `(1)`

. While following from a seemingly logical set of premises, it is essential to understand that this is patently wrong — each goal in a `conde`

clause is "composed in conjunction". Since it is not possible for `q`

to be 2 and 1 at the same time, the clause fails, and hence `conde`

fails. Without a possibility of success, `q`

returns the value `()`

.

`(run* [q]`

` (conde`

` [(== q 1)]`

` [(== q 2)]))`

returns `(1 2)`

. The difference here is that each unification is in a different clause of `conde`

, and each can succeeds independently, producing a value for `q`

.

### More Goals

We've seen the interaction of the three operators: `fresh`

, `conde`

and `==`

, and these are the primitives of logic programming. `core.logic`

provides some higher level goals based on these primitives, let's take a look at a few of them.

`conso`

(the Magnificent)

The most basic of these goals is `conso`

; understand this and the rest will follow. `conso`

is, unsurprisingly, the logic programming equivalent of `cons`

. Recall

`(cons x r)`

returns `s`

where `s`

is a seq with the element `x`

as its head and the seq `r`

as its rest:

`(cons 0 [1 2 3])`

returns `(0 1 2 3)`

. `conso`

is very similar but with the 'resulting' seq passed as an argument

`(conso x r s)`

It is a function that succeeds only if `s`

is a list with head `x`

and rest `r`

. Hence, within a logic expression it constrains `x`

, `r`

and `s`

in this way. Again we can use either `lvars`

or literals for any of `x r s`

. So:

`(run* [q]`

` (conso 1 [2 3] q))`

returns `((1 2 3))`

; that is, `q`

is the `lvar`

that can only take on the value of the list `(1 2 3)`

. We have asked `run*`

to find the value of `q`

, being a list with head 1 and rest `(2 3)`

, and it finds `(1 2 3)`

.

Now some more magic:

`(run* [q]`

` (conso 1 q [1 2 3]))`

returns `((2 3))`

; `q`

is constrained to be that list which, when 1 is added as the head results in the list `(1 2 3)`

.

`(run* [q]`

` (conso q [2 3] [1 2 3]))`

returns `(1)`

; `q`

is the element that when added to the head of the vector `(2 3)`

results in vector `(1 2 3)`

. Even more interesting:

`(run* [q]`

` (conso 1 [2 q] [1 2 3]))`

returns `(3)`

; `q`

is that element of the vector (2 element) that when 1 is added as the head becomes the vector `(1 2 3).`

In summary: `(conso f r s)`

succeeds if `(first s)`

is `f`

and `(rest s)`

is `r`

.

`resto`

`resto`

is the complement of `conso`

`(resto l r)`

constrains whatever logic variables are present such that `r`

is `(rest l)`

. So

`(run* [q]`

` (resto [1 2 3 4] q))`

returns `((2 3 4))`

. The same reorderings and substitutions that we showed for `conso`

apply here too.

In summary: `(resto l r)`

succeeds if `(rest l)`

is `r`

.

`membero`

We've already had a sneak peak at `membero`

:

`(membero x l)`

constrains whatever logic variables are present such that `x`

is an element of `l`

.

`(run* [q]`

` (membero q [1 2 3]))`

returns `(1, 2, 3)`

; that is, either 1 or 2 or 3.

`(run* [q]`

` (membero 7 [1 3 8 q]))`

returns `(7)`

, the only value that `q`

can take such that `7`

is an element of `(1 3 8 q)`

.

In summary: `(membero x l)`

succeeds if `x`

is any of the members of `l`

.

## Summary

This introduction has given the basic idea of logic programming: it is a set of logic variables and the set of constraints upon them, which are input to a solution engine which returns the complete set of consistent solutions to that set of constraints.

The key concepts are the logic variable and the goal:

A logic variable is a variable that can assume a number of distinct values one at a time.

A goal is a function that returns succeed or fail.

Goals are composed into a logic expression.

`run*`

invokes the logic engine over a logic expression and returns the complete set of values of the query logic variable that allow the logic expression to succeed.