From cd512dbad3aedc68d0b13e692e822c16d1567609 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 17:14:20 +0000 Subject: [PATCH 1/3] feat(logic): add extensible FO(LFP), tuple closure, and certified synthesis Add scoped operator syntax, variance-aware positive recursion, least-fixed-point semantics and finite-stage bounds, tuple transitive closure, and uniform formula synthesis. Include behavior and rejection tests and a guide chapter. AI-assisted implementation by OpenAI Codex at the repository owner's request. --- Complexity.lean | 12 + .../Foundations/Order/FiniteFixedPoint.lean | 90 ++++++ .../Logics/FirstOrder/Operator/Basic.lean | 251 ++++++++++++++++ .../FirstOrder/Operator/Definability.lean | 211 ++++++++++++++ .../Operator/Definability/Polarity.lean | 207 ++++++++++++++ .../FirstOrder/Operator/LeastFixedPoint.lean | 213 ++++++++++++++ .../LeastFixedPoint/Definability.lean | 90 ++++++ .../Logics/FirstOrder/Operator/Polarity.lean | 269 ++++++++++++++++++ .../Logics/FirstOrder/Operator/Relabel.lean | 158 ++++++++++ .../Operator/TransitiveClosure.lean | 158 ++++++++++ .../TransitiveClosure/Definability.lean | 81 ++++++ Complexity/Tactic/FOOperator.lean | 64 +++++ Complexity/Tactic/FOOperator/Init.lean | 22 ++ ComplexityTests/FOOperators.lean | 265 +++++++++++++++++ README.md | 1 + ROADMAP.md | 5 +- guide/ComplexityGuide.lean | 9 +- .../ComplexityGuide/FirstOrderOperators.lean | 177 ++++++++++++ references.bib | 22 ++ 19 files changed, 2301 insertions(+), 4 deletions(-) create mode 100644 Complexity/Foundations/Order/FiniteFixedPoint.lean create mode 100644 Complexity/Logics/FirstOrder/Operator/Basic.lean create mode 100644 Complexity/Logics/FirstOrder/Operator/Definability.lean create mode 100644 Complexity/Logics/FirstOrder/Operator/Definability/Polarity.lean create mode 100644 Complexity/Logics/FirstOrder/Operator/LeastFixedPoint.lean create mode 100644 Complexity/Logics/FirstOrder/Operator/LeastFixedPoint/Definability.lean create mode 100644 Complexity/Logics/FirstOrder/Operator/Polarity.lean create mode 100644 Complexity/Logics/FirstOrder/Operator/Relabel.lean create mode 100644 Complexity/Logics/FirstOrder/Operator/TransitiveClosure.lean create mode 100644 Complexity/Logics/FirstOrder/Operator/TransitiveClosure/Definability.lean create mode 100644 Complexity/Tactic/FOOperator.lean create mode 100644 Complexity/Tactic/FOOperator/Init.lean create mode 100644 ComplexityTests/FOOperators.lean create mode 100644 guide/ComplexityGuide/FirstOrderOperators.lean diff --git a/Complexity.lean b/Complexity.lean index 301474fcb..46633598f 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2726,6 +2726,7 @@ public import Complexity.Foundations.NumberTheory.PrimeWindow public import Complexity.Foundations.NumberTheory.SqrtPrimeWindow public import Complexity.Foundations.Order.BooleanSubalgebra public import Complexity.Foundations.Order.Changes +public import Complexity.Foundations.Order.FiniteFixedPoint public import Complexity.Foundations.Order.UpperLower public import Complexity.Foundations.Probability.AtomCutoffs public import Complexity.Foundations.Probability.ColumnDetector @@ -2798,6 +2799,15 @@ public import Complexity.Logics.FirstOrder.Interpretation.Rank public import Complexity.Logics.FirstOrder.Interpretation.Tagged 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.Polarity +public import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint +public import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint.Definability +public import Complexity.Logics.FirstOrder.Operator.Polarity +public import Complexity.Logics.FirstOrder.Operator.Relabel +public import Complexity.Logics.FirstOrder.Operator.TransitiveClosure +public import Complexity.Logics.FirstOrder.Operator.TransitiveClosure.Definability public import Complexity.Logics.FirstOrder.Ordered.Addition public import Complexity.Logics.FirstOrder.Ordered.Basic public import Complexity.Logics.FirstOrder.Ordered.BitArithmetic @@ -3029,6 +3039,8 @@ public import Complexity.Probability.StatisticalDistance.UniformMod public import Complexity.Probability.Uniform public import Complexity.Probability.UniformNat public import Complexity.Probability.UniversalHash +public import Complexity.Tactic.FOOperator +public import Complexity.Tactic.FOOperator.Init public import Complexity.Tactic.FirstOrder public import Complexity.Tactic.FirstOrder.Init public import Complexity.Tactic.PPT diff --git a/Complexity/Foundations/Order/FiniteFixedPoint.lean b/Complexity/Foundations/Order/FiniteFixedPoint.lean new file mode 100644 index 000000000..592c3193e --- /dev/null +++ b/Complexity/Foundations/Order/FiniteFixedPoint.lean @@ -0,0 +1,90 @@ +/- +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 (Mathlib, finite iteration bounds for `Mathlib/Order/FixedPoints.lean`) + +public import Complexity.Init +public import Mathlib.Order.FixedPoints +public import Mathlib.Data.Fintype.Card +import Mathlib.Data.Set.Card +import Mathlib.Order.Iterate + +/-! +# Least fixed points on finite powersets + +A monotone map on subsets of a finite type reaches its least fixed point by iterating from the +empty set at most the cardinality of the underlying type times. This is the number of elements, +not the cardinality of the powerset. No inflationarity assumption is needed: the iteration from +the empty set is increasing by monotonicity. + +## Main results + +* `OrderHom.iterate_bot_le_lfp`: every iterate from the bottom lies below the least fixed point. +* `OrderHom.iterate_card_bot_eq_lfp`: on `Set α`, the iterate at `Fintype.card α` is the least + fixed point, including when `α` is empty. +* `OrderHom.iterate_bot_eq_lfp_of_card_le`: every subsequent iterate has the same value. +-/ + +public section + +namespace OrderHom + +variable {α β : Type*} + +/-- Every finite iterate from the bottom lies below the least fixed point. -/ +theorem iterate_bot_le_lfp [CompleteLattice β] (f : β →o β) (n : ℕ) : + (f^[n]) ⊥ ≤ f.lfp := by + induction n with + | zero => exact bot_le + | succ n ih => + rw [Function.iterate_succ_apply'] + exact (f.monotone ih).trans_eq f.map_lfp + +/-- A monotone map on a finite powerset reaches its least fixed point from the empty set after +at most the cardinality of the underlying type many iterations. -/ +theorem iterate_card_bot_eq_lfp [Fintype α] (f : Set α →o Set α) : + (f^[Fintype.card α]) ⊥ = f.lfp := by + have hmono : Monotone fun n => (f^[n]) ⊥ := + f.monotone.monotone_iterate_of_le_map bot_le + have hgrowth : ∀ n, (f^[n]) ⊥ = f.lfp ∨ n ≤ ((f^[n]) ⊥).ncard := by + intro n + induction n with + | zero => exact Or.inr (Nat.zero_le _) + | succ n ih => + rcases ih with hfixed | hcard + · left + rw [Function.iterate_succ_apply', hfixed, f.map_lfp] + · by_cases heq : (f^[n]) ⊥ = (f^[n + 1]) ⊥ + · left + have hfixed : f ((f^[n]) ⊥) = (f^[n]) ⊥ := by + exact (Function.iterate_succ_apply' f n ⊥).symm.trans heq.symm + rw [← heq] + exact le_antisymm (f.iterate_bot_le_lfp n) (f.lfp_le_fixed hfixed) + · right + have hlt : ((f^[n]) ⊥).ncard < ((f^[n + 1]) ⊥).ncard := + Set.ncard_lt_ncard (lt_of_le_of_ne (hmono (Nat.le_succ n)) heq) + omega + rcases hgrowth (Fintype.card α) with hfixed | hcard + · exact hfixed + · have huniv : (f^[Fintype.card α]) ⊥ = Set.univ := by + apply (Set.eq_univ_iff_ncard _).2 + rw [Nat.card_eq_fintype_card] + apply le_antisymm ?_ hcard + simpa only [Nat.card_eq_fintype_card] using + (Set.ncard_le_card ((f^[Fintype.card α]) ⊥)) + apply le_antisymm (f.iterate_bot_le_lfp _) + rw [huniv] + exact Set.subset_univ _ + +/-- Every iteration at or beyond the finite powerset bound equals the least fixed point. -/ +theorem iterate_bot_eq_lfp_of_card_le [Fintype α] (f : Set α →o Set α) {n : ℕ} + (hn : Fintype.card α ≤ n) : (f^[n]) ⊥ = f.lfp := by + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hn + rw [Nat.add_comm, Function.iterate_add_apply, f.iterate_card_bot_eq_lfp] + exact Function.iterate_fixed f.map_lfp k + +end OrderHom diff --git a/Complexity/Logics/FirstOrder/Operator/Basic.lean b/Complexity/Logics/FirstOrder/Operator/Basic.lean new file mode 100644 index 000000000..38cf0bbae --- /dev/null +++ b/Complexity/Logics/FirstOrder/Operator/Basic.lean @@ -0,0 +1,251 @@ +/- +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.Basic + +/-! +# First-order logic with scoped operators + +An operator has finitely many formula bodies, each with its own first-order and relation +binders, and a tuple of term arguments. This separates binding from the meaning of an operator: +least fixed points, tuple transitive closure, and language quantifiers share the same syntax. +Ordinary terms, formulas, and structures are Mathlib's first-order objects. + +`Formula` is raw syntax. An interpretation gives it a total meaning; an operator's formation +conditions (such as positive recursion) are a separate layer. In particular, this interface does +not assume that every operator is monotone or that every structure is finite or ordered. + +## Main definitions + +* `RelVar`, `RelEnv`: scoped, arity-indexed relation variables and their valuations. +* `Binder`, `Shape`: the binding and application interface of an operator. +* `Formula`, `Formula.Realize`: common syntax and interpretation. +* `Formula.relabel`, `Formula.realize_relabel`: capture-avoiding renaming of free variables. + +## References + +* [N. Immerman, *Descriptive Complexity*][Immerman1999] +* [Z. Ésik and K. G. Larsen, *Regular Languages Definable by Lindström Quantifiers*][EsikLarsen2003], + Section 2, for multiple scoped bodies in regular-language quantifiers. +-/ + +public section + +universe u v w z s + +open FirstOrder Language + +namespace Cslib.Logic.FO.Operator + +/-- A relation variable whose arity is recorded in its context. The head is the nearest binder. -/ +inductive RelVar : List ℕ → ℕ → Type + | here {Γ : List ℕ} {k : ℕ} : RelVar (k :: Γ) k + | there {Γ : List ℕ} {k l : ℕ} : RelVar Γ k → RelVar (l :: Γ) k + +namespace RelVar + +/-- Distinguish a locally bound relation variable from a variable in the outer context. -/ +@[expose] def split {Γ : List ℕ} {k : ℕ} (Δ : List ℕ) : + RelVar (Δ ++ Γ) k → RelVar Δ k ⊕ RelVar Γ k := + match Δ with + | [] => fun r => .inr r + | _ :: Δ => fun r => match r with + | .here => .inl .here + | .there r => match split Δ r with + | .inl r => .inl (.there r) + | .inr r => .inr r + +/-- Lift an outer relation variable through a list of new binders. -/ +@[expose] def lift {Γ : List ℕ} {k : ℕ} (Δ : List ℕ) (r : RelVar Γ k) : + RelVar (Δ ++ Γ) k := + match Δ with + | [] => r + | _ :: Δ => .there (lift Δ r) + +/-- Splitting a lifted variable recovers the outer variable. -/ +@[simp] theorem split_lift {Γ : List ℕ} {k : ℕ} (Δ : List ℕ) (r : RelVar Γ k) : + split Δ (lift Δ r) = .inr r := by + induction Δ with + | nil => rfl + | cons _ _ ih => simp [split, lift, ih] + +end RelVar + +/-- An interpretation of all relation variables in a context. -/ +abbrev RelEnv (Γ : List ℕ) (M : Type z) := ∀ {k}, RelVar Γ k → Set (Fin k → M) + +namespace RelEnv + +/-- The unique valuation of an empty relation context. -/ +@[expose] def empty {M : Type z} : RelEnv [] M := fun r => nomatch r + +/-- Extend a relation valuation by local relations, without changing the outer relations. -/ +@[expose] def append {Γ Δ : List ℕ} {M : Type z} (δ : RelEnv Δ M) + (outer : RelEnv Γ M) : RelEnv (Δ ++ Γ) M := + fun r => Sum.elim (fun r => δ r) (fun r => outer r) (r.split Δ) + +/-- Add one relation as the nearest binder. -/ +@[expose] def cons {Γ : List ℕ} {M : Type z} {k : ℕ} (R : Set (Fin k → M)) + (outer : RelEnv Γ M) : RelEnv (k :: Γ) M + | _, .here => R + | _, .there r => outer r + +/-- Extending by an empty context leaves a valuation unchanged. -/ +@[simp] theorem append_empty {Γ : List ℕ} {M : Type z} (outer : RelEnv Γ M) : + @append Γ [] M (@empty M) outer = @outer := rfl + +/-- Outer relation variables retain their meanings under a binder. -/ +@[simp] theorem append_lift {Γ Δ : List ℕ} {M : Type z} (δ : RelEnv Δ M) + (outer : RelEnv Γ M) {k : ℕ} (r : RelVar Γ k) : + append δ outer (r.lift Δ) = outer r := by + simp [append] + +end RelEnv + +/-- The local variables available in one body of a logical operator. -/ +structure Binder where + /-- Arities of locally bound relation variables, nearest first. -/ + relations : List ℕ + /-- Number of locally bound first-order variables. -/ + vars : ℕ + +/-- The finite binding interface of a logical operator. -/ +structure Shape where + /-- Number of terms at which the operator's resulting relation is applied. -/ + arity : ℕ + /-- Number of formula bodies. -/ + slots : ℕ + /-- Local binding context of each body. -/ + binder : Fin slots → Binder + +/-- The meaning of a body as a function of its locally bound relations and variables. -/ +abbrev BodyValue (b : Binder) (M : Type z) := + RelEnv b.relations M → (Fin b.vars → M) → Prop + +/-- An operator interpretation. It may use additional structure on `M` supplied by its caller. -/ +abbrev Interpretation {O : Type s} (shape : O → Shape) (M : Type z) := + (o : O) → ((i : Fin (shape o).slots) → BodyValue ((shape o).binder i) M) → + (Fin (shape o).arity → M) → Prop + +/-- First-order syntax extended by an arbitrary family of scoped logical operators. -/ +inductive Formula (L : Language.{u, v}) {O : Type s} (shape : O → Shape) : + List ℕ → Type w → Type (max u v (w + 1) s) + | ofFO {Γ α} : L.Formula α → Formula L shape Γ α + | rel {Γ α k} : RelVar Γ k → (Fin k → L.Term α) → Formula L shape Γ α + | neg {Γ α} : Formula L shape Γ α → Formula L shape Γ α + | conj {Γ α} : Formula L shape Γ α → Formula L shape Γ α → Formula L shape Γ α + | ex {Γ α} : Formula L shape Γ (Option α) → Formula L shape Γ α + | op {Γ α} (o : O) + (body : (i : Fin (shape o).slots) → + Formula L shape (((shape o).binder i).relations ++ Γ) + (α ⊕ Fin ((shape o).binder i).vars)) + (args : Fin (shape o).arity → L.Term α) : Formula L shape Γ α + +namespace Formula + +variable {L : Language.{u, v}} {O : Type s} {shape : O → Shape} + {Γ : List ℕ} {α β : Type w} {M : Type z} [L.Structure M] + +/-- Interpret a formula, capturing the ambient free-variable assignment in every operator body. -/ +@[expose] def Realize (I : Interpretation shape M) : + {Γ : List ℕ} → {α : Type w} → Formula L shape Γ α → RelEnv Γ M → (α → M) → Prop + | _, _, .ofFO φ, _, v => φ.Realize v + | _, _, .rel r args, ρ, v => (fun i => (args i).realize v) ∈ ρ r + | _, _, .neg φ, ρ, v => ¬ φ.Realize I ρ v + | _, _, .conj φ ψ, ρ, v => φ.Realize I ρ v ∧ ψ.Realize I ρ v + | _, _, .ex φ, ρ, v => ∃ x, φ.Realize I ρ (Option.elim · x v) + | _, _, .op o body args, ρ, v => + I o (fun i δ xs => (body i).Realize I (δ.append ρ) (Sum.elim v xs)) + (fun i => (args i).realize v) + +/-- Capture-avoiding relabeling of free first-order variables. -/ +@[expose] def relabel : {Γ : List ℕ} → {α β : Type w} → + (α → β) → Formula L shape Γ α → Formula L shape Γ β + | _, _, _, f, .ofFO φ => .ofFO (φ.relabel f) + | _, _, _, f, .rel r args => .rel r (fun i => (args i).relabel f) + | _, _, _, f, .neg φ => .neg (φ.relabel f) + | _, _, _, f, .conj φ ψ => .conj (φ.relabel f) (ψ.relabel f) + | _, _, _, f, .ex φ => .ex (φ.relabel (Option.map f)) + | _, _, _, f, .op o body args => + .op o (fun i => (body i).relabel (Sum.map f id)) (fun i => (args i).relabel f) + +/-- Embedded first-order formulas keep their original semantics. -/ +@[simp, fo_realize] theorem realize_ofFO (I : Interpretation shape M) (φ : L.Formula α) + (ρ : RelEnv Γ M) (v : α → M) : (ofFO φ).Realize I ρ v ↔ φ.Realize v := Iff.rfl + +/-- Relation variables are applied to the interpreted term arguments. -/ +@[simp, fo_realize] theorem realize_rel (I : Interpretation shape M) {k : ℕ} + (r : RelVar Γ k) (args : Fin k → L.Term α) (ρ : RelEnv Γ M) (v : α → M) : + (rel r args).Realize I ρ v ↔ (fun i => (args i).realize v) ∈ ρ r := Iff.rfl + +/-- Semantic negation. -/ +@[simp, fo_realize] theorem realize_neg (I : Interpretation shape M) (φ : Formula L shape Γ α) + (ρ : RelEnv Γ M) (v : α → M) : (neg φ).Realize I ρ v ↔ ¬ φ.Realize I ρ v := Iff.rfl + +/-- Semantic conjunction. -/ +@[simp, fo_realize] theorem realize_conj (I : Interpretation shape M) + (φ ψ : Formula L shape Γ α) (ρ : RelEnv Γ M) (v : α → M) : + (conj φ ψ).Realize I ρ v ↔ φ.Realize I ρ v ∧ ψ.Realize I ρ v := Iff.rfl + +/-- Existential binding changes only the new variable. -/ +@[simp, fo_realize] theorem realize_ex (I : Interpretation shape M) + (φ : Formula L shape Γ (Option α)) (ρ : RelEnv Γ M) (v : α → M) : + (ex φ).Realize I ρ v ↔ ∃ x, φ.Realize I ρ (Option.elim · x v) := Iff.rfl + +/-- Relabeling is interpreted by precomposing the free-variable assignment. -/ +@[simp, fo_realize] theorem realize_relabel (I : Interpretation shape M) + (φ : Formula L shape Γ α) (f : α → β) (ρ : RelEnv Γ M) (v : β → M) : + (φ.relabel f).Realize I ρ v ↔ φ.Realize I ρ (v ∘ f) := by + induction φ generalizing β with + | ofFO φ => simp [relabel] + | rel r args => simp [relabel, Realize, Term.realize_relabel] + | neg φ ih => exact not_congr (ih f ρ v) + | conj φ ψ ihφ ihψ => exact and_congr (ihφ f ρ v) (ihψ f ρ v) + | ex φ ih => + simp only [relabel, realize_ex, ih] + apply exists_congr + intro x + apply iff_of_eq + congr 1 + funext y + cases y <;> rfl + | op o body args ih => + simp only [relabel, Realize, Term.realize_relabel] + simp_rw [ih] + apply iff_of_eq + congr 1 + funext i δ xs + congr 1 + funext y + cases y <;> rfl + +/-- Disjunction as a derived connective. -/ +@[expose] def disj (φ ψ : Formula L shape Γ α) : Formula L shape Γ α := + .neg (.conj (.neg φ) (.neg ψ)) + +/-- Universal quantification as a derived connective. -/ +@[expose] def all (φ : Formula L shape Γ (Option α)) : Formula L shape Γ α := + .neg (.ex (.neg φ)) + +/-- Derived disjunction has the usual classical semantics. -/ +@[simp, fo_realize] theorem realize_disj (I : Interpretation shape M) + (φ ψ : Formula L shape Γ α) (ρ : RelEnv Γ M) (v : α → M) : + (disj φ ψ).Realize I ρ v ↔ φ.Realize I ρ v ∨ ψ.Realize I ρ v := by + simp only [disj, realize_neg, realize_conj] + tauto + +/-- Derived universal quantification has the usual classical semantics. -/ +@[simp, fo_realize] theorem realize_all (I : Interpretation shape M) + (φ : Formula L shape Γ (Option α)) (ρ : RelEnv Γ M) (v : α → M) : + (all φ).Realize I ρ v ↔ ∀ x, φ.Realize I ρ (Option.elim · x v) := by + simp [all] + +end Formula + +end Cslib.Logic.FO.Operator diff --git a/Complexity/Logics/FirstOrder/Operator/Definability.lean b/Complexity/Logics/FirstOrder/Operator/Definability.lean new file mode 100644 index 000000000..aa204fb53 --- /dev/null +++ b/Complexity/Logics/FirstOrder/Operator/Definability.lean @@ -0,0 +1,211 @@ +/- +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.Polarity + +/-! +# Uniform definability by first-order formulas with operators + +`Definable` certifies that one well-formed formula defines a Lean predicate across a family of +structures. The formula is independent of the family index, structure size, and assignment. +This is the semantic interface for formula synthesis: compositional rules construct syntax and +prove its formation conditions and meaning together. + +The family supplies the interpretations of the operators and free relation variables. Particular +logics can therefore register rules about their own semantic operations without extending this +interface. A registered rule must produce a well-formed witness, rather than raw syntax alone. + +## Main definitions + +* `Definable`: uniform definability across an indexed family of structures. +* `Definable.of_formula`: use a checked formula as a definability certificate. + +## Main results + +* `Definable.neg`, `Definable.conj`, `Definable.disj`, `Definable.ex`, `Definable.all`: + compositional construction of well-formed formulas. +* `Definable.ofFO`, `Definable.equal`, `Definable.rel`: atomic certificates. + +## References + +* [N. Immerman, *Descriptive Complexity*][Immerman1999] +-/ + +public section + +universe u v w z s t + +open FirstOrder Language + +namespace Cslib.Logic.FO.Operator + +/-- A single well-formed formula defines the predicate in every member of a family of structures. +The existential witness is outside the quantification over structures and assignments. -/ +@[expose] def Definable {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)) + {α : Type w} (P : ∀ i, (α → M i) → Prop) : Prop := + ∃ φ : Formula L shape Γ α, φ.wellFormed policy = true ∧ + ∀ i v, φ.Realize (I i) (ρ i) v ↔ P i v + +namespace Definable + +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)} + {α β : Type w} {P Q : ∀ i, (α → M i) → Prop} + +/-- Register an explicit well-formed formula through its semantics. -/ +theorem of_formula (φ : Formula L shape Γ α) (hφ : φ.wellFormed policy = true) : + Definable (L := L) policy M I ρ (fun i v => φ.Realize (I i) (ρ i) v) := + ⟨φ, hφ, fun _ _ => Iff.rfl⟩ + +/-- Replace a predicate by an equivalent one without changing its formula. -/ +theorem congr (hP : Definable (L := L) policy M I ρ P) (h : ∀ i v, P i v ↔ Q i v) : + Definable (L := L) policy M I ρ Q := by + obtain ⟨φ, hφ, hP⟩ := hP + exact ⟨φ, hφ, fun i v => (hP i v).trans (h i v)⟩ + +/-- Relabeling free variables composes the predicate with the assignment map. -/ +theorem relabel (hP : Definable (L := L) policy M I ρ P) (f : α → β) : + Definable (L := L) policy M I ρ (fun i v => P i (v ∘ f)) := by + obtain ⟨φ, hφ, hP⟩ := hP + refine ⟨φ.relabel f, by simpa only [Formula.wellFormed_relabel] using hφ, ?_⟩ + intro i v + exact (Formula.realize_relabel _ _ _ _ _).trans (hP i (v ∘ f)) + +/-- A native first-order formula has the same meaning in the extended logic. -/ +theorem ofFO (φ : L.Formula α) : + Definable (L := L) policy M I ρ (fun i v => φ.Realize (M := M i) v) := + ⟨.ofFO φ, rfl, fun _ _ => Iff.rfl⟩ + +/-- Negation preserves uniform definability. -/ +theorem neg (hP : Definable (L := L) policy M I ρ P) : + Definable (L := L) policy M I ρ (fun i v => ¬ P i v) := by + obtain ⟨φ, hφ, hP⟩ := hP + exact ⟨.neg φ, hφ, fun i v => not_congr (hP i v)⟩ + +/-- Conjunction combines the two defining formulas. -/ +theorem conj (hP : Definable (L := L) policy M I ρ P) (hQ : Definable (L := L) policy M I ρ Q) : + Definable (L := L) policy M I ρ (fun i v => P i v ∧ Q i v) := by + obtain ⟨φ, hφ, hP⟩ := hP + obtain ⟨ψ, hψ, hQ⟩ := hQ + exact ⟨.conj φ ψ, by simp [Formula.wellFormed, hφ, hψ], + fun i v => and_congr (hP i v) (hQ i v)⟩ + +/-- Disjunction combines the two defining formulas. -/ +theorem disj (hP : Definable (L := L) policy M I ρ P) (hQ : Definable (L := L) policy M I ρ Q) : + Definable (L := L) policy M I ρ (fun i v => P i v ∨ Q i v) := by + obtain ⟨φ, hφ, hP⟩ := hP + obtain ⟨ψ, hψ, hQ⟩ := hQ + refine ⟨φ.disj ψ, by simp [Formula.disj, Formula.wellFormed, hφ, hψ], ?_⟩ + intro i v + exact (Formula.realize_disj _ _ _ _ _).trans (or_congr (hP i v) (hQ i v)) + +/-- Implication is a derived first-order connective. -/ +theorem imp (hP : Definable (L := L) policy M I ρ P) (hQ : Definable (L := L) policy M I ρ Q) : + Definable (L := L) policy M I ρ (fun i v => P i v → Q i v) := + (hP.neg.disj hQ).congr fun _ _ => by simp only [or_iff_not_imp_left, not_not] + +/-- Existential quantification is synthesized by adding one scoped first-order variable. -/ +theorem ex {P : ∀ i, M i → (α → M i) → Prop} + (hP : Definable (L := L) policy M I ρ + (fun i v => P i (v none) (fun a => v (some a)))) : + Definable (L := L) policy M I ρ (fun i v => ∃ x, P i x v) := by + obtain ⟨φ, hφ, hP⟩ := hP + refine ⟨.ex φ, hφ, ?_⟩ + intro i v + exact exists_congr fun x => hP i (Option.elim · x v) + +/-- Universal quantification is synthesized from a defining formula with one extra variable. -/ +theorem all {P : ∀ i, M i → (α → M i) → Prop} + (hP : Definable (L := L) policy M I ρ + (fun i v => P i (v none) (fun a => v (some a)))) : + Definable (L := L) policy M I ρ (fun i v => ∀ x, P i x v) := by + obtain ⟨φ, hφ, hP⟩ := hP + refine ⟨φ.all, hφ, ?_⟩ + intro i v + exact (Formula.realize_all _ _ _ _).trans (forall_congr' fun x => + hP i (Option.elim · x v)) + +/-- The constant true predicate is uniformly definable, including on empty structures. -/ +theorem truth : Definable (L := L) policy M I ρ (fun _ (_ : α → _) => True) := + (ofFO (⊤ : L.Formula α)).congr fun _ _ => FirstOrder.Language.Formula.realize_top + +/-- The constant false predicate is uniformly definable. -/ +theorem falsity : Definable (L := L) policy M I ρ (fun _ (_ : α → _) => False) := + (ofFO (⊥ : L.Formula α)).congr fun _ _ => FirstOrder.Language.Formula.realize_bot + +/-- Equality of two native first-order terms is uniformly definable. -/ +theorem equal (a b : L.Term α) : + Definable (L := L) policy M I ρ (fun i v => a.realize (M := M i) v = b.realize v) := by + apply (ofFO (a.equal b)).congr + intro i v + simp + +/-- Equality of two free variables is an atomic synthesis rule. -/ +theorem var_eq (a b : α) : Definable (L := L) policy M I ρ (fun _ v => v a = v b) := + equal (.var a) (.var b) + +/-- A base-language relation applied to native terms is uniformly definable. -/ +theorem relation {k : ℕ} (r : L.Relations k) (args : Fin k → L.Term α) : + Definable (L := L) policy M I ρ + (fun i v => Structure.RelMap (M := M i) r (fun j => (args j).realize v)) := by + apply (ofFO (r.formula args)).congr + intro i v + simp + +/-- A base-language relation applied to free variables is an atomic synthesis rule. -/ +theorem relation_vars {k : ℕ} (r : L.Relations k) (args : Fin k → α) : + Definable (L := L) policy M I ρ (fun i v => Structure.RelMap (M := M i) r (v ∘ args)) := + relation r (fun j => .var (args j)) + +/-- Unary relation application in the usual vector notation is an atomic synthesis rule. -/ +theorem relation₁ (r : L.Relations 1) (a : α) : + Definable (L := L) policy M I ρ (fun i v => Structure.RelMap (M := M i) r ![v a]) := + ⟨.ofFO (FO.rel₁ r a), rfl, fun _ v => FO.realize_rel₁ v r a⟩ + +/-- Binary relation application in the usual vector notation is an atomic synthesis rule. -/ +theorem relation₂ (r : L.Relations 2) (a b : α) : + Definable (L := L) policy M I ρ (fun i v => Structure.RelMap (M := M i) r ![v a, v b]) := + ⟨.ofFO (FO.rel₂ r a b), rfl, fun _ v => FO.realize_rel₂ v r a b⟩ + +/-- Free relation variables are also available to formula synthesis. -/ +theorem rel {k : ℕ} (r : RelVar Γ k) (args : Fin k → L.Term α) : + Definable (L := L) policy M I ρ (fun i v => (fun j => (args j).realize v) ∈ ρ i r) := + ⟨.rel r args, rfl, fun _ _ => Iff.rfl⟩ + +/-- A free relation variable applied to a tuple of free variables is uniformly definable. -/ +theorem rel_vars {k : ℕ} (r : RelVar Γ k) (args : Fin k → α) : + Definable (L := L) policy M I ρ (fun i v => (v ∘ args) ∈ ρ i r) := + rel r (fun j => .var (args j)) + +/-- Unary free-relation application in vector notation is an atomic synthesis rule. -/ +theorem rel₁ (r : RelVar Γ 1) (a : α) : + Definable (L := L) policy M I ρ (fun i v => ![v a] ∈ ρ i r) := by + apply (rel_vars r ![a]).congr + intro i v + have h : v ∘ ![a] = ![v a] := by + funext j + exact Fin.cases rfl (fun k => k.elim0) j + rw [h] + +/-- Binary free-relation application in vector notation is an atomic synthesis rule. -/ +theorem rel₂ (r : RelVar Γ 2) (a b : α) : + Definable (L := L) policy M I ρ (fun i v => ![v a, v b] ∈ ρ i r) := by + apply (rel_vars r ![a, b]).congr + intro i v + have h : v ∘ ![a, b] = ![v a, v b] := by + funext j + exact Fin.cases rfl (fun k => Fin.cases rfl (fun l => l.elim0) k) j + rw [h] + +end Definable + +end Cslib.Logic.FO.Operator diff --git a/Complexity/Logics/FirstOrder/Operator/Definability/Polarity.lean b/Complexity/Logics/FirstOrder/Operator/Definability/Polarity.lean new file mode 100644 index 000000000..e34cf8623 --- /dev/null +++ b/Complexity/Logics/FirstOrder/Operator/Definability/Polarity.lean @@ -0,0 +1,207 @@ +/- +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 +public import Complexity.Tactic.FOOperator.Init + +/-! +# Formula synthesis with certified polarity + +`PolarityDefinable` strengthens uniform definability by requiring a syntactic polarity +certificate for the same defining formula. This lets a fixed-point synthesis rule construct +its body from a Lean predicate while checking that recursive relation occurrences are positive. +Monotonicity is never assumed in place of this syntactic check. + +The compositional rules are registered in `FODefinable`, so `fo_definable` handles these goals +as well as ordinary `Definable` goals. Negation reverses the requested polarity; marked relation +atoms are available only positively. Unmarked relation atoms are available with either sign. + +## Main definitions + +* `PolarityDefinable`: one well-formed, polarity-checked formula for a family of predicates. + +## Main results + +* `PolarityDefinable.toDefinable`: forget the additional polarity certificate. +* `PolarityDefinable.neg`, `PolarityDefinable.conj`, `PolarityDefinable.disj`, + `PolarityDefinable.ex`, `PolarityDefinable.all`: compositional synthesis rules. +* `PolarityDefinable.head_vars`: a positive recursive atom in the nearest relation binder. +-/ + +public section + +universe u v w z s t + +open FirstOrder Language + +namespace Cslib.Logic.FO.Operator + +/-- Uniform definability with a syntactic polarity check on the defining formula itself. -/ +@[expose] def PolarityDefinable {L : Language.{u, v}} {O : Type s} {shape : O → Shape} + (policy : Policy shape) {Γ : List ℕ} (mark : Marking Γ) (sign : Bool) + {ι : Type t} (M : ι → Type z) [∀ i, L.Structure (M i)] + (I : ∀ i, Interpretation shape (M i)) (ρ : ∀ i, RelEnv Γ (M i)) + {α : Type w} (P : ∀ i, (α → M i) → Prop) : Prop := + ∃ φ : Formula L shape Γ α, φ.wellFormed policy = true ∧ + φ.checkPolarity policy.variance sign mark = true ∧ + ∀ i v, φ.Realize (I i) (ρ i) v ↔ P i v + +namespace 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} {P Q : ∀ i, (α → M i) → Prop} + +/-- Forget the polarity requirement while retaining the well-formed defining formula. -/ +theorem toDefinable (h : PolarityDefinable (L := L) policy mark sign M I ρ P) : + Definable (L := L) policy M I ρ P := by + obtain ⟨φ, hφ, _, hP⟩ := h + exact ⟨φ, hφ, hP⟩ + +/-- Equivalent semantic presentations use the same syntax and polarity certificate. -/ +theorem congr (hP : PolarityDefinable (L := L) policy mark sign M I ρ P) + (h : ∀ i v, P i v ↔ Q i v) : PolarityDefinable (L := L) policy mark sign M I ρ Q := by + obtain ⟨φ, hφ, hp, hP⟩ := hP + exact ⟨φ, hφ, hp, fun i v => (hP i v).trans (h i v)⟩ + +/-- Native first-order formulas are independent of all scoped relation variables. -/ +theorem ofFO (φ : L.Formula α) : + PolarityDefinable (L := L) policy mark sign M I ρ + (fun i v => φ.Realize (M := M i) v) := + ⟨.ofFO φ, rfl, rfl, fun _ _ => Iff.rfl⟩ + +/-- Negation reverses the required polarity of its body. -/ +theorem neg (hP : PolarityDefinable (L := L) policy mark (!sign) M I ρ P) : + PolarityDefinable (L := L) policy mark sign M I ρ (fun i v => ¬ P i v) := by + obtain ⟨φ, hφ, hp, hP⟩ := hP + exact ⟨.neg φ, hφ, hp, fun i v => not_congr (hP i v)⟩ + +/-- Conjunction preserves the polarity of both bodies. -/ +theorem conj (hP : PolarityDefinable (L := L) policy mark sign M I ρ P) + (hQ : PolarityDefinable (L := L) policy mark sign M I ρ Q) : + PolarityDefinable (L := L) policy mark sign M I ρ (fun i v => P i v ∧ Q i v) := by + obtain ⟨φ, hφ, hp, hP⟩ := hP + obtain ⟨ψ, hψ, hq, hQ⟩ := hQ + exact ⟨.conj φ ψ, by simp [Formula.wellFormed, hφ, hψ], + by simp [Formula.checkPolarity, hp, hq], fun i v => and_congr (hP i v) (hQ i v)⟩ + +/-- Derived disjunction preserves the polarity of both bodies. -/ +theorem disj (hP : PolarityDefinable (L := L) policy mark sign M I ρ P) + (hQ : PolarityDefinable (L := L) policy mark sign M I ρ Q) : + PolarityDefinable (L := L) policy mark sign M I ρ (fun i v => P i v ∨ Q i v) := by + obtain ⟨φ, hφ, hp, hP⟩ := hP + obtain ⟨ψ, hψ, hq, hQ⟩ := hQ + refine ⟨φ.disj ψ, by simp [Formula.disj, Formula.wellFormed, hφ, hψ], + by simp [Formula.disj, Formula.checkPolarity, hp, hq], ?_⟩ + exact fun i v => (Formula.realize_disj _ _ _ _ _).trans (or_congr (hP i v) (hQ i v)) + +/-- Implication reverses polarity in its antecedent and preserves it in its consequent. -/ +theorem imp (hP : PolarityDefinable (L := L) policy mark (!sign) M I ρ P) + (hQ : PolarityDefinable (L := L) policy mark sign M I ρ Q) : + PolarityDefinable (L := L) policy mark sign M I ρ (fun i v => P i v → Q i v) := + (hP.neg.disj hQ).congr fun _ _ => by simp only [or_iff_not_imp_left, not_not] + +/-- Existential quantification preserves polarity while binding a fresh first-order variable. -/ +theorem ex {P : ∀ i, M i → (α → M i) → Prop} + (hP : PolarityDefinable (L := L) policy mark sign M I ρ + (fun i v => P i (v none) (fun a => v (some a)))) : + PolarityDefinable (L := L) policy mark sign M I ρ (fun i v => ∃ x, P i x v) := by + obtain ⟨φ, hφ, hp, hP⟩ := hP + exact ⟨.ex φ, hφ, hp, fun i v => exists_congr fun x => hP i (Option.elim · x v)⟩ + +/-- Universal quantification preserves polarity while binding a fresh first-order variable. -/ +theorem all {P : ∀ i, M i → (α → M i) → Prop} + (hP : PolarityDefinable (L := L) policy mark sign M I ρ + (fun i v => P i (v none) (fun a => v (some a)))) : + PolarityDefinable (L := L) policy mark sign M I ρ (fun i v => ∀ x, P i x v) := by + obtain ⟨φ, hφ, hp, hP⟩ := hP + refine ⟨φ.all, hφ, by simpa only [Formula.all, Formula.checkPolarity, Bool.not_not] + using hp, ?_⟩ + exact fun i v => (Formula.realize_all _ _ _ _).trans + (forall_congr' fun x => hP i (Option.elim · x v)) + +/-- The constant true predicate has either polarity. -/ +theorem truth : + PolarityDefinable (L := L) policy mark sign M I ρ (fun _ (_ : α → _) => True) := + (ofFO (⊤ : L.Formula α)).congr fun _ _ => FirstOrder.Language.Formula.realize_top + +/-- The constant false predicate has either polarity. -/ +theorem falsity : + PolarityDefinable (L := L) policy mark sign M I ρ (fun _ (_ : α → _) => False) := + (ofFO (⊥ : L.Formula α)).congr fun _ _ => FirstOrder.Language.Formula.realize_bot + +/-- Equality of native terms has either polarity. -/ +theorem equal (a b : L.Term α) : + PolarityDefinable (L := L) policy mark sign M I ρ + (fun i v => a.realize (M := M i) v = b.realize v) := + (ofFO (a.equal b)).congr fun _ _ => by simp + +/-- Equality of variables is an atomic polarity-aware synthesis rule. -/ +theorem var_eq (a b : α) : + PolarityDefinable (L := L) policy mark sign M I ρ (fun _ v => v a = v b) := + equal (.var a) (.var b) + +/-- Native vocabulary relations have either polarity in scoped relation variables. -/ +theorem relation {k : ℕ} (r : L.Relations k) (args : Fin k → L.Term α) : + PolarityDefinable (L := L) policy mark sign M I ρ + (fun i v => Structure.RelMap (M := M i) r (fun j => (args j).realize v)) := + (ofFO (r.formula args)).congr fun _ _ => by simp + +/-- Native vocabulary relations applied to variable tuples have either polarity. -/ +theorem relation_vars {k : ℕ} (r : L.Relations k) (args : Fin k → α) : + PolarityDefinable (L := L) policy mark sign M I ρ + (fun i v => Structure.RelMap (M := M i) r (v ∘ args)) := + relation r (fun j => .var (args j)) + +/-- Binary vocabulary relations in vector notation are atomic synthesis rules. -/ +theorem relation₂ (r : L.Relations 2) (a b : α) : + PolarityDefinable (L := L) policy mark sign M I ρ + (fun i v => Structure.RelMap (M := M i) r ![v a, v b]) := + (ofFO (FO.rel₂ r a b)).congr fun _ v => FO.realize_rel₂ v r a b + +/-- A scoped relation atom is positive in every marked relation. -/ +theorem rel {k : ℕ} (r : RelVar Γ k) (args : Fin k → L.Term α) : + PolarityDefinable (L := L) policy mark true M I ρ + (fun i v => (fun j => (args j).realize v) ∈ ρ i r) := + ⟨.rel r args, rfl, rfl, fun _ _ => Iff.rfl⟩ + +/-- An unmarked relation atom has either polarity. -/ +theorem rel_unmarked {k : ℕ} (r : RelVar Γ k) (hm : mark r = false) + (args : Fin k → L.Term α) : + PolarityDefinable (L := L) policy mark sign M I ρ + (fun i v => (fun j => (args j).realize v) ∈ ρ i r) := + ⟨.rel r args, rfl, by simp [Formula.checkPolarity, hm], fun _ _ => Iff.rfl⟩ + +/-- Variable arguments give the usual positive relation application. -/ +theorem rel_vars {k : ℕ} (r : RelVar Γ k) (args : Fin k → α) : + PolarityDefinable (L := L) policy mark true M I ρ (fun i v => (v ∘ args) ∈ ρ i r) := + rel r (fun j => .var (args j)) + +/-- Unmarked relation variables can be applied to variables at either polarity. -/ +theorem rel_vars_unmarked {k : ℕ} (r : RelVar Γ k) (hm : mark r = false) + (args : Fin k → α) : + PolarityDefinable (L := L) policy mark sign M I ρ (fun i v => (v ∘ args) ∈ ρ i r) := + rel_unmarked r hm (fun j => .var (args j)) + +/-- Direct membership in the nearest bound relation is a positive atom. This form lets +synthesis start from the ordinary relation predicate, without reconstructing a relation index. -/ +theorem head_vars {k : ℕ} (mark : Marking (k :: Γ)) (R : ∀ i, Set (Fin k → M i)) + (args : Fin k → α) : + PolarityDefinable (L := L) policy mark true M I + (fun i => RelEnv.cons (R i) (ρ i)) (fun i v => (v ∘ args) ∈ R i) := + rel .here (fun j => .var (args j)) + +attribute [aesop safe apply (rule_sets := [FODefinable])] + ofFO neg conj disj imp ex all truth falsity equal var_eq relation relation_vars relation₂ + rel rel_unmarked rel_vars rel_vars_unmarked head_vars + +end PolarityDefinable + +end Cslib.Logic.FO.Operator diff --git a/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint.lean b/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint.lean new file mode 100644 index 000000000..a72e77f41 --- /dev/null +++ b/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint.lean @@ -0,0 +1,213 @@ +/- +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.Polarity +public import Complexity.Foundations.Order.FiniteFixedPoint + +/-! +# First-order logic with least fixed points + +FO(LFP) is an instance of the common first-order operator syntax. An arity-`k` binder adds one +`k`-ary relation and `k` first-order variables to its body. Other free variables are parameters, +fixed throughout the iteration. Terms at the application site are evaluated in the outer scope. + +`RawFormula` includes unchecked syntax; its total interpretation takes the intersection of +pre-fixed relations. For nonpositive bodies this need not be a fixed point. `Formula` bundles +the decidable well-formedness condition, checking positive recursion at every nested binder. +All fixed-point laws explicitly require positivity, which is proved to imply monotonicity. +Negation outside a fixed-point binder and arbitrary nesting remain available. + +## Main definitions + +* `shape`, `policy`, `interpretation`: the LFP instance of the shared operator interface. +* `RawFormula`, `Formula`, `lfp`, `Formula.lfp`: raw and checked FO(LFP) constructors. +* `step`, `stepHom`: the induced relation operator with fixed first-order parameters. + +## Main results + +* `step_monotone`: syntactic positivity implies semantic monotonicity. +* `realize_lfp`: LFP semantics agrees with Mathlib's `OrderHom.lfp`. +* `step_lfp`, `lfp_le`: fixed-point and leastness laws. +* `iterate_card_pow_eq_lfp`: on a domain of size `n`, arity `k` stabilizes at stage `n^k`. + +## References + +* [N. Immerman, *Descriptive Complexity*][Immerman1999], Chapter 4. +* [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. +-/ + +public section + +universe u v w z + +open FirstOrder Language + +namespace Cslib.Logic.FO.LFP + +/-- A least fixed point binds a relation and a tuple of the same arity. -/ +abbrev shape (k : ℕ) : Operator.Shape := + ⟨k, 1, fun _ => ⟨[k], k⟩⟩ + +/-- Least fixed points are monotone in their body and require positive self-reference. -/ +@[expose] def policy : Operator.Policy shape where + variance _ _ := .positive + positive _ _ {_} _ := true + +/-- FO(LFP) syntax before its recursive positivity conditions have been checked. -/ +abbrev RawFormula (L : Language.{u, v}) (Γ : List ℕ) (α : Type w) := + Operator.Formula L shape Γ α + +/-- FO(LFP) syntax with positive recursion at every nested binder. -/ +abbrev Formula (L : Language.{u, v}) (Γ : List ℕ) (α : Type w) := + Operator.CheckedFormula L policy Γ α + +/-- Total raw semantics: intersect all pre-fixed relations. The fixed-point laws below require +positive bodies; no fixed-point claim is made for invalid raw syntax. -/ +@[expose] def interpretation {M : Type z} : Operator.Interpretation shape M := + fun k F xs => xs ∈ sInf {R : Set (Fin k → M) | + ∀ ys, F (0 : Fin 1) (Operator.RelEnv.cons R Operator.RelEnv.empty) ys → ys ∈ R} + +/-- Raw LFP interpretation is monotone in the body transformer, even before checking positivity. -/ +theorem interpretation_respects {M : Type z} : + (interpretation (M := M)).Respects policy.variance := by + intro k F G h xs hx + apply Set.mem_of_subset_of_mem ?_ hx + apply sInf_le_sInf + intro R hR ys hy + exact hR ys (h (0 : Fin 1) (Operator.RelEnv.cons R Operator.RelEnv.empty) ys hy) + +variable {L : Language.{u, v}} {Γ : List ℕ} {α : Type w} {k : ℕ} + +/-- Apply a raw least-fixed-point binder to a tuple of terms. -/ +@[expose] def lfp (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) + (args : Fin k → L.Term α) : RawFormula L Γ α := + .op k (fun _ => body) args + +/-- Mark just the newly bound relation, leaving all outer relations fixed. -/ +@[expose] def headMark : Operator.Marking (k :: Γ) + | _, .here => true + | _, .there _ => false + +/-- A body is syntactically positive in the relation bound by this LFP. -/ +@[expose] def Positive (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) : Prop := + body.checkPolarity policy.variance true headMark = true + +/-- Positivity is a decidable syntactic property. -/ +instance (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) : Decidable (Positive body) := + inferInstanceAs (Decidable (_ = true)) + +/-- The generic local marking specializes to the nearest LFP relation. -/ +theorem inner_positive_eq_headMark : + @Operator.Marking.inner Γ [k] (policy.positive k (0 : Fin 1)) = @headMark Γ k := by + funext n r + cases r with + | here => rfl + | there r => rfl + +/-- An LFP is well formed exactly when its body is well formed and positive in its own relation. -/ +@[simp] theorem wellFormed_lfp (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) + (args : Fin k → L.Term α) : + (lfp body args).wellFormed policy = true ↔ body.wellFormed policy = true ∧ Positive body := by + simp only [lfp, Operator.Formula.wellFormed, decide_eq_true_eq] + change (∀ i : Fin 1, body.wellFormed policy = true ∧ + body.checkPolarity policy.variance true + (Operator.Marking.inner (policy.positive k i)) = true) ↔ _ + simp only [Fin.forall_fin_one, Positive] + have hcheck := congrArg + (fun mark : Operator.Marking (k :: Γ) => body.checkPolarity policy.variance true mark) + (inner_positive_eq_headMark (Γ := Γ) (k := k)) + rw [hcheck] + +namespace Formula + +/-- Construct a checked least fixed point from a checked, positive body. -/ +@[expose] def lfp (body : Formula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive body.val) + (args : Fin k → L.Term α) : Formula L Γ α := + ⟨LFP.lfp body.val args, (wellFormed_lfp _ _).2 ⟨body.property, hpos⟩⟩ + +/-- Realization of a checked FO(LFP) formula. -/ +@[expose] def Realize {M : Type z} [L.Structure M] (φ : Formula L Γ α) + (ρ : Operator.RelEnv Γ M) (v : α → M) : Prop := + φ.val.Realize interpretation ρ v + +end Formula + +variable {M : Type z} [L.Structure M] + +/-- The relation operator induced by a body, with its outer assignment and relations fixed. -/ +@[expose] def step (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) + (ρ : Operator.RelEnv Γ M) (v : α → M) (R : Set (Fin k → M)) : Set (Fin k → M) := + {xs | body.Realize interpretation (Operator.RelEnv.cons R ρ) (Sum.elim v xs)} + +/-- Positive recursion induces a monotone relation operator. -/ +theorem step_monotone (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive body) + (ρ : Operator.RelEnv Γ M) (v : α → M) : Monotone (step body ρ v) := by + intro R S hRS xs hx + apply Operator.Formula.realize_checkPolarity interpretation interpretation_respects body + hpos ?_ (Sum.elim v xs) hx + intro n r ys + cases r with + | here => exact ⟨fun hy => hRS hy, by simp [headMark]⟩ + | there r => exact ⟨id, fun _ => id⟩ + +/-- Bundle the syntactically certified relation operator as a Mathlib order homomorphism. -/ +@[expose] def stepHom (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive body) + (ρ : Operator.RelEnv Γ M) (v : α → M) : Set (Fin k → M) →o Set (Fin k → M) := + ⟨step body ρ v, step_monotone body hpos ρ v⟩ + +private theorem append_singleton (R : Set (Fin k → M)) (ρ : Operator.RelEnv Γ M) : + @Operator.RelEnv.append Γ [k] M (@Operator.RelEnv.cons [] M k R + (@Operator.RelEnv.empty M)) ρ = @Operator.RelEnv.cons Γ M k R ρ := by + funext n r + cases r <;> rfl + +/-- A positive raw LFP has the standard least-fixed-point semantics. This rewrites syntax to +the mathematical fixed point without recursively unfolding its defining equation. -/ +@[fo_realize] +theorem realize_lfp (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive body) + (args : Fin k → L.Term α) (ρ : Operator.RelEnv Γ M) (v : α → M) : + (lfp body args).Realize interpretation ρ v ↔ + (fun i => (args i).realize v) ∈ (stepHom body hpos ρ v).lfp := by + simp only [lfp, Operator.Formula.Realize, interpretation, shape, stepHom, OrderHom.lfp, + OrderHom.coe_mk, append_singleton, step, Set.subset_def, Set.mem_ofPred_eq] + +/-- The checked constructor exposes the same fixed-point semantics directly to simplification. -/ +@[simp, fo_realize] theorem Formula.realize_lfp + (body : Formula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive body.val) + (args : Fin k → L.Term α) (ρ : Operator.RelEnv Γ M) (v : α → M) : + (Formula.lfp body hpos args).Realize ρ v ↔ + (fun i => (args i).realize v) ∈ (stepHom body.val hpos ρ v).lfp := + LFP.realize_lfp body.val hpos args ρ v + +/-- The denotation is a fixed point of the body's actual relation operator. -/ +theorem step_lfp (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive body) + (ρ : Operator.RelEnv Γ M) (v : α → M) : + step body ρ v (stepHom body hpos ρ v).lfp = (stepHom body hpos ρ v).lfp := + (stepHom body hpos ρ v).map_lfp + +/-- The denotation is contained in every pre-fixed relation: the useful LFP induction rule. -/ +theorem lfp_le (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive body) + (ρ : Operator.RelEnv Γ M) (v : α → M) {R : Set (Fin k → M)} + (hR : step body ρ v R ⊆ R) : (stepHom body hpos ρ v).lfp ⊆ R := + (stepHom body hpos ρ v).lfp_le hR + +/-- A `k`-ary positive operator on a domain of size `n` reaches its least fixed point after +`n^k` applications from the empty relation. This includes empty domains and nullary relations. -/ +theorem iterate_card_pow_eq_lfp [Fintype M] + (body : RawFormula L (k :: Γ) (α ⊕ Fin k)) (hpos : Positive body) + (ρ : Operator.RelEnv Γ M) (v : α → M) : + ((step body ρ v)^[Fintype.card M ^ k]) ∅ = (stepHom body hpos ρ v).lfp := by + simpa only [Fintype.card_fun, Fintype.card_fin, stepHom, OrderHom.coe_mk, Set.bot_eq_empty] using + (stepHom body hpos ρ v).iterate_card_bot_eq_lfp + +end Cslib.Logic.FO.LFP diff --git a/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint/Definability.lean b/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint/Definability.lean new file mode 100644 index 000000000..66a5379ec --- /dev/null +++ b/Complexity/Logics/FirstOrder/Operator/LeastFixedPoint/Definability.lean @@ -0,0 +1,90 @@ +/- +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.LeastFixedPoint +public import Complexity.Logics.FirstOrder.Operator.Definability.Polarity +public import Complexity.Tactic.FOOperator.Init + +/-! +# Certified synthesis of least-fixed-point formulas + +A positive defining formula for a relation transformer gives a defining formula for its least +fixed point. The body certificate is uniform over both structures and candidate relations. The +polarity certificate is syntactic, so synthesis cannot hide negative recursion behind a semantic +monotonicity hypothesis. `fo_definable` composes the registered body rules and this LFP rule. + +## Main results + +* `definable_lfp`: synthesize a fixed-point application to arbitrary first-order terms. +* `definable_lfp_vars`, `definable_lfp_unary`: forms suited to predicates on free variables. +-/ + +public section + +universe u v w z t + +open FirstOrder Language + +namespace Cslib.Logic.FO.LFP + +variable {L : Language.{u, v}} {ι : Type t} {M : ι → Type z} [∀ i, L.Structure (M i)] + {Γ : List ℕ} {ρ : ∀ i, Operator.RelEnv Γ (M i)} {α : Type w} {k : ℕ} + +/-- A positive body certificate synthesizes an LFP formula defining a given family of monotone +operators. The single body witness works for every structure and every candidate relation. -/ +@[aesop safe apply (rule_sets := [FODefinable])] +theorem definable_lfp (F : ∀ i, (α → M i) → Set (Fin k → M i) →o Set (Fin k → M i)) + (args : Fin k → L.Term α) + (hF : Operator.PolarityDefinable (L := L) policy headMark true + (fun j : (i : ι) × Set (Fin k → M i) => M j.1) + (fun _ => interpretation) (fun j => Operator.RelEnv.cons j.2 (ρ j.1)) + (fun j v => (v ∘ Sum.inr) ∈ F j.1 (v ∘ Sum.inl) j.2)) : + Operator.Definable (L := L) policy M (fun _ => interpretation) ρ + (fun i v => (fun j => (args j).realize v) ∈ (F i v).lfp) := by + obtain ⟨body, hwf, hpos, hbody⟩ := hF + refine ⟨lfp body args, (wellFormed_lfp _ _).2 ⟨hwf, hpos⟩, ?_⟩ + intro i v + rw [realize_lfp body hpos args (ρ i) v] + have hstep : stepHom body hpos (ρ i) v = F i v := by + apply OrderHom.ext + funext R + ext xs + exact hbody ⟨i, R⟩ (Sum.elim v xs) + rw [hstep] + +/-- Free-variable tuples provide a directly matching synthesis rule for LFP membership. -/ +@[aesop safe apply (rule_sets := [FODefinable])] +theorem definable_lfp_vars + (F : ∀ i, (α → M i) → Set (Fin k → M i) →o Set (Fin k → M i)) (args : Fin k → α) + (hF : Operator.PolarityDefinable (L := L) policy headMark true + (fun j : (i : ι) × Set (Fin k → M i) => M j.1) + (fun _ => interpretation) (fun j => Operator.RelEnv.cons j.2 (ρ j.1)) + (fun j v => (v ∘ Sum.inr) ∈ F j.1 (v ∘ Sum.inl) j.2)) : + Operator.Definable (L := L) policy M (fun _ => interpretation) ρ + (fun i v => (v ∘ args) ∈ (F i v).lfp) := + definable_lfp F (fun j => .var (args j)) hF + +/-- Unary fixed-point predicates written with vector notation are synthesized directly. -/ +@[aesop safe apply (rule_sets := [FODefinable])] +theorem definable_lfp_unary + (F : ∀ i, (α → M i) → Set (Fin 1 → M i) →o Set (Fin 1 → M i)) (a : α) + (hF : Operator.PolarityDefinable (L := L) policy headMark true + (fun j : (i : ι) × Set (Fin 1 → M i) => M j.1) + (fun _ => interpretation) (fun j => Operator.RelEnv.cons j.2 (ρ j.1)) + (fun j v => (v ∘ Sum.inr) ∈ F j.1 (v ∘ Sum.inl) j.2)) : + Operator.Definable (L := L) policy M (fun _ => interpretation) ρ + (fun i v => ![v a] ∈ (F i v).lfp) := by + apply (definable_lfp F ![.var a] hF).congr + intro i v + have htuple : (fun j => ((![.var a] : Fin 1 → L.Term α) j).realize v) = ![v a] := by + funext j + simp only [Matrix.cons_val_fin_one, Term.realize_var] + rw [htuple] + +end Cslib.Logic.FO.LFP diff --git a/Complexity/Logics/FirstOrder/Operator/Polarity.lean b/Complexity/Logics/FirstOrder/Operator/Polarity.lean new file mode 100644 index 000000000..11974266c --- /dev/null +++ b/Complexity/Logics/FirstOrder/Operator/Polarity.lean @@ -0,0 +1,269 @@ +/- +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.Basic + +/-! +# Variance and formation rules for first-order operators + +Operator bodies may be monotone, antitone, or arbitrary. Positivity propagates through this +variance, not just through negations: an arbitrary operator (for example, a parity quantifier) +must not introduce a hidden negative dependency into a least fixed point. + +`Formula.checkPolarity` is a decidable syntactic check. `Formula.realize_checkPolarity` proves +its semantic guarantee from the operator interpretation's variance law. `Policy` separately +specifies which locally bound relations must occur positively; `Formula.wellFormed` checks this +condition at every nested operator. Raw interpretation itself does not assume well-formedness. + +## Main definitions + +* `Variance`, `Interpretation.Respects`: the semantic extension contract. +* `Policy`, `Formula.wellFormed`, `CheckedFormula`: formation rules and checked formulas. +* `Formula.checkPolarity`: syntactic dependence on a marked set of relation variables. + +## Main results + +* `Formula.realize_checkPolarity`: syntactic polarity implies semantic monotonicity or antitonicity. +* `Formula.wellFormed_relabel`: free-variable renaming preserves formation conditions. +-/ + +public section + +universe u v w z s + +open FirstOrder Language + +namespace Cslib.Logic.FO.Operator + +/-- The variance of an operator in one of its body predicates. -/ +inductive Variance + | positive + | negative + | arbitrary + deriving DecidableEq + +/-- The pointwise relation on body predicates required by a variance annotation. -/ +@[expose] def Variance.Relates : Variance → Prop → Prop → Prop + | .positive, p, q => p → q + | .negative, p, q => q → p + | .arbitrary, p, q => p ↔ q + +/-- A Boolean marking of relation variables. -/ +abbrev Marking (Γ : List ℕ) := ∀ {k}, RelVar Γ k → Bool + +namespace Marking + +/-- Mark only outer variables when passing under a binder. -/ +@[expose] def outer {Γ : List ℕ} (Δ : List ℕ) (mark : Marking Γ) : Marking (Δ ++ Γ) := + fun r => Sum.elim (fun _ => false) (fun r => mark r) (r.split Δ) + +/-- Mark only the selected locally bound variables. -/ +@[expose] def inner {Γ Δ : List ℕ} (mark : Marking Δ) : Marking (Δ ++ Γ) := + fun r => Sum.elim (fun r => mark r) (fun _ => false) (r.split Δ) + +/-- An empty marking stays empty under any number of relation binders. -/ +@[simp] theorem outer_false {Γ : List ℕ} (Δ : List ℕ) : + @outer Γ Δ (fun {_} _ => false) = (fun {_} _ => false) := by + funext k r + simp only [outer] + cases r.split Δ <;> rfl + +end Marking + +/-- The declared variance of every body of every operator. -/ +abbrev Variances {O : Type s} (shape : O → Shape) := + (o : O) → Fin (shape o).slots → Variance + +/-- An interpretation obeys the declared body variances. Arbitrary bodies must be equivalent. -/ +@[expose] def Interpretation.Respects {O : Type s} {shape : O → Shape} {M : Type z} + (I : Interpretation shape M) (variance : Variances shape) : Prop := + ∀ o F G, (∀ i δ xs, (variance o i).Relates (F i δ xs) (G i δ xs)) → + ∀ args, I o F args → I o G args + +/-- Operator-specific formation conditions, separate from binding and interpretation. -/ +structure Policy {O : Type s} (shape : O → Shape) where + /-- How an operator depends on each body. -/ + variance : Variances shape + /-- Locally bound relations required to occur positively in each body. -/ + positive : (o : O) → (i : Fin (shape o).slots) → Marking ((shape o).binder i).relations + +namespace Formula + +variable {L : Language.{u, v}} {O : Type s} {shape : O → Shape} + +/-- Check positive (`true`) or negative (`false`) dependence on the marked relations. +Arbitrary operator slots require both checks, conservatively excluding marked dependencies. -/ +@[expose] def checkPolarity (variance : Variances shape) : + {Γ : List ℕ} → {α : Type w} → Formula L shape Γ α → Bool → Marking Γ → Bool + | _, _, .ofFO _, _, _ => true + | _, _, .rel r _, sign, mark => sign || !mark r + | _, _, .neg φ, sign, mark => φ.checkPolarity variance (!sign) mark + | _, _, .conj φ ψ, sign, mark => + φ.checkPolarity variance sign mark && ψ.checkPolarity variance sign mark + | _, _, .ex φ, sign, mark => φ.checkPolarity variance sign mark + | _, _, .op o body _, sign, mark => decide (∀ i, + (match variance o i with + | .positive => (body i).checkPolarity variance sign + (mark.outer ((shape o).binder i).relations) + | .negative => (body i).checkPolarity variance (!sign) + (mark.outer ((shape o).binder i).relations) + | .arbitrary => (body i).checkPolarity variance true + (mark.outer ((shape o).binder i).relations) && + (body i).checkPolarity variance false + (mark.outer ((shape o).binder i).relations)) = true) + +/-- Check the local positivity requirements and recursively check all nested bodies. -/ +@[expose] def wellFormed (policy : Policy shape) : + {Γ : List ℕ} → {α : Type w} → Formula L shape Γ α → Bool + | _, _, .ofFO _ => true + | _, _, .rel _ _ => true + | _, _, .neg φ => φ.wellFormed policy + | _, _, .conj φ ψ => φ.wellFormed policy && ψ.wellFormed policy + | _, _, .ex φ => φ.wellFormed policy + | _, _, .op o body _ => decide (∀ i, (body i).wellFormed policy = true ∧ + (body i).checkPolarity policy.variance true (Marking.inner (policy.positive o i)) = true) + +/-- Every formula has both polarities when no relation variable is marked. -/ +@[simp] theorem checkPolarity_false {Γ : List ℕ} {α : Type w} + (variance : Variances shape) (φ : Formula L shape Γ α) (sign : Bool) : + φ.checkPolarity variance sign (fun {_} _ => false) = true := by + induction φ generalizing sign with + | ofFO _ => rfl + | rel _ _ => simp [checkPolarity] + | neg φ ih => exact ih _ + | conj φ ψ ihφ ihψ => simp [checkPolarity, ihφ, ihψ] + | ex φ ih => exact ih _ + | op o body args ih => + simp only [checkPolarity, Marking.outer_false, ih, Bool.and_self, decide_eq_true_eq] + intro i + cases variance o i <;> rfl + +/-- A checker's result does not depend on the names of free first-order variables. -/ +@[simp] theorem checkPolarity_relabel {Γ : List ℕ} {α β : Type w} + (variance : Variances shape) (φ : Formula L shape Γ α) (f : α → β) + (sign : Bool) (mark : Marking Γ) : + (φ.relabel f).checkPolarity variance sign mark = φ.checkPolarity variance sign mark := by + induction φ generalizing β sign with + | ofFO _ => rfl + | rel _ _ => rfl + | neg φ ih => exact ih _ _ _ + | conj φ ψ ihφ ihψ => simp only [relabel, checkPolarity, ihφ, ihψ] + | ex φ ih => exact ih _ _ _ + | op o body args ih => simp only [relabel, checkPolarity, ih] + +/-- Renaming free first-order variables preserves operator formation conditions. -/ +@[simp] theorem wellFormed_relabel {Γ : List ℕ} {α β : Type w} + (policy : Policy shape) (φ : Formula L shape Γ α) (f : α → β) : + (φ.relabel f).wellFormed policy = φ.wellFormed policy := by + induction φ generalizing β with + | ofFO _ => rfl + | rel _ _ => rfl + | neg φ ih => exact ih _ + | conj φ ψ ihφ ihψ => simp only [relabel, wellFormed, ihφ, ihψ] + | ex φ ih => exact ih _ + | op o body args ih => simp only [relabel, wellFormed, ih, checkPolarity_relabel] + +end Formula + +/-- A formula together with its checked operator formation conditions. -/ +abbrev CheckedFormula (L : Language.{u, v}) {O : Type s} {shape : O → Shape} + (policy : Policy shape) (Γ : List ℕ) (α : Type w) := + {φ : Formula L shape Γ α // φ.wellFormed policy = true} + +namespace RelEnv + +/-- Increase marked relations, keeping every unmarked relation fixed. -/ +@[expose] def LeOn {Γ : List ℕ} {M : Type z} (mark : Marking Γ) + (ρ σ : RelEnv Γ M) : Prop := + ∀ {k} (r : RelVar Γ k) xs, (xs ∈ ρ r → xs ∈ σ r) ∧ + (mark r = false → xs ∈ σ r → xs ∈ ρ r) + +/-- Equal local valuations preserve the comparison of the outer valuations. -/ +theorem LeOn.append {Γ Δ : List ℕ} {M : Type z} {mark : Marking Γ} {ρ σ : RelEnv Γ M} + (h : LeOn mark ρ σ) (δ : RelEnv Δ M) : + LeOn (mark.outer Δ) (δ.append ρ) (δ.append σ) := by + intro k r xs + simp only [RelEnv.append, Marking.outer] + cases r.split Δ with + | inl r => exact ⟨id, fun _ => id⟩ + | inr r => exact h r xs + +end RelEnv + +/-- The implication direction selected by a polarity. -/ +@[expose] def Directed : Bool → Prop → Prop → Prop + | true, p, q => p → q + | false, p, q => q → p + +namespace Formula + +variable {L : Language.{u, v}} {O : Type s} {shape : O → Shape} + {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] + +/-- The syntactic polarity check implies the corresponding semantic implication. +This includes nested operators and does not assume that raw syntax is well-formed. -/ +theorem realize_checkPolarity {variance : Variances shape} (I : Interpretation shape M) + (hI : I.Respects variance) (φ : Formula L shape Γ α) + {sign : Bool} {mark : Marking Γ} {ρ σ : RelEnv Γ M} + (hφ : φ.checkPolarity variance sign mark = true) (hρ : RelEnv.LeOn mark ρ σ) + (v : α → M) : Directed sign (φ.Realize I ρ v) (φ.Realize I σ v) := by + induction φ generalizing sign with + | ofFO φ => cases sign <;> exact id + | rel r args => + cases sign with + | false => + have hm : mark r = false := by simpa [checkPolarity] using hφ + exact (hρ r _).2 hm + | true => exact (hρ r _).1 + | neg φ ih => + cases sign with + | false => exact fun h hp => h (ih hφ hρ v hp) + | true => exact fun h hp => h (ih hφ hρ v hp) + | conj φ ψ ihφ ihψ => + have ⟨hφ, hψ⟩ : φ.checkPolarity variance sign mark = true ∧ + ψ.checkPolarity variance sign mark = true := by simpa [checkPolarity] using hφ + cases sign <;> exact fun h => ⟨ihφ hφ hρ v h.1, ihψ hψ hρ v h.2⟩ + | ex φ ih => + cases sign <;> exact fun ⟨x, hx⟩ => ⟨x, ih hφ hρ _ hx⟩ + | op o body args ih => + simp only [checkPolarity, decide_eq_true_eq] at hφ + have hbody := hφ + cases sign with + | true => + apply hI o + intro i δ xs + have hi := hbody i + cases hv : variance o i with + | positive => + simp only [hv] at hi + exact ih i hi (hρ.append δ) _ + | negative => + simp only [hv] at hi + exact ih i hi (hρ.append δ) _ + | arbitrary => + simp only [hv, Bool.and_eq_true] at hi + exact ⟨ih i hi.1 (hρ.append δ) _, ih i hi.2 (hρ.append δ) _⟩ + | false => + apply hI o + intro i δ xs + have hi := hbody i + cases hv : variance o i with + | positive => + simp only [hv] at hi + exact ih i hi (hρ.append δ) _ + | negative => + simp only [hv] at hi + exact ih i hi (hρ.append δ) _ + | arbitrary => + simp only [hv, Bool.and_eq_true] at hi + exact ⟨ih i hi.2 (hρ.append δ) _, ih i hi.1 (hρ.append δ) _⟩ + +end Formula + +end Cslib.Logic.FO.Operator diff --git a/Complexity/Logics/FirstOrder/Operator/Relabel.lean b/Complexity/Logics/FirstOrder/Operator/Relabel.lean new file mode 100644 index 000000000..75fde6012 --- /dev/null +++ b/Complexity/Logics/FirstOrder/Operator/Relabel.lean @@ -0,0 +1,158 @@ +/- +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.Polarity + +/-! +# Renaming and weakening free relation variables + +`Formula.relabelRel` renames outer relation variables by an arity-preserving map, leaving every +locally bound relation and all first-order variables unchanged. `Formula.weakenRel` specializes +this to adding an unused relation context, so reusable formulas can move beneath new binders +without reconstructing their relation atoms. + +## Main results + +* `Formula.realize_relabelRel`: renaming pulls back the relation valuation. +* `Formula.checkPolarity_relabelRel`: polarity checks pull back the marking. +* `Formula.wellFormed_relabelRel`: renaming preserves formation checks, even for noninjective maps. +* `Formula.realize_weakenRel`: new relation values do not affect a weakened formula. +-/ + +public section + +universe u v w z s + +open FirstOrder Language + +namespace Cslib.Logic.FO.Operator + +/-- Extend an arity-preserving renaming beneath a fixed prefix of local relation binders. -/ +@[expose] def RelVar.mapUnder {Γ Δ : List ℕ} + (Λ : List ℕ) (f : ∀ {k}, RelVar Γ k → RelVar Δ k) : + ∀ {k}, RelVar (Λ ++ Γ) k → RelVar (Λ ++ Δ) k := + match Λ with + | [] => f + | _ :: Λ => fun r => match r with + | .here => .here + | .there r => .there (mapUnder Λ f r) + +/-- Renaming beneath a binder leaves local variables fixed and maps only outer variables. -/ +@[simp] theorem RelVar.split_mapUnder {Γ Δ : List ℕ} + (Λ : List ℕ) (f : ∀ {k}, RelVar Γ k → RelVar Δ k) + {k : ℕ} (r : RelVar (Λ ++ Γ) k) : + (mapUnder Λ f r).split Λ = Sum.map id f (r.split Λ) := by + induction Λ with + | nil => rfl + | cons _ Λ ih => + cases r with + | here => rfl + | there r => + simp only [mapUnder, split, ih] + cases r.split Λ <;> rfl + +private theorem pull_append {Γ Δ Λ : List ℕ} {M : Type z} + (f : ∀ {k}, RelVar Γ k → RelVar Δ k) (δ : RelEnv Λ M) (ρ : RelEnv Δ M) : + (fun {k} (r : RelVar (Λ ++ Γ) k) => δ.append ρ (RelVar.mapUnder Λ f r)) = + @RelEnv.append Γ Λ M δ (fun {_} r => ρ (f r)) := by + funext k r + simp only [RelEnv.append, RelVar.split_mapUnder] + cases r.split Λ <;> rfl + +private theorem pull_outer {Γ Δ : List ℕ} (Λ : List ℕ) + (f : ∀ {k}, RelVar Γ k → RelVar Δ k) (mark : Marking Δ) : + (fun {k} (r : RelVar (Λ ++ Γ) k) => mark.outer Λ (RelVar.mapUnder Λ f r)) = + @Marking.outer Γ Λ (fun {_} r => mark (f r)) := by + funext k r + simp only [Marking.outer, RelVar.split_mapUnder] + cases r.split Λ <;> rfl + +private theorem pull_inner {Γ Δ Λ : List ℕ} + (f : ∀ {k}, RelVar Γ k → RelVar Δ k) (mark : Marking Λ) : + (fun {k} (r : RelVar (Λ ++ Γ) k) => mark.inner (RelVar.mapUnder Λ f r)) = + (mark.inner : Marking (Λ ++ Γ)) := by + funext k r + simp only [Marking.inner, RelVar.split_mapUnder] + cases r.split Λ <;> rfl + +namespace Formula + +variable {L : Language.{u, v}} {O : Type s} {shape : O → Shape} + {Γ Δ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] + +/-- Rename only free relation variables, fixing local binders and all first-order variables. -/ +@[expose] def relabelRel : {Γ Δ : List ℕ} → {α : Type w} → + (∀ {k}, RelVar Γ k → RelVar Δ k) → Formula L shape Γ α → Formula L shape Δ α + | _, _, _, _, .ofFO φ => .ofFO φ + | _, _, _, f, .rel r args => .rel (f r) args + | _, _, _, f, .neg φ => .neg (φ.relabelRel f) + | _, _, _, f, .conj φ ψ => .conj (φ.relabelRel f) (ψ.relabelRel f) + | _, _, _, f, .ex φ => .ex (φ.relabelRel f) + | _, _, _, f, .op o body args => + .op o (fun i => (body i).relabelRel (RelVar.mapUnder ((shape o).binder i).relations f)) args + +/-- Relabeling relations is interpreted by pulling back their valuation. -/ +@[simp, fo_realize] theorem realize_relabelRel (I : Interpretation shape M) + (φ : Formula L shape Γ α) (f : ∀ {k}, RelVar Γ k → RelVar Δ k) + (ρ : RelEnv Δ M) (v : α → M) : + (φ.relabelRel f).Realize I ρ v ↔ φ.Realize I (fun {_} r => ρ (f r)) v := by + induction φ generalizing Δ with + | ofFO _ => rfl + | rel _ _ => rfl + | neg φ ih => exact not_congr (ih _ _ _) + | conj φ ψ ihφ ihψ => exact and_congr (ihφ _ _ _) (ihψ _ _ _) + | ex φ ih => exact exists_congr fun _ => ih _ _ _ + | op o body args ih => simp only [relabelRel, Realize, ih, pull_append] + +/-- The polarity of renamed relations is checked using the pulled-back marking. -/ +@[simp] theorem checkPolarity_relabelRel (variance : Variances shape) + (φ : Formula L shape Γ α) (f : ∀ {k}, RelVar Γ k → RelVar Δ k) + (sign : Bool) (mark : Marking Δ) : + (φ.relabelRel f).checkPolarity variance sign mark = + φ.checkPolarity variance sign (fun {_} r => mark (f r)) := by + induction φ generalizing Δ sign with + | ofFO _ => rfl + | rel _ _ => rfl + | neg φ ih => exact ih _ _ _ + | conj φ ψ ihφ ihψ => simp only [relabelRel, checkPolarity, ihφ, ihψ] + | ex φ ih => exact ih _ _ _ + | op o body args ih => simp only [relabelRel, checkPolarity, ih, pull_outer] + +/-- Relation renaming leaves all locally checked formation conditions unchanged. -/ +@[simp] theorem wellFormed_relabelRel (policy : Policy shape) + (φ : Formula L shape Γ α) (f : ∀ {k}, RelVar Γ k → RelVar Δ k) : + (φ.relabelRel f).wellFormed policy = φ.wellFormed policy := by + induction φ generalizing Δ with + | ofFO _ => rfl + | rel _ _ => rfl + | neg φ ih => exact ih _ + | conj φ ψ ihφ ihψ => simp only [relabelRel, wellFormed, ihφ, ihψ] + | ex φ ih => exact ih _ + | op o body args ih => + simp only [relabelRel, wellFormed, ih, checkPolarity_relabelRel, pull_inner] + +/-- Add unused relation binders to the outer context of a reusable formula. -/ +@[expose] def weakenRel (Λ : List ℕ) (φ : Formula L shape Γ α) : + Formula L shape (Λ ++ Γ) α := φ.relabelRel (RelVar.lift Λ) + +/-- New relation values do not affect a weakened formula. -/ +@[simp, fo_realize] theorem realize_weakenRel (I : Interpretation shape M) + (Λ : List ℕ) (φ : Formula L shape Γ α) (δ : RelEnv Λ M) (ρ : RelEnv Γ M) + (v : α → M) : (φ.weakenRel Λ).Realize I (δ.append ρ) v ↔ φ.Realize I ρ v := by + simp only [weakenRel, realize_relabelRel, RelEnv.append_lift] + +/-- Adding unused relation binders preserves well-formedness. -/ +@[simp] theorem wellFormed_weakenRel (policy : Policy shape) + (Λ : List ℕ) (φ : Formula L shape Γ α) : + (φ.weakenRel Λ).wellFormed policy = φ.wellFormed policy := + wellFormed_relabelRel policy φ _ + +end Formula + +end Cslib.Logic.FO.Operator diff --git a/Complexity/Logics/FirstOrder/Operator/TransitiveClosure.lean b/Complexity/Logics/FirstOrder/Operator/TransitiveClosure.lean new file mode 100644 index 000000000..277b5bcc6 --- /dev/null +++ b/Complexity/Logics/FirstOrder/Operator/TransitiveClosure.lean @@ -0,0 +1,158 @@ +/- +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.Polarity +public import Mathlib.Data.Fin.Tuple.Basic +public import Mathlib.Logic.Relation + +/-! +# First-order logic with tuple transitive closure + +The operator of width `k` binds two `k`-tuples in one formula body and is applied to two +`k`-tuples of terms. Its interpretation is the **reflexive** transitive closure of the relation +defined by the body. Free parameters are held fixed along the path, and bodies may contain +nested closure operators. Width zero is allowed: there is one empty tuple, even on an empty +domain, and its reflexive reachability always holds. + +## Main definitions + +* `shape`, `policy`, `interpretation`: tuple closure as a scoped, positive logical operator. +* `tc`: the formula constructor. +* `pair`, `left`, `right`: concatenate and split the endpoint tuples. + +## Main results + +* `interpretation_respects`: closure is monotone in its body relation. +* `realize_tc`: semantics in terms of Mathlib's `Relation.ReflTransGen`. +* `realize_tc_pair`: the same semantics with explicit source and target term tuples. +* `realize_tc_refl`, `realize_tc_of_body`, `realize_tc_trans`: reflexivity, edge inclusion, + and composition of paths. + +This file provides logical syntax and semantics, not a complexity-class capture theorem. + +## References + +* [N. Immerman, *Descriptive Complexity*, Chapter 9][Immerman1999] +-/ + +public section + +universe u v w z + +open FirstOrder Language Cslib.Logic.FO.Operator + +namespace Cslib.Logic.FO.TC + +/-- Concatenate equal-length tuples, with the resulting arity written as `2 * k`. -/ +@[expose] def pair {A : Type*} {k : ℕ} (xs ys : Fin k → A) : Fin (2 * k) → A := + fun i => Fin.append xs ys (Fin.cast (Nat.two_mul k) i) + +/-- The source tuple of a closure application. -/ +@[expose] def left {A : Type*} {k : ℕ} (xs : Fin (2 * k) → A) : Fin k → A := + fun i => xs (Fin.cast (Nat.two_mul k).symm (Fin.castAdd k i)) + +/-- The target tuple of a closure application. -/ +@[expose] def right {A : Type*} {k : ℕ} (xs : Fin (2 * k) → A) : Fin k → A := + fun i => xs (Fin.cast (Nat.two_mul k).symm (Fin.natAdd k i)) + +/-- Concatenation preserves the source tuple. -/ +@[simp] theorem left_pair {A : Type*} {k : ℕ} (xs ys : Fin k → A) : + left (pair xs ys) = xs := by + funext i + simp [left, pair] + +/-- Concatenation preserves the target tuple. -/ +@[simp] theorem right_pair {A : Type*} {k : ℕ} (xs ys : Fin k → A) : + right (pair xs ys) = ys := by + funext i + simp only [right, pair, Fin.cast_cast, Fin.cast_eq_self, Fin.append_right] + +/-- Tuple closure binds two tuples and no relation variables. -/ +@[expose] def shape (k : ℕ) : Shape where + arity := 2 * k + slots := 1 + binder := fun _ => ⟨[], 2 * k⟩ + +/-- Closure is positive in its single body and imposes no local relation constraints. -/ +@[expose] def policy : Policy shape where + variance := fun _ _ => .positive + positive := fun _ _ {_} _ => false + +/-- Interpret closure as reflexive reachability between endpoint tuples. -/ +@[expose] def interpretation {M : Type z} : Interpretation shape M := + fun _ bodies args => + Relation.ReflTransGen (fun xs ys => bodies (0 : Fin 1) RelEnv.empty (pair xs ys)) + (left args) (right args) + +/-- Enlarging the body relation preserves all paths. -/ +theorem interpretation_respects {M : Type z} : + (@interpretation M).Respects policy.variance := by + intro k F G h args hp + exact Relation.ReflTransGen.mono + (fun xs ys hxy => h (0 : Fin 1) RelEnv.empty (pair xs ys) hxy) _ _ hp + +variable {L : Language.{u, v}} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Structure M] + +/-- Apply tuple closure to a body with two locally bound endpoint tuples. -/ +@[expose] def tc {k : ℕ} (body : Formula L shape Γ (α ⊕ Fin (2 * k))) + (args : Fin (2 * k) → L.Term α) : Formula L shape Γ α := + .op k (fun _ => body) args + +/-- Closure adds no formation condition beyond those already present in its body. -/ +@[simp] theorem wellFormed_tc {k : ℕ} + (body : Formula L shape Γ (α ⊕ Fin (2 * k))) (args : Fin (2 * k) → L.Term α) : + (tc body args).wellFormed policy = body.wellFormed policy := by + change decide (∀ _ : Fin 1, body.wellFormed policy = true ∧ + body.checkPolarity policy.variance true (fun {_} _ => false) = true) = + body.wellFormed policy + simp + +/-- Closure holds exactly when a finite path connects the evaluated endpoint tuples. -/ +@[simp, fo_realize] theorem realize_tc {k : ℕ} + (body : Formula L shape Γ (α ⊕ Fin (2 * k))) (args : Fin (2 * k) → L.Term α) + (ρ : RelEnv Γ M) (v : α → M) : + (tc body args).Realize interpretation ρ v ↔ + Relation.ReflTransGen + (fun xs ys => body.Realize interpretation ρ (Sum.elim v (pair xs ys))) + (fun i => (left args i).realize v) (fun i => (right args i).realize v) := Iff.rfl + +/-- Applying closure to concatenated endpoint terms realizes ordinary tuple reachability. -/ +@[simp, fo_realize] theorem realize_tc_pair {k : ℕ} + (body : Formula L shape Γ (α ⊕ Fin (2 * k))) (xs ys : Fin k → L.Term α) + (ρ : RelEnv Γ M) (v : α → M) : + (tc body (pair xs ys)).Realize interpretation ρ v ↔ + Relation.ReflTransGen + (fun us vs => body.Realize interpretation ρ (Sum.elim v (pair us vs))) + (fun i => (xs i).realize v) (fun i => (ys i).realize v) := by + simp only [realize_tc, left_pair, right_pair] + +/-- The empty path makes every tuple reachable from itself. -/ +theorem realize_tc_refl {k : ℕ} (body : Formula L shape Γ (α ⊕ Fin (2 * k))) + (xs : Fin k → L.Term α) (ρ : RelEnv Γ M) (v : α → M) : + (tc body (pair xs xs)).Realize interpretation ρ v := + (realize_tc_pair body xs xs ρ v).2 .refl + +/-- Every edge defined by the body is a closure path of length one. -/ +theorem realize_tc_of_body {k : ℕ} (body : Formula L shape Γ (α ⊕ Fin (2 * k))) + (xs ys : Fin k → L.Term α) (ρ : RelEnv Γ M) (v : α → M) + (h : body.Realize interpretation ρ + (Sum.elim v (pair (fun i => (xs i).realize v) (fun i => (ys i).realize v)))) : + (tc body (pair xs ys)).Realize interpretation ρ v := + (realize_tc_pair body xs ys ρ v).2 (.single h) + +/-- Paths with a common intermediate tuple compose. -/ +theorem realize_tc_trans {k : ℕ} (body : Formula L shape Γ (α ⊕ Fin (2 * k))) + (xs ys zs : Fin k → L.Term α) (ρ : RelEnv Γ M) (v : α → M) + (hxy : (tc body (pair xs ys)).Realize interpretation ρ v) + (hyz : (tc body (pair ys zs)).Realize interpretation ρ v) : + (tc body (pair xs zs)).Realize interpretation ρ v := + (realize_tc_pair body xs zs ρ v).2 + (((realize_tc_pair body xs ys ρ v).1 hxy).trans ((realize_tc_pair body ys zs ρ v).1 hyz)) + +end Cslib.Logic.FO.TC diff --git a/Complexity/Logics/FirstOrder/Operator/TransitiveClosure/Definability.lean b/Complexity/Logics/FirstOrder/Operator/TransitiveClosure/Definability.lean new file mode 100644 index 000000000..02b16dce5 --- /dev/null +++ b/Complexity/Logics/FirstOrder/Operator/TransitiveClosure/Definability.lean @@ -0,0 +1,81 @@ +/- +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.TransitiveClosure +public import Complexity.Logics.FirstOrder.Operator.Definability +public import Complexity.Tactic.FOOperator.Init + +/-! +# Certified synthesis of tuple transitive closure + +`definable_tc` constructs a well-formed closure formula from a certificate for its body. The +same formula works across the whole family of structures, including empty structures. Its rule +is registered in `FODefinable`, so `fo_definable` can compose closure with the ordinary logical +connectives and quantifiers. + +## Main results + +* `definable_tc`: synthesize closure from a uniformly definable body predicate. +* `definable_tc_pair`: the same certificate with separate source and target term tuples. +* `definable_tc_relation`: synthesize a semantic relation's closure directly. +-/ + +public section + +universe u v w z t + +open FirstOrder Language Cslib.Logic.FO.Operator + +namespace Cslib.Logic.FO.TC + +variable {L : Language.{u, v}} {ι : Type t} {M : ι → Type z} + [∀ i, L.Structure (M i)] {Γ : List ℕ} {ρ : ∀ i, RelEnv Γ (M i)} + {α : Type w} {k : ℕ} {P : ∀ i, (α ⊕ Fin (2 * k) → M i) → Prop} + +/-- A uniformly definable body has a uniformly definable tuple transitive closure. -/ +@[aesop safe apply (rule_sets := [FODefinable])] +theorem definable_tc (args : Fin (2 * k) → L.Term α) + (hP : Operator.Definable (L := L) policy M (fun _ => interpretation) ρ P) : + Operator.Definable (L := L) policy M (fun _ => interpretation) ρ + (fun i v => Relation.ReflTransGen (fun xs ys => P i (Sum.elim v (pair xs ys))) + (fun j => (left args j).realize v) (fun j => (right args j).realize v)) := by + obtain ⟨body, hbody, hP⟩ := hP + refine ⟨tc body args, by simpa only [wellFormed_tc] using hbody, ?_⟩ + intro i v + rw [realize_tc] + constructor + · exact Relation.ReflTransGen.mono (fun xs ys h => (hP i (Sum.elim v (pair xs ys))).1 h) _ _ + · exact Relation.ReflTransGen.mono (fun xs ys h => (hP i (Sum.elim v (pair xs ys))).2 h) _ _ + +/-- Synthesize tuple closure with separately supplied source and target terms. -/ +@[aesop safe apply (rule_sets := [FODefinable])] +theorem definable_tc_pair (xs ys : Fin k → L.Term α) + (hP : Operator.Definable (L := L) policy M (fun _ => interpretation) ρ P) : + Operator.Definable (L := L) policy M (fun _ => interpretation) ρ + (fun i v => Relation.ReflTransGen (fun us vs => P i (Sum.elim v (pair us vs))) + (fun j => (xs j).realize v) (fun j => (ys j).realize v)) := by + simpa only [left_pair, right_pair] using definable_tc (pair xs ys) hP + +/-- Synthesize a relation's closure directly. The body premise places the free parameters in +`Sum.inl` and the two endpoint tuples in `Sum.inr`. This formulation lets synthesis infer the +semantic relation without solving for a predicate applied to a composed assignment. -/ +@[aesop safe apply (rule_sets := [FODefinable])] +theorem definable_tc_relation (xs ys : Fin k → L.Term α) + {R : ∀ i, (α → M i) → (Fin k → M i) → (Fin k → M i) → Prop} + (hR : Operator.Definable (L := L) policy M (fun _ => interpretation) ρ + (fun i (v : α ⊕ Fin (2 * k) → M i) => + R i (v ∘ Sum.inl) (left (v ∘ Sum.inr)) (right (v ∘ Sum.inr)))) : + Operator.Definable (L := L) policy M (fun _ => interpretation) ρ + (fun i v => Relation.ReflTransGen (R i v) + (fun j => (xs j).realize v) (fun j => (ys j).realize v)) := by + apply (definable_tc_pair xs ys hR).congr + intro i v + simp only [Function.comp_def, Sum.elim_inl, Sum.elim_inr, left_pair, right_pair] + +end Cslib.Logic.FO.TC diff --git a/Complexity/Tactic/FOOperator.lean b/Complexity/Tactic/FOOperator.lean new file mode 100644 index 000000000..a3ab1933d --- /dev/null +++ b/Complexity/Tactic/FOOperator.lean @@ -0,0 +1,64 @@ +/- +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 +public import Complexity.Tactic.FOOperator.Init + +/-! +# Certified synthesis of formulas with logical operators + +`fo_definable` proves uniform definability of an ordinary Lean predicate by constructing a +well-formed formula, using the extensible Aesop rule set `FODefinable`. Its witness is a single +formula for the whole family of structures, rather than a formula chosen separately for each +structure. The built-in rules cover first-order atoms, Boolean connectives, and quantification. + +To add a semantic operation, prove a theorem whose conclusion is `Operator.Definable` and +register it with `@[aesop safe apply (rule_sets := [FODefinable])]`. The theorem must supply a +well-formed formula and prove its meaning; `Definable.of_formula` provides the explicit-witness +entry point. Free-variable renaming and equivalent semantic presentations are also available +through `Definable.relabel` and `Definable.congr`. + +Synthesis does not unfold fixed points or search over arbitrary formulas. Semantic reasoning +about an explicit formula continues to use the existing `fo_realize` simp set. In particular, +fixed-point unfolding is not a global simplification rule. + +## Main definitions + +* `fo_definable`: synthesize a uniformly defining, well-formed formula from registered rules. +* `fo_wf`: check formation conditions of explicit syntax, with optional simplification lemmas. +-/ + +public section + +open Cslib.Logic.FO.Operator +open Lean Parser.Tactic + +attribute [aesop safe apply (rule_sets := [FODefinable])] + Definable.ofFO Definable.neg Definable.conj Definable.disj Definable.imp + Definable.ex Definable.all Definable.truth Definable.falsity + Definable.var_eq Definable.equal Definable.relation Definable.relation_vars Definable.rel + Definable.relation₁ Definable.relation₂ Definable.rel_vars Definable.rel₁ Definable.rel₂ + +/-- Construct a well-formed defining formula by composing registered semantic certificates. -/ +macro "fo_definable" : tactic => + `(tactic| aesop (rule_sets := [FODefinable]) + (config := { terminal := true, enableSimp := false })) + +/-- Prove the formation conditions of explicit formula syntax. `fo_wf [φ, policy]` unfolds +named formulas and formation policies in addition to the structural checks. The tactic fails +unless it closes the goal; it never assumes positivity of a recursive relation. -/ +syntax (name := foWf) "fo_wf" (simpArgs)? : tactic + +macro_rules + | `(tactic| fo_wf $[[$args,*]]?) => + let args := args.map (·.getElems) |>.getD #[] + `(tactic| solve + | decide + | simp [Formula.wellFormed, Formula.checkPolarity, Formula.disj, Formula.all, + Marking.inner, Marking.outer, RelVar.split, $args,*]) diff --git a/Complexity/Tactic/FOOperator/Init.lean b/Complexity/Tactic/FOOperator/Init.lean new file mode 100644 index 000000000..05ce2b46d --- /dev/null +++ b/Complexity/Tactic/FOOperator/Init.lean @@ -0,0 +1,22 @@ +/- +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.Tactic.FirstOrder.Init + +/-! +# Rule set for certified formula synthesis + +`FODefinable` contains compositional certificates that synthesize a single well-formed formula +from a Lean predicate across a family of structures. Logical extensions can register their own +semantic operations in this rule set. The tactic is defined in `Complexity.Tactic.FOOperator`. +-/ + +public section + +declare_aesop_rule_sets [FODefinable] diff --git a/ComplexityTests/FOOperators.lean b/ComplexityTests/FOOperators.lean new file mode 100644 index 000000000..be049b3f1 --- /dev/null +++ b/ComplexityTests/FOOperators.lean @@ -0,0 +1,265 @@ +import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint.Definability +import Complexity.Logics.FirstOrder.Operator.Relabel +import Complexity.Logics.FirstOrder.Operator.TransitiveClosure.Definability +import Complexity.Tactic.FOOperator + +/-! Regression clients for scoped operators, exact least fixed points, and certified synthesis. -/ + +open FirstOrder Language Cslib.Logic.FO + +local instance {M : Type*} : Language.empty.Structure M := Language.emptyStructure + +namespace Formation + +private def selfBody : LFP.RawFormula Language.empty [1] (Unit ⊕ Fin 1) := + .rel .here ![.var (.inr 0)] + +private def self : LFP.RawFormula Language.empty [] Unit := + LFP.lfp selfBody ![.var ()] + +example : self.wellFormed LFP.policy = true := by + fo_wf [self, selfBody, LFP.lfp, LFP.policy, LFP.shape] + +-- Negating a completed fixed point is allowed; negating its recursive relation is not. +example : (Operator.Formula.neg self).wellFormed LFP.policy = true := by + fo_wf [self, selfBody, LFP.lfp, LFP.policy, LFP.shape] + +example : (LFP.lfp (.neg selfBody) ![.var ()]).wellFormed LFP.policy = false := by + fo_wf [selfBody, LFP.lfp, LFP.policy, LFP.shape] + +example : True := by + fail_if_success + have : (LFP.lfp (.neg selfBody) ![.var ()]).wellFormed LFP.policy = true := by + fo_wf [selfBody, LFP.lfp, LFP.policy, LFP.shape] + trivial + +-- The inner fixed point may depend negatively on a free outer relation. Binding that outer +-- relation as a least fixed point must reject the resulting negative recursion. +private def nestedNegative : LFP.RawFormula Language.empty [1] (Unit ⊕ Fin 1) := + LFP.lfp (.neg (.rel (.there .here) ![.var (.inr 0)])) ![.var (.inr 0)] + +example : nestedNegative.wellFormed LFP.policy = true := by + fo_wf [nestedNegative, LFP.lfp, LFP.policy, LFP.shape] + +example : (LFP.lfp nestedNegative ![.var ()]).wellFormed LFP.policy = false := by + fo_wf [nestedNegative, LFP.lfp, LFP.policy, LFP.shape] + +private def nestedPositive : LFP.RawFormula Language.empty [1] (Unit ⊕ Fin 1) := + LFP.lfp + (.disj (.rel (.there .here) ![.var (.inr 0)]) (.rel .here ![.var (.inr 0)])) + ![.var (.inr 0)] + +example : (LFP.lfp nestedPositive ![.var ()]).wellFormed LFP.policy = true := by + fo_wf [nestedPositive, LFP.lfp, LFP.policy, LFP.shape] + +-- μR.R is empty, even though every relation is a fixed point of its body. +example (b : Bool) : ¬ self.Realize LFP.interpretation Operator.RelEnv.empty (fun _ => b) := by + have hp : LFP.Positive selfBody := by decide + rw [self, LFP.realize_lfp selfBody hp] + have hle := LFP.lfp_le selfBody hp Operator.RelEnv.empty (fun _ => b) (R := ∅) + (by intro xs hx; exact hx) + exact fun h => hle h + +end Formation + +namespace Weakening + +private def unaryAtom : LFP.RawFormula Language.empty [1] Bool := + .rel .here (fun _ => .var true) + +-- Reusing an outer formula under a new binary binder does not capture its unary relation. +example : (unaryAtom.weakenRel [2]).relabel (Sum.inl : Bool → Bool ⊕ Fin 2) = + (.rel (.there .here) (fun _ => .var (.inl true)) : + LFP.RawFormula Language.empty [2, 1] (Bool ⊕ Fin 2)) := rfl + +example {L : Language} {Γ : List ℕ} {α : Type} (φ : LFP.RawFormula L Γ α) (k : ℕ) : + LFP.Positive ((φ.weakenRel [k]).relabel (Sum.inl : α → α ⊕ Fin k)) := by + unfold LFP.Positive + rw [Operator.Formula.checkPolarity_relabel] + change (φ.relabelRel (Operator.RelVar.lift [k])).checkPolarity _ _ _ = true + rw [Operator.Formula.checkPolarity_relabelRel] + exact Operator.Formula.checkPolarity_false _ φ true + +end Weakening + +namespace Parameters + +private def body : LFP.RawFormula Language.empty [1] (Bool ⊕ Fin 1) := + .ofFO (Term.equal (.var (.inr 0)) (.var (.inl false))) + +private theorem positive : LFP.Positive body := by decide + +-- One formula defines equality to the captured source parameter for every assignment. +private theorem parameter_iff (v : Bool → Bool) : + (LFP.lfp body ![.var true]).Realize LFP.interpretation Operator.RelEnv.empty v ↔ + v true = v false := by + rw [LFP.realize_lfp body positive] + rw [← LFP.step_lfp body positive Operator.RelEnv.empty v] + simp [LFP.step, body] + +example : ¬ (LFP.lfp body ![.var true]).Realize LFP.interpretation Operator.RelEnv.empty id := by + simp [parameter_iff] + +example : (LFP.lfp body ![.var true]).Realize LFP.interpretation Operator.RelEnv.empty + (fun _ => false) := (parameter_iff _).2 rfl + +-- The checked constructor also participates in the existing fo_realize simplification set. +example (v : Bool → Bool) : + (LFP.Formula.lfp ⟨body, rfl⟩ positive ![.var true]).Realize + Operator.RelEnv.empty v ↔ + ![v true] ∈ (LFP.stepHom body positive Operator.RelEnv.empty v).lfp := by + simp only [fo_realize] + apply iff_of_eq + congr 1 + funext i + simp only [Matrix.cons_val_fin_one, Term.realize_var] + +end Parameters + +namespace FiniteStages + +private def grow : Set Bool →o Set Bool where + toFun s := {b | b = false ∨ false ∈ s} + monotone' := fun _ _ h _ hb => hb.imp_right (fun hs => h hs) + +private theorem grow_lfp : grow.lfp = Set.univ := by + rw [← grow.iterate_card_bot_eq_lfp] + change (grow^[2]) ⊥ = Set.univ + ext b + change (b = false ∨ false = false ∨ false ∈ (∅ : Set Bool)) ↔ True + simp + +example : (grow^[1]) ∅ ≠ grow.lfp := by + intro h + have ht : true ∈ grow.lfp := by rw [grow_lfp]; trivial + rw [← h] at ht + change true = false ∨ false ∈ (∅ : Set Bool) at ht + simp at ht + +example : (grow^[9]) ∅ = Set.univ := + (grow.iterate_bot_eq_lfp_of_card_le (by decide)).trans grow_lfp + +example (f : Set (Fin 0) →o Set (Fin 0)) : f.lfp = ∅ := by + simpa using f.iterate_card_bot_eq_lfp.symm + +-- An empty domain still has one nullary tuple, so a true nullary body needs one stage. +private def nullary : LFP.RawFormula Language.empty [0] (Empty ⊕ Fin 0) := .ofFO ⊤ + +example : ((LFP.step nullary (Operator.RelEnv.empty (M := Empty)) Empty.elim)^[1]) ∅ = + (LFP.stepHom nullary (by decide) Operator.RelEnv.empty Empty.elim).lfp := by + simpa using LFP.iterate_card_pow_eq_lfp nullary (by decide) + (Operator.RelEnv.empty (M := Empty)) Empty.elim + +example : (Fin.elim0 : Fin 0 → Empty) ∈ + (LFP.stepHom nullary (by decide) Operator.RelEnv.empty Empty.elim).lfp := by + rw [← LFP.step_lfp nullary (by decide) Operator.RelEnv.empty Empty.elim] + simp [LFP.step, nullary] + +end FiniteStages + +namespace Closure + +private def falseBody : Operator.Formula Language.empty TC.shape [] (Bool ⊕ Fin 2) := .ofFO ⊥ +private def vertex (b : Bool) : Fin 1 → Language.empty.Term Bool := fun _ => .var b + +example : (TC.tc falseBody (TC.pair (vertex false) (vertex false))).Realize + TC.interpretation Operator.RelEnv.empty id := + TC.realize_tc_refl falseBody (vertex false) Operator.RelEnv.empty id + +example : ¬ (TC.tc falseBody (TC.pair (vertex false) (vertex true))).Realize + TC.interpretation Operator.RelEnv.empty id := by + rw [TC.realize_tc_pair] + intro h + rcases h.cases_head with heq | ⟨c, hc, _⟩ + · have := congrFun heq 0 + simp [vertex] at this + · simp [falseBody] at hc + +example : (TC.tc (k := 0) (.ofFO (⊥ : Language.empty.Formula (Empty ⊕ Fin 0))) + (TC.pair (k := 0) (Fin.elim0 : Fin 0 → Language.empty.Term Empty) Fin.elim0)).Realize + TC.interpretation (Operator.RelEnv.empty (M := Empty)) Empty.elim := + TC.realize_tc_refl _ _ _ _ + +end Closure + +namespace Synthesis + +variable {L : Language} {ι : Type} {M : ι → Type} [∀ i, L.Structure (M i)] {α : Type} + +example (a b c : α) : Operator.Definable (L := L) LFP.policy M (fun _ => LFP.interpretation) + (fun _ => Operator.RelEnv.empty) (fun _ v => v a = v b ∧ v b ≠ v c) := by + fo_definable + +example (a : α) : Operator.Definable (L := L) LFP.policy M (fun _ => LFP.interpretation) + (fun _ => Operator.RelEnv.empty) (fun _ v => ∃ x, x = v a) := by + fo_definable + +example (r : L.Relations 2) (xs ys : Fin 1 → L.Term α) : + Operator.Definable (L := L) TC.policy M (fun _ => TC.interpretation) + (fun _ => Operator.RelEnv.empty) + (fun i v => Relation.ReflTransGen + (fun us vs : Fin 1 → M i => Structure.RelMap r ![us 0, vs 0]) + (fun j => (xs j).realize v) (fun j => (ys j).realize v)) := by + fo_definable + +private def seeded {A : Type} (a : A) : Set (Fin 1 → A) →o Set (Fin 1 → A) where + toFun R := {xs | xs 0 = a ∨ xs ∈ R} + monotone' := fun _ _ h _ hx => hx.imp_right (fun hr => h hr) + +-- An ordinary Lean monotone operator is compiled to an LFP formula, including its positive body. +example (a b : α) : Operator.Definable (L := L) LFP.policy M (fun _ => LFP.interpretation) + (fun _ => Operator.RelEnv.empty) (fun _ v => ![v b] ∈ (seeded (v a)).lfp) := by + fo_definable + +private def reachStep {A : Type} [L.Structure A] (edge : L.Relations 2) (start : A) : + Set (Fin 1 → A) →o Set (Fin 1 → A) where + toFun R := {ys | ys 0 = start ∨ ∃ x, + (fun _ : Fin 1 => x) ∈ R ∧ Structure.RelMap edge ![x, ys 0]} + monotone' := by + intro R S h ys hy + rcases hy with hstart | ⟨x, hx, hedge⟩ + · exact Or.inl hstart + · exact Or.inr ⟨x, h hx, hedge⟩ + +-- The tactic also synthesizes the positive existential body of graph reachability. +example (edge : L.Relations 2) (a b : α) : + Operator.Definable (L := L) LFP.policy M (fun _ => LFP.interpretation) + (fun _ => Operator.RelEnv.empty) + (fun _ v => ![v b] ∈ (reachStep edge (v a)).lfp) := by + fo_definable + +example : True := by + fail_if_success + have : Operator.PolarityDefinable (L := Language.empty) LFP.policy + (LFP.headMark (Γ := []) (k := 1)) true + (fun _ : Set (Fin 1 → Bool) => Bool) (fun _ => LFP.interpretation) + (fun R => Operator.RelEnv.cons R Operator.RelEnv.empty) + (fun R v => ¬ v ∈ R) := by + fo_definable + trivial + +end Synthesis + +namespace MixedSignature + +-- This is a binding-shape/variance regression, not an implementation of regular languages. +-- A REG-style operator can have several bodies and arbitrary variance in each letter predicate. +private abbrev shape : ℕ ⊕ Unit → Operator.Shape := + Sum.elim LFP.shape (fun _ => ⟨0, 2, fun _ => ⟨[], 1⟩⟩) + +private def policy : Operator.Policy shape where + variance o _ := match o with | .inl _ => .positive | .inr _ => .arbitrary + positive o _ {_} _ := match o with | .inl _ => true | .inr _ => false + +private def bad : Operator.Formula Language.empty shape [] Unit := + .op (.inl 1) + (fun _ => .op (.inr ()) (fun _ => .rel .here ![.var (.inr (0 : Fin 1))]) Fin.elim0) + ![.var ()] + +private def good : Operator.Formula Language.empty shape [] Unit := + .op (.inl 1) (fun _ => .op (.inr ()) (fun _ => .ofFO ⊤) Fin.elim0) ![.var ()] + +example : bad.wellFormed policy = false := by decide +example : good.wellFormed policy = true := by decide + +end MixedSignature diff --git a/README.md b/README.md index c49bc594a..17745c7f6 100644 --- a/README.md +++ b/README.md @@ -27,6 +27,7 @@ examples. For setup or a particular task, start below. | Certify functional programs and loops | [PolyTime examples](ComplexityTests/PolyTimeTactic.lean) | | 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) | | 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 db07115f6..213f77551 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -264,7 +264,10 @@ universe size, not supplied as unverified input tables. In dependency order: 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. + 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. - 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.lean b/guide/ComplexityGuide.lean index c741152ae..c0a73a448 100644 --- a/guide/ComplexityGuide.lean +++ b/guide/ComplexityGuide.lean @@ -7,6 +7,7 @@ import VersoManual import ComplexityGuide.FirstSteps import ComplexityGuide.NPCompleteness import ComplexityGuide.Streaming +import ComplexityGuide.FirstOrderOperators open Verso.Genre Manual @@ -32,9 +33,9 @@ docstring and source. Other entry points: * [ROADMAP.md][roadmap] records outstanding work, and [CONTRIBUTING.md][contributing] explains how to propose and review changes. -The guide is new: after first steps, it has chapters on NP-completeness and streaming. Further -areas follow one at a time, and each chapter's friction points are fixed in the library rather -than documented around. +The guide is new: after first steps, it has chapters on NP-completeness, streaming, and first-order +logic with operators. Further areas follow one at a time, and each chapter's friction points are +fixed in the library rather than documented around. [cslib]: https://github.com/leanprover/cslib [api]: https://www.cslib.io/complexitylib/ @@ -49,3 +50,5 @@ than documented around. {include 1 ComplexityGuide.NPCompleteness} {include 1 ComplexityGuide.Streaming} + +{include 1 ComplexityGuide.FirstOrderOperators} diff --git a/guide/ComplexityGuide/FirstOrderOperators.lean b/guide/ComplexityGuide/FirstOrderOperators.lean new file mode 100644 index 000000000..058b4f233 --- /dev/null +++ b/guide/ComplexityGuide/FirstOrderOperators.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 +-/ +import VersoManual +import Complexity.Logics.FirstOrder.Operator.LeastFixedPoint.Definability +import Complexity.Logics.FirstOrder.Operator.Relabel +import Complexity.Logics.FirstOrder.Operator.TransitiveClosure.Definability +import Complexity.Tactic.FOOperator + +open Verso.Genre Manual +open Verso.Genre.Manual.InlineLean + +set_option pp.rawOnError true +set_option verso.code.warnLineLength 80 + +#doc (Manual) "First-Order Logic with Operators" => +%%% +tag := "first-order-operators" +%%% + +First-order formulas often describe a local step: two vertices share an edge, a tuple satisfies +a constraint, or a relation gains a new tuple. Logical operators turn those steps into paths or +least fixed points. The library provides a shared syntax for these extensions, concrete FO(LFP) +and FO(TC) interpretations, and certificates that construct formulas from ordinary Lean predicates. + +```lean -show +open FirstOrder Language Cslib.Logic.FO +``` + +# Binding and Interpretation +%%% +tag := "operator-binding" +%%% + +{name}`Cslib.Logic.FO.Operator.Shape` records the number of term arguments, the number of formula +bodies, and the local binders of each body. Each binder lists its relation arities and its number +of first-order variables. A body keeps ambient parameters under `Sum.inl` and sees its new tuple +variables under `Sum.inr`. + +{name}`Cslib.Logic.FO.Operator.Formula` uses Mathlib's native first-order terms and formulas for +its base language. A relation context is a list of arities: `RelVar.here` denotes the nearest +relation binder, and `RelVar.there` passes an inner binder to reach an outer variable. An +interpretation supplies the meaning of each operator; binding itself is independent of that meaning. + +Reusable formulas can move beneath a new relation binder with +`(φ.weakenRel [k]).relabel Sum.inl`. The first operation shifts outer relation variables; the +second shifts the free first-order parameters. Local binders inside `φ` remain local. The +{name}`Cslib.Logic.FO.Operator.Formula.realize_weakenRel` theorem shows that the new relation's +value cannot affect the weakened formula, and both operations preserve formation checks. + +# Least Fixed Points +%%% +tag := "operator-lfp" +%%% + +{name}`Cslib.Logic.FO.LFP.RawFormula` is syntax whose formation conditions have not yet been +checked. {name}`Cslib.Logic.FO.LFP.Formula` packages that syntax with a proof of well-formedness. +The `lfp` constructor binds a relation and a tuple of the same arity; its body must contain its +own relation positively. Ordinary negation outside that recursion is allowed, as are nested +fixed points and free parameters. + +Raw semantics is total: it intersects all pre-fixed relations. The fixed-point unfolding and +leastness laws require the positivity certificate. This distinction prevents a negative recursive +body from silently acquiring the laws of a monotone least fixed point. `fo_wf [definitions]` +checks formation of explicit syntax by unfolding its named formulas and the syntactic checks. + +For a finite structure with `n` elements and an arity-`k` relation, iteration starts at the empty +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. + +# Tuple Reachability +%%% +tag := "operator-tc" +%%% + +{name}`Cslib.Logic.FO.TC.tc` binds two `k`-tuples in its body and takes two endpoint tuples as +arguments. Its semantics is {name}`Relation.ReflTransGen`: a path of zero or more body edges. +The zero-length path makes a tuple reachable from itself even when the body is false. +Parameters stay fixed along the path. Width-zero closure is meaningful on an empty domain, +because there is still one empty tuple. + +{name}`Cslib.Logic.FO.TC.pair` concatenates the endpoints; `TC.left` and `TC.right` recover them. +The semantic API proves reflexivity, inclusion of body edges, and composition of paths. It does +not yet certify an FO(TC) model-checking machine or a capture theorem for NL. + +# Constructing Formulas from Predicates +%%% +tag := "operator-synthesis" +%%% + +{name}`Cslib.Logic.FO.Operator.Definable` asserts that one well-formed formula defines a predicate +throughout an indexed family of structures. The formula is chosen before the family index and +the variable assignment. A certificate therefore cannot select a different formula for each size. + +The `fo_definable` tactic composes certified construction rules. Here it builds a formula from an +ordinary predicate using existential quantification, conjunction, and equality: + +```lean +example {L : Language} {ι : Type} {M : ι → Type} + [∀ i, L.Structure (M i)] {α : Type} (a b : α) : + Operator.Definable (L := L) LFP.policy M + (fun _ => LFP.interpretation) (fun _ => Operator.RelEnv.empty) + (fun i v => ∃ x : M i, x = v a ∧ x = v b) := by + fo_definable +``` + +The LFP rule also starts from an ordinary Lean relation transformer. This step includes the +starting vertex and extends the current relation by one edge. The final `fo_definable` constructs +the fixed-point formula and certifies its positive, existential body: + +```lean +def exampleReachStep {L : Language} {A : Type} [L.Structure A] + (edge : L.Relations 2) (start : A) : + Set (Fin 1 → A) →o Set (Fin 1 → A) where + toFun R := {ys | ys 0 = start ∨ ∃ x, + (fun _ : Fin 1 => x) ∈ R ∧ Structure.RelMap edge ![x, ys 0]} + monotone' := by + intro R S h ys hy + rcases hy with hstart | ⟨x, hx, hedge⟩ + · exact Or.inl hstart + · exact Or.inr ⟨x, h hx, hedge⟩ + +example {L : Language} {ι : Type} {M : ι → Type} + [∀ i, L.Structure (M i)] {α : Type} + (edge : L.Relations 2) (a b : α) : + Operator.Definable (L := L) LFP.policy M + (fun _ => LFP.interpretation) (fun _ => Operator.RelEnv.empty) + (fun _ v => ![v b] ∈ (exampleReachStep edge (v a)).lfp) := by + fo_definable +``` + +Importing the TC synthesis module registers the closure rule as well. This example starts with +semantic reachability for an arbitrary binary relation symbol; the tactic constructs the closure +formula and its correctness proof: + +```lean +example {L : Language} {ι : Type} {M : ι → Type} + [∀ i, L.Structure (M i)] {α : Type} + (r : L.Relations 2) (xs ys : Fin 1 → L.Term α) : + Operator.Definable (L := L) TC.policy M + (fun _ => TC.interpretation) (fun _ => Operator.RelEnv.empty) + (fun i v => Relation.ReflTransGen + (fun us vs : Fin 1 → M i => Structure.RelMap r ![us 0, vs 0]) + (fun j => (xs j).realize v) (fun j => (ys j).realize v)) := by + fo_definable +``` + +An extension rule concludes `Operator.Definable`, supplies a well-formed formula witness, and +proves its semantics uniformly across the family. Register it with +`@[aesop safe apply (rule_sets := [FODefinable])]`. Rules for recursive bodies must also preserve +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. + +# Adding Other Operators +%%% +tag := "operator-extensions" +%%% + +{name}`Cslib.Logic.FO.Operator.Policy` declares each body's variance and its locally positive +relation variables. An interpretation proves {name}`Cslib.Logic.FO.Operator.Interpretation.Respects` +for that variance. Positive slots preserve implication; negative slots reverse it; arbitrary +slots require equivalence. The polarity checker propagates these requirements through nesting. + +A regular-language quantifier can use this binding interface and declare arbitrary variance for +a body whose changes are not monotone. In a recursive context, that declaration requires both +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. + +[examples]: https://github.com/cslib-community/complexitylib/blob/main/ComplexityTests/FOOperators.lean diff --git a/references.bib b/references.bib index dcfa40115..264d1991f 100644 --- a/references.bib +++ b/references.bib @@ -1458,6 +1458,18 @@ @article{EricksonVanDerHoogMiltzow2024 archivePrefix = {arXiv} } +@article{EsikLarsen2003, + author = {Ésik, Zoltán and Larsen, Kim G.}, + title = {Regular Languages Definable by Lindström Quantifiers}, + journal = {RAIRO -- Theoretical Informatics and Applications}, + volume = {37}, + number = {3}, + pages = {179--241}, + year = {2003}, + doi = {10.1051/ita:2003017}, + url = {https://www.numdam.org/item/10.1051/ita:2003017.pdf} +} + @article{EvenMansour1997, author = {Even, Shimon and Mansour, Yishay}, title = {A Construction of a Cipher from a Single Pseudorandom Permutation}, @@ -2332,6 +2344,16 @@ @inproceedings{IlangoLoffOliveira2020 doi = {10.4230/LIPIcs.CCC.2020.22} } +@article{Immerman1986, + author = {Immerman, Neil}, + title = {Relational Queries Computable in Polynomial Time}, + journal = {Information and Control}, + volume = {68}, + pages = {86--104}, + year = {1986}, + url = {https://people.cs.umass.edu/~immerman/pub/query.pdf} +} + @article{Immerman1988, author = {Immerman, Neil}, title = {Nondeterministic Space Is Closed under Complementation}, From 0f50f86f50959030e67fce8455c525fdb4d762b5 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 17:32:37 +0000 Subject: [PATCH 2/3] style(logic): wrap operator reference documentation --- Complexity/Logics/FirstOrder/Operator/Basic.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Complexity/Logics/FirstOrder/Operator/Basic.lean b/Complexity/Logics/FirstOrder/Operator/Basic.lean index 38cf0bbae..5ccb29b03 100644 --- a/Complexity/Logics/FirstOrder/Operator/Basic.lean +++ b/Complexity/Logics/FirstOrder/Operator/Basic.lean @@ -31,8 +31,9 @@ not assume that every operator is monotone or that every structure is finite or ## References * [N. Immerman, *Descriptive Complexity*][Immerman1999] -* [Z. Ésik and K. G. Larsen, *Regular Languages Definable by Lindström Quantifiers*][EsikLarsen2003], - Section 2, for multiple scoped bodies in regular-language quantifiers. +* [Z. Ésik and K. G. Larsen, *Regular Languages Definable by Lindström + Quantifiers*][EsikLarsen2003], Section 2, for multiple scoped bodies + in regular-language quantifiers. -/ public section From 746c420f90ffceca479b42b75f65244e3bec3b0a Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 21:38:27 -0400 Subject: [PATCH 3/3] fix(logic): resolve operator automation lints Name the existing fo_definable macro explicitly without changing its token or expansion. Remove only the redundant global simp attribute from realize_tc_pair, retaining fo_realize, the statement and proof. AI assistance: OpenAI Codex prepared this bounded coordinator fix for the two existing PR #1774 lint findings; the original mathematical authorship is preserved. --- Complexity/Logics/FirstOrder/Operator/TransitiveClosure.lean | 2 +- Complexity/Tactic/FOOperator.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Complexity/Logics/FirstOrder/Operator/TransitiveClosure.lean b/Complexity/Logics/FirstOrder/Operator/TransitiveClosure.lean index 277b5bcc6..21e48cfa1 100644 --- a/Complexity/Logics/FirstOrder/Operator/TransitiveClosure.lean +++ b/Complexity/Logics/FirstOrder/Operator/TransitiveClosure.lean @@ -123,7 +123,7 @@ variable {L : Language.{u, v}} {Γ : List ℕ} {α : Type w} {M : Type z} [L.Str (fun i => (left args i).realize v) (fun i => (right args i).realize v) := Iff.rfl /-- Applying closure to concatenated endpoint terms realizes ordinary tuple reachability. -/ -@[simp, fo_realize] theorem realize_tc_pair {k : ℕ} +@[fo_realize] theorem realize_tc_pair {k : ℕ} (body : Formula L shape Γ (α ⊕ Fin (2 * k))) (xs ys : Fin k → L.Term α) (ρ : RelEnv Γ M) (v : α → M) : (tc body (pair xs ys)).Realize interpretation ρ v ↔ diff --git a/Complexity/Tactic/FOOperator.lean b/Complexity/Tactic/FOOperator.lean index a3ab1933d..bb10104ca 100644 --- a/Complexity/Tactic/FOOperator.lean +++ b/Complexity/Tactic/FOOperator.lean @@ -46,7 +46,7 @@ attribute [aesop safe apply (rule_sets := [FODefinable])] Definable.relation₁ Definable.relation₂ Definable.rel_vars Definable.rel₁ Definable.rel₂ /-- Construct a well-formed defining formula by composing registered semantic certificates. -/ -macro "fo_definable" : tactic => +macro (name := foDefinable) "fo_definable" : tactic => `(tactic| aesop (rule_sets := [FODefinable]) (config := { terminal := true, enableSimp := false }))