diff options
author | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-20 13:33:07 +0900 |
---|---|---|
committer | Masaya Tojo <masaya@tojo.tokyo> | 2020-11-20 13:33:07 +0900 |
commit | d75c913a514c3a4299502a93d3025b03d2320109 (patch) | |
tree | 6004acf41b99c89367ea1fad0e3d6ad765d26069 /vikalpa/prelude.scm | |
parent | 7dbfe95af52e9870f0b3f234f7aedc1202cce5fd (diff) |
wip27
Diffstat (limited to 'vikalpa/prelude.scm')
-rw-r--r-- | vikalpa/prelude.scm | 145 |
1 files changed, 127 insertions, 18 deletions
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm index 874614d..264773d 100644 --- a/vikalpa/prelude.scm +++ b/vikalpa/prelude.scm @@ -17,7 +17,7 @@ ;;; along with Vikalpa. If not, see <http://www.gnu.org/licenses/>. (define-module (vikalpa prelude) - #:export (atom? natural? size implies prelude) + #:export (atom? size implies natural? prelude) #:use-module (vikalpa)) (define (atom? x) @@ -41,17 +41,8 @@ (if x (implies y z rest ...) #t)))) (define-system prelude () - (define-primitive-function natural? (x)) - (define-primitive-function equal? (x y)) - (define-primitive-function atom? (x)) - (define-primitive-function cons (x y)) - (define-primitive-function car (x)) - - (define-primitive-function cdr (x)) - (define-primitive-function size (x)) - (define-primitive-function not (x)) - (define-primitive-function < (x y)) - + (define-function atom? (x) + (not (pair? x))) (define-syntax-rules list () ((list) '()) ((list x . y) (cons x (list . y)))) @@ -71,7 +62,7 @@ ((implies x y) (if x y #t)) ((implies x y z . rest) (if x (implies y z . rest) #t))) - + (define-axiom equal-same (x) (equal? (equal? x x) '#t)) (define-axiom equal-swap (x y) @@ -93,24 +84,142 @@ (equal? (if x y z) y) (equal? (if x y z) z))) (define-axiom if-true (x y) - (equal? (if '#f x y) y)) + (equal? (if '#t x y) x)) (define-axiom if-false (x y) (equal? (if '#f x y) y)) (define-axiom if-same (x y) (equal? (if x y y) y)) - (define-axiom natural/size (x) + (define-axiom natural?/size (x) (equal? (natural? (size x)) '#t)) - (define-axiom size/car (x) + (define-axiom </size/car (x) (if (atom? x) '#t (equal? (< (size (car x)) (size x)) '#t))) - (define-axiom size/cdr (x) + (define-axiom </size/cdr (x) (if (atom? x) '#t (equal? (< (size (cdr x)) (size x)) '#t))) (define-axiom if-not (x y z) (equal? (if (not x) y z) - (if x z y)))) + (if x z y))) + (define-axiom sub1/add1 (x) + (implies (natural? x) + (equal? (sub1 (add1 x)) x))) + (define-axiom natural?/0 (x) + (equal? (natural? '0) '#t)) + (define-axiom natural?/add1 (x) + (implies (natural? x) + (equal? (natural? (add1 x)) '#t))) + (define-axiom sub1/add1 (x) + (implies (natural? x) + (equal? (sub1 (add1 x)) x))) + (define-axiom </sub1 (x) + (implies (natural? x) + (equal? (< (sub1 x) x) '#t))) + (define-axiom common-add1 (x y) + (implies (natural? x) + (natural? y) + (equal? (equal? (add1 x) (add1 y)) + (equal? x y)))) + (define-axiom false-if (x) + (if x '#t (equal? x '#f))) + (define-axiom equal?/01 (x) + (equal? (equal? '0 '1) #f)) + (define-axiom natural?/sub1 (x) + (if (natural? x) + (if (equal? '0 x) + '#t + (equal? (natural? (sub1 x)) '#t)) + '#t)) + (define-axiom add1/sub1 (x) + (if (natural? x) + (if (equal? '0 x) + '#t + (equal? (add1 (sub1 x)) x)) + '#t)) + + (define-primitive-function + (x y) + (if (natural? x) + (if (equal? '0 x) + y + (add1 (+ (sub1 x) y))) + 'undefined)) + + (define-proof + + (total/natural? x) + (((2) if-nest) + ((2 3) </sub1) + ((2) if-same) + (() if-same))) + + (define-theorem thm-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)) + + (define-proof natural-induction + (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)) + + (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))) + + (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-true)))) |