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*
• ==
• defrel
• disj2
• conj2
• disj
• conj
• fresh
• conde
• conda
• condu
• success
• fail

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 Goals 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) -> '()