diff options
Diffstat (limited to 'vikalpa')
| -rw-r--r-- | vikalpa/prelude.scm | 353 |
1 files changed, 191 insertions, 162 deletions
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index d03df7e..1ee56af 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -27,10 +27,6 @@ (if x (implies y z rest ...) #t)))) (define-system prelude () - (define-primitive-function < (x y)) - (define-primitive-function natural? (x)) - (define-totality-claim natural? natural? <) - (define-syntax-rules list () ((list) '()) ((list x . y) (cons x (list . y)))) @@ -54,7 +50,18 @@ ((implies x y) (if x y #t)) ((implies x y z . rest) (if x (implies y z . rest) #t))) + + (define-function zero? (x) + (equal? 0 x)) + + (define-function natural? (x) + (and (integer? x) + (or (equal? x 0) + (< x 0)))) + + (define-totality-claim natural? natural? <) + (define-axiom equal-same (x) (equal? (equal? x x) '#t)) @@ -82,222 +89,244 @@ (equal? (if (not x) y z) (if x z y))) - (define-axiom pair-cons (x y) + (define-axiom pair/cons (x y) (equal? (pair? (cons x y)) '#t)) - (define-axiom car-cdr-elim (x) - (if (pair? x) - (equal? (cons (car x) (cdr x)) x) - '#t)) + (define-axiom cons/car+cdr (x) + (implies (pair? x) + (equal? (cons (car x) (cdr x)) x))) - (define-axiom car-cons (x y) + (define-axiom car/cons (x y) (equal? (car (cons x y)) x)) - (define-axiom cdr-cons (x y) + (define-axiom cdr/cons (x y) (equal? (cdr (cons x y)) y)) - - (define-axiom car-cdr-elim (x) - (implies (pair? x) - (equal? (cons (car x) (cdr x)) x))) - (define-axiom cons-equal-car (x1 y1 x2 y2) + (define-axiom equal-car (x1 y1 x2 y2) (implies (equal? (cons x1 y1) (cons x2 y2)) (equal? x1 x2))) - (define-axiom cons-equal-cdr (x1 y1 x2 y2) + (define-axiom equal-cdr (x1 y1 x2 y2) (implies (equal? (cons x1 y1) (cons x2 y2)) (equal? y1 y2))) - - #; - (define-axiom natural?/0 () - (equal? (natural? '0) '#t)) - #; - (define-theorem equal/zero-less-than (x) + (define-axiom pred/succ (x) (implies (natural? x) - (equal? (not (< '0 x)) - (equal? x '0)))) + (equal? (pred (succ x)) x))) + + (define-axiom succ/pred (x) + (implies (natural? x) + (not (zero? x)) + (equal? (succ (pred x)) x))) - #; - (define-proof equal/zero-less-than - (natural-induction x) - (((2 2) if-nest) - ((3) if-nest) - ((2 2 1) if-same (set x (natural? '0))) - ((2 2 1 2 1) axiom-less-than) - ((2 2 1 1) natural/zero) - ((2 2 1) if-true) - ((2 2 1 1 1) equal-same) - ((2 2 1 1) if-true) - ((2 2 1 1 1 2) equal-if) - ((2 2 1 1 1) equal-same) - ((2 2 1 1) if-true) - ((2 2 1) not/false) - ((2 2 2 1) equal-if) - ((2 2 2) equal-same) - ((2 2) equal-same) - ((2 3 2 2) if-same (set x (natural? '0))) - ((2 3 2 2 2 1 1) axiom-less-than) - ((2 3 2 2 2 1 1 1) equal-same) - ((2 3 2 2 2 1 1) if-true) - ((2 3 2 2 2 1 1) if-nest) - ((2 3 2 2 2 1) not/true) - ((2 3 2 2 2 2) equal-swap) - ((2 3 2 2 2 2) false-if) - ((2 3 2 2 2) equal-same) - ((2 3 2 2 1) natural/zero) - ((2 3 2 2) if-true) - ((2 3 2) if-same) - ((2 3) if-same) - ((2) if-same) - (() if-same))) + (define-theorem less-than/pred-1 (x) + (implies (not (zero? x)) + (natural? x) + (natural? (pred x)) + (not (zero? (pred x))) + (equal? (< (pred (pred x)) (pred x)) '#t) + (equal? + (if (zero? (pred x)) + '#t + (< (pred (pred x)) (pred x))) + '#t))) - ;; (define-axiom natural/sub1 (x) - ;; (implies (natural? x) - ;; (if (equal? '0 x) - ;; '#t - ;; (equal? (natural? (sub1 x)) #t)))) + (define-theorem if-implies (x y z w) + (equal? (if (if x y #t) + z + w) + (if x + (if y + z + w) + z))) + + (define-theorem less-than/pred-2 (x) + (implies (not (natural? x)) + (equal? (zero? x) #f))) + + (define-primitive-function natural-induction (x) + (if (natural? x) + (if (zero? x) + 0 + (succ (natural-induction (pred x)))) + #f)) + + (define-theorem less-than/pred (x) + (implies (natural? x) + (not (zero? x)) + (equal? (< (pred x) x) #t))) + + ;; (define-proof if-implies + ;; () + ;; (((1) if-same (set x x)) + ;; ((1 2 1) if-nest) + ;; ((1 3 1) if-nest) + ;; ((1 3) if-true) + ;; (() equal-same))) + + ;; (define-proof less-than/pred + ;; (natural-induction x) + ;; (((2 2) if-nest) + ;; ((2 2) if-not) + ;; ((2 2) if-nest) + ;; ((2 3 2) if-nest) + ;; ((2 3 2) if-nest) + ;; ((2 3) if-implies) + ;; ((2 3 2) if-implies) + + ;; (() error) + ;; (() error))) + + ;; (define-proof less-than/pred-1 + ;; () + ;; (((2 2) if-same (set x (natural? (pred x)))) + ;; ((2 2 2) if-same (set x (not (zero? (pred x))))) + ;; ((2 2 2) if-same (set x (not (zero? (pred x))))) + ;; ;; ((2 2 3 1 1) zero?) + ;; ;; ((2 2 3 1 1) if-nest) + ;; ;; ((2 2 3 1) if-false) + ;; ;; ((2 2 3 1) if-false) + ;; )) -;; (define-proof natural-induction -;; (total/natural? n) -;; (((2) if-nest) -;; ((2 3) </sub1) -;; ((2) if-same) -;; (() if-same))) + (define-function + (x y) + (if (equal? 0 x) + y + (succ (+ (pred x) y)))) -;; (define-theorem natural/add1 (x) -;; (implies (natural? x) -;; (equal? (natural? (add1 x)) #t))) + ;; (define-theorem natural/add1 (x) + ;; (implies (natural? x) + ;; (equal? (natural? (add1 x)) #t))) #; (define-axiom natural/sub1 (x) - (if (natural? x) - (if (< '0 x) - (equal? (natural? (sub1 x)) '#t) - '#t) - '#t)) + (if (natural? x) + (if (< '0 x) + (equal? (natural? (sub1 x)) '#t) + '#t) + '#t)) #; (define-theorem less-than/sub1 (x) - (implies (natural? x) - (< '0 x) - (equal? (< (sub1 x) x) '#t))) + (implies (natural? x) + (< '0 x) + (equal? (< (sub1 x) x) '#t))) #; (define-axiom add1/sub1 (x) - (if (natural? x) - (if (equal? '0 x) - '#t - (equal? (add1 (sub1 x)) x)) - '#t)) + (if (natural? x) + (if (equal? '0 x) + '#t + (equal? (add1 (sub1 x)) x)) + '#t)) #; (define-built-in-function + (x y) - (if (natural? x) - (if (equal? '0 x) - y - (add1 (+ (sub1 x) y))) - 'undefined)) + (if (natural? x) + (if (equal? '0 x) + y + (add1 (+ (sub1 x) y))) + 'undefined)) -#; + #; (define-axiom natural/size (x) - (equal? (natural? (size x)) - '#t)) + (equal? (natural? (size x)) + '#t)) #; (define-axiom size/car (x) - (if (pair? x) - (equal? (< (size (car x)) (size x)) - '#t) - '#t)) + (if (pair? x) + (equal? (< (size (car x)) (size x)) + '#t) + '#t)) #; (define-axiom size/cdr (x) - (if (pair? x) - (equal? (< (size (cdr x)) (size x)) - '#t) - '#t)) + (if (pair? x) + (equal? (< (size (cdr x)) (size x)) + '#t) + '#t)) #; (define-proof + - (total/natural? x) - (((2) if-nest) - ((2 3) </sub1) - ((2) if-same) - (() if-same))) + (total/natural? x) + (((2) if-nest) + ((2 3) </sub1) + ((2) if-same) + (() if-same))) #; (define-theorem thm-1+1=2 () - (equal? (+ 1 1) 2)) + (equal? (+ 1 1) 2)) #; (define-function natural-induction (n) - (if (natural? n) - (if (equal? '0 n) - '0 - (add1 (natural-induction (sub1 n)))) - 'undefined)) + (if (natural? n) + (if (equal? '0 n) + '0 + (add1 (natural-induction (sub1 n)))) + 'undefined)) #; (define-proof natural-induction - (total/natural? n) - (((2) if-nest) - ((2 3) </sub1) - ((2) if-same) - (() if-same))) + (total/natural? n) + (((2) if-nest) + ((2 3) </sub1) + ((2) if-same) + (() if-same))) #; (define-theorem equal?/add1 (n) - (if (natural? n) - (equal? (equal? n (add1 n)) #f) - #t)) + (if (natural? n) + (equal? (equal? n (add1 n)) #f) + #t)) #; (define-proof equal?/add1 - (induction (natural-induction n)) - (((2 2 2 1 1) equal-if) - ((2 2 2 1 2 1) equal-if) - ((2 2 2 1) equal?/01) - ((2 2 2) equal-same) - ((2 2) if-same) - ((2 3 1 1) natural?/sub1) - ((2 3 1) if-true) - ((2 3 2 2 1 1) add1/sub1) - ((2 3 2 2 1 2 1) add1/sub1) - ((2 3 2 2) if-same (set x (natural? (add1 (sub1 n))))) - ((2 3 2 2) if-same (set x (natural? (sub1 n)))) - ((2 3 2 2 2 2 1) common-add1 - ;; ルール探索のアルゴリズムにバグがある - (set x (sub1 n)) - (set y (add1 (sub1 n)))) - ((2 3 2 2 2 2 1) equal-if) - ((2 3 2 2 2 2) equal-same) - ((2 3 2 2 2 1) natural?/add1) - ((2 3 2 2 2) if-true) - ((2 3 2 2 1) natural?/sub1) - ((2 3 2 2) if-true) - ((2 3 2) if-same) - ((2 3) if-same) - ((2) if-same) - ((3) if-nest) - (() if-same))) + (induction (natural-induction n)) + (((2 2 2 1 1) equal-if) + ((2 2 2 1 2 1) equal-if) + ((2 2 2 1) equal?/01) + ((2 2 2) equal-same) + ((2 2) if-same) + ((2 3 1 1) natural?/sub1) + ((2 3 1) if-true) + ((2 3 2 2 1 1) add1/sub1) + ((2 3 2 2 1 2 1) add1/sub1) + ((2 3 2 2) if-same (set x (natural? (add1 (sub1 n))))) + ((2 3 2 2) if-same (set x (natural? (sub1 n)))) + ((2 3 2 2 2 2 1) common-add1 + ;; ルール探索のアルゴリズムにバグがある + (set x (sub1 n)) + (set y (add1 (sub1 n)))) + ((2 3 2 2 2 2 1) equal-if) + ((2 3 2 2 2 2) equal-same) + ((2 3 2 2 2 1) natural?/add1) + ((2 3 2 2 2) if-true) + ((2 3 2 2 1) natural?/sub1) + ((2 3 2 2) if-true) + ((2 3 2) if-same) + ((2 3) if-same) + ((2) if-same) + ((3) if-nest) + (() if-same))) #; (define-proof thm-1+1=2 - () - ((() if-same (set x (natural? '0))) - ((2 1) +) - ((2 1 2 2 1) equal-if) - ((2 1 2 3 1 1) sub1/add1) - ((2 1 2 3 1) +) - ((2 1 2 3 1 2 1) equal-same) - ((2 1 2 3 1 2) if-true) - ((2 1 2 3 1 1) natural?/0) - ((2 1 2 3 1) if-true) - ((2 1 2) if-same) - ((2 1 1) natural?/add1) - ((2 1) if-true) - ((2) equal-same) - ((1) natural?/0) + () + ((() if-same (set x (natural? '0))) + ((2 1) +) + ((2 1 2 2 1) equal-if) + ((2 1 2 3 1 1) sub1/add1) + ((2 1 2 3 1) +) + ((2 1 2 3 1 2 1) equal-same) + ((2 1 2 3 1 2) if-true) + ((2 1 2 3 1 1) natural?/0) + ((2 1 2 3 1) if-true) + ((2 1 2) if-same) + ((2 1 1) natural?/add1) + ((2 1) if-true) + ((2) equal-same) + ((1) natural?/0) (() if-true))) ) |