Polynomial-time circuit depths

The raw depth computation uses binary wire indices, unary input count, and unary computed depths. A prefix of k gates has n + k depth entries, all at most k, so its full framed encoding has length at most (n + k) * (2 * k + 1). This bound also holds on malformed code: missing arguments and unavailable wires read zero. Binary lookups cap the index before converting it to unary, so a large invalid index is charged only its binary encoded length.

Main results

• Cslib.Circuits.Boolean.computableInPolyTime_wireDepthsCode: compute the entire table.
• Cslib.Circuits.Boolean.computableInPolyTime_depthCode: compute the maximum depth of the designated outputs, including their binary lookups.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

theorem Cslib.Circuits.Boolean.computableInPolyTime_wireDepthsCode {α : Type} {input : α ↪ List Bool} {inputCount : α → ℕ} {gates : α → List (Op × List ℕ)} (hn : Turing.MultiTapeTM.ComputableInPolyTime inputCount input Turing.MultiTapeTM.encUnary) (hgates : Turing.MultiTapeTM.ComputableInPolyTime gates input (Turing.MultiTapeTM.encList encGate)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => wireDepthsCode (inputCount a) (gates a)) input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary)

Compute all wire depths, charging every unary depth and list delimiter. The gate code may be malformed, and its wire indices retain their binary encoding.

theorem Cslib.Circuits.Boolean.computableInPolyTime_depthCode {α : Type} {input : α ↪ List Bool} {inputCount : α → ℕ} {code : α → List (Op × List ℕ) × List ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime inputCount input Turing.MultiTapeTM.encUnary) (hcode : Turing.MultiTapeTM.ComputableInPolyTime code input encCode) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => depthCode (inputCount a) (code a)) input Turing.MultiTapeTM.encUnary

Compute the designated-output maximum. Both construction of the table and every binary output lookup are charged; no validity or promised-depth hypothesis is needed.