LISP Interpreter Run [[[[[ Show that a formal axiomatic system (fas) can only prove that finitely many LISP expressions are elegant. (An expression is elegant if no smaller expression has the same value.) More precisely, show that a fas of LISP complexity N can't prove that a LISP expression X is elegant if X's size is greater than N + 356. (fas N) returns the theorem proved by the Nth proof (Nth S-expression) in the fas, or nil if the proof is invalid, or stop to stop everything. ]]]]] [ This expression searches for an elegant expression that is larger than it is and returns the value of that expression as its own value. ] define expression [Formal Axiomatic System #1] let (fas n) if = n 1 '(is-elegant x) if = n 2 nil if = n 3 '(is-elegant yyy) [else] stop let (loop n) let theorem [be] display (fas n) if = nil theorem [then] (loop + n 1) if = stop theorem [then] fas-has-stopped if = is-elegant car theorem if > display size cadr theorem display + 356 size fas [return] eval cadr theorem [else] (loop + n 1) [else] (loop + n 1) (loop 1) define expression value ((' (lambda (fas) ((' (lambda (loop) (loop 1))) (' (lambda (n) ((' (lambda (theorem) (if (= nil theo rem) (loop (+ n 1)) (if (= stop theorem) fas-has-s topped (if (= is-elegant (car theorem)) (if (> (di splay (size (car (cdr theorem)))) (display (+ 356 (size fas)))) (eval (car (cdr theorem))) (loop (+ n 1))) (loop (+ n 1))))))) (display (fas n)))))))) (' (lambda (n) (if (= n 1) (' (is-elegant x)) (if (= n 2) nil (if (= n 3) (' (is-elegant yyy)) stop )))))) [Show that this expression knows its own size.] size expression expression (size expression) value 456 [ Run #1. Here it doesn't find an elegant expression larger than it is: ] eval expression expression (eval expression) display (is-elegant x) display 1 display 456 display () display (is-elegant yyy) display 3 display 456 display stop value fas-has-stopped define expression [Formal Axiomatic System #2] let (fas n) if = n 1 '(is-elegant x) if = n 2 nil if = n 3 '(is-elegant yyy) if = n 4 cons is-elegant cons ^ 10 509 [<=====] nil [else] stop let (loop n) let theorem [be] display (fas n) if = nil theorem [then] (loop + n 1) if = stop theorem [then] fas-has-stopped if = is-elegant car theorem if > display size cadr theorem display + 356 size fas [return] eval cadr theorem [else] (loop + n 1) [else] (loop + n 1) (loop 1) define expression value ((' (lambda (fas) ((' (lambda (loop) (loop 1))) (' (lambda (n) ((' (lambda (theorem) (if (= nil theo rem) (loop (+ n 1)) (if (= stop theorem) fas-has-s topped (if (= is-elegant (car theorem)) (if (> (di splay (size (car (cdr theorem)))) (display (+ 356 (size fas)))) (eval (car (cdr theorem))) (loop (+ n 1))) (loop (+ n 1))))))) (display (fas n)))))))) (' (lambda (n) (if (= n 1) (' (is-elegant x)) (if (= n 2) nil (if (= n 3) (' (is-elegant yyy)) (if (= n 4) (cons is-elegant (cons (^ 10 509) nil)) st op))))))) [Show that this expression knows its own size.] size expression expression (size expression) value 509 [ Run #2. Here it finds an elegant expression exactly one character larger than it is: ] eval expression expression (eval expression) display (is-elegant x) display 1 display 509 display () display (is-elegant yyy) display 3 display 509 display (is-elegant 10000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 0000000000000000000000) display 510 display 509 value 10000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 0000000000 define expression [Formal Axiomatic System #3] let (fas n) if = n 1 '(is-elegant x) if = n 2 nil if = n 3 '(is-elegant yyy) if = n 4 cons is-elegant cons ^ 10 508 [<=====] nil [else] stop let (loop n) let theorem [be] display (fas n) if = nil theorem [then] (loop + n 1) if = stop theorem [then] fas-has-stopped if = is-elegant car theorem if > display size cadr theorem display + 356 size fas [return] eval cadr theorem [else] (loop + n 1) [else] (loop + n 1) (loop 1) define expression value ((' (lambda (fas) ((' (lambda (loop) (loop 1))) (' (lambda (n) ((' (lambda (theorem) (if (= nil theo rem) (loop (+ n 1)) (if (= stop theorem) fas-has-s topped (if (= is-elegant (car theorem)) (if (> (di splay (size (car (cdr theorem)))) (display (+ 356 (size fas)))) (eval (car (cdr theorem))) (loop (+ n 1))) (loop (+ n 1))))))) (display (fas n)))))))) (' (lambda (n) (if (= n 1) (' (is-elegant x)) (if (= n 2) nil (if (= n 3) (' (is-elegant yyy)) (if (= n 4) (cons is-elegant (cons (^ 10 508) nil)) st op))))))) [Show that this expression knows its own size.] size expression expression (size expression) value 509 [ Run #3. Here it finds an elegant expression exactly the same size as it is: ] eval expression expression (eval expression) display (is-elegant x) display 1 display 509 display () display (is-elegant yyy) display 3 display 509 display (is-elegant 10000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 000000000000000000000) display 509 display 509 display stop value fas-has-stopped define expression [Formal Axiomatic System #4] let (fas n) if = n 1 '(is-elegant x) if = n 2 nil if = n 3 '(is-elegant yyy) if = n 4 cons is-elegant cons cons "- cons ^ 10 600 [<=====] cons 1 nil nil [else] stop let (loop n) let theorem [be] display (fas n) if = nil theorem [then] (loop + n 1) if = stop theorem [then] fas-has-stopped if = is-elegant car theorem if > display size cadr theorem display + 356 size fas [return] eval cadr theorem [else] (loop + n 1) [else] (loop + n 1) (loop 1) define expression value ((' (lambda (fas) ((' (lambda (loop) (loop 1))) (' (lambda (n) ((' (lambda (theorem) (if (= nil theo rem) (loop (+ n 1)) (if (= stop theorem) fas-has-s topped (if (= is-elegant (car theorem)) (if (> (di splay (size (car (cdr theorem)))) (display (+ 356 (size fas)))) (eval (car (cdr theorem))) (loop (+ n 1))) (loop (+ n 1))))))) (display (fas n)))))))) (' (lambda (n) (if (= n 1) (' (is-elegant x)) (if (= n 2) nil (if (= n 3) (' (is-elegant yyy)) (if (= n 4) (cons is-elegant (cons (cons - (cons (^ 10 600) (cons 1 nil))) nil)) stop))))))) [Show that this expression knows its own size.] size expression expression (size expression) value 538 [ Run #4. Here it finds an elegant expression much larger than it is, and evaluates it: ] eval expression expression (eval expression) display (is-elegant x) display 1 display 538 display () display (is-elegant yyy) display 3 display 538 display (is-elegant (- 10000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000 0000000000000000 1)) display 607 display 538 value 99999999999999999999999999999999999999999999999999 99999999999999999999999999999999999999999999999999 99999999999999999999999999999999999999999999999999 99999999999999999999999999999999999999999999999999 99999999999999999999999999999999999999999999999999 99999999999999999999999999999999999999999999999999 99999999999999999999999999999999999999999999999999 99999999999999999999999999999999999999999999999999 99999999999999999999999999999999999999999999999999 99999999999999999999999999999999999999999999999999 99999999999999999999999999999999999999999999999999 99999999999999999999999999999999999999999999999999 End of LISP Run Elapsed time is 0 seconds.