Work-tape placement

This file defines a layout combinator that places the work tapes of a machine inside a larger, contiguous middle block. The surrounding physical tapes are idled, so later phases can reserve disjoint tape regions without changing the source machine.

Main definitions

• TM.placeWorkIdx — physical index of a source work tape
• TM.placeWorkCoord — source coordinate of a physical middle-block tape
• TM.placeWorkTM — place a machine between pre prefix and post suffix tapes
• TM.placeWorkCfg — embed a configuration with an arbitrary extra-tape frame
• TM.placeWorkFrameStep — one idle action on every physical frame tape
• TM.placeWorkParkedCfg — the canonical embedding with parked blank extras

def Complexity.TM.placeWorkIdx {n : ℕ} (pre post : ℕ) (i : Fin n) : Fin (pre + n + post)

Physical work-tape index occupied by source work tape i after placement.

Equations

• Complexity.TM.placeWorkIdx pre post i = ⟨pre + ↑i, ⋯⟩

def Complexity.TM.placeWorkInMiddle (pre n : ℕ) {post : ℕ} (i : Fin (pre + n + post)) : Prop

A physical work tape lies in the block occupied by the source machine.

Equations

• Complexity.TM.placeWorkInMiddle pre n i = (pre ≤ ↑i ∧ ↑i < pre + n)

@[implicit_reducible]

instance Complexity.TM.instDecidablePlaceWorkInMiddle (pre n : ℕ) {post : ℕ} (i : Fin (pre + n + post)) : Decidable (placeWorkInMiddle pre n i)

Equations

• Complexity.TM.instDecidablePlaceWorkInMiddle pre n i = id inferInstance

def Complexity.TM.placeWorkCoord (pre n : ℕ) {post : ℕ} (i : Fin (pre + n + post)) (h : placeWorkInMiddle pre n i) : Fin n

Source coordinate corresponding to a physical tape in the middle block.

Equations

• Complexity.TM.placeWorkCoord pre n i h = ⟨↑i - pre, ⋯⟩

@[simp]

theorem Complexity.TM.placeWorkIdx_val {n : ℕ} (pre post : ℕ) (i : Fin n) : ↑(placeWorkIdx pre post i) = pre + ↑i

@[simp]

theorem Complexity.TM.placeWorkInMiddle_placeWorkIdx {n : ℕ} (pre post : ℕ) (i : Fin n) : placeWorkInMiddle pre n (placeWorkIdx pre post i)

@[simp]

theorem Complexity.TM.placeWorkCoord_placeWorkIdx {n : ℕ} (pre post : ℕ) (i : Fin n) : placeWorkCoord pre n (placeWorkIdx pre post i) ⋯ = i

theorem Complexity.TM.placeWorkIdx_placeWorkCoord {n pre post : ℕ} (i : Fin (pre + n + post)) (h : placeWorkInMiddle pre n i) : placeWorkIdx pre post (placeWorkCoord pre n i h) = i

theorem Complexity.TM.placeWorkIdx_injective {n : ℕ} (pre post : ℕ) : Function.Injective (placeWorkIdx pre post)

def Complexity.TM.placeWorkTM {n : ℕ} (pre post : ℕ) (tm : TM n) : TM (pre + n + post)

Place tm after pre reserved work tapes and before post reserved work tapes. Physical tapes in the middle block simulate tm; every other work tape writes back the symbol it reads and idles. Input and output actions are unchanged.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.placeWorkCfg {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) (c : Cfg n tm.Q) : Cfg (pre + n + post) (placeWorkTM pre post tm).Q

Embed c into the placed layout. The supplied physical extras frame is used outside the middle block and ignored inside it.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.placeWorkFrameStep {pre n post : ℕ} (extras : Fin (pre + n + post) → Tape) : Fin (pre + n + post) → Tape

Apply the placement machine's idle work-tape action to an extra-tape frame. Only values outside the middle block are observable through placeWorkCfg.

Equations

• Complexity.TM.placeWorkFrameStep extras i = (extras i).writeAndMove (Complexity.TM.readBackWrite (extras i).read).toΓ (Complexity.TM.idleDir (extras i).read)

def Complexity.TM.placeWorkParkedCfg {n : ℕ} (tm : TM n) (pre post : ℕ) (c : Cfg n tm.Q) : Cfg (pre + n + post) (placeWorkTM pre post tm).Q

Canonical embedding whose prefix and suffix tapes are parked and blank.

Equations

• tm.placeWorkParkedCfg pre post c = tm.placeWorkCfg pre post (fun (x : Fin (pre + n + post)) => (Complexity.Tape.init []).move Complexity.Dir3.right) c

@[simp]

theorem Complexity.TM.placeWorkCfg_state {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) (c : Cfg n tm.Q) : (tm.placeWorkCfg pre post extras c).state = c.state

@[simp]

theorem Complexity.TM.placeWorkCfg_input {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) (c : Cfg n tm.Q) : (tm.placeWorkCfg pre post extras c).input = c.input

@[simp]

theorem Complexity.TM.placeWorkCfg_output {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) (c : Cfg n tm.Q) : (tm.placeWorkCfg pre post extras c).output = c.output

@[simp]

theorem Complexity.TM.placeWorkCfg_work_middle {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) (c : Cfg n tm.Q) (i : Fin n) : (tm.placeWorkCfg pre post extras c).work (placeWorkIdx pre post i) = c.work i

theorem Complexity.TM.placeWorkCfg_work_extra {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) (c : Cfg n tm.Q) (i : Fin (pre + n + post)) (h : ¬placeWorkInMiddle pre n i) : (tm.placeWorkCfg pre post extras c).work i = extras i

theorem Complexity.TM.placeWorkCfg_work_prefix {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) (c : Cfg n tm.Q) (i : Fin pre) : (tm.placeWorkCfg pre post extras c).work ⟨↑i, ⋯⟩ = extras ⟨↑i, ⋯⟩

theorem Complexity.TM.placeWorkCfg_work_suffix {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) (c : Cfg n tm.Q) (i : Fin post) : (tm.placeWorkCfg pre post extras c).work ⟨pre + n + ↑i, ⋯⟩ = extras ⟨pre + n + ↑i, ⋯⟩