From 40ec0f41261fa08e57c7edeb2728b628bfb8c281 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:12:13 +0000 Subject: [PATCH] feat(descriptive): compile ordered FO and prove parity nondefinability Compile canonical ordered FO sentences to constant-depth polynomial-size formulas over the original relation atoms, including genuine numeric constants. Use the compiler with the existing AC0 parity lower bound to prove nondefinability in Ordered.Definable. Add concrete compiler and query regression examples. Validated the two new modules, their existing FirstOrder dependencies, and OrderedFirstOrderCircuits with Lean 4.36.0-rc2, autoImplicit=false and warnings as errors. Full repository gates are delegated to hosted CI. AI assistance: OpenAI ChatGPT/Codex authoring. Published through the GitHub connector. Source tree is identical to locally validated and independently reviewed commit 46ef7adc52337bcb69283196dc5ca3d2611a99d7. --- Complexity.lean | 2 + .../Circuit/Boolean/FirstOrder.lean | 2 + .../Circuit/Boolean/FirstOrder/Ordered.lean | 264 ++++++++++++++++++ .../Boolean/FirstOrder/Ordered/Parity.lean | 177 ++++++++++++ .../Circuit/Boolean/FirstOrder/Parity.lean | 2 + .../OrderedFirstOrderCircuits.lean | 237 ++++++++++++++++ 6 files changed, 684 insertions(+) create mode 100644 Complexity/Computability/Circuit/Boolean/FirstOrder/Ordered.lean create mode 100644 Complexity/Computability/Circuit/Boolean/FirstOrder/Ordered/Parity.lean create mode 100644 ComplexityTests/OrderedFirstOrderCircuits.lean diff --git a/Complexity.lean b/Complexity.lean index e9ed8c9a26..1037577cb8 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -594,6 +594,8 @@ public import Complexity.Computability.Circuit.Boolean.Equality public import Complexity.Computability.Circuit.Boolean.EvaluationTime public import Complexity.Computability.Circuit.Boolean.FanInTwo public import Complexity.Computability.Circuit.Boolean.FirstOrder +public import Complexity.Computability.Circuit.Boolean.FirstOrder.Ordered +public import Complexity.Computability.Circuit.Boolean.FirstOrder.Ordered.Parity public import Complexity.Computability.Circuit.Boolean.FirstOrder.Parity public import Complexity.Computability.Circuit.Boolean.Formula public import Complexity.Computability.Circuit.Boolean.Formula.Andreev diff --git a/Complexity/Computability/Circuit/Boolean/FirstOrder.lean b/Complexity/Computability/Circuit/Boolean/FirstOrder.lean index 0e6bb8e97f..bbec0d5af9 100644 --- a/Complexity/Computability/Circuit/Boolean/FirstOrder.lean +++ b/Complexity/Computability/Circuit/Boolean/FirstOrder.lean @@ -35,6 +35,8 @@ facts to grow with `n`. Sentences are those of Mathlib's model theory (`FirstOrder.Language.Sentence`), and the statements are about structures rather than an encoding of structures as bit strings. +The canonical ordered extension, including genuine `0`, `1`, and `max` constants and hardwired +`≤` and `BIT`, is in `Complexity.Computability.Circuit.Boolean.FirstOrder.Ordered`. ## Main definitions diff --git a/Complexity/Computability/Circuit/Boolean/FirstOrder/Ordered.lean b/Complexity/Computability/Circuit/Boolean/FirstOrder/Ordered.lean new file mode 100644 index 0000000000..517248895c --- /dev/null +++ b/Complexity/Computability/Circuit/Boolean/FirstOrder/Ordered.lean @@ -0,0 +1,264 @@ +/- +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.Circuit.Boolean.FirstOrder +public import Complexity.Logics.FirstOrder.Ordered.Basic +import Mathlib.Algebra.BigOperators.Fin +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.Linarith + +/-! +# Canonical ordered first-order model checking in constant depth + +A sentence of `FO.Ordered.language L` is compiled into an unbounded fan-in Boolean formula +reading only the atomic facts of the relational input vocabulary `L`. The constants `0`, `1`, +and `max`, weak order, and zero-indexed `BIT` have their canonical meanings on `Fin n`, with +`n ≥ 2`. Numeric atoms are evaluated during construction: their truth tables are not additional +input bits. Constants may occur in input-relation arguments and under quantifiers. + +The same formula decides the sentence for every input structure on this canonical universe. +Its depth is bounded independently of `n`, and its size and number of leaves are polynomial in +`n`, using the measures of the order-free compiler. This is the nonuniform upper-bound direction +of the FO(≤, BIT) characterization of AC⁰. No circuit-generation or DLOGTIME-uniformity bound is +asserted. Inputs are relation-table atoms, not serialized structure encodings; the bounds are in +the universe size, including when the input vocabulary has no positive-arity relation symbol. + +## Main definitions + +* `Cslib.Circuits.Boolean.ModelChecking.Ordered.termValue`: canonical values of ordered terms. +* `Cslib.Circuits.Boolean.ModelChecking.Ordered.toUnbounded`: compilation reading only the input + relation tables. + +## Main results + +* `Cslib.Circuits.Boolean.ModelChecking.Ordered.eval_toUnbounded_atomsOf`: correctness for + arbitrary assignments and input structures on the canonical universe. +* `Cslib.Circuits.Boolean.ModelChecking.Ordered.exists_formula_realize`: every fixed ordered + sentence has constant-depth, polynomial-size formulas on its input relation tables. +* `Cslib.Circuits.Boolean.ModelChecking.Ordered.leafSize_toUnbounded_le`: a polynomial leaf bound + for subsequent substitutions. + +## References + +* [N. Immerman, *Descriptive Complexity*][Immerman1999], Chapter 5. The formula-expansion argument + is in Section 5.4, proof of Theorem 5.22, in the + [author-hosted chapter draft](https://people.cs.umass.edu/~immerman/book/ch5.pdf); this locator + refers to that draft. Here it is specialized to a fixed sentence and proves only the + logical-to-circuit upper bound. The canonical numeric vocabulary follows Section 1.2, + Provisos 1.14–1.15. +* [D. A. M. Barrington, N. Immerman, H. Straubing, *On uniformity within NC¹*] + [BarringtonImmermanStraubing1990]. Uniformity is not proved here. +-/ + +public section + +namespace Cslib.Circuits.Boolean.ModelChecking.Ordered + +open FirstOrder FirstOrder.Language +open Cslib.Logic.FO.Ordered (language) + +variable {L : Language} [L.IsRelational] {n N : ℕ} [Fact (2 ≤ n)] + +/-- Evaluate an ordered term without using any input relation: terms are variables or one of +the three canonical numeric constants. -/ +@[expose] +def termValue {α : Type*} (v : α → Fin n) : (language L).Term α → Fin n + | .var x => v x + | .func (.inl f) _ => isEmptyElim f + | .func (.inr c) _ => ⟨c.index n, c.index_lt Fact.out⟩ + +/-- The relation-independent term evaluator agrees with canonical ordered term semantics. -/ +@[simp] +theorem termValue_eq_realize [L.Structure (Fin n)] {α : Type*} (v : α → Fin n) + (t : (language L).Term α) : termValue v t = t.realize v := by + cases t with + | var x => rfl + | func f ts => + cases f with + | inl f => exact isEmptyElim f + | inr c => cases c <;> rfl + +/-- Compile an ordered formula on `Fin n`: input relations read their original atomic facts, +numeric atoms become constants, and universal quantifiers become conjunctions over the universe. +The input enumeration contains no numeric relation tables. -/ +@[expose] +def toUnbounded (e : Atom L n ≃ Fin N) : + ∀ {k}, (language L).BoundedFormula Empty k → (Fin k → Fin n) → + Formula Unbounded.signature N + | _, .falsum, _ => constUnbounded false + | _, .equal t₁ t₂, xs => + constUnbounded (decide (termValue (Sum.elim Empty.elim xs) t₁ = + termValue (Sum.elim Empty.elim xs) t₂)) + | _, .rel (.inl R) ts, xs => + .input (e ⟨⟨_, R⟩, fun i => termValue (Sum.elim Empty.elim xs) (ts i)⟩) + | _, .rel (.inr .le) ts, xs => + constUnbounded (decide (termValue (Sum.elim Empty.elim xs) (ts 0) ≤ + termValue (Sum.elim Empty.elim xs) (ts 1))) + | _, .rel (.inr .bit) ts, xs => + constUnbounded ((termValue (Sum.elim Empty.elim xs) (ts 0)).val.testBit + (termValue (Sum.elim Empty.elim xs) (ts 1)).val) + | _, .imp φ ψ, xs => + .gate (.or 2) ![.gate .not ![toUnbounded e φ xs], toUnbounded e ψ xs] + | _, .all φ, xs => .gate (.and n) fun a => toUnbounded e φ (Fin.snoc xs a) + +/-- Compilation decides the formula on any input structure on `Fin n`, expanded by the actual +canonical numeric constants, weak order and zero-indexed BIT. -/ +theorem eval_toUnbounded_atomsOf [L.Structure (Fin n)] (e : Atom L n ≃ Fin N) {k : ℕ} + (φ : (language L).BoundedFormula Empty k) (xs : Fin k → Fin n) : + (toUnbounded e φ xs).eval Unbounded.interpretation + (atomsOf (L := L) (Equiv.refl _) ∘ e.symm) = true ↔ φ.Realize Empty.elim xs := by + classical + induction φ with + | falsum => simp [toUnbounded, BoundedFormula.Realize] + | equal t₁ t₂ => + simp only [toUnbounded, eval_constUnbounded, decide_eq_true_iff, BoundedFormula.Realize, + termValue_eq_realize] + | rel R ts => + cases R with + | inl R => + simp only [toUnbounded, Formula.eval_input, Function.comp_apply] + refine (iff_of_eq (congrArg + (fun a : Atom L n => atomsOf (L := L) (Equiv.refl _) a = true) + (e.symm_apply_apply _))).trans ?_ + simp only [atomsOf, decide_eq_true_iff, BoundedFormula.Realize, termValue_eq_realize] + rfl + | inr R => + cases R <;> + simp only [toUnbounded, eval_constUnbounded, decide_eq_true_iff, BoundedFormula.Realize, + termValue_eq_realize] <;> rfl + | imp φ ψ ihφ ihψ => + simp only [toUnbounded, Formula.eval_gate, Unbounded.interpretation_or, + BoundedFormula.Realize, ← ihφ, ← ihψ] + simp [Fin.exists_fin_two, imp_iff_not_or] + | all φ ih => + simp only [toUnbounded, Formula.eval_gate, Unbounded.interpretation_and, decide_eq_true_iff, + BoundedFormula.Realize] + exact forall_congr' fun a => ih _ + +/-- The compiled formula's depth is bounded independently of the universe size. -/ +theorem depth_toUnbounded_le (e : Atom L n ≃ Fin N) {k : ℕ} + (φ : (language L).BoundedFormula Empty k) (xs : Fin k → Fin n) : + (toUnbounded e φ xs).depth ≤ foDepth φ := by + induction φ with + | falsum => simp [toUnbounded, constUnbounded, foDepth] + | equal t₁ t₂ => + simp only [toUnbounded, constUnbounded, foDepth] + split_ifs <;> simp + | rel R ts => + cases R with + | inl R => simp [toUnbounded, foDepth] + | inr R => + cases R <;> simp only [toUnbounded, constUnbounded, foDepth] <;> split_ifs <;> simp + | imp φ ψ ihφ ihψ => + rw [toUnbounded, foDepth, Formula.depth_gate] + refine (Nat.add_le_add_right (Finset.sup_le (a := max (foDepth φ) (foDepth ψ) + 1) + fun j _ => ?_) 1).trans (by omega) + fin_cases j + · change (Formula.gate _ _).depth ≤ _ + rw [Formula.depth_gate] + refine (Nat.add_le_add_right (Finset.sup_le (a := foDepth φ) fun j _ => ?_) 1).trans + (by omega) + fin_cases j + exact ihφ xs + · exact (ihψ xs).trans (by omega) + | all φ ih => + simp only [toUnbounded, Formula.depth_gate, foDepth] + exact Nat.add_le_add_right (Finset.sup_le fun a _ => ih _) 1 + +/-- The compiled formula's size is polynomial in the universe size for each fixed formula. -/ +theorem size_toUnbounded_le (e : Atom L n ≃ Fin N) {k : ℕ} + (φ : (language L).BoundedFormula Empty k) (xs : Fin k → Fin n) : + (toUnbounded e φ xs).size ≤ foSize φ * (n + 2) ^ foSize φ := by + induction φ with + | falsum => simp [toUnbounded, constUnbounded, foSize] + | equal t₁ t₂ => + simp only [toUnbounded, constUnbounded, foSize] + split_ifs <;> simp + | rel R ts => + cases R with + | inl R => simp [toUnbounded, foSize] + | inr R => + cases R <;> simp only [toUnbounded, constUnbounded, foSize] <;> split_ifs <;> simp + | imp φ ψ ihφ ihψ => + have h₁ := ihφ xs + have h₂ := ihψ xs + simp only [toUnbounded, Formula.size_gate, Fin.sum_univ_two, Matrix.cons_val_zero, + Matrix.cons_val_one, Fin.sum_univ_one, foSize] + have hφ : (n + 2) ^ foSize φ ≤ (n + 2) ^ (foSize φ + foSize ψ + 1) := + Nat.pow_le_pow_right (by omega) (by omega) + have hψ : (n + 2) ^ foSize ψ ≤ (n + 2) ^ (foSize φ + foSize ψ + 1) := + Nat.pow_le_pow_right (by omega) (by omega) + have hpos : 2 ≤ (n + 2) ^ (foSize φ + foSize ψ + 1) := + (show 2 ≤ n + 2 by omega).trans (Nat.le_self_pow (by omega) _) + nlinarith [Nat.mul_le_mul_left (foSize φ) hφ, Nat.mul_le_mul_left (foSize ψ) hψ] + | all φ ih => + simp only [toUnbounded, Formula.size_gate, foSize] + have hsum : ∑ a : Fin n, (toUnbounded e φ (Fin.snoc xs a)).size ≤ + n * (foSize φ * (n + 2) ^ foSize φ) := + (Finset.sum_le_card_nsmul _ _ _ fun a _ => ih _).trans_eq (by simp) + have hpos : 1 ≤ (n + 2) ^ foSize φ := Nat.one_le_pow _ _ (by omega) + have := foSize_pos φ + calc _ ≤ n * (foSize φ * (n + 2) ^ foSize φ) + 1 := Nat.add_le_add_right hsum 1 + _ ≤ (foSize φ + 1) * (n + 2) ^ (foSize φ + 1) := by + rw [pow_succ] + nlinarith + +/-- The number of input leaves is polynomial in the universe size. -/ +theorem leafSize_toUnbounded_le (e : Atom L n ≃ Fin N) {k : ℕ} + (φ : (language L).BoundedFormula Empty k) (xs : Fin k → Fin n) : + (toUnbounded e φ xs).leafSize ≤ (n + 2) ^ foSize φ := by + induction φ with + | falsum => simp [toUnbounded, constUnbounded] + | equal t₁ t₂ => + simp only [toUnbounded, constUnbounded] + split_ifs <;> simp + | rel R ts => + cases R with + | inl R => simp [toUnbounded, foSize] + | inr R => + cases R <;> simp only [toUnbounded, constUnbounded] <;> split_ifs <;> simp + | imp φ ψ ihφ ihψ => + have h₁ := ihφ xs + have h₂ := ihψ xs + simp only [toUnbounded, Formula.leafSize_gate, Fin.sum_univ_two, Matrix.cons_val_zero, + Matrix.cons_val_one, Fin.sum_univ_one, foSize] + have hφ : (n + 2) ^ foSize φ ≤ (n + 2) ^ (foSize φ + foSize ψ) := + Nat.pow_le_pow_right (by omega) (by omega) + have hψ : (n + 2) ^ foSize ψ ≤ (n + 2) ^ (foSize φ + foSize ψ) := + Nat.pow_le_pow_right (by omega) (by omega) + rw [pow_succ] + nlinarith + | all φ ih => + simp only [toUnbounded, Formula.leafSize_gate, foSize] + have hsum : ∑ a : Fin n, (toUnbounded e φ (Fin.snoc xs a)).leafSize ≤ + n * (n + 2) ^ foSize φ := + (Finset.sum_le_card_nsmul _ _ _ fun a _ => ih _).trans_eq (by simp) + refine hsum.trans ?_ + rw [pow_succ, mul_comm] + exact Nat.mul_le_mul_left _ (by omega) + +/-- For each universe size at least two, one constant-depth, polynomial-size formula decides +the ordered sentence on every interpretation of the input relations. Only the original input +relation tables are inputs; the canonical numeric symbols are fixed by the universe size. -/ +theorem exists_formula_realize (φ : (language L).Sentence) (e : Atom L n ≃ Fin N) : + ∃ F : Formula Unbounded.signature N, + (∀ s : L.Structure (Fin n), letI := s; + F.eval Unbounded.interpretation (atomsOf (L := L) (Equiv.refl _) ∘ e.symm) = true ↔ + Fin n ⊨ φ) ∧ + F.depth ≤ foDepth φ ∧ F.size ≤ foSize φ * (n + 2) ^ foSize φ := by + refine ⟨toUnbounded e φ Fin.elim0, fun s => ?_, + depth_toUnbounded_le e φ _, size_toUnbounded_le e φ _⟩ + let := s + exact (eval_toUnbounded_atomsOf e φ Fin.elim0).trans (by + rw [Sentence.Realize, Formula.Realize, + Subsingleton.elim (Empty.elim : Empty → Fin n) default, + Subsingleton.elim (Fin.elim0 : Fin 0 → Fin n) default]) + +end Cslib.Circuits.Boolean.ModelChecking.Ordered diff --git a/Complexity/Computability/Circuit/Boolean/FirstOrder/Ordered/Parity.lean b/Complexity/Computability/Circuit/Boolean/FirstOrder/Ordered/Parity.lean new file mode 100644 index 0000000000..bbfacd83b2 --- /dev/null +++ b/Complexity/Computability/Circuit/Boolean/FirstOrder/Ordered/Parity.lean @@ -0,0 +1,177 @@ +/- +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.Query +public import Mathlib.SetTheory.Cardinal.Finite +import Complexity.Computability.Circuit.Boolean.FirstOrder.Ordered +import Complexity.Computability.Circuit.Boolean.FirstOrder.Parity +import Complexity.Computability.Circuit.Boolean.AC0 +import Complexity.Computability.Languages.Slice +import Mathlib.Algebra.BigOperators.Fin +import Mathlib.Tactic.Linarith + +/-! +# Parity is not definable in the canonical ordered vocabulary + +No sentence with the canonical numeric constants `0`, `1`, and `max`, weak order, and `BIT` +defines even cardinality of a unary input relation on all ordered structures of size at least +two. This states the parity separation directly in `FO.Ordered.Definable`. + +The proof compiles a hypothetical defining sentence with `ModelChecking.Ordered.toUnbounded`, +fixes the other input relations, and obtains polynomial-size constant-depth formulas for parity. +Their circuits contradict the existing `parity_notMem_AC0` theorem. The two input lengths excluded +by the ordered-structure convention are supplied by a constant circuit and an input wire. +Numeric constants are genuine function symbols with interpretations determined by the universe +size; only original relation tables supply input bits. No uniformity theorem is used. + +## Main results + +* `Cslib.Circuits.Boolean.ModelChecking.Ordered.not_definable_even_card`: even cardinality of a + unary input relation is not definable by a canonical ordered first-order sentence. + +## References + +* [M. Furst, J. B. Saxe, M. Sipser, *Parity, circuits, and the polynomial-time + hierarchy*][FurstSaxeSipser1984] +* [M. Ajtai, *Σ¹₁-formulae on finite structures*][Ajtai1983] +* [N. Immerman, *Descriptive Complexity*][Immerman1999] + +The result here is the canonical-structure corollary of the library's parity circuit lower bound; +it includes the genuine numeric constants excluded by the relational-only separation. +-/ + +public section + +namespace Cslib.Circuits.Boolean.ModelChecking.Ordered + +open FirstOrder FirstOrder.Language Finset +open Cslib.Logic.FO.Ordered (language) + +variable {L : Language} [L.IsRelational] [Finite (Σ l, L.Relations l)] {n : ℕ} + +/-- Compiling and restricting an ordered sentence defining even cardinality gives small, +bounded-depth formulas for parity. -/ +private theorem exists_formula_computes_parity [Fact (2 ≤ n)] (P : L.Relations 1) + (N : L.Structure (Fin n)) (φ : (language L).Sentence) + (h : ∀ S : Finset (Fin n), + letI : L.Structure (Fin n) := inferInstanceAs (L.Structure (Expansion P N S)); + Fin n ⊨ φ ↔ Even #S) : + ∃ F : Circuits.Formula Unbounded.signature n, + F.Computes Unbounded.interpretation (parity n) ∧ F.depth ≤ foDepth φ + 2 ∧ + F.size ≤ (foSize φ + 2) * (n + 2) ^ foSize φ := by + classical + have := Fintype.ofFinite (Σ l, L.Relations l) + let e : Atom L n ≃ Fin (Fintype.card (Atom L n)) := Fintype.equivFin _ + let G := toUnbounded e φ Fin.elim0 + let sub : Fin (Fintype.card (Atom L n)) → Circuits.Formula Unbounded.signature n := fun j => + if (e.symm j).1 = ⟨1, P⟩ then .gate (.and _) fun i => .input ((e.symm j).2 i) + else constUnbounded (decide (N.RelMap (e.symm j).1.2 (e.symm j).2)) + have hsubd : ∀ j, (sub j).depth ≤ 1 := fun j => by + simp only [sub, constUnbounded] + split_ifs <;> simp + have hsubs : ∀ j, (sub j).size ≤ 1 := fun j => by + simp only [sub, constUnbounded] + split_ifs <;> simp + refine ⟨.gate .not ![G.bind sub], fun y => ?_, ?_, ?_⟩ + · set S : Finset (Fin n) := {i | y i = true} + let : L.Structure (Fin n) := inferInstanceAs (L.Structure (Expansion P N S)) + have hatoms : (fun j => (sub j).eval Unbounded.interpretation y) = + atomsOf (L := L) (M := Expansion P N S) (Equiv.refl _) ∘ e.symm := by + funext j + simp only [sub, Function.comp_apply, atomsOf] + obtain ⟨⟨l, R⟩, t⟩ := e.symm j + by_cases hR : (⟨l, R⟩ : Σ l, L.Relations l) = ⟨1, P⟩ + · rw [ite_eq_left hR] + refine Bool.eq_iff_iff.2 ?_ + simp only [Circuits.Formula.eval_gate, Circuits.Formula.eval_input, + Unbounded.interpretation_and, decide_eq_true_iff] + change _ ↔ (if _ then _ else _) + rw [ite_eq_left hR] + refine forall_congr' fun i => ?_ + change _ ↔ t i ∈ S + simp [S] + · rw [ite_eq_right hR] + refine Bool.eq_iff_iff.2 ?_ + simp only [eval_constUnbounded, decide_eq_true_iff] + exact (Expansion.relMap_of_ne hR _).symm + have hreal : (G.bind sub).eval Unbounded.interpretation y = true ↔ Even #S := by + rw [Circuits.Formula.eval_bind, hatoms] + refine (eval_toUnbounded_atomsOf e φ Fin.elim0).trans ?_ + rw [Subsingleton.elim (Empty.elim : Empty → Fin n) default, + Subsingleton.elim (Fin.elim0 : Fin 0 → Fin n) default] + exact h S + simp only [Circuits.Formula.eval_gate, Unbounded.interpretation_not, Matrix.cons_val_zero] + change _ = decide (#S % 2 = 1) + rw [Nat.even_iff] at hreal + cases hv : (G.bind sub).eval Unbounded.interpretation y + · rw [hv] at hreal + have : #S % 2 = 1 := by + rcases Nat.mod_two_eq_zero_or_one #S with h0 | h1 + · exact absurd (hreal.2 h0) (by simp) + · exact h1 + simp [this] + · have := hreal.1 hv + simp [this] + · have h := Circuits.Formula.depth_bind_le hsubd G + have hG : G.depth ≤ foDepth φ := depth_toUnbounded_le e φ Fin.elim0 + simp only [Circuits.Formula.depth_gate, Finset.univ_unique, Finset.sup_singleton, + Fin.default_eq_zero, Matrix.cons_val_zero] + omega + · have h := Circuits.Formula.size_bind_le hsubs G + have hs : G.size ≤ foSize φ * (n + 2) ^ foSize φ := size_toUnbounded_le e φ Fin.elim0 + have hl : G.leafSize ≤ (n + 2) ^ foSize φ := leafSize_toUnbounded_le e φ Fin.elim0 + have hpos : 1 ≤ (n + 2) ^ foSize φ := Nat.one_le_pow _ _ (by omega) + simp only [Circuits.Formula.size_gate, Fin.sum_univ_one, Matrix.cons_val_zero] + nlinarith + +/-- **Parity is not definable in canonical ordered first-order logic.** In any finite relational +input vocabulary with a unary relation `P`, no sentence using canonical `≤`, `BIT`, `0`, `1`, and +`max` defines even cardinality of `P` on all ordered structures of size at least two. -/ +theorem not_definable_even_card (P : L.Relations 1) : + ¬ Cslib.Logic.FO.Ordered.Definable {M : Cslib.Logic.FO.Ordered.Structure L | + Even (Nat.card {x : M // Structure.RelMap P ![x]})} := by + classical + rintro ⟨φ, hφ⟩ + apply parity_notMem_AC0 + refine ConstDepth.mem_iff.2 + ⟨foDepth φ + 2, fun n => (foSize φ + 2) * (n + 2) ^ foSize φ, by fun_prop, fun n => ?_⟩ + rw [_root_.Language.slice_ofSlices] + suffices ∃ F : Circuits.Formula Unbounded.signature n, + F.Computes Unbounded.interpretation (parity n) ∧ F.depth ≤ foDepth φ + 2 ∧ + F.size ≤ (foSize φ + 2) * (n + 2) ^ foSize φ by + obtain ⟨F, hF, hd, hs⟩ := this + exact ⟨F.toCircuit, hF.toCircuit, F.depth_toCircuit_le.trans hd, by simpa using hs⟩ + by_cases hn : 2 ≤ n + · let : Fact (2 ≤ n) := ⟨hn⟩ + let N : L.Structure (Fin n) := ⟨fun f => isEmptyElim f, fun _ _ => False⟩ + refine exists_formula_computes_parity P N φ fun S => ?_ + let : L.Structure (Fin n) := inferInstanceAs (L.Structure (Expansion P N S)) + let M : Cslib.Logic.FO.Ordered.Structure L := + ⟨n, hn, inferInstanceAs (L.Structure (Expansion P N S))⟩ + have hcard : Nat.card {x : M // Structure.RelMap P ![x]} = #S := by + rw [← Nat.card_eq_finsetCard S] + refine Nat.card_congr (Equiv.subtypeEquivRight fun x => ?_) + exact Expansion.relMap_self (P := P) (N := N) (S := S) ![x] + have hM := (hφ M).symm + change (Fin n ⊨ φ) ↔ Even (Nat.card {x : M // Structure.RelMap P ![x]}) at hM + rwa [hcard] at hM + · have hn' : n = 0 ∨ n = 1 := by omega + rcases hn' with rfl | rfl + · refine ⟨constUnbounded false, ?_, ?_, ?_⟩ + · intro x + simp [parity] + · simp [constUnbounded] + · have hpow : 1 ≤ (0 + 2) ^ foSize φ := Nat.one_le_pow _ _ (by omega) + simp only [constUnbounded, Bool.false_eq_true, ↓reduceIte, Circuits.Formula.size_gate] + simpa using (show 1 ≤ (foSize φ + 2) * (0 + 2) ^ foSize φ by nlinarith) + · refine ⟨.input 0, ?_, by simp, by simp⟩ + intro x + simp [parity, Finset.univ_unique, Fin.default_eq_zero] + +end Cslib.Circuits.Boolean.ModelChecking.Ordered diff --git a/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean b/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean index aa59154d99..ff2420c4cc 100644 --- a/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean +++ b/Complexity/Computability/Circuit/Boolean/FirstOrder/Parity.lean @@ -44,6 +44,8 @@ The language is relational, as in `ModelChecking.toUnbounded`, and has finitely symbols, so that a structure on `Fin n` has finitely many atomic facts. Constant symbols, such as `min` and `max` in [Immerman1999], are not covered; a numerical constant can be expressed by a unary numerical relation holding of one element. +The separation with genuine canonical `0`, `1`, and `max` constants, stated directly through +`FO.Ordered.Definable`, is in `Complexity.Computability.Circuit.Boolean.FirstOrder.Ordered.Parity`. ## Main definitions diff --git a/ComplexityTests/OrderedFirstOrderCircuits.lean b/ComplexityTests/OrderedFirstOrderCircuits.lean new file mode 100644 index 0000000000..52d5ec3925 --- /dev/null +++ b/ComplexityTests/OrderedFirstOrderCircuits.lean @@ -0,0 +1,237 @@ +/- +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.Circuit.Boolean.FirstOrder.Ordered +import Complexity.Computability.Circuit.Boolean.FirstOrder.Ordered.Parity + +/-! +# Canonical ordered first-order circuit clients + +These examples evaluate the generated formulas on actual input bits. They cover genuine numeric +constants in input atoms, least-significant-bit indexing, quantifier binding, exact gate and leaf +counts, the minimum permitted universe, and a numeric-only sentence with no input bits. +-/ + +namespace ComplexityTests.OrderedFirstOrderCircuits + +open FirstOrder Language +open Cslib.Circuits.Boolean + +private inductive Relation : ℕ → Type + | mark : Relation 1 + +private abbrev inputLanguage : Language where + Functions _ := Empty + Relations := Relation + +private instance : inputLanguage.IsRelational := fun _ => inferInstance + +private def atomEquiv (n : ℕ) : ModelChecking.Atom inputLanguage n ≃ Fin n where + toFun a := match a with | ⟨⟨_, .mark⟩, xs⟩ => xs 0 + invFun i := ⟨⟨1, .mark⟩, fun _ => i⟩ + left_inv := by + rintro ⟨⟨_, r⟩, xs⟩ + cases r + exact congrArg + (fun t : Fin 1 → Fin n => (⟨⟨1, Relation.mark⟩, t⟩ : ModelChecking.Atom inputLanguage n)) + (funext fun i => congrArg xs (Subsingleton.elim 0 i)) + right_inv _ := rfl + +open Cslib.Logic.FO.Ordered + +private instance : Fact (2 ≤ 2) := ⟨by decide⟩ +private instance : Fact (2 ≤ 3) := ⟨by decide⟩ +private instance : Fact (2 ≤ 9) := ⟨by decide⟩ + +private def compile {n : ℕ} [Fact (2 ≤ n)] (φ : (language inputLanguage).Sentence) := + ModelChecking.Ordered.toUnbounded (atomEquiv n) φ Fin.elim0 + +private def marked (t : (language inputLanguage).Term Empty) : + (language inputLanguage).Sentence := + Relations.formula₁ (L := language inputLanguage) (Sum.inl Relation.mark) t + +-- All three numeric constants can occur directly in an input-relation argument. +example : + (compile (n := 3) (marked (zero inputLanguage))).eval Unbounded.interpretation + ![true, false, true] = true ∧ + (compile (n := 3) (marked (one inputLanguage))).eval Unbounded.interpretation + ![true, false, true] = false ∧ + (compile (n := 3) (marked (max inputLanguage))).eval Unbounded.interpretation + ![true, false, true] = true := by decide + +-- Compiling an input atom produces exactly one input leaf and no operation gate. +example : + (compile (n := 3) (marked (max inputLanguage))).size = 0 ∧ + (compile (n := 3) (marked (max inputLanguage))).depth = 0 ∧ + (compile (n := 3) (marked (max inputLanguage))).leafSize = 1 := by decide + +private def lowBit : (language inputLanguage).Sentence := + bit inputLanguage (max inputLanguage) (zero inputLanguage) + +private def nextBit : (language inputLanguage).Sentence := + bit inputLanguage (max inputLanguage) (one inputLanguage) + +-- In the non-power-of-two universe of size three, max is binary 10. +example : + (compile (n := 3) lowBit).eval Unbounded.interpretation ![true, true, true] = false ∧ + (compile (n := 3) nextBit).eval Unbounded.interpretation ![false, false, false] = true ∧ + (compile (n := 2) lowBit).eval Unbounded.interpretation ![false, false] = true := by decide + +-- Numeric predicates read no input leaves, even when all source bits change. +example (x y : Fin 3 → Bool) : + (compile (n := 3) nextBit).eval Unbounded.interpretation x = + (compile (n := 3) nextBit).eval Unbounded.interpretation y ∧ + (compile (n := 3) nextBit).size = 1 ∧ + (compile (n := 3) nextBit).depth = 1 ∧ + (compile (n := 3) nextBit).leafSize = 0 := by + refine ⟨?_, by decide⟩ + change (ModelChecking.constUnbounded true).eval Unbounded.interpretation x = + (ModelChecking.constUnbounded true).eval Unbounded.interpretation y + simp + +private def mixed : (language inputLanguage).Sentence := + ((Relations.boundedFormula₁ (L := language inputLanguage) (Sum.inl Relation.mark) + (.var (.inr 0))).iff + (Relations.boundedFormula₂ (L := language inputLanguage) (Sum.inr NumericRelation.bit) + (.var (.inr 0)) (one inputLanguage)) ⊓ + (Relations.boundedFormula₂ (L := language inputLanguage) (Sum.inr NumericRelation.le) + (zero inputLanguage) (.var (.inr 0))) ⊓ + (Relations.boundedFormula₂ (L := language inputLanguage) (Sum.inr NumericRelation.le) + (.var (.inr 0)) (max inputLanguage))).all + +-- A quantified formula accepts exactly the intended input predicate, with fixed numeric data. +example : + (compile (n := 3) mixed).eval Unbounded.interpretation ![false, false, true] = true ∧ + (compile (n := 3) mixed).eval Unbounded.interpretation ![false, true, true] = false ∧ + (compile (n := 2) mixed).eval Unbounded.interpretation ![false, false] = true := by decide + +private def nested : (language inputLanguage).Sentence := + ((Term.var (Sum.inr (0 : Fin 2)) : (language inputLanguage).Term (Empty ⊕ Fin 2)).bdEqual + (.var (.inr 1)) ⊓ + Relations.boundedFormula₂ (L := language inputLanguage) (Sum.inr NumericRelation.le) + (.var (.inr 1)) (max inputLanguage)).ex.all + +-- The existentially bound variable can equal the surrounding universally bound variable. +example : + (compile (n := 3) nested).eval Unbounded.interpretation ![false, true, false] = true ∧ + (compile (n := 2) nested).eval Unbounded.interpretation ![true, false] = true := by decide + +private def markedAbove : (language inputLanguage).Sentence := + (Relations.boundedFormula₂ (L := language inputLanguage) (Sum.inr NumericRelation.le) + (.var (.inr (0 : Fin 2))) (.var (.inr 1)) ⊓ + Relations.boundedFormula₁ (L := language inputLanguage) (Sum.inl Relation.mark) + (.var (.inr 1))).ex.all + +-- Every x has a marked y above it exactly when max is marked. Reversing the two bound +-- variables, or capturing the outer variable, changes one of these two verdicts. +example : + (compile (n := 3) markedAbove).eval Unbounded.interpretation ![false, false, true] = true ∧ + (compile (n := 3) markedAbove).eval Unbounded.interpretation ![true, false, false] = false := + by decide + +private def allMarked : (language inputLanguage).Sentence := + (Relations.boundedFormula₁ (L := language inputLanguage) (Sum.inl Relation.mark) + (.var (.inr 0))).all + +-- Quantifier expansion adds one gate, while its three relation-table leaves remain inputs. +example : + (compile (n := 3) allMarked).size = 1 ∧ + (compile (n := 3) allMarked).depth = 1 ∧ + (compile (n := 3) allMarked).leafSize = 3 := by decide + +-- The correctness theorem applies to the same explicit enumeration used by computation. +example (s : inputLanguage.Structure (Fin 3)) : + letI := s; + (compile (n := 3) mixed).eval Unbounded.interpretation + (ModelChecking.atomsOf (L := inputLanguage) (Equiv.refl _) ∘ (atomEquiv 3).symm) = true ↔ + Fin 3 ⊨ mixed := by + let _ := s + exact (ModelChecking.Ordered.eval_toUnbounded_atomsOf (atomEquiv 3) mixed Fin.elim0).trans (by + rw [Sentence.Realize, Formula.Realize] + exact iff_of_eq (congrArg₂ + (fun (v : Empty → Fin 3) (xs : Fin 0 → Fin 3) => BoundedFormula.Realize mixed v xs) + (Subsingleton.elim _ _) (Subsingleton.elim _ _))) + +private def emptyAtoms (n : ℕ) : ModelChecking.Atom Language.empty n ≃ Fin 0 where + toFun a := a.1.2.elim + invFun := Fin.elim0 + left_inv a := a.1.2.elim + right_inv i := i.elim0 + +-- No positive-arity input symbol is required: this is a formula on zero input bits. +example : + (ModelChecking.Ordered.toUnbounded (n := 3) (emptyAtoms 3) + (bit Language.empty (max Language.empty) (one Language.empty)) Fin.elim0).eval + Unbounded.interpretation Fin.elim0 = true ∧ + (ModelChecking.Ordered.toUnbounded (n := 2) (emptyAtoms 2) + ((zero Language.empty).equal (one Language.empty)) Fin.elim0).eval + Unbounded.interpretation Fin.elim0 = false := by decide + +private inductive NullaryRelation : ℕ → Type + | flag : NullaryRelation 0 + +private abbrev nullaryLanguage : Language where + Functions _ := Empty + Relations := NullaryRelation + +private instance : nullaryLanguage.IsRelational := fun _ => inferInstance + +private def nullaryAtoms (n : ℕ) : ModelChecking.Atom nullaryLanguage n ≃ Fin 1 where + toFun _ := 0 + invFun _ := ⟨⟨0, .flag⟩, Fin.elim0⟩ + left_inv := by + rintro ⟨⟨_, r⟩, xs⟩ + cases r + exact congrArg + (fun t : Fin 0 → Fin n => (⟨⟨0, NullaryRelation.flag⟩, t⟩ : + ModelChecking.Atom nullaryLanguage n)) (Subsingleton.elim _ _) + right_inv i := Subsingleton.elim _ _ + +private def flag : (language nullaryLanguage).Sentence := + .rel (Sum.inl NullaryRelation.flag) Fin.elim0 + +-- A nullary input relation still contributes one input bit at every universe size. +example : + (ModelChecking.Ordered.toUnbounded (n := 2) (nullaryAtoms 2) flag Fin.elim0).eval + Unbounded.interpretation ![true] = true ∧ + (ModelChecking.Ordered.toUnbounded (n := 3) (nullaryAtoms 3) flag Fin.elim0).eval + Unbounded.interpretation ![false] = false ∧ + (ModelChecking.Ordered.toUnbounded (n := 3) (nullaryAtoms 3) flag Fin.elim0).leafSize = 1 := + by decide + +private instance : Fintype (Σ l, inputLanguage.Relations l) where + elems := {⟨1, Relation.mark⟩} + complete := by rintro ⟨_, r⟩; cases r; simp + +private def markedStructure {n : ℕ} [Fact (2 ≤ n)] (x : Fin n → Bool) : + Cslib.Logic.FO.Ordered.Structure inputLanguage := + ⟨n, Fact.out, { RelMap := fun r t => match r with | .mark => x (t 0) = true }⟩ + +private def evenMarked : Query inputLanguage := + {M | Even (Nat.card {x : M // + FirstOrder.Language.Structure.RelMap (L := inputLanguage) Relation.mark ![x]})} + +-- The separated query has both accepting and rejecting canonical structures, including +-- the empty predicate, an even nonempty predicate, and a singleton predicate. +example : markedStructure ![false, false] ∈ evenMarked := by + change Even (Nat.card {x : Fin 2 // ![false, false] x = true}) + rw [Nat.card_eq_fintype_card] + decide + +example : markedStructure ![true, true] ∈ evenMarked := by + change Even (Nat.card {x : Fin 2 // ![true, true] x = true}) + rw [Nat.card_eq_fintype_card] + decide + +example : markedStructure ![true, false] ∉ evenMarked := by + change ¬ Even (Nat.card {x : Fin 2 // ![true, false] x = true}) + rw [Nat.card_eq_fintype_card] + decide + +example : ¬ Definable evenMarked := + ModelChecking.Ordered.not_definable_even_card (L := inputLanguage) Relation.mark + +end ComplexityTests.OrderedFirstOrderCircuits