;  Scheme Coding of the Halting Problem in the untyped Lambda Calculus
;  Chuck Liang, for CPSC 415, December 1998.


(define I (lambda (x) x))

; Booleans as pure lambda terms:

(define TRUE (lambda (x y) x))
(define FALSE (lambda (x y) y))

(define IFELSE (lambda (c a b) (c a b)))

(define lNOT (lambda (x) (IFELSE x FALSE TRUE)))
(define lAND (lambda (x y) (IFELSE x y FALSE)))
(define lOR  (lambda (x y) (IFELSE x TRUE y)))


; The following lambda term has no normal form when applied to itself:

(define SELFAPP (lambda (x) (x x)))


; The coding of the halting problem can now continue:

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

; Then we can define the following combinator:

; (define Q (lambda (P) (IFELSE (HALT (P P)) (SELFAPP SELFAPP) I)))

; 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 FALSE
; and so (Q Q) does not halt.  If (Q Q) does not halt, then (HALT (Q Q))
; must be TRUE so (Q Q) halts.  We have a contradiction.


; ----------------------------------------------
; For the typed lambda calculus, non-termination is impossible without
; a "fixed point operator":

(define FIX (lambda (F) (F (FIX F))))

; (FIX (lambda (F) F))  will not terminate.