Chaitin's Unknowable code

unknowable.lisp

;;
;; Liberal transcription of (some of) the lisp code found in Chaitin's "The Unknowable"
;;
;;                                                             Immad Naseer -- Dec 26th
;;

;;
;; A lisp expression which evaluates to itself.
;;

(defun f(x)
  `(,x ,x))

;; f(1) -> (1 1)
;; f('(1 2 3)) -> ((1 2 3) (1 2 3))
;; f('hello) -> ('hello 'hello)

;; Now let's define f anonymously and pass f a copy of itself.

(setq f '((lambda (x) `(,x ,x))
	  (lambda (x) `(,x ,x))))

;; The above is equivalent to calling f passing it its own code. 
;; The output is the exact same expression, as certified by the
;; equality check below which evaluates to true.

(equal f (eval f))


;;
;; Godel's Incompleteness Theorem
;;

;; A statement saying x is unprovable.

(defun g(x)
  `(is-unprovable (value-of (,x ,x))))

;; Calling g w/ its own code which is equivalent to saying that 'this statement is unprovable'!

(setq g '((lambda (x) `(is-unprovable (value-of (,x ,x))))
	  (lambda (x) `(is-unprovable (value-of (,x ,x))))))

(equal g (cadr (cadr (eval g))))

;;
;; Turing's halting problem
;;


;; Arbitrary implementation of the halting function. In this case, it
;; always returns false. In order to always return true, return 't

(defun halts? (s-exp) nil) 

;; The turing function takes a program x. 
;; If x halts, it goes in an infinite loop thus never halting (here simulated by just returning the symbol 'loop).
;; If x doesn't halt, it halts by returning nil

(defun turing(x)
  (let ((z `(,x ,x)))
    (if
	(halts? z)
	'loop
      nil)))

;;
;; The following expression calls the turing function passing a copy of itself to it.
;; It halts because the turing function doesn't halt (because of how we defined halts?) -- a contradiction!
;;   Alternatively, if we change the definiction of halts? to always return 't
;;   Then it'll go in an infinite loop because it halts -- still a contradiction!
;;

((lambda (x)
   (let ((z `(,x ,x)))
     (if (halts? z)
	 'loop
         nil)))
 (lambda (x)
   (let ((z `(,x ,x)))
     (if (halts? z)
	 'loop
         nil))))