Documentation

Complexity.Computability.Machines.Turing.MultiTape.Plumbing.ExtendTapesView

The view of a configuration through a tape embedding #

For an embedding e : Fin k ↪ Fin k' of work tapes, viewCfg e cfg is the configuration of a machine with k work tapes that sees the tapes e j of cfg. Placing it back with Turing.MultiTapeTM.embed gives cfg (embed_viewCfg), so the run of tm.extendTapes e from any configuration is the run of tm on the view, placed back (runFrom_extendTapes). This generalises Turing.MultiTapeTM.oneTapeCfg and Turing.MultiTapeTM.runFrom_tapeEmb from one tape to any embedding.

Main definitions #

Main results #

source
def Turing.MultiTapeTM.viewCfg {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (e : Fin k ↪ Fin k') (cfg : Cfg k' Symbol State input) :
Cfg k Symbol State input

The configuration of a machine with k work tapes seeing the tapes e j of cfg.

Instances For
    source
    theorem Turing.MultiTapeTM.embed_viewCfg {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (e : Fin k ↪ Fin k') (cfg : Cfg k' Symbol State input) :
    embed e (viewCfg e cfg) cfg.workTapes cfg.workTapePos = cfg

    A configuration is its view through e, placed back on the tapes e j.

    source
    theorem Turing.MultiTapeTM.runFrom_extendTapes {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') (cfg : Cfg k' Symbol State input) (n : ℕ) :
    runFrom cfg n = embed e (runFrom (viewCfg e cfg) n) cfg.workTapes cfg.workTapePos

    Running a machine on the tapes selected by an embedding. The run is the run on the view of the configuration, placed back on the selected tapes; every other tape and head keeps its starting value.

    source
    theorem Turing.MultiTapeTM.space_extendTapes_le {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') (cfg : Cfg k' Symbol State input) (n : ℕ) :
    space cfg n ≤ space (viewCfg e cfg) n + (k' - k)

    Space of a machine run on the tapes selected by an embedding: the space of the run on the view, plus one cell for each tape the machine does not use.

    source
    theorem Turing.MultiTapeTM.embed_castAdd {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) (tapes : Fin (k + k') → ℤ → Option Symbol) (heads : Fin (k + k') → ℤ) :
    embed (Fin.castAddEmb k') cfg tapes heads = { state := cfg.state, inputPos := cfg.inputPos, workTapes := Fin.append cfg.workTapes fun (i : Fin k') => tapes (Fin.natAdd k i), workTapePos := Fin.append cfg.workTapePos fun (i : Fin k') => heads (Fin.natAdd k i), output := cfg.output }

    Placing a configuration before a block of extra tapes gives an appended family.

    source
    theorem Turing.MultiTapeTM.embed_natAdd {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) (tapes : Fin (k' + k) → ℤ → Option Symbol) (heads : Fin (k' + k) → ℤ) :
    embed (Fin.natAddEmb k') cfg tapes heads = { state := cfg.state, inputPos := cfg.inputPos, workTapes := Fin.append (fun (i : Fin k') => tapes (Fin.castAdd k i)) cfg.workTapes, workTapePos := Fin.append (fun (i : Fin k') => heads (Fin.castAdd k i)) cfg.workTapePos, output := cfg.output }

    Placing a configuration after a block of extra tapes gives an appended family.

    source
    theorem Turing.MultiTapeTM.embed_castSucc {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (cfg : Cfg k Symbol State input) (tapes : Fin (k + 1) → ℤ → Option Symbol) (heads : Fin (k + 1) → ℤ) :
    embed Fin.castSuccEmb cfg tapes heads = { state := cfg.state, inputPos := cfg.inputPos, workTapes := fun (i : Fin (k + 1)) => Fin.lastCases (motive := fun (x : Fin (k + 1)) => ℤ → Option Symbol) (tapes (Fin.last k)) cfg.workTapes i, workTapePos := fun (i : Fin (k + 1)) => Fin.lastCases (heads (Fin.last k)) cfg.workTapePos i, output := cfg.output }

    Reserving one last tape is the corresponding Fin.lastCases family.