t3x.org / sketchy / prog / amk.html
SketchyLISP Stuff Copyright (C) 2007 Nils M Holm

Another Micro KANREN

Language: R5RS Scheme

Purpose: This is a small subset of the KANREN logic programming system, which embeds logic programming idioms into Scheme programs.
 
This implementation has been inspired by
"The Reason Schemer" by Daniel P. Friedman, et al
and by "Sokuza Mini-KANREN" by Oleg Kiselyov.
 
AMK is discussed in "Logic Programming in Scheme"
http://www.lulu.com/content/659829

Implementation:

(define amk #t)  ; for require

; ===== core ==========================================

(define (fail x)
  '())

(define (succeed x)
  (list x))

(define failed? null?)

(define (var x)
  (cons '? x))

(define (var? x)
  (and (pair? x)
       (eq? (car x) '?)))

(define empty-s '())

(define _BOTTOM_ (var 'bottom))

(define (atom? x)
  (not (pair? x)))

(define (ext-s x v s)
  (cons (cons x v) s))

(define (walk x s)
  (cond ((not (var? x)) x)
    (else (let ((v (assq x s)))
            (if v (walk (cdr v) s)
                  x)))))

(define (unify x y s)
  (let ((x (walk x s))
        (y (walk y s)))
    (cond
      ((eqv? x y) s)
      ((var? x) (ext-s x y s))
      ((var? y) (ext-s y x s))
      ((or (atom? x) (atom? y)) #f)
      (else (let ((s (unify (car x) (car y) s)))
              (and s (unify (cdr x) (cdr y) s)))))))

(define (== x y)
  (lambda (s)
    (let ((s2 (unify x y s)))
      (if s2 (succeed s2)
             (fail s)))))

(define (any* . g*)
  (lambda (s)
    (letrec
      ((try
         (lambda g*
           (cond ((null? g*) (fail s))
             (else (append ((car g*) s)
                           (apply try (cdr g*))))))))
      (apply try g*))))

(define-syntax any
  (syntax-rules ()
    ((_) fail)
    ((_ g ...)
       (any* (lambda (s) (g s)) ...))))

(define (all . gs)
  (lambda (s)
    (letrec
      ((try
         (lambda (gs subs)
           (cond ((null? gs) subs)
             (else (try (cdr gs)
                        (apply append
                          (map (car gs) subs))))))))
      (try gs (succeed s)))))

(define (one* . gs)
  (lambda (s)
    (letrec
      ((try
         (lambda gs
           (cond ((null? gs) (fail s))
             (else (let ((out ((car gs) s)))
                     (cond ((failed? out)
                         (apply try (cdr gs)))
                       (else out))))))))
      (apply try gs))))

(define-syntax one
  (syntax-rules ()
    ((_) fail)
    ((_ g ...)
       (one* (lambda (s) (g s)) ...))))

(define (neg g)
  (lambda (s)
    (let ((out (g s)))
      (cond ((failed? out) (succeed s))
        (else (fail s))))))

(define-syntax fresh
  (syntax-rules ()
    ((_ () g)
       (let () g))
    ((_ (v ...) g)
       (let ((v (var 'v)) ...) g))))

(define (occurs? x y s)
  (let ((v (walk y s)))
    (cond
      ((var? y) (eq? x y))
      ((var? v) (eq? x v))
      ((atom? v) #f)
      (else (or (occurs? x (car v) s)
                (occurs? x (cdr v) s))))))

(define (circular? x s)
  (let ((v (walk x s)))
    (cond ((eq? x v) #f)
      (else (occurs? x (walk x s) s)))))

(define (walk* x s)
  (letrec
    ((w*
       (lambda (x s)
         (let ((x (walk x s)))
           (cond
             ((var? x) x)
             ((atom? x) x)
             (else (cons (w* (car x) s)
                         (w* (cdr x) s))))))))
    (cond ((circular? x s) _BOTTOM_)
      ((eq? x (walk x s)) empty-s)
      (else (w* x s)))))

(define (preserve-bottom s)
  (if (occurs? _BOTTOM_ s s) '() s))

(define (reify-name n)
  (string->symbol
    (string-append "_." (number->string n))))

(define (reify v)
  (letrec
    ((reify-s
       (lambda (v s)
         (let ((v (walk v s)))
           (cond ((var? v)
               (ext-s v (reify-name (length s)) s))
             ((atom? v) s)
             (else (reify-s (cdr v)
                     (reify-s (car v) s))))))))
    (reify-s v empty-s)))

(define (_) (var '_))

(define (run x g)
  (preserve-bottom
    (map (lambda (s)
           (walk* x (append s (reify (walk* x s)))))
         (g empty-s))))

(define-syntax run*
  (syntax-rules ()
    ((_ () goal) (run #f goal))
    ((_ (v) goal) (run v goal))))

; ===== tools =========================================

(define vp (var 'p))
(define vq (var 'q))
(define vr (var 'r))

(define (conso a d p)
  (== (cons a d) p))

(define (caro p a)
  (conso a (_) p))

(define (cdro p d)
  (conso (_) d p))

(define (pairo p)
  (conso (_) (_) p))

(define (eqo x y)
  (== x y))

(define (nullo a)
  (eqo a '()))

(define (memo x l)
  (fresh (a d)
    (any (all (caro l a)
              (eqo x a))
         (all (cdro l d)
              (memo x d)))))

(define (r-memo x l)
  (fresh (a d)
    (any (all (cdro l d)
              (r-memo x d))
         (all (caro l a)
              (eqo x a)))))

(define (reverseo l r)
  (r-memo r l))

(define (appendo x y r)
  (any (all (== x '()) (== y r))
       (fresh (vh vt va)
         (all (conso vh vt x)
              (conso vh va r)
              (appendo vt y va)))))

(define (membero x l r)
  (fresh (a d)
    (any (all (caro l a)
              (eqo x a) 
              (== r l))
         (all (cdro l d)
              (membero x d r)))))

(define (r-membero x l r)
  (fresh (a d)
    (any (all (cdro l d)
              (r-membero x d r))
         (all (caro l a)
              (eqo x a)
              (== r l)))))

Example:

(run* (vq) (appendo vq (_) '(a b c))) 
=> (() (a) (a b) (a b c))