Restricting a single-tape machine to a supporting set of states

DefinitionRestriction of a single-tape machine to a supporting set of states#✓fully proved

Let \(M\) be a single-tape Turing machine with tape alphabet \(\Gamma\) and states \(\Lambda\), and let \(S \subseteq \Lambda\) support \(M\): \(S\) contains the default state and every transition of \(M\) from a state in \(S\) leads to a state in \(S\). The restriction of \(M\) to \(S\) is the machine with states \(S\) that, in state \(q \in S\) reading \(a\), does what \(M\) does in state \(q\) reading \(a\): it halts if \(M\) halts, and otherwise performs the same action and moves to the same next state, which lies in \(S\).

def restrict (hS : TM0.Supports M S) : TM0.Machine Γ S := fun q a ↦
  (M q a).pbind fun p hp ↦ some (⟨p.1, hS.2 hp q.2⟩, p.2)

Used by 4

Used byThe restricted machine evaluates like the original · The original machine simulates the restricted one step for step · Some finite Thue system has an undecidable word problem · Reachability for string rewriting is undecidable

DefinitionForgetting the restriction on a configuration#✓fully proved

Let \(S\) be a set of states of a single-tape Turing machine with tape alphabet \(\Gamma\) and states \(\Lambda\). A configuration with state \(q \in S\) and tape \(T\) is sent to the configuration with state \(q\), viewed as an element of \(\Lambda\), and the same tape \(T\).

def cfgVal (c : TM0.Cfg Γ S) : TM0.Cfg Γ Λ := ⟨c.q.1, c.Tape⟩

Used by 2

Used byThe restricted machine evaluates like the original · The original machine simulates the restricted one step for step

TheoremThe original machine simulates the restricted one step for step#✓fully proved

Let \(S\) be a set of states supporting a single-tape Turing machine \(M\), and relate a configuration of the restriction of \(M\) to \(S\) to the configuration of \(M\) with the same state, viewed as a state of \(M\), and the same tape. Suppose the configuration \(c\) of the restricted machine is related to the configuration \(d\) of \(M\). If the restricted machine steps from \(c\) to \(c'\), then \(M\) reaches, in one or more steps from \(d\), the configuration related to \(c'\). If the restricted machine has no step from \(c\), then \(M\) has no step from \(d\).

theorem respects (hS : TM0.Supports M S) :
    StateTransition.Respects (TM0.step (restrict hS)) (TM0.step M) fun a b ↦ cfgVal a = b

Uses 2 · Used by 1

Statement usesForgetting the restriction on a configuration · Restriction of a single-tape machine to a supporting set of states

Used byThe restricted machine evaluates like the original

TheoremThe restricted machine evaluates like the original#✓fully proved

Let \(M\) be a single-tape Turing machine with tape alphabet \(\Gamma\) and states \(\Lambda\), and let \(S \subseteq \Lambda\) be a set of states that supports \(M\): it contains the default state and is closed under the transitions of \(M\). If the default state of the restriction of \(M\) to \(S\) is the default state of \(M\), then for every input list \(l\) over \(\Gamma\) the evaluation of the restricted machine on \(l\) equals that of \(M\): either both fail to halt, or both halt with the same output.

theorem eval_restrict (hS : TM0.Supports M S) (hdef : (default : S).1 = default) (l : List Γ) :
    TM0.eval (restrict hS) l = TM0.eval M l

Uses 3 · Used by 2

Statement usesRestriction of a single-tape machine to a supporting set of states

Proof usesForgetting the restriction on a configuration · The original machine simulates the restricted one step for step

Used bySome finite Thue system has an undecidable word problem · Reachability for string rewriting is undecidable

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.