; Halting problem in Scheme notation.  

; The undecidability of the halting problem states that, there is no
; program H such that, given program Q and input P, H can determine
; if Q ever terminates on P.  Note that even if we already know the
; INPUT to the program, we still cannot in general statically determine
; the behavior of the program.

; We already know that basic programming language constructs such as booleans
; and ifelse can be defined as pure lambda terms:
(load "lambda.scm")  ; loads definitions from another file

; We also know that there are lambda terms that will loop forever when
; beta reduced - they do not "halt":

(define infloop ((lambda (x) (x x)) (lambda (x) (x x))))

; The coding of the halting problem is as follows:

; Assume there is a combinator (pure lambda term) HALT such that 
; for all lambda terms R and X, (HALT R X) beta-reduces to TRUE iff
; (R X) has a normal form (i.e, "halts"), and (HALT R X) beta-reduces to FALSE 
; iff (R X) has no normal form (i.e, "loops forever":).

; Then we define the following lambda term:

(define Q (lambda (P) (IFELSE (HALT P P) infloop I)))

; I is the term (lambda (x) x), which is already a normal form (it "halts")

; Notice that (Q P) halts if and only if (P P) does not halt.

; Consider (Q Q).  If (Q Q) halts, then (HALT Q Q) must be TRUE
; and so (Q Q) does not halt.  If (Q Q) does not halt, then (HALT Q Q)
; must be FALSE so (Q Q) halts.  We have a contradiction.  Thus there cannot
; possibly be a term HALT that behaves in the way we hoped.