N or Space for next slide, P for previous slide, F for full screen, M for menu

Lec 8: Universality and Uncomputability

Boaz Barak (instructor), Brian Sapozhnikov (Head TF), Albert Chalom, Alexis Ross, Charles O’Mara, Daniel Chen, David Li , Jambay Kinley, Jane Ahn, John Shen, Josh Seides, Laura Pierson, Pranay Tankala, Raymond Lin, Theresa Nguyen, Wanqian Yang, William Fu, Hikari Sorensen (Extension TF), Eric Lu (Patel Fellow)


Laptops/phones only on last 5 rows please.

Uncomputability

“A function of a variable quantity is an analytic expression composed in any way whatsoever of the variable quantity and numbers or constant quantities”, Leonhard Euler, 1748

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 mystery2(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 mystery2(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
  • Exists \(f \in F \setminus 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)

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\).

  1. \(B\) gets as input a pair \((P,x)\).
  1. 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)
}
  1. 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:

  1. Design an algorithm that solves \(X\) using an algorithm that solves \(HALT\).

  2. 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\):

  1. Run \(Q(0)\).
  2. 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\):

  1. Run \(Q(0)\).
  2. 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.

Opps, you cannot play draw N guess with this browser!