Skip to content

Instantly share code, notes, and snippets.


alex-hhh/mk.rkt Secret

Last active August 16, 2022 12:16
What would you like to do?
yet another minikanren implementation,
#lang racket/base
;; miniKanren logic programming Domain Specific Language (DSL) for Racket.
;; There are many miniKanren implementations out there, but this one is mine.
;; See for more info about miniKanren.
;; This implementation is based on the Second Edition of "The Reasoned Schemer
;; (TRS), with some small modifications to adapt it to Racket -- these
;; modifications are described in the comments throughout the code.
;; The basic goals
fail succeed ==
;; Goal combiners
once conj disj ifte cond/e cond/a cond/u
;; variables and relations
fresh defrel project ground? ground*?
;; Running miniKanren programs
run run*
;; A small miniKanren library
car/o cdr/o pair/o cons/o null/o list/o member/o proper-member/o append/o
always/o never/o
;; Debugging aids
;; Note that the second edition is a slightly different language than the
;; first edition. If you are familiar with the first edition, this message
;; contains a summary of the differences:
;; Also note that this code uses a different spelling for the key terms. In
;; particular the superscripts of the names in the book are translated as a
;; "/". That is, we use "cond/e" instead of "conde" and "member/o" instead of
;; "membero"
;; You probably need to read the TRS book or one of the miniKanren papers to
;; fully understand the implementation but here are a few key concepts:
;; * a VARIABLE is a unique name within the language. Variables are
;; represented as an instance of a `var` structure containing a name, but
;; the name is ignored. Two variables are the same if they are
;; `eq?`. I.e. we want (eq? (var 'foo) (var 'foo)) to be #f
;; * a TERM represents data: it can be an immediate value, like 1, "hello" or
;; 'foo, a variable, like (var 'foo), or a nested list of these, e.g. (list
;; 1 'foo (var 'bar))
;; * a SUBSTITUTION is a mapping from VARIABLES to TERMS. These are
;; represented as immutable hash tables, which are extended functionally.
;; * a STREAM has the same meaning as streams in Racket, but we build our own
;; here. It is a "generalized list", where the CDR can be a procedure
;; producing other streams. This allows representing infinite streams using
;; finite resources. See `stream-cons` in the Racket documentation if you
;; want to better understand the concept. In miniKanren, all values
;; produced by a stream are substitutions, that is, streams are only used as
;; substitution streams
;; * a GOAL is a function which accepts a SUBSTITUTION and returns a STREAM of
;; substitutions. The basic goals are `fail`, `succeed` and `==` (see their
;; implementation). Other goals, like `conj` and `disj` can be used to
;; combine goals, `defrel` can be used to create new goals and `fresh` and
;; `cond/e` can be used to provide some "flow control"
;; * a miniKanren program can be run using `run` or `run*` which takes a goal
;; and feeds it an empty substitution and extracts the substitutions it
;; produces, which are the result of the program. RUN finds a specified
;; number of solutions, while RUN* finds all the possible solutions. `(run*
;; q goal)` is equivalent to `(run #f q goal)`
;; If you are using racket-mode
;; (, the add the following to
;; your emacs config to properly indent miniKanren programs
;; (defun setup-miniKanren-indentation ()
;; (put 'fresh 'racket-indent-function 1)
;; (put 'project 'racket-indent-function 1)
;; (put 'defrel 'racket-indent-function 1)
;; (put 'run 'racket-indent-function 2)
;; (put 'run* 'racket-indent-function 1))
;; (add-hook 'racket-mode-hook #'setup-miniKanren-indentation)
(module+ test
;; NOTE: rackunit defines `fail`, which we don't use and also we define a
;; goal named `fail`, so don't import that name..
(require (except-in rackunit fail))
(printf "Running the test module in miniKanren~%"))
;;.......................................... Variables and Substitutions ....
;; A logic variable. TRS represents them as vectors, but in Racket we can
;; just use a struct. Note that the NAME is not used, and var instances are
;; compared using EQV?, that is (eqv? (var 'foo) (var 'foo)) is #f and we make
;; use of that fact.
(struct var (name) #:transparent)
(module+ test
;; We rely on the fact that two var instances of the same name are not
;; equal, encode that in a test...
(check-false (eqv? (var 'x) (var 'x)))
;; Make some variables which will be used in the tests below
(define u (var 'u))
(define v (var 'v))
(define w (var 'w))
(define x (var 'x))
(define y (var 'y))
(define z (var 'z)))
;; A substitution maps variables to terms. TRS represents them as lists and
;; uses ASSV? to search them, we represent them as immutable hash tables.
(define the-empty-substitution (hasheq))
;; Sentry value to differentiate a "not found" walked variable, since
;; variables can be associated with #f. This is simply a value that is not
;; `eq?` with anything else.
(define walk-sentry (var 'walk-sentry))
;; Walks the value V in the substitution S. If V is not a variable, it is
;; simply returned, otherwise it is looked up in the substitution. If the
;; result of the lookup is also a variable, it is looked up again in the same
;; substitution, until we either reach a value (i.e. a non-variable) or a
;; variable which is not in the substitution (i.e. it is fresh)
(define (walk v s)
(if (var? v)
(let ([a (hash-ref s v walk-sentry)])
(if (eq? a walk-sentry)
(walk a s)))
(module+ test
(define f13 (hasheq z 'a x w y z))
(check-equal? (walk y f13) 'a)
(check-equal? (walk z f13) 'a)
(check-equal? (walk x f13) w)
(define f16 (hasheq x y v x w x))
(check-equal? (walk y f16) y)
(check-equal? (walk v f16) y)
(check-equal? (walk w f16) y)
(define f80 (hasheq x #f))
(check-equal? (walk x f80) #f)
;; Check if the variable U occurs anywhere in the term V based on the
;; substitution S. OCCURS? is used to prevent adding cycles of variable
;; references to substitutions.
(define (occurs? u v s)
(let ([v (walk v s)])
(cond ((var? v) (eqv? v u))
((pair? v)
(or (occurs? u (car v) s)
(occurs? u (cdr v) s)))
(else #f))))
(module+ test
(check-equal? (occurs? x y (hasheq y 1)) #f)
;; A var cannot reference itself, even through cycles or nested in terms...
(check-equal? (occurs? x x the-empty-substitution) #t)
(check-equal? (occurs? x `(,y) (hasheq y x)) #t)
(check-equal? (occurs? x `(,x) the-empty-substitution) #t))
;; Extent the substitution S with a mapping from U to V, but only if this
;; would not create a cycle (according to OCCURS?)
(define (extend u v s)
(and (not (occurs? u v s))
(hash-set s u v)))
(module+ test
;; Cannot extend if cycles are created.
(check-equal? (extend x `(,y) (hasheq y x)) #f)
(check-equal? (let ([s (hasheq z x y z)])
(let ([s (extend x 'e s)])
(and s (walk y s))))
;; Unify the two terms U and V extending the substitution S with new variable
;; mappings as needed. Returns an updated substitution, or #f if the two
;; values cannot be unified.
(define (unify u v s)
(let ([u (walk u s)]
[v (walk v s)])
(cond ((eqv? u v) s)
((var? u) (extend u v s))
((var? v) (extend v u s))
((and (pair? u) (pair? v))
(let ([s (unify (car u) (car v) s)])
(and s (unify (cdr u) (cdr v) s))))
(else #f))))
(module+ test
(unify `(,x ,y, z) `(,u . ,v) the-empty-substitution)
(hasheq x u v `(,y ,z)))
(unify `(,x ,y ,z) `(,u ,v, w . ()) the-empty-substitution)
(hasheq x u y v z w)))
;;.............................................................. Streams ....
;; Wrapper around (lambda () ...) which is used to create suspensions of
;; streams to better see where these suspensions happen (copied from
(define-syntax suspend
(syntax-rules ()
((_ body) (lambda () body))))
;; Take N values from the stream S -- takes less values if the stream has less
;; than N values. If N is #t it takes all values from the stream S -- this is
;; bad if the stream is infinite
(define (take n s)
(cond ((and n (zero? n)) '())
((null? s) '())
((pair? s)
(cons (car s)
(take (and n (sub1 n)) (cdr s))))
(else (take n (s)))))
(module+ test
;; Lists are streams
(check-equal? (take 0 '(1 2 3)) '())
(check-equal? (take 2 '(1 2 3)) '(1 2))
(check-equal? (take 5 '(1 2 3)) '(1 2 3))
(check-equal? (take #f '(1 2 3)) '(1 2 3))
(define number-stream
(lambda (n)
(cons n (suspend (number-stream (add1 n))))))
(check-equal? (take 0 (number-stream 0)) '())
(check-equal? (take 3 (number-stream 0)) '(0 1 2)))
;; Interleave values from two (possibly infinite) streams. TRS calls this
;; `append-inf` -- NOTE that this is implemented differently than `append-inf`
(define (interleave s-inf t-inf)
((null? s-inf) t-inf)
((pair? s-inf)
(cons (car s-inf) (suspend (interleave t-inf (cdr s-inf)))))
((procedure? s-inf)
;; Force the stream, but only once, this prevents streams that keep
;; producing only procedures to overtake the evaluation.
(let ([forced (s-inf)])
(if (or (null? forced) (pair? forced))
(interleave forced t-inf)
(interleave t-inf forced)))))
(error (format "interleave: unexpected value for s-inf: ~a" s-inf)))))
(module+ test
(check-equal? (take #f (interleave '(a b c) '(1 2 3)))
'(a 1 b 2 c 3))
(check-equal? (take 6
(interleave (number-stream 0)
(number-stream 100)))
'(0 100 1 101 2 102))
(check-equal? (take 8
(interleave '(0 1 2 3) (number-stream 100)))
'(0 100 1 101 2 102 3 103))
(check-equal? (take 10
(interleave (number-stream 100) '(0 1 2 3)))
'(100 0 101 1 102 2 103 3 104 105))
;; This is an infinite stream which does not produce any values, every time
;; it is forced, it just produces another procedure.
(define infinite-stream-of-nothing
(lambda ()
(suspend (infinite-stream-of-nothing))))
;; We should still be able to interleave such streams...
(check-equal? (take 3 (interleave infinite-stream-of-nothing
(number-stream 0)))
'(0 1 2))
(check-equal? (take 3 (interleave (number-stream 0)
'(0 1 2))
;; No infinite recursion on this one...
(check-equal? (take 0 (interleave infinite-stream-of-nothing
;; Apply the goal G to every substitution from S-INF (a possibly infinite
;; stream) and interleave the resulting streams together. TRS calls this
;; `append-map-inf`
(define (map-and-interleave g s-inf)
((null? s-inf) '())
((pair? s-inf)
(interleave (g (car s-inf))
(map-and-interleave g (cdr s-inf))))
(suspend (map-and-interleave g (s-inf))))))
(module+ test
(define number-stream/prefix
(lambda (prefix n)
(cons (list prefix n) (suspend (number-stream/prefix prefix (add1 n))))))
(define letter-stream-stream
(lambda (n)
(number-stream/prefix (integer->char(+ (char->integer #\a) n)) 0)))
(check-equal? (take 20 (map-and-interleave letter-stream-stream (number-stream 0)))
'((#\a 0) (#\b 0) (#\a 1) (#\a 2) (#\c 0) (#\a 3) (#\a 4)
(#\b 1) (#\a 5) (#\a 6) (#\a 7) (#\b 2) (#\a 8) (#\a 9)
(#\d 0) (#\a 10) (#\a 11) (#\b 3) (#\a 12) (#\a 13))))
;;................................................................ Goals ....
;; SUCCEED is a goal that always succeeds, returning a stream of the single
;; substitution that is passed in.
(define succeed
(lambda (s)
(list s)))
;; FAIL is a goal that always fails, returning the empty stream, regardless of
;; what substitutions are passed in.
(define fail
(lambda (_s)
;; == is a goal that attempts to unify the terms U and V using `unify`. If
;; unification succeeds, the goal succeeds with the extended substitution,
;; otherwise this goal fails.
(define (== u v)
(lambda (s)
(let ([s (unify u v s)])
(if s (succeed s) (fail s)))))
;; Disjunction of two goals: the two goals must hold, but not at the same time.
(define (disj/2 g1 g2)
(lambda (s)
(interleave (suspend (g1 s)) (suspend (g2 s)))))
;; Disjunction of any number of goals.
(define-syntax disj
(syntax-rules ()
((disj) fail)
((disj g) g)
((disj g0 g ...) (disj/2 g0 (disj g ...)))))
;; Conjunction of two goals. G1 and G2 must hold together.
(define (conj/2 g1 g2)
(lambda (s)
(map-and-interleave g2 (suspend (g1 s)))))
;; Conjunction of any number of goals.
(define-syntax conj
(syntax-rules ()
((conj) succeed)
((conj g) g)
((conj g0 g ...) (conj/2 g0 (conj g ...)))))
;; Syntax sugar to define new relations, so the user does not need to know
;; about substitutions and streams.
(define-syntax defrel
(syntax-rules ()
((defrel (name x ...) g ...)
(define (name x ...)
(lambda (s)
(suspend ((conj g ...) s)))))))
;; if,then,else for logic programming: If G1 holds, G2 must also hold, with
;; any unifications made by G1, otherwise G3 holds.
(define (ifte g1 g2 g3)
(lambda (s)
(let loop ((s-inf (g1 s)))
(cond ((null? s-inf)
(g3 s))
((pair? s-inf)
(map-and-interleave g2 s-inf))
(suspend (loop (s-inf))))))))
(module+ test
(check-equal? (take #f ((ifte succeed (== #f y) (== #t y)) the-empty-substitution))
(list (hasheq y #f)))
(check-equal? (take #f ((ifte fail (== #f y) (== #t y)) the-empty-substitution))
(list (hasheq y #t)))
(check-equal? (take #f ((ifte (== #t x) (== #f y) (== #t y)) the-empty-substitution))
(list (hasheq x #t y #f)))
(check-equal? (take #f ((ifte (disj (== #t x) (== #f x)) (== #f y) (== #t x))
;; NOTE: two substitutions are produced by this if statement
(hasheq x #t y #f)
(hasheq x #f y #f))))
(define (once g)
(lambda (s)
(let loop ((s-inf (g s)))
(cond ((null? s-inf)
((pair? s-inf)
(cons (car s-inf) '()))
(suspend (loop (s-inf))))))))
(define-syntax fresh
(syntax-rules ()
((fresh () g ...)
(conj g ...))
((fresh (x ...) g ...)
((lambda (x ...)
(conj g ...))
(var 'x) ...))))
;; A "COND" goal -- all branches contribute values
(define-syntax cond/e
(syntax-rules ()
((conde (g ...) ...)
(disj (conj g ...) ...))))
;; Similar to cond/e, but only the first branch that succeeds contributes
;; values.
(define-syntax cond/a
(syntax-rules ()
((cond/a (g0 g ...)) (conj g0 g ...))
((cond/a (g0 g ...) ln ...)
(ifte g0 (conj g ...) (cond/a ln ...)))))
;; Similar to cond/a, but a successful question succeeds once
(define-syntax cond/u
(syntax-rules ()
((cond/u (g0 g ...) ...)
(cond/a ((once g0) g ...) ...))))
;; Run a toplevel goal G and take N substitutions (results) from it using
;; TAKE.
(define (run-goal n g)
(take n (g the-empty-substitution)))
;; Produce a reified symbol (one that is unique) based on the number N. This
;; is used for variables which remained fresh (unbound) after running the
;; goals.
(define (reify-name n)
(string->symbol (string-append "_." (number->string n))))
;; Same as WALK, but V is a term (e.g. a list of other variables) and all the
;; elements of V are walked.
(define (walk* v s)
(let ([v (walk v s)])
(cond ((var? v) v)
((pair? v)
(walk* (car v) s)
(walk* (cdr v) s)))
(else v))))
(define (reify-s v r)
(let ((v (walk v r)))
(cond ((var? v)
(let ([n (hash-count r)])
(let ((rn (reify-name n)))
(hash-set r v rn))))
((pair? v)
(let ([r (reify-s (car v) r)])
(reify-s (cdr v) r)))
(define (reify v)
(lambda (s)
(let ([v (walk* v s)])
(let ([r (reify-s v the-empty-substitution)])
(walk* v r)))))
(module+ test
(check-equal? (reify-s `(,x ,y ,x ,z ,z) the-empty-substitution)
(hasheq x '_.0 y '_.1 z '_.2))
(check-equal? ((reify `(,x ,y ,x ,z ,z)) the-empty-substitution)
'(_.0 _.1 _.0 _.2 _.2)))
;; Run a goal with a toplevel fresh variable (or list of variables) that are
;; available to the goals. substitutions are taken out of the goal using
;; RUN-GOAL and the variable (or list of variables) are reified (their vales
;; resolved and returned.
(define-syntax run
(syntax-rules ()
((run n (x0 x ...) g ...)
(run n q (fresh (x0 x ...)
(== `(,x0 ,x ...) q) g ...)))
((run n q g ...)
(let ([q (var 'q)])
(map (reify q)
(run-goal n (conj g ...)))))))
;; Same as RUN, but fetches all the results from a goal -- this will run
;; forever for goals that produce an infinite number of values.
(define-syntax run*
(syntax-rules ()
((run* q g ...)
(run #f q g ...))))
;; Project is similar to fresh, except that it binds walked variables to the
;; names
(define-syntax project
(syntax-rules ()
((project (x ...) g ...)
(lambda (s)
(let ([x (walk* x s)] ...)
((conj g ...) s))))))
;; Return true if X is a ground value (i.e. not a variable)
(define (ground? x) (not (var? x)))
;; Return true if X is a ground value all the way down, that is, X is not a
;; variable nor a list containing variables.
(define (ground*? x)
(cond ((var? x) #f)
((pair? x) (and (ground*? (car x)) (ground*? (cdr x))))
(else #t)))
;;........................................................ Debgging Aids ....
;; A goal used to print out values of miniKanren variables when running
;; programs. Does not change the substitution, just prints the reified values
;; if the variables passed in. Note that reification happens just for a
;; single show call, so reified values from different show calls are not the
;; same...
;; This is the internal implementation, see show for the actual macro
(define show-impl
(lambda (heading vars vals)
(lambda (s)
(printf "*** ~a~%" heading)
(let loop ([vars vars]
[vals vals]
[reify-substitution the-empty-substitution])
(unless (or (null? vars) (null? vals))
(let* ([v (walk* (car vals) s)]
[r (reify-s v reify-substitution)])
(printf " ~a -> ~a~%" (car vars) (walk* v r))
(loop (cdr vars) (cdr vals) r))))
(list s))))
(define-syntax show
(syntax-rules ()
((show heading)
(show-impl heading '() '()))
((show heading x ...)
(show-impl heading '(x ...) (list x ...)))))
;;........................................... A small miniKanren library ....
(defrel (car/o p a)
(fresh (d)
(== (cons a d) p)))
(defrel (cdr/o p d)
(fresh (a)
(== (cons a d) p)))
(defrel (cons/o a d p)
(== (cons a d) p))
(defrel (null/o p)
(== '() p))
(defrel (pair/o p)
(fresh (a d)
(cons/o a d p)))
;; NOTE: this is the faster version of member/o, with all "fail" relations
;; removed, since they are not needed. Also we use disj/2 instead of cond/e
(defrel (member/o x l)
(car/o l x)
(fresh (d)
(cdr/o l d)
(member/o x d))))
(defrel (list/o l)
((null/o l))
((fresh (d)
(cdr/o l d)
(list/o d)))))
(defrel (proper-member/o x l)
((car/o l x)
(fresh (d)
(cdr/o l d)
(list/o d)))
((fresh (d)
(cdr/o l d)
(proper-member/o x d)))))
(defrel (append/o l t out)
((null/o l) (== t out))
((fresh (a d res)
(cons/o a d l)
(cons/o a res out)
;; NOTE: recursive goal is last, see the "First Commandment"
(append/o d t res)))))
(defrel (always/o)
(defrel (never/o)
(module+ test
;; This hangs if defrel is not defined to suspend relations
(check-equal? (run 1 q (cond/e ((never/o)) (succeed))) '(_.0)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment