~ashton314/microKanren

668fe5d9f75f0af49c3041827bbd284be24b0827 — Ashton Wiersdorf 6 months ago 9bf4bc1
Add predicate checking
3 files changed, 31 insertions(+), 0 deletions(-)

M README.org
M kanren.rkt
M relations_playground.rkt
M README.org => README.org +21 -0
@@ 107,6 107,27 @@ These are some syntactic sugar that make working with μKanren nicer. Most of th

I deviated from the paper's implementation of variables and wrote them as structs instead of vectors. I think further changes could be made (e.g. not having to keep around a number in the state to generate fresh variable names but these might rely on some more language-specific features. (E.g. generating fresh strings/symbols.)

** Predicates in ~unify~

I've added some rudimentary predicate checking to the ~unify~ function:

#+begin_src racket
(define (fav-num n)
  (disj (== n 42)
        (== (cons '? even?) n)))
#+end_src

#+begin_src racket
> (run* (n) (== n 12) (fav-num n))
'(12)

> (run* (n) (== n 13) (fav-num n))
'()

> (run* (n) (fav-num n))
'(42 (? . #<procedure:even?>))
#+end_src

* Author

I hope is /very clear/ that /I/ did /not/ write the μKanren paper. That would be Daniel P. Friedman and Jason Hemann. I merely wrote up this annotation.

M kanren.rkt => kanren.rkt +5 -0
@@ 68,6 68,11 @@
       (extend-subst u v subst)]
      [(var? v)
       (extend-subst v u subst)]
      ;; predicates
      [(and (pair? u) (eq? (car u) '?))
       (and ((cdr u) v) subst)]
      [(and (pair? v) (eq? (car v) '?))
       (and ((cdr v) u) subst)]
      ;; unify structures: walk down lists
      [(and (pair? u) (pair? v))
       (let ([subst₁ (unify (car u) (car v) subst)])

M relations_playground.rkt => relations_playground.rkt +5 -0
@@ 21,3 21,8 @@
(define (grandparent g s)
  (fresh (p) (parent g p) (parent p s)))

;; (run 20 (rel p c) (conj+ (grandparent c p) (== (cons c p) rel)))

(define (fav-num n)
  (disj (== n 42)
        (== (cons '? even?) n)))