git @ Cat's Eye Technologies define-opaque / master eg / a-small-logic.scm
master

Tree @master (Download .tar.gz)

a-small-logic.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
; SPDX-FileCopyrightText: In 2023, Chris Pressey, the original author 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 a-small-logic.scm

; A proof system based on the section 4 ("A Small Logic") in
; "Logic as Algebra" by Paul Halmos and Steven Givant, 1998
; ( https://archive.org/details/logicasalgebra0000halm ).
; It preserves the additive properties of parity.

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

(define get-at (lambda (pos sentence)
  (if (equal? pos 0)
    (car sentence)
    (get-at (- pos 1) (cdr sentence)))))

(define sub-at (lambda (pos phrase sentence)
  (if (equal? pos 0)
    (append phrase (cdr sentence))
    (cons (car sentence) (sub-at (- pos 1) phrase (cdr sentence))))))

(define-opaque theorem make-theorem (sentence) ('nil)
  (
    (refl (lambda (what)
      (if (or (equal? what 'even) (equal? what 'odd))
        (make-theorem (list what '= what))
        (error "Argument must be 'even or 'odd: " what))))
    (replace (lambda (pos lhs-what rhs-what)
      (let* ((that (get-at pos sentence)))
        (cond
          ((and (equal? that 'even)
                (or (and (equal? lhs-what 'odd) (equal? rhs-what 'odd))
                    (and (equal? lhs-what 'even) (equal? rhs-what 'even))))
            (make-theorem (sub-at pos (list lhs-what '+ rhs-what) sentence)))
          ((and (equal? that 'odd)
                (or (and (equal? lhs-what 'odd) (equal? rhs-what 'even))
                    (and (equal? lhs-what 'even) (equal? rhs-what 'odd))))
            (make-theorem (sub-at pos (list lhs-what '+ rhs-what) sentence)))
          (else
            (error "Cannot replace: " that 'with lhs-what '+ rhs-what))))))
    (repr (lambda ()
      sentence))
  )
)

(define demo (lambda ()
  (let* (
    (thm0 (theorem 'refl 'odd))
    (thm1 (thm0 'replace 0 'odd 'even))
    ;(thm2 (thm1 'replace 2 'odd 'even))  ; this will error!
    (thm2 (thm1 'replace 2 'odd 'odd))
  )
    (display (thm0 'repr)) (newline)
    (display (thm1 'repr)) (newline)
    (display (thm2 'repr)) (newline)
  )))

(demo)