The Reasoned Schemer

miniKanren, microKanren and some implementations

 Posted on March 9, 2018  (Last modified on July 10, 2026)  |   19 min  |   Daniel P. Friedman William E. Byrd Oleg Kiselyov Jason Hemann

References

The Reasoned Schemer little book

Friedman, Daniel P. and Byrd, William E. and Kiselyov, Oleg and Hemann, Jason, 2018. The Reasoned Schemer. 2nd edition, The MIT Press,

Abstract: A new edition of a book, written in a humorous question-and-answer style, that shows how to implement and use an elegant little programming language for logic programming. The goal of this book is to show the beauty and elegance of relational programming, which captures the essence of logic programming. The book shows how to implement a relational programming language in Scheme, or in any other functional language, and demonstrates the remarkable flexibility of the resulting relational programs. As in the first edition, the pedagogical method is a series of questions and answers, which proceed with the characteristic humor that marked The Little Schemer and The Seasoned Schemer. Familiarity with a functional language or with the first five chapters of The Little Schemer is assumed. For this second edition, the authors have greatly simplified the programming language used in the book, as well as the implementation of the language. In addition to revising the text extensively, and simplifying and revising the Laws and Commandments, they have added explicit Translation rules to ease translation of Scheme functions into relations.

The µkanren paper

Jason Hemann and Friedman, Daniel P., 2013. microkanren: A Minimal Functional Core for Relational Programming.

Abstract: This paper presents µKanren, a minimalist language in the miniKanren family of relational (logic) programming languages. Its implementation comprises fewer than 40 lines of Scheme. We motivate the need for a minimalist miniKanren language, and iteratively develop a complete search strategy. Finally, we demonstrate that through suf cient user-level features one regains much of the expressiveness of other miniKanren languages. In our opinion its brevity and simple semantics make µKanren uniquely elegant.

The Relational programming in minikanren Byrd’s thesis

William E. Byrd, 2009. Relational programming in minikanren: techniques, applications, and implementations.

Abstract: The promise of logic programming is that programs can be written relationally , without distinguishing between input and output arguments. Relational programs are remarkably flexible—for example, a relational type-inferencer also performs type checking and type inhabitation, while a relational theorem prover generates theorems as well as proofs and can even be used as a simple proof assistant. Unfortunately, writing relational programs is difficult, and requires many interesting and unusual tools and techniques. For example, a relational interpreter for a subset of Scheme might use nominal unification to support variable binding and scope, Constraint Logic Programming over Finite Domains (CLP(FD)) to implement relational arithmetic, and tabling to improve termination behavior. In this dissertation I present miniKanren , a family of languages specifically designed for relational programming, and which supports a variety of relational idioms and techniques. I show how miniKanren can be used to write interesting relational programs, including an extremely flexible lean tableau theorem prover and a novel constraint-free binary arithmetic system with strong termination guarantees. I also present interesting and practical techniques used to implement miniKanren, including a nominal unifier that uses triangular rather than idempotent substitutions and a novel “walk”-based algorithm for variable lookup in triangular substitutions. The result of this research is a family of languages that supports a variety of relational idioms and techniques, making it feasible and useful to write interesting programs as relations.

The Efficient representations for triangular substitutions paper

Bender, David and Kuper, Lindsey and Byrd, William and Friedman, Daniel, 2015. Efficient representations for triangular substitutions: A comparison in miniKanren.

Abstract: Unification, a fundamental process for logic programming systems, relies on the ability to efficiently look up values of variables in a substitution. Triangular substitutions, which allow associations to variables that are themselves bound by another association, are an attractive choice for purely functional implementations of logic programming systems because of their fast extension time and linear space requirement, but have the disadvantage of costly lookup. We present several representations for triangular substitutions that decrease the cost of lookup to linear or logarithmic time in the size of the substitution while maintaining most of their desirable properties. In particular, we show that triangular substitutions can be represented efficiently using skew binary random-access lists, and that this representation provides a significant decrease in running time for existing programs written in miniKanren, a declarative logic programming system implemented in a pure functional subset of Scheme.

test/find: pass

(define (test/find _)
  (let* ((v1 (make-μkanren-var 0))
         (v2 (make-μkanren-var 1))
         (s0 μkanren-state-empty)
         (s1 (make-μkanren-state
               1
               (cons/sbral 'a (μkanren-state-S s0))
               empty/sbral
               empty/sbral
               empty/sbral
               '()))
         (s2 (make-μkanren-state
               2
               (cons/sbral v1 (μkanren-state-S s1))
               empty/sbral
               empty/sbral
               empty/sbral
               '())))
    (⊦= 5 (μkanren-state-find 5 s2))
    (⊦= 'a (μkanren-state-find v1 s2))
    (⊦= 'a (μkanren-state-find v2 s2))))

((eta 0.0) (memory #(12582912 3102104 1048576)) (stdout "") (stderr ""))

test/find/values: pass

(define (test/find/values _)
  (let* ((v1 (make-μkanren-var 0))
         (v2 (make-μkanren-var 1))
         (s0 μkanren-state-empty)
         (s1 (make-μkanren-state
               1
               (cons/sbral 'a (μkanren-state-S s0))
               empty/sbral
               empty/sbral
               empty/sbral
               '()))
         (s2 (make-μkanren-state
               2
               (cons/sbral v1 (μkanren-state-S s1))
               empty/sbral
               empty/sbral
               empty/sbral
               '())))
    (⊦= 1 (μkanren-var-index/sbral (μkanren-state-S s2) v1))
    (⊦= 0 (μkanren-var-index/sbral (μkanren-state-S s2) v2))
    (⊦= 'a (μkanren-sbral-ref/var (μkanren-state-S s2) v1))
    (⊦= v1 (μkanren-sbral-ref/var (μkanren-state-S s2) v2))
    (⊦= '(a a 5) (μkanren-state-find/values (list v1 v2 5) s2))))

((eta 0.0) (memory #(12582912 3103256 1048576)) (stdout "") (stderr ""))

test/state-with: pass

(define (test/state-with _)
  (let* ((s (make-μkanren-state 3 empty/sbral '((d)) '((a)) '((t)) '(tag)))
         (s* (μkanren-state-with s #:D '() #:tags '())))
    (⊦= 3 (μkanren-state-vars-count s*))
    (⊦= '() (μkanren-state-D s*))
    (⊦= '((a)) (μkanren-state-A s*))
    (⊦= '((t)) (μkanren-state-T s*))
    (⊦= '() (μkanren-state-tags s*))
    (⊦= '((d)) (μkanren-state-D (μkanren-state-with s)))))

((eta 0.0) (memory #(12582912 3104880 1048576)) (stdout "") (stderr ""))

test/state-unify/stores: pass

(define (test/state-unify/stores _)
  (define ((raw=° u v) s)
    (let1 (r (μkanren-state-unify u v s '())) (if r (list (car r)) '())))
  (define ((rawS=° u v) s)
    (let1 (r (μkanren-state-unify u v s '()))
          (if r
            (list (μkanren-state-with s #:S (μkanren-state-S (car r))))
            '())))
  (⊦= '()
      (°->list
        #f
        (fresh°
          (q)
          (fresh° (x y) (=° q (list x y)) (number° x) (raw=° x 'a) (=° y 1)))))
  (⊦= '()
      (°->list
        #f
        (fresh°
          (q)
          (fresh°
            (x y)
            (=° q (list x y))
            (absent° 'a x)
            (raw=° x 'a)
            (=° y 1)))))
  (⊦= '()
      (°->list
        #f
        (fresh°
          (q)
          (fresh°
            (x y)
            (=° q (list x y))
            (number° x)
            (rawS=° x 'a)
            (=° y 1)))))
  (⊦= '()
      (°->list
        #f
        (fresh°
          (q)
          (fresh°
            (x y)
            (=° q (list x y))
            (absent° 'a x)
            (rawS=° x 'a)
            (=° y 1))))))

((eta 0.0) (memory #(12582912 3095192 1048576)) (stdout "") (stderr ""))

test/rem-subsumed/by: pass

(define (test/rem-subsumed/by _)
  (⊦= '(2 3 1) ((μkanren-rem-subsumed/by member?) '(1 2 1 3 2)))
  (⊦= '() ((μkanren-rem-subsumed/by member?) '()))
  (⊦= '(2 3 1) ((μkanren-rem-subsumed/by member? identity list) '(1 2 1 3 2)))
  (⊦= '(6) ((μkanren-rem-subsumed/by (λ (x L) (pair? L))) '(1 2 3 4 6)))
  (⊦= '(6 3)
      ((μkanren-rem-subsumed/by
         (λ (x L) (pair? L))
         (μ x (modulo x 2))
         (μ x (list (modulo x 2))))
       '(1 2 3 4 6))))

((eta 0.0) (memory #(12582912 3095904 1048576)) (stdout "") (stderr ""))

test/foldr/verify: pass

(define (test/foldr/verify _)
  (define (step x acc) (and (odd? x) (cons x acc)))
  (⊦= '(1 3 5) (μkanren-foldr/verify step '(1 3 5)))
  (⊦= #f (μkanren-foldr/verify step '(1 2 5)))
  (⊦= '() (μkanren-foldr/verify step '()))
  (⊦= '() ((μkanren-verify-T+ 'x μkanren-tag/sym μkanren-state-empty) '()))
  (⊦= #f ((μkanren-verify-T+ 5 μkanren-tag/sym μkanren-state-empty) '())))

((eta 0.0) (memory #(12582912 3096912 1048576)) (stdout "") (stderr ""))

test/partition*: pass

(define (test/partition* _)
  (let1 (A (list (cons 'a μkanren-tag/sym)
                 (cons 'b μkanren-tag/num)
                 (cons 'a μkanren-tag/sym)
                 (cons 'c μkanren-tag/sym)))
        (⊦= `((,μkanren-tag/sym a c) (,μkanren-tag/num b))
            (μkanren-partition* A)))
  (⊦= '((λ (α β γ)
           (assert (every (μ v (symbol? v)) (list α γ)))
           (assert (every (μ v (number? v)) (list β)))
           (cons α (cons β (cons γ '())))))
      (°->list
        #f
        (fresh°
          (q a b c)
          (=° q (list a b c))
          (symbol° a)
          (number° b)
          (symbol° c)))))

((eta 0.0) (memory #(12582912 3098240 1048576)) (stdout "") (stderr ""))

test/=°: pass

(define (test/=° _) (⊦= '(α) (°->list/ground (=° 'z 'z))))

((eta 0.001) (memory #(12582912 3098536 1048576)) (stdout "") (stderr ""))

test/sharing: pass

(define (test/sharing _)
  (⊦= '(((α z) z (α β)))
      (°->list/ground
        (fresh°
          r
          ←
          (n q x)
          (=° q 'z)
          (fresh° (w r) (=° n (list w q)) (=° x (list w r)))))))

((eta 0.0) (memory #(12582912 3102656 1048576)) (stdout "") (stderr ""))

test/fresh°/typo: pass

(define (test/fresh°/typo _)
  (⊦= 'syntax-error
      (condition-case
        (eval '(μkanren-run (q 3 #f) (fresh° x (null° x) (=° q x))))
        ((exn syntax) 'syntax-error)))
  (⊦= '(()) (μkanren-run (q 3 #t) (fresh° (x) (null° x) (=° q x)))))

((eta 0.0) (memory #(12582912 3105376 1048576)) (stdout "") (stderr ""))

test/define-relation/recursive: pass

(define (test/define-relation/recursive _)
  (define-relation (ones° x) (or° (=° x 1) (ones° x)))
  (⊦= '(1 1 1) (°->list/ground (take° 3 (fresh° (q) (ones° q))))))

((eta 0.0) (memory #(12582912 3102744 1048576)) (stdout "") (stderr ""))

test/peano°: pass

(define (test/peano° _)
  (define-relation
    (peano° n)
    (or° (=° n 'z) (fresh° (r) (=° n `(s ,r)) (peano° r))))
  (define-relation
    (church° n)
    (fresh° (b) (=° n `(λ (s) (λ (z) ,b))) (peano° b)))
  (⊦= '(z (s z)
          (s (s z))
          (s (s (s z)))
          (s (s (s (s z))))
          (s (s (s (s (s z)))))
          (s (s (s (s (s (s z))))))
          (s (s (s (s (s (s (s z)))))))
          (s (s (s (s (s (s (s (s z))))))))
          (s (s (s (s (s (s (s (s (s z))))))))))
      (°->list/ground (take° 10 (fresh° (n) (peano° n)))))
  (⊦= '((λ (s) (λ (z) z))
        (λ (s) (λ (z) (s z)))
        (λ (s) (λ (z) (s (s z))))
        (λ (s) (λ (z) (s (s (s z)))))
        (λ (s) (λ (z) (s (s (s (s z))))))
        (λ (s) (λ (z) (s (s (s (s (s z)))))))
        (λ (s) (λ (z) (s (s (s (s (s (s z))))))))
        (λ (s) (λ (z) (s (s (s (s (s (s (s z)))))))))
        (λ (s) (λ (z) (s (s (s (s (s (s (s (s z))))))))))
        (λ (s) (λ (z) (s (s (s (s (s (s (s (s (s z))))))))))))
      (°->list/ground (take° 10 (fresh° (n) (church° n))))))

((eta 0.011) (memory #(12582912 3116984 1048576)) (stdout "") (stderr ""))

test/append°: pass

(define (test/append° _)
  (define-relation
    (append° r s rs)
    (cond° ((null° r) (=° s rs))
           ((fresh° (a d c) (cons° a d r) (append° d s c) (cons° a c rs)))))
  (⊦ equal?
     '((λ (α) α)
       (λ (α β) (cons α β))
       (λ (α β γ) (cons α (cons β γ)))
       (λ (α β γ δ) (cons α (cons β (cons γ δ))))
       (λ (α β γ δ ε) (cons α (cons β (cons γ (cons δ ε)))))
       (λ (α β γ δ ε ζ) (cons α (cons β (cons γ (cons δ (cons ε ζ))))))
       (λ (α β γ δ ε ζ η)
          (cons α (cons β (cons γ (cons δ (cons ε (cons ζ η)))))))
       (λ (α β γ δ ε ζ η θ)
          (cons α (cons β (cons γ (cons δ (cons ε (cons ζ (cons η θ))))))))
       (λ (α β γ δ ε ζ η θ ι)
          (cons α
                (cons β
                      (cons γ
                            (cons δ (cons ε (cons ζ (cons η (cons θ ι)))))))))
       (λ (α β γ δ ε ζ η θ ι κ)
          (cons α
                (cons β
                      (cons γ
                            (cons δ
                                  (cons ε (cons ζ (cons η (cons θ (cons ι κ)))))))))))
     (μkanren-run (l 10 #f) (fresh° (a d) (append° a d l)))))

((eta 0.001) (memory #(12582912 3117912 1048576)) (stdout "") (stderr ""))

test/=°/nan: pass

(define (test/=°/nan _)
  (⊦= 1 (length (μkanren-run (q 2 #f) (=° q (/ 0.0 0.0)) (=° q (/ 0.0 0.0)))))
  (⊦= 1
      (length
        (μkanren-run
          (q 2 #f)
          (=° q (list 1 (/ 0.0 0.0)))
          (=° q (list 1 (/ 0.0 0.0))))))
  (⊦= '() (μkanren-run (q 2 #f) (=° q (/ 0.0 0.0)) (≠° q (/ 0.0 0.0))))
  (⊦= '() (μkanren-run (q 2 #f) (=° q (/ 0.0 0.0)) (=° q 1.0)))
  (⊦= '() (μkanren-run (q 2 #f) (absent° (/ 0.0 0.0) q) (=° q (/ 0.0 0.0))))
  (⊦= '() (μkanren-run (q 2 #f) (=° q (/ 0.0 0.0)) (absent° (/ 0.0 0.0) q)))
  (⊦= '()
      (μkanren-run
        (q 2 #f)
        (absent° (/ 0.0 0.0) q)
        (=° q (list 1 (/ 0.0 0.0)))))
  (⊦= '()
      (μkanren-run
        (q 2 #f)
        (absent° (list (/ 0.0 0.0)) q)
        (=° q (list (/ 0.0 0.0)))))
  (⊦= 1
      (length
        (μkanren-run (q 2 #f) (absent° (/ 0.0 0.0) q) (=° q (list 1.0 2)))))
  (let1 (c (λ (s) (string->number s)))
        (⊦= 1
            (length
              (μkanren-run
                (q 2 #f)
                (=° q (c "+nan.0+1i"))
                (=° q (c "+nan.0+1i")))))
        (⊦= '()
            (μkanren-run
              (q 2 #f)
              (=° q (c "+nan.0+1i"))
              (=° q (c "+nan.0+2i"))))
        (⊦= '()
            (μkanren-run
              (q 2 #f)
              (=° q (c "+nan.0+1i"))
              (=° q (c "1+nan.0i"))))
        (⊦= '()
            (μkanren-run (q 2 #f) (=° q (c "+nan.0+1i")) (=° q (/ 0.0 0.0))))
        (⊦= '()
            (μkanren-run
              (q 2 #f)
              (=° q (c "+nan.0+1i"))
              (≠° q (c "+nan.0+1i"))))
        (⊦= 1
            (length
              (μkanren-run
                (q 2 #f)
                (=° q (c "+nan.0+1i"))
                (≠° q (c "7+nan.0i")))))))

((eta 0.0) (memory #(12582912 3105792 1048576)) (stdout "") (stderr ""))

test/≠°/verify: pass

(define (test/≠°/verify _)
  (⊦= '() (°->list #f (fresh° (q x y) (≠° x y) (=° q 1) (=° x 5) (=° y 5))))
  (⊦= '()
      (°->list
        #f
        (fresh° (q x y) (≠° (list x y) '(1 2)) (=° q 0) (=° x 1) (=° y 2))))
  (⊦= '()
      (°->list
        #f
        (fresh° (q x y z) (≠° x (list y)) (=° q 0) (=° y z) (=° x (list z)))))
  (⊦= '((λ (α) α))
      (°->list #f (fresh° (q x b) (=° q b) (≠° b (list x)) (=° x b))))
  (⊦= '((λ (α) (begin (deny (equal? α (cons 1 '())))) (cons α (cons 1 '()))))
      (°->list
        #f
        (fresh° (q b x) (=° q (list b x)) (≠° b (list x)) (=° x 1)))))

((eta 0.0) (memory #(12582912 3107144 1048576)) (stdout "") (stderr ""))

test/=°/structure: pass

(define (test/=°/structure _)
  (define-record person name age)
  (define p (make-person 'alice 30))
  (⊦= #t (record-instance? p))
  (⊦= `((record ,p)) (°->list/ground (fresh° (r) (=° r (list 'record p)))))
  (⊦= `((record ,(make-person 'α 30)))
      (°->list/ground
        (fresh° (r a) (=° r (list 'record (make-person a 30)))))))

((eta 0.001) (memory #(12582912 3109992 1048576)) (stdout "") (stderr ""))

test/=°/structure/vector: pass

(define (test/=°/structure/vector _)
  (define-record person name age)
  (define p (make-person 'alice 30))
  (⊦= #t (record-instance? p))
  (⊦= #(person alice 30) (record->vector p))
  (⊦= '((person alice 30))
      (°->list/ground (fresh° r ← (t n a) (=° `#(,t ,n ,a) p)))))

((eta 0.0) (memory #(12582912 3110304 1048576)) (stdout "") (stderr ""))

test/=°/structure/vector/answer: pass

(define (test/=°/structure/vector/answer _)
  (⊦= '((λ () (vector 1 2))) (°->list #f (fresh° (q) (=° q (vector 1 2)))))
  (⊦= '((λ (α) (vector 1 α))) (°->list #f (fresh° (q r) (=° q (vector 1 r))))))

((eta 0.0) (memory #(12582912 3111224 1048576)) (stdout "") (stderr ""))

test/var->symbol/overflow: pass

(define (test/var->symbol/overflow _)
  (⊦= '((α β γ δ ε ζ η θ ι κ λ μ ν ξ ο π ρ σ τ υ φ χ ψ ω α1 β1))
      (°->list/ground
        (fresh° r ← (a b c d e f g h i j k l m n o p q s t u v w x y z aa)))))

((eta 0.0) (memory #(12582912 3129480 1048576)) (stdout "") (stderr ""))

test/ground/constrained: pass

(define (test/ground/constrained _)
  (⊦= '(α) (°->list/ground (fresh° (q) (number° q))))
  (⊦= '(α) (°->list/ground (fresh° (q) (≠° q 'α))))
  (⊦= '(α) (°->list/ground (fresh° (q) (symbol° q)))))

((eta 0.0) (memory #(12582912 3112728 1048576)) (stdout "") (stderr ""))

test/absent°/symbol°: pass

(define (test/absent°/symbol° _)
  (⊦= '()
      (°->list
        #f
        (fresh° (q) (symbol° q) (absent° 'closure q) (=° q 'closure))))
  (⊦= '()
      (°->list
        #f
        (fresh° (q) (absent° 'closure q) (symbol° q) (=° q 'closure))))
  (⊦= '((λ (α)
           (begin (deny (equal? α 'closure)))
           (assert (every (μ v (symbol? v)) (list α)))
           α))
      (°->list #f (fresh° (q) (symbol° q) (absent° 'closure q))))
  (⊦= '((λ (α β γ)
           (begin (deny (equal? β 'a)))
           (assert (every (μ v (symbol? v)) (list α β γ)))
           (cons α (cons β (cons γ '())))))
      (°->list
        #f
        (fresh°
          (q x y z)
          (=° q (list x y z))
          (symbol° x)
          (symbol° y)
          (symbol° z)
          (absent° 'a y)))))

((eta 0.001) (memory #(12582912 3115688 1048576)) (stdout "") (stderr ""))

test/≠°/subsumed: pass

(define (test/≠°/subsumed _)
  (⊦= '((λ (α β)
           (assert (every (μ v (symbol? v)) (list α β)))
           (cons α (cons β '()))))
      (°->list
        #f
        (fresh°
          (q x y)
          (=° q (list x y))
          (symbol° x)
          (symbol° y)
          (≠° (list x y) (list 1 2)))))
  (⊦= '((λ (α β)
           (assert (every (μ v (symbol? v)) (list α β)))
           (cons α (cons β '()))))
      (°->list
        #f
        (fresh°
          (q x y)
          (=° q (list x y))
          (symbol° x)
          (symbol° y)
          (≠° (list x y) (list 'a 2))))))

((eta 0.0) (memory #(12582912 3117168 1048576)) (stdout "") (stderr ""))

test/≠°/subsumed/keyed: pass

(define (test/≠°/subsumed/keyed _)
  (⊦= '((λ (α β γ) (begin (deny (equal? α β))) (cons α (cons β (cons γ '())))))
      (°->list
        #f
        (fresh°
          (q x y z)
          (=° q (list x y z))
          (≠° x y)
          (≠° (list x z) (list y 1)))))
  (⊦= '((λ (α β γ) (begin (deny (equal? α β))) (cons α (cons β (cons γ '())))))
      (°->list
        #f
        (fresh°
          (q x y z)
          (=° q (list x y z))
          (≠° (list z x) (list 1 y))
          (≠° y x))))
  (⊦= '((λ (α β) (begin (deny (equal? β 2))) (cons α (cons β '()))))
      (°->list
        #f
        (fresh°
          (q x y)
          (=° q (list x y))
          (≠° (list x y) (list 1 2))
          (≠° y 2))))
  (⊦= '((λ (α β γ δ)
           (begin (deny (equal? α δ)))
           (begin (deny (equal? β δ)))
           (cons α (cons β (cons γ (cons δ '()))))))
      (°->list
        #f
        (fresh°
          (q a b c x)
          (=° q (list a b c x))
          (≠° x a)
          (≠° x b)
          (≠° (list x c) (list b 1)))))
  (⊦= '((λ (α β γ δ)
           (begin (deny (equal? α δ)))
           (begin (deny (equal? β δ)))
           (begin (deny (equal? γ δ)))
           (cons α (cons β (cons γ (cons δ '()))))))
      (°->list
        #f
        (fresh°
          (q a b c)
          (fresh°
            (x)
            (=° q (list a b c x))
            (≠° x a)
            (≠° (list c x) (list 1 b))
            (≠° x b)
            (≠° x c))))))

((eta 0.0) (memory #(12582912 3120776 1048576)) (stdout "") (stderr ""))

test/stores/order: pass

(define (test/stores/order _)
  (⊦= (°->list #f (fresh° (q) (absent° 'a q) (absent° '(b) q) (absent° 'c q)))
      (°->list #f (fresh° (q) (absent° 'c q) (absent° '(b) q) (absent° 'a q))))
  (⊦= (°->list
        #f
        (fresh°
          (q)
          (≠° q (make-record-instance 'box 1))
          (≠° q (make-record-instance 'box 2))))
      (°->list
        #f
        (fresh°
          (q)
          (≠° q (make-record-instance 'box 2))
          (≠° q (make-record-instance 'box 1)))))
  (⊦= (°->list
        #f
        (fresh°
          (q x y)
          (=° q (list x y))
          (≠° (list x y) '(1 2))
          (≠° (list y x) '(3 4))))
      (°->list
        #f
        (fresh°
          (q x y)
          (=° q (list x y))
          (≠° (list y x) '(3 4))
          (≠° (list x y) '(1 2))))))

((eta 0.0) (memory #(12582912 3122960 1048576)) (stdout "") (stderr ""))

test/=°/hands-on: pass

(define (test/=°/hands-on _)
  (⊦= '() (°->list #f (fresh° (q x y) (symbol° x) (=° x y) (=° y 5))))
  (⊦= '() (°->list #f (fresh° (q x y) (symbol° x) (number° y) (=° x y))))
  (⊦= '() (°->list #f (fresh° (q x y) (≠° x 1) (=° x y) (=° y 1))))
  (⊦= '()
      (°->list #f (fresh° (q x y) (absent° 'z x) (=° x (list y)) (=° y 'z))))
  (⊦= '()
      (°->list
        #f
        (fresh°
          (q x y z)
          (absent° '(1 2) (cons x y))
          (=° y (list z))
          (=° x 1)
          (=° z 2))))
  (⊦= '((λ (α)
           (begin (deny (equal? α 'a)))
           (assert (every (μ v (symbol? v)) (list α)))
           α))
      (°->list
        #f
        (fresh° (q) (fresh° (x) (absent° 'a x) (symbol° q) (=° x q)))))
  (⊦= '((λ (α)
           (begin (deny (equal? α 'a)))
           (assert (every (μ v (symbol? v)) (list α)))
           α))
      (°->list
        #f
        (fresh° (q) (fresh° (x) (absent° 'a q) (symbol° x) (=° x q))))))

((eta 0.0) (memory #(12582912 3120440 1048576)) (stdout "") (stderr ""))

test/absent°/structure: pass

(define (test/absent°/structure _)
  (⊦= '() (°->list #f (fresh° (q) (absent° 'a q) (=° q (vector 'a)))))
  (⊦= '()
      (°->list #f (fresh° (q x) (=° q (vector x)) (absent° 'a q) (=° x 'a))))
  (⊦= '((λ () (vector 'b)))
      (°->list #f (fresh° (q) (=° q (vector 'b)) (absent° 'a q))))
  (⊦= '()
      (°->list
        #f
        (fresh° (q) (=° q (make-record-instance 'box 'a)) (absent° 'a q)))))

((eta 0.0) (memory #(12582912 3121816 1048576)) (stdout "") (stderr ""))

test/absent°/subsumed: pass

(define (test/absent°/subsumed _)
  (⊦= (°->list #f (fresh° (q) (absent° 'a q) (absent° 'b q)))
      (°->list #f (fresh° (q) (absent° 'a q) (absent° 'b q) (≠° q 'a))))
  (⊦= (°->list #f (fresh° (q) (absent° 'a q) (absent° 'b q)))
      (°->list #f (fresh° (q) (absent° 'a q) (absent° 'b q) (≠° q 'b)))))

((eta 0.0) (memory #(12582912 3121224 1048576)) (stdout "") (stderr ""))

test/absent°/datum: pass

(define (test/absent°/datum _)
  (⊦= '((λ () (cons 1 (cons 2 '()))))
      (°->list #f (fresh° (q) (=° q '(1 2)) (absent° 5 q))))
  (⊦= '() (°->list #f (fresh° (q) (=° q '(1 2)) (absent° 2 q))))
  (⊦= '() (°->list #f (fresh° (q) (absent° 5 q) (=° q '(1 5))))))

((eta 0.0) (memory #(12582912 3122544 1048576)) (stdout "") (stderr ""))

test/absent°/compound: pass

(define (test/absent°/compound _)
  (⊦= '() (°->list #f (fresh° (q) (absent° '(1 2) q) (=° q '(1 2)))))
  (⊦= '() (°->list #f (fresh° (q) (=° q '(1 2)) (absent° '(1 2) q))))
  (⊦= '() (°->list #f (fresh° (q) (=° q '(0 (1 2) 3)) (absent° '(1 2) q))))
  (⊦= '() (°->list #f (fresh° (q) (=° q '(0 1 2)) (absent° '(1 2) q))))
  (⊦= '((λ () (cons 0 (cons 1 (cons 2 (cons 3 '()))))))
      (°->list #f (fresh° (q) (=° q '(0 1 2 3)) (absent° '(1 2) q))))
  (⊦= '()
      (°->list
        #f
        (fresh° (q) (=° q (list (vector 1 2))) (absent° (vector 1 2) q))))
  (⊦= '((λ () (vector 0 1 2)))
      (°->list #f (fresh° (q) (=° q (vector 0 1 2)) (absent° '(1 2) q))))
  (⊦= '((λ () (vector 1)))
      (°->list #f (fresh° (q) (=° q (vector 1)) (absent° '() q))))
  (⊦= '()
      (°->list
        #f
        (fresh° (q x) (=° q (cons 1 x)) (absent° '(1 2) q) (=° x '(2)))))
  (⊦= '()
      (°->list
        #f
        (fresh° (q x) (absent° '(1 2) q) (=° q (cons 1 x)) (=° x '(2)))))
  (⊦= '()
      (°->list
        #f
        (fresh° (q x) (absent° '(1 2) q) (=° q (list 0 x)) (=° x '(1 2)))))
  (⊦= '((λ () (cons 1 (cons 3 '()))))
      (°->list
        #f
        (fresh° (q x) (=° q (cons 1 x)) (absent° '(1 2) q) (=° x '(3)))))
  (⊦= '((λ (α) (assert (absent? '(1 2) (cons 1 α))) (cons 1 α)))
      (°->list #f (fresh° (q x) (=° q (cons 1 x)) (absent° '(1 2) q))))
  (⊦= '((λ (α) (assert (absent? '(1 2) α)) α))
      (°->list #f (fresh° (q) (fresh° (z) (absent° '(1 2) (cons q z))))))
  (⊦= '((λ (α) (assert (absent? '(1 2) α)) α))
      (°->list #f (fresh° (q) (fresh° (z) (absent° '(1 2) (list q z))))))
  (⊦= '((λ (α) (assert (absent? '(()) α)) α))
      (°->list #f (fresh° (q) (fresh° (z) (absent° '(()) (cons q z))))))
  (⊦= '((λ (α) (assert (absent? '(1 2) (cons 1 α))) α))
      (°->list
        #f
        (fresh° (q) (fresh° (z) (absent° '(1 2) (list (cons 1 q) z))))))
  (⊦= '((λ (α) (assert (absent? '(1 2) α)) α))
      (°->list #f (fresh° (q) (fresh° (z) (absent° '(1 2) (vector z q))))))
  (⊦= '((λ (α) α))
      (°->list #f (fresh° (q) (fresh° (z) (absent° '(1 2) (cons z z))))))
  (⊦= '()
      (°->list
        #f
        (fresh° (q) (fresh° (z) (absent° '(1 2) (cons q z)) (=° q '(1 2)))))))

((eta 0.001) (memory #(12582912 3123992 1048576)) (stdout "") (stderr ""))
Categories: scheme  logic programming 
Tags: sbral 

See also

The SBRAL data structure Skew Binary Random-Access Lists The (aux kanren) modules Arithmetic, dates, presentation of answers and a union-find miniKanren The (aux hansei) modules Inference, random sources, lazy lists, logic programming and example models Aggregation predicates for µkanren Groups, window functions, sets and enumerations miniKanren, live and untagged Quine generation via relational interpreters Pure, declarative, and constructive arithmetic relations A declarative pearl The (aux anthropic) module The Anthropic Messages API, offline The (aux cml) module Events, threads, synchronous variables, the library and I/O The (aux hakaru10) modules Random sources, distributions, the language, exact inference and examples The (aux games dice-of-doom) module Dice of Doom The (aux machine) modules Environments, the SC machine and the SECD machine The (aux schemer seasoned) module The Seasoned Schemer The (aux continuation) modules Classic operators, escapers, amb and Collatz sequences The (aux category) modules Monads: list, maybe, probability, ziplist, difference lists and state The (aux timsort) module Sorting and the trace buffer The (aux fds) modules Functional queues and union-find The (aux sxml) module Rendering SXML to HTML The (aux variable) module Logic variables introduced by fresh The (aux tabling) module Memoization and tabled definitions The (aux commons) module Learning tests for CHICKEN Scheme Promises delay and make-promise The Ackermann function On unary numbers, as lists Concurrent ML for CHICKEN Scheme Porting SML/NJ CML as the (aux cml) library CHICKEN Scheme Versions and implementation notes Pattern matching Scheme macrology: a generalized pattern matcher The (aux nondeterministic) module Learning tests for Scheme The (aux stream) modules Streams, streams after SICP, and sequences and power series The (aux unittest) module Bootstrapping a unittest framework Scheme lang: Chez, 48 and Chicken Some docs, refs and containers, respectively. Final shift for call/cc Direct implementation of shift and reset Call with Current Continuation Patterns Cogen in six lines The Seasoned Schemer The Little Schemer Adding generic functions to Scheme Handling control