Limits of
Computation
8 – Our first non-computable problem Bernhard Reus
1
A non-computable problem
THIS TIME
•
• we consider a decision problem:
the Halting Problem,
and prove it is WHILE- undecidable!
Deep Thought
we define formally what computability and decidability means (for WHILE)
“What is the Ultimate Answer to Life,
the Universe, and Everything?”
2
(a, b) ⇧ g we write b = g(a), that is, we put parenthes have written f((3,2)) = 2, rather than f(3,2) = 2. H
Problems Revisited
(a, b) ⇧ g we write b = g(a), that is, we put parentheses aroun set of parentheses, and we shall also do so.
Remember
have written f ((3, 2)) = 2, rather than f (3, 2) = 2. However i
For a partial function f : A ⇥ B set of parentheses, and we shall also do so.
the domain of we restricted to problems of the form:
•
can we compute a given function of type
For a partial function f :A⇥B
⇥
•
InL-cdaasteaf➝iLs-tdoattal, ?dom(f) = A.
the domain of f is the dom(f) = {a ⇧ A|f(a
⊥
dom(f) = {a ⇧ A|f(a) ⌅}
•
(i.e. can we compute whether a given
5canwEeldecmidenmtemsboerfshCipoinmaspetu
tability
In case f is total, dom(f) = A.
The codomain of a total or partial function from
The codomain of a total or partial function from A into B The range of a total or partial function from A i
The range of a total or partial function from A into B is element is in argnivge(fn)s=et{–b ⇧yeBs|otrhneroe?)is a a ⇧ A s
ents of Computarnbg(ifl)i=ty{b ⇧TB |hteheorerisya a ⇧ A such that
•
notion of computability:
Chapter ?? set up our model WHILE of computation, Ch we now narrow this down to our chosen
WHILE programs as input to other WHILE programs, a
existence of universal programs. We are now in a position to up our model WHILE of computation, Chapter 3 gave a way to pass
AA.3..34.4 Totallvveresrusupsarptaiarltfiuanlcftuioncstions
fundamental results of computability theory, including those ms as input to other WHILE programs, and Chapter 4 showed the
Any total function is also a partial function. For a partial f
in Chapter 1.
Any total function is also a partial function. For a
⇥
5 Elem
Chapter ?? set
WHILE progra
existence of universal programs. We are now in a position to state and prove some of the
fundamental results of computability theory, including those that were informally proven
the set
uch that f(a)
happen that for all a ⇧3 A, f(a) is defined, i.e. dom(f) = A. In that case f is a Section 5.1 defines the notions of computable function and decidable set, happen that for all a ⇧ A, f(a) is defined, i.e. dom(f) = A. In tha
function.
related notions of semi-decidable and enumerable sets. Section 5.2 presen
function.
There are two standard ways of obtaining a total function f from a parti
in Chapter 1.
Section 5.1 defines the notionsTofhceormepaurteabtlwe founscttaionndanrddwecaidyasbolefsoetb,tanidnitnhegtawototal function f f
izer for WHILE programs. Section 5.3 proves that the halting problem is
f : A ⇥ B⇥:
Section 5.4 proves that all properties of WHILE programs that depend onl
relatednotionsofsemi-decidafb:leAan⇥deBnum:erablesets.Section5.2presentsaspecial- ⇥
d: Define f : do izerforWHILE5provessome
Section5.4prohatthehaltin
gram’s input-o decidable and semi-decidable. sets.
5.1 Com
As mentioned some WHILE p
Definition 5.1
WHILE progra 1. If f (d) =
2. If f (d) = A set A will be
program that always terminathese.sIefttwheillpbroegcramlledpossesmibil-ydelocoidpasbolne.elements outside A,
As we can encode numbers in WHILE’s data type, we know that a WHILE-
4
the set will be called semi-decidaWble. will show semi-decidability equivalent to enumerability, where a se computable partial function on natural numbers is one that can be implemented in
We will show semi-decidability equivalent to enumerability, where a set A is called
WHILE. ThiseinsuimpeoratabnltewihfenthceormepaisrinsgomWHeILpEro-cgormamputtahbialittyliwsittsh oatlhlear nodtionsly the elements o
of computation that use the natural numbers as data type (this is quite common).
enumerable if there is some program that lists all and only the elements of A in some
order. This allows repetitions, and does not necessarily list A’s elements in
es around a. owever it is c
d a. Thus above t is customary t
f is the set set
) ⌅}
A into B is t
Theory
is the set B. nto B is the s
f(a)=b} apter 3 gave a
nd Chapter 4 state and prove
that were infor
unction f : A ⇥ partial functi
undefined: D
whenever f is merable and se
dom(f), and f ( he result wh
r all a⇧dom es
merabilit
re equal if and o
al values
utable if it is c
ions f,g : A ⇥ B wo sets are e
ctions f and g t tal functions
E computable i dom(f ) = dom(
total functio equal i do
for A can be a ops on element
Funct
1. Remove all those elements of A on which f is undefine programs. Sgecrtaimon’s5i.n3ppurto-voeustpthuattbtheheahvaioltuinrgapreroubnledmeciisdaubnldee.ciSdaecbtleio.n 5.
The slogan here is:
1. Remove all those elements of A on which f is by f (a) = f(a) for all a ⇧ dom(f).
ves that all prodpeecridtiaebsloef aWnHdIsLeEmpi-rdoegcriadmasbltehastetdse,paend oSnelcytionth5.e6psrho-ows t
by f (a) = f(a) for all a ⇧ dom(f).
2. Add a new element to B and let that be the result
utput behaviour are undecidable. Section 5.5 proves some properties of semi-decidable. Section 5.7 proves some properties of enu
WHILE Computability a⇧A\dom (f).
Define f :A⇥(B⌃{ }) by: f (a)=f(a) for all a⇧ 2. Add a new element to B and let that be t
semi-decidable sets, and Section 5.6 shows that the halting problem is
sets.
88 Define f : A ⇥8(BAn⌃Un{d ec}id)abbley(N:onf-co(map)uta=blef) P(raob)lemfo Section 5.7 proves some properties of enumerable and semi-decidable
a ⇧ A\dom(f ).
Definition 8.1 A partial function f : D → D is WHILE-computable if there is A.3.5 Equality of fu⊥nctions and partial valu
5.1 Computability, decidability, enu
a WHILE-program p such that f = pWHILE, in other words if f is equal to the
Recall that functions are just certain sets, and that two sets a
semantics of p (we can also say “if p implements f ”).
A.3.5 Equality of functions and parti
putability, decidability, enumerability
As mentioned earlier, a function is henceforth called comp
contain the same elements. This implies that two total funct
sRomecealWl tHhIaLtEfpurnocgtriaomn:s are just certain sets, and that t if and only if they are the same sets of pairs. Equal total fun
Slogan: a WHILE-computable function on trees is one that earlier, a function is henceforth called computable if it is computed by
cofn(ta)in= gt(hae) fsoarmalel ael⇧emA.ents. This implies that two to
A WHILE-computable (partial) function on trees is one that can be implemented in WHILE.
can be implemented in WHILE.
rogram:
Definition 5.1.1 A partial function f : ID ID is WHIL
Similarly, two partial functions f,g : A ⇥ B are equal i if and only if they are the same sets of pa⇥irs. Equal
The above definition of f being WHILE-computable means in more detail that for
WHILE program p such that f = [[p]], i.e. for all d, e ⇥ ID: all a⇧dom(f):f(a)=g(a), i.e. i for all a⇧A:
.1aAnypda,reti∈alDfu(f(noacrt)ailo=lntregfe(s:adID)afn odreID)a:lliasso⇧WHAI.LE computable i there is a
m p such that f = [[p]]W,HiI.LeE. for all d, e ⇥ ID:
1.S1iIm.f fil((ad)r)⇤ly=a,n⇤tdwtgoh(aemp)n⇤ae;[[rapotn]ri]s(adlt)hf=autn⇤fc.itsiounsdeffi,nged: Aat⇥d B are
1. If f (d)↑ then p (d)↑ ⇥ Notation
Whenever f applied to d is undefined, then so is the semantics of p, in other all a2⇧. fd(oam)⌅(afn)d:gf(a(m)a⌅)ea=ndsgft(ha(a))t,=fi.iegs.(adi)e .fifnoerdaltl a ⇧ A:
2. If f (d) =e⇥ ID then [[p]](d) =e.
⇤ then [[p]](d) = ⇤.
words program p does not terminate when run on input d.
e ⇥ ID then [[p]](d) = e. 2. If f (d) = e th1e.n fp(a)⇤ a(nd)d= ge(a)⇤; or
WHILE
A set A will be called decidable if the membership question Whenever f applied to d equals e, then so does semantics of p applied to d, in
2. f (a)⌅ and g(a)⌅ and f (a) = g(a).
program that always terminates. If the program possibly lo
called decidable if the membership question for A can be answered by a other words program p terminates when run on input d and produces e as output.
A decision problem A with domain D corresponds to a set A ⊆ D of trees. The order. This allows repetitions, and does not necessarily list ’s elements in any specific
i
o
m
y
o
B
t
a
u
r
m
p g
u
m
e (
y
q h
n m
n t
A decision problem A with domain D corresponds to a set A ⊆ D of trees. The
uniform question problem for A is the following: Isagivenelementd∈Din A?
Or in other words: Given d ∈ D, does d ∈ A hold? Note how this is a problem
in our sense: it is uniform, the input type is well defined (D) as well as the output type which has to allow for answers ‘yes’ and ‘no’ (‘true’ and ‘false’) and is thus the type of Boolean values. Elements of each of both types are finite and precisely describable.
WHILE decidability
able by an effective procedure, as we know we use WHILE as effective procedures:
We can now instantiate the generic definition of a problem computable or decid-
A decidable set (or a decidable problem) is one for which the membership test can be computed by a WHILE-program that always terminates.
These definitions can also be given more precisely and formally:
Definition8.2 AsetA⊆DisWHILE-decidableif,andonlyif,thereisaWHILE- program p such that pWHILE (d)↓ (meaning pWHILE (d) is defined) for all d in D, and, moreover, d ∈ A if, and only if, pWHILE (d) = true.
Note that in the (older) literature, when computability is defined in terms of natural nuSmlobegracno:mapuWtatHioIn,LaEd-edciedacbidleasbetleis soeftetnocrallpedroa brelceumrsivoenset.rees is one for
which the membership test can be implemented in WHILE.
(formally)
5
Our first Non-computable Problem
6
8.2 The Halting Problem for WHILE
89
8.2 The Halting Problem for WHILE
Let us look at the following problem which is about WHILE-programs (represented
A decision problem:
as elements of D, we already know how to encode programs as data so this is not a problem).
Definition8.3 TheHaltingproblem—assetHALT⊆D—isdefinedasfollows: HALT={[p,d]∈D| pWHILE(d)↓}
What does the problem say informally speaking, given as a class of (uniform) ques- tions? Well, the question is this:
WHILE-program as data WHILE-data
Given a WHILE-program p (as data) and a value d ∈ D, does program p terminate if we run
it on input d?
the list (and thus the
program) are encoded but
Note again the uniformity, the answer must be given for an arbitrary program and
we drop the encoding
data. We also have a problem about two pieces of information here, the program and
brackets
its input, but we can pair them together into one input tree in the way we already encountered for otherWHILE-programs using the encoding of pairing (p,d) as list [p,d] which can be itself encoded in D. We drop the encoding brackets from the list to improve readability. We will drop those encoding brackets most of the time in
the following chapters too.
We will show in this section that the set HALT is not WHILE-decidable in the sense
explained earlier (Definition8.2). This is equivalent to showing that the function halt defined below is not computable by a WHILE-program. In other words, the (total) function
7
halt(a) = true if a = [p,d] and pWHILE(d) ↓ false otherwise
Big Question:
(which is the membership test for the Halting set HALT) is not computable by a
WHILE-program.
It should be clear that it would be really useful if we could compute/solve this prob-
lem. A compiler could then check if we had inadvertently written a non-terminating program for some specific input and warn us like a type checker warns us about incompatible types when we have used expressions in an ill-typed way.
It is desirable to be able to recognise undecidable problems. Nobody wants to
star
It should be pointed out that there is still a considerable amount of research going on how to find out whether a program might not terminate for some input. Termination checkers have been recognised as a useful tool even if they cannot work for all input
is HALT WHILE-decidable
t wor
king
for a non-computable problem. One would like to avoid wasting time on that. It is of course not always easy to find out whether a problem is undecidable and, maybe quite surprisingly, there is an abundance of undecidable problems. We will soon present more of them in Chap. 9. It turns out that some of them can be easily recognised.
ona
proje
ct tha
sto
devel
t seek
tes
the
s
opa
pro
gra
mth
at
co
mpu
olut
?
ion
8
About the Halting Problem
• Solving the Halting Problem would be most useful, e.g. a compiler could check for termination of function calls and warn about non-termination like a type checker warns about incompatible types.
• Note that simply interpreting the program on its input does not work: if the interpreter does not terminate, one cannot return the answer ‘no’.
9
Proof of the Undecidability of the
IDEA
Halting Problem
• Assume a WHILE-program h exists that DOES solve the Halting Problem.
• With h’s help write a new WHILE-program r
• establish a contradiction
• so that the assumption that h exists must be wrong.
Establishing a contradiction to destroy a robot or computer is a very popular SciFi plot line (a.k.a. Logic Bombs).
10
The Barber of Seville Paradox
strictly speaking not a “paradox” as the contradiction can be resolved.
The Barber of Seville says:
http://www.wno.org.uk/4299
“In my town Seville, I shave all men who do not shave themselves. Those who actually shave themselves, I do not shave.”
This is a version of Bertrand Russell’s paradox (Famous Welsh logician, 1872-1970)
11
The Barber of Seville Paradox
The Barber of Seville says:
“In my town Seville, I shave all men who do not shave themselves. Those who actually shave themselves I do not shave.”
Does the barber shave himself?
(note that he lives in Seville and is a man):
No implies he shaves himself
Yes implies he does not shave himself
http://www.wno.org.uk/4299
contradiction
“paradox” can be resolved by saying such a Barber does not exist :-). Does not contradict any laws of nature.
12
The Barber of Seville Paradox as Diagonalisation
diagonal
man of Seville no
shaves 1 2 3 4 5 6 … 3466 3467 …Barber’s row
1 yes yes no yes no no
2 nonoyesnonoyes
3 no yes no no no no
4 yes yes no no yes yes
5 nonononono no
6 yesyesnononoyes
no no no yes no yes yes yes no no yes yes
is the negated diagonal. It thus
can’t be one of the rows of the table, so Barbercan’t be a male
… … … … … … … … …
3466 yes yes no no yes yes 3467
no yes yes no yes yes
…
Barber’s row no yes yes yes yes no
yes
yes no
… no yes …
yes from Seville,
but he is!
contradiction
What is the table entry (x,y) ?
At row x and column y we put yes if man # x shaves man # y and false otherwise.
13
More on that theme
http://xkcd.com/468/
14
man of Seville no.
The problem is the implicit self-reference.
if Y then
true if [[p]](d) if [[p
h alt( , )= ⇥ true if [[p]](d)
)
⇥
mf t
a
e
t
i
;
e
a C
o
=
n( e
o (
mt W
s e
t a u
un d
m
d mr
h B
u i i i
e
s
d
:
e
o
maoe
h
c
s n o
c
s
td l
u ro
c
Tr a
a c q
eh m
o j
6 7
76
16
false [[q]](p,d) = WHILE
[[q]](p,d)=
In iosthneort wcoomrtdprsu,temdobryeifca[on[pyn]c]p(idsroe)g lyr,am“D. oes r (r
while Y do Y f:a=lsYe; if [[p]](d) = ⇥(*
false if[[p]](d)= go through r and inteisrpnroet citowmiptuhtredasbyinapnuyt.pIrnogthrae
[[q]](p,d) =
writefaYlse if[[p]](d)=⇥ (*
Proof. Suppose halt were computed by some progra By assumption this has the form: q = read
brackets from the program arguments, so we do no
value
Proof. Suppose halt were compu P,D; C; wr he sake of read
By assumption this has the form: q = r
terminating loop but instead terminates with re
15 = false on input (r,rC).onTchlusiocnom: m[[ra]]n(rd)w=hi⇥lemYus Thus every possibility leads to a cont Thus every possibility leads to a contradiction. The on was the existence of a program q that comp false or, ignoring the result, rWHILE(r) ↓. Bu
program r will term=infatlesoenoninipnupturt,(arn,ro)t.heTrhcuosnct
was the existence of a program q that was the existence of a program q that computes halt, so supp6osed to be false? Indeed it was, and theref
ThAusceovnesreyqupeonscspeibriosilgitrhyaamltearldlswptirololgatreacromnstinrmaadtyeicbotienonrien.p
which means by assumption (h decides the H ThiAs acrognusmeqenuteniscceloisetlhyartelaltledprtogtrhaempsamraadyoxbe A conseqwueansctehies tehxaisttaelnlcperogframTphsroumgsraeayvmebreyqrptehpoarsestsibecnioltmietydpulaetsaedeslseht
This argumteserinmtilinasarctTleoxhsaweimlsyhpaerlenegl:uart“mueTndehntewtobitstahrcebliopensrapersluahydtarovrexe,lesaistjnueodsfotmthtoahetotrhsewemwpoahartdroi was the existence of a program
7
er of the two enrtpiountsr[[,r]a](nro) t
nwwille yaireldobYv=io give r as input m q will yield
=tetrrmuienaotne winhpe rseatcohaescconmtrmaa
what happens if
n it reaches co
minute, was Y and while Y
mt.woqatssheartiocnos [[ n[.r, r ] must be
yuriestlhdebYeo=tthretureuo.ef to
alting problem)
⇥ must be tr eBsncupotrmotmghriasnmdimqwphwli
rams may be r
command wh d to the parado HILE (r ) ↓. Thi
Tmhur,swchoemnmitarena hileYdoY
nput r, anoth es just those w
e then. In this
netrtarduiec.tiBonu.t thi on input r, a her contradicti s to a contradi
of
ppl’sy
Apply program q to CliefarYlytohneenor the other o
Halting Problem existed:
h read A {B} write C then define r as:
in other words:
HAL
d
By assumption this has the form: q = read
read X;
y
T
2. After the first assignme[[nqt]](opf,dth)e=
A
pro
and itnsgdaptraorgerparmesern,tbatuioilnt fromfoqr:t
n
gra
ing progra m r, built from
value d
Now let us see what happens
Proof
U
read X; false if [[p]](d Apply program q to inp
ing program r, built from q: true if [[p]](d read X;
1. Initia[[lqly]],(pw,de)r=ead in the input and
r to itself: X = r.
d
e
c
id
m
Bvyalausesu[mri,pfrti]oY.nthiesnhas the form: q
a
q whileYdoY:=Y;
to
inp
if Y then
If [[r]](r) , then program q
Does whihleolBdYy? adsosumY p:ti=onYt Assume a program deciding the 3. inTghepnrobglroacmk Br,isbeuxiletcfurotemd wq:hich d
write Y whileYdoY:=Y; (*
write Y does program r pltiieosnt).hTaht epreraofgterra,imnvgarpi,arobwglerhaeCmncrio,tn
write Y read X; terminate wh(en*run
WHILE
Y = C A=pplhy progr[arm, rq ].to input (X read X;
ut
(
b
i
l
i
t
X
,
X
);
(
on input r, a contradiction.
NiofwYlettheuns see what happens 4. Next, is executed andraofgter
oth arlyproongeroarmthre wotihllerteorfmthineatwteooanssi
First Iafss[[urm]](er)Y ,isthinednepedrotgruraem, thqe Now let us see what happens if we iIf [[r]](r) t,htehnen
progra
r]](r) lo,otph,esnopwroegkrnaomwqthwatilrl ydioeelds nYot pTlihesutsheavteprryogproasmsirb,ilwithyenleiatd
with r as input?
happ ⇥m
r read X {
A:= [ X, X ];
B;
Y:= C;
Cle while Y { Y:=Y }
}
write Y
Now le
r to its
If [[ plies th
tussenr 5. F ws,
= Thu
elf: X tero
Yd
rtoitself:X=r. Nowletussee WHILrE doesn’t terminate
plies that program r, whe
r (r) = ⊥. But, hang on a
at program r, when it reaches comm
wasonCthlieneaprleuyxtoirsnt,eeaonrctorehnetotorofaittadhseiecprlftr:oiofXngt=h.rear else r terminates
WHILE it waosn. Iinpthuist cra,seaYco=ntrhadictio
and derive a contradiction. Then h cannot exist.
If [C[ro]](nrc)l u,stihoenn: p[[rro]g](rra)m=q⇥wilml if then
Y:=C Apply p
Now let us see what
Y = true means h says termination but r Conclusion: [[r]](r)= while Y do Y := Y; ee what happens iiffweY gtihv
r to itself: X = r.
or the bwehaivlees oltoheorpwisteh. at follo
wrritteoYitself: X=r.
while fYa=lfalseemeoans hinsapysunotn-(term,rina)t.ion
=r.
rue oCrlneaort.ly one or the oth
butrbehavesotherwisrei.teY Clearly one or the
on input r, a contradiction. Clearly one o
6
by assumption (h decides the H Conclusion: [[r]](r)=
A consequence is that all prog
Concluspiolinefs: t[h[ra]t](prr)o=gra⇥mtmrh,uewIsnfhte[[brn]e]i(trtr)re ua,ect.h 7=falseoninput(r,r). ThuWs
with input r, in other words r on in=putfar,lasecoonntrpailndieipcsuttitohna(.trp,ro)g.ra
This argument is closely relate
= false on input (r,r). Thus command w program r will terminate on i similar example: “The barber shav
Ok, maybe this means Y is fals
Conclusion: [[r]o](nr)in=pu⇥trm,uastcob program r will terminate program r will terminate on input r, anot
Thus every possibility lead
q:
if we give r )
afterwards X c
) =t⇥rue if [[p ut (X,X); (* program, A:=[
input (X,X)
false if [[p f the two ass * Does progr
= read P,D; (*L
will yield Y e;hciisdheassthteheHfaolrtmi
(*T LoopifXst
btuaiilnt sfrtohme qre: sul reaches com
Terminate if
,X); (* Does
if we givera rawmaqrdstoY i=nphut
ens if we give
ust be true.
as input to th
(* Loop if
we have to dist
(* Termina
o Y := Y;
s command w f the two asser
Proof
HALT
Undecidability
of
similar example: “
’s
6A consequence is that all programs
r WHILE (r ) ↓.
This argument is clos6ely related to th
similar example:7 “sTimheilbaarrebxearmshpalve:es“jTushtetbhaorsbeewr
sSimoilawr hexicahmepvle: r“cTahseebwa7rbeecr oshnasviedsejru,st This argument
• The proof was using the Barber paradox technique.
• Can we also understand (reformulate) this as a proof by diagonalisation?
• In order to do that, first note that we can enumerate all WHILE-programs (like we could enumerate all men in Seville). Why is that?
A consequence
may be represented
hsohadvoensojtusthatvheost e paradoxes of mat is that all progra
wtehoaselwahyo sdogentota is closely related t
The barber shaves
The Halting Problem as Diagonalisation • How does r behave for
arbitrary input programs X:
• If X run on input X terminates,
r does not terminate.
• IfXrun on inputXdoes not
terminate, r does terminate.
• So r behaves a bit like the Barber.
read A {B} write C
assumed to decide the Halting Problem
r read X {
A:= [X,X]; B;
Y:= C;
while Y {
Y:=Y }
} write Y
17
The Halting Problem as Diagonalisation
doesprogramA WHILEprogramBno terminate when
input is program 1 2 3 4 5 6 … 3466 3467 … B?
1 2 3 4 5 6
yesyesnoyesno no no no
r’s row is the negated diagonal. It thus
can’t be one of the rows of the table, so r can’t be a WHILE program,
but it is!
nonoyesnonoyes noyesnono no no yes yes no no yes yes no no no no no no yesyesnononoyes
no yes no yes yes yes no no yes yes … … yes yes
yes no
no yes …
“r terminates if its argument (program) does not terminate when it is given itself as input; otherwise r does not terminate.”
… … … … … … … 3466 yes yes no no yes yes 3467
no yes yes no yes yes
…
r’s row no yes yes yes yes no
…
diagonal
contradiction
18
r
WHILE program A no
Diagonalisation Idea
• … is very clever
• … needs items of interest to be enumerable
• … was discovered by Cantor in 1891 to show the existence of sets that are larger than the set of natural numbers.
Georg Cantor 1845-1918
19
END
© 2008-21. Bernhard Reus, University of Sussex
Next time:
More on semi-decidability
20