miniKanren

_miniKanren_
_miniKanren.plt_

============================================================
DESCRIPTION

An embedding of logic programming in Scheme. 

The miniKanren language in this package is the language presented in
Byrd and Friedman's "From variadic functions to variadic relations"
[1]; it is a descendant of the language presented in Friedman, Byrd,
and Kiselyov's _The Reasoned Schemer_ [2]. The code itself was written
by (in alphabetical order) Will Byrd, Dan Friedman, Oleg Kiselyov, and
Chung-Chieh Shan.

============================================================
PROVIDED FILES AND NAMES

This collection provides one file:

_minikanren.ss_

minikanren.ss provides the following new core forms, which comprise
the core of the miniKanren language. These forms are all described in
much greater detail in Byrd and Friedman's "From variadic functions to
variadic relations" [1], which those interested in learning how to
use this library should consult. The documentation here is included
only for reference.

> (== e_1 e_2)                                             SYNTAX
Introduces a new goal that unifies two values.

> (conde ((goal_1 goal_1a ...) (goal_2 goal_2a ...) ...))  SYNTAX
Introduces a new goal that behaves analagously to cond.

> (fresh (x ...) goal_0 goal_1 ...)                        SYNTAX 
Introduces a new logic variable bound to each x in the scope of its
body, each clause of which should be a goal.

> (run n (x) goal_0 goal_1 ...)                            SYNTAX
Finds up to n ways to instantiate the logic variable bound to x
such that all the goals in its body succeed. (If n is #f, then run finds
all satisfying instantiations for x.) 



minikanren.ss also provides the following helpers:

> (run* (x) goal_0 goal_1 ...)                             SYNTAX
Equivalent to (run #f (x) goal_0 goal_1 ...)

> (conda ((goal_1 goal_1a ...) (goal_2 goal_2a ...) ...))  SYNTAX
> (condu ((goal_1 goal_1a ...) (goal_2 goal_2a ...) ...))  SYNTAX
Variants of conde that correspond to the committed-choice of Mercury
and are used in place of Prolog's cut.

> (project (x ...) goal_1 goal_2 ...)                      SYNTAX
Applies the implicit substitution to zero or more lexical variables,
rebinds those variables to the values returned, and evaluates the goal
expressions in its body. The body of a project typically includes at
least one begin expression --- any expression is a goal expression if
its value is a miniKanren goal. project has many uses, such as
displaying the values associated with variables when tracing a
program.


============================================================
REFERENCES

[1] Byrd, William and Friedman, Daniel. "From variadic functions to
variadic relations: a miniKanren perspective." In Proceedings of the
2006 Scheme and Functional Programming Workshop, 2006. Available
online: http://scheme2006.cs.uchicago.edu/12-byrd.pdf.

[2] Friedman, Daniel, Byrd, William, and Kiselyov, Oleg. The Reasoned
Schemer. MIT Press, 2005.