Mini  Kanren:   logic programming in Scheme
==
conde
condi
fresh
run
succeed
fail
run*
conda
condu
project
8.12

MiniKanren: logic programming in Scheme🔗ℹ

 (require minikanren) package: minikanren

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.

Minikanren 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.

syntax

(== e_1 e_2)

Introduces a new goal that unifies two values.

syntax

(conde [goal_1 goal_1a ...] [goal_2 goal_2a ...] ...)

Introduces a new goal that behaves analagously to cond.

syntax

(condi [goal_1 goal_1a ...] [goal_2 goal_2a ...] ...)

condi behaves like conde, except that its values are interleaved.

syntax

(fresh (x ...) goal_0 goal_1 ...)

Introduces a new logic variable bound to each x in the scope of its body, each clause of which should be a goal.

syntax

(run n (x) goal_0 goal_1 ...)

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.)

value

succeed : goal? = (== #t #t)

It is a goal that succeeds.

value

fail : goal? = (== #t #f)

It is a goal that fails; it is unsuccessful.

Minikanren also provides the following helpers:

syntax

(run* (x) goal_0 goal_1 ...)

Equivalent to (run #f (x) goal_0 goal_1 ...).

syntax

(conda [goal_1 goal_1a ...] [goal_2 goal_2a ...] ...)

syntax

(condu [goal_1 goal_1a ...] [goal_2 goal_2a ...] ...)

Variants of conde that correspond to the committed-choice of Mercury and are used in place of Prolog’s cut.

syntax

(project (x ...) goal_1 goal_2 ...)

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.