MiniKanren语言入门

综述

miniKanren语言脱胎于Kanren语言，最初嵌入scheme语言之中，后来又出现了许多其他宿主语言的实现。miniKanren语言的设计哲学是为其他语言提供嵌入式的、方便的逻辑式语言，并因为简单而适用于教学。它易于理解，并易于修改以支持各种扩展。

预备概念

1. 逻辑变量 logic variable 需要求解或引进的未知元
2. 替换 substitution 变量到其值的映射
3. 出现检查 occur check 检查变量对应的值中是否包含自身
4. 目标 goal 替换到流的映射
5. 流 stream 一种延时数据结构
6. 关系 relation 生成目标的函数
7. 合一 unification 根据替换进行匹配，返回新的替换的函数
8. 具体化 reification 根据替换将变量转换为具体值

具体实现

(define (var) (vector #f))
(define var? vector?)
(define (walk v s)
  (let ((a (and (var? v) (assv v s))))
    (if a (walk (cdr a) s) v)))
(define (occurs? x v s)
  (let ((v (walk v s)))
    (cond ((var? v) (eqv? x v))
          ((pair? v) (or (occurs? x (car v) s)
                         (occurs? x (cdr v) s)))
          (else #f))))
(define (ext-s x v s)
  (if (occurs? x v s) #f (cons (cons x v) s)))
(define (unify u v s)
  (let ((u (walk u s)) (v (walk v s)))
    (cond ((eqv? u v) s)
          ((var? u) (if (var? v)
                        (cons (cons u v) s)
                        (ext-s u v s)))
          ((var? v) (ext-s 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))))
(define (succeed s) (list s))
(define (fail s) '())
(define (== u v)
  (lambda (s)
    (let ((s (unify u v s)))
      (if s (list s) '()))))
(define (take n $)
  (cond ((null? $) '())
        ((= n 0) '())
        ((pair? $) (cons (car $) (take (- n 1) (cdr $))))
        (else (take n ($)))))
(define (disj2 g1 g2)
  (lambda (s)
    (mix (g1 s) (g2 s))))
(define (mix $1 $2)
  (cond ((null? $1) $2)
        ((pair? $1) (cons (car $1) (mix (cdr $1) $2)))
        (else (lambda () (mix $2 ($1))))))
(define (conj2 g1 g2)
  (lambda (s)
    (mix-map g2 (g1 s))))
(define (mix-map g $)
  (cond ((null? $) '())
        ((pair? $) (mix (g (car $)) (mix-map g (cdr $))))
        (else (mix-map g ($)))))
(define-syntax disj
  (syntax-rules ()
    ((_) fail)
    ((_ g) g)
    ((_ g0 g1 ...)
     (disj2 g0
            (lambda (s) (lambda () ((disj g1 ...) s)))))))
(define-syntax conj
  (syntax-rules ()
    ((_) succeed)
    ((_ g) g)
    ((_ g0 g1 ...) (conj2 g0 (conj g1 ...)))))
(define-syntax fresh
  (syntax-rules ()
    ((_ (x ...) g ...)
     (let ((x (var)) ...) (conj g ...)))))
(define (reify-name n)
  (string->symbol
   (string-append "_." (number->string n))))
(define (reify v)
  (lambda (s)
    (let ((v (walk* v s)))
      (walk* v (reify-s v '())))))
(define (walk* v d)
  (let ((v (walk v d)))
    (if (pair? v)
        (cons (walk* (car v) d)
              (walk* (cdr v) d))
        v)))
(define (reify-s v r)
  (let ((v (walk v r)))
    (cond ((var? v)
           (let ((rn (reify-name (length r))))
             (cons (cons v rn) r)))
          ((pair? v)
           (reify-s (cdr v)
                    (reify-s (car v) r)))
          (else r))))
(define-syntax run
  (syntax-rules ()
    ((_ n (x ...) g ...)
     (let ((x (var)) ...)
       (map (reify `(,x ...))
            (take n ((conj g ...) '())))))))
(define-syntax conde
  (syntax-rules ()
    ((_ (g ...) ...)
     (disj (conj g ...) ...))))
(define (take-all $)
  (cond ((null? $) '())
        ((pair? $) (cons (car $) (take-all (cdr $))))
        (else (take-all ($)))))
(define-syntax run*
  (syntax-rules ()
    ((_ (x ...) g ...)
     (let ((x (var)) ...)
       (map (reify `(,x ...))
            (take-all ((conj g ...) '())))))))