02 Connection with Logic Programming (cf. SICP 4.4)

Note: This is a bonus section! If you don't understand Lisp and don't care about SICP ch4-4 it might be greek.

In this notes section, my goal is to understand automatic proof discovery and certificate generation using the logic programming of SICP ch4-4.

This is not as exciting as it sounds, SICP ch4-4 is really about expanding your consciousness to think about what you can do with computer languages and architectures. It's not about making some super sophisticated superpowered algorithm that churns out proofs. But there are some analogies and correspondences that I want to understand, namely (using Metamath ch2 as an example problem)...

In the query system, without changing the code, how do we encode the axioms so we can simply do a query for '(|- t = t)?
As statements grow larger, what's the algorithmic complexity for searching for such a statement?
In parsing a Metamath proof, I'm told that the unification algorithm used is much simpler than that in SICP 4-4. In doing our "automated proof discovery", do we use the full power of the SICP 4-4 unification algorithm?
Is there a way to write our query such that the SICP ch4-4 code basically just does the straightforward parsing of a metamath proof?

Next, modifying the code...

Once the query system has found (|- t = t), how can we get it to print out the Metamath proof?
How do we turn the algorithm on its head, and enumerate valid axioms? Do we just add in a maximum stack size of something and search for (|- . ?x)?

And finally... - How do we implement a metamath kernel in Lean?

Reviewing SICP 4-4

Remembering how streams work

sicp44-1.rkt(click to expand)

#lang sicp

(define (stream-car stream) (car stream))
(define (stream-cdr stream) (force (cdr stream)))
(define (singleton-stream x)
        (cons-stream x the-empty-stream))

(define (integers-starting-from n) (cons-stream n (integers-starting-from (+ n 1))))
(define (stream-ref s n) 
        (if (<= n 0)
            (stream-car s)
            (stream-ref (stream-cdr s) (- n 1))))


(define (stream-map proc s)
  (if (stream-null? s)
      the-empty-stream
      (cons-stream (proc (stream-car s))
                   (stream-map proc (stream-cdr s)))))

(define (stream-filter pred s)
  (cond ((stream-null? s) the-empty-stream)
        ((pred (stream-car s))
         (cons-stream (stream-car s)
                      (stream-filter pred (stream-cdr s))))
        (else
         (stream-filter pred (stream-cdr s)))))

(define integers (integers-starting-from 1))

(stream-ref integers 9)
;; 10

(stream-ref
 (stream-map (lambda (x) (* x x)) integers)
 4)
;; 25

(stream-ref (stream-filter even? integers) 4)
;; 10

(stream-null?
 (stream-cdr
  (stream-map (lambda (x) (* x x))
              (singleton-stream 3))))
;; #t

(stream-null?
 (stream-filter even? (singleton-stream 3)))
;; #t

Output:

10
25
10
#t
#t

Remembering how frames work

sicp44-2.rkt(click to expand)

#lang sicp

(define (stream-car stream) (car stream))
(define (stream-cdr stream) (force (cdr stream)))
(define (singleton-stream x)
        (cons-stream x the-empty-stream))
(define (stream-map proc s)
  (if (stream-null? s)
      the-empty-stream
      (cons-stream (proc (stream-car s))
                   (stream-map proc (stream-cdr s)))))
(define (stream-ref s n) 
        (if (<= n 0)
            (stream-car s)
            (stream-ref (stream-cdr s) (- n 1))))

(define (make-binding variable value)
  (cons variable value))

(define (binding-variable binding) (car binding))
(define (binding-value binding) (cdr binding))

(define (binding-in-frame variable frame)
  (assoc variable frame))

(define (extend variable value frame)
  (cons (make-binding variable value) frame))

(define (tagged-list? exp tag)
  (if (pair? exp) (eq? (car exp) tag) false))

(define (var? exp)
  (tagged-list? exp '?))

(define (err-on-unbound variable frame)
  (display "Variable ")
  (display variable)
  (display " is unbound in frame ")
  (display frame)
  (display "\n")
  false)


(define frame
  (extend '(? x) '(? y)
          (extend '(? y) '(a b) '())))

(binding-in-frame '(? y) frame)
;; ((? y) a b)

; Apply the substitutions in "frame" to "expression". This is a bit like
; the Mathematica "ReplaceRepeated" or "//." operation.
(define (instantiate exp frame unbound-var-handler)
  (cond ((var? exp) 
         (let ((res (assoc exp frame)))
              (if res 
                (instantiate (cdr res) frame unbound-var-handler)
                (unbound-var-handler exp frame))))
        ((pair? exp) 
         (cons 
           (instantiate (car exp) frame unbound-var-handler)
           (instantiate (cdr exp) frame unbound-var-handler)))
         (else exp)))

(instantiate '(p (? x) (? missing))
             frame
             (lambda (v f) v))
;; (p (a b) (? missing))


(define frames
  (cons-stream frame
               (singleton-stream
                (extend '(? x) 'c '()))))

(define answers
  (stream-map
   (lambda (f)
     (instantiate '(p (? x)) f (lambda (v f) v)))
   frames))

(list (stream-ref answers 0)
      (stream-ref answers 1))
;; ((p (a b)) (p c))

Output:

((? y) a b)
(p (a b) (? missing))
((p (a b)) (p c))

Remembering the pattern match algo

sicp44-3.rkt(click to expand)

#lang sicp

(define (stream-car stream) (car stream))
(define (stream-cdr stream) (force (cdr stream)))
(define (singleton-stream x)
        (cons-stream x the-empty-stream))
(define (stream-map proc s)
  (if (stream-null? s)
      the-empty-stream
      (cons-stream (proc (stream-car s))
                   (stream-map proc (stream-cdr s)))))
(define (stream-ref s n) 
        (if (<= n 0)
            (stream-car s)
            (stream-ref (stream-cdr s) (- n 1))))

(define (make-binding variable value)
  (cons variable value))
(define (binding-variable binding) (car binding))
(define (binding-value binding) (cdr binding))
(define (binding-in-frame variable frame)
  (assoc variable frame))
(define (extend variable value frame)
  (cons (make-binding variable value) frame))
(define (tagged-list? exp tag)
  (if (pair? exp) (eq? (car exp) tag) false))
(define (var? exp)
  (tagged-list? exp '?))

; Apply the substitutions in "frame" to "expression". This is a bit like
; the Mathematica "ReplaceRepeated" or "//." operation.
(define (instantiate exp frame unbound-var-handler)
  (cond ((var? exp) 
         (let ((res (assoc exp frame)))
              (if res 
                (instantiate (cdr res) frame unbound-var-handler)
                (unbound-var-handler exp frame))))
        ((pair? exp) 
         (cons 
           (instantiate (car exp) frame unbound-var-handler)
           (instantiate (cdr exp) frame unbound-var-handler)))
         (else exp)))

(define (extend-if-consistent var dat frame)
  (let ((l (assoc var frame)))
       (if l 
         ; If it's defined, the data has to be consistent with the matched variable
         (pattern-match dat (cdr l) frame)
         ; Else, var is free for us to define.
         (extend var dat frame))))
(define (pattern-match pat dat frame)
  (cond ((var? pat) (extend-if-consistent pat dat frame))
        ((and (pair? pat) (pair? dat)) 
          (let ((nf (pattern-match (car pat) (car dat) frame)))
               (if (eq? nf 'failed) 
                   'failed
                   (pattern-match (cdr pat) (cdr dat) nf))))
        ((eq? pat dat) frame)
        (else 'failed)))



(pattern-match '(p (? x) (? x))
               '(p a a)
               '())
;; (((? x) . a))

(pattern-match '(p (? x) (? x))
               '(p a b)
               '())
;; failed

(pattern-match '(a . (? rest))
               '(a b c)
               '())
;; (((? rest) b c))

Output:

(((? x) . a))
failed
(((? rest) b c))

Remembering the unification algo

sicp44-4.rkt(click to expand)

#lang sicp

(define (stream-car stream) (car stream))
(define (stream-cdr stream) (force (cdr stream)))
(define (singleton-stream x)
        (cons-stream x the-empty-stream))
(define (stream-map proc s)
  (if (stream-null? s)
      the-empty-stream
      (cons-stream (proc (stream-car s))
                   (stream-map proc (stream-cdr s)))))
(define (stream-ref s n) 
        (if (<= n 0)
            (stream-car s)
            (stream-ref (stream-cdr s) (- n 1))))

(define (make-binding variable value)
  (cons variable value))
(define (binding-variable binding) (car binding))
(define (binding-value binding) (cdr binding))
(define (binding-in-frame variable frame)
  (assoc variable frame))
(define (extend variable value frame)
  (cons (make-binding variable value) frame))
(define (tagged-list? exp tag)
  (if (pair? exp) (eq? (car exp) tag) false))
(define (var? exp)
  (tagged-list? exp '?))

; Apply the substitutions in "frame" to "expression". This is a bit like
; the Mathematica "ReplaceRepeated" or "//." operation.
(define (instantiate exp frame unbound-var-handler)
  (cond ((var? exp) 
         (let ((res (assoc exp frame)))
              (if res 
                (instantiate (cdr res) frame unbound-var-handler)
                (unbound-var-handler exp frame))))
        ((pair? exp) 
         (cons 
           (instantiate (car exp) frame unbound-var-handler)
           (instantiate (cdr exp) frame unbound-var-handler)))
         (else exp)))

(define (extend-if-consistent var dat frame)
  (let ((l (assoc var frame)))
       (if l 
         ; If it's defined, the data has to be consistent with the matched variable
         (pattern-match (cdr l) dat frame)
         ; Else, var is free for us to define.
         (extend var dat frame))))
(define (pattern-match pat dat frame)
  (cond ((eq? frame 'failed) 'failed)
        ((var? pat) (extend-if-consistent pat dat frame))
        ((and (pair? pat) (pair? dat)) 
          (let ((nf (pattern-match (car pat) (car dat) frame)))
               (if (eq? nf 'failed) 
                   'failed
                   (pattern-match (cdr pat) (cdr dat) nf))))
        ((equal? pat dat) frame)
        (else 'failed)))


(define (extend-if-possible var val frame)
  (let ((existing (binding-in-frame var frame)))
    (cond
      (existing
       (unify-match (binding-value existing) val frame))

      ((var? val)
       (let ((other (binding-in-frame val frame)))
         (if other
             (unify-match var (binding-value other) frame)
             (extend var val frame))))

      ((depends-on? val var frame)
       'failed)

      (else
       (extend var val frame)))))
(define (unify-match p1 p2 frame)
  (cond ((eq? frame 'failed) 'failed)
    ((equal? p1 p2) frame)
    ((var? p1) (extend-if-possible p1 p2 frame))
    ((var? p2) (extend-if-possible p2 p1 frame))
    ((and (pair? p1) (pair? p2))
     (unify-match
       (cdr p1)
       (cdr p2)
       (unify-match (car p1) (car p2) frame)))
    (else 'failed)))

(define (depends-on? exp var frame)
  (cond
    ((var? exp)
     (or (equal? exp var)
         (let ((binding (binding-in-frame exp frame)))
           (and binding
                (depends-on?
                  (binding-value binding)
                  var
                  frame)))))
    ((pair? exp)
     (or (depends-on? (car exp) var frame)
         (depends-on? (cdr exp) var frame)))
    (else false)))

(unify-match '(p (? x) (? y))
             '(p (? y) (? x))
             '())
;; (((? x) ? y))
(define unified
  (unify-match '(p (? x) (? y))
               '(p (f (? y)) 3)
               '()))

(instantiate '(? x) unified (lambda (v f) v))
;; (f 3)
(unify-match '(? y)
             '(f (? x))
             (extend '(? x) '(? y) '()))
;; failed

Output:

(((? x) ? y))
(f 3)
failed