Circuits for first targets and halting

Let c compute f on n-bit states and let a circuit p recognize a target set. Stopping at targets is computed by a circuit of size c.size + p.size + 4 * n (absorbing_circuit), and 2 ^ n steps of it reach the first target of every orbit that has one (FunctionalGraph.absorb_iterate_card). With the fixed-power bound this gives the first target state (first_target_state) and whether a target is ever reached (target_reachability). When the halting states are fixed by f itself, 2 ^ n steps of f reach the halting configuration of every halting computation, and no recognizer is charged (halting_computation).

The first visit to a target is the transient depth of the map that stops at targets (FunctionalGraph.first_target_depth), so the depth circuits give a reachability flag and the exact first target time (first_target_time, first_target_time_optimized), and the first halting time (halting_time).

The circuits are native De Morgan circuits: every NOT, AND and OR gate and every constant is charged, while wiring and fanout are free. They exist for each parameter choice; nothing here bounds the time to construct them. For halting computations the state holds every persistent bit of the computation, including its input and workspace.

Main results

• Cslib.Circuits.Boolean.Iteration.absorbing_circuit: stopping at recognized targets.
• Cslib.Circuits.Boolean.Iteration.first_target_state, Cslib.Circuits.Boolean.Iteration.target_reachability: first targets and reachability.
• Cslib.Circuits.Boolean.Iteration.halting_computation: final configurations.
• Cslib.Circuits.Boolean.Iteration.first_target_time, Cslib.Circuits.Boolean.Iteration.first_target_time_optimized: first target times.
• Cslib.Circuits.Boolean.Iteration.halting_time: first halting times.

References

• Adapted from lean/Proofs/{Targets,TargetTimes}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions, whose first-time and halting-time bounds have the constants 3120000 and 3000000.

theorem Cslib.Circuits.Boolean.Iteration.absorbing_circuit {n : ℕ} (c : Circuit signature n n) (p : Circuit signature n 1) : ∃ (g : Circuit signature n n), g.Computes interpretation (FunctionalGraph.absorb (c.eval interpretation) fun (x : Fin n → Bool) => p.eval interpretation x 0 = true) ∧ g.size ≤ c.size + p.size + 4 * n

Absorbing targets. The map that stops at states accepted by p and otherwise applies c has a circuit of size at most c.size + p.size + 4 * n.

theorem Cslib.Circuits.Boolean.Iteration.first_target_state {n : ℕ} (c : Circuit signature n n) (p : Circuit signature n 1) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n n), (∀ (x : Fin n → Bool), p.eval interpretation (out.eval interpretation x) 0 = true ↔ ∃ (t : ℕ), p.eval interpretation ((c.eval interpretation)^[t] x) 0 = true) ∧ (∀ (x : Fin n → Bool), (∃ (t : ℕ), p.eval interpretation ((c.eval interpretation)^[t] x) 0 = true) → ∃ t < 2 ^ n, out.eval interpretation x = (c.eval interpretation)^[t] x ∧ p.eval interpretation ((c.eval interpretation)^[t] x) 0 = true ∧ ∀ j < t, p.eval interpretation ((c.eval interpretation)^[j] x) 0 ≠ true) ∧ out.size ≤ 40000 * powerBudget n (c.size + p.size + 4 * n) (2 ^ n) L

First target states. For every 0 < L ≤ 2 ^ n, some circuit of size at most 40000 * powerBudget n (c.size + p.size + 4 * n) (2 ^ n) L returns a state accepted by p exactly when the orbit of its input ever reaches one, and then returns the first such state, reached before time 2 ^ n.

theorem Cslib.Circuits.Boolean.Iteration.target_reachability {n : ℕ} (c : Circuit signature n n) (p : Circuit signature n 1) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n 1), (∀ (x : Fin n → Bool), out.eval interpretation x 0 = true ↔ ∃ (t : ℕ), p.eval interpretation ((c.eval interpretation)^[t] x) 0 = true) ∧ out.size ≤ 40000 * powerBudget n (c.size + p.size + 4 * n) (2 ^ n) L + p.size

Target reachability. For every 0 < L ≤ 2 ^ n, some circuit of size at most 40000 * powerBudget n (c.size + p.size + 4 * n) (2 ^ n) L + p.size decides whether the orbit of its input ever reaches a state accepted by p.

theorem Cslib.Circuits.Boolean.Iteration.halting_computation {n : ℕ} (c : Circuit signature n n) (H : BitString n → Prop) (initial : Set (BitString n)) (hstop : ∀ (x : BitString n), H x → c.eval interpretation x = x) (hhalt : ∀ x ∈ initial, ∃ (t : ℕ), H ((c.eval interpretation)^[t] x)) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n n), (∀ x ∈ initial, H (out.eval interpretation x) ∧ ∃ t < 2 ^ n, out.eval interpretation x = (c.eval interpretation)^[t] x ∧ ∀ j < t, ¬H ((c.eval interpretation)^[j] x)) ∧ out.size ≤ 40000 * powerBudget n c.size (2 ^ n) L

Halting computations. If c fixes every halting state and the orbit of every initial state halts, then for every 0 < L ≤ 2 ^ n some circuit of size at most 40000 * powerBudget n c.size (2 ^ n) L returns the halting state of every initial state, first reached before time 2 ^ n. No circuit recognizing halting states is needed.

theorem Cslib.Circuits.Boolean.Iteration.first_target_time {n : ℕ} (c : Circuit signature n n) (p : Circuit signature n 1) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n (1 + (n + 2))), (∀ (x : Fin n → Bool), out.eval interpretation x 0 = true ↔ ∃ (t : ℕ), p.eval interpretation ((c.eval interpretation)^[t] x) 0 = true) ∧ (∀ (x : Fin n → Bool), out.eval interpretation x 0 = true → have t := (word fun (i : Fin (n + 2)) => out.eval interpretation x (Fin.natAdd 1 i)).toNat; p.eval interpretation ((c.eval interpretation)^[t] x) 0 = true ∧ (∀ j < t, p.eval interpretation ((c.eval interpretation)^[j] x) 0 ≠ true) ∧ t < 2 ^ n) ∧ out.size ≤ 90000 * powerBudget n (c.size + p.size + 4 * n) (2 ^ n) L + p.size

First target times. For every 0 < L ≤ 2 ^ n, some circuit of size at most 90000 * powerBudget n (c.size + p.size + 4 * n) (2 ^ n) L + p.size returns a flag, set exactly when the orbit of its input reaches a state accepted by p, followed by n + 2 bits. When the flag is set they are the first time a target is visited, which is below 2 ^ n; otherwise nothing is claimed about them.

theorem Cslib.Circuits.Boolean.Iteration.first_target_time_optimized {n : ℕ} (c : Circuit signature n n) (p : Circuit signature n 1) : ∃ (out : Circuit signature n (1 + (n + 2))), (∀ (x : Fin n → Bool), out.eval interpretation x 0 = true ↔ ∃ (t : ℕ), p.eval interpretation ((c.eval interpretation)^[t] x) 0 = true) ∧ (∀ (x : Fin n → Bool), out.eval interpretation x 0 = true → have t := (word fun (i : Fin (n + 2)) => out.eval interpretation x (Fin.natAdd 1 i)).toNat; p.eval interpretation ((c.eval interpretation)^[t] x) 0 = true ∧ (∀ j < t, p.eval interpretation ((c.eval interpretation)^[j] x) 0 ≠ true) ∧ t < 2 ^ n) ∧ ↑out.size ≤ 270000 * optimizedBudget n (c.size + p.size + 4 * n) (2 ^ n) + ↑p.size

Square-root first target times. Some circuit of size at most 270000 * optimizedBudget n (c.size + p.size + 4 * n) (2 ^ n) + p.size returns the reachability flag and, when it is set, the first target time, as in first_target_time.

theorem Cslib.Circuits.Boolean.Iteration.halting_time {n : ℕ} (c : Circuit signature n n) (H : BitString n → Prop) (initial : Set (BitString n)) (hstop : ∀ (x : BitString n), H x → c.eval interpretation x = x) (hhalt : ∀ x ∈ initial, ∃ (t : ℕ), H ((c.eval interpretation)^[t] x)) : ∃ (out : Circuit signature n (n + 2)), (∀ x ∈ initial, have t := (word (out.eval interpretation x)).toNat; H ((c.eval interpretation)^[t] x) ∧ (∀ j < t, ¬H ((c.eval interpretation)^[j] x)) ∧ t < 2 ^ n) ∧ ↑out.size ≤ 150000 * optimizedBudget n c.size (2 ^ n)

Halting times. If c fixes every halting state and the orbit of every initial state halts, some circuit of size at most 150000 * optimizedBudget n c.size (2 ^ n) returns, in n + 2 bits, the first halting time of every initial state, which is below 2 ^ n. No circuit recognizing halting states is needed.