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

prolog

Conformance: R5RS

Purpose: A simple PROLOG interpreter.
 
This program is based on another tiny PROLOG interpreter in MACLISP written by Ken Kahn.
 
If the *print* variable is set to #f this interpreter is completely free of side effects, and the PROLOG function returns its query results in a list.

Arguments:
Q - query
DB - database

Implementation:

(define *print* #t)

(define (prolog q db)
  (letrec

  ((symbol-p (lambda (x)
    (cond ((null? x) #t)
      (#t (symbol? x)))))

  ; Is X a variable?
  ; Variables are lists beginning with '?
  (variable? (lambda (x)
    (cond ((symbol-p x) #f)
      (#t (eq? (car x) '?)))))

  ; Create an environment of unique names by
  ; appending ID to each variable.
  (newscope (lambda (x id)
    (letrec
      ((nsc (lambda (x)
        (cond ((symbol-p x) x)
          ((variable? x) (append x id))
          (#t (cons (nsc (car x)) (nsc (cdr x))))))))
      (nsc x))))

  ; Increment ID.
  (nextid (lambda (x)
    (list (cons 'i (car x)))))

  ; Find the value of a variable in a given environment.
  (value (lambda (x env)
    (cond ((variable? x)
        (let ((b (assoc x env)))
          ; If the variable is not bound, return its name
          (cond ((not b) x)
            ; else return the value of its value
            ; (variables may be bound to variables).
            (#t (value (cdr b) env)))))
      ; Pass thru non-variables.
      (#t x))))

  ; Unify two expressions X and Y in a given environment.
  ; If X and Y can be unified, return a new environment in
  ; which the variables of X and Y are bound.
  ; If the unification fails, return '().
  (unify (lambda (x y env)
    ; First retrieve the values of the expressions.
    (let ((x (value x env))
          (y (value y env)))
      (cond
        ; Variables are unified by binding them to
        ; the other expression.
        ((variable? x) (cons (cons x y) env))
        ((variable? y) (cons (cons y x) env))
        ; Only identical atoms can be unified.
        ((symbol-p x) (cond ((eq? x y) env) (#t '())))
        ((symbol-p y) (cond ((eq? x y) env) (#t '())))
        ; Rules are unified by unifying their heads,
        ; giving a new environment.
        ; If the new environment is non-(), the rest
        ; of the rules is unified in the new environment.
        (#t (let ((newenv (unify (car x) (car y) env)))
              (cond
                ; Heads could not be unified.
                ((null? newenv) '())
                (#t (unify (cdr x) (cdr y) newenv)))))))))

  ; Attempt to unify each goal with each rule.
  ; RULES  = list of rules (database)
  ; GOALS  = conjunction of goals
  ; ENV    = environment to unify in
  ; ID     = scope ID
  ; RESULT = list of results so far
  (tryrules (lambda (rules goals env id result)
    (cond ((null? rules)
            result)  ; Out of rules: return result.
      (#t (let
            ; Create new scope for the current rule
            ((thisrule (newscope (car rules) id)))
            ; and attempt to unify the current goal with the
            ; head of this rule.
            (let ((newenv (unify (car goals)
                                 (car thisrule)
                                 env)))
              (cond ((null? newenv)
                  ; Unification failed, try next rule.
                  (tryrules (cdr rules) goals env id result))
                ; Unification succeeded, prove union
                ; of rest of this rule and remainder
                ; of goals in NEWENV.
                (#t (let ((res (prove
                                 (append (cdr thisrule)
                                         (cdr goals))
                                 newenv (nextid id))))
                  ; Add the result of above proof to the
                  ; result list and advance to the next rule.
                  (tryrules (cdr rules) goals env id
                    (append result res)))))))))))

  ; Pretty-print results if *print* = #t
  (print (lambda (x)
    (cond (*print*
        (begin
          (display x)
          (newline)
          x))
      (#t x))))

  ; Create an N-tuple of bindings
  ; ( (VAR-1 = VALUE-1) ... (VAR-N = VALUE-N) ).
  ; Each binding is prepresented by
  ; (VAR = VALUE),
  ; where VAR is the name and VALUE is the value
  ; of a variable bound in the outermost scope
  ; (the scope of the query).
  ; N is the number of variables in the query.
  (listenv (lambda (env)
    (letrec
      ((lse (lambda (e res)
        (cond ((null? (cdr e)) (list (print res)))
          ; Variables of the outer scope have ID=()
          ((null? (caddr (caar e))) ; ID=()?
            ; Move to next variable
            (lse (cdr e)
              ; adding a new binding to the result list
              (cons (list (cadr (caar e))
                          '= (value (caar e) env))
                    res)))
          ; Inner scope, skip
          (#t (lse (cdr e) res))))))
      (lse env '()))))

  ; Prove a list of goals in a given environment.
  ; GOALS = list of goals
  ; ENV   = environment
  ; ID    = scope ID, see NEWSCOPE above
  (prove (lambda (goals env id)
    (cond ((null? goals) (listenv env)) 
      (#t (tryrules db goals env id '()))))))

  ; '((())) is the initial environment. It looks like
  ; this because '(()) would indicate failure in UNIFY.
  (prove (list (newscope q '(()))) '((())) '((i)))))

; This is a utility function to submit queries to
; a predefined database bound to DATABASE.
; The result is discarded.
; QUERY requires *PRINT* = #T.
(define (query q)
  (let ((result (prolog q database)))
    (cond ((equal? result '(())) 'yes)
      (#t 'no))))

Example:

:load prolog.db
; Sample queries:
; whose father is Anthony?
  (query '(father anthony (? child)))
; who are Eric's parents?
  (query '(parent (? parent) eric))
; list descendants of Bertram.
  (query '(descendant (? descendant) bertram))
; who is who's wife?
  (query '(wife (? wife) (? husband)))
; which relations does Cathy have?
  (query '((? relation) cathy (? person)))