Machines that diverge on a verdict

A machine computing a total function can compute a partial one: let the first symbol it emits be a verdict. tm.partialize runs tm, but reads the first emitted symbol as a verdict instead of emitting it. After the verdict true it emits nothing, and once tm halts it loops forever in a state of its own; after the verdict false it emits the rest of the output of tm and halts with tm. So if tm halts with the output encPartial r on an input, encoding the divergence r = none as [true] and an output r = some o as false :: o, then tm.partialize diverges on that input when r = none and halts with output o when r = some o (Turing.MultiTapeTM.Computes.partialize).

The proof is a step-by-step correspondence: the configurations of tm.partialize are images of the configurations of tm under a map commuting with the steps (Turing.MultiTapeTM.Partialize.step_liftCfg), so its runs are the images of the runs of tm (Turing.MultiTapeTM.runFrom_partialize).

Main definitions

• Turing.MultiTapeTM.partialize: the machine diverging on the verdict true.
• Turing.MultiTapeTM.encPartial: partial results as words.

Main results

• Turing.MultiTapeTM.runFrom_partialize: the runs of tm.partialize.
• Turing.MultiTapeTM.Computes.partialize, Turing.MultiTapeTM.Computes.halts_partialize: tm.partialize computes the partial result encoded by the output of tm.

References

• M. Sipser, Introduction to the Theory of Computation, Section 3.1

def Turing.MultiTapeTM.Partialize.verdict (out : List Bool) : Option Bool

The verdict read from an output: its first symbol, if any.

def Turing.MultiTapeTM.Partialize.strip : List Bool → List Bool

What follows the verdict false in an output; nothing before a verdict or after the verdict true.

def Turing.MultiTapeTM.Partialize.liftState {State : Type u_1} : Option State → Option Bool → Option (Option State × Option Bool)

The state of tm.partialize for a state of tm and a verdict: a running state is kept with the verdict; once tm halts, the verdict true loops in the state (none, some true) and every other verdict halts.

theorem Turing.MultiTapeTM.Partialize.verdict_append (out : List Bool) (o : Option Bool) : verdict (out ++ o.toList) = (verdict out).or o

Emitting a symbol fixes the verdict if there was none.

theorem Turing.MultiTapeTM.Partialize.strip_append (out : List Bool) (o : Option Bool) : strip (out ++ o.toList) = strip out ++ (if verdict out = some false then o else none).toList

Emitting a symbol extends what follows the verdict only after the verdict false.

noncomputable def Turing.MultiTapeTM.partialize {k : ℕ} {State : Type u_1} (tm : MultiTapeTM k Bool State) : MultiTapeTM k Bool (Option State × Option Bool)

tm.partialize runs tm, reading the first symbol it emits as a verdict. After the verdict true it emits nothing, and once tm halts it loops forever in the state (none, some true). After the verdict false it emits the rest of the output of tm and halts with tm. The second component of a state is the verdict read so far.

def Turing.MultiTapeTM.Partialize.liftCfg {k : ℕ} {State : Type u_1} {input : List Bool} (c : Cfg k Bool State input) : Cfg k Bool (Option State × Option Bool) input

The configuration of tm.partialize corresponding to a configuration of tm: the state carries the verdict of the output, and the output keeps what follows the verdict false.

theorem Turing.MultiTapeTM.Partialize.inputSymbol_liftCfg {k : ℕ} {State : Type u_1} {input : List Bool} (c : Cfg k Bool State input) : (liftCfg c).inputSymbol = c.inputSymbol

The symbol under the input head is that of tm.

theorem Turing.MultiTapeTM.Partialize.workTapeSymbols_liftCfg {k : ℕ} {State : Type u_1} {input : List Bool} (c : Cfg k Bool State input) : (liftCfg c).workTapeSymbols = c.workTapeSymbols

The symbols under the work-tape heads are those of tm.

theorem Turing.MultiTapeTM.Partialize.step_liftCfg {k : ℕ} {State : Type u_1} {input : List Bool} (tm : MultiTapeTM k Bool State) (c : Cfg k Bool State input) : step (liftCfg c) = liftCfg (step c)

tm.partialize steps along tm.

theorem Turing.MultiTapeTM.Partialize.liftCfg_halted_iff {k : ℕ} {State : Type u_1} {input : List Bool} (c : Cfg k Bool State input) : (liftCfg c).Halted ↔ c.Halted ∧ verdict c.output ≠ some true

tm.partialize has halted when tm has, unless the verdict is true.

@[simp]

theorem Turing.MultiTapeTM.Partialize.output_liftCfg {k : ℕ} {State : Type u_1} {input : List Bool} (c : Cfg k Bool State input) : (liftCfg c).output = strip c.output

theorem Turing.MultiTapeTM.runFrom_partialize {k : ℕ} {State : Type u_1} (tm : MultiTapeTM k Bool State) (input : List Bool) (t : ℕ) : runFrom (tm.partialize.initCfg input) t = Partialize.liftCfg (runFrom (tm.initCfg input) t)

The runs of tm.partialize are the images of the runs of tm.

def Turing.MultiTapeTM.encPartial : Option (List Bool) ↪ List Bool

Partial results as words: the divergence none as [true], the output some o as false :: o.

@[simp]

theorem Turing.MultiTapeTM.encPartial_none : encPartial none = [true]

@[simp]

theorem Turing.MultiTapeTM.encPartial_some (o : List Bool) : encPartial (some o) = false :: o

theorem Turing.MultiTapeTM.Computes.partialize {k : ℕ} {State : Type u_1} {tm : MultiTapeTM k Bool State} {input : List Bool} {r : Option (List Bool)} (h : tm.Computes input (encPartial r)) (o : List Bool) : tm.partialize.Computes input o ↔ o ∈ r

tm.partialize computes the partial result encoded by the output of tm: if tm halts with output encPartial r, then tm.partialize halts with output o exactly when r = some o, and diverges when r = none.

theorem Turing.MultiTapeTM.Computes.halts_partialize {k : ℕ} {State : Type u_1} {tm : MultiTapeTM k Bool State} {input : List Bool} {r : Option (List Bool)} (h : tm.Computes input (encPartial r)) : tm.partialize.Halts input ↔ r.isSome = true

If tm halts with output encPartial r, then tm.partialize halts exactly when r is a result.