chickadee » mini-kanren

CHICKEN miniKanren

This repository provides the canonical miniKanren implementation, wrapped as an egg for CHICKEN Scheme. The egg also includes extensions originally provided by Alex Shinn and modified to work with this version of miniKanren, which represent code and relations from *The Reasoned Schemer 2nd Ed.* (Dan Friedman, William Byrd, and Oleg Kiselyov, MIT Press.).

Installation

$ chicken-install -s mini-kanren

Or

$ chicken-install -s -test mini-kanren

Modules

To get started with this egg, you can import mini-kanren module:

#;1> (import mini-kanren)

miniKanren Language

The miniKanren language is a relational programming language described in the book "The Reasoned Schemer." For a complete understanding of the language and how to use the various procedures provided by this egg, it is suggested that one work through the Reasoned Schemer.

If you cannot obtain a copy of the book, or simply wish to learn miniKanren through different means, the official language page has a host of useful tutorials for getting started.

Glossary

Here is a list of terms that may pop up often in the documentation.

Succeed / success

A condition in which a goal has completed and unified any and all symbols relevant to the goal's definition.

Fail / failure

A condition in which a goal has completed and has not unified all symbols passed to that goal.

Goal

A statement within the miniKanren language that seeks to unify zero or more logic variables relevant to its definition. A goal can be thought of as a statment about some entity or entities, e.g. The goal (caro l a) unifies the variable a with the car of list l. A goal can be thought of as any relational procedure that returns a success or failure.

Logic variable

A symbol representing some quantity (known or unknown) to be related by some goal(s). A variable is ground if-and-only-if it represents a single possible value. Otherwise, the variable is considered fresh

Unification

the process in which a logic variable is ground to a value. E.g. the goal (== q 1) unifies the variable q to the value 1. If q is already ground, this goal must fail. However, if q is fresh, then this goal succeeds and the logic variable q is thereafter ground.

Egg / Language API

Core Language

Interface operators

(run* (x) goal0 goal ...)syntax

Primary interface operator for miniKanren. run* instantiates a fresh variable x, and runs through each subsequent goal provided. It returns a list of all possible unifications of x where goals goal0, goal, and so on succeed.

Note: As long as there are a finite number of possible values that can be unified with x, then run* is guaranteed to terminate. However, this importantly doesn't make two guarantees:

1. The speed at which the answers will be found. The runtime is generally fast, but miniKanren, and more generally relational and logic programming necessarily requires one to think about the best way to prune the search space of possible answers.
2. The order of answers in x that satisfy the goals.

(run n (x) goal0 goal ...)syntax

Interface operator for miniKanren. Behaves like run*, except that it will only provide up to n possible unifications of x. This is useful if there are a finite number of solutions and one wants to merely take the first n possible solutions.

Logical Operators

succeedconstant

A goal that is always successful. Equivalent to (== #f #f).

failconstant

A goal that always fails. Equivalent to (== #t #f).

(fresh (a ...) goal0 goal ...)syntax

Creates a logic variable bound to each of the symbol(s) (a ...). These logic variables are then lexically scoped within this macro, whereupon each of the subsequent goals can be evaluated.

Example:

(run* (q)
  (fresh (a d)
    (== a 1)
    (nullo d)
    (conso a d q)))
; => ((1))

(conde (goal0 goal ...) (goal0^ goal^ ...) ...)syntax

Conditional performing logical disjunction over each set of (goal0 goal ...) clauses. The first goal in each clause (i.e. goal0 or goal0^) is considered the head of that clause. Behaves similarly to cond in regular Scheme, except that each clause provides one possible path to unification through the subsequent goals.

In the first edition of miniKanren, conde was separate from condi, which is no longer provided as part of the language. conde now interleaves each of the possible clauses on recursive calls, so condi (which used to stand for interleaving-conditional) is no longer needed.

(conda (goal0 goal ...) (goal0^ goal^ ...) ...)syntax

Conditional behaving much like conde, except that conda does a soft-cut over the remaining goals. That is to say, if any of the heads of the clauses succeed, then the remaining clauses will all be cut (i.e. ignored) from future searches.

(ifa (goal0 goal ...) b ...)syntax

Single-branch version of conda. ifa relates to conda the way that if relates to cond in regular Scheme.

(condu (goal0 goal ...) (goal0^ goal^ ...) ...)syntax

Conditional behaving much like conde, except that condu performs a committed choice. What that means is that if the head of any goal succeeds, then the remaining goals of that clause will only be run once thereafter.

(ifu (goal0 goal ...) b ...)syntax

Single-branch version of condu. ifu relates to condu the way that if relates to cond in regular Scheme.

== u vprocedure

Primary unification goal. u and v are either logic variables or values. If the two can be unified (i.e. if the two logic variables hold the same value, or if two values are the same) then this goal succeeds. When used on fresh variables, guarantees that the two logic variables will always be unified.

=/= u vprocedure

Disequality goal. This goal succeeds if-and-only-if u and v are not unified. When used on fresh variables, ensures that u and v never unify.

var? vprocedure

Predicate procedure (not a goal) that returns true if-and-only-if v is a logic variable.

(project (x ...) goal0 goal ...)syntax

Extracts the value of zero or more logic variables into lexical variables of the same name, and executes the goals within the body of the project call.

Example:

;; The following code will fail because `+` is not relational.
(run 1 (q)
  (fresh (a b)
    (== a 1)
    (== b 2)
    (== q (+ a b))))

; => Error: (+) bad argument type - not a number: #(a)


;; However, if we use project to get the values of the logic variables,
;; we can use those directly.
(run 1 (q)
  (fresh (a b)
    (== a 1)
    (== b 1)
    (project (a b)
      (== q (+ a b)))))

; => (3)

project can be though of as an escape hatch to break out of miniKanren. It will give you the values of the variables, but it only works if the variables are grounded. In the above example, if the logic variable b is not ground, then the b inside the body of project will not be lexically bound to anything, and will still be a fresh logic variable.

In most cases it is advised to avoid project when you can. It can be a powerful tool for debugging the values of logic variables when writing miniKanren code; however, excessive use will lead to extremely non-relational code that will be hard to work with in miniKanren.

onceo goalprocedure

A procedure that ensures that goal executes exactly one time.

Predicate Goals

make-tag-A tag predprocedure

Constructs a goal that succeeds whenever pred returns #t for a single value, and fails if pred returns #f for that value. This creates a predicate-goal that tags the logic variable with the tag name tag.

Note: This is primarily useful for atomic-type predicates, i.e. predicates for atomic types that do not have explicit constructors. This is what is used to implement symbolo, for example:

(define symbolo (make-tag-A 'sym symbol?))

One should avoid using this for types that have constructors (e.g. pairs have cons, lists have list), and should instead prefer creating relational constructors for such types. This egg provides symbolo, numbero, booleano, charo, and atomo using this method. However, make-tag-A is highlighted here in case users have new atomic types that they wish to extend miniKanren with.

symbolo sprocedure

A tagged constraint goal that succeeds if-and-only-if s can be unified with a symbol.

numbero nprocedure

A tagged constraint goal that succeeds if-and-only-if n can be unified with a number.

booleano bprocedure

Predicate goal that succeeds if-and-only-if b can be unified with a boolean. When b is fresh, this guarantees that b can only be unified with #t or #f.

charo cprocedure

A tagged constraint goal that succeeds if-and-only-if c can be unified with a character.

atomo aprocedure

A tagged constraint goal that succeeds if-and-only-if a can be unified with an atom.

nullo pprocedure

Predicate goal that succeeds if-and-only-if p is the null list. When p is fresh, it guarantees that p can only unify with the null list '().

pairo pprocedure

Predicate goal that succeeds if-and-only-if p unifies with any pair. When p is fresh, it guarantees that p can only unify with a pair.

listo lprocedure

Predicate goal that succeeds if-and-only-if l unifies with any list. When l is fresh, it guarantees that l can only unify with a proper list.

Numbers in miniKanren

The procedures defined here are largely the same as in The Reasoned Schemer. As it turns out, constructing relations over numbers is very hard. Specifically, relations involving decimal number systems are very hard. It is much easier when representing numbers as bits, where operations on each bit can be performed relationally.

While individual numbers can be unified in the miniKanren language, doing any kind of arithmetic on them will be quite difficult if you want to keep everything relational. To get around this, we first convert numbers into a list of bits in little-endian order, and perform relations on those lists. From there, we can convert to / from bit-lists in order to switch between decimal representations (e.g 1, 2, 7, 42, ...) and bit representations (e.g. 0 is '(), 1 is (1), 2 is (0 1), etc.).

As you might guess, this can end up making many numerical operations quite slow, especially for large numbers. There are some ways to get around this by introducing finite domains, but this egg does not currently provide operations on finite domains of numbers. Likewise, project is always an option, but remember: it is an escape hatch and is not generally recommended.

Floating point / inexact numbers are not supported in miniKanren.

Negative numbers are not supported in miniKanren.

build-num nprocedure

Constructs a bit-list to represent a number given a positive exact number.

Example:

(build-num 0) ; => ()
(build-num 1) ; => (1)
(build-num 2) ; => (0 1)

little-endian->number bprocedure

Procedure that converts a bit-list in little-endian form back into a Scheme number. The opposite of build-num.

zeroo nprocedure

A goal that succeeds if-and-only-if the logic variable n is zero (i.e. null bit list). When n is fresh, this guarantees that it can only ever be bound to the null list. This makes it equivalent to (nullo n).

poso nprocedure

A goal that succeeds if-and-only-if the logic variable n is a positive number (i.e. non-null bit list). When n is fresh, this guarantees that it can only ever be bound to a non-null bit list. This makes it equivalent to (listo n).

pluso n m kprocedure

+o n m kprocedure

A goal that unifies two logic variables n and m such that the bit-lists they represent sum to k when added. Think of this as if you were doing (define k (+ n m)), except that it is relational.

Example:

(run 1 (q)
  (let ((a (build-num 4))
        (b (build-num 3)))
    (fresh (n k)
      (== k a)
      (== n b)
      (pluso n q k))))
; => (1)

minuso n m kprocedure

-o n m kprocedure

A goal that unifies two logic variables n and m such that the bit-lists they represent subtract to k. Think of this as if you were doing define k (- n m)), except that it is relational.

*o n m pprocedure

A goal that unifies two logic variables n and m such that the bit-lists they represent multiply to k. Think of this as if you were doing (define k (* n m)), except that it is relational.

/o n m q rprocedure

A goal that unifies two logic variables n and m such that the bit-lists they represent divide to the quotient q with remainder r.

<o n mprocedure

<=o n mprocedure

Predicate goals that succeed if-and-only-if n is less than (or equal to, in the latter case) m.

logo n b q rprocedure

Goal that unifies two logic variables n (number) and b (base) such that they form the logarithm with power q and remainder r.

expo b q nprocedure

Goal that unifies the two logic variables b and q such that they form the exponential n. Think of this as doing (define n (expt b q)), except that it is relational.

Extras

caro p aprocedure

Goal that unifies a logic variable representing a pair p with the car of that pair, a.

cdro p dprocedure

Goal that unifies a logic variable representing a pair p with the cdr of that pair, d.

conso a d pprocedure

Goal that unifies two logic variables a and d, representing the car and cdr of a pair, with the logic variable representing the pair p.

membero x lprocedure

Goal that unifies x with any member of the list l.

rembero x l outprocedure

Goal that unifies out with a list where x has been removed from l.

appendo l s outprocedure

Goal that unifies two lists l and s with a list out, which is the two lists appended to one another.

flatteno s outprocedure

Goal that unifies a list s with out, where out represents a list with the same elements of s, except that out is flattened (i.e. only contains atoms, not pairs).

lengtho s nprocedure

Goal that unifies a list s with the length of that list k.

anyo goalprocedure

Goal that succeeds if goal succeeds.

neveroconstant

Goal that always fails. Equivalent to (anyo fail).

alwaysoconstant

Goal that always succeeds.

distincto sprocedure

Goal that guarantees that no element of the list s will ever unify with another element of s.

permuteo xl ylprocedure

Goal that permutes xl into yl. It may not terminate if xl is not ground.

Example:

;; Get 5-permute-2, i.e. all 2 permutations of the numbers 1 through 5.
(run* (q)
  (lengtho q (build-num 2))
  (permuteo '(1 2 3 4 5) q))

; => (1 2) (2 1) (2 3) (1 3) (3 1) (3 2) (3 4) (2 4) (1 4) (4 1) (4 2)
;    (4 3) (3 5) (4 5) (2 5) (1 5) (5 1) (5 2) (5 3) (5 4))

Repository

Find the project on Github.

Version History

1.2.0

Adds flatteno, lengtho, distincto, and permuteo

1.1.1

Removes test egg from test-dependencies.

1.1

CHICKEN 5 support

License

The MIT License (MIT)

Copyright (c) 2014 Daniel P. Friedman, Oleg Kiselyov, and William E. Byrd
Modifications Copyright (c) 2016 Alex Shinn, Jeremy Steward

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.