CS计算机代考程序代写 js ER Haskell algorithm interpreter Hive Limits of

Generalising the Halting Problem
• We have shown (by contradiction) that the Halting Problem cannot be decided by a WHILE program.
• The Halting Problem is a problem about a property of WHILE-programs, namely whether they terminate (for specific input).
• We now generalise to all (”interesting”) properties (of a certain kind) of WHILE-programs.
7
“Interesting” Properties of Programs
• “interesting” here means:
 non-trivial & extensional .
informally
• A non-trivial property is one that not all programs have, but that at least one program has.
• An extensional program property is one that depends exclusively on the input-output behaviour of the program, i.e. its semantics.
8

I
h e
e
i
D
Halting problem is a problem of (WHILE-) programs, namely whether such a pro-
oe
h
d
m e
a
g
that A is decidable must have been false and therefore A must
e semantics o
show that a pr able, namely
let us first prov
ecidable”. We n other words a
gram terminated on a specific input. It describes a property of WHILE-programs. We can actually generalise this and show that more properties of programs are un- decidable, actually all “interesting” properties of programs are undecidable if they exclusively rely on the behaviour (semantics) of the program. We need to say what
we mean by that.
A property of a program is interesting if it is a non-trivial property, i.e. one that
not every program has but also that at least one program has, and extensional. An extensional property is one that depends exclusively on the semantics, i.e. the in-
“Interesting” Properties of Programs
put/output behaviour of the program. So “interesting” program properties are “se- mantical” program properties.
More precisely we define:
Definition 9.3. A program property A is a subset of WHILE-programs. A program property A is non-trivial if {} 6= A 6= WHILE-programs.
A program property is extensional if for all p,q 2 WHILE-programs such that JpKWHILE = JqKWHILE it holds that p 2 A if and only if q 2 A.
The last property states that an extensional property is one that cannot distinguish Tbehtiwseseanysetmhatn:t
ically equal programs. If we have two different programs that have itfhpeshaamsepsreompaenrtiycsAeiathnedribtostshemuasnttbicesinisththeesestaomrenoansethofathoefmqa,rteheintheset.It
cannot be that one is in the set and the other one is not.
also q must have property A. 

If p does not have property A, and its semantics is the same as
that of q, then also q does not have property A. 103
9
.
Theorem 9.3 (Rice [19]). If A is an extension then A is undecidable.
Rice’s Theorem
EM CHAPTER 9. UNDECIDABLE PROBLEMS
9.2. RICE’S THEOREM CHAPTE
his definition we can now formulate Rice’s theorem, named
1 ice:
With the help of this definition we can no
after Henry Gordon Rice:1
Rice’s Theorem:
19]). If A is an extensional and non-trivial program property
emarkable result as from thTishewoeregmet9a.3niesnatirremfarmkailbyleorfeusunldtea-s from
Proof by contradiction:
rmally speaking, theorecmidsatbaltepsrtohbalte“masn.yIninfotermreasltliyngspperaokpinegr,tytheore
about the semantics of computation itself is und f computation itself is undecidable”. We also ontain a “recipe”
Henry Gordon Rice (1920–2003)
Assume A is decidable, 

how to show that a problem about programs (i
oblemthaebnoushtopwrotghratmthse(iHnaoltitnhgePrrwobolermdsisadpercoidgarbalme. property) is undecidable, namely by applying Rice’s theore
by applying Rice’s theorem.
e this theorem.
But let us first prove this theorem.
CE’S THEOR
the help of t nry Gordon R
m 9.3 (Rice [
s undecidable
R 9. UNDECI
w formulate Ri
al and non-triv
rem 9.3 is a r problems.Infomstatesthat“an
m.
Proof. Once again we do a proof by contradiction. We are
Once again we do a proof by contradiction. We are given a property of a
10
program (i.e. a problem about programs, namely whether the (i.e. a problem about programs, namely whether they have this property)
A that is extensional and non-trivial. We now assume A is deci s extensional and non-trivial. We now assume A is decidable. Then we show
that the Halting problem is decidable. The latter is clearly fal Halting problem is decidable. The latter is clearly false so our assumption
this we get an
contradiction
formally

r Y R
i
n
q
p
a s
e c n
o a
o m
o
o
u
e .
L
g a
r f
r t
s e
v
e
a h
In order to do carry out this plan, we need two auxiliary programs called diverge
t ad
there can be no general program verification tool, that can check for any program
e
thattheHaltingpthroabtlemAiissdedceidcaibdlea.bTlhelmattuersitshclaeavrelybfaelsensofaoulrseassa}unmdptitohnereforeAmustbeundecidable. and comp. Let us define diverge, as the program that never terminates like e.g. in
ead X th{at A is decidable must have been false and therefore A must be undecidable.
9.2. RICE’S THEOREM CHAPTER 9. UNDECIDABLE PROBLEMS
How can we derive the decidability ofwtrhietHealtRinegsproblem from the assumption
Fig. 9.2
How can we derive the decidability of the Halting problem from the assumption
:=

“e”; (* run p on value e *)
that A is decidable? We will show that any given program p on any given input e that A is decidable? We will show that any given program p on any given input e
With the help of this definition we can now formulate Rice’s theorem, named
es := X (* run comp on input X *)
taeftremr HinenaryteGsoirdf,onaRnidce:only if, another program (that we construct) is in A. As a conse-
y program q to
Fig. 9.2 Fig.9.3urofqandwh
terminates if, and only if, another program 1(that we construct) is in A. As a conse-
decidable if, and only if, the Halting problem is decidable.
quence A is decidable if, and only if, the Halting problem is decidable.
todoTcahreryoroeumtth9i.s3p(lRanic,ew[e1n9e])e.dItwfAoaisuxainliaerxytepnrsoigornaamlsancadllneodnd-itvreivrigaelprogramproperty
Fig. 9.3: Auxiliar Let usthdenfiIAneiosdriuvdnedergercei,tdoasbdtlheoe. pcraorgraymothuat tnheviesr ptelramnin,awteselinkee.dg. tinwo auxiliary programs calle
diverge read X {
while true {
and comp. Let us define diverge, as the program that never terminates li Theorem 9.3 is a remarkable result as from this we get an entire family of unde-
how to show that a problem about programs (in other words a program property) is
}
Proof of Rice’s Thm.
Fciidgab.l9e p.2roblems. Informally speaking, theorem states that “any interesting property
}
undecidable, namFeilrysbtywapeplydinegfiRnice’sttwheoremp.ro?grtahmens wcleanreleydJ:qK (d) = ? But let us first prove this theorem. then JqKWHILE (d) = JcompKWHIL
about the semantics of computation itself is undecidable”. We also ontain a “recipe”
: Auxiliary program q to show Rice’s ThWeoerenmow consider the behavio
write Y
read X { WHILE
true {
ebeheritisinAornot.IfJpK(e)= Pr by contradiction. We are given a property of a HILE-program that never terminates
diverge read X {
haviour of q and whet oof. Once again we do a proof
while tFriuge.9{.2:W ogram (i.e. a problem about pro
LE know that thWeHrIeLiEs a program prgrams,namelywhethertheyhavethisproperty)⇢
(d On the other hand, if JpK (e) #
) = ? for all d 2 D. that is extensional and non-trivia
}
Al.WenowassumeAisdecidable.ThenweshowJd
W}HILE
ig. 9.2: WHILE-program that nev
F er terminates comthpKbDle..TThehlaettreerfisocrlearwlyefalgsestotohuartassumJqptKion=
at the Haltin(gdp)rofbolermaislldedcid2a
ILE Let us call this program comp.
Wth J K false(dan)d=the?refofroerAamnuystbdeu2ndDec.idBabyle.non-trivialityofA
Jc H⇢ow cWaHnILwEe derive the decidability of the Halting problem from the assumption
write Y
WH
aet Ahaisvdectihdabtle mduivstehragve been
that JdivergeK (d) = ?WHfoIrLaEny d 2 D. ByWnHoInL-tEriviality of A we
know that there is a program that is not in A. Let us call this program comp.
ILE that A isJdeicvidearbglee? KWe will shoiwf tJhapt Kany given (pero)gr=am ?p on any given input e ere is a program that is not in A. Let us call this program comp.
=
Now assume A contains diverge (if this is not the case just swap the roles terminates if, and oWnHlyIiLf,Eanother programWH(tIhLatEwe construct) is in A. As a conse-
Soif pdoesnothaltoneweha ume A contains diverge (if this is not the case just swap the roles of A
comp if JpK (e)6=? quenceAisdecidableif,Fanigd.on9l.y2i:f,WthHeHIaLltiEng-probglermamisdtehcaidtabnle.verterminates
JK
palnemdenits complement and perfofr).mBythexetenasnioanlaoligtyooufsApwreoof). By extensionality of A
t and perform the analogous pro
n, we need two auxiliary programs called diverge contaiteforanyinput.
Iniforndeort,tosdwoacparryooluet tohfis pAl
 a ns all programs that never termina
knowramsthatneverterminateforanyinput.
that A contains all prog d comp. Let us define dWivHeIrgLeE,
an as the program thaWt nHeIvLerEterminates like e.g. in thattheumewearegivendaoperosgrhamalptonethenJqK=
and its complement
new J K =JdivergeK andsobyexten-
Halting problem is decidable ass ehavethat q
Fig. 9.2 WHILE WHILE
To show that the Halting problem is decidable assume we are given a progra
t e. We wish to decide whether JpK (e) 6= ?.
We have that JdivergeK (d) = ? for any d 2 D. By non-triviality
fact that comp 2/ A we get that q factthatdiverge2Awegetthatq2A.Ontheotherhand,if p
and its input e. We wish to decide whether JpKWHILE (e) 6= ?. onWRHickeIn(LJouElwy18t,h19a2t0t–hAepriel1W4i,sH2I0a0L3p)ErwoasgarnaAmertichanaltogiiscianoantdimnathAem.aLti-etuscallthisprogramcom
= comp andsobyextepnhsiaolntsaloitnyeofsoAtahnedlathtterwould HAPTER 9. UNDECIDABLE PROBLEMS 9.2. RICE’S THEOR
ed “his” theorem in his doctoral dissertation of 1951.
1 Now assume A contains diverge (if this is not the case just swap the r
diverge read X {
Henry Gordon Rice (July 18, 1920 – April 14, 2003) was an American logician and mathe
get that q / A. Therefore we get thatprqo/ofA. if, and only if, if
while true {
WHILE
By non-triviality of A we
that is not in A. WHILE
sionality of A and the fact that di
WHILE
quence A is te Res Inorder and comp.
d diverge ke e.g. in
diverge
while
} }
for all d 2 D E (d) for all d
KWHILE(d)=JompKWHILE we
now consider th clearlyJqKWHIivergeKWHILE
write Y
We have
JqKWH know that th
WHI
Now ass
and its com we knowthatAverge2Awe
does not halt o and its inpu tyofAandthe
mp
of A we
To show JcompKWHILE
2/ A. Therefo 1HenryGordp.
alt on e then JqK J cian. He prov
oles of A mati-
K be decidable i CEM
t comp 2/ A we 2
2
and its complement and perform the analogous proof). By extensionality of A we
cian. He proved “his” theorem in his doctoral dissertation of 1951.
}
know that A contains all programs that never terminate for any input. CHwAriPtTeEYR 9. UNDECIDABLE PROBLEMS 9.2. RICE’S THEOREM
104
on e so the latteWr withoo}ultdlobsesdoefcgidenaebrlaeliitfy,thasesufomremtehratwtahse.aTbhovisecporomgpralemteps tahned the program
11
comp(thatisnotinA)havenovariablesincoTmhmeonim.Ipfltihceaytihoanves,ojufsRtciocnes’istTenhtelyoremcanha To show that the Halting problem is decidable assume we are given a program p
rename them without changing the sema1n0t4ics. We WnHoIwLEconstruct a program q as
there can be no general program verification
and its input e. We wish to decide whether JpK (e) 6= ?.
Without loss of generality, assume that the above program p and the program
Fig. 9.2: WHILE-program that never terminates implicationsouftRliniceed’isnTFhige.o9r.e3m: canhardlybeunderestimated.Itshowsthat
and any specification that the program meet reHnaemnreytGheomrdownitRhiocuet(cJuhlayng1i8n,g19th2e0s–emApanritlic1s4.,W20e0n3o)wacsoannstArumcteraicparnogloragmiciaqnaasnd mathemati-
comp (that is not in A) have no variables in common. If they have, just consistently
1
an be no general program verification tool, that can check for any program
n check wheth he fact the the clearly nontri nto these issue
of A
ve that JqK
c
CHAPTER9.UNDECIDABLEPRthOeBrLeEMcSanbeno9p.2r.oRgICrEa’mSTtHhEaOtRcEaM We have that JdivergeKWHILE (d) = ? for any d 2 D. By non-triviality of A we
o
nli.nHede ipnroFviegd. 9“.h3i:s” theorem in his doctoral dissertation of 1951.
i
a
u
t
that the program meets the specification. So, for instance,
know that there is a program that is not in A. Let us call this program comp.
This follows immediately from t
Now assume AWcitohnotauitnslodsisveorfgege(infetrhailsitiys, naostsuthmeecathseatjuthsteswabaopvteheproglersamof Ap and the program mqtrheaatdcaXnc{heckwhetheranyothergivenprogramisavirus.
P
r
o
s
o
f
o
f
R
i
c
e
’s
T
comp(thatisnotinA)havenovaribaboletshinccaomsemsona.rIfetheyxtheavnes,jiuostncaonlsi(satentdly
and its complement and perform the analogous proof). By extensionality of A we
ional (and clearly nontrivia*l) if de
put
X
)
>
X
ru
* 104*
Y:=

“e”; ( runponvaluee )
telyknforwomthattAhceonftaicntsatlhlperotghraempsrthoaptnervteiretesrmthinattehfoarvaneyitnopubt.echeckedin
q read rXen{ame them without changing the semantics. We now construct a program q as
To show that the Halting problem is decidable assume we are given a program p } Y := olin”ede”in;Fig. 9.3(: run p on value e )
Res
:=
X ( run comp on input X )
o
mp
on
in
fi
n
e
h
HI
* using mean*s discussed in Sect.
ually run into these issues quite regularly. They sidestep them 1 } e as tree literal
write Res
L
E
Henry Gordon Rice (July 18, 1920 – April 14, 2003) was an American logician and mathemati-
write Re Of course, one can try and
d inciSane. Hcetp.ro9v.e6d “.
m
(II)
his” theorem in his doctoral dissertation of 1951.
q read X {
ax (e.g.. the byt ntryanddefiansin
Y :=

“e”; ( runteprmonsvoaflutehe s)ynt **
ne what verification or being a virus me
Res := X ( **
Fieorem arithmetic is al
g. 9.3: Auxiliary p1r0o4gram q to show Rice’s Th } into problems as oFdieg).9o.3f:aAguxivileianrypprogrraamq.tBosuhtoewvReincet’hseTnheorne
.g..thebytecemruns
not contradict
write Res
this, however, is
metic is already undecidable (see Entscheidungsproblem). All
2 WHILE
run comp on input X )
coWnetrnaodwicctoingsidtehrethfeabcethtahvaitouvreorfifiqcaantdiodwnoheatahcnetdruiatalinlsytiin-evAxiirosurts.noRtto.iocIflesJ’spKTheor(e We now consider the behaviour of q and whether it is in A or not. If J pKWHILE (e) =
Fig. 9.3: Auxiliary program q to show Rice’s Theorem
WHIWLHIELE WHILEWHILE
the?ntchleenacrleyarJlqyKJqK (d()d)⇢==?fforalld2DD.O.Onnthethoethoetrhhearnhd,ainfdJ,piKfJpK(e)#(e e’s Theorem just tells us that those tocolrsreccantl’yt fporssailbllyinwpuotrsk.
WHILE WHILE
WHILE WHILE
then JqK (d) = JcompK en JqK (d) = JcompK
(d) for all d 2 D. Therefore we get that
(d) for all d 2 D. Therefore we get that
s. We now consider the behaviour of q and whether it is in A or not. If J pKWHILE (e) =
⇢ 2 Program verification is actually a t ? then clearly JqK (d) = ? for all d 2 D. On the other hand, if JpK (e) #
WHILE WHILE WHILE WHILE
JdivergeKWHILEif JpK WHI(LeE)=?
WHILE
JqKWHILE = JdivergWeHKILE if JpK (e) = ?
actually a thrivthienngJqdKiscipl(idn)e=anJcdomqpuKite co(ndms)iadfoderrealiblnldet2hpeDro.lgaTsrhetesrfesefwohraedswebecegaedntethsa[t20] and JqKWHILE = JcompKWHILE if JpKWHILE (e) 6= ?
JcompKWHILE if JpKWHILE (e) 6= ? des [20] and has even reached giants li⇢ke Facebook [3].
JdivergeKWHILE if JpKWHILE (e) = ? JqKWHILE = WHILE WHILE
So if p does not halt on e we have that JqK WHI=LE JdivergeWKHILE and so by exten- JcompK if JpK (e) 6= ?
o ifsipondaolietsy nofoAt haanldttohne feacwt tehahtadvievetrhgaet2 Aq we get t=hat qdi2veAr.gOen the othearnhdansod,bifypext
WHILE WHILE
does halt on e then q WHILE = comp WHILE and so by extensionality of A and the
WHILE WHILE
y specification an be no progra llows immedia ses are extens grammers act eans discusse
course, one ca f the syntax (e oblems as arith
9.6.
define what v
ecode)ofagi ready undecid ing the fact t
wever, is not
ally exist. Ric th
ly for all input m verification is
)m=just tells us ?)#
hriving disciplin has even reache
the last few deca
S JKJKen-
105 does halt on e then JqKWHILE = JcompKW1H2ILE and so by extensionality of A and the
JKJK sionalityofAanSoditfhped1foa0ecs5tntohtahatldtoivnerwgeh2avAetwhaetJgqeKtthat=qJ2divAer.gOeKntheaontdhseorbhyaenxtde,n-ifp
fact that comsipon2/alAitywoef Ageatndthtahteqfa2c/t Ath.atTdhieverergfoer2eAwweeggeetttthat q 2/A. Oifn, athnedoothnelryhiafn,di,fif p
does halt on e then JqKWHILE = JcompKWHILE and so by extensionality of A and the p halts on e so the latter would be decidable if the former was. This completes the
fact that comp 2/ A we get that q 2/ A. Therefore we get that q 2/ A if, and only if, if
fact that comp 2/ A we get that q 2/ A. Therefore we get that q 2/ A if, and only if, if
p halts on e so pthealtlsaottneer swo othueldlatbteer wdoeucliddbaebdlecidfatbhleifothremfoerrmwerawsa.sT. Thhiis comppleltestethsethe proof.Theimplpicroaotifo.nsofRice’sTheoremcanhardlybeunderestimated.Itshowsthat
proof.

i
Fig. 9.3: Auxiliary program q to show Rice’s Theorem Fig. 9.3: Auxiliary program q to show Rice’s Theorem
s Jw
o no
h
2/ n
e
dH
m i
t
s c
b s
e
a u
h
se
l
f v
w
**
}
q read X {
g. 9.3: Auxiliary program q to show Rice’s Theorem
Y :=

“e”; (* run p on value e *)
write Res
Fig. 9.3: Auxiliary program q to show Rice’s Theorem
Res := X (* run comp on input X *)
WHILE WHILE
HIWLHEILE
WenoWwecnonwsicdoenrstihderbteheabveiohuarvioofuqraonfdqwanhdewthheertihteisritnisAionrAnort.nIoft.pIf pK (e)(=e)=
}
write
citohleuearnrolcyfleqJaqarKnlydJwqhKe(thde)r=i(tdi?s)i=nfoA?raoflrolnrdoat2l.lIdDfJ.2pOKDn.tWOhHenILo(tEhethe)e=orthearndha,nifdJ,pifKJ
d) = ? for all d 2 D. On the other hand, if JpK (e) #
Proof of Rice’s Thm (III)
enoWwHIcLoEnsiderthebehaviourofqandwhetheritisinAornot.IfJpK (e)= ILE (d) for all d 2 D. Therefore we get that
Fig. 9.3: Auxiliary pro⇢gram q to show Rice’s Theorem
WHILE
⇢
pK (d) for all d 2 D. Therefore we get that
WHILE WHILE WHILE WHILE
WHILE WHILE
J KJ
Res WHILE Fig.W9H.I3L:EAWHuIxLilEiaryprogramqtoshowRice’sTheorem W
ehaviour of q and whether it is in A or not. If JpK (e) = WHILEWHILE WHILEWHILE WHILE
n?JfqoKr(adll)d=(2dJ)cDo=.mOJpcnKotmhpeKot(hde)r hf(oadrn)daf,lolirfdaJ2lplKdD2.WTHDhI.Le(ETreh)feo#refowre gwetgtheatt
JdiveJrdgievKergeK if JpifKJpK (e)=(e)?=?
n clearly JqK (d) = ? for all d 2 D. On the other hand, if JpK (e) #
WHILEWHILE
JqK JqK = =
⇢ WHILE WHILE WHILE WHILE
WHILE WHILE
JqK (d) = JcompK (d) for WaHllIdL2E D. TherefoWrHeIwLeEget that JdivergeK if JpKJcomJpc(Keo)m=pK? if JpifKJpK (e)6=(e)?6=?
JdivergeKWHILE if JpKWHILE (e) = ?
(d) = ? for all d 2 D. On the other hand, if JpK
JdivergeKWHILE if JpKWHILE (e) = ? WHILE
w considWeHrItLhEe behaviourWoHfIqLaEnd whether it is in A or not. If J pK (e) =
=⇢
JcompK if JpK (e) 6= ? JcomWHpIKLE if JpK (e)6=?
learly JqK
WHILE WHILE
WHILE
JqKWHILE =
(e) # WHILWEHILE WHILWEHILE
WHILE WHILE implies
andasnod ynaoavfleitAtyhaontfdJAqthKanedfathcte=tfhaacJtdtditvhiveaertgrdgeiKeve2rgAe 2waeAngdwesteotghbeayttteqhxa2tteqnA-.2OAn. Othne tohteheort
dHioIfeLpsE dnoetshnaolttohnaletWHowInLeEehwaveehtahvaet tJhqaKt JqK = Jd=ivJedrgiveKrgeK
JcompK if JpK (e) 6= ?
(d) = JcompK (d) for all d 2 D. Therefore we get that
WHILE WHILE
we have that JqKWHILE = JdivergeKWHILE and so by exten-
uld be decida .nebedecseaocuitshdeeaofbloalutetreir
⇢ WHILE WHILE WHILEWHILE WHILEWHILWEHIWLHEILE
p does not halt on e we have that JqK = JdivergeK and so by exten- tledttsihovhanetarldegtievtohe2nregneAetJw2hqeKAngwJeqetiJKftgdfheiav=ttethrqJgac2et=oKqAm2J.pcOAKomn. OiptfhnKeJtphoKaetnhodetrhasehnor(adehnb)asdy=no,deib?,fxyitpfeenpxstieonsaiolintyaloitfy
JqKWHILE =
lIitLyEof A anWdHthIeLWEfHacItLtEhat divergWeH2ILAE we get thaWtHqIL2E A. On the other hand, if p
JcompK if JpK (e) 6= ?
t cJocmo=mpJp2c/KoAmpwKe gaentdtahsnoadtbsqyo2/ebxyAte.nxTstehionesnrieaoflniotayrleitoywfoeAfgAaentadnthdthatethqe 2/ A if, and
t that comp 2/ A weiffget that q 2/ A. Therefore we get that q 2/ A if, halt on e then JqKWHILE = comp WHILE and so by extensionality of A and the
t that q 2/ A. The that q 2/ A if, and only if, if onesothelatteecidableiftheformerwas.Thiscom htaqlt2/soAn.Tehseorethfoetbqe2d/eAcidifa,balnedifotnhleyfiof,rmiferwas.Thisc
because A is et that q 2/ A. T
JK
refore we get r would be d rleatwter gweotuthlda
hatcomp2/Aweghereforewegetthatq2/Aif,andonlyif,if oes not halt on e w J KWHILE = JdivergeKWHILE and so by exten-
ehavethat q
womerwas.Thiscompletesthe otdsoofbdwaabsle.iTfhthiesfcoormeprlwetaess.Ttheiscompletesthe
ble if the for
fetxhtenfsoiromnaerl would be deci
ofhatdiverge2Awegetthatq2A.Ontheotherhand,ifp .LEWHILE contradiction
Aandthefactt assumptions
WHI
on e then JqK = JcompK and so by extensionality of A and the implications of Rice’s Theorem can hardly be underestimated. It s
The implSiocaitfiownes ocfanRidcec’sidTehAeo,rweme can dhearcdidlyebHeAuLnTderestimated.
comp 2/ A we get that q 2/ A. Therefore we get that q 2/ A if, and only if, if
ieceim’spTlihcaetoiornesmofcaRnichea’srdTlhyeobremuncdaenrehsatridmlyabtedu.nIdtesrheostwimsatheda.t It shows that
n be no general program verification tool, that can check for an Trehecoarnembecnaongheanrdelryalbperuongdraemresvteimrifiatceadti.oIntsthoowl,sththatatcancheckfor
n e so the latter would be decidable if the former was. This completes the can be no general program verification tool, that can check for any program
program verification tool, that can check for any program
specification that the program meets the specification. So, for damanvyersipfieccaitfiiocnatitonol,ththatatthceanpcrohgercakmfomreaentyspthroegsrpaemcification.So,
ny specification that the program meets the specification. So, for instance,
ider th?e btehhea?nv pK (e)(#e) # consider the b
WHILE qKthWe(HdnI)LJtE⇢=qhKehat
arly JqK ( WH
I)L=E JcompKW (d) = Jcom
? the WHILE then
JqK = JqKWeno
WHILE
? then c
So if SpoW bsyo ebxytenx-ten-
then JqK ehsanltotoshniaoeltnwoanlseitoehhearnhda,nidf,pifp
So if
df Athaenfdaotchetesthfhdaoact AofaAndanthdethe
WHIsLioEnWaH
on e thfeancJtqtKha only if, if
en JqK fa=c and only if, if does
omp 2/ A we ge phaltspletesthe
Awegetthpaompletesthe fact t
So if p d
e so the latter proof.
he latter wopurl p hal
sionality
proof does halt
fact that plications ofTRh
It shows that
there ca ons of Ricet’hse
y program any program
c.kSwoh,eftohrerinasntyanocteh,ergivenprogramisavirus. en
and any general proagnr
instance, for instance,
Thehowsthat
p halts o there
be no general
proof. and a
pecification that the program meets the specification. So, for instance,
there can be no program that can check whether any other given program is a virus.
ationthatthereprcoagnrabmenmoepertosgrtahmesthpaetcicfiacnactiho
there can be no program that can check whether any other given program is a virus.
e no program that can check whether any other given program is a virus.
The implications of Rice’s Theorem can hardly be underestimated. It shows that
1
3
This follows immediately from the fact the the properties that have to be checked in This follows immediately from the fact the the properties that have to be checked in
programthaTthciasnfcohlleocwkswimhemtheedriatneylyoftrhoemrgthiveefnacptrothgeratmheipsraopveirutise.sthathavetobecheckedin ws immtheedrieatcealny bfreomnotghenfearcatl tphreotghreamprvoepreirfitcieastiothnatohoalv, ethtaot bceanchcehcekcekdfoinr any program
both cases are extensional (and clearly nontrivial) if defined naturally. It turns out
both cases are extensional (and clearly nontrivial) if defined naturally. It turns out
mediately frboomththceasfeasctatrheeetxhtenpsriopnearlti(easntdhactleharvlye tnoobnetricvhieacl)keifddienfined naturally. It turns out and any specification that the program meets the specification. So, for instance,
are extensional (and clearly nontrivial) if defined naturally. It turns out
that programmers actually run into these issues quite regularly. They sidestep them
that programmers actually run into these issues quite regularly. They sidestep them xtensional(tahnadtpcrloegaralymnmoenrtsriavciatul)alilfydreufinniendtontahteusrealilsys.uIetstuqrunitseoruegtularly.Theysidestepthem
there can be no program that can check whether any other given program is a virus. ammers actually run into these issues quite regularly. They sidestep them
using m rs actuTahlliys froulsnl ns discussedOin
rse, one can tr
using means discussed in Sect. 9.6.
eans discussed in Sect. 9.6. ionwignstmoimethmaenesdeidaiitsesslcuyuefssrsoeqmduitihtneSrfeagctu.tlh9aer.6ltyh..eTphroepyerstidesesthteapt htahveemto be checked in fScoeucrts.e9,.6on.ecantryanddefinewhatverificationorbeingavirusmeansin
eosuarrse,exotnenesicoannalt(rayndancdleadrelyfinoenwtrihviaatl)viefrdifieficnaetidonatourablleyi.nIgt taurnvsirouust
.O9f.6c.ourse, one can try and define what verification or being a vi of the syntax (e.g.. the byte code) of a given program. But even then one runs
y and define what verification or being a virus means in
rammers actually run into these issues quite regularly. They sidestep them f the syntax (e.g.. the byte code) of a given program. But even the
roblems as arithmetic is already undecidable (see Entscheidungsproblem). All mdseofifntehewshyanttavxer(iefi.gca..titohne boyrtebeciondge)aovfiarugsivmeneapnrsoginram. But even
the byte code) of a given program. But even then one runs
T
i
l
i
n
g
P
ans discussed in Sect. 9.6. 2 hbolwemevsera,sisarniotthmcoentriacdisctianlgretahdeyfaucntdtheactidvearbifileca(tsioeneEandtsacnhtei-ivdiurunsgtsoporlso
toyictpeirscoaobldrlema)dosyfauasnagdrieivct
nele(msreu)e.nAEslnltscheidungs
ehidnmap
ber
lteio
cg(
sirseae
malEr.enB
atsudctyh
urse, one can try and define what verification or being a virus means in 2
tually exist. Rice’s Theorem just tells us that those tools can’t possibly work
22
wever, is not contradicting the fact that verification and anti-v
r
euv
o
indedun
b
entcghis
l
e
dep
narbolb
m
astl,rraehdaoidcwtyienuvgenrdt,heeicsifdnaacobttletcho(asntetveraeErdinifictctsiacnthigoenitdhueannfgdascpatrnotthbi-alvetimrvu)es.riAtfiolcolalstion and an the syntax (e.g.. the byte code) of a given program. But even then one runs
ctly for all inputs.
ally exist. Rice’s Theorem just2tells us that those tools can’t poss Theorem just tells us that those tools can’t possibly work catcintugatlhlyeefxaicst. tRhaictev’serTifihceaotrieomn juasntdteallnstiu-vsitrhuast toholse tools can’t p lems as arithmetic is already undecidable (see Entscheidungsproblem). All
yramfovreraifillcaitniopnuistsa.ctually a thriving discipline and quite consid2erable progress has been rerevmcert,ljyuisftonrtoetallcsloinuntsprautdhtisac.tinthgotsheetfoaocltsthcatn’vterpiofiscsaitbiolny waondrkanti-virus tools
in the last few decades [20] and has even reached giants like Facebook [3].
12
lly exist. Rice’s Theorem just tells us that those tools can’t possibly work
mualvlyeraifitcharitvioing idsisacitpulianlelyanadthqruiivtiencgondsisidceipralbinle parnodgrqesusitheacsobneseinderable progre rfogrramll ivnepruifitsc.ation is actually a thriving discipline and quite considerable pr
Given an infinite supply of tiles that
[h2e0]lasntdfehwasdeevcenadresac[h2e0d]gainadntshaliskevFeancerbeoaockhe[3d]g.iantslikeFacebook[3].
de in the last few decades [20] and1h0a5s even reached giants like Facebook [3]. thriving discipline and quite considerable progress has been
are of a finite type (here:1,2), can we
verification is actually a thriving discipline and quite considerable progress has been nd has even reached giants like Facebook [3].
etlialset faenwydeacardbesit[2r0a] ranyd lhasregven rqeuacahdedragtiaincts like Facebook [3].
105
floor (i.e. the plane) so that the 105
patterns of all tiles match (in all 4 105 105
directions)? you are not allowed to rotate the DECISION PROBLEM tiles, rotation requires a new tile
105
type
bothOcfacs means in
cussedinSectrusmeansin terms
that prog termsononeruns
into p
ne can try atenrd then one runs
e syntax (e.g..
using me
intothpisr,oblem).All etamxs(aes.ga.r.ithmeinebtproblem).All
Of co
do ac
this,hoirustools vaerri,thismneotitcctihosinti-virustools
terms of corre
doactuiblywork y exist. Rice’s
snotcontraddoiossiblywork into prob
2 correPcrtolg
or all inputs. this, hcoow
t. Rice’s Theo
do actua inputs.
last fewmdaedceadienst
ma tion is actually a
made
2 erificationPriosga2rcatsshasbeen
correctlyPogresshasbeen
2 Program
decades [20] a made in th
14

Tiling Problem (cont’d)
old
• Note that swapping South-facing colours of tile type 2 and 3 as above will mean we
cannot even tile a 3×3 square. (Try it out yourself! Exercises.)
• The tiling problem for arbitrary finite sets of tile types is undecidable.
15
Tiling Problem is Hard
• 1961: H. Wang presents an algorithm that decides whether any given finite set of tile types can tile the plane. In his proof he assumed that any set that could tile the plane would be able to do so periodically (ie with a repeating pattern like a wallpaper)
• 1966: Robert Berger proved Wang’s conjecture wrong. He presented a case where the tiles would only tile the plane without repeating pattern, allegedly using
20,426 distinct tile shapes! ”Undecidability of the domino problem”, Memoirs of the AMS in 1966.
16
current record is using 
 only 13 tiles

Undecidability of Tiling the Plane
• tiling problem for a fixed size floor, n×n, is clearly decidable (check all tilings);
• infinity of the plane alone is not the reason why tiling of the plane is undecidable;
• How to prove undecidability?

if the Tiling Problem was decidable so would be the Halting Problem for Turing Machines (encode sequence of Turing Machine states by tiles which match if they are successor states in a step).
17
Reduction
• already several times this principle was used:

to show that a problem is undecidable (non-computable), argue that if it was decidable (computable) then we could decide (compute) the Halting Problem.
• Halting Problem is “at most as hard” than these other problems.
• This is called a (computable) problem reduction.
• We have seen that the Halting Problem can be reduced to any non-trivial & extensional program property or the Tiling problem. Thus those can’t be decidable either.
18

WHILE-decidability X and Y will be D, the type of binary trees.) Informally, we have a reduction from problem A on X (or the question “is a given x 2 X in A”) to problemBonY (orthequestion“isagiveny2Y inB”)ifwecanfind
1. a computable total function f : X
Y , mapping every element of X to an element
!
2. such that we know that x 2 A if, and only, if f (x) 2 B. This condition is important
ofY
to guarantee that the reduction is correct.
Whatdothesetwoconditionsmean?Thefirstconditionstatesthatutx2X Reduction
of which one can ask the question whether it is in A must be “translatable” into an element y 2 Y of which one can ask whether it is in B; and, moreover, this translation
• Assume A⊆X and B⊆Y.
cannot be “magic”, it must be computable. The second condition states that the
question whether x is in A or whether the translated x, namely f(x), is in B are equiTvahlent.dIef ycoisuikonnowptrhoe abnlsewmer txo∈onAe?, ycoaunknbowe the answer to the other.
•
f
f(x) ∈B? procedure’s input is at the bottom such that the simpler (or at least not harder than
The reduction and its ingredients are depicted in Fig. 9.5 where the decision
reduced to the decision problem
y∈B? …
B) problem A is below B.
== decision procedure

for B
• …if we find a computable (total) function 
 yes/no
f: X→Ysuchthat

x∈A “holds exactly if” f(x)B∈B iff
decision 
 procedure
 for A
any inp
x∈A?
yes/no
19
f(x)2Y f
A
x2X
Fig. 9.5: Solving A in terms of B via f: A rec B
Reduction
CHAPTER 9. UNDECIDABLE PROBLEMS 9.5. FAMOUS PROBLEM
Formally the above explanations can be stated as follows:
The above definition specifies just one particular type of reduction. There ar many others. The one we use here is also often called “recursive many-one reduc
Definition 9.4 (Reduction). Suppose oneiis given A ✓ X and B ✓ Y . Define A to be tion”. This is because many elements in B can correspond to one and the same ele
effectively reducible to B if there is a total computable function f : X ! Y such that ment5 in A via f and because, historically6 recursive is another word for “effective
forallx2X,wehavex2Aif,andonlyif, f(x)2B. or computable.
Symbolically we write this relation as A rec B (“A is effectively reducible to B”). The following theorem now explains the importance of this concept of reductio
and we have implicitly used it already to prove Rice’s theorem and argue for th
undecidability of the Tiling problem:
Theorem 9.4. If A rec B and B is decidable then A is also decidable.
Contrapositively, if A rec B and A is undecidable then B is also undecidable. Proof in Exercises.
108
Proof. The proof of this little theorem is simple and shows how both condition of a reduction, A rec B, put together ensure that we can find a decision procedur for A if we already have one for B: Just plug the implementation of the translatio function f together with the decision procedure you already have for B and, he presto, you have a decision procedure for A. Why? Well, the resulting “plugge
B is at least as hard as A
together” procedure always terminates 2(0since the decision procedure for B and the implementation of f always terminate). It remains to check that the new procedure run on x returns true if, and only if, x 2 A. But the new procedure when run on x will return whatever the decision procedure for B returns on f (x) and by assumption (the second condition in the definition of reduction) this is equivalent to x A.
S
e – – ”
n e
s e n y d
informally
from A to B
formally
2

Other undecidable Problems
• Decision Problem: do languages accepted by two
given context free grammars (CFGs) overlap?
• Decision Problem: is a CFG ambiguous?
• Decision Problem: does a CFG generate all words over a given alphabet?
• Rewriting problem (does one string rewrite into another one using a set of given rewrite rules)
• Type Checking/Inference for functional languages
with polymorphic types, where the type of all types is
Haskell avoids this “type of all types”
a type itself, is undecidable. 

Joe Wells: “Typability and Type-checking in System F are equivalent and
undecidable”, AnnalsofPureandAppliedLogic,1999.
21
Other (famous) undecidable Problems in Mathematics
• Given a system of equations with integer coefficients, does it have an integer solution?
• word problem for groups
proved undecidable by Matiyasevic in 1977
• Hilbert’s Entscheidungsproblem (is a given formulae valid in arithmetic?)
There are many others…
22

Dealing with Undecidability
• use approximation of problem (if appropriate) • give up on uniformity (restricted input)
• give up on (full) automation
• be content solving a simpler problem
23
Busy Beaver
• “Can we compute the function BB that for every input number n returns the greatest number that can be outputted by any WHILE-program that is (as syntactic string) at most n characters long (when run with input 0)?”
• T. Radó in his 1962 paper “On Non-
Computable Functions” (using Turing-Machines where n is the number of states)
Tibor Radó 
 (1895 -1965)
24
a non-computable function on numbers

Busy Beaver Research
• In theoretical computer science the Busy Beaver Problem for Turing Machines has been a challenge some researchers could not keep away from.
• Marxen and Bundtrock “Attacking the Busy Beaver 5”, Bulletin of the EATCS, No. 40, 1990, pp. 247-251, used a significant amount of resources to compute BB(5) for TMs:
25
BB(5) Attack
• They used a brute-force simulation technique going through 99.7% of all 88 million 5-state TMs but spending much thought on how to speed up simulation (using “macro-machines” that can simulate several steps in one).
• C program of about 8,000 lines
• it took 10 days to run on a 33MHz CPU
• Result: BB(5) ≥ 4098
26

END
© 2008-21. Bernhard Reus, University of Sussex
Next time:
Is there a program that can return “itself ”?
27