kanren

[:toc:]

kanren

Logic: Programming it is about. - Relational Programming :-)

---

some Nomenklatura

• reify: to convert mentally into a thing; to materialize.

• unify: to make, form into, or cause to become one; to combine (two or more) in one; to join (one or more) to or with another or others so as to form one whole or unit; to unite, consolidate.

• expression The action of expressing or representing (a meaning, thought, state of things) in words or symbols; the utterance (of feelings, intentions, etc.). The action or process of manifesting (qualities or feelings) by action, appearance or other evidences or tokens.

---

Logical Statement

A logical statement is built along states from variables, and goals.

Create an initial state, then obtain some variables (and resulting state) from it.

Construct a goal consisting of variable bindings and logical operations (AND, OR), or predicates.

Then evaluate the goal using the state resulting from making the variables.

Evaluating a goal returns all possible solutions to the statement in the form of a number of states containing suitable variable bindings.

---

Note: Most often, the EmptyState is used as initial state.

A predicate is what -given some variable- evaluates to #t or #f (with/in a given state).

---

Any value used in a state must be unifiable.

Unifying two values produces zero or more possible states, where variables that may be contained in the values may be bound in various combinations.

---

Basics

Basic constructs of relational programming are

• the Goals
  • Yeah aka #s (aka Succeed) and
  • Fail aka #u,
• fresh logic Variables ,u ,v ,w...
• operators
  • ==, aka Eq,
  • Fresh and
  • Conde.

The laws of operators fresh, == and conde are postulated:

The law of ==:

(== v w) is the same as (== w v)

The law of Fresh:

If x is fresh, then (== v x) succeeds and associates x with v.

The law of Conde:

To get more values from conde, pretend that the successful line has failed, refreshing all variables that got an association from that line.

---

µKanren

The entire system is comprised of a handful of facilities and functions for

• the implementation of variables,
• streams themselves,
• the interface for creating and combining streams, and
• four primitive goal constructors.

Variables & eXpressions

V - Variable

A logical Variable may be named or anonymous.

• Method Fresh(name string) V creates a named Variable
• Method V() V produces a new anonymous Variable

Note: Internally, V() calls Fresh with a auto-generated (and previously unused) name-string.

Equality is determined by coincidence of their name-string.

• u.Equal(v) bool reports it.

X -eXpression

In our context. this is what a Variable may represent, what a Variable may be bound to.

• Some call it Value - as in "Value of a Variable".
• Some call it Term - as in "Term as part of an eXpression".

Circular reference

Some eXpression x may be very basic, e.g consist of just one single thing (Atom). And such, in turn, may just happen to be a Variable.

• x.IsVariable() bool reports this,
• x.AsVariable() (V, bool) reveals the Variable (if any)
• v.Expr() X expresses a Variable v as eXpression.

Thus, we have a circular self reference:

• any Variable may camouflage as an eXpression, and
• some eXpression may reveal to be nothing but a single Variable.

V->X->V->X->V->X->V->X->V->X->V->X->V->X->V->X->V ...

This (indirect) self-reference is almost magical - and very important.

Bind & Substitute

In the literature we meet a lot of overloaded terminology here and we need to take great care in order to avoid confusion.

Constraint programming calls it: Assignment or assignation (or model).

bind V<->X

How to bind a Variable and/with/to some eXpression?

A bind consists of:

• some Variable being bound, and
• some eXpression(Value/Term) related to it, given to it, assigned to it.

The eXpression(Value/Term) substitutes the Variable, so to say.

Thus: bind establishes a relation between V and X.

Within the notation of symbolic expressions we may write individual members of such relation as pair: (x . y) or (y . 5) or (x . (y . 5)).

The Binding of some Variable may change over time.

Any Variable may be (or may become) unbound.

No Variable can ever be bound to more than one eXpression at the same time.

Note: Some bound eXpression may itself be a logic Variable: e.g. (y . 5)(x . y)

Substitute

Once there is a bind, we may use it on any other eXpression (think: formula).

Every occurrence of the Variable (being bound) shall be replaced/substituted by the eXpression (the Variable is bound to/with).

Thus, we may need to Walk the eXpression, and replace any occurrence of the Variable.

bind.Ings

b.Bind( V, X )
b.Bound( V )     -> ( value X, isBound bool )
b.IsBound( V )   -> ( isBound bool )

b.Resolve( X )   -> X
b.Walk( X )      -> X

b.Occurs( V, X ) -> bool

b.Unify(x, y X ) -> bool 

Representations:

• triangular
• idempotent

Logical State

Mainly, it's just a bind.Ings. (Which some call Substitution).

Thus, a logical state is a collection of variable bindings.

Some say: A _Substitution_ `S` is a mapping/association between logic variables `V` and their values `T` (also called `terms`).

Note: Some `T`  may itself be a logic Variable: e.g. `(y . 5)(x . y)`

() is the _empty Substitution_

Unify & Reify

Unify

b.Unify(a, b) attempts to unify a and b (with respect to binding b) and returns a (potentially extended) Substitution, or #f (fails).

Reify

Any eXpression containing some logic variable may be considered "vague" due to their "real" or "appropriate" or "right" content / meaning / value not being known (yet).

In general, "Reify" means to convert mentally into a thing; to materialize it. In our context,Reification is the process of turning some eXpression into another eXpression that does not contain any logic variable any more.

S.Reify( X ) -> X

Reify takes an arbitrary eXpression, perhaps containing variables, and returns it reified.

Logical Goals and Goal Constructors

Goals are used to specify logical statements.

A Goal g is a function that maps a substitution s to an ordered sequence of zero or more values. (These values are almost always substitutions.)

The sequence of values may be infinite. Thus, it is not a list but as a special kind of stream.

type Goal func(S) ValueStream:

Evaluate a Goal to produce zero or more States, or collections of variable bindings/Substitutions.

ValueStream

(mZero) represents the empty stream of values.

(Unit a) represents the stream containing just a, if a is a value.

(Choice a f) represents a non-empty stream, where

• a is the first value in the stream, and where
• f is a function of zero arguments. Invoking the function f produces the remainder of the stream.

type Cons struct {head, tail}is an alternative name & implementation for Choice

Goal Constructors

A Goal does either

• fail, or
• succeed

Evaluating a Fail goal always results in zero states.

Evaluating a UnifyVal goal attempts to unify a variable and a value.

Evaluating a UnifyVar goal attempts to unify the variables.

A Conjunction goal evaluates its sub-goal a using a given state, then evaluates sub-goal b using the results.

Evaluating a Disjunction goal returns all the possible states of evaluating a and b.

Evaluating a Predicate goal returns the given state only if the function returns true.

αKanren

αKanren extends core miniKanren with operators for nominal logic programming

fresh

introduces noms ("Names" / "Atoms")

hash # - a term constructor`

used to limit the scope of a nom within a term ...

tie - a term constructor

A term constructed using tie ◃▹ is called binder. In the term created by the expression (◃▹ a t), all occurrences of the nom a within term t are considered bound.

We refer to the term t as the body of (◃▹ a t), and to the nom a as being in binding position.

The ◃▹ constructor does not create noms; rather, it delimits the scope of noms, already introduced using fresh.

References

Kanren Implementations

S-Expression based languages

Lisp

./.

Scheme

miniKanren - a canonical implementation.

Implements the language described in the paper:

William E. Byrd, Eric Holk, and Daniel P. Friedman. miniKanren, Live and Untagged: Quine Generation via Relational Interpreters (Programming Pearl). To appear in the Proceedings of the 2012 Workshop on Scheme and Functional Programming, Copenhagen, Denmark, 2012.

Core µKanren: ==(aka Unify), fresh, conde Extensions: =/=, symbolo, numbero, absento

µKanren - a reference implementation.

Kanren-Book

The little Schemer The seasoned Schemer The reasoned Schemer

Code from the books by Peteris Krumins ([email protected]). His blog is at http://www.catonmat.net/ -- good coders code, great reuse.

Racket

Clojure

core.logic) core.logic.wiki

logic-tutorial

Rust

rslogic is a logic programming framework for Rust inspired by µKanren.

Go

gologic includes examples

gominikanren

ukanren-go

Bibliograpy

Fairness mentions early Kanren.

• miniKanren Live and Untagged: Quine Generation via Relational Interpreters

• cKanren: miniKanren with Constraints

• μKanren: A Minimal Functional Core for Relational Programming

• Relational Programming in miniKanren: Techniques, Applications, and Implementations

• Pure, Declarative, and Constructive Arithmetic Relations (Declarative Pearl)

• From Variadic Functions to Variadic Relations - A miniKanren Perspective

• core.logic

Notes todo

Plenty of other miniKanren use log-time persistent maps for their substitutions; core.logic (https://github.com/clojure/core.logic) and veneer (https://github.com/tca/veneer) certainly do.

---

JaCoP is a finite domain solver written in pure Java that has been in continuous development since 2001. In the yearly MiniZinc constraint challenges it has received the Silver award in the fixed category for the past three years.

Some basic testing seems to show that JaCoP is anywhere from 10X-100X faster than core.logic at solving Finite Domain problems. While there is a considerable amount of work to be done to improve the performance of core.logic's general constraint framework, it's unlikely we'll achieve JaCoP finite domain solving performance in the near future. Thus JaCoP integration is attractive.

---

miniKanren operators

eq is the basic goal constructor: it succeeds if its arguments unify, fails otherwise.

conde accepts two or more clauses made of lists of goals, and returns the logical disjunction of these clauses.

fresh accepts a list of one or more logic variables, and a block containing one or more goals. The logic variables are bound into the lexical scope of the block, and the logical conjuction of the goals is performed.

Interface operators

run is similar to run_all, but returns at most n results.

run_all accepts a list of one or more logic variables, an optional module name for a constraint solver, and a block containing one or more goals. The logic variables are bound into the lexical scope of the block, and the logical conjunction of the goals is performed. All results of the conjunction are evaluated, and are returned in terms of the first logic variable given.

Impure operators

ExKanren/lib/minikanren.ex

conda

conda accepts lists of goal clauses similar to conde, but returns the result of at most one clause: the first clause to have its first goal succeed.

run_all([out, x, y]) do
	conda do
		[eq(1, 2), eq(out, "First clause")]
		[appendo(x, y, [1, 2, 3]), eq(out, {x, "Second clause"})]
		[eq(x, y), eq(x, 1), eq(out, {{x, y}, "Third clause"})]
	end
end

[{[], "Second clause"}, {[1], "Second clause"}, {[1, 2], "Second clause"}, {[1, 2, 3], "Second clause"}]

condu

condu is similar to conda, but takes only a single result from the first goal of the first successful clause.

project

project binds the associated value (if any) of one or more logic variables into lexical scope and allows them to be operated on.

run_all([out, x, y]) do
	eq(x, 3)
	eq(y, 7)
	project([x, y]) do
		eq(x + y, out)
	end
end
[10]

Some common relations used in miniKanren.

succeed is a goal that always succeeds. succeed is a goal that ignores its argument and always succeeds.

fail is a goal that always fails. fail is a goal that ignores its argument and always fails.

heado relates h as the head of list ls. tailo relates t as the tail of list ls. conso relates h and t as the head and tail of list ls. (Equivalent to eq([h | t], ls).)

membero relates a as being a member of the list ls.

appendo relates the list ls as the result of appending lists l1 and l2.

emptyo relates a to the empty list.

Non-relational functions

onceo accepts a goal function, and allows it to succeed at most once.

copy_term copies the term associated with x to y, replacing any fresh logic variables in x with distinct fresh variables in y.

is projects its argument b, and associates a with the result of the unary operation f.(b)

fresho succeeds if its argument is a fresh logic variable, fails otherwise.