Multiplying the block lengths of a pair — proof internals

This module builds the one quadratic-output transducer needed by Cobham's soundness direction: from pair A B it emits |A| · |B| copies of false, which is exactly the length behaviour of Complexity.smash. The soundness proof then applies unaryLength_mem_FP to turn this internal zero-filled ruler into Cobham's all-one smash word.

The machine mulLenTM is self-contained (one work tape, eight control states):

1. scan — parse the leading self-delimiting block two symbols at a time, writing one unary mark on the work tape per payload bit, so the work tape ends up holding |A| in unary;
2. outer loop — for every remaining input symbol (i.e. |B| times) run the emit pass, which walks the |A| marks writing one false per mark, and the rewind pass, which returns the work head to cell one.

Malformed input halts with empty output, matching unpair? = none.

Main results

• Complexity.Cobham.mulUnpair_mem_FP — the block-length product is FP

The function computed by the scanner

def Complexity.Cobham.mulAux (k : ℕ) (w : List Bool) : List Bool

The remaining output of the length-multiplication scanner when k payload bits of the leading block have already been counted and w is the unread part of the input: |A| · |B| copies of false for a well-formed remainder, and nothing at all when the block framing is broken.

Equations

• Complexity.Cobham.mulAux k w = match Complexity.unpair? w with | some (x, y) => List.replicate ((k + x.length) * y.length) false | none => []

def Complexity.Cobham.mulUnpair (p : List Bool) : List Bool

Emit |A| · |B| copies of false from a pair pair A B; the empty string on input that is not a valid pair encoding.

Equations

• Complexity.Cobham.mulUnpair p = Complexity.Cobham.mulAux 0 p

@[simp]

theorem Complexity.Cobham.mulAux_nil (k : ℕ) : mulAux k [] = []

@[simp]

theorem Complexity.Cobham.mulAux_singleton (k : ℕ) (b : Bool) : mulAux k [b] = []

@[simp]

theorem Complexity.Cobham.mulAux_sep (k : ℕ) (z : List Bool) : mulAux k (false :: true :: z) = List.replicate (k * z.length) false

Reaching the separator ends the block: only the suffix remains.

theorem Complexity.Cobham.mulAux_double (k : ℕ) (b : Bool) (z : List Bool) : mulAux k (b :: b :: z) = mulAux (k + 1) z

A doubled payload bit increments the counted length.

@[simp]

theorem Complexity.Cobham.mulAux_broken (k : ℕ) (z : List Bool) : mulAux k (true :: false :: z) = []

A broken doubling halts the scan with no output.

theorem Complexity.Cobham.mulUnpair_pair (A B : List Bool) : mulUnpair (pair A B) = List.replicate (A.length * B.length) false

On a genuine pair the scanner emits |A| · |B| copies of false.

The scanner

inductive Complexity.Cobham.MulPhase : Type

Control states of mulLenTM.

• skip : MulPhase

  Move every head off the left-end marker.

• scanA : MulPhase

  Read the first symbol of a doubled payload bit.

• scanB0 : MulPhase

  The first symbol of the pair was 0.

• scanB1 : MulPhase

  The first symbol of the pair was 1.

• outer : MulPhase

  Consume one symbol of the suffix, or halt at its end.

• emit : MulPhase

  Walk the unary marks, emitting one false per mark.

• rew : MulPhase

  Rewind the work head to cell one.

• done : MulPhase

  Halt.

@[implicit_reducible]

instance Complexity.Cobham.instDecidableEqMulPhase : DecidableEq MulPhase

Equations

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

@[implicit_reducible]

instance Complexity.Cobham.instFintypeMulPhase : Fintype MulPhase

Equations

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

def Complexity.Cobham.mulLenTM : TM 1

The length-multiplication scanner. Parses the leading self-delimiting block into |A| unary marks on its work tape, then emits |A| zeros for each of the |B| remaining input symbols. Computes mulUnpair.

Equations

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

Correctness of the scanner

theorem Complexity.Cobham.mulUnpair_mem_FP : mulUnpair ∈ FP

mulUnpair is polynomial-time, via the mulLenTM scanner.