Encoding the start of a nondeterministic path

NTM.choiceTM runs one path of a nondeterministic machine deterministically, reading its choice bits from the last work tape. To simulate such a run inside Cobham's algebra, the starting configuration must be encoded with the choice string already on that tape and its head parked on the first bit.

This file supplies that encoder — Cobham.initChoiceFn, the counterpart of Cobham.initFn — together with its algebra membership and the identification with Cobham.cfgCode of the intended configuration.

Main definitions

• Cobham.choiceTape — the choice string on a tape, head at cell 1
• Cobham.choiceCfg — the starting configuration of NTM.choiceTM
• Cobham.initChoiceFn — its encoding, as a function of the two strings

Main results

• Cobham.initChoiceFn_mem — the encoder is in the algebra
• Cobham.initChoiceFn_eq — the encoder computes cfgCode of choiceCfg
• Cobham.dropChoice_choiceCfg — forgetting the choice tape gives the nondeterministic machine's own initial configuration

def Complexity.Cobham.choiceTape (c : List Bool) : Tape

The choice string on a tape, with the head parked on the first bit.

Equations

• Complexity.Cobham.choiceTape c = { head := 1, cells := (Complexity.Tape.init (List.map Complexity.Γ.ofBool c)).cells }

@[simp]

theorem Complexity.Cobham.choiceTape_head (c : List Bool) : (choiceTape c).head = 1

@[simp]

theorem Complexity.Cobham.choiceTape_cells (c : List Bool) : (choiceTape c).cells = (Tape.init (List.map Γ.ofBool c)).cells

noncomputable def Complexity.Cobham.choiceCfg {k : ℕ} (tm : NTM k) (x c : List Bool) : Cfg (k + 1) tm.Q

The starting configuration of NTM.choiceTM tm: the input on the input tape, the choice string on the appended choice tape.

Equations

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

@[simp]

theorem Complexity.Cobham.dropChoice_choiceCfg {k : ℕ} (tm : NTM k) (x c : List Bool) : NTM.dropChoice (choiceCfg tm x c) = tm.initCfg x

Forgetting the choice tape gives the nondeterministic machine's own initial configuration.

noncomputable def Complexity.Cobham.initChoiceFn {k : ℕ} (tm : NTM k) (R x c : List Bool) : List Bool

The encoded starting configuration of a nondeterministic path. Everything but the input tape's and the choice tape's right half-blocks is a constant of the machine.

Equations

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

theorem Complexity.Cobham.initChoiceFn_mem {k n : ℕ} (tm : NTM k) {gR gx gc : (Fin n → List Bool) → List Bool} (hR : Cobham gR) (hx : Cobham gx) (hc : Cobham gc) : Cobham fun (v : Fin n → List Bool) => initChoiceFn tm (gR v) (gx v) (gc v)

The encoder is in the algebra.

theorem Complexity.Cobham.initChoiceFn_eq {k : ℕ} (tm : NTM k) (W : ℕ) (x c : List Bool) (hx : x.length ≤ W) (hc : c.length ≤ W) : initChoiceFn tm (blockRuler W) x c = cfgCode W (choiceCfg tm x c)

The encoder computes the encoding of the starting configuration.

Iterating the encoded step from a choice configuration

theorem Complexity.Cobham.runCfg_choiceCfg_startInvariant {k : ℕ} (tm : NTM k) (x c : List Bool) (n : ℕ) : (tm.choiceTM.runCfg (choiceCfg tm x c) n).input.StartInvariant ∧ (∀ (i : Fin (k + 1)), ((tm.choiceTM.runCfg (choiceCfg tm x c) n).work i).StartInvariant) ∧ (tm.choiceTM.runCfg (choiceCfg tm x c) n).output.StartInvariant

Every tape of a run from a choice configuration keeps its left-end marker.

theorem Complexity.Cobham.runCfg_choiceCfg_head_le {k : ℕ} (tm : NTM k) (x c : List Bool) (n : ℕ) : (tm.choiceTM.runCfg (choiceCfg tm x c) n).input.head ≤ n + 1 ∧ (∀ (i : Fin (k + 1)), ((tm.choiceTM.runCfg (choiceCfg tm x c) n).work i).head ≤ n + 1) ∧ (tm.choiceTM.runCfg (choiceCfg tm x c) n).output.head ≤ n + 1

After n steps of a run from a choice configuration every head is within n + 1 cells of the start: the choice head begins one cell in.

theorem Complexity.Cobham.cfgTapes_runCfg_choiceCfg_inv {k : ℕ} (tm : NTM k) (x c : List Bool) (n W : ℕ) (hn : n + 1 ≤ W) : (∀ t ∈ cfgTapes (tm.choiceTM.runCfg (choiceCfg tm x c) n), t.StartInvariant) ∧ ∀ t ∈ cfgTapes (tm.choiceTM.runCfg (choiceCfg tm x c) n), t.head ≤ W

The invariants of a choice run, in the form the encoding lemmas want.

theorem Complexity.Cobham.iterate_stepFn_choice {k : ℕ} (tm : NTM k) (W : ℕ) (x c : List Bool) (hq : Fintype.card tm.Q ≤ blockWidth W) (n : ℕ) : n + 1 ≤ W → (stepFn tm.choiceTM (blockRuler W))^[n] (cfgCode W (choiceCfg tm x c)) = cfgCode W (tm.choiceTM.runCfg (choiceCfg tm x c) n)

The encoded iteration tracks a choice run.

Running the path inside the algebra

@[simp]

theorem Complexity.Cobham.initChoiceFn_length {k : ℕ} (tm : NTM k) (R x c : List Bool) : (initChoiceFn tm R x c).length = (2 * (k + 3) + 1) * R.length

theorem Complexity.Cobham.iterate_stepFn_choice_length_le {k : ℕ} (tm : NTM k) (R x c : List Bool) (n : ℕ) : ((stepFn tm.choiceTM R)^[n] (initChoiceFn tm R x c)).length ≤ (2 * (k + 3) + 1) * R.length

The encoded run stays inside its blocks.

noncomputable def Complexity.Cobham.runChoiceFn {k : ℕ} (tm : NTM k) (u x c : List Bool) : List Bool

The encoded configuration after running the path for |c| steps, under a ruler derived from the clock string u.

Equations

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

theorem Complexity.Cobham.runChoiceFn_mem {k n : ℕ} (tm : NTM k) {gu gx gc : (Fin n → List Bool) → List Bool} (hu : Cobham gu) (hx : Cobham gx) (hc : Cobham gc) : Cobham fun (v : Fin n → List Bool) => runChoiceFn tm (gu v) (gx v) (gc v)

Running the path is in the algebra.

Reading the verdict

noncomputable def Complexity.Cobham.outPairChoiceFn {k : ℕ} (tm : NTM k) (u x c : List Bool) : List Bool

The output tape's two half-blocks after the run, rewound to cell 0.

Equations

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

theorem Complexity.Cobham.outPairChoiceFn_mem {k n : ℕ} (tm : NTM k) {gu gx gc : (Fin n → List Bool) → List Bool} (hu : Cobham gu) (hx : Cobham gx) (hc : Cobham gc) : Cobham fun (v : Fin n → List Bool) => outPairChoiceFn tm (gu v) (gx v) (gc v)

The rewind stage is in the algebra.

noncomputable def Complexity.Cobham.acceptChoiceFn {k : ℕ} (tm : NTM k) (u x c : List Bool) : List Bool

The verdict of the path: the machine halted with 1 on output cell 1.

Equations

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

theorem Complexity.Cobham.acceptChoiceFn_flag {k : ℕ} (tm : NTM k) (u x c : List Bool) : acceptChoiceFn tm u x c = [true] ∨ acceptChoiceFn tm u x c = [false]

The verdict is a genuine one-bit flag.

theorem Complexity.Cobham.acceptChoiceFn_mem {k n : ℕ} (tm : NTM k) {gu gx gc : (Fin n → List Bool) → List Bool} (hu : Cobham gu) (hx : Cobham gx) (hc : Cobham gc) : Cobham fun (v : Fin n → List Bool) => acceptChoiceFn tm (gu v) (gx v) (gc v)

The verdict is in the algebra.

The run is the nondeterministic trace

theorem Complexity.Cobham.choiceStream_choiceCfg {k : ℕ} (tm : NTM k) (x c : List Bool) (j : ℕ) (hj : j < c.length) : NTM.choiceStream (choiceCfg tm x c) j = c[j]

The choice bits found on the choice tape are the bits of c.

theorem Complexity.Cobham.dropChoice_runCfg_choiceCfg {k : ℕ} (tm : NTM k) (T : ℕ) (x c : List Bool) : NTM.dropChoice (tm.choiceTM.runCfg (choiceCfg tm x c) T) = tm.trace T (fun (j : Fin T) => NTM.choiceStream (choiceCfg tm x c) ↑j) (tm.initCfg x)

The deterministic run from a choice configuration is the trace.

The verdict is the path's verdict

def Complexity.Cobham.PathAccepts {k : ℕ} (tm : NTM k) (x c : List Bool) : Prop

The predicate the verdict computes: after |c| steps along the choice bits of c, the machine has halted with 1 on the first output cell.

Equations

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

theorem Complexity.Cobham.acceptChoiceFn_eq_true_iff {k : ℕ} (tm : NTM k) (u x c : List Bool) (hlen : x.length + c.length + Fintype.card tm.Q + 3 ≤ u.length) : acceptChoiceFn tm u x c = [true] ↔ PathAccepts tm x c

The algebra's verdict is the path's verdict.