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 ...) '())))))))