N or Space for next slide, P for previous slide, F for full screen, M for menu
Lec 11:Uncomputability
Boaz Barak (instructor), Salil Vadhan (co-instructor), Juan Perdomo (Head TF).
Team: Aditya Mahadevan, Brian Sapozhnikov (surveys), Chan Kang (extension), Gabe Abrams (Ed Tech), Gabe Montague (NAND web), Jessica Zhu (proof workshops), John Shen, Juan Esteller (NAND implementation), Karl Otness, Katherine Binney, Mark Goldstein (clicker expert), Stefan Spataru, Susan Xu, Tara Sowrirajan, Thomas Orton (Advanced Section)
Slides will be posted online.
Laptops/phones only on last 3 rows please.
Announcements
More office hours
Salil review lecture
\(\lambda\) for OCaml, Python
Midterm prep post
Survey: http://tiny.cc/cs121survey
Uncomputability
“This conviction of the solvability of every mathematical problem is a powerful incentive to the worker. We hear within us the perpetual call: There is the problem. Seek its solution. You can find it by pure reason, for in mathematics there is no ignorabimus”, David Hilbert, 1900
Question 1
Does the C function below halt on every input?
int mystery(int n) {
if (n < 1) { return 1; }
return n*mystery(n-1);
}a. Yes
b. No
Question 2
Does the C function below halt on the input \(n=2\)? (assume bigint and power functions)
int mystery(int n) {
int i,j,k;
for(i=2;i < ;i++) {
for(j=2;j < n;j++) {
for(k=2;k < n;k++){
if (pow(i,11)==(pow(j,11)+pow(k,11) )) {
return 1;
}
}
}
}
return mystery(n+1);
}a. Yes
b. No
Theorems of the day
Def: \(D = \{ F : F:\{0,1\}^* \rightarrow \{0,1\} s.t. F \text{ computable by NAND++ program} \}\).
Thm 1: There exists uncomputable function \(F \not\in D\).
Thm 2: \(HALT\) is uncomputable where \(HALT(P,x)=1\) iff \(P\) halts on input \(x\).
Proof of Theorem 1.
Thm 1: There exists uncomputable function \(F \not\in D\).
- \(D\) = computable functions
- \(F\) = all functions
- \(D\) is countable
- \(F\) is not
- \(|D|\lt|F|\)
- \(F \not\subseteq D\).
Prove Thm 1+ 2 in one shot
Thm 2: \(HALT\) is uncomputable where \(HALT(P,x)=1\) iff \(P\) halts on input \(x\).
(move to powerpoint)
Reductions
HALTONZERO
Def: \(HALTONZERO(P)=1\) iff \(P(0)\) halts.
Thm: \(HALTONZERO\) is uncomputable.
Proof: Suppose toward contr. \(A\) computes \(HALTONZERO\), we’ll build \(B\) computing \(HALT\).
HALTONZERO
Def: \(HALTONZERO(P)=1\) iff \(P(0)\) halts.
Thm: \(HALTONZERO\) is uncomputable.
Proof: Suppose toward contr. \(A\) computes \(HALTONZERO\), we’ll build \(B\) computing \(HALT\).
- \(B\) gets as input a pair \((P,x)\).
- Construct program \(Q=Q_{P,x}\) s.t. for every \(w\), \(Q(w)=P(x)\)
int Q(char *w) {
const char *P = "001000010111";
const char *x = "011010101011110101010010001010101001"
return EVAL(P,x)
}- Return \(A(Q)\). (i.e.,\(A\) applied to representation of \(Q\) as string)
Lemma: For every \(P\),\(x\), \(P\) halts on \(x\) iff \(Q_{P,x}\) halts on \(0\).
Question
If I want to prove that Problem \(X\) is uncomputable by a reduction from \(HALT\), I need to:
Design an algorithm that solves \(X\) using an algorithm that solves \(HALT\).
Design an algorithm that solves \(HALT\) using an algorithm that solves \(X\).
Intuition: Can solve \(HALT\) using \(X\) \(\approx\) “\(HALT\) is easier than \(X\)”
therefore: If you cannot solve \(HALT\) then you cannot solve \(X\).
Rice’s Theorem
Syntactic properties of programs: Has comments, variables begin with lower case, has at least 100 lines, no syntax errors (follows grammar),..
Semantic properties of programs: Does not go into infinite loop, computes parity function, never reveals credit card.
Fundamental Theorem of Software Verification:
Depressing Theorem of Software Verification: Every non-trivial semantic property of programs is uncomputable.
Thm: Every \(F:\{0,1\}^* \rightarrow \{0,1\}\) satisfying:
1. If \(P\) and \(P'\) compute same function* then \(F(P)=F(P')\).
2. There exist \(P_0,P_1\) s.t. \(F(P_0)=0\) and \(F(P_1)=1\).
is uncomputable.
Proof of Rice’s Thm
Thm: Every \(F:\{0,1\}^* \rightarrow \{0,1\}\) satisfying:
1. If \(P\) and \(P'\) compute same function then \(F(P)=F(P')\).
2. There exist \(P_0,P_1\) s.t. \(F(P_0)=0\) and \(F(P_1)=1\).
is uncomputable.
Proof: We reduce from \(HALTONZERO\). Given \(A\) that solves \(F\) we will construct \(B\) that solves \(HALTONZERO\).
Proof of Rice’s Thm
Thm: Every \(F:\{0,1\}^* \rightarrow \{0,1\}\) satisfying:
1. If \(P\) and \(P'\) compute same function then \(F(P)=F(P')\).
2. There exist \(P_0,P_1\) s.t. \(F(P_0)=0\) and \(F(P_1)=1\).
is uncomputable.
Proof: We reduce from \(HALTONZERO\). Given \(A\) that solves \(F\) we will construct \(B\) that solves \(HALTONZERO\).
Desiderata: Map \(Q\) to \(P=P_Q\) s.t. (1) \(Q\) halts on \(0\) \(\Rightarrow\) \(F(P)=1\) and (2) \(Q\) does not halt on \(0\) \(\Rightarrow\) \(F(P)=1\)
First attempt: On input \(x\):
- Run \(Q(0)\).
- If halts then output \(P_1(x)\) else output \(P_0(x)\).
Question: What is right and what is wrong in this attempt.
Proof of Rice’s Thm
Thm: Every \(F:\{0,1\}^* \rightarrow \{0,1\}\) satisfying:
1. If \(P\) and \(P'\) compute same function then \(F(P)=F(P')\).
2. There exist \(P_0,P_1\) s.t. \(F(P_0)=0\) and \(F(P_1)=1\).
is uncomputable.
Proof: We reduce from \(HALTONZERO\). Given \(A\) that solves \(F\) we will construct \(B\) that solves \(HALTONZERO\).
Desiderata: Map \(Q\) to \(P=P_Q\) s.t. (1) \(Q\) halts on \(0\) \(\Rightarrow\) \(F(P)=1\) and (2) \(Q\) does not halt on \(0\) \(\Rightarrow\) \(F(P)=1\)
Idea: Let \(INF\) program that goes to infinite loop. Either \(F(INF)=0\) or \(F(INF)=1\). (wlog \(F(INF)=0\))
Definition of \(Q\): On input \(x\):
- Run \(Q(0)\).
- Output \(P_1(x)\)
Example
Def: \(F:\{0,1\}^* \rightarrow \{0,1\}\) is monotone if for every \(x,x' \in \{0,1\}^n\) on which \(F\) is defined, if \(x_i \leq x'_i\) for \(i\in [n]\) then \(F(x) \leq F(x')\).
Thm: Let \(MONOTONE(P)=1\) if \(P\) computes a partial monotone function, then \(MONOTONE\) is uncomputable.
Is software verification doomed?
What do you think?
No general verification for all programs.
But can verify some programs.