Deterministic unrolling families — definitions

This module packages the bounded acceptance circuit of a deterministic Turing machine at every input length. The embedded NTM ignores its choice bits, so the family fixes them all to false and leaves only the ordinary data input live.

The length-zero output is the same bounded trace predicate evaluated directly; the construction therefore depends only on the machine and time horizon, not on a target language or correctness proof.

noncomputable def Complexity.TM.unrollingCircuitFamily {k : ℕ} (tm : TM k) (f : ℕ → ℕ) : CircuitFamily Basis.andOr2

The nonuniform circuit family obtained by unrolling tm through the exact horizon f n and fixing the choice bits of tm.toNTM to false.

Equations

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