git @ Cat's Eye Technologies define-opaque / master eg / hilbert-system.scm
master

Tree @master (Download .tar.gz)

hilbert-system.scm @master — raw · history · blame 

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
; SPDX-FileCopyrightText: In 2026, Chris Pressey, the creator of this work, placed it into the public domain.
; For more information, please refer to <https://unlicense.org/>
; SPDX-License-Identifier: Unlicense

; example usage with Chicken Scheme: csi -q -b hilbert-system.scm

(load "define-opaque-0.3.scm")

(define-opaque-adt theorem make-theorem open-theorem formula 'nil
  (
    (a1 (lambda (phi psi)
      (make-theorem (list '-> phi (list '-> psi phi)))))

    (a2 (lambda (phi psi chi)
      (make-theorem (list '->
        (list '-> phi (list '-> psi chi))
        (list '-> (list '-> phi psi) (list '-> phi chi))))))

    ; Modus ponens: from a proof of P and a proof of P->Q, derive a
    ; proof of Q.
    ;
    ; open-theorem verifies that thm-p and thm-impl are genuine theorems.
    ; Passing any non-theorem value here raises an error.
    (modus-ponens (lambda (thm-p thm-impl)
      (let* (
        (given-p    (open-theorem thm-p))
        (given-impl (open-theorem thm-impl))
      )
        (if (and (pair? given-impl)
                 (equal? (car given-impl) '->)
                 (equal? (cadr given-impl) given-p))
          (make-theorem (caddr given-impl))
          (error "Cannot apply modus ponens:" given-p given-impl)))))

    (repr (lambda () formula))
  )
)

(define demo (lambda ()
  ; Derive p -> p using only A1, A2, and modus ponens.
  (let* (
    ; t1: p -> (p -> p)         by A1(p, p)
    (t1 (theorem 'a1 'p 'p))
    ; t2: p -> ((p->p) -> p)    by A1(p, p->p)
    (t2 (theorem 'a1 'p '(-> p p)))
    ; t3: (p -> ((p->p) -> p)) -> ((p -> (p->p)) -> (p -> p))
    ;                            by A2(p, p->p, p)
    (t3 (theorem 'a2 'p '(-> p p) 'p))
    ; t4: (p -> (p->p)) -> (p -> p)   by MP(t2, t3)
    (t4 (theorem 'modus-ponens t2 t3))
    ; t5: p -> p                by MP(t1, t4)
    (t5 (theorem 'modus-ponens t1 t4))
  )
    (display "Derived theorem: ")
    (display (t5 'repr))
    (newline)
  )))

(demo)

; --------------------------------------------------------------------------

; Demonstration that other data structures are rejected (even in the case
; that they define the same operations - duck-typing would not reject this.)

(define-opaque-adt ersatz-theorem make-theorem open-theorem formula 'nil
  (
    (a1 (lambda (phi psi)
      (make-theorem (list '-> phi (list '-> psi phi)))))

    (a2 (lambda (phi psi chi)
      (make-theorem (list '->
        (list '-> phi (list '-> psi chi))
        (list '-> (list '-> phi psi) (list '-> phi chi))))))

    (modus-ponens (lambda (thm-p thm-impl)
      (let* (
        (given-p    (open-theorem thm-p))
        (given-impl (open-theorem thm-impl))
      )
        (if (and (pair? given-impl)
                 (equal? (car given-impl) '->)
                 (equal? (cadr given-impl) given-p))
          (make-theorem (caddr given-impl))
          (error "Cannot apply modus ponens:" given-p given-impl)))))
  )
)

(define errorful-demo (lambda ()
  (let* (
    (t1 (theorem 'a1 'p 'p))
    (t2 (theorem 'a1 'p '(-> p p)))
    (t3 (theorem 'a2 'p '(-> p p) 'p))
    (t4 (theorem 'modus-ponens t2 t3))
    (t5 (ersatz-theorem 'modus-ponens t1 t4))
  )
    (display "Derived theorem: ")
    (display (t5 'repr))
    (newline)
  )))