From 9d5caea2ba3a41e7ecaff51089d4031066cb3206 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 17:56:13 +0000 Subject: [PATCH] feat(descriptive): prove the Immerman-Vardi characterization --- Complexity.lean | 8 + .../Complexity/ImmermanVardi.lean | 148 +++++++++++ .../Complexity/ImmermanVardi/Input.lean | 113 ++++++++ .../ImmermanVardi/Tableau/Acceptance.lean | 110 ++++++++ .../ImmermanVardi/Tableau/Correct.lean | 219 ++++++++++++++++ .../ImmermanVardi/Tableau/Definability.lean | 247 ++++++++++++++++++ .../ImmermanVardi/Tableau/FixedPoint.lean | 192 ++++++++++++++ .../ImmermanVardi/Tableau/Step.lean | 209 +++++++++++++++ .../Operator/Definability/Finite.lean | 77 ++++++ .../FirstOrder/Operator/LeastFixedPoint.lean | 5 +- ComplexityTests/ImmermanVardi.lean | 88 +++++++ ComplexityTests/ImmermanVardiTableau.lean | 73 ++++++ README.md | 1 + ROADMAP.md | 9 +- .../ComplexityGuide/FirstOrderOperators.lean | 63 ++++- 15 files changed, 1548 insertions(+), 14 deletions(-) create mode 100644 Complexity/Computability/Complexity/ImmermanVardi.lean create mode 100644 Complexity/Computability/Complexity/ImmermanVardi/Input.lean create mode 100644 Complexity/Computability/Complexity/ImmermanVardi/Tableau/Acceptance.lean create mode 100644 Complexity/Computability/Complexity/ImmermanVardi/Tableau/Correct.lean create mode 100644 Complexity/Computability/Complexity/ImmermanVardi/Tableau/Definability.lean create mode 100644 Complexity/Computability/Complexity/ImmermanVardi/Tableau/FixedPoint.lean create mode 100644 Complexity/Computability/Complexity/ImmermanVardi/Tableau/Step.lean create mode 100644 Complexity/Logics/FirstOrder/Operator/Definability/Finite.lean create mode 100644 ComplexityTests/ImmermanVardi.lean create mode 100644 ComplexityTests/ImmermanVardiTableau.lean diff --git a/Complexity.lean b/Complexity.lean index 8c090fd2d..ca13d5ab9 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1259,6 +1259,13 @@ public import Complexity.Computability.Complexity.FineGrained.Sparsification public import Complexity.Computability.Complexity.FineGrained.ThreeOccurrenceReduction public import Complexity.Computability.Complexity.HardnessEncoding.PolyTime public import Complexity.Computability.Complexity.HardnessEncoding.Program +public import Complexity.Computability.Complexity.ImmermanVardi +public import Complexity.Computability.Complexity.ImmermanVardi.Input +public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.Acceptance +public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.Correct +public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.Definability +public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.FixedPoint +public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.Step public import Complexity.Computability.Complexity.Parameterized public import Complexity.Computability.Complexity.Parameterized.Kernelization public import Complexity.Computability.Complexity.Parameterized.VertexCover @@ -2803,6 +2810,7 @@ public import Complexity.Logics.FirstOrder.Interpretation.Tuple public import Complexity.Logics.FirstOrder.Interpretation.Unit public import Complexity.Logics.FirstOrder.Operator.Basic public import Complexity.Logics.FirstOrder.Operator.Definability +public import Complexity.Logics.FirstOrder.Operator.Definability.Finite public import Complexity.Logics.FirstOrder.Operator.Definability.Polarity public import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint public import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint.Definability diff --git a/Complexity/Computability/Complexity/ImmermanVardi.lean b/Complexity/Computability/Complexity/ImmermanVardi.lean new file mode 100644 index 000000000..48cb6d041 --- /dev/null +++ b/Complexity/Computability/Complexity/ImmermanVardi.lean @@ -0,0 +1,148 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.P.FirstOrder +public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.Acceptance +public import Complexity.Computability.Complexity.ImmermanVardi.Input +public import Complexity.Logics.FirstOrder.Ordered.FullTuple.LeastFixedPoint +public import Complexity.Logics.FirstOrder.Ordered.FullTuple.Power +import Complexity.Computability.Complexity.Fagin.Converse + +/-! +# The Immerman–Vardi characterization of polynomial time + +On the library's canonically ordered finite structures, a query is definable by one checked +FO(LFP) sentence exactly when its source-only encoded language belongs to native `P`. +The vocabulary is finite and relational; its fixed enumeration determines truth-table order. +Universes are `Fin n` with `n ≥ 2`. Order, BIT, zero, one, and maximum are canonical numeric +symbols, computed from the universe size rather than supplied as input tables. + +The forward direction compiles a fixed formula to a native polynomial-time model checker. +For the converse, a native deterministic machine has a positive local tableau. Its input +symbols are defined directly from the actual binary encoding. A fixed tuple width bounds the +machine's time, input length, and finite feature tags for all input sizes. Pullback along the +canonical full-tuple interpretation gives one sentence over the original input universe. + +## Main results + +* `FO.Ordered.LFPDefinable.of_encodedLanguage_mem_P`: every native polynomial-time ordered + query has a uniform checked FO(LFP) sentence. +* `FO.Ordered.lfpDefinable_iff_encodedLanguage_mem_P`: FO(LFP) captures native polynomial time. + +## References + +* [N. Immerman, *Relational Queries Computable in Polynomial Time*][Immerman1986], Theorem 1 + and Section 3. The theorem is instantiated here at the existing canonical ordered vocabulary + and unary-cardinality/full-truth-table encoding. Malformed table shapes and universes below + two are rejected. +-/ + +public section + +open FirstOrder Language Turing Turing.MultiTapeTM + +namespace Cslib.Logic + +namespace Vocabulary + +variable {L : Language} (v : Vocabulary L) + +/-- A single tuple dimension contains the input, runtime, and fixed finite feature tags of a +polynomial-time native machine, uniformly over well-formed ordered structures. -/ +theorem exists_lfp_power_bound (t : ℕ → ℕ) (ht : Cslib.PolynomiallyBounded t) (tags : ℕ) : + ∃ k : ℕ, 1 ≤ k ∧ (∀ i : Fin v.count, v.arity i ≤ k) ∧ + ∀ a : EncodedStructure, v.WellFormed a → 2 ≤ a.1 → + (encStructure a).length + 1 < a.1 ^ k ∧ + t (encStructure a).length < a.1 ^ k ∧ tags ≤ a.1 ^ k := by + obtain ⟨c, d, htime⟩ := Cslib.polynomiallyBounded_iff_le.mp ht + obtain ⟨k, hk, har, hpow⟩ := v.exists_pow_bound 0 (c + tags) d + refine ⟨k, hk, har, fun a ha hn => ?_⟩ + obtain ⟨hinput, hclock⟩ := hpow a ha hn + simp only [Polynomial.eval_zero, Nat.add_zero] at hinput hclock + have hlen : (encStructure a).length + 1 ≤ (frame (encStructure a)).length + 1 := by + rw [length_frame] + omega + have ht' : t (encStructure a).length ≤ + (c + tags) * ((frame (encStructure a)).length + 1) ^ d := + (htime _).trans (Nat.mul_le_mul (Nat.le_add_right c tags) + (Nat.pow_le_pow_left hlen d)) + have hp : 1 ≤ ((frame (encStructure a)).length + 1) ^ d := + Nat.one_le_pow _ _ (by omega) + have htags : tags ≤ (c + tags) * ((frame (encStructure a)).length + 1) ^ d := + calc tags ≤ c + tags := Nat.le_add_left _ _ + _ = (c + tags) * 1 := (Nat.mul_one _).symm + _ ≤ _ := Nat.mul_le_mul_left _ hp + exact ⟨by omega, by omega, by omega⟩ + +end Vocabulary + +namespace FO.Ordered + +open Cslib.Complexity + +/-- Every ordered query decided by an actual native polynomial-time machine is defined by one +checked FO(LFP) sentence over the original ordered input structures. -/ +theorem LFPDefinable.of_encodedLanguage_mem_P {L : Language} [L.IsRelational] + (v : Vocabulary L) {K : Query L} (hK : K.encodedLanguage v ∈ P encStructure) : + LFPDefinable K := by + classical + obtain ⟨f, ⟨t, _, ht, _, m, State, hfinite, tm, htm⟩, hdec⟩ := hK + let _ := hfinite + let _ := Fintype.ofFinite State + obtain ⟨k, hk, har, hpow⟩ := + v.exists_lfp_power_bound t ht (Fintype.card (ImmermanVardi.Tableau.Tag m State)) + let A := {a : EncodedStructure // v.WellFormed a ∧ 2 ≤ a.1} + let size (a : A) := a.val.1 ^ k + let input (a : A) := encStructure a.val + let inst (a : A) : v.powerLanguage.Structure (Fin (size a)) := + v.powerStructure a.val (size a) + let instSize (a : A) : Fact (2 ≤ size a) := by + let _ : Fact (2 ≤ a.val.1) := ⟨a.property.2⟩ + exact ⟨FullTupleInterpretation.two_le_pow (n := a.val.1) hk⟩ + have hb (a : A) : + (input a).length + 1 < size a ∧ t (input a).length < size a ∧ + Fintype.card (ImmermanVardi.Tableau.Tag m State) ≤ size a := + hpow a.val a.property.1 a.property.2 + obtain ⟨ψ, hψ⟩ := ImmermanVardi.Tableau.exists_acceptance_sentence + (L := v.powerLanguage) (size := size) tm input v.inputSymbol + (fun a s p => v.realize_inputSymbol a.property.1 + ((Nat.lt_succ_self _).trans (hb a).1) s p) + (fun a => (hb a).1) (fun a => (hb a).2.2) + let I := v.orderedPowerInterpretation k har + refine ⟨I.onLFPSentence ψ, fun M => ?_⟩ + let a : A := ⟨encode v M, v.wellFormed_encode M (Equiv.refl M), M.size_ge_two⟩ + have hm := (htm (encode v M)).runFrom_of_le + (show t (input a).length ≤ size a - 1 by have := (hb a).2.1; omega) + have haccept : ψ.Realize (M := Fin (size a)) Operator.RelEnv.empty Empty.elim ↔ + f (encode v M) = true := by + have hψ' := hψ a + have hv (v : Empty → Fin (size a)) : v = Empty.elim := Subsingleton.elim _ _ + simp only [hv] at hψ' + rw [hψ'] + change ((tm.runFrom (tm.initCfg (encStructure (encode v M))) (size a - 1)).Halted ∧ + (tm.runFrom (tm.initCfg (encStructure (encode v M))) (size a - 1)).output = [true]) ↔ _ + simp only [hm.2, encBool_apply, List.singleton_inj] + exact ⟨And.right, fun h => ⟨hm.1, h⟩⟩ + have hquery : M ∈ K ↔ f (encode v M) = true := + (mem_encodedLanguage_encode v K M).symm.trans (hdec (encode v M)) + rw [I.realize_onLFPSentence hk ψ] + have he := v.inputStructure_orderedPowerInterpretation k har hk M + change I.inputStructure (n := M.size) = inst a at he + rw [he] + exact hquery.trans haccept.symm + +/-- **Immerman–Vardi:** a single checked FO(LFP) sentence defines an ordered query exactly +when its source-only language is decidable in native polynomial time. -/ +theorem lfpDefinable_iff_encodedLanguage_mem_P {L : Language} [L.IsRelational] + (v : Vocabulary L) (K : Query L) : + LFPDefinable K ↔ K.encodedLanguage v ∈ P encStructure := + ⟨fun h => h.encodedLanguage_mem_P v, LFPDefinable.of_encodedLanguage_mem_P v⟩ + +end FO.Ordered +end Cslib.Logic diff --git a/Complexity/Computability/Complexity/ImmermanVardi/Input.lean b/Complexity/Computability/Complexity/ImmermanVardi/Input.lean new file mode 100644 index 000000000..246a6efa5 --- /dev/null +++ b/Complexity/Computability/Complexity/ImmermanVardi/Input.lean @@ -0,0 +1,113 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Logics.FirstOrder.Ordered.Encoding +public import Complexity.Computability.Machines.Turing.MultiTape.Run + +/-! +# First-order input symbols for native deterministic machines + +The direct length and bit formulas for `encStructure` yield formulas for all three native +input-tape symbols. Position zero is the left endmarker; the first data bit is at position one. +The formulas include the right endmarker and padding, and use no guessed relations. +-/ + +public section + +open FirstOrder Language Turing Turing.MultiTapeTM + +namespace Cslib.Logic.Vocabulary + +open FO.Ordered + +variable {L : Language} (v : Vocabulary L) + +/-- The native input-tape symbol, including both endmarkers, defined from the encoded input. -/ +noncomputable def inputSymbol : Option Bool → (language v.powerLanguage).Formula (Fin 1) + | none => natEq v.powerLanguage 0 (.var 0) ⊔ Formula.iExs (Fin 1) + (v.inputLength.relabel (fun _ => .inr 0) ⊓ + ∼(le v.powerLanguage (.var (.inl 0)) (.var (.inr 0)))) + | some b => Formula.iExs (Fin 2) + (v.inputLength.relabel (fun _ => .inr 1) ⊓ + ∼(le v.powerLanguage (.var (.inr 1)) (.var (.inr 0))) ⊓ + addEq v.powerLanguage (.var (.inr 0)) (one v.powerLanguage) (.var (.inl 0)) ⊓ + (if b then v.inputBit.relabel (fun _ => .inr 0) + else ∼(v.inputBit.relabel (fun _ => .inr 0)))) + +/-- The first-order input-symbol formula agrees exactly with the native machine input lookup. -/ +theorem realize_inputSymbol {a : EncodedStructure} (ha : v.WellFormed a) + {B : ℕ} [Fact (2 ≤ B)] (hB : (encStructure a).length < B) + (s : Option Bool) (p : Fin B) : + letI := v.powerStructure a B + (v.inputSymbol s).Realize ![p] ↔ inputAt (encStructure a) p.val = s := by + let _ := v.powerStructure a B + have hlen (x : Fin B) := v.realize_inputLength ha hB x + have hbit (x : Fin B) := v.realize_inputBit ha hB x + rcases s with _ | b + · simp only [inputSymbol, Formula.realize_sup, realize_natEq, Term.realize_var, + Matrix.cons_val_zero, Formula.realize_iExs, Formula.realize_inf, + Formula.realize_relabel, Formula.realize_not, realize_le, Function.comp_def, + Sum.elim_inl, Sum.elim_inr, not_le] + constructor + · rintro (hz | ⟨xs, hx, hp⟩) + · simp [inputAt, hz] + · have hx' : (encStructure a).length = (xs 0).val := by + apply (hlen (xs 0)).mp + simpa only [Matrix.cons_fin_one] using hx + have hn : p.val ≠ 0 := by change (xs 0).val < p.val at hp; omega + simp only [inputAt, hn, ite_false, List.getElem?_eq_none_iff] + change (xs 0).val < p.val at hp + omega + · intro h + by_cases hp : p.val = 0 + · exact Or.inl hp + · right + simp only [inputAt, hp, ite_false, List.getElem?_eq_none_iff] at h + let l : Fin B := ⟨(encStructure a).length, hB⟩ + refine ⟨![l], ?_, ?_⟩ + · simpa only [Matrix.cons_fin_one] using (hlen l).mpr rfl + · change (encStructure a).length < p.val + omega + · have hdata (q : Fin B) (hq : q.val < (encStructure a).length) : + (if b then v.inputBit.Realize ![q] else ¬v.inputBit.Realize ![q]) ↔ + (encStructure a)[q.val]? = some b := by + rw [hbit q, List.getElem?_eq_getElem hq] + cases b <;> cases (encStructure a)[q.val] <;> simp + have hform : (v.inputSymbol (some b)).Realize ![p] ↔ + ∃ xs : Fin 2 → Fin B, + (encStructure a).length = (xs 1).val ∧ + (xs 0).val < (xs 1).val ∧ (xs 0).val + 1 = p.val ∧ + (if b then v.inputBit.Realize ![xs 0] else ¬v.inputBit.Realize ![xs 0]) := by + simp only [inputSymbol, Formula.realize_iExs, Formula.realize_inf] + apply exists_congr + intro xs + have hl : v.inputLength.Realize (fun _ : Fin 1 => xs 1) ↔ + (encStructure a).length = (xs 1).val := by + simpa only [Matrix.cons_fin_one] using hlen (xs 1) + cases b <;> simp only [Bool.false_eq_true, ↓reduceIte, Formula.realize_relabel, + Formula.realize_not, realize_le, realize_addEq, realize_one_val, + Term.realize_var, Function.comp_def, Sum.elim_inl, Sum.elim_inr, + hl, not_le, Fin.lt_def, Matrix.cons_fin_one, and_assoc] + rw [hform] + constructor + · rintro ⟨xs, hlen, hlt, hs, hb⟩ + have hq : (xs 0).val < (encStructure a).length := by omega + have hp : p.val ≠ 0 := by omega + have he : p.val - 1 = (xs 0).val := by omega + simpa only [inputAt, hp, ite_false, he] using (hdata (xs 0) hq).mp hb + · intro h + have hp : p.val ≠ 0 := by intro hp; simp [inputAt, hp] at h + simp only [inputAt, hp, ite_false] at h + have hq : p.val - 1 < (encStructure a).length := + (List.getElem?_eq_some_iff.mp h).choose + let q : Fin B := ⟨p.val - 1, by omega⟩ + let l : Fin B := ⟨(encStructure a).length, hB⟩ + exact ⟨![q, l], rfl, hq, by dsimp [q]; omega, (hdata q hq).mpr h⟩ + +end Cslib.Logic.Vocabulary diff --git a/Complexity/Computability/Complexity/ImmermanVardi/Tableau/Acceptance.lean b/Complexity/Computability/Complexity/ImmermanVardi/Tableau/Acceptance.lean new file mode 100644 index 000000000..8e7cc938e --- /dev/null +++ b/Complexity/Computability/Complexity/ImmermanVardi/Tableau/Acceptance.lean @@ -0,0 +1,110 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.Definability +import Mathlib.Tactic.FinCases + +/-! +# FO(LFP) sentences for native machine acceptance + +One sentence expresses that a given deterministic native machine has halted with output +`[true]` by the maximum time in a finite ordered domain. The sentence is uniform in the +input structure and the domain size. Its input-symbol formulas are ordinary first-order +formulas, so no computational predicate is hidden in an added relation. + +## Main results + +* `exists_acceptance_sentence`: native bounded machine acceptance has a single checked + FO(LFP) sentence, given the first-order interpretation of its input tape. +-/ + +public section + +namespace Cslib.Complexity.ImmermanVardi.Tableau + +open Turing Turing.MultiTapeTM +open FirstOrder Language +open Cslib.Logic.FO +open Cslib.Logic.FO.Operator + +variable {L : Language} {ι : Type} {size : ι → ℕ} + [∀ i, L.Structure (Fin (size i))] [∀ i, Fact (2 ≤ size i)] + {m : ℕ} {State : Type} [Fintype State] + +private def maximum (i : ι) : Fin (size i) := + ⟨size i - 1, Nat.sub_lt (by have := (Fact.out : 2 ≤ size i); omega) (by omega)⟩ + +private theorem trace_lfp_definable_terms (tm : MultiTapeTM m Bool State) + (input : ι → List Bool) + (inputFormula : Option Bool → (Ordered.language L).Formula (Fin 1)) + (hinput : ∀ i s (a : Fin (size i)), + (inputFormula s).Realize ![a] ↔ inputAt (input i) a.val = s) + {α : Type} (args : Fin 3 → (Ordered.language L).Term α) : + Operator.Definable (L := Ordered.language L) LFP.policy + (fun i => Fin (size i)) (fun _ => LFP.interpretation) (fun _ => RelEnv.empty) + (fun i v => (fun j => (args j).realize v) ∈ (traceStep tm (input i)).lfp) := by + apply LFP.definable_lfp (fun i _ => traceStep tm (input i)) args + exact traceStep_polarityDefinable tm input inputFormula hinput Sum.inr + +private theorem row_at_maximum_definable (tm : MultiTapeTM m Bool State) + (input : ι → List Bool) + (inputFormula : Option Bool → (Ordered.language L).Formula (Fin 1)) + (hinput : ∀ i s (a : Fin (size i)), + (inputFormula s).Realize ![a] ↔ inputAt (input i) a.val = s) + (hn : ∀ i, (input i).length + 1 < size i) + (hB : ∀ i, Fintype.card (Tag m State) ≤ size i) (q : Tag m State) : + Operator.Definable (L := Ordered.language L) LFP.policy + (fun i => Fin (size i)) (fun _ => LFP.interpretation) (fun _ => RelEnv.empty) + (fun i (_ : Empty → Fin (size i)) => + row (tm.runFrom (tm.initCfg (input i)) (size i - 1)) q (maximum (size := size) i)) := by + have hf : Operator.Definable (L := Ordered.language L) LFP.policy + (fun i => Fin (size i)) (fun _ => LFP.interpretation) (fun _ => RelEnv.empty) + (fun i (_ : Empty → Fin (size i)) => + traceRow (traceStep tm (input i)).lfp (maximum (size := size) i) q + (maximum (size := size) i)) := by + apply Definable.ex + apply Definable.conj + · exact (Definable.ofFO (Ordered.natEq L (tagIndex q) (.var none))).congr + fun _ _ => Ordered.realize_natEq _ _ _ + · apply (trace_lfp_definable_terms tm input inputFormula hinput + ![.var none, Ordered.max L, Ordered.max L]).congr + intro i v + have hm : (Ordered.max L).realize v = maximum (size := size) i := + Fin.ext (Ordered.realize_max_val _) + have htuple : + (fun j => ((![.var none, Ordered.max L, Ordered.max L] : + Fin 3 → (Ordered.language L).Term (Option Empty)) j).realize v) = + ![v none, maximum (size := size) i, maximum (size := size) i] := by + ext j + fin_cases j <;> simp [hm] + rw [htuple] + exact hf.congr fun i _ => traceRow_lfp tm (input i) (hn i) (hB i) + (maximum (size := size) i) q (maximum (size := size) i) + +/-- A native deterministic machine's acceptance by the domain's final time is described by one +checked FO(LFP) sentence. All input symbols are interpreted by ordinary first-order formulas. -/ +theorem exists_acceptance_sentence (tm : MultiTapeTM m Bool State) + (input : ι → List Bool) + (inputFormula : Option Bool → (Ordered.language L).Formula (Fin 1)) + (hinput : ∀ i s (a : Fin (size i)), + (inputFormula s).Realize ![a] ↔ inputAt (input i) a.val = s) + (hn : ∀ i, (input i).length + 1 < size i) + (hB : ∀ i, Fintype.card (Tag m State) ≤ size i) : + ∃ φ : LFP.Formula (Ordered.language L) [] Empty, ∀ i, + φ.Realize (M := Fin (size i)) RelEnv.empty (fun e => nomatch e) ↔ + (tm.runFrom (tm.initCfg (input i)) (size i - 1)).Halted ∧ + (tm.runFrom (tm.initCfg (input i)) (size i - 1)).output = [true] := by + have hs := row_at_maximum_definable tm input inputFormula hinput hn hB (.state none) + have ho := row_at_maximum_definable tm input inputFormula hinput hn hB (.out (.one true)) + obtain ⟨φ, hwf, hφ⟩ := hs.conj ho + refine ⟨⟨φ, hwf⟩, fun i => ?_⟩ + exact (hφ i (fun e => nomatch e)).trans (by + simp only [row, Tag.feature, Feature.Holds, OutView.ofList_eq_one_iff, Cfg.Halted]) + +end Cslib.Complexity.ImmermanVardi.Tableau diff --git a/Complexity/Computability/Complexity/ImmermanVardi/Tableau/Correct.lean b/Complexity/Computability/Complexity/ImmermanVardi/Tableau/Correct.lean new file mode 100644 index 000000000..5032517ec --- /dev/null +++ b/Complexity/Computability/Complexity/ImmermanVardi/Tableau/Correct.lean @@ -0,0 +1,219 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.Step + +/-! +# Correctness of the positive native tableau rules + +The positive local rules compute the next native configuration exactly. The finite domain +must contain both input endmarkers and the next work-head position. No property of an +arbitrary recursive approximation is assumed: the monotonicity theorem applies to every row, +and correctness is proved separately on the rows of actual native configurations. + +## Main results + +* `read_row`, `situation_row`: positive read and situation predicates have native semantics. +* `elsewhere_row`: the positive replacement for head negation is exact on native rows. +* `rowStep_row`: the positive rules compute exactly the next native configuration. +-/ + +public section + +namespace Cslib.Complexity.ImmermanVardi.Tableau + +open Turing Turing.MultiTapeTM Turing.MultiTapeTM.Feature + +variable {m B : ℕ} {State : Type} {input : List Bool} {cfg : Cfg m Bool State input} + +/-- The positive read rule recovers the symbol under a head inside the finite domain. -/ +theorem read_row (hb : ∀ i, |cfg.workTapePos i| < B) (i : Fin m) (s : Option Bool) : + read (row (B := B) cfg) i s ↔ (Feature.read i s).Holds cfg := by + simp only [read, row, Tag.feature, Feature.Holds, offset, ↓reduceIte, + Bool.false_eq_true, Cfg.workTapeSymbols] + constructor + · rintro ⟨a, ⟨hh, hc⟩ | ⟨hh, hc⟩⟩ <;> rwa [hh] + · intro hs + have hbi := hb i + rw [abs_lt] at hbi + by_cases hp : 0 ≤ cfg.workTapePos i + · let a : Fin B := ⟨(cfg.workTapePos i).toNat, by omega⟩ + refine ⟨a, Or.inl ⟨by dsimp [a]; omega, ?_⟩⟩ + have he : (a.val : ℤ) = cfg.workTapePos i := by dsimp [a]; omega + rwa [he] + · let a : Fin B := ⟨(-cfg.workTapePos i).toNat, by omega⟩ + refine ⟨a, Or.inr ⟨by dsimp [a]; omega, ?_⟩⟩ + have he : -(a.val : ℤ) = cfg.workTapePos i := by dsimp [a]; omega + rwa [he] + +/-- Positive situation predicates agree with the native situation. -/ +theorem situation_row (hn : input.length + 1 < B) (hb : ∀ i, |cfg.workTapePos i| < B) + (y : Situation m State) (a : Fin B) : + situation input (row cfg) y a ↔ (Feature.sit y).Holds cfg := by + rw [situation, holds_sit_iff] + simp only [row, Tag.feature] + refine and_congr Iff.rfl (and_congr ?_ (forall_congr' fun i => read_row hb i _)) + simp only [holds_inPos, holds_inRead, Cfg.inputSymbol_eq_inputAt] + constructor + · rintro ⟨j, hj, hs⟩ + rwa [hj] + · intro hs + exact ⟨⟨cfg.inputPos.val, lt_of_lt_of_le cfg.inputPos.isLt hn⟩, rfl, hs⟩ + +/-- A positively witnessed other head position is equivalent to head inequality. -/ +theorem elsewhere_row (hb : ∀ i, |cfg.workTapePos i| < B) + (i : Fin m) (sign : Bool) (a : Fin B) : + elsewhere (row cfg) i sign a ↔ ¬(Feature.head i (offset sign a)).Holds cfg := by + have hbi := hb i + rw [abs_lt] at hbi + simp only [elsewhere, row, Tag.feature, Feature.Holds] + constructor + · rintro ⟨b, ⟨hb', hba⟩ | ⟨hb', hba⟩⟩ hpos + · apply hba + apply Fin.ext + cases sign <;> simp only [offset, Bool.false_eq_true, ↓reduceIte] at * <;> + omega + · apply hba + cases sign <;> simp only [offset, Bool.false_eq_true, Bool.not_true, + Bool.not_false, ↓reduceIte] at * <;> omega + · intro hne + by_cases hp : 0 ≤ cfg.workTapePos i + · let b : Fin B := ⟨(cfg.workTapePos i).toNat, by omega⟩ + have hb' : (b.val : ℤ) = cfg.workTapePos i := by dsimp [b]; omega + refine ⟨b, ?_⟩ + cases sign + · right + simp only [offset, Bool.not_false, Bool.false_eq_true, ↓reduceIte] at * + exact ⟨hb'.symm, by omega⟩ + · left + simp only [offset, ↓reduceIte] at * + exact ⟨hb'.symm, fun h => hne (by simpa [h] using hb'.symm)⟩ + · let b : Fin B := ⟨(-cfg.workTapePos i).toNat, by omega⟩ + have hb' : -(b.val : ℤ) = cfg.workTapePos i := by dsimp [b]; omega + refine ⟨b, ?_⟩ + cases sign + · left + simp only [offset, Bool.false_eq_true, ↓reduceIte] at * + exact ⟨hb'.symm, fun h => hne (by simpa [h] using hb'.symm)⟩ + · right + simp only [offset, Bool.not_true, Bool.false_eq_true, ↓reduceIte] at * + exact ⟨hb'.symm, by omega⟩ + +private theorem inputAt_eq_none_iff (j : ℕ) : + inputAt input j = none ↔ j = 0 ∨ input.length < j := by + by_cases hj : j = 0 + · simp [inputAt, hj] + · simp only [inputAt, hj, ↓reduceIte, List.getElem?_eq_none_iff, false_or] + omega + +/-- The positive input-head predecessor rule describes the native clamped move. -/ +theorem inputPrev_row (hn : input.length + 1 < B) (d : SignType) (a : Fin B) : + inputPrev input (row cfg) d a ↔ + moveInputPosNat input.length cfg.inputPos.val d = a.val := by + have hp := cfg.inputPos.isLt + cases d <;> simp only [inputPrev, row, Tag.feature, Feature.Holds, + moveInputPosNat, SignType.zero_eq_zero, SignType.neg_eq_neg_one, SignType.pos_eq_one, + SignType.coe_zero, SignType.coe_neg_one, SignType.coe_one] + · omega + · constructor + · rintro (⟨ha, hh⟩ | ⟨b, hb, hh⟩) <;> omega + · intro hmove + by_cases hz : cfg.inputPos.val = 0 + · exact Or.inl ⟨by omega, by omega⟩ + · exact Or.inr ⟨⟨cfg.inputPos.val, by omega⟩, by dsimp; omega, rfl⟩ + · simp only [ne_eq, inputAt_eq_none_iff, not_or] + constructor + · rintro (⟨ha, hh, hp'⟩ | ⟨b, hb, hp', hx⟩) + · omega + · omega + · intro hmove + by_cases he : cfg.inputPos.val = input.length + 1 + · left + exact ⟨by omega, Or.inr (by omega), by omega⟩ + · right + refine ⟨⟨cfg.inputPos.val, by omega⟩, by dsimp; omega, rfl, ?_⟩ + dsimp + omega + +/-- The positive work-head predecessor rule describes the native signed move. -/ +theorem headPrev_row (hb : ∀ i, |cfg.workTapePos i| + 1 < B) + (i : Fin m) (sign : Bool) (d : SignType) (a : Fin B) : + headPrev (row cfg) i sign d a ↔ + cfg.workTapePos i + (d : ℤ) = offset sign a := by + have hbi := hb i + have hbi' : |cfg.workTapePos i| < (B : ℤ) - 1 := by omega + rw [abs_lt] at hbi' + cases sign <;> cases d <;> + simp only [headPrev, row, Tag.feature, Feature.Holds, offset, Bool.false_eq_true, + Bool.not_false, Bool.not_true, ↓reduceIte, + SignType.zero_eq_zero, SignType.neg_eq_neg_one, SignType.pos_eq_one, + SignType.coe_zero, SignType.coe_neg_one, SignType.coe_one, neg_zero, neg_neg, + add_zero] + · constructor + · rintro (⟨ha, b, hb', hp⟩ | ⟨b, hb', hp⟩) <;> omega + · intro hmove + by_cases ha : a.val = 0 + · exact Or.inl ⟨ha, ⟨1, by omega⟩, rfl, by dsimp; omega⟩ + · exact Or.inr ⟨⟨a.val - 1, by omega⟩, by dsimp; omega, by dsimp; omega⟩ + · constructor + · rintro ⟨b, hb', hp⟩ + omega + · intro hmove + exact ⟨⟨a.val + 1, by omega⟩, rfl, by dsimp; omega⟩ + · constructor + · rintro ⟨b, hb', hp⟩ + omega + · intro hmove + exact ⟨⟨a.val + 1, by omega⟩, rfl, by dsimp; omega⟩ + · constructor + · rintro (⟨ha, b, hb', hp⟩ | ⟨b, hb', hp⟩) <;> omega + · intro hmove + by_cases ha : a.val = 0 + · exact Or.inl ⟨ha, ⟨1, by omega⟩, rfl, by dsimp; omega⟩ + · exact Or.inr ⟨⟨a.val - 1, by omega⟩, by dsimp; omega, by dsimp; omega⟩ + +variable [Finite State] (tm : MultiTapeTM m Bool State) + +/-- The positive rules produce exactly the row of the next native configuration. -/ +theorem rowStep_row (hn : input.length + 1 < B) + (hb : ∀ i, |cfg.workTapePos i| + 1 < B) (q : Tag m State) (a : Fin B) : + rowStep tm input (row cfg) q a ↔ row (tm.step cfg) q a := by + classical + let _ := Fintype.ofFinite State + have hb' : ∀ i, |cfg.workTapePos i| < B := fun i => by have := hb i; omega + cases q with + | state q => + simp only [rowStep, situation_row hn hb', row, Tag.feature, + holds_step_state_iff, Finset.mem_filter, Finset.mem_univ, true_and] + | out o => + simp only [rowStep, situation_row hn hb', row, Tag.feature, holds_step_out_iff, + Finset.mem_filter, Finset.mem_product, Finset.mem_univ, true_and, + Prod.exists] + | inPos => + simp only [rowStep, situation_row hn hb', inputPrev_row hn, + row, Tag.feature, holds_inPos] + cases hq : cfg.state with + | none => simp [hq, not_holds_sit hq] + | some q => + simp [holds_state, hq, holds_sit_iff_eq hq, step_eq_apply tm hq, + Action.apply_inputPos, val_moveInputPos_eq_moveInputPosNat] + | head i sign => + simp only [rowStep, situation_row hn hb', headPrev_row hb, + row, Tag.feature, holds_head] + cases hq : cfg.state with + | none => simp [hq, not_holds_sit hq] + | some q => + simp [holds_state, hq, holds_sit_iff_eq hq, step_eq_apply tm hq, + Action.apply_workTapePos] + | cell i sign s => + simp only [rowStep, situation_row hn hb', elsewhere_row hb', row, Tag.feature, + holds_step_cell_iff, Finset.mem_filter, Finset.mem_product, Finset.mem_univ, + true_and, Prod.exists] + +end Cslib.Complexity.ImmermanVardi.Tableau diff --git a/Complexity/Computability/Complexity/ImmermanVardi/Tableau/Definability.lean b/Complexity/Computability/Complexity/ImmermanVardi/Tableau/Definability.lean new file mode 100644 index 000000000..0a497ca05 --- /dev/null +++ b/Complexity/Computability/Complexity/ImmermanVardi/Tableau/Definability.lean @@ -0,0 +1,247 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.FixedPoint +public import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint.Definability +public import Complexity.Logics.FirstOrder.Operator.Definability.Finite +public import Complexity.Logics.FirstOrder.Ordered.BitArithmetic +import Complexity.Tactic.FOOperator +import Mathlib.Tactic.FinCases + +/-! +# Synthesizing a positive native computation tableau + +Fixed finite transition tables become fixed finite disjunctions. The three input-symbol +formulas are ordinary first-order formulas; every recursive relation occurrence is certified +positive by the shared synthesis calculus. A single resulting formula works for every input +structure and every finite domain size. + +## Main results + +* `traceStep_polarityDefinable`: syntactic positivity and uniform definability of the native + tableau transformer. +* `trace_lfp_definable`: a single FO(LFP) formula for the native tableau fixed point. +-/ + +public section + +namespace Cslib.Complexity.ImmermanVardi.Tableau + +open Turing Turing.MultiTapeTM +open FirstOrder Language +open Cslib.Logic.FO +open Cslib.Logic.FO.Operator + +variable {L : Language} {ι : Type} (size : ι → ℕ) + [∀ i, L.Structure (Fin (size i))] [∀ i, Fact (2 ≤ size i)] + +private abbrev Candidate := (i : ι) × Set (Fin 3 → Fin (size i)) + +private abbrev BodyDefinable {α : Type} (sign : Bool) + (P : ∀ j : Candidate size, (α → Fin (size j.1)) → Prop) : Prop := + PolarityDefinable (L := Ordered.language L) LFP.policy LFP.headMark sign + (fun j : Candidate size => Fin (size j.1)) (fun _ => LFP.interpretation) + (fun j => RelEnv.cons j.2 RelEnv.empty) P + +variable {size} + +private theorem numeral_definable {α : Type} (sign : Bool) (n : ℕ) (a : α) : + BodyDefinable (L := L) size sign (fun _ v => (v a).val = n) := + (PolarityDefinable.ofFO (Ordered.natEq L n (.var a))).congr + fun _ _ => Ordered.realize_natEq _ _ _ + +private theorem successor_definable {α : Type} (sign : Bool) (a b : α) : + BodyDefinable (L := L) size sign (fun _ v => (v a).val + 1 = (v b).val) := + (PolarityDefinable.ofFO (Ordered.addEq L (.var a) (Ordered.one L) (.var b))).congr + fun _ _ => by simp only [Ordered.realize_addEq, Term.realize_var, Ordered.realize_one_val] + +private theorem recursive_atom_definable {α : Type} (a b c : α) : + BodyDefinable (L := L) size true (fun j v => ![v a, v b, v c] ∈ j.2) := by + apply (PolarityDefinable.head_vars LFP.headMark + (fun j : Candidate size => j.2) ![a, b, c]).congr + intro j v + have hv : v ∘ ![a, b, c] = ![v a, v b, v c] := by + ext k + fin_cases k <;> rfl + rw [hv] + +private theorem input_definable (input : ι → List Bool) + (inputFormula : Option Bool → (Ordered.language L).Formula (Fin 1)) + (hinput : ∀ i s (a : Fin (size i)), + (inputFormula s).Realize ![a] ↔ inputAt (input i) a.val = s) + {α : Type} (sign : Bool) (s : Option Bool) (a : α) : + BodyDefinable (L := L) size sign + (fun j v => inputAt (input j.1) (v a).val = s) := by + apply (PolarityDefinable.ofFO ((inputFormula s).relabel (fun _ => a))).congr + intro j v + have hv : v ∘ (fun _ : Fin 1 => a) = ![v a] := by + funext k + fin_cases k + rfl + rw [Language.Formula.realize_relabel, hv] + exact hinput j.1 s (v a) + +variable {m : ℕ} {State : Type} [Fintype State] + +private theorem traceRow_definable {α : Type} (q : Tag m State) (t a : α) : + BodyDefinable (L := L) size true (fun j v => traceRow j.2 (v t) q (v a)) := by + apply PolarityDefinable.ex + exact (numeral_definable true (tagIndex q) none).conj + (recursive_atom_definable none (some t) (some a)) + +attribute [local aesop safe apply (rule_sets := [FODefinable])] + numeral_definable successor_definable recursive_atom_definable traceRow_definable + +private theorem read_definable {α : Type} (i : Fin m) (s : Option Bool) (t : α) : + BodyDefinable (L := L) size true + (fun j v => read (traceRow (State := State) j.2 (v t)) i s) := by + unfold read + fo_definable + +attribute [local aesop safe apply (rule_sets := [FODefinable])] read_definable + +private theorem situation_definable (input : ι → List Bool) + (inputFormula : Option Bool → (Ordered.language L).Formula (Fin 1)) + (hinput : ∀ i s (a : Fin (size i)), + (inputFormula s).Realize ![a] ↔ inputAt (input i) a.val = s) + {α : Type} (y : Situation m State) (t a : α) : + BodyDefinable (L := L) size true + (fun j v => situation (input j.1) (traceRow j.2 (v t)) y (v a)) := by + unfold situation + apply PolarityDefinable.conj (traceRow_definable _ _ _) + apply PolarityDefinable.conj + · apply PolarityDefinable.ex + exact (traceRow_definable .inPos (some t) none).conj + (input_definable input inputFormula hinput true y.2.1 none) + · exact PolarityDefinable.iAll fun i => read_definable i (y.2.2 i) t + +private theorem elsewhere_definable {α : Type} (i : Fin m) (sign : Bool) (t a : α) : + BodyDefinable (L := L) size true + (fun j v => elsewhere (traceRow (State := State) j.2 (v t)) i sign (v a)) := by + simp only [elsewhere, ne_eq] + fo_definable + +private theorem inputPrev_definable (input : ι → List Bool) + (inputFormula : Option Bool → (Ordered.language L).Formula (Fin 1)) + (hinput : ∀ i s (a : Fin (size i)), + (inputFormula s).Realize ![a] ↔ inputAt (input i) a.val = s) + {α : Type} (d : SignType) (t a : α) : + BodyDefinable (L := L) size true + (fun j v => inputPrev (m := m) (State := State) + (input j.1) (traceRow j.2 (v t)) d (v a)) := by + cases d with + | zero => exact traceRow_definable .inPos t a + | neg => + simp only [inputPrev] + fo_definable + | pos => + apply PolarityDefinable.disj + · exact (numeral_definable false 0 a).neg.conj + ((input_definable input inputFormula hinput true none a).conj + (traceRow_definable .inPos t a)) + · apply PolarityDefinable.ex + exact (successor_definable true none (some a)).conj + ((traceRow_definable .inPos (some t) none).conj + ((numeral_definable true 0 none).disj + (input_definable input inputFormula hinput false none none).neg)) + +private theorem headPrev_definable {α : Type} (i : Fin m) (sign : Bool) + (d : SignType) (t a : α) : + BodyDefinable (L := L) size true + (fun j v => headPrev (State := State) (traceRow j.2 (v t)) i sign d (v a)) := by + unfold headPrev + generalize (if sign then d else -d) = e + cases e <;> fo_definable + +omit [Fintype State] in +private theorem initial_definable (tm : MultiTapeTM m Bool State) {α : Type} + (q : Tag m State) (a : α) : + BodyDefinable (L := L) size true (fun _ v => initial tm q (v a)) := by + cases q <;> simp only [initial] <;> fo_definable + +private theorem rowStep_definable (tm : MultiTapeTM m Bool State) (input : ι → List Bool) + (inputFormula : Option Bool → (Ordered.language L).Formula (Fin 1)) + (hinput : ∀ i s (a : Fin (size i)), + (inputFormula s).Realize ![a] ↔ inputAt (input i) a.val = s) + {α : Type} (q : Tag m State) (t a : α) : + BodyDefinable (L := L) size true + (fun j v => rowStep tm (input j.1) (traceRow j.2 (v t)) q (v a)) := by + have hs (y : Situation m State) := + situation_definable (size := size) input inputFormula hinput y t a + have hi (d : SignType) := + inputPrev_definable (size := size) (m := m) (State := State) + input inputFormula hinput d t a + have hh (i : Fin m) (s : Bool) (d : SignType) := + headPrev_definable (L := L) (size := size) (State := State) i s d t a + have he (i : Fin m) (s : Bool) := + elsewhere_definable (L := L) (size := size) (State := State) i s t a + cases q with + | state q => + exact ((traceRow_definable (.state none) t a).conj + (PolarityDefinable.constant (q = none))).disj + (PolarityDefinable.iEx fun y => + (PolarityDefinable.constant ((tm.actionOf y).state = q)).conj (hs y)) + | out o => + exact ((traceRow_definable (.state none) t a).conj + (traceRow_definable (.out o) t a)).disj + (PolarityDefinable.iEx fun y => PolarityDefinable.iEx fun o' => + (PolarityDefinable.constant (o'.push (tm.actionOf y).output = o)).conj + ((hs y).conj (traceRow_definable (.out o') t a))) + | inPos => + exact ((traceRow_definable (.state none) t a).conj + (traceRow_definable .inPos t a)).disj + (PolarityDefinable.iEx fun y => (hs y).conj (hi (tm.actionOf y).inputTape)) + | head i sign => + exact ((traceRow_definable (.state none) t a).conj + (traceRow_definable (.head i sign) t a)).disj + (PolarityDefinable.iEx fun y => + (hs y).conj (hh i sign ((tm.actionOf y).workTapes i).2)) + | cell i sign s => + exact ((traceRow_definable (.cell i sign s) t a).conj + ((traceRow_definable (.state none) t a).disj (he i sign))).disj + (PolarityDefinable.iEx fun y => PolarityDefinable.iEx fun s' => + (PolarityDefinable.constant (((tm.actionOf y).workTapes i).1.getD s' = s)).conj + ((hs y).conj ((traceRow_definable (.head i sign) t a).conj + (traceRow_definable (.cell i sign s') t a)))) + +/-- The native tableau transformer has one syntactically positive defining body, uniform over +all input structures and candidate ternary relations. -/ +theorem traceStep_polarityDefinable (tm : MultiTapeTM m Bool State) (input : ι → List Bool) + (inputFormula : Option Bool → (Ordered.language L).Formula (Fin 1)) + (hinput : ∀ i s (a : Fin (size i)), + (inputFormula s).Realize ![a] ↔ inputAt (input i) a.val = s) + {α : Type} (args : Fin 3 → α) : + PolarityDefinable (L := Ordered.language L) LFP.policy LFP.headMark true + (fun j : (i : ι) × Set (Fin 3 → Fin (size i)) => Fin (size j.1)) + (fun _ => LFP.interpretation) (fun j => RelEnv.cons j.2 RelEnv.empty) + (fun j v => (v ∘ args) ∈ traceStep tm (input j.1) j.2) := by + change BodyDefinable (L := L) size true _ + simp only [traceStep, OrderHom.coe_mk, Set.mem_ofPred_eq, Function.comp_apply] + apply PolarityDefinable.iEx + intro q + apply PolarityDefinable.conj (numeral_definable true (tagIndex q) (args 0)) + apply PolarityDefinable.disj + · exact (numeral_definable true 0 (args 1)).conj (initial_definable tm q (args 2)) + · apply PolarityDefinable.ex + exact (successor_definable true none (some (args 1))).conj + (rowStep_definable tm input inputFormula hinput q none (some (args 2))) + +/-- The native tableau least fixed point is uniformly FO(LFP)-definable. -/ +theorem trace_lfp_definable (tm : MultiTapeTM m Bool State) (input : ι → List Bool) + (inputFormula : Option Bool → (Ordered.language L).Formula (Fin 1)) + (hinput : ∀ i s (a : Fin (size i)), + (inputFormula s).Realize ![a] ↔ inputAt (input i) a.val = s) + {α : Type} (args : Fin 3 → α) : + Operator.Definable (L := Ordered.language L) LFP.policy + (fun i => Fin (size i)) (fun _ => LFP.interpretation) (fun _ => RelEnv.empty) + (fun i v => (v ∘ args) ∈ (traceStep tm (input i)).lfp) := by + apply LFP.definable_lfp_vars (fun i _ => traceStep tm (input i)) args + exact traceStep_polarityDefinable tm input inputFormula hinput Sum.inr + +end Cslib.Complexity.ImmermanVardi.Tableau diff --git a/Complexity/Computability/Complexity/ImmermanVardi/Tableau/FixedPoint.lean b/Complexity/Computability/Complexity/ImmermanVardi/Tableau/FixedPoint.lean new file mode 100644 index 000000000..26329877e --- /dev/null +++ b/Complexity/Computability/Complexity/ImmermanVardi/Tableau/FixedPoint.lean @@ -0,0 +1,192 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.ImmermanVardi.Tableau.Correct +public import Mathlib.Order.FixedPoints +import Mathlib.Data.Fintype.EquivFin +import Mathlib.Data.Fin.VecNotation +import Mathlib.Tactic.FinCases + +/-! +# A least fixed point for the native deterministic computation tableau + +One ternary relation stores `(feature tag, time, position)`. Its positive transformer adds +initial facts and consequences of the preceding row. The least fixed point is exactly the +native deterministic run, uniformly for every finite domain large enough to hold the input +endmarkers and the fixed finite collection of tags. + +## Main definitions + +* `tagIndex`: input-independent numerical feature tags. +* `initial`: the initial native row, independent of the input bits. +* `traceRow`: project a ternary relation to a named row. +* `traceStep`: the monotone tableau transformer. + +## Main results + +* `traceStep_lfp`: the least fixed point equals the native run tableau. +* `traceRow_lfp`: a named row of the fixed point agrees with the corresponding native run. +-/ + +@[expose] public section + +namespace Cslib.Complexity.ImmermanVardi.Tableau + +open Turing Turing.MultiTapeTM Turing.MultiTapeTM.Feature + +variable {m B : ℕ} {State : Type} [Fintype State] + +/-- A fixed numerical encoding of the finite set of feature names. -/ +noncomputable def tagIndex (q : Tag m State) : ℕ := (Fintype.equivFin (Tag m State) q).val + +/-- The tag encoding is injective. -/ +theorem tagIndex_injective : Function.Injective (tagIndex (m := m) (State := State)) := + fun _ _ h => (Fintype.equivFin _).injective (Fin.ext h) + +/-- Every feature tag fits in a domain at least as large as the set of names. -/ +theorem tagIndex_lt (hB : Fintype.card (Tag m State) ≤ B) (q : Tag m State) : + tagIndex q < B := + lt_of_lt_of_le (Fintype.equivFin (Tag m State) q).isLt hB + +/-- The initial row of a native machine, with blank work tapes and input head at one. -/ +def initial (tm : MultiTapeTM m Bool State) : Row m State B + | .state q, _ => q = some tm.q₀ + | .out o, _ => o = .empty + | .inPos, a => a.val = 1 + | .head _ _, a => a.val = 0 + | .cell _ _ s, _ => s = none + +omit [Fintype State] in +/-- The explicit initial row agrees with the actual native initial configuration. -/ +theorem initial_iff (tm : MultiTapeTM m Bool State) (input : List Bool) + (q : Tag m State) (a : Fin B) : + initial tm q a ↔ row (tm.initCfg input) q a := by + cases q with + | head i sign => + cases sign <;> simp [initial, row, Tag.feature, Feature.Holds, offset, eq_comm] + | state q => simp [initial, row, Tag.feature, Feature.Holds, eq_comm] + | out o => simp [initial, row, Tag.feature, Feature.Holds, eq_comm] + | inPos => simp [initial, row, Tag.feature, Feature.Holds, eq_comm] + | cell i sign s => simp [initial, row, Tag.feature, Feature.Holds, eq_comm] + +/-- The row of a ternary relation at time `t`, using the fixed feature tags. -/ +def traceRow (R : Set (Fin 3 → Fin B)) (t : Fin B) : Row m State B := + fun q a => ∃ z : Fin B, z.val = tagIndex q ∧ ![z, t, a] ∈ R + +/-- The positive, time-indexed tableau transformer. -/ +noncomputable def traceStep (tm : MultiTapeTM m Bool State) (input : List Bool) : + Set (Fin 3 → Fin B) →o Set (Fin 3 → Fin B) where + toFun R := {x | ∃ q : Tag m State, (x 0).val = tagIndex q ∧ + (((x 1).val = 0 ∧ initial tm q (x 2)) ∨ + ∃ t : Fin B, t.val + 1 = (x 1).val ∧ rowStep tm input (traceRow R t) q (x 2))} + monotone' := by + intro R S h x hx + rcases hx with ⟨q, hq, hbase | ⟨t, ht, hstep⟩⟩ + · exact ⟨q, hq, Or.inl hbase⟩ + · refine ⟨q, hq, Or.inr ⟨t, ht, rowStep_mono tm input ?_ q (x 2) hstep⟩⟩ + intro q a ha + rcases ha with ⟨z, hz, hr⟩ + exact ⟨z, hz, h hr⟩ + +/-- The canonical ternary relation of all rows of the bounded native run. -/ +def runTable (tm : MultiTapeTM m Bool State) (input : List Bool) : Set (Fin 3 → Fin B) := + {x | ∃ q : Tag m State, (x 0).val = tagIndex q ∧ + row (tm.runFrom (tm.initCfg input) (x 1).val) q (x 2)} + +/-- Projecting the canonical ternary table recovers exactly the desired native row. -/ +theorem traceRow_runTable (tm : MultiTapeTM m Bool State) (input : List Bool) + (hB : Fintype.card (Tag m State) ≤ B) (t : Fin B) (q : Tag m State) (a : Fin B) : + traceRow (runTable tm input) t q a ↔ + row (tm.runFrom (tm.initCfg input) t.val) q a := by + constructor + · rintro ⟨z, hz, q', hq', hr⟩ + have hqq : q' = q := tagIndex_injective (hq'.symm.trans hz) + simpa [hqq] using hr + · intro hr + exact ⟨⟨tagIndex q, tagIndex_lt hB q⟩, rfl, q, rfl, hr⟩ + +private theorem traceRow_runTable_eq (tm : MultiTapeTM m Bool State) (input : List Bool) + (hB : Fintype.card (Tag m State) ≤ B) (t : Fin B) : + traceRow (runTable tm input) t = row (tm.runFrom (tm.initCfg input) t.val) := + funext fun q => funext fun a => propext (traceRow_runTable tm input hB t q a) + +/-- The exact native table is closed under all positive tableau rules. -/ +theorem traceStep_runTable_le (tm : MultiTapeTM m Bool State) (input : List Bool) + (hn : input.length + 1 < B) (hB : Fintype.card (Tag m State) ≤ B) : + traceStep (B := B) tm input (runTable tm input) ⊆ runTable tm input := by + rintro x ⟨q, hq, ⟨ht, hinit⟩ | ⟨t, ht, hstep⟩⟩ + · refine ⟨q, hq, ?_⟩ + simpa only [ht, runFrom, Function.iterate_zero_apply] + using (initial_iff tm input q (x 2)).1 hinit + · refine ⟨q, hq, ?_⟩ + rw [traceRow_runTable_eq tm input hB] at hstep + have hb : ∀ i, |(tm.runFrom (tm.initCfg input) t.val).workTapePos i| + 1 < B := by + intro i + have := tm.abs_workTapePos_runFrom_le input t.val i + have := (x 1).isLt + omega + have hs := (rowStep_row tm hn hb q (x 2)).1 hstep + simpa only [← ht, runFrom_succ] using hs + +/-- The least fixed point contains every native row. -/ +theorem runTable_le_traceStep_lfp (tm : MultiTapeTM m Bool State) (input : List Bool) + (hn : input.length + 1 < B) (hB : Fintype.card (Tag m State) ≤ B) : + runTable tm input ⊆ (traceStep (B := B) tm input).lfp := by + have hrow : ∀ n, ∀ (t : Fin B), t.val = n → ∀ q a, + row (tm.runFrom (tm.initCfg input) n) q a → + traceRow (traceStep tm input).lfp t q a := by + intro n + induction n with + | zero => + intro t ht q a hr + let z : Fin B := ⟨tagIndex q, tagIndex_lt hB q⟩ + refine ⟨z, rfl, ?_⟩ + rw [← (traceStep (B := B) tm input).map_lfp] + exact ⟨q, rfl, Or.inl ⟨ht, (initial_iff tm input q a).2 hr⟩⟩ + | succ n ih => + intro t ht q a hr + let p : Fin B := ⟨n, by have := t.isLt; omega⟩ + let z : Fin B := ⟨tagIndex q, tagIndex_lt hB q⟩ + refine ⟨z, rfl, ?_⟩ + rw [← (traceStep (B := B) tm input).map_lfp] + refine ⟨q, rfl, Or.inr ⟨p, ht.symm, ?_⟩⟩ + have hb : ∀ i, |(tm.runFrom (tm.initCfg input) n).workTapePos i| + 1 < B := by + intro i + have := tm.abs_workTapePos_runFrom_le input n i + have := t.isLt + omega + have hs : rowStep tm input (row (tm.runFrom (tm.initCfg input) n)) q a := + (rowStep_row tm hn hb q a).2 (by simpa only [runFrom_succ] using hr) + exact rowStep_mono tm input (fun q a ha => ih p rfl q a ha) q a hs + rintro x ⟨q, hq, hx⟩ + obtain ⟨z, hz, hr⟩ := hrow (x 1).val (x 1) rfl q (x 2) hx + have hz' : z = x 0 := Fin.ext (hz.trans hq.symm) + have hvec : ![z, x 1, x 2] = x := by + ext i + fin_cases i <;> simp [hz'] + rwa [hvec] at hr + +/-- The native deterministic tableau is exactly a least fixed point of positive local rules. -/ +theorem traceStep_lfp (tm : MultiTapeTM m Bool State) (input : List Bool) + (hn : input.length + 1 < B) (hB : Fintype.card (Tag m State) ≤ B) : + (traceStep (B := B) tm input).lfp = runTable tm input := + Set.Subset.antisymm + ((traceStep tm input).lfp_le (traceStep_runTable_le tm input hn hB)) + (runTable_le_traceStep_lfp tm input hn hB) + +/-- Each named row of the least fixed point is the corresponding native configuration. -/ +theorem traceRow_lfp (tm : MultiTapeTM m Bool State) (input : List Bool) + (hn : input.length + 1 < B) (hB : Fintype.card (Tag m State) ≤ B) + (t : Fin B) (q : Tag m State) (a : Fin B) : + traceRow (traceStep tm input).lfp t q a ↔ + row (tm.runFrom (tm.initCfg input) t.val) q a := by + rw [traceStep_lfp tm input hn hB] + exact traceRow_runTable tm input hB t q a + +end Cslib.Complexity.ImmermanVardi.Tableau diff --git a/Complexity/Computability/Complexity/ImmermanVardi/Tableau/Step.lean b/Complexity/Computability/Complexity/ImmermanVardi/Tableau/Step.lean new file mode 100644 index 000000000..c4c9d91ab --- /dev/null +++ b/Complexity/Computability/Complexity/ImmermanVardi/Tableau/Step.lean @@ -0,0 +1,209 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Machines.Turing.MultiTape.Feature +import Mathlib.Data.Fintype.Sum + +/-! +# Positive local rules for native deterministic tableaux + +The finite collection of tape-feature names is independent of the input and time bound. +`rowStep` computes the next row using only positive occurrences of the preceding row. +In particular, a cell is preserved when a positively witnessed head is elsewhere. This +avoids the negative recursive head test in an ordinary tableau constraint. + +The semantics are the native `Turing.MultiTapeTM` configurations and transition function. +These rules are the local part of the machine-to-LFP construction in the proof of the +Immerman–Vardi theorem; they do not assume a machine-to-formula compiler. + +## Main definitions + +* `Tag`: the finite feature names, with signed work-tape coordinates. +* `row`: the row described by a native configuration. +* `rowStep`: the positive local transition rules. + +## Main results + +* `rowStep_mono`: monotonicity in every preceding-row fact. + +## References + +* [N. Immerman, *Relational Queries Computable in Polynomial Time*][Immerman1986], Section 3. +-/ + +@[expose] public section + +namespace Cslib.Complexity.ImmermanVardi.Tableau + +open Turing Turing.MultiTapeTM Turing.MultiTapeTM.Feature + +/-- The input-independent names of basic features. Unary facts use every coordinate. -/ +inductive Tag (m : ℕ) (State : Type) where + /-- The control state, including the halted state. -/ + | state (q : Option State) + /-- The finite view of the output word. -/ + | out (o : OutView) + /-- The position of the input head. -/ + | inPos + /-- The position of a work head; `true` is the nonnegative orientation. -/ + | head (i : Fin m) (sign : Bool) + /-- The contents of a signed work cell. -/ + | cell (i : Fin m) (sign : Bool) (s : Option Bool) + deriving DecidableEq, Fintype + +variable {m B : ℕ} {State : Type} + +/-- Interpret an oriented coordinate as an integer tape offset. -/ +def offset (sign : Bool) (a : Fin B) : ℤ := if sign then a.val else -a.val + +/-- The feature named by a tag at the specified coordinate. -/ +def Tag.feature : Tag m State → Fin B → Feature m State + | .state q, _ => .state q + | .out o, _ => .out o + | .inPos, a => .inPos a.val + | .head i sign, a => .head i (offset sign a) + | .cell i sign s, a => .cell i (offset sign a) s + +/-- A row of facts, represented by its positive relation entries. -/ +abbrev Row (m : ℕ) (State : Type) (B : ℕ) := Tag m State → Fin B → Prop + +/-- The row described by a native machine configuration. -/ +def row {input : List Bool} (cfg : Cfg m Bool State input) : Row m State B := + fun q a => (q.feature a).Holds cfg + +/-- A positive witness for the symbol under a work head. -/ +def read (R : Row m State B) (i : Fin m) (s : Option Bool) : Prop := + ∃ a, (R (.head i true) a ∧ R (.cell i true s) a) ∨ + (R (.head i false) a ∧ R (.cell i false s) a) + +/-- A positive witness for a running situation. -/ +def situation (input : List Bool) (R : Row m State B) (y : Situation m State) + (a : Fin B) : Prop := + R (.state (some y.1)) a ∧ + (∃ j, R .inPos j ∧ inputAt input j.val = y.2.1) ∧ + ∀ i, read R i (y.2.2 i) + +/-- A head known positively to be somewhere other than the specified signed cell. -/ +def elsewhere (R : Row m State B) (i : Fin m) (sign : Bool) (a : Fin B) : Prop := + ∃ b, (R (.head i sign) b ∧ b ≠ a) ∨ + (R (.head i (!sign)) b ∧ ¬(b.val = 0 ∧ a.val = 0)) + +/-- The positive predecessor rule for an input-head movement, including clamped end cells. -/ +def inputPrev (input : List Bool) (R : Row m State B) (d : SignType) (a : Fin B) : Prop := + match d with + | .zero => R .inPos a + | .neg => (a.val = 0 ∧ R .inPos a) ∨ ∃ b, a.val + 1 = b.val ∧ R .inPos b + | .pos => (a.val ≠ 0 ∧ inputAt input a.val = none ∧ R .inPos a) ∨ + ∃ b, b.val + 1 = a.val ∧ R .inPos b ∧ + (b.val = 0 ∨ inputAt input b.val ≠ none) + +/-- The positive predecessor rule for a work-head movement, in the target orientation. -/ +def headPrev (R : Row m State B) (i : Fin m) (sign : Bool) (d : SignType) + (a : Fin B) : Prop := + match (if sign then d else -d) with + | .zero => R (.head i sign) a + | .neg => ∃ b, a.val + 1 = b.val ∧ R (.head i sign) b + | .pos => + (a.val = 0 ∧ ∃ b, b.val = 1 ∧ R (.head i (!sign)) b) ∨ + ∃ b, b.val + 1 = a.val ∧ R (.head i sign) b + +/-- Positive local transition rules for each basic feature. -/ +noncomputable def rowStep (tm : MultiTapeTM m Bool State) (input : List Bool) + (R : Row m State B) : Row m State B + | .state q, a => + (R (.state none) a ∧ q = none) ∨ + ∃ y, (tm.actionOf y).state = q ∧ situation input R y a + | .out o, a => + (R (.state none) a ∧ R (.out o) a) ∨ + ∃ y o', o'.push (tm.actionOf y).output = o ∧ + situation input R y a ∧ R (.out o') a + | .inPos, a => + (R (.state none) a ∧ R .inPos a) ∨ + ∃ y, situation input R y a ∧ inputPrev input R (tm.actionOf y).inputTape a + | .head i sign, a => + (R (.state none) a ∧ R (.head i sign) a) ∨ + ∃ y, situation input R y a ∧ headPrev R i sign ((tm.actionOf y).workTapes i).2 a + | .cell i sign s, a => + (R (.cell i sign s) a ∧ (R (.state none) a ∨ elsewhere R i sign a)) ∨ + ∃ y s', ((tm.actionOf y).workTapes i).1.getD s' = s ∧ + situation input R y a ∧ R (.head i sign) a ∧ R (.cell i sign s') a + +private theorem read_mono {R S : Row m State B} (h : ∀ q a, R q a → S q a) + {i : Fin m} {s : Option Bool} (hr : read R i s) : read S i s := by + rcases hr with ⟨a, h' | h'⟩ + · exact ⟨a, Or.inl ⟨h _ _ h'.1, h _ _ h'.2⟩⟩ + · exact ⟨a, Or.inr ⟨h _ _ h'.1, h _ _ h'.2⟩⟩ + +private theorem situation_mono {input : List Bool} {R S : Row m State B} + (h : ∀ q a, R q a → S q a) {y : Situation m State} {a : Fin B} + (hr : situation input R y a) : situation input S y a := by + rcases hr with ⟨hq, ⟨j, hj, hs⟩, hw⟩ + exact ⟨h _ _ hq, ⟨j, h _ _ hj, hs⟩, fun i => read_mono h (hw i)⟩ + +private theorem elsewhere_mono {R S : Row m State B} (h : ∀ q a, R q a → S q a) + {i : Fin m} {sign : Bool} {a : Fin B} (hr : elsewhere R i sign a) : + elsewhere S i sign a := by + rcases hr with ⟨b, h' | h'⟩ + · exact ⟨b, Or.inl ⟨h _ _ h'.1, h'.2⟩⟩ + · exact ⟨b, Or.inr ⟨h _ _ h'.1, h'.2⟩⟩ + +private theorem inputPrev_mono {input : List Bool} {R S : Row m State B} + (h : ∀ q a, R q a → S q a) {d : SignType} {a : Fin B} + (hr : inputPrev input R d a) : inputPrev input S d a := by + cases d <;> simp only [inputPrev] at hr ⊢ + · exact h _ _ hr + · rcases hr with ⟨ha, hr⟩ | ⟨b, hb, hr⟩ + · exact Or.inl ⟨ha, h _ _ hr⟩ + · exact Or.inr ⟨b, hb, h _ _ hr⟩ + · rcases hr with ⟨ha, hb, hr⟩ | ⟨b, hb, hr, hx⟩ + · exact Or.inl ⟨ha, hb, h _ _ hr⟩ + · exact Or.inr ⟨b, hb, h _ _ hr, hx⟩ + +private theorem headPrev_mono {R S : Row m State B} (h : ∀ q a, R q a → S q a) + {i : Fin m} {sign : Bool} {d : SignType} {a : Fin B} + (hr : headPrev R i sign d a) : headPrev S i sign d a := by + unfold headPrev at hr ⊢ + generalize (if sign then d else -d) = e at hr ⊢ + cases e + · exact h _ _ hr + · rcases hr with ⟨b, hb, hr⟩ + exact ⟨b, hb, h _ _ hr⟩ + · rcases hr with ⟨ha, b, hb, hr⟩ | ⟨b, hb, hr⟩ + · exact Or.inl ⟨ha, b, hb, h _ _ hr⟩ + · exact Or.inr ⟨b, hb, h _ _ hr⟩ + +/-- Every recursive occurrence in the local transition rules is monotone. -/ +theorem rowStep_mono (tm : MultiTapeTM m Bool State) (input : List Bool) + {R S : Row m State B} (h : ∀ q a, R q a → S q a) : + ∀ q a, rowStep tm input R q a → rowStep tm input S q a := by + intro q a hr + cases q with + | state q => + rcases hr with ⟨hq, he⟩ | ⟨y, he, hy⟩ + · exact Or.inl ⟨h _ _ hq, he⟩ + · exact Or.inr ⟨y, he, situation_mono h hy⟩ + | out o => + rcases hr with ⟨hq, ho⟩ | ⟨y, o', he, hy, ho⟩ + · exact Or.inl ⟨h _ _ hq, h _ _ ho⟩ + · exact Or.inr ⟨y, o', he, situation_mono h hy, h _ _ ho⟩ + | inPos => + rcases hr with ⟨hq, hp⟩ | ⟨y, hy, hp⟩ + · exact Or.inl ⟨h _ _ hq, h _ _ hp⟩ + · exact Or.inr ⟨y, situation_mono h hy, inputPrev_mono h hp⟩ + | head i sign => + rcases hr with ⟨hq, hp⟩ | ⟨y, hy, hp⟩ + · exact Or.inl ⟨h _ _ hq, h _ _ hp⟩ + · exact Or.inr ⟨y, situation_mono h hy, headPrev_mono h hp⟩ + | cell i sign s => + rcases hr with ⟨hc, hq | he⟩ | ⟨y, s', he, hy, hh, hc⟩ + · exact Or.inl ⟨h _ _ hc, Or.inl (h _ _ hq)⟩ + · exact Or.inl ⟨h _ _ hc, Or.inr (elsewhere_mono h he)⟩ + · exact Or.inr ⟨y, s', he, situation_mono h hy, h _ _ hh, h _ _ hc⟩ + +end Cslib.Complexity.ImmermanVardi.Tableau diff --git a/Complexity/Logics/FirstOrder/Operator/Definability/Finite.lean b/Complexity/Logics/FirstOrder/Operator/Definability/Finite.lean new file mode 100644 index 000000000..0ef74598c --- /dev/null +++ b/Complexity/Logics/FirstOrder/Operator/Definability/Finite.lean @@ -0,0 +1,77 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Logics.FirstOrder.Operator.Definability.Polarity + +/-! +# Formula synthesis for fixed finite choices + +A fixed finite family of defining formulas can be conjoined or disjoined without changing +the relational polarity. The indexing type is independent of the structure, so these rules +construct one finite formula uniformly across all domain sizes. They support, for example, +finite machine transition tables in descriptive-complexity proofs. + +## Main results + +* `PolarityDefinable.constant`: structure-independent truth values are definable. +* `PolarityDefinable.iEx`, `PolarityDefinable.iAll`: fixed finite choices and conjunctions. + +All three rules participate in the extensible `FODefinable` synthesis rule set. +-/ + +public section + +universe u v w z s t r + +open FirstOrder Language + +namespace Cslib.Logic.FO.Operator.PolarityDefinable + +variable {L : Language.{u, v}} {O : Type s} {shape : O → Shape} {policy : Policy shape} + {ι : Type t} {M : ι → Type z} [∀ i, L.Structure (M i)] + {I : ∀ i, Interpretation shape (M i)} {Γ : List ℕ} {ρ : ∀ i, RelEnv Γ (M i)} + {mark : Marking Γ} {sign : Bool} {α : Type w} + +/-- A proposition independent of the structure and assignment has a constant formula. -/ +theorem constant (p : Prop) : + PolarityDefinable (L := L) policy mark sign M I ρ (fun _ (_ : α → _) => p) := by + classical + by_cases hp : p + · exact truth.congr fun _ _ => iff_of_true trivial hp + · exact falsity.congr fun _ _ => iff_of_false not_false hp + +/-- A fixed finite disjunction preserves a certified polarity. -/ +theorem iEx {β : Type r} [Finite β] {P : β → ∀ i, (α → M i) → Prop} + (hP : ∀ b, PolarityDefinable (L := L) policy mark sign M I ρ (P b)) : + PolarityDefinable (L := L) policy mark sign M I ρ (fun i v => ∃ b, P b i v) := by + classical + let _ := Fintype.ofFinite β + have hlist (l : List β) : PolarityDefinable (L := L) policy mark sign M I ρ + (fun i v => ∃ b ∈ l, P b i v) := by + induction l with + | nil => exact falsity.congr fun _ _ => by simp + | cons b l ih => exact ((hP b).disj ih).congr fun _ _ => by simp + exact (hlist (Finset.univ : Finset β).toList).congr fun _ _ => by simp + +/-- A fixed finite conjunction preserves a certified polarity. -/ +theorem iAll {β : Type r} [Finite β] {P : β → ∀ i, (α → M i) → Prop} + (hP : ∀ b, PolarityDefinable (L := L) policy mark sign M I ρ (P b)) : + PolarityDefinable (L := L) policy mark sign M I ρ (fun i v => ∀ b, P b i v) := by + classical + let _ := Fintype.ofFinite β + have hlist (l : List β) : PolarityDefinable (L := L) policy mark sign M I ρ + (fun i v => ∀ b ∈ l, P b i v) := by + induction l with + | nil => exact truth.congr fun _ _ => by simp + | cons b l ih => exact ((hP b).conj ih).congr fun _ _ => by simp + exact (hlist (Finset.univ : Finset β).toList).congr fun _ _ => by simp + +attribute [aesop safe apply (rule_sets := [FODefinable])] constant iEx iAll + +end Cslib.Logic.FO.Operator.PolarityDefinable diff --git a/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint.lean b/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint.lean index a72e77f41..f913edd6a 100644 --- a/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint.lean +++ b/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint.lean @@ -42,8 +42,9 @@ Negation outside a fixed-point binder and arbitrary nesting remain available. * [N. Immerman, *Relational Queries Computable in Polynomial Time*][Immerman1986], Section 1 (positive nested syntax) and Section 2, Fact 2.1 (the finite-stage bound). -This implements the logic and finite-stage semantics. A native polynomial-time evaluator and -the Immerman–Vardi capturing theorem require separate machine and encoding developments. +This module implements the logic and finite-stage semantics. The native polynomial-time evaluator +is in `Complexity.Computability.Complexity.Classes.P.FirstOrder`; the ordered characterization +is in `Complexity.Computability.Complexity.ImmermanVardi`. -/ public section diff --git a/ComplexityTests/ImmermanVardi.lean b/ComplexityTests/ImmermanVardi.lean new file mode 100644 index 000000000..86e26abf9 --- /dev/null +++ b/ComplexityTests/ImmermanVardi.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Complexity.ImmermanVardi +import Complexity.Computability.Complexity.Fagin.Verifier + +/-! # Native polynomial-time queries produce uniform checked FO(LFP) sentences -/ + +namespace ComplexityTests.ImmermanVardi + +open FirstOrder Language Turing Turing.MultiTapeTM +open Cslib.Logic Cslib.Logic.FO Cslib.Complexity + +section Queries + +variable {L : Language} [L.IsRelational] (v : Vocabulary L) + +-- The public characterization uses the existing source encoding and native machine class. +example (K : Ordered.Query L) : + Ordered.LFPDefinable K ↔ Ordered.Query.encodedLanguage K v ∈ P encStructure := + Ordered.lfpDefinable_iff_encodedLanguage_mem_P v K + +-- Start from a native constant decider, then obtain one sentence rejecting every ordered input. +example : ∃ φ : LFP.Formula (Ordered.language L) [] Empty, + ∀ M : Ordered.Structure L, ¬ φ.Realize (M := M) Operator.RelEnv.empty Empty.elim := by + have hP : Ordered.Query.encodedLanguage (∅ : Ordered.Query L) v ∈ P encStructure := by + refine ⟨fun _ => false, ComputableInPolyTime.const false, ?_⟩ + intro a + simp [Ordered.Query.encodedLanguage] + obtain ⟨φ, hφ⟩ := Ordered.LFPDefinable.of_encodedLanguage_mem_P v hP + exact ⟨φ, fun M h => (hφ M).mpr h⟩ + +-- Accepting every ordered structure still requires rejecting malformed encodings and n < 2. +-- The native guard is certified directly, before applying the machine-to-LFP direction. +example : ∃ φ : LFP.Formula (Ordered.language L) [] Empty, + ∀ M : Ordered.Structure L, φ.Realize (M := M) Operator.RelEnv.empty Empty.elim := by + have hP : Ordered.Query.encodedLanguage (Set.univ : Ordered.Query L) v ∈ P encStructure := by + refine ⟨fun a => v.checkShape a && decide (2 ≤ a.1), ?_, ?_⟩ + · fun_prop + · intro a + simp [Ordered.Query.encodedLanguage, Vocabulary.checkShape_eq_true_iff] + obtain ⟨φ, hφ⟩ := Ordered.LFPDefinable.of_encodedLanguage_mem_P v hP + exact ⟨φ, fun M => (hφ M).mp (Set.mem_univ M)⟩ + +end Queries + +private def vocabulary : Vocabulary Language.empty where + count := 0 + symbol := Equiv.equivOfIsEmpty _ _ + +private def input : EncodedStructure := (2, []) + +private theorem wellFormed : vocabulary.WellFormed input := by decide +kernel + +private instance : Fact (2 ≤ 8) := ⟨by decide⟩ + +private instance : vocabulary.powerLanguage.Structure (Fin 8) := + vocabulary.powerStructure input 8 + +-- The word is [true,true,true,true,false]: native input position one reads its first bit. +example : (vocabulary.inputSymbol none).Realize ![(0 : Fin 8)] ∧ + (vocabulary.inputSymbol (some true)).Realize ![(1 : Fin 8)] ∧ + (vocabulary.inputSymbol (some false)).Realize ![(5 : Fin 8)] := by + rw [vocabulary.realize_inputSymbol wellFormed (by decide), + vocabulary.realize_inputSymbol wellFormed (by decide), + vocabulary.realize_inputSymbol wellFormed (by decide)] + decide + +-- The right endmarker and padding are blank; the final false data bit is not blank. +example : (vocabulary.inputSymbol none).Realize ![(6 : Fin 8)] ∧ + (vocabulary.inputSymbol none).Realize ![(7 : Fin 8)] ∧ + ¬ (vocabulary.inputSymbol none).Realize ![(5 : Fin 8)] := by + rw [vocabulary.realize_inputSymbol wellFormed (by decide), + vocabulary.realize_inputSymbol wellFormed (by decide), + vocabulary.realize_inputSymbol wellFormed (by decide)] + decide + +-- Neither endmarker is misclassified as a data bit. +example : ¬ (vocabulary.inputSymbol (some true)).Realize ![(0 : Fin 8)] ∧ + ¬ (vocabulary.inputSymbol (some false)).Realize ![(6 : Fin 8)] := by + rw [vocabulary.realize_inputSymbol wellFormed (by decide), + vocabulary.realize_inputSymbol wellFormed (by decide)] + decide + +end ComplexityTests.ImmermanVardi diff --git a/ComplexityTests/ImmermanVardiTableau.lean b/ComplexityTests/ImmermanVardiTableau.lean new file mode 100644 index 000000000..3b3ece9b6 --- /dev/null +++ b/ComplexityTests/ImmermanVardiTableau.lean @@ -0,0 +1,73 @@ +import Complexity.Computability.Complexity.ImmermanVardi.Tableau.Acceptance +import Complexity.Tactic.FOOperator + +/-! Behavioral regression clients for native positive tableaux and uniform LFP synthesis. -/ + +open FirstOrder Language Turing Turing.MultiTapeTM +open Cslib.Logic.FO Cslib.Complexity.ImmermanVardi.Tableau + +local instance {M : Type} : Language.empty.Structure M := Language.emptyStructure + +private def answer (b : Bool) : MultiTapeTM 0 Bool Unit := + ofTr () fun _ _ _ => ⟨0, Fin.elim0, some b, none⟩ + +private theorem answer_one (b : Bool) (input : List Bool) : + ((answer b).runFrom ((answer b).initCfg input) 1).Halted ∧ + ((answer b).runFrom ((answer b).initCfg input) 1).output = [b] := by + rw [runFrom_one, step_of_state (q := ()) rfl] + simp [answer, tr_ofTr, Cfg.Halted, Action.apply_state, Action.apply_output] + +-- The positive tableau records the actual output of a native machine, for either answer. +example (b : Bool) : + traceRow (m := 0) (State := Unit) (traceStep (B := 8) (answer b) []).lfp + 1 (.out (.one true)) 0 ↔ b = true := by + rw [traceRow_lfp (answer b) [] (by decide) (by decide)] + change OutView.ofList ((answer b).runFrom ((answer b).initCfg []) 1).output = .one true ↔ _ + rw [(answer_one b []).2] + simp [OutView.ofList] + +-- Initial configurations are not confused with the halted configurations reached one step later. +example (b : Bool) : + ¬ traceRow (m := 0) (State := Unit) (traceStep (B := 8) (answer b) []).lfp + 0 (.state none) 0 := by + rw [traceRow_lfp (answer b) [] (by decide) (by decide)] + simp [row, Tag.feature, Feature.Holds, runFrom] + +-- The two signed representations of zero are the same cell, not an "elsewhere" witness. +example : ¬ elsewhere (B := 3) (State := Unit) + (fun q b => q = Tag.head (m := 1) 0 false ∧ b = 0) 0 true 0 := by + simp [elsewhere] + +private def emptyInputFormula : Option Bool → + (Ordered.language Language.empty).Formula (Fin 1) + | none => ⊤ + | some _ => ⊥ + +private abbrev LargeSize := {n : ℕ // 8 ≤ n} + +local instance (i : LargeSize) : Fact (2 ≤ i.val) := ⟨by have := i.property; omega⟩ + +-- A single checked sentence works simultaneously in every sufficiently large domain. +example (b : Bool) : + ∃ φ : LFP.Formula (Ordered.language Language.empty) [] Empty, + ∀ i : LargeSize, φ.Realize (M := Fin i.val) Operator.RelEnv.empty + (fun e => nomatch e) ↔ b = true := by + obtain ⟨φ, hφ⟩ := exists_acceptance_sentence (size := fun i : LargeSize => i.val) + (answer b) (fun _ => []) emptyInputFormula + (by intro i s a; cases s <;> simp [emptyInputFormula, inputAt]) + (by intro i; have := i.property; simp only [List.length_nil]; omega) + (by intro i; exact (by decide : Fintype.card (Tag 0 Unit) ≤ 8).trans i.property) + refine ⟨φ, fun i => (hφ i).trans ?_⟩ + have hrun := runFrom_eq_of_halt (answer b) ((answer b).initCfg []) + (show 1 ≤ i.val - 1 by have := i.property; omega) (answer_one b []).1 + rw [hrun] + rw [(answer_one b []).2] + simp only [List.cons.injEq, and_true] + exact ⟨And.right, fun hb => ⟨(answer_one b []).1, hb⟩⟩ + +-- Finite transition-table choices synthesize without enumerating a model's domain. +example : Operator.PolarityDefinable (L := Language.empty) LFP.policy + (Γ := []) (fun r => nomatch r) true (fun i : LargeSize => Fin i.val) + (fun _ => LFP.interpretation) (fun _ => Operator.RelEnv.empty) + (fun _ (v : Bool → _) => ∃ q : Fin 3, q = 1 ∧ v false = v true) := by + fo_definable diff --git a/README.md b/README.md index 17745c7f6..c238a3505 100644 --- a/README.md +++ b/README.md @@ -28,6 +28,7 @@ examples. For setup or a particular task, start below. | State P/NP membership or prove a problem NP-complete | [Checked plain examples](ComplexityTests/NPCompleteness.lean), then [Clique](Complexity/Computability/Complexity/Problems/Clique.lean) | | Construct circuits for polynomial-time function families | [Uniform circuit examples](ComplexityTests/UniformCircuits.lean) | | Define queries using least fixed points or tuple closure | [FO(LFP), FO(TC), and synthesis examples](ComplexityTests/FOOperators.lean) | +| Move between ordered FO(LFP) queries and native polynomial time | [Immerman–Vardi characterization](Complexity/Computability/Complexity/ImmermanVardi.lean) | | Write probabilistic programs or oracle reductions | [PPT examples](ComplexityTests/PPTTactic.lean), [oracle examples](ComplexityTests/OraclePPT.lean) | | Estimate frequencies in a stream | [Count-Min examples](ComplexityTests/CountMin.lean), then [fixed-query accuracy](Complexity/Algorithms/Streaming/CountMin/Probability.lean) | | Find a computational model or mathematical tool | [Search the API documentation](https://www.cslib.io/complexitylib/search.html), rebuilt nightly from `main`; [Complexity.lean](Complexity.lean) lists every module, and each documents its definitions, results, and references | diff --git a/ROADMAP.md b/ROADMAP.md index 213f77551..c91f75470 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -43,7 +43,6 @@ Priorities live in this list and in the tiers of [#897]. 7. [The Kabanets–Impagliazzo theorem](#circuits-and-algebraic-complexity) ([#891]) 8. [MIP = NEXP](#interactive-proofs) ([#892]) 9. [Regev's worst-case to average-case reduction](#cryptographic-landmarks) -10. [The Immerman–Vardi theorem](#descriptive-complexity-and-first-order-reductions) ## Cryptography @@ -262,12 +261,8 @@ universe size, not supplied as unverified input tables. In dependency order: - The ordered ESO-to-NP direction of Fagin's theorem. - Order-free: SAT-to-3SAT, graph-property hardness, and bridges to the separately encoded problems. -- **The Immerman–Vardi theorem:** on ordered finite structures, first-order logic with least - fixed points defines exactly the polynomial-time properties, with the machine side proved for - actual native algorithms in both directions. Build on the scoped FO(LFP) syntax and finite-stage - semantics: certify a fixed-formula evaluator with explicitly charged relation tables, then prove - the native-machine-to-positive-LFP converse. Extend the synthesis rules to nested operator bodies - and give regular-language quantifiers their ordered characteristic-word semantics. +- Extend the synthesis rules to nested operator bodies and give regular-language quantifiers + their ordered characteristic-word semantics. - Further logical characterizations on ordered structures: FO(TC) = NL and FO(DTC) = L, SO-Horn = P (Grädel), and DLOGTIME-uniform AC⁰ = FO(≤, BIT) (Barrington–Immerman–Straubing); then order-invariant and fixed-point queries and uniform translations between syntax, diff --git a/guide/ComplexityGuide/FirstOrderOperators.lean b/guide/ComplexityGuide/FirstOrderOperators.lean index 058b4f233..9c0ec75c3 100644 --- a/guide/ComplexityGuide/FirstOrderOperators.lean +++ b/guide/ComplexityGuide/FirstOrderOperators.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Samuel Schlesinger -/ import VersoManual +import Complexity.Computability.Complexity.ImmermanVardi import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint.Definability import Complexity.Logics.FirstOrder.Operator.Relabel import Complexity.Logics.FirstOrder.Operator.TransitiveClosure.Definability @@ -26,7 +27,7 @@ least fixed points. The library provides a shared syntax for these extensions, c and FO(TC) interpretations, and certificates that construct formulas from ordinary Lean predicates. ```lean -show -open FirstOrder Language Cslib.Logic.FO +open FirstOrder Language Cslib.Logic Cslib.Logic.FO ``` # Binding and Interpretation @@ -70,8 +71,50 @@ For a finite structure with `n` elements and an arity-`k` relation, iteration st relation and reaches the least fixed point by stage `n ^ k`. The theorem proves equality at that stage, including empty domains and arity zero; it counts possible tuples, rather than all possible relations. {name}`OrderHom.iterate_card_bot_eq_lfp` provides the underlying general powerset bound. -This is a semantic iteration theorem. A native polynomial-time evaluator and the ordered -Immerman–Vardi capture theorem remain separate work. +The native model checker uses this bound and charges for constructing and reading its relation +tables. Its polynomial-time certificate covers arbitrary fixed formulas, including nested fixed +points and captured parameters. + +# Capturing Polynomial Time +%%% +tag := "operator-capture" +%%% + +{name}`Cslib.Logic.FO.Ordered.lfpDefinable_iff_encodedLanguage_mem_P` proves the +Immerman–Vardi characterization using the library's native multitape Turing-machine class P: + +```lean +example {L : Language} [L.IsRelational] + (v : Vocabulary L) (K : Ordered.Query L) : + Ordered.LFPDefinable K ↔ + K.encodedLanguage v ∈ Cslib.Complexity.P encStructure := + Ordered.lfpDefinable_iff_encodedLanguage_mem_P v K +``` + +The vocabulary is fixed, finite, and relational. An ordered structure has universe `Fin n` with +`n ≥ 2`; order, BIT, zero, one, and maximum have their canonical numeric meanings. Its encoded +input contains the unary cardinality and full truth tables of the source relations. Numeric +symbols are computed from the universe size. Malformed table shapes and universes below two +are rejected by the language. This is the existing FO(≤, BIT) convention; the theorem does not +include a separate elimination of BIT from pure-order FO(LFP). + +The forward direction is {name}`Cslib.Logic.FO.Ordered.LFPDefinable.encodedLanguage_mem_P`. +For each fixed formula, the executable evaluator enumerates assignments and builds finite +relation tables, using `n ^ k` iterations at each arity-`k` binder. The native loop calculus +accounts for intermediate tables and captured input. The claim is data complexity: the formula +and vocabulary are fixed while the input structure varies. + +The converse is {name}`Cslib.Logic.FO.Ordered.LFPDefinable.of_encodedLanguage_mem_P`. +It takes an actual native polynomial-time machine and constructs one syntactically positive +tableau formula. Its least fixed point equals the native execution table. First-order formulas +recover the input symbols directly from the source encoding, including its framing and the +machine's input endmarkers. One tuple width bounds the runtime, input length, and finite feature +tags for every structure. The width and sentence are chosen before the input structure. + +{name}`Cslib.Logic.FO.Ordered.FullTupleInterpretation.onLFPSentence` transports that sentence +back to the original universe. The reusable translation handles nested binders, scales relation +arities by the tuple width, and preserves both syntactic positivity and realization. Its proof +transports all candidate fixed-point relations through the tuple equivalence. # Tuple Reachability %%% @@ -156,6 +199,12 @@ proves its semantics uniformly across the family. Register it with their syntactic polarity certificate. The current LFP synthesis rules cover first-order bodies; nested LFP syntax is supported, but an automatic rule for nested fixed-point bodies is not supplied. +Finite-choice rules also let `fo_definable` combine a fixed finite family of alternatives. The +native tableau compiler uses these rules for transition cases, with the machine's finite state +and symbol sets fixed before the input varies. Model-checker certificates are registered with +`fun_prop`, so later native programs can compose a fixed FO(LFP) query with other polynomial-time +computations without unfolding its evaluator. + # Adding Other Operators %%% tag := "operator-extensions" @@ -171,7 +220,11 @@ a body whose changes are not monotone. In a recursive context, that declaration polarity checks and conservatively excludes dependence on the recursive relation. The interface supports such an extension; no REG interpretation or FO(REG) capture theorem is implemented here. -The [checked regression examples][examples] exercise nesting, rejected negative recursion, -finite iteration, relation weakening, empty domains, and formula synthesis. +The [operator examples][examples] exercise nesting, rejected negative recursion, finite iteration, +relation weakening, empty domains, and formula synthesis. The [model-checker tests][evaluator] +cover executable iteration and encoding rejection; the [capture tests][capture] use the public +characterization and native input-symbol formulas. [examples]: https://github.com/cslib-community/complexitylib/blob/main/ComplexityTests/FOOperators.lean +[evaluator]: https://github.com/cslib-community/complexitylib/blob/main/ComplexityTests/FOLeastFixedPointPolyTime.lean +[capture]: https://github.com/cslib-community/complexitylib/blob/main/ComplexityTests/ImmermanVardi.lean