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.
Tests
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.005) (memory #(12582912 2120344 1048576)) (stdout "") (stderr ""))
test/=°: pass
(define (test/=° _) (⊦= '(α) (°->list/ground (=° 'z 'z))))
((eta 0.014) (memory #(12582912 2121488 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.007) (memory #(12582912 2127656 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.013) (memory #(12582912 2139224 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 2136080 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.002) (memory #(12582912 2129616 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.002) (memory #(12582912 2129608 1048576)) (stdout "") (stderr ""))