Rice's theorem

Every nontrivial property of the behavior of machines is undecidable on their descriptions (Turing.MultiTapeTM.rice) Rice Sipser, Problem 5.28. The behavior of the machine described by a word w (Turing.MultiTapeTM.behavior) relates each input of bits on which it halts to the output it halts with; a property of behaviors is nontrivial when the machine described by some word has it and the machine described by another does not. Equivalently, a set of words that depends only on the behavior of the machines they describe, and is neither empty nor everything, is undecidable (Turing.MultiTapeTM.not_isDecidable_of_behavior).

The proof goes through the two-way case of Kleene's recursion theorem (Turing.MultiTapeTM.exists_behavior_eq) Sipser, Theorem 6.3: for every computable verdict f on words and descriptions d false and d true, some word e describes a machine behaving as d (f e). The full theorem allows any computable transformation of descriptions in place of the choice between d false and d true; the choice is all that Rice's theorem needs. Applied to a decider of the property, with d true outside the property and d false inside it, it gives a word describing a machine inside the property exactly when it is outside. For each input of bits x, halting on x is such a property (Turing.MultiTapeTM.not_isDecidable_halts), the native form of Mathlib's ComputablePred.halting_problem.

The recursion theorem is Kleene's construction, from two constructions on descriptions. The s-m-n theorem builds an input prefix into a description (Turing.MultiTapeTM.Universal.hardwire), in polynomial time. Dispatching (Turing.MultiTapeTM.Universal.dispatch) runs a machine computing a total function, keeping its output on a work tape, and then runs d b on that output without its first bit b (Turing.MultiTapeTM.Universal.Desc.computes_dispatch). Let t describe the machine that reads a word y before its input x and dispatches on f (s y) :: x, where s y describes the machine described by y with y built in. Then e = s t describes a machine that runs the machine described by t on y = t and x, so behaves as d (f (s t)). No universal machine is needed: d false and d true are fixed, and their transitions are part of the description of the dispatching machine, reading their input from the work tape as in Turing.MultiTapeTM.Universal.Redirect.redirect.

Main definitions

• Turing.MultiTapeTM.behavior: the behavior of the machine described by a word.
• Turing.MultiTapeTM.Universal.dispatch: dispatching on the first bit computed by a machine.

Main results

• Turing.MultiTapeTM.Universal.Desc.computes_dispatch: the behavior of a dispatching machine.
• Turing.MultiTapeTM.exists_behavior_eq: the two-way case of the recursion theorem.
• Turing.MultiTapeTM.rice, Turing.MultiTapeTM.not_isDecidable_of_behavior: Rice's theorem.
• Turing.MultiTapeTM.not_isDecidable_halts: halting on a fixed input is undecidable.

References

• H. G. Rice, Classes of Recursively Enumerable Sets and Their Decision Problems
• M. Sipser, Introduction to the Theory of Computation

Finding transitions

theorem Turing.MultiTapeTM.Universal.find?_desc {k : ℕ} {S Y : Type} [Fintype S] [Fintype Y] (eS : S ↪ ℕ) (eY : Y ↪ ℕ) (tm : MultiTapeTM k Y S) (q : S) (inp : Option Y) (work : Fin k → Option Y) : List.find? (fun (x : Key × Act) => decide (x.1 = key (eS q) (Option.map (⇑eY) inp) (Option.map ⇑eY ∘ work))) (desc eS eY tm).table = some (key (eS q) (Option.map (⇑eY) inp) (Option.map ⇑eY ∘ work), Act.ofAction (Action.map eS eY (tm.tr q inp work)))

The transition found in the description of a machine is the renamed transition of the machine.

theorem Turing.MultiTapeTM.Universal.SCfg.key_eq_key_toCfg {k : ℕ} {x : List ℕ} {s : SCfg} (hs : WellShaped k x s) (out : List ℕ) (q : ℕ) : s.key x q = Universal.key q (toCfg k x s out).inputSymbol (toCfg k x s out).workTapeSymbols

The key read in a well-shaped configuration of the simulation is the key of the configuration it represents.

Dispatching on a computed bit

def Turing.MultiTapeTM.Universal.Dispatch.outAct (o : Option ℕ) : TapeAct

The action on the virtual input tape writing there the symbol o emitted by a transition.

def Turing.MultiTapeTM.Universal.Dispatch.dstate (b : Bool) (q : ℕ) : ℕ

The states of the description d b in Turing.MultiTapeTM.Universal.dispatch.

def Turing.MultiTapeTM.Universal.Dispatch.width (d : Bool → Desc) : ℕ

The number of work tapes of the two descriptions.

def Turing.MultiTapeTM.Universal.Dispatch.rest (d : Bool → Desc) (k : ℕ) : List (Option ℕ)

What the work tapes after the virtual input tape read before and after the run of tm.

def Turing.MultiTapeTM.Universal.Dispatch.markerEntries {k : ℕ} {S : Type} (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) (d : Bool → Desc) : List (Key × Act)

Writing the marker, in the state 0.

noncomputable def Turing.MultiTapeTM.Universal.Dispatch.runEntries {k : ℕ} {S : Type} [Fintype S] (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) (d : Bool → Desc) : List (Key × Act)

The transitions of tm, in the states 4 * q + 1, writing its output on the virtual input tape, and moving to the state 4 when tm halts.

def Turing.MultiTapeTM.Universal.Dispatch.branchEntries (d : Bool → Desc) (k : ℕ) : List (Key × Act)

Rewinding the virtual input tape, in the state 4, and branching on its first symbol in the state 8: the symbol becomes the marker, and the input head moves onto the blank left of the input.

def Turing.MultiTapeTM.Universal.Dispatch.redirectEntries (d : Bool → Desc) (k : ℕ) (b : Bool) : List (Key × Act)

The transitions of d b, reading the input from the virtual input tape.

noncomputable def Turing.MultiTapeTM.Universal.dispatch {k : ℕ} {S : Type} [Fintype S] (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) (d : Bool → Desc) : Desc

Dispatching on a computed bit. The description runs the machine tm, buffering its output on a new first work tape, the virtual input tape; when tm halts with output b :: v and blank work tapes, as after a tidy computation, it runs the description d b on v, reading it from the virtual input tape (Turing.MultiTapeTM.Universal.Desc.computes_dispatch).

The transitions of dispatch eS tm d

def Turing.MultiTapeTM.Universal.Dispatch.prepAct {k : ℕ} {S : Type} (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) (d : Bool → Desc) (key : Key) : Act

The action of the transitions writing the marker, rewinding and branching, as a function of their keys.

theorem Turing.MultiTapeTM.Universal.Dispatch.table_dispatch {k : ℕ} {S : Type} [Fintype S] (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) (d : Bool → Desc) : (dispatch eS tm d).table = markerEntries eS tm d ++ runEntries eS tm d ++ branchEntries d k ++ redirectEntries d k false ++ redirectEntries d k true

theorem Turing.MultiTapeTM.Universal.Dispatch.prep_spec {k : ℕ} {S : Type} (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) (d : Bool → Desc) {e : Key × Act} (he : e ∈ markerEntries eS tm d ++ branchEntries d k) : (e.1.state = 0 ∨ e.1.state = 4 ∨ e.1.state = 8) ∧ e.2 = prepAct eS tm d e.1

theorem Turing.MultiTapeTM.Universal.Dispatch.state_runEntries {k : ℕ} {S : Type} [Fintype S] (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) (d : Bool → Desc) {e : Key × Act} (he : e ∈ runEntries eS tm d) : e.1.state % 4 = 1

theorem Turing.MultiTapeTM.Universal.Dispatch.state_redirectEntries {k : ℕ} (d : Bool → Desc) {b : Bool} {e : Key × Act} (he : e ∈ redirectEntries d k b) : e.1.state % 4 = 2 + b.toNat

theorem Turing.MultiTapeTM.Universal.Dispatch.find?_prep {k : ℕ} {S : Type} [Fintype S] (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) (d : Bool → Desc) {e : Key × Act} (he : e ∈ markerEntries eS tm d ++ branchEntries d k) : List.find? (fun (x : Key × Act) => decide (x.1 = e.1)) (dispatch eS tm d).table = some e

Each transition writing the marker, rewinding or branching is the one found for its key.

theorem Turing.MultiTapeTM.Universal.Dispatch.find?_run {k : ℕ} {S : Type} [Fintype S] (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) (d : Bool → Desc) (q : ℕ) (i : Option ℕ) (ws : List (Option ℕ)) : List.find? (fun (x : Key × Act) => decide (x.1 = { state := 4 * q + 1, input := i, work := none :: (ws ++ List.replicate (width d) none) })) (dispatch eS tm d).table = Option.map (fun (e : Key × Act) => ({ state := 4 * e.1.state + 1, input := e.1.input, work := none :: (e.1.work ++ List.replicate (width d) none) }, { inputTape := e.2.inputTape, workTapes := outAct e.2.output :: e.2.workTapes, output := none, state := some (e.2.state.elim 4 fun (q : ℕ) => 4 * q + 1) })) (List.find? (fun (x : Key × Act) => decide (x.1 = { state := q, input := i, work := ws })) (desc eS eBit tm).table)

For the states of tm, the transitions found are those of tm, writing the output on the virtual input tape.

theorem Turing.MultiTapeTM.Universal.Dispatch.find?_redirectEntries {k : ℕ} {S : Type} [Fintype S] (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) (d : Bool → Desc) (b : Bool) (q : ℕ) (ws : List (Option ℕ)) : List.find? (fun (x : Key × Act) => decide (x.1 = { state := dstate b q, input := none, work := ws })) (dispatch eS tm d).table = List.find? (fun (x : Key × Act) => decide (x.1 = { state := dstate b q, input := none, work := ws })) (redirectEntries d k b)

For the states of d b and an input head reading a blank, the transitions found are those of d b, redirected.

Running tm

def Turing.MultiTapeTM.Universal.Dispatch.runCfg (d : Bool → Desc) (c : SCfg) (out : List ℕ) : SCfg

The configuration of dispatch eS tm d standing for the configuration c of the description of tm, with the output out so far written on the virtual input tape.

theorem Turing.MultiTapeTM.Universal.Dispatch.applyTapes_append_of_length_le {ts us : List Tape} {as : List TapeAct} (h : as.length ≤ ts.length) : applyTapes (ts ++ us) as = applyTapes ts as ++ us

theorem Turing.MultiTapeTM.Universal.Dispatch.wtape_apply_outAct (cs : List (Option ℕ)) (o : Option ℕ) : (Redirect.wtape cs).apply (outAct o) = Redirect.wtape (cs ++ List.map some o.toList)

theorem Turing.MultiTapeTM.Universal.Dispatch.stepOut_runCfg {k : ℕ} {S : Type} [Fintype S] (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) (d : Bool → Desc) {X : List ℕ} {c : SCfg} {q : ℕ} (hq : c.state = some q) {e : Key × Act} (he : List.find? (fun (x : Key × Act) => decide (x.1 = c.key X q)) (desc eS eBit tm).table = some e) (hlen : e.2.workTapes.length ≤ c.workTapes.length) (out : List ℕ) : stepOut (dispatch eS tm d) X (runCfg d c out, []) = (runCfg d (step (desc eS eBit tm) X c).1 (out ++ (step (desc eS eBit tm) X c).2.toList), [])

A step of tm is a step of dispatch eS tm d, which emits nothing.

noncomputable def Turing.MultiTapeTM.Universal.Dispatch.descRun {k : ℕ} {S : Type} [Fintype S] (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) (x : List ℕ) (t : ℕ) : SCfg × List ℕ

The run of the description of tm on the input x, with its output.

theorem Turing.MultiTapeTM.Universal.Dispatch.iterate_runCfg {k : ℕ} {S : Type} [Fintype S] (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) (d : Bool → Desc) {x : List ℕ} (hx : inputSymbol x 1 ∈ Redirect.bitSyms) {u : ℕ} (hrun : ∀ t < u, ∃ (q : ℕ) (e : Key × Act), (descRun eS tm x t).1.state = some q ∧ List.find? (fun (x_1 : Key × Act) => decide (x_1.1 = (descRun eS tm x t).1.key x q)) (desc eS eBit tm).table = some e ∧ e.2.workTapes.length ≤ (descRun eS tm x t).1.workTapes.length) (t : ℕ) : t ≤ u → (stepOut (dispatch eS tm d) x)^[t + 1] (init (dispatch eS tm d), []) = (runCfg d (descRun eS tm x t).1 (descRun eS tm x t).2, [])

While the description of tm runs, dispatch eS tm d runs it after writing the marker.

theorem Turing.MultiTapeTM.Universal.Dispatch.exists_run_of_computesTidily {k : ℕ} {S : Type} [Fintype S] (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) {w o : List Bool} {t₀ s₀ : ℕ} (htm : tm.ComputesTidilyInTimeAndSpace w o t₀ s₀) : ∃ (u : ℕ), (∀ t < u, ∃ (q : ℕ) (e : Key × Act), (descRun eS tm (List.map (⇑eBit) w) t).1.state = some q ∧ List.find? (fun (x : Key × Act) => decide (x.1 = (descRun eS tm (List.map (⇑eBit) w) t).1.key (List.map (⇑eBit) w) q)) (desc eS eBit tm).table = some e ∧ e.2.workTapes.length ≤ (descRun eS tm (List.map (⇑eBit) w) t).1.workTapes.length) ∧ (descRun eS tm (List.map (⇑eBit) w) u).1.state = none ∧ (descRun eS tm (List.map (⇑eBit) w) u).1.inputPos = 1 ∧ List.map Tape.read (descRun eS tm (List.map (⇑eBit) w) u).1.workTapes = List.replicate k none ∧ (descRun eS tm (List.map (⇑eBit) w) u).2 = List.map (⇑eBit) o

The run of tm on w, from a tidy computation: the description of tm runs, with a transition for every key it meets, until it halts with the input head on the first symbol, blank work tapes and the output b :: v.

theorem Turing.MultiTapeTM.Universal.Desc.computes_dispatch {k : ℕ} {S : Type} [Fintype S] (eS : S ↪ ℕ) (tm : MultiTapeTM k Bool S) (d : Bool → Desc) {w : List Bool} {b : Bool} {v : List Bool} {t₀ s₀ : ℕ} (htm : tm.ComputesTidilyInTimeAndSpace w (b :: v) t₀ s₀) (o : List ℕ) : (dispatch eS tm d).Computes (List.map (⇑eBit) w) o ↔ (d b).Computes (List.map (⇑eBit) v) o

Dispatching on a computed bit: if tm computes b :: v from w tidily, then dispatch eS tm d halts on w with output o exactly when d b halts on v with output o.

The recursion theorem and Rice's theorem

def Turing.MultiTapeTM.behavior (w x : List Bool) (o : List ℕ) : Prop

The behavior, on inputs of bits, of the machine described by the word w: the relation between the inputs on which it halts and the outputs it halts with.

theorem Turing.MultiTapeTM.computableTidilyInPolyTime_selfHardwire : ComputableTidilyInPolyTime (fun (y : List Bool) => Universal.eDesc (Universal.hardwire (Universal.decodeDesc y) (frame y))) encBits encBits

Building the description of a word into itself, as an input prefix, is computable in polynomial time.

theorem Turing.MultiTapeTM.exists_behavior_eq {f : List Bool → Bool} (hf : IsComputable f encBits encBool) (d : Bool → Universal.Desc) : ∃ (e : List Bool), ∀ (x : List Bool) (o : List ℕ), (Universal.decodeDesc e).Computes (List.map (⇑Universal.eBit) x) o ↔ (d (f e)).Computes (List.map (⇑Universal.eBit) x) o

Kleene's recursion theorem, in its two-way case. For every computable verdict f on words and descriptions d false, d true, some word e describes a machine behaving on inputs of bits as d (f e) does: a machine can make its whole behavior depend on a computable verdict about its own description. The full recursion theorem allows any computable transformation of descriptions in place of the choice between d false and d true. The proof is Kleene's construction: a machine reads a word y before its input, computes the verdict on the description of the machine described by y with y built in, and dispatches on it; e is that description for y the description of the machine itself.

theorem Turing.MultiTapeTM.rice {C : Set (List Bool → List ℕ → Prop)} {w₀ w₁ : List Bool} (h₀ : behavior w₀ ∉ C) (h₁ : behavior w₁ ∈ C) : ¬IsDecidable {w : List Bool | behavior w ∈ C} encBits

Rice's theorem. Every nontrivial property of the behavior of machines is undecidable on their descriptions: if C contains the behavior of the machine described by some word and not that of the machine described by another, then the set of words describing machines whose behavior is in C is undecidable Rice Sipser, Problem 5.28.

theorem Turing.MultiTapeTM.not_isDecidable_of_behavior {P : Set (List Bool)} (hP : ∀ (w w' : List Bool), behavior w = behavior w' → w ∈ P → w' ∈ P) {w₀ w₁ : List Bool} (h₀ : w₀ ∉ P) (h₁ : w₁ ∈ P) : ¬IsDecidable P encBits

Rice's theorem, for sets of words. A set of words that holds of a word or not according to the behavior of the machine it describes, and is neither empty nor everything, is undecidable. This is the counterpart of Mathlib's ComputablePred.rice₂ for partial recursive codes.

Halting on a fixed input

theorem Turing.MultiTapeTM.not_isDecidable_halts (x : List Bool) : ¬IsDecidable {w : List Bool | (Universal.decodeDesc w).Halts (List.map (⇑Universal.eBit) x)} encBits

Halting on a fixed input is undecidable: for every input of bits x, no computable function decides, of a word, whether the machine it describes halts on x. This is the native counterpart of Mathlib's ComputablePred.halting_problem, a corollary of Rice's theorem.