The bit successor — proof internals

Cobham.consBitTM b prepends the fixed bit b to its input: the machine behind the bit constructor of Cobham's algebra.

Main results

• Cobham.cons_mem_FP — prepending a fixed bit is in FP

The bit-successor transducer

A small machine computing x ↦ b :: x: skip the left marker, emit b, then copy the input verbatim after it. Modelled on TM.copyInputToOutputTM.

inductive Complexity.Cobham.ConsPhase : Type

Control states of consBitTM: skip the ▷ marker, emit the fixed bit, copy the input, halt.

• skip : ConsPhase
• emit : ConsPhase
• copy : ConsPhase
• done : ConsPhase

@[implicit_reducible]

instance Complexity.Cobham.instDecidableEqConsPhase : DecidableEq ConsPhase

Equations

• Complexity.Cobham.instDecidableEqConsPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.Cobham.instFintypeConsPhase : Fintype ConsPhase

Equations

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

def Complexity.Cobham.consBitTM (b : Bool) : TM 0

The bit-successor machine: on input x it writes b :: x to the output tape in |x| + 3 steps. First skip advances past the left markers, emit writes b into output cell 1, and copy copies the input bits after it.

Equations

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

theorem Complexity.Cobham.consBitTM_computesInTime (b : Bool) : (consBitTM b).ComputesInTime (fun (x : List Bool) => b :: x) fun (m : ℕ) => m + 3

consBitTM b computes x ↦ b :: x within the linear bound |x| + 3.

theorem Complexity.Cobham.cons_mem_FP (b : Bool) : (fun (x : List Bool) => b :: x) ∈ FP

Prepending a fixed bit is polynomial-time — the string-successor underlying the bit constructor. Witnessed by consBitTM.