#|
Copyright (C) 1994 by Robert S. Boyer and J Strother Moore.  All Rights
Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Robert S. Boyer and J Strother Moore PROVIDE ABSOLUTELY NO WARRANTY.  THE
EVENT SCRIPT IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS
OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO
THE QUALITY AND PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT
PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR
CORRECTION.
IN NO EVENT WILL Robert S. Boyer or J Strother Moore BE LIABLE TO YOU FOR ANY
DAMAGES, ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR
CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT
(INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE
OR LOSSES SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE
POSSIBILITY OF SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#

Event: Start with the initial nqthm theory.

Event: For efficiency, compile those definitions not yet compiled.

Event: Add the shell btm, with recognizer function symbol btmp and no accessors.

Definition: get (x, alist) = if alist ≃ nil then btm

elseif x = caar (alist) then cdar (alist)

else get (x, cdr (alist)) endif

Definition: unsolv-subrp (fn)

= (fn ∈ '(zero true false add1 sub1 numberp cons car cdr
       listp pack unpack litatom equal list))

Definition: unsolv-apply-subr (fn, lst) = if fn = 'zero then zero

elseif fn = 'true then true elseif fn = 'false then false elseif fn = 'add1 then 1 + car (lst) elseif fn = 'sub1 then car (lst) − 1 elseif fn = 'numberp then car (lst) ∈ N elseif fn = 'cons then cons (car (lst), cadr (lst)) elseif fn = 'list then lst elseif fn = 'car then car (car (lst)) elseif fn = 'cdr then cdr (car (lst)) elseif fn = 'listp then listp (car (lst)) elseif fn = 'pack then pack (car (lst)) elseif fn = 'unpack then unpack (car (lst)) elseif fn = 'litatom then litatom (car (lst)) elseif fn = 'equal then car (lst) = cadr (lst) else 0 endif

Definition: ev (flg, x, va, fa, n) = if flg = 'al

then if x ≃ nil

then if x ∈ N then x elseif x = 't then t elseif x = 'f then f elseif x = nil then nil else get (x, va) endif elseif car (x) = 'quote then cadr (x) elseif car (x) = 'if then if btmp (ev ('al, cadr (x), va, fa, n)) then btm

elseif ev ('al, cadr (x), va, fa, n) then ev ('al, caddr (x), va, fa, n) else ev ('al, cadddr (x), va, fa, n) endif elseif btmp (ev ('list, cdr (x), va, fa, n)) then btm elseif unsolv-subrp (car (x)) then unsolv-apply-subr (car (x), ev ('list, cdr (x), va, fa, n)) elseif btmp (get (car (x), fa)) then btm elseif n ≃ 0 then btm else ev ('al,

cadr (get (car (x), fa)), pairlist (car (get (car (x), fa)),

ev ('list, cdr (x), va, fa, n)), fa, n − 1) endif

elseif listp (x)

then if btmp (ev ('al, car (x), va, fa, n)) then btm elseif btmp (ev ('list, cdr (x), va, fa, n)) then btm else cons (ev ('al, car (x), va, fa, n),

ev ('list, cdr (x), va, fa, n)) endif

else nil endif

Definition: pr-eval (x, va, fa, n) = ev ('al, x, va, fa, n)

Definition: evlist (x, va, fa, n) = ev ('list, x, va, fa, n)

;   We now define the functions x, va, fa, and k. To do so we first define
;   SUBLIS, which applies a substitution to an s-expression.  Then we use the
;   names CIRC and LOOP in the definitions of x and fa and use SUBLIS to
;   replace those names with "new" names. It is not important whether we have
;   defined this notion of substitution correctly, since all that is required
;   is that we exhibit some x, va, fa, and k with the desired properties.

Definition: sublis (alist, x) = if x ≃ nil

then if assoc (x, alist) then cdr (assoc (x, alist))

else x endif else cons (sublis (alist, car (x)), sublis (alist, cdr (x))) endif

Definition: x (fa) = sublis (list (cons ('circ, cons (fa, 0))), '(circ a))

Definition: fa (fa) = append (sublis (list (cons ('circ, cons (fa, 0)), cons ('loop, cons (fa, 1))),

                '((circ
                   (a)
                   (if
                    (halts '(circ a) (list (cons 'a a)) a)
                    (loop)
                    t))
                  (loop nil (loop)))),

fa)

Definition: va (fa) = list (cons ('a, fa (fa)))

Definition: k (n) = (1 + n)

;   We wish to prove that having "new" program names in the function
;   environment does not effect the computation of the body of HALTS.  To state
;   this we must first define formally what we mean by "new". Then we will
;   prove the general result we need and then we will instantiate it for the
;   particular "new" program names we choose.

Definition: occur (x, y) = if x = y then t

elseif y ≃ nil then f

else occur (x, car (y)) ∨ occur (x, cdr (y)) endif

Definition: occur-in-defns (x, lst) = if lst ≃ nil then f

else occur (x, caddr (car (lst))) ∨ occur-in-defns (x, cdr (lst)) endif

Theorem: occur-occur-in-defns ((¬ occur-in-defns (fn, fa)) ∧ (¬ btmp (get (x, fa)))) → (¬ occur (fn, cadr (get (x, fa))))

Theorem: lemma1 ((¬ occur (fn, x)) ∧ (¬ occur-in-defns (fn, fa))) → (ev (flg, x, va, cons (cons (fn, def ), fa), n) = ev (flg, x, va, fa, n))

Theorem: count-occur (count (y) < count (x)) → (¬ occur (x, y))

Theorem: count-get count (cadr (get (fn, fa))) < (1 + count (fa))

Theorem: count-occur-in-defns (count (fa) < count (x)) → (¬ occur-in-defns (x, fa))

Theorem: corollary1 ev ('al,

cadr (get ('halts, fa)),

va,

cons (cons (cons (fa, 0), def0 ),

cons (list (cons (fa, 1), nil, list (cons (fa, 1))), fa)), n)

= ev ('al, cadr (get ('halts, fa)), va, fa, n)

Event: Disable lemma1.

Theorem: lemma2 ((¬ btmp (ev (flg, x, va, fa, n))) ∧ (¬ btmp (ev (flg, x, va, fa, k)))) → (ev (flg, x, va, fa, n) = ev (flg, x, va, fa, k))

Theorem: corollary2 (ev (flg, x, va, fa, n) = t) → ev (flg, x, va, fa, k)

Theorem: lemma3 (listp (x) ∧ listp (car (x)) ∧ (cdr (x) ≃ nil) ∧ listp (get (car (x), fa)) ∧ (car (get (car (x), fa)) = nil) ∧ (cadr (get (car (x), fa)) = x)) → btmp (ev ('al, x, va, fa, n))

Theorem: expand-circ ((¬ btmp (val)) ∧ (¬ btmp (get (cons (fn, 0), fa)))) → (ev ('al, cons (cons (fn, 0), '(a)), list (cons ('a, val)), fa, j )

= if j ≃ 0 then btm else ev ('al,

cadr (get (cons (fn, 0), fa)),

pairlist (car (get (cons (fn, 0), fa)),

                       ev ('list,
                          '(a),

list (cons ('a, val)), fa, j )),

fa,

j − 1) endif)

;   After we published a proof of the unsolvability of the halting problem in
;   the JACM, a student in one of our classes named Jonathan Bellin observed
;   that one could get a trivial proof by defining (x FA) = (BTM).  However,
;   the "idea" is that the frustrating values (x FA), (va FA), and (fa FA) are
;   supposed to be objects on which EVAL behaves normally.  This class consists
;   of those objects for which SEXP, defined below is, true.  So we added the
;   second conjunct to our statement of UNSOLVABILITY-OF-THE-HALTING-PROBLEM.

Definition: sexp (x)

= if x = t then t elseif x = f then t elseif x ∈ N then t elseif listp (x) then sexp (car (x)) ∧ sexp (cdr (x)) elseif litatom (x) then sexp (unpack (x)) else f endif

Theorem: unsolvability-of-the-halting-problem ((h = pr-eval (list ('halts,

list ('quote, x (fa)), list ('quote, va (fa)), list ('quote, fa (fa))),

nil, fa, n))

→ (((h = f) → (¬ btmp (pr-eval (x (fa), va (fa), fa (fa), k (n)))))

∧ ((h = t) → btmp (pr-eval (x (fa), va (fa), fa (fa), k))))) ∧ (sexp (fa) → (sexp (x (fa)) ∧ sexp (va (fa)) ∧ sexp (fa (fa))))

Event: Make the library "unsolv" and compile it.

Index

btm, 1–3, 5 btmp, 2–6

corollary1, 4 corollary2, 5 count-get, 4 count-occur, 4 count-occur-in-defns, 4

ev, 2–5 evlist, 3 expand-circ, 5

fa, 3, 6

get, 1–5

k, 4, 6

lemma1, 4 lemma2, 5 lemma3, 5

occur, 4 occur-in-defns, 4 occur-occur-in-defns, 4

pr-eval, 3, 6

sexp, 5, 6 sublis, 3

unsolv-apply-subr, 2 unsolv-subrp, 1, 2 unsolvability-of-the-halting-pr

oblem, 6

va, 3, 6

x, 3, 6