163 lines
3.9 KiB
Scheme
163 lines
3.9 KiB
Scheme
;; okay, i'll keep these procedures for the sake of nesting
|
|
|
|
(define (make-pand p q) `(and ,p ,q))
|
|
|
|
(define pand
|
|
(case-lambda
|
|
[() #t]
|
|
[(p) p]
|
|
[(p . qs) (fold-left make-pand p qs)]))
|
|
|
|
(define (make-por p q) `(or ,p ,q))
|
|
|
|
(define por
|
|
(case-lambda
|
|
[() #f]
|
|
[(p) p]
|
|
[(p . qs) (fold-left make-por p qs)]))
|
|
|
|
;; iirc, or: (not p) or q
|
|
(define (make-p-> p q) `(-> ,p ,q))
|
|
|
|
;; could fold but laziness
|
|
(define p->
|
|
(case-lambda
|
|
[() #t]
|
|
[(p) p]
|
|
[(p . qs) (make-p-> p (apply p-> qs))]))
|
|
|
|
(define (p<-> p q) (pand (p-> p q) (p-> q p)))
|
|
;; maybe could have some pretty-printing logic? this definition is just 2 good 2 pass up
|
|
(define (pnot p) (p-> p #f))
|
|
(define ~ pnot)
|
|
|
|
;; maybe a var is just a sym? no forall lel
|
|
;; existence l8r
|
|
;; nah
|
|
;; valued vars? :o
|
|
|
|
;; (define-record-type forall
|
|
;; (fields vars p)
|
|
;; (nongenerative forall))
|
|
;; (define-syntax forall
|
|
;; (syntax-rules ()
|
|
;; [(forall (var* ...) p)
|
|
;; (make-forall
|
|
;; '(var* ...)
|
|
;; (let ([var* 'var*] ...) p))]
|
|
;; [(forall var p) (forall (var) p)]))
|
|
|
|
(define-record-type argument
|
|
(fields premises conclusions)
|
|
(nongenerative argument))
|
|
|
|
(define-syntax argument
|
|
(syntax-rules ()
|
|
[(_ (var* ...) (premise* ...) (conclusion* ...))
|
|
(lambda (var* ...)
|
|
(make-argument (list premise* ...) (list conclusion* ...)))]))
|
|
|
|
(define modus-ponens
|
|
(argument (p q)
|
|
[(p-> p q)
|
|
p]
|
|
[q]))
|
|
|
|
(define modus-tollens
|
|
(argument (p q)
|
|
[(p-> p q)
|
|
(~ q)]
|
|
[(~ p)]))
|
|
|
|
;; YES: multiple conclusions (no more simplification-{l,r})
|
|
(define simplification
|
|
(argument (p q)
|
|
[(pand p q)]
|
|
[p q]))
|
|
|
|
(define conjunction
|
|
(argument (p q)
|
|
[p
|
|
q]
|
|
[(pand p q)]))
|
|
|
|
;; (follows (P* ... (-> p q) p Q* ...) q modus-ponens) => #t
|
|
;; iterative argument
|
|
;; laws of inference are taken as fact
|
|
;; norm vars
|
|
;; order irrelevant
|
|
;; search for reqs?
|
|
|
|
(define (premises<=? p1 p2)
|
|
(and (andmap (lambda (prem) (member prem p2)) p1)
|
|
#t))
|
|
|
|
(define (follows? prems q by)
|
|
(and (member q (argument-conclusions by))
|
|
(premises<=? (argument-premises by) prems)))
|
|
|
|
(define-record-type step
|
|
(fields conclusion rule)
|
|
(nongenerative step))
|
|
|
|
(define-record-type proof
|
|
(fields argument steps)
|
|
(nongenerative proof))
|
|
|
|
(define-syntax proof
|
|
(syntax-rules ()
|
|
[(_ (var* ...) arg (conclusion* rule*) ...)
|
|
(lambda (var* ...)
|
|
(make-proof (arg var* ...)
|
|
(list (make-step conclusion* rule*) ...)))]))
|
|
|
|
;; bleh
|
|
;; huh, procedure-arity-mask can handle 1000+ no problem
|
|
;; returns the lowest arity
|
|
(define (procedure-arity proc)
|
|
(define mask (procedure-arity-mask proc))
|
|
(let loop ([i 0])
|
|
(if (logbit? i mask)
|
|
i
|
|
(loop (add1 i)))))
|
|
|
|
(define (proof-valid? proof%)
|
|
(define (gensyms n xs)
|
|
(if (zero? n)
|
|
;; less confusing to apply (proof g0 g1 ...)
|
|
(reverse xs)
|
|
(gensyms (sub1 n) (cons (gensym) xs))))
|
|
(define proof (apply proof% (gensyms (procedure-arity proof%) '())))
|
|
(define arg (proof-argument proof))
|
|
;; reversing here lets us recover a nice order at the end
|
|
(define prems (reverse (argument-premises arg)))
|
|
(define goals (argument-conclusions arg))
|
|
|
|
(call/1cc
|
|
(lambda (return)
|
|
(for-each
|
|
(lambda (step)
|
|
(let ([concl (step-conclusion step)]
|
|
[rule (step-rule step)])
|
|
(unless (follows? prems concl rule)
|
|
(format #t "fool, ~a does not follow from ~a and ~a!\n"
|
|
concl (reverse prems) rule)
|
|
(return #f))
|
|
(set! prems (cons concl prems))))
|
|
(proof-steps proof))
|
|
(when (premises<=? goals prems)
|
|
(return #t))
|
|
(format #t "forgetting something? you're trying to prove ~a, but you've only got ~a\n"
|
|
goals prems))))
|
|
|
|
;; TODO: i can just guess lol
|
|
(define and-comm
|
|
(proof (p q)
|
|
(argument (p q)
|
|
[(pand p q)]
|
|
[(pand q p)])
|
|
[p (simplification p q)]
|
|
[q (simplification p q)]
|
|
[(pand q p) (conjunction q p)]))
|
|
|