mykanren
Racket implementation of minikanren using The Reasoned Schemer Second Edition syntax.
This is the minikanren language as used in The Reasoned Schemer Second Edition. Unlike other implementations in Racket, this implementation includes defrel
, conj2
, disj2
, conj
, and disj
to make following the examples in the book slightly easier.
To use, import mykanren.rkt
with (require "mykanren.rkt")
(see example.rkt
).
Also, feel free to take a look inside mykanren.rkt
, which has been annotated in HtDP
style. Note that I have no idea what I'm doing so if something is painfully wrong then edits are more than welcome.
Provided
run
(run n q g ...)
or (run n (q ...) g ...)
Returns at most n
possible solutions that successfully satisfy goal g and goals in ...
. If less than n
solutions exist, then recurs infinitely (no value).
(run 1 q (== 'olive q)) -> '((olive))
(run 1 q (== 'olive q) (== 'oil q)) -> '()
(run 1 (q v) (== 'olive q) (== 'oil v)) -> '((olive oil))
(run 4237 q (== 'olive q)) -> '((olive))
(run 0 q (== 'olive q)) -> '()
(run 2 (q w) (appendo q w '(1 2 3))) -> '((() (1 2 3))
((1) (2 3)))
run*
(run* q g ...)
or (run* (q ...) g ...)
Returns all possible solutions that successfully satisfy goal g and goals in ...
. If no solutions exist, then recurs infinitely (no value).
Shorthand for (run #f (q) g ...)
.
(run* q (== 'olive q) (== 'oil q)) -> '()
(run* (q) (== 'olive q)) -> '((olive))
(run* (q w) (appendo q w '(1 2 3))) -> '((() (1 2 3))
((1) (2 3))
((1 2) (3))
((1 2 3)
()))
==
(== u v)
Value Value -> Goal
Associates value u
with value v
. Equivalent to (== v u)
.
(run* (q) (== 'olive q)) -> '((olive))
(run* (q) (== q 'olive)) -> '((olive))
(run* (x y z) (== `(,x ,y, z) '(1 2 3))) -> '((1 2 3))
defrel
(defrel (relation-name arg0 ...) ...)
Defines a relation between the arguments. The body of defrel
must be a logical expression: it must evaluate to some Goal
.
(defrel (nullo l)
(== l '()))
(defrel (conso f r out)
(== (cons f r) out))
(defrel (caro l out)
(fresh (r)
(conso out r l)))
(defrel (cdro l out)
(fresh (f)
(conso f out l)))
disj2
(disj2 g1 g2)
Goal Goal -> Goal
Produces the combined goal of acheiving g1
or g2
.
(run* (q) (disj2 (== 'olive q) (== 'oil q))) -> '((olive) (oil))
conj2
(disj2 g1 g2)
Goal Goal -> Goal
Produces the combined goal of acheiving g1
and g2
.
(run* (q) (conj2 (== 'olive q) (== 'oil q))) -> '()
(run* (q w) (conj2 (== q '()) (appendo q w '(1 2 3)))) -> '((() (1 2 3)))
disj
(disj2 g ...)
(...Goal) -> Goal
Like disj2
but for an arbitrary number of arguments.
(run* (q) (disj (== 'olive q))) -> '((olive))
(run* (q) (disj (== 'extra q)
(== 'virgin q)
(== 'olive q)
(== 'oil q))) -> '((extra)
(virgin)
(olive)
(oil))
conj
(disj2 g1 g2)
Goal Goal -> Goal
Like conj
but for an arbitrary number of arguments. Not paticularly useful, as this is the default behavior for Goal
s in the body of run
.
(run* (q) (conj (== 'olive q))) -> '((olive))
fresh
(fresh (var-name ...) ...)
Creates a fresh variable(s) var-name
, which can be used within the body of fresh
.
(defrel (caro l out)
(fresh (r)
(conso out r l)))
(defrel (cdro l out)
(fresh (f)
(conso f out l)))
conde
(conde [g1 ...] [g2 ...] ...)
Defines a series of goals, where each "branch" of the conde
is in a disj
(Branch A OR Branch B OR Branch C etc.), and each series of goal within a branch is in a conj
(Goal A OR Goal B OR Goal C etc.). Syntactically and behaviorlly similar to cond
.
(defrel (appendo l t out)
(conde
[(nullo l)(== t out)]
[(fresh (a d res)
(conso a d l)
(conso a res out)
(appendo d t res))]))
conda
(conda [g1 ...] [g2 ...] ...)
Syntactically identical to conde
, but only the first line that succeeds may contribute values. "a" stands for "a single line", since at most only a single line can contribute values.
(run* x
(conda
[(== 'olive x)]
[(== 'oil x)])) -> '((olive))
(run* (q w x)
(conda
[(appendo q w '(1 2 3))]
[(== 'oil x)])) -> '((() (1 2 3) _0)
((1) (2 3) _0)
((1 2) (3) _0)
((1 2 3) () _0))
condu
(condu [g1 ...] [g2 ...] ...)
Syntactically identical to conde
, but a successful question succeeds only once. "u" stands for "U will never use this", as it only appears for 3 pages then vanishes.
Just kidding, it actually corresponds to Mercury's commited choice.
(run* (q w x)
(condu
[(appendo q w '(1 2 3))]
[(== 'oil x)])) -> '((() (1 2 3) _0))
success
Shorthand for (== #t #t)
, represents a goal that is always successful.
(run* q succeed) -> '(_0)
fail
Shorthand for (== #f #t)
, represents a goal that always fails.
(run* q fail) -> '()