diff options
| -rw-r--r-- | vikalpa.scm | 362 | ||||
| -rw-r--r-- | vikalpa/prelude.scm | 353 |
2 files changed, 439 insertions, 276 deletions
diff --git a/vikalpa.scm b/vikalpa.scm index 671082a..dc5b6de 100644 --- a/vikalpa.scm +++ b/vikalpa.scm @@ -33,16 +33,20 @@ define-theorem define-primitive-function define-function + define-scheme-function define-proof define-totality-claim define-syntax-rules + system-eval + natural? succ pred) #:use-module (ice-9 match) #:use-module (ice-9 format) #:use-module (ice-9 control) #:use-module ((srfi srfi-1) - #:select (every any member lset-union fold append-map)) + #:select (every any member lset-union fold append-map + find)) #:use-module (srfi srfi-8) #:use-module (srfi srfi-11) #:use-module (srfi srfi-26) @@ -53,17 +57,40 @@ (apply format #t f args) #t)) -(define-syntax-rule (define/guard (name (var pred?) ...) b b* ...) +(define-syntax-rule (define/guard (name (var p?) ...) b b* ...) (define (name var ...) - (unless (pred? var) + (unless (p? var) (error (format #f "~a:~% expected: ~a~% given: " 'name - 'pred?) + 'p?) var)) ... b b* ...)) +(define-syntax define-type + (syntax-rules () + ((_ name + constractor + (m p?) + (n t? getter-name getter) ...) + (begin + (define len (+ 1 (length (list n ...)))) + (define (constractor getter-name ...) + (let ((data (make-list len))) + (list-set! data m 'name) + (list-set! data n getter-name) + ... + data)) + (define (p? x) + (and (list? x) + (= len (length x)) + (eq? 'name (list-ref x m)) + (t? (list-ref x n)) ...)) + (define (getter x) + (list-ref x n)) + ...)))) + ;; (natural? x) -> boolean? (define (natural? x) (and (exact-integer? x) @@ -141,7 +168,7 @@ (define (expression-vars expr) (cond - ((app-form? expr) + ((pair? expr) (apply lset-union eq? (map expression-vars (app-form-args expr)))) ((variable? expr) (list expr)) @@ -323,7 +350,6 @@ => (cut substitute <> (rule-rhs rl))) (else #f))) - (define (system? x) (and (list? x) (= 4 (length x)) @@ -385,14 +411,16 @@ (define (primitive-function? x) (and (list? x) - (= 3 (length x)) + (= 5 (length x)) (variable? (primitive-function-name x)) (eq? 'primitive-function (list-ref x 1)) - (vars? (primitive-function-vars x)))) + (vars? (primitive-function-vars x)) + ((option expression?) (primitive-function-expression x)) + ((option code?) (primitive-function-code x)))) ;; (primitive-function variable? vars?) -> primitive-function? -(define (primitive-function name vs) - (list name 'primitive-function vs)) +(define (primitive-function name vs expr code) + (list name 'primitive-function vs expr code)) (define (primitive-function-name pf) (list-ref pf 0)) @@ -400,23 +428,39 @@ (define (primitive-function-vars pf) (list-ref pf 2)) +(define (primitive-function-expression pf) + (list-ref pf 3)) + +(define (primitive-function-code pf) + (list-ref pf 4)) + (define (function? x) (and (list? x) - (= 6 (length x)) + (= 5 (length x)) (variable? (function-name x)) (eq? 'function (list-ref x 1)) (vars? (function-vars x)) (expression? (function-expression x)) - ((const #t) (function-code x)) - (boolean? (function-primitive? x)))) + ((option code?) (function-code x)))) + +(define (code? x) + (and (list? x) + (= 2 (length x)) + (eq? 'code (list-ref x 0)) + ((const #t) (code-expr x)))) + +(define (code x) + (list 'code x)) + +(define (code-expr x) + (cadr x)) ;; (function variable? vars? expression?) -> function? (define/guard (function (name variable?) (vars vars?) (expr expression?) - (code (const #t)) - (primitive boolean?)) - (list name 'function vars expr code primitive)) + (code (option code?))) + (list name 'function vars expr code)) (define (function-name f) (list-ref f 0)) @@ -430,9 +474,6 @@ (define (function-code f) (list-ref f 4)) -(define (function-primitive? f) - (list-ref f 5)) - (define (definition-name d) (list-ref d 0)) @@ -644,26 +685,10 @@ ,(pair->expr (cdr x))) (expr-quote x))) -(define (expand-quoted x) - (cond - ((expr-quoted? x) - (let ((val (expr-unquote x))) - (cond - ((natural? val) - (natural->expr val)) - ((pair? val) - (pair->expr val)) - (else x)))) - ((pair? x) - (cons (expand-quoted (car x)) - (expand-quoted (cdr x)))) - (else x))) - (define (convert-to-expression x) - (expand-quoted - (quote-all - (expand* (filter macro? (system-definitions (current-system))) - (expand-let x))))) + (quote-all + (expand* (filter macro? (system-definitions (current-system))) + (expand-let x)))) ;; (axiom variable? vars? expression?) -> axiom? ;; axiom? is theorem* @@ -719,6 +744,39 @@ '() (theorem*-expression x))) +(define (error? x) + (and (pair? x) + (eq? 'error (car x)))) + +(define (rewrite/eval expr sys) + (let eval ((expr expr)) + (cond + ((error? expr) expr) + ((expr-quoted? expr) expr) + ((app-form? expr) + (let ((args (map eval (app-form-args expr))) + (name (app-form-name expr))) + (or (find error? args) + (eval (rewrite1 sys + `(,name ,@args) + (lambda args + (cons* 'error rewrite name args)) + (rewriter '() `(,name))))))) + ((if-form? expr) + (let ((test (eval (if-form-test expr)))) + (if (error? test) + test + (if (expr-unquote test) + (eval (if-form-then expr)) + (eval (if-form-else expr)))))) + (else + `(error eval invalid-expression ,expr))))) + +(define/guard (system-eval (expr (const #t)) (sys system?)) + (rewrite/eval (parameterize ((current-system sys)) + (convert-to-expression expr)) + sys)) + ;; (rewriter path? command?) -> rewriter? (define (rewriter p c) (cons p c)) @@ -809,10 +867,10 @@ (list (rule (function-vars x) '() (function-app-form x) - (function-expression x)) + (definition-expression x)) (rule (function-vars x) '() - (function-expression x) + (definition-expression x) (function-app-form x)))) (define (apply-function f args) @@ -854,24 +912,10 @@ (extract (rewriter-path r) expr fail) (builder (cond - ((eq? 'equal? cmd/name) - (match extracted-expr - (('equal? `(quote ,x) `(quote ,y)) - (expr-quote (equal? x y))) - (else - (fail 'equal? extracted-expr)))) - ((eq? 'pair? cmd/name) - (match extracted-expr - (('pair? `(quote ,x)) - (expr-quote (pair? x))) - (else - (fail 'pair? extracted-expr)))) - ((eq? 'not cmd/name) - (match extracted-expr - (('not `(quote ,x)) - (expr-quote (not x))) - (else - (fail 'not extracted-expr)))) + ((core-function-name? cmd/name) + (rewrite/core cmd/name extracted-expr fail)) + ((equal? '(eval) cmd/name) + (rewrite/eval extracted-expr sys)) ((eq? 'error cmd/name) (fail extracted-expr)) ((and (symbol? cmd/name) (lookup cmd/name sys)) @@ -879,7 +923,9 @@ (cond ((theorem*? x) (rewrite/theorem cmd sys x preconds extracted-expr fail)) - ((function? x) + ((or (function? x) + (and (primitive-function? x) + (primitive-function-expression x))) (cond ((any (cut apply-rule '() <> extracted-expr '()) (function->rules x)) => identity) @@ -1012,23 +1058,24 @@ ((_ name (var ...) expr) (let ((f (function 'name '(var ...) (convert-to-expression 'expr) - 'expr - #f))) + (code 'expr)))) (add-definition f) (validate-definition f) f)))) -(define-syntax define-primitive-function +(define-syntax define-core-function (syntax-rules () ((_ name (var ...)) - (let ((f (primitive-function 'name '(var ...)))) + (let ((f (primitive-function 'name '(var ...) #f #f))) (add-definition f) - f)) + f)))) + +(define-syntax define-primitive-function + (syntax-rules () ((_ name (var ...) expr) - (let ((f (function 'name '(var ...) - (convert-to-expression 'expr) - 'expr - '#t))) + (let ((f (primitive-function 'name '(var ...) + (convert-to-expression 'expr) + (code 'expr)))) (add-definition f) (validate-definition f) f)))) @@ -1070,16 +1117,90 @@ (define-syntax-rule (define-totality-claim name nat? <) (add-totality-claim (totality-claim 'name 'nat? '<))) +(define core-function-names + '(not equal? pair? cons car cdr integer? < succ pred)) + +(define (core-function-name? x) + (member x core-function-names)) + +(define (rewrite/core name extracted-expr fail) + (case name + ((not) + (match extracted-expr + (('not `(quote ,x)) + (expr-quote (not x))) + (else + (fail 'not extracted-expr)))) + ((equal?) + (match extracted-expr + (('equal? `(quote ,x) `(quote ,y)) + (expr-quote (equal? x y))) + (else + (fail 'equal? extracted-expr)))) + ((pair?) + (match extracted-expr + (('pair? `(quote ,x)) + (expr-quote (pair? x))) + (else + (fail 'pair? extracted-expr)))) + ((cons) + (match extracted-expr + (('cons `(quote ,x) `(quote ,y)) + (expr-quote (cons x y))) + (else + (fail 'cons extracted-expr)))) + ((car) + (match extracted-expr + (('car `(quote ,x)) + (if (pair? x) + (expr-quote (car x)) + ''undefined)) + (else + (fail 'car extracted-expr)))) + ((cdr) + (match extracted-expr + (('cdr `(quote ,x)) + (if (pair? x) + (expr-quote (cdr x)) + ''undefined)) + (else + (fail 'cdr extracted-expr)))) + ((integer?) + (match extracted-expr + (('integer? `(quote ,x)) + (expr-quote (integer? x))) + (else + (fail 'integer? extracted-expr)))) + ((succ) + (match extracted-expr + (('succ `(quote ,x)) + (if (integer? x) + (expr-quote (succ x)) + ''undefined)) + (else + (fail 'succ extracted-expr)))) + ((pred) + (match extracted-expr + (('pred `(quote ,x)) + (if (integer? x) + (expr-quote (pred x)) + ''undefined)) + (else + (fail 'pred extracted-expr)))) + (else (fail 'rewrite/core 'invalid)))) + (define* (core-system #:optional (parent (make-system '() '() '()))) (parameterize ((current-system parent)) - (define-primitive-function not (x)) - (define-primitive-function equal? (x y)) - (define-primitive-function pair? (x y)) - (define-primitive-function cons (x y)) - (define-primitive-function car (x)) - (define-primitive-function cdr (x)) - (define-primitive-function succ (x)) - (define-primitive-function pred (x)) + (define-core-function not (x)) + (define-core-function equal? (x y)) + (define-core-function pair? (x y)) + (define-core-function cons (x y)) + (define-core-function car (x)) + (define-core-function cdr (x)) + (define-core-function integer? (x)) + (define-core-function < (x y)) + (define-core-function succ (x)) + (define-core-function pred (x)) (current-system))) (define-syntax define-system @@ -1267,32 +1388,34 @@ (or (function? x) (primitive-function? x))) -(define (validate-definition d) - (let* ((expr (definition-expression d)) - (vars (definition-vars d)) - (name (definition-name d)) - (expr-fnames (expression-functions expr)) +(define (validate-expression sys name vars expr) + (let* ((expr-fnames (expression-functions expr)) (expr-vars (expression-vars expr))) (when (reserved? name) (error (format #f "(vikalpa) ~a: reserved name" name))) (for-each (lambda (x) - (unless (cond - ((lookup x (current-system)) => function*?) - (else #f)) + (when (member x expr-fnames) + (error (format #f "(vikalpa) ~a: invalid variable name" name) + x))) + vars) + (for-each (lambda (x) + (unless (cond ((lookup x sys) => function*?) + (else #f)) (error (format #f "(vikalpa) ~a: undefined function" name) x))) expr-fnames) (for-each (lambda (x) (unless (member x vars) (error (format #f "(vikalpa) ~a: undefined variable" name) - x)) - (when (member x (if (function? d) - (cons name expr-fnames) - expr-fnames)) - (error (format #f "(vikalpa) ~a: invalid variable name" name) x))) expr-vars))) +(define (validate-definition d) + (let* ((vars (definition-vars d)) + (name (definition-name d)) + (expr (definition-expression d))) + (validate-expression (current-system) name vars expr))) + (define (trivial-total? f) (not (member (function-name f) (expression-functions (function-expression f))))) @@ -1306,25 +1429,31 @@ (else (error "prove" def pf)))) (define (prove/theorem sys t pf) - (match (proof-seed pf) - ((f . vars) - (cond - ((lookup f sys) - => (lambda (seed) - (rewrite sys - (make-induction-claim seed - vars - t) - (proof-sequence pf)))) - (else (error "(vikalpa) define-proof: induction function is not found." - (proof-name pf) - (cons f vars))))) - (() - (rewrite sys - (theorem*-expression t) - (proof-sequence pf))) - (else - (error "prove/theorem: fail")))) + (let ((sys-without-self + (make-system (filter (lambda (d) (not (equal? t d))) + (system-definitions sys)) + (system-proofs sys) + (system-totality-claim-list sys)))) + (match (proof-seed pf) + ((f . vars) + (cond + ((lookup f sys-without-self) + => (lambda (seed) + (let ((claim (make-induction-claim seed vars t))) + (validate-expression sys + `(claim-of ,(proof-name pf)) + (theorem*-vars t) + claim) + (rewrite sys-without-self claim (proof-sequence pf))))) + (else (error "(vikalpa) define-proof: induction function is not found." + (proof-name pf) + (cons f vars))))) + (() + (rewrite sys-without-self + (theorem*-expression t) + (proof-sequence pf))) + (else + (error "prove/theorem: fail"))))) (define (prove/function sys f pf) (match (proof-seed pf) @@ -1332,9 +1461,14 @@ (cond ((find-totality-claim id sys) => (lambda (tc) - (rewrite sys - (make-totality-claim tc m-expr f) - (proof-sequence pf)))) + (let ((claim (make-totality-claim tc m-expr f))) + (validate-expression sys + `(claim-of ,(function-name f)) + (function-vars f) + claim) + (rewrite sys + claim + (proof-sequence pf))))) (else (error "(vikalpa) define-proof: totality-claim is not found:" (proof-name pf) @@ -1347,10 +1481,10 @@ `(begin ,@(map (lambda (f) `(define (,(function-name f) ,@(function-vars f)) - ,(function-code f))) + ,(code-expr (function-code f)))) (reverse (filter (lambda (x) - (and (function? x) - (not (function-primitive? x)))) + (and (function*? x) + (function-code x))) (system-definitions sys)))))) (define/guard (check (sys system?)) 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))) ) |