miniKanren, live and untagged
Quine generation via relational interpreters
We present relational interpreters for several subsets of Scheme, written in the pure logic programming language miniKanren. We demonstrate these interpreters running “backwards”—that is, generating programs that evaluate to a specified value—and show how the interpreters can trivially generate quines (programs that evaluate to themselves). We demonstrate how to transform environment-passing interpreters written in Scheme into relational interpreters written in miniKanren. We show how constraint extensions to core miniKanren can be used to allow shadowing of the interpreter’s primitive forms (using the absent° tree constraint), and to avoid having to tag expressions in the languages being interpreted (using disequality constraints and symbol/number type-constraints), simplifying the interpreters and eliminating the need for parsers/unparsers.We provide four appendices to make the code in the paper completely self-contained. Three of these appendices contain new code: the complete implementation of core miniKanren extended with the new constraints; an extended relational interpreter capable of running factorial and doing list processing; and a simple pattern matcher that uses Dijkstra guards. The other appendix presents our preferred version of code that has been presented elsewhere: the miniKanren relational arithmetic system used in the extended interpreter.
William E. Byrd, Eric Holk, and Daniel P. Friedman. miniKanren, live and untagged: quine generation via relational interpreters (programming pearl). In Proceedings of the 2012 Annual Workshop on Scheme and Functional Programming, Scheme '12, pages 8–29, New York, NY, USA, 2012. Association for Computing Machinery. ISBN 9781450318952. doi: 10.1145/2661103.2661105. URL https://doi.org/10.1145/2661103.2661105.
test-λ-calculus-interpreter: pass
(define (test-λ-calculus-interpreter _)
(define-syntax-rule
(eval/env0 body)
(eval-exp 'body (interaction-environment/symbols '())))
(⊦ equal?
`(closure z z ())
(eval/env0 (((λ (x) (λ (y) x)) (λ (z) z)) (λ (a) a))))
(⊦ equal?
`(closure y x ((x closure z z ())))
(eval/env0 ((λ (x) (λ (y) x)) (λ (z) z))))
(⊦ equal? `(closure y y ()) (eval/env0 ((λ (x) x) (λ (y) y))))
(⊦ equal? `(closure y y ()) (eval/env0 ('(closure x x ()) (λ (y) y)))))
((eta 0.0) (memory #(12582912 4360144 1048576)) (stdout "") (stderr ""))
test/eval-exp°: pass
(define (test/eval-exp° _)
(⊦= '(bar)
(°->list
#t
(fresh° (q) (lookup° 'y (list (cons 'x 'foo) (cons 'y 'bar)) q))))
(⊦= '()
(°->list
#t
(fresh° (q) (lookup° 'w (list (cons 'x 'foo) (cons 'y 'bar)) q))))
(let* ((Q (car (°->list #f (take° 1 (fresh° (q) (eval-exp° q '() q))))))
(λQ (eval Q))
(quine (λQ 'α)))
(⊦= '(λ (α)
(begin (deny (equal? α 'closure)))
(begin (deny (equal? α 'list)))
(begin (deny (equal? α 'quote)))
(assert (every (μ v (symbol? v)) (list α)))
(cons (cons 'λ
(cons (cons α '())
(cons (cons 'list
(cons α
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons α '())))
'())))
'())))
(cons (cons 'quote
(cons (cons 'λ
(cons (cons α '())
(cons (cons 'list
(cons α
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons α '())))
'())))
'())))
'()))
'())))
Q)
(⊦= '((λ (α) (list α (list 'quote α))) '(λ (α) (list α (list 'quote α))))
quine)
(⊦= quine (eval quine)))
(⊦= '((λ (α)
(assert (absent? 'closure α))
(cons (cons 'quote (cons α '())) (cons '→ (cons α '()))))
(λ () (cons (cons 'list '()) (cons '→ (cons '() '()))))
(λ (α β)
(assert (every (μ v (symbol? v)) (list α)))
(cons (cons 'λ (cons (cons α '()) (cons β '())))
(cons '→
(cons (cons 'closure (cons α (cons β (cons '() '()))))
'()))))
(λ (α)
(assert (absent? 'closure α))
(cons (cons 'list (cons (cons 'quote (cons α '())) '()))
(cons '→ (cons (cons α '()) '()))))
(λ ()
(cons (cons 'list (cons (cons 'list '()) '()))
(cons '→ (cons (cons '() '()) '()))))
(λ (α β)
(assert (absent? 'closure α))
(assert (absent? 'closure β))
(cons (cons 'list
(cons (cons 'quote (cons α '()))
(cons (cons 'quote (cons β '())) '())))
(cons '→ (cons (cons α (cons β '())) '())))))
(°->list
#f
(take° 6 (fresh° (q e v) (eval-exp° e '() v) (=° `(,e → ,v) q))))))
((eta 0.076) (memory #(12582912 4409264 1048576)) (stdout "") (stderr ""))
test/eval-exp/shadowing: pass
(define (test/eval-exp/shadowing _)
(⊦= '(closure x x ()) (eval-exp '((λ (λ) (λ λ)) (λ (x) x)) '()))
(⊦= '(closure y y ()) (eval-exp '((λ (quote) 'quote) (λ (y) y)) '()))
(⊦= 'a (eval-exp '((λ (list) (list 'a)) (λ (x) x)) '()))
(⊦= '(a) (eval-exp '((λ (y) (list 'a)) (λ (x) x)) '())))
((eta 0.001) (memory #(12582912 4362248 1048576)) (stdout "") (stderr ""))
test/eval-exp°/agrees-with-eval-exp: pass
(define (test/eval-exp°/agrees-with-eval-exp _)
(let1 (programs
'(((λ (λ) (λ λ)) (λ (x) x))
((λ (quote) 'quote) (λ (y) y))
((λ (quote) '(λ (x) x)) (λ (y) y))
((λ (list) (list 'a)) (λ (x) x))
((λ (y) (list 'a)) (λ (x) x))
((λ (list) (list list)) (λ (z) z))
(((λ (x) (λ (y) x)) (λ (z) z)) (λ (a) a))))
(⊦= (map (λ (p) (list (eval-exp p '()))) programs)
(map (λ (p) (°->list #t (fresh° (q) (eval-exp° p '() q))))
programs))))
((eta 0.007) (memory #(12582912 4365496 1048576)) (stdout "") (stderr ""))
test/eval-λ°/forward-pairs: pass
(define (test/eval-λ°/forward-pairs _)
(⊦= '((λ (α β)
(assert (every (μ v (symbol? v)) (list α)))
(cons (cons 'λ (cons (cons α '()) (cons β '())))
(cons '→
(cons (cons 'closure (cons α (cons β (cons '() '()))))
'()))))
(λ (α β γ)
(assert (every (μ v (symbol? v)) (list α β)))
(cons (cons (cons 'λ (cons (cons α '()) (cons α '())))
(cons (cons 'λ (cons (cons β '()) (cons γ '()))) '()))
(cons '→
(cons (cons 'closure (cons β (cons γ (cons '() '()))))
'()))))
(λ (α β γ δ ε)
(begin (deny (equal? α 'λ)))
(assert (every (μ v (symbol? v)) (list α β δ)))
(cons (cons (cons 'λ
(cons (cons α '())
(cons (cons 'λ (cons (cons β '()) (cons γ '())))
'())))
(cons (cons 'λ (cons (cons δ '()) (cons ε '()))) '()))
(cons '→
(cons (cons 'closure
(cons β
(cons γ
(cons (cons (cons α
(cons 'closure (cons δ (cons ε (cons '() '())))))
'())
'()))))
'()))))
(λ (α β)
(assert (every (μ v (symbol? v)) (list α β)))
(cons (cons (cons 'λ
(cons (cons α '())
(cons (cons α (cons α '())) '())))
(cons (cons 'λ (cons (cons β '()) (cons β '()))) '()))
(cons '→
(cons (cons 'closure (cons β (cons β (cons '() '()))))
'()))))
(λ (α β γ δ)
(begin (deny (equal? β 'λ)))
(assert (every (μ v (symbol? v)) (list α β γ)))
(cons (cons (cons 'λ
(cons (cons α '())
(cons (cons α (cons α '())) '())))
(cons (cons 'λ
(cons (cons β '())
(cons (cons 'λ (cons (cons γ '()) (cons δ '())))
'())))
'()))
(cons '→
(cons (cons 'closure
(cons γ
(cons δ
(cons (cons (cons β
(cons 'closure
(cons β
(cons (cons 'λ (cons (cons γ '()) (cons δ '())))
(cons '() '())))))
'())
'()))))
'())))))
(°->list
#f
(take° 5 (fresh° (q e v) (eval-λ° e '() v) (=° `(,e → ,v) q))))))
((eta 0.004) (memory #(12582912 4386280 1048576)) (stdout "") (stderr ""))
test/eval-λ°/backwards: pass
(define (test/eval-λ°/backwards _)
(⊦= '(((λ (x) (λ (y) x)) (λ (z) z))
((λ (x) (x (λ (y) x))) (λ (z) z))
((λ (x) (λ (y) x)) ((λ (α) α) (λ (z) z)))
(((λ (α) α) (λ (x) (λ (y) x))) (λ (z) z))
((λ (α) α) ((λ (x) (λ (y) x)) (λ (z) z))))
(°->list
#t
(take° 5
(fresh°
(q)
(eval-λ° q '() '(closure y x ((x closure z z ()))))))))
(⊦= '(()
()
((assert (every (μ v (symbol? v)) (list α))))
((assert (every (μ v (symbol? v)) (list α))))
((assert (every (μ v (symbol? v)) (list α)))))
(map reified-constraints
(°->list
#f
(take° 5
(fresh°
(q)
(eval-λ° q '() '(closure y x ((x closure z z ())))))))))
(⊦= '(((λ (x) (λ (y) x)) (λ (z) z)) ((λ (x) (x (λ (y) x))) (λ (z) z)))
(°->list
#t
(take° 2
(fresh°
(q)
(eval-exp° q '() '(closure y x ((x closure z z ())))))))))
((eta 0.955) (memory #(25165824 4371216 1048576)) (stdout "") (stderr ""))
test/eval-exp°/shadowed-λ: pass
(define (test/eval-exp°/shadowed-λ _)
(⊦= '((closure λ (λ λ) ()))
(°->list #t (fresh° (q) (eval-exp° '(λ (λ) (λ λ)) '() q))))
(⊦= '((closure x x ()))
(°->list #t (fresh° (q) (eval-exp° '((λ (λ) (λ λ)) (λ (x) x)) '() q))))
(⊦= '()
(°->list
#t
(fresh° (q) (eval-exp° '((λ (λ) (λ (x) x)) (λ (y) y)) '() q)))))
((eta 0.002) (memory #(25165824 4371096 1048576)) (stdout "") (stderr ""))
test/eval-exp°/shadowed-quote: pass
(define (test/eval-exp°/shadowed-quote _)
(⊦= '((closure y y ()))
(°->list
#t
(fresh° (q) (eval-exp° '((λ (quote) 'quote) (λ (y) y)) '() q))))
(⊦= '((closure x x ((quote closure y y ()))))
(°->list
#t
(fresh° (q) (eval-exp° '((λ (quote) '(λ (x) x)) (λ (y) y)) '() q))))
(⊦= '((closure x x ((quote closure y y ()))))
(°->list
#t
(fresh° (q) (eval-exp° ''(λ (x) x) '((quote closure y y ())) q))))
(⊦= '() (°->list #t (fresh° (q) (eval-exp° ''(λ (x) x) '((quote . foo)) q))))
(⊦= '((λ (x) x)) (°->list #t (fresh° (q) (eval-exp° ''(λ (x) x) '() q))))
(⊦= '(quote) (°->list #t (fresh° (q) (eval-exp° ''quote '() q)))))
((eta 0.003) (memory #(25165824 4374368 1048576)) (stdout "") (stderr ""))
test/eval-exp°/shadowed-list: pass
(define (test/eval-exp°/shadowed-list _)
(⊦= '(a)
(°->list
#t
(fresh° (q) (eval-exp° '((λ (list) (list 'a)) (λ (x) x)) '() q))))
(⊦= '((a))
(°->list
#t
(fresh° (q) (eval-exp° '((λ (y) (list 'a)) (λ (x) x)) '() q))))
(⊦= '((closure z z ()))
(°->list
#t
(fresh° (q) (eval-exp° '((λ (list) (list list)) (λ (z) z)) '() q)))))
((eta 0.003) (memory #(25165824 4370424 1048576)) (stdout "") (stderr ""))
test/eval-exp°/unguarded-overlap: pass
(define (test/eval-exp°/unguarded-overlap _)
(define (proper-list/unguarded° exp env val)
(cond° ((=° '() exp) (=° '() val))
((fresh°
(a d v-a v-d)
(=° `(,a unquote d) exp)
(=° `(,v-a unquote v-d) val)
(eval-exp/unguarded° a env v-a)
(proper-list/unguarded° d env v-d)))))
(define (eval-exp/unguarded° exp env val)
(cond° ((fresh° (v) (=° `',v exp) (absent° 'closure v) (=° v val)))
((fresh°
(a*)
(=° `(list unquote a*) exp)
(absent° 'closure a*)
(proper-list/unguarded° a* env val)))
((symbol° exp) (lookup° exp env val))
((fresh°
(rator rand x body envˆ a)
(=° `(,rator ,rand) exp)
(eval-exp/unguarded° rator env `(closure ,x ,body ,envˆ))
(eval-exp/unguarded° rand env a)
(eval-exp/unguarded° body `((,x unquote a) unquote envˆ) val)))
((fresh°
(x body)
(=° `(λ (,x) ,body) exp)
(symbol° x)
(=° `(closure ,x ,body ,env) val)))))
(⊦= '((a) a)
(°->list
#t
(fresh°
(q)
(eval-exp/unguarded° '((λ (list) (list 'a)) (λ (x) x)) '() q))))
(⊦= (list 'quote '(closure y y ()))
(°->list
#t
(fresh°
(q)
(eval-exp/unguarded° '((λ (quote) 'quote) (λ (y) y)) '() q))))
(⊦= '((closure x x ((λ closure y y ()))))
(°->list
#t
(fresh°
(q)
(eval-exp/unguarded° '((λ (λ) (λ (x) x)) (λ (y) y)) '() q)))))
((eta 0.004) (memory #(25165824 4373808 1048576)) (stdout "") (stderr ""))
test/absent°/closure-tag: pass
(define (test/absent°/closure-tag _)
(⊦= '()
(°->list
#t
(fresh° (q) (eval-exp° '('(closure x x ()) (λ (y) y)) '() q))))
(⊦= '() (°->list #t (fresh° (q) (eval-exp° ''(closure x x ()) '() q))))
(⊦= '() (°->list #f (fresh° (q) (eval-exp° `',q '() '(closure x x ())))))
(⊦= '((λ () (cons 'λ (cons (cons 'x '()) (cons 'x '()))))
(λ (α)
(begin (deny (equal? α 'closure)))
(assert (every (μ v (symbol? v)) (list α)))
(cons (cons 'λ (cons (cons α '()) (cons α '())))
(cons (cons 'λ (cons (cons 'x '()) (cons 'x '()))) '())))
(λ (α)
(begin (deny (equal? α 'closure)))
(assert (every (μ v (symbol? v)) (list α)))
(cons (cons 'λ (cons (cons α '()) (cons (cons α (cons α '())) '())))
(cons (cons 'λ (cons (cons 'x '()) (cons 'x '()))) '()))))
(°->list
#f
(take° 3
(fresh° (q) (eval-exp° `(list ,q) '() '((closure x x ()))))))))
((eta 0.17) (memory #(25165824 6684984 1048576)) (stdout "") (stderr ""))
test/eval-exp°/backwards-shadowed-quote: pass
(define (test/eval-exp°/backwards-shadowed-quote _)
(let1 (answers
(°->list
#f
(take° 6
(fresh°
(q)
(eval-exp°
`((λ (quote) ,q) (λ (x) x))
'()
'(closure x x ()))))))
(⊦= '(quote 'quote
((λ (α) α) quote)
((λ (α) quote) quote)
((λ (α) quote) (list))
((λ (α) (α α)) quote))
(map (λ (A) (apply (eval A) (cadr A))) answers))
(⊦= '(()
()
((assert (every (μ v (symbol? v)) (list α))))
((begin (deny (equal? α 'quote)))
(assert (every (μ v (symbol? v)) (list α))))
((begin (deny (equal? α 'quote)))
(assert (every (μ v (symbol? v)) (list α))))
((assert (every (μ v (symbol? v)) (list α)))))
(map reified-constraints answers))))
((eta 0.025) (memory #(25165824 4382696 1048576)) (stdout "") (stderr ""))
test/eval-exp°/backwards-shadowed-list: pass
(define (test/eval-exp°/backwards-shadowed-list _)
(let1 (programs
(°->list
#t
(take° 10
(fresh°
(p q)
(=° `((λ (list) ,q) (λ (x) x)) p)
(eval-exp° p '() '(a))))))
(⊦= '(((λ (list) '(a)) (λ (x) x))
((λ (list) (list '(a))) (λ (x) x))
((λ (list) ((λ (α) '(a)) 'β)) (λ (x) x))
((λ (list) ((λ (α) α) '(a))) (λ (x) x))
((λ (list) ((λ (α) '(a)) list)) (λ (x) x))
((λ (list) ((λ (α) (list '(a))) 'β)) (λ (x) x))
((λ (list) ((λ (α) (list α)) '(a))) (λ (x) x))
((λ (list) ((λ (α) '(a)) (λ (β) γ))) (λ (x) x))
((λ (list) ((λ (α) ((λ (β) '(a)) 'γ)) 'δ)) (λ (x) x))
((λ (list) ((λ (α) (α '(a))) list)) (λ (x) x)))
programs)
(⊦= (make-list 10 '(a)) (map eval programs))))
((eta 0.022) (memory #(25165824 4374624 1048576)) (stdout "") (stderr ""))
test/eval-exp°/untagged-answers-run-in-scheme: pass
(define (test/eval-exp°/untagged-answers-run-in-scheme _)
(let1 (programs
(°->list #t (take° 30 (fresh° (q) (eval-exp° q '() '(I love you))))))
(⊦= '('(I love you)
((λ (α) '(I love you)) 'β)
((λ (α) α) '(I love you))
(list 'I 'love 'you)
((λ (α) '(I love you)) (list))
((λ (α) '(I love you)) (λ (β) γ)))
(take programs 6))
(⊦= (make-list 30 '(I love you)) (map eval programs))
(⊦= (make-list 30 '(I love you))
(map (λ (p) (eval-exp p '())) programs))))
((eta 0.074) (memory #(25165824 4390944 1048576)) (stdout "") (stderr ""))
test/quinec/scheme: pass
(define (test/quinec/scheme _) (⊦= quinec (eval quinec)))
((eta 0.0) (memory #(25165824 4376160 1048576)) (stdout "") (stderr ""))
test/quinec/forward: pass
(define (test/quinec/forward _)
(⊦= (list quinec) (μkanren-run (v -1 #t) (eval-exp° quinec '() v)))
(⊦= (list quinec) (μkanren-run (q -1 #t) (=° q quinec) (quine° q))))
((eta 0.005) (memory #(25165824 4387760 1048576)) (stdout "") (stderr ""))
test/quine°/α-equivalent-to-quinec: pass
(define (test/quine°/α-equivalent-to-quinec _)
(let* ((Q (car (°->list #f (take° 1 (fresh° (q) (quine° q))))))
(λQ (eval Q)))
(⊦= quinec (λQ 'x))
(⊦= (λQ 'y) (eval (λQ 'y)))
(⊦= (list (λQ 'y)) (μkanren-run (v -1 #t) (eval-exp° (λQ 'y) '() v)))
(⊦raises (exn) (λQ 'closure))
(⊦raises (exn) (λQ 'list))
(⊦raises (exn) (λQ 'quote))))
((eta 0.066) (memory #(25165824 4410280 1048576)) (stdout "") (stderr ""))
test/quine°/disequalities-are-needed: pass
(define (test/quine°/disequalities-are-needed _)
(let* ((Q (car (°->list #f (take° 1 (fresh° (q) (quine° q))))))
(λQ! (eval `(λ (α) ,(last Q)))))
(⊦= '() (μkanren-run (v -1 #t) (eval-exp° (λQ! 'closure) '() v)))
(⊦= '() (μkanren-run (v -1 #t) (eval-exp° (λQ! 'list) '() v)))
(⊦= '() (μkanren-run (v -1 #t) (eval-exp° (λQ! 'quote) '() v)))
(⊦= '((λ (λ) (list λ (list 'quote λ))) '(λ (λ) (list λ (list 'quote λ))))
(λQ! 'λ))
(⊦= (list (λQ! 'λ)) (μkanren-run (v -1 #t) (eval-exp° (λQ! 'λ) '() v)))
(⊦= (λQ! 'λ) (eval (λQ! 'λ)))))
((eta 0.066) (memory #(25165824 4381344 1048576)) (stdout "") (stderr ""))
test/quine°/no-literal-quines: pass
(define (test/quine°/no-literal-quines _)
(⊦= 5 (eval 5))
(⊦= #t (eval #t))
(⊦= '() (μkanren-run (v -1 #t) (eval-exp° 5 '() v)))
(⊦= '() (μkanren-run (v -1 #t) (eval-exp° #t '() v)))
(⊦= '() (μkanren-run (q -1 #t) (symbol° q) (quine° q)))
(⊦= '() (μkanren-run (q -1 #t) (fresh° (v) (=° `',v q) (quine° q))))
(⊦= '()
(μkanren-run (q -1 #t) (fresh° (x b) (=° `(λ (,x) ,b) q) (quine° q)))))
((eta 0.0) (memory #(25165824 4386792 1048576)) (stdout "") (stderr ""))
test/quine°/second: pass
(define (test/quine°/second _)
(⊦= '(λ (α β γ)
(begin (deny (equal? α 'closure)))
(begin (deny (equal? α 'list)))
(begin (deny (equal? α 'quote)))
(begin (deny (equal? α 'λ)))
(begin (deny (equal? β 'closure)))
(begin (deny (equal? β α)))
(assert (every (μ v (symbol? v)) (list α β)))
(assert (absent? 'closure γ))
(cons (cons 'λ
(cons (cons α '())
(cons (cons 'list
(cons (cons (cons 'λ (cons (cons β '()) (cons α '())))
(cons (cons 'quote (cons γ '())) '()))
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons α '())))
'())))
'())))
(cons (cons 'quote
(cons (cons 'λ
(cons (cons α '())
(cons (cons 'list
(cons (cons (cons 'λ (cons (cons β '()) (cons α '())))
(cons (cons 'quote (cons γ '())) '()))
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons α '())))
'())))
'())))
'()))
'())))
(cadr (°->list #f (take° 2 (fresh° (q) (quine° q)))))))
((eta 0.27) (memory #(25165824 4410752 1048576)) (stdout "") (stderr ""))
test/quine°/ten: pass
(define (test/quine°/ten _)
(let1 (qs (μkanren-run (q 10 #t) (quine° q)))
(⊦= '(((λ (α) (list α (list 'quote α)))
'(λ (α) (list α (list 'quote α))))
((λ (α) (list ((λ (β) α) 'γ) (list 'quote α)))
'(λ (α) (list ((λ (β) α) 'γ) (list 'quote α))))
((λ (α) (list α (list ((λ (β) 'quote) 'γ) α)))
'(λ (α) (list α (list ((λ (β) 'quote) 'γ) α))))
((λ (α) (list (list 'λ '(α) α) (list 'quote α)))
'(list (list 'λ '(α) α) (list 'quote α)))
((λ (α) ((λ (β) (list α (list 'quote α))) 'γ))
'(λ (α) ((λ (β) (list α (list 'quote α))) 'γ)))
((λ (α) (list α (list ((λ (β) β) 'quote) α)))
'(λ (α) (list α (list ((λ (β) β) 'quote) α))))
((λ (α) (list α ((λ (β) (list 'quote α)) 'γ)))
'(λ (α) (list α ((λ (β) (list 'quote α)) 'γ))))
((λ (α) (list α (list 'quote ((λ (β) α) 'γ))))
'(λ (α) (list α (list 'quote ((λ (β) α) 'γ)))))
((λ (α) ((λ (β) (list β (list 'quote β))) α))
'(λ (α) ((λ (β) (list β (list 'quote β))) α)))
((λ (α) (list α ((λ (β) (list 'quote β)) α)))
'(λ (α) (list α ((λ (β) (list 'quote β)) α)))))
qs)
(⊦= 10 (length (delete-duplicates qs)))
(⊦ every (λ (p) (equal? p (eval p))) qs)
(⊦ every
(λ (p)
(equal? (list p) (μkanren-run (v -1 #t) (eval-exp° p '() v))))
qs)))
((eta 1.048) (memory #(25165824 4406272 1048576)) (stdout "") (stderr ""))
test/quine°/fixed-variable: pass
(define (test/quine°/fixed-variable _)
(⊦= (list quinec)
(μkanren-run
(q 1 #t)
(fresh° (b r) (=° `((λ (x) ,b) ,r) q) (quine° q)))))
((eta 0.028) (memory #(25165824 4393056 1048576)) (stdout "") (stderr ""))
test/quine°/application-body: pass
(define (test/quine°/application-body _)
(⊦= '((λ (α β γ)
(begin (deny (equal? α 'closure)))
(begin (deny (equal? α 'list)))
(begin (deny (equal? α 'quote)))
(begin (deny (equal? α 'λ)))
(begin (deny (equal? β 'closure)))
(begin (deny (equal? β 'list)))
(begin (deny (equal? β 'quote)))
(begin (deny (equal? β α)))
(assert (every (μ v (symbol? v)) (list α β)))
(assert (absent? 'closure γ))
(cons (cons 'λ
(cons (cons α '())
(cons (cons (cons 'λ
(cons (cons β '())
(cons (cons 'list
(cons α
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons α '())))
'())))
'())))
(cons (cons 'quote (cons γ '())) '()))
'())))
(cons (cons 'quote
(cons (cons 'λ
(cons (cons α '())
(cons (cons (cons 'λ
(cons (cons β '())
(cons (cons 'list
(cons α
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons α '())))
'())))
'())))
(cons (cons 'quote (cons γ '())) '()))
'())))
'()))
'()))))
(°->list
#f
(take° 1
(fresh°
(q x f y r)
(=° `((λ (,x) (,f ,y)) ,r) q)
(quine° q))))))
((eta 0.238) (memory #(25165824 4414664 1048576)) (stdout "") (stderr ""))
test/quine°/operand-hole: pass
(define (test/quine°/operand-hole _)
(⊦= '('(λ (x) (list x (list 'quote x))))
(μkanren-run (r 1 #t) (quine° `((λ (x) (list x (list 'quote x))) ,r)))))
((eta 0.003) (memory #(25165824 4391464 1048576)) (stdout "") (stderr ""))
test/quine°/body-hole: pass
(define (test/quine°/body-hole _)
(⊦= '((λ ()
(cons 'list
(cons 'x
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons 'x '())))
'()))))
(λ (α β)
(begin (deny (equal? α 'closure)))
(begin (deny (equal? α 'x)))
(assert (every (μ v (symbol? v)) (list α)))
(assert (absent? 'closure β))
(cons 'list
(cons (cons (cons 'λ (cons (cons α '()) (cons 'x '())))
(cons (cons 'quote (cons β '())) '()))
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons 'x '())))
'()))))
(λ (α β)
(begin (deny (equal? α 'closure)))
(begin (deny (equal? α 'quote)))
(assert (every (μ v (symbol? v)) (list α)))
(assert (absent? 'closure β))
(cons 'list
(cons 'x
(cons (cons 'list
(cons (cons (cons 'λ
(cons (cons α '())
(cons (cons 'quote (cons 'quote '())) '())))
(cons (cons 'quote (cons β '())) '()))
(cons 'x '())))
'())))))
(°->list #f (take° 3 (fresh° (b) (quine° `((λ (x) ,b) '(λ (x) ,b))))))))
((eta 0.067) (memory #(25165824 4403160 1048576)) (stdout "") (stderr ""))
test/quine°/quote-hole: pass
(define (test/quine°/quote-hole _)
(⊦= '((λ () (cons 'quote (cons 'quote '())))
(λ (α β)
(begin (deny (equal? α 'closure)))
(begin (deny (equal? α 'quote)))
(assert (every (μ v (symbol? v)) (list α)))
(assert (absent? 'closure β))
(cons (cons 'λ
(cons (cons α '())
(cons (cons 'quote (cons 'quote '())) '())))
(cons (cons 'quote (cons β '())) '())))
(λ (α)
(begin (deny (equal? α 'closure)))
(assert (every (μ v (symbol? v)) (list α)))
(cons (cons 'λ (cons (cons α '()) (cons α '())))
(cons (cons 'quote (cons 'quote '())) '()))))
(°->list
#f
(take° 3
(fresh°
(h)
(quine°
`((λ (x) (list x (list ,h x)))
'(λ (x) (list x (list ,h x))))))))))
((eta 0.004) (memory #(25165824 4399784 1048576)) (stdout "") (stderr ""))
test/twine°/run1: pass
(define (test/twine°/run1 _)
(let* ((X (car (°->list #f (take° 1 (fresh° (x) (twine° x))))))
(twine ((eval X) 'α))
(p (car twine))
(q (cadr twine)))
(⊦= '(λ (α)
(begin (deny (equal? α 'closure)))
(begin (deny (equal? α 'list)))
(begin (deny (equal? α 'quote)))
(assert (every (μ v (symbol? v)) (list α)))
(cons (cons 'quote
(cons (cons (cons 'λ
(cons (cons α '())
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons (cons 'list
(cons α
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons α '())))
'())))
'())))
'())))
(cons (cons 'quote
(cons (cons 'λ
(cons (cons α '())
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons (cons 'list
(cons α
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons α '())))
'())))
'())))
'())))
'()))
'()))
'()))
(cons (cons (cons 'λ
(cons (cons α '())
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons (cons 'list
(cons α
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons α '())))
'())))
'())))
'())))
(cons (cons 'quote
(cons (cons 'λ
(cons (cons α '())
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons (cons 'list
(cons α
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons α '())))
'())))
'())))
'())))
'()))
'()))
'())))
X)
(⊦= '('((λ (α) (list 'quote (list α (list 'quote α))))
'(λ (α) (list 'quote (list α (list 'quote α)))))
((λ (α) (list 'quote (list α (list 'quote α))))
'(λ (α) (list 'quote (list α (list 'quote α))))))
twine)
(⊦ equal? q (eval p))
(⊦ equal? p (eval q))
(⊦≠ p q)
(⊦= `',q p)))
((eta 0.825) (memory #(25165824 4403144 1048576)) (stdout "") (stderr ""))
test/twine°/forwards: pass
(define (test/twine°/forwards _)
(define p
''((λ (α) (list 'quote (list α (list 'quote α))))
'(λ (α) (list 'quote (list α (list 'quote α))))))
(define q
'((λ (α) (list 'quote (list α (list 'quote α))))
'(λ (α) (list 'quote (list α (list 'quote α))))))
(⊦= (list q) (°->list #t (fresh° (v) (eval-exp° p '() v))))
(⊦= (list p) (°->list #t (fresh° (v) (eval-exp° q '() v))))
(⊦= (list q)
(°->list #t (fresh° (r) (eval-exp° p '() r) (eval-exp° r '() p))))
(⊦= (list p) (°->list #t (take° 1 (fresh° (e) (eval-exp° e '() q))))))
((eta 0.011) (memory #(25165824 4404808 1048576)) (stdout "") (stderr ""))
test/twine°/quine: pass
(define (test/twine°/quine _)
(define quine
'((λ (α) (list α (list 'quote α))) '(λ (α) (list α (list 'quote α)))))
(⊦= (list quine)
(°->list
#t
(fresh° (q) (eval-exp° quine '() q) (eval-exp° q '() quine))))
(⊦= '()
(°->list
#t
(fresh°
(q)
(≠° quine q)
(eval-exp° quine '() q)
(eval-exp° q '() quine))))
(let* ((X (car (°->list
#f
(take° 1
(fresh°
(x p q)
(=° p q)
(eval-exp° p '() q)
(eval-exp° q '() p)
(=° `(,p ,q) x))))))
(twine ((eval X) 'α)))
(⊦= '((begin (deny (equal? α 'closure)))
(begin (deny (equal? α 'list)))
(begin (deny (equal? α 'quote)))
(assert (every (μ v (symbol? v)) (list α))))
(reified-constraints X))
(⊦= (list quine quine) twine)))
((eta 0.084) (memory #(25165824 4417200 1048576)) (stdout "") (stderr ""))
test/twine°/run2: pass
(define (test/twine°/run2 _)
(let* ((X (cadr (°->list #f (take° 2 (fresh° (x) (twine° x))))))
(twine ((eval X) 'α 'β 'γ))
(p (car twine))
(q (cadr twine)))
(⊦= '((begin (deny (equal? α 'closure)))
(begin (deny (equal? α 'list)))
(begin (deny (equal? α 'quote)))
(begin (deny (equal? α 'λ)))
(begin (deny (equal? β 'closure)))
(begin (deny (equal? β α)))
(assert (every (μ v (symbol? v)) (list α β)))
(assert (absent? 'closure γ)))
(reified-constraints X))
(⊦= '('((λ (α) (list 'quote (list ((λ (β) α) 'γ) (list 'quote α))))
'(λ (α) (list 'quote (list ((λ (β) α) 'γ) (list 'quote α)))))
((λ (α) (list 'quote (list ((λ (β) α) 'γ) (list 'quote α))))
'(λ (α) (list 'quote (list ((λ (β) α) 'γ) (list 'quote α))))))
twine)
(⊦ equal? q (eval p))
(⊦ equal? p (eval q))
(⊦≠ p q)))
((eta 4.252) (memory #(50331648 4412168 1048576)) (stdout "") (stderr ""))
test/thrine°/search: pass
(define (test/thrine°/search _)
(let* ((Q (car (°->list
#f
(take° 1
(fresh°
(x p q r)
(≠° p q)
(≠° q r)
(≠° r p)
(eval-exp° p '() q)
(eval-exp° q '() r)
(eval-exp° r '() p)
(=° `(,p ,q ,r) x))))))
(λQ (eval Q))
(thrine (λQ 'α))
(p (first thrine))
(q (second thrine))
(r (third thrine)))
(⊦= '(λ (α)
(begin (deny (equal? α 'closure)))
(begin (deny (equal? α 'list)))
(begin (deny (equal? α 'quote)))
(assert (every (μ v (symbol? v)) (list α))))
(drop-right Q 1))
(⊦= '(''((λ (α) (list 'quote (list 'quote (list α (list 'quote α)))))
'(λ (α) (list 'quote (list 'quote (list α (list 'quote α))))))
'((λ (α) (list 'quote (list 'quote (list α (list 'quote α)))))
'(λ (α) (list 'quote (list 'quote (list α (list 'quote α))))))
((λ (α) (list 'quote (list 'quote (list α (list 'quote α)))))
'(λ (α) (list 'quote (list 'quote (list α (list 'quote α)))))))
thrine)
(⊦ equal? q (eval p))
(⊦ equal? r (eval q))
(⊦ equal? p (eval r))
(⊦= '(#f #f #f) (list (equal? p q) (equal? q r) (equal? r p)))
(⊦= '(#f #f #f) (map (λ (e) (equal? e (eval e))) thrine))
(⊦= '(#f #f #f) (map (λ (e) (equal? e (eval (eval e)))) thrine))
(let* ((thrine/x (λQ 'x))
(p/x (first thrine/x))
(q/x (second thrine/x))
(r/x (third thrine/x)))
(⊦= '((λ (x) (list 'quote (list 'quote (list x (list 'quote x)))))
'(λ (x) (list 'quote (list 'quote (list x (list 'quote x))))))
r/x)
(⊦= (list q/x r/x p/x) (map eval thrine/x)))))
((eta 5.312) (memory #(50331648 4401016 1048576)) (stdout "") (stderr ""))
test/thrine°/ground: pass
(define (test/thrine°/ground _)
(let* ((R '(λ (α) (list 'quote (list 'quote (list α (list 'quote α))))))
(r `(,R ',R))
(q `',r)
(p `',q))
(⊦= (list q) (°->list #t (fresh° (v) (eval-exp° p '() v))))
(⊦= (list r) (°->list #t (fresh° (v) (eval-exp° q '() v))))
(⊦= (list p) (°->list #t (fresh° (v) (eval-exp° r '() v))))
(⊦= '() (°->list #t (fresh° (v) (eval-exp° p '() p))))
(⊦= '() (°->list #t (fresh° (v) (eval-exp° q '() q))))
(⊦= '() (°->list #t (fresh° (v) (eval-exp° r '() r))))))
((eta 0.01) (memory #(50331648 4403616 1048576)) (stdout "") (stderr ""))
test/eval-exp/extended°/fact5: pass
(define (test/eval-exp/extended°/fact5 _)
(define rel-fact5
`((λ (f) ((f f) (int-exp ,(build-num 5))))
(λ (f)
(λ (n)
(if (zero? n) (int-exp ,(build-num 1)) (* n ((f f) (sub1 n))))))))
(⊦= '((int-val (0 0 0 1 1 1 1)))
(μkanren-run (q -1 #t) (eval-exp/extended° rel-fact5 '() q))))
((eta 0.077) (memory #(50331648 4400112 1048576)) (stdout "") (stderr ""))
test/eval-exp/extended°/forward: pass
(define (test/eval-exp/extended°/forward _)
(⊦= '((closure (x y) x ()))
(μkanren-run (q -1 #t) (eval-exp/extended° '(λ (x y) x) '() q)))
(⊦= '((b . a))
(μkanren-run
(q -1 #t)
(eval-exp/extended° '((λ (x y) (cons y x)) 'a 'b) '() q)))
(⊦= '((#t))
(μkanren-run
(q -1 #t)
(eval-exp/extended° '(cdr (cons #f (cons #t '()))) '() q)))
(⊦= '(yes)
(μkanren-run
(q -1 #t)
(eval-exp/extended°
'(if (zero? (sub1 (int-exp (1)))) 'yes 'no)
'()
q)))
(⊦= '(#t)
(μkanren-run
(q -1 #t)
(eval-exp/extended° '(not (zero? (int-exp (1)))) '() q)))
(⊦= '(((int-val (1)) #t))
(μkanren-run
(q -1 #t)
(eval-exp/extended° '(list (int-exp (1)) #t) '() q))))
((eta 0.028) (memory #(50331648 4398400 1048576)) (stdout "") (stderr ""))
test/eval-exp/extended°/guards: pass
(define (test/eval-exp/extended°/guards _)
(⊦= '(#t)
(μkanren-run
(q -1 #t)
(eval-exp/extended° '((λ (not) (not #t)) (λ (x) x)) '() q)))
(⊦= '() (μkanren-run (q -1 #t) (eval-exp/extended° ''(int-val (1)) '() q)))
(⊦= '()
(μkanren-run
(q -1 #t)
(eval-exp/extended° '(cons (int-exp (1)) #t) '() q)))
(⊦= '()
(μkanren-run (q -1 #t) (eval-exp/extended° '(car (int-exp (1))) '() q)))
(⊦= '()
(μkanren-run (q -1 #t) (eval-exp/extended° '(sub1 (int-exp ())) '() q))))
((eta 0.012) (memory #(50331648 4410432 1048576)) (stdout "") (stderr ""))
test/eval-exp/extended°/backward-arithmetic: pass
(define (test/eval-exp/extended°/backward-arithmetic _)
(⊦= '((0 1))
(μkanren-run
(q -1 #t)
(eval-exp/extended°
`(* (int-exp ,q) (int-exp (1 1)))
'()
'(int-val (0 1 1)))))
(⊦= '(((1) (0 1 1)) ((0 1 1) (1)) ((0 1) (1 1)) ((1 1) (0 1)))
(μkanren-run
(q -1 #t)
(fresh°
(a b)
(=° q (list a b))
(eval-exp/extended°
`(* (int-exp ,a) (int-exp ,b))
'()
'(int-val (0 1 1))))))
(⊦= '((1 1 1))
(μkanren-run
(q -1 #t)
(eval-exp/extended° `(sub1 (int-exp ,q)) '() '(int-val (0 1 1))))))
((eta 0.02) (memory #(50331648 4399640 1048576)) (stdout "") (stderr ""))
test/eval-exp/extended°/six: pass
(define (test/eval-exp/extended°/six _)
(let1 (six (μkanren-run
(q 15 #t)
(eval-exp/extended° q '() `(int-val ,(build-num 6)))))
(⊦= '((int-exp (0 1 1))
((λ () (int-exp (0 1 1))))
(sub1 (int-exp (1 1 1)))
((λ (α) (int-exp (0 1 1))) 'β)
(* (int-exp (1)) (int-exp (0 1 1)))
(* (int-exp (0 1 1)) (int-exp (1)))
(* (int-exp (0 1)) (int-exp (1 1)))
((λ (α) (int-exp (0 1 1))) (list))
(car (list (int-exp (0 1 1))))
((λ () ((λ () (int-exp (0 1 1))))))
(sub1 ((λ () (int-exp (1 1 1)))))
(car (list (int-exp (0 1 1)) 'α)))
(take six 12))
(⊦= '(* (int-exp (0 1)) (int-exp (1 1))) (list-ref six 6))
(⊦= '((λ () (sub1 (int-exp (1 1 1))))) (list-ref six 14)))
(⊦= '(λ (α β)
(begin (deny (equal? α 'int-exp)))
(assert (absent? 'closure β))
(assert (absent? 'int-val β))
(cons (cons 'λ
(cons (cons α '())
(cons (cons 'int-exp
(cons (cons 0 (cons 1 (cons 1 '()))) '()))
'())))
(cons (cons 'quote (cons β '())) '())))
(list-ref
(°->list
#f
(take° 4
(fresh°
(q)
(eval-exp/extended° q '() `(int-val ,(build-num 6))))))
3)))
((eta 0.198) (memory #(50331648 4409992 1048576)) (stdout "") (stderr ""))
test/eval-exp/extended°/boolean-quines: pass
(define (test/eval-exp/extended°/boolean-quines _)
(⊦= '((λ () #t) (λ () #f))
(°->list #f (take° 2 (fresh° (q) (eval-exp/extended° q '() q)))))
(let1 (booleans (μkanren-run (q 2 #t) (eval-exp/extended° q '() q)))
(⊦= '(#t #f) booleans)
(⊦= booleans (map eval booleans))))
((eta 0.0) (memory #(50331648 4401040 1048576)) (stdout "") (stderr ""))
test/eval-exp/extended°/quines: pass
(define (test/eval-exp/extended°/quines _)
(let* ((Qs (°->list #f (take° 5 (fresh° (q) (eval-exp/extended° q '() q)))))
(quines
(map (λ (Q) (apply (eval Q) (take '(α β) (length (cadr Q))))) Qs)))
(⊦= '(λ (α)
(begin (deny (equal? α 'closure)))
(begin (deny (equal? α 'int-val)))
(begin (deny (equal? α 'list)))
(begin (deny (equal? α 'quote)))
(assert (every (μ v (symbol? v)) (list α)))
(cons (cons 'λ
(cons (cons α '())
(cons (cons 'list
(cons α
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons α '())))
'())))
'())))
(cons (cons 'quote
(cons (cons 'λ
(cons (cons α '())
(cons (cons 'list
(cons α
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons α '())))
'())))
'())))
'()))
'())))
(list-ref Qs 2))
(⊦= '(λ (α β)
(begin (deny (equal? α 'car)))
(begin (deny (equal? α 'closure)))
(begin (deny (equal? α 'int-val)))
(begin (deny (equal? α 'list)))
(begin (deny (equal? α 'quote)))
(assert (every (μ v (symbol? v)) (list α)))
(assert (absent? 'closure β))
(assert (absent? 'int-val β))
(cons (cons 'λ
(cons (cons α '())
(cons (cons 'list
(cons α
(cons (cons 'list
(cons (cons 'car
(cons (cons 'quote (cons (cons 'quote β) '()))
'()))
(cons α '())))
'())))
'())))
(cons (cons 'quote
(cons (cons 'λ
(cons (cons α '())
(cons (cons 'list
(cons α
(cons (cons 'list
(cons (cons 'car
(cons (cons 'quote (cons (cons 'quote β) '()))
'()))
(cons α '())))
'())))
'())))
'()))
'())))
(list-ref Qs 3))
(⊦= '(λ (α)
(begin (deny (equal? α 'closure)))
(begin (deny (equal? α 'int-val)))
(begin (deny (equal? α 'list)))
(begin (deny (equal? α 'quote)))
(assert (every (μ v (symbol? v)) (list α)))
(cons (cons 'λ
(cons (cons α '())
(cons (cons 'list
(cons (cons 'list
(cons (cons 'quote (cons 'λ '()))
(cons (cons 'quote (cons (cons α '()) '()))
(cons α '()))))
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons α '())))
'())))
'())))
(cons (cons 'quote
(cons (cons 'list
(cons (cons 'list
(cons (cons 'quote (cons 'λ '()))
(cons (cons 'quote (cons (cons α '()) '()))
(cons α '()))))
(cons (cons 'list
(cons (cons 'quote (cons 'quote '()))
(cons α '())))
'())))
'()))
'())))
(list-ref Qs 4))
(⊦= '(#t
#f
((λ (α) (list α (list 'quote α))) '(λ (α) (list α (list 'quote α))))
((λ (α) (list α (list (car '(quote . β)) α)))
'(λ (α) (list α (list (car '(quote . β)) α))))
((λ (α) (list (list 'λ '(α) α) (list 'quote α)))
'(list (list 'λ '(α) α) (list 'quote α))))
quines)
(⊦ every (λ (quine) (equal? quine (eval quine))) quines)))
((eta 3.017) (memory #(50331648 4421936 1048576)) (stdout "") (stderr ""))
test/symbol°: pass
(define (test/symbol° _)
(⊦= '((λ (α) (assert (every (μ v (symbol? v)) (list α))) α))
(°->list #f (fresh° (s) (symbol° s))))
(⊦= '((λ (α) α)) (°->list #f (fresh° (s r) (symbol° r)))))
((eta 0.0) (memory #(50331648 4405328 1048576)) (stdout "") (stderr ""))
test/≠°: pass
(define (test/≠° _)
(⊦= '() (°->list #f (fresh° (s) (≠° (+ 2 3) 5))))
(⊦= '((λ (α) α)) (°->list #f (fresh° (s) (≠° (* 2 3) 5))))
(⊦= '((λ (α) (begin (deny (equal? α 5))) (begin (deny (equal? α 6))) α))
(°->list #f (fresh° (q x) (≠° 5 q) (=° x q) (≠° 6 x))))
(⊦= '((λ (α) α)) (°->list #f (fresh° (q y z) (≠° (cons y z) q))))
(⊦= '((λ (α β γ)
(begin (deny (equal? α (cons β γ))))
(cons α (cons β (cons γ '())))))
(°->list #f (fresh° (q x y z) (≠° (cons y z) x) (=° (list x y z) q))))
(⊦= '((λ (α)
(begin (deny (equal? α 6)))
(cons (cons 5 α) (cons 5 (cons α '())))))
(°->list
#f
(fresh°
(q x y z)
(=° (cons y z) x)
(≠° (cons 5 6) x)
(=° 5 y)
(=° (list x y z) q))))
(⊦= '((λ (α) (cons (cons 6 α) (cons 6 (cons α '())))))
(°->list
#f
(fresh°
(q x y z)
(=° (cons y z) x)
(≠° (cons 5 6) x)
(=° 6 y)
(=° (list x y z) q))))
(⊦= '((λ (α β γ)
(begin (deny (equal? α 5)))
(begin (deny (equal? α 6)))
(begin (deny (and (equal? β 2) (equal? γ 1))))
(cons α (cons β (cons γ '())))))
(°->list
#f
(fresh°
(q x y z)
(≠° 5 x)
(≠° 6 x)
(≠° (list y 1) (list 2 z))
(=° (list x y z) q))))
(⊦= '((λ (α) (begin (deny (equal? α 1))) α))
(°->list #f (fresh° (s) (≠° s 1))))
(⊦= '() (°->list #f (fresh° (s) (≠° s 1) (=° s 1))))
(⊦= '((λ (α) (begin (deny (equal? α (cons 'a (cons 'b '()))))) α))
(°->list #f (fresh° (s) (≠° s '(a b)))))
(⊦= '((λ (α β)
(begin (deny (and (equal? α 1) (equal? β 2))))
(cons α (cons β '()))))
(°->list #f (fresh° (q p r) (≠° (list p r) '(1 2)) (=° q (list p r)))))
(⊦= '((λ (α) (begin (deny (equal? α 2))) (cons 1 (cons α '()))))
(°->list
#f
(fresh° (q p r) (≠° (list p r) '(1 2)) (=° p 1) (=° q (list p r)))))
(⊦= '()
(°->list
#f
(fresh°
(q p r)
(≠° (list p r) '(1 2))
(=° p 1)
(=° r 2)
(=° q (list p r))))))
((eta 0.001) (memory #(50331648 4405224 1048576)) (stdout "") (stderr ""))
test/rember°/naive: pass
(define (test/rember°/naive _)
(define-relation
(rember° x ls out)
(cond° ((=° '() ls) (=° '() out))
((fresh° (a d) (=° `(,a unquote d) ls) (=° a x) (=° d out)))
((fresh°
(a d res)
(=° `(,a unquote d) ls)
(=° `(,a unquote res) out)
(rember° x d res)))))
(⊦= '((a c b d)) (μkanren-run (q 1 #t) (rember° 'b '(a b c b d) q)))
(⊦= '((a b c)) (μkanren-run (q 1 #t) (rember° 'd '(a b c) q)))
(⊦= '((a c b d) (a b c d) (a b c b d))
(μkanren-run (q -1 #t) (rember° 'b '(a b c b d) q)))
(⊦= '(α) (μkanren-run (q -1 #t) (rember° 'b '(b) '(b)))))
((eta 0.001) (memory #(50331648 4405832 1048576)) (stdout "") (stderr ""))
test/rember°/fixed: pass
(define (test/rember°/fixed _)
(define-relation
(rember° x ls out)
(cond° ((=° '() ls) (=° '() out))
((fresh° (a d) (=° `(,a unquote d) ls) (=° a x) (=° d out)))
((fresh°
(a d res)
(=° `(,a unquote d) ls)
(≠° a x)
(=° `(,a unquote res) out)
(rember° x d res)))))
(⊦= '((a c b d)) (μkanren-run (q -1 #t) (rember° 'b '(a b c b d) q)))
(⊦= '() (μkanren-run (q -1 #t) (rember° 'b '(b) '(b))))
(⊦= '((λ () (cons 'a (cons (cons 'b (cons 'c '())) '())))
(λ () (cons 'b (cons (cons 'a (cons 'c '())) '())))
(λ () (cons 'c (cons (cons 'a (cons 'b '())) '())))
(λ (α)
(begin (deny (equal? α 'a)))
(begin (deny (equal? α 'b)))
(begin (deny (equal? α 'c)))
(cons α (cons (cons 'a (cons 'b (cons 'c '()))) '()))))
(°->list
#f
(fresh° (q x out) (rember° x '(a b c) out) (=° (list x out) q)))))
((eta 0.001) (memory #(50331648 4413872 1048576)) (stdout "") (stderr ""))
test/absent°: pass
(define (test/absent° _)
(⊦= '((λ (α β)
(assert (absent? 'panda α))
(assert (absent? 'panda β))
(cons 'jackal (cons (cons α (cons 'leopard (cons β '()))) '()))))
(°->list
#f
(fresh° (q x y) (=° `(jackal (,y leopard ,x)) q) (absent° 'panda q)))))
((eta 0.0) (memory #(50331648 4411408 1048576)) (stdout "") (stderr ""))