Iterating circuits

A circuit c with as many outputs as inputs computes a map c.eval I on states. Composing t copies gives c.iterate t, which computes the t-th power of that map (Circuit.eval_iterate); its arbitrary weighted cost and its size are exactly t times those of c (Circuit.cost_program_iterate, Circuit.size_iterate). Zero copies are the identity wiring, with no gates.

When the intermediate states are needed as well, the orbit prefix can be retained within the same budget: Synthesis.orbit makes every state (c.eval I)^[j] (init x) with j ≤ t available at cost t * c.size, sharing each state with every later construction (Synthesis.stages, Synthesis.steps). This uses one copy of c per transition, applied to wires that are already available.

The signature and the carrier are arbitrary. Sizes bound circuits; they do not certify the running time of any construction of them.

Main definitions

• Cslib.Circuits.Circuit.iterate: t copies of a circuit composed in sequence.
• Cslib.Circuits.Synthesis.stages: the values retained through a stage.

Main results

• Cslib.Circuits.Circuit.eval_iterate, Cslib.Circuits.Circuit.cost_program_iterate, Cslib.Circuits.Circuit.size_iterate: exact semantics, weighted cost and size.
• Cslib.Circuits.Synthesis.steps: a sequence of constructions adds its costs.
• Cslib.Circuits.Synthesis.orbit: retain an orbit prefix with one circuit per transition.

References

• Circuit.iterate and its semantics and costs follow Algebraic/Iteration.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib, with Mathlib's Nat.iterate in place of its own function iteration.
• The retained orbits are adapted from lean/Proofs/{Iteration,Synthesis}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

def Cslib.Circuits.Circuit.iterate {σ : Signature} {m : ℕ} (c : Circuit σ m m) : ℕ → Circuit σ m m

t copies of c composed in sequence; zero copies are the identity wiring.

@[simp]

theorem Cslib.Circuits.Circuit.eval_iterate {σ : Signature} {U : Type u} {m : ℕ} (c : Circuit σ m m) (I : Interpretation σ U) (t : ℕ) : (c.iterate t).eval I = (c.eval I)^[t]

Iterating a circuit computes the power of its map.

theorem Cslib.Circuits.Circuit.cost_program_iterate {σ : Signature} {m : ℕ} (c : Circuit σ m m) (t : ℕ) (cost : σ.Op → ℕ) : (c.iterate t).program.cost cost = t * c.program.cost cost

Iterating a circuit multiplies its arbitrary weighted cost exactly.

@[simp]

theorem Cslib.Circuits.Circuit.size_iterate {σ : Signature} {m : ℕ} (c : Circuit σ m m) (t : ℕ) : (c.iterate t).size = t * c.size

Iterating a circuit multiplies its size exactly.

theorem Cslib.Circuits.Circuit.Computes.iterate {σ : Signature} {U : Type u} {m : ℕ} {c : Circuit σ m m} {I : Interpretation σ U} {f : (Fin m → U) → Fin m → U} (hc : c.Computes I f) (t : ℕ) : (c.iterate t).Computes I f^[t]

A circuit computing f iterates to a circuit computing the powers of f.

def Cslib.Circuits.Synthesis.stages {U : Type u} {n : ℕ} (q : ℕ → Set ((Fin n → U) → U)) (t : ℕ) : Set ((Fin n → U) → U)

The values retained through stage t of a straight-line construction.

@[simp]

theorem Cslib.Circuits.Synthesis.stages_zero {U : Type u} {n : ℕ} (q : ℕ → Set ((Fin n → U) → U)) : stages q 0 = q 0

theorem Cslib.Circuits.Synthesis.stages_succ {U : Type u} {n : ℕ} (q : ℕ → Set ((Fin n → U) → U)) (t : ℕ) : stages q (t + 1) = stages q t ∪ q (t + 1)

theorem Cslib.Circuits.Synthesis.subset_stages {U : Type u} {n : ℕ} (q : ℕ → Set ((Fin n → U) → U)) {j t : ℕ} (hj : j ≤ t) : q j ⊆ stages q t

theorem Cslib.Circuits.Synthesis.steps {σ : Signature} {U : Type u} {I : Interpretation σ U} {n : ℕ} {s : Set ((Fin n → U) → U)} (q : ℕ → Set ((Fin n → U) → U)) (C t : ℕ) (hzero : q 0 ⊆ s) (hstep : ∀ j < t, Synthesis I (s ∪ stages q j) (q (j + 1)) C) : Synthesis I s (stages q t) (t * C)

A sequence of t constructions of cost C each costs t * C, and retains every stage.

theorem Cslib.Circuits.Synthesis.orbit {σ : Signature} {U : Type u} {I : Interpretation σ U} {n : ℕ} {s : Set ((Fin n → U) → U)} {m : ℕ} (c : Circuit σ m m) (init : (Fin n → U) → Fin m → U) (hinit : ∀ (i : Fin m), (fun (x : Fin n → U) => init x i) ∈ s) (t : ℕ) : Synthesis I s (stages (fun (j : ℕ) => Set.range fun (i : Fin m) (x : Fin n → U) => (c.eval I)^[j] (init x) i) t) (t * c.size)

Retained orbit prefixes. If every coordinate of the initial state is available, then all coordinates of the states (c.eval I)^[j] (init x) for j ≤ t become available with t * c.size additional gates: one copy of c per transition.