The class FP, by quantitative first-order logic with least fixed points

Lax366625.QuantitativeLogic · concepts/Lax366625/QuantitativeLogic.lean · lax-366625

definition

Loading review…

Natural Language Statement

Definition

The terms of quantitative first-order logic QFO are built from first-order formulas, read as $1$ or $0$ , and constants, by addition, multiplication, and sums and products over tuples of elements. A definition in QFO(LFP) over $L$ is a rule system defining a least fixed point, as in FO(LFP), and a closed QFO term over $L \cup \{\le\}$ expanded by the relation variables, read at the fixed point. A counting problem is in FP when some definition takes the value $C(A)$ on every nonempty finite $L$ -structure $A$ , for every linear order on $A$ ; this is the logic of polynomial-time computable functions of Arenas, Muñoz, and Riveros. FP is the counting class of these problems.

A digit definition is a least fixed point together with relation variables of a common arity holding the binary digits of a number: the digit of weight $2^r$ is $1$ when the tuple of rank $r$ in the lexicographic order is in its relation. A counting problem is digit-definable when its value is given by such a definition.

Concept map

11 concepts; 12 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Algebra.BigOperators.Finprod
2	import Mathlib.Order.PiLex
3	import Mathlib.Data.Prod.Lex
4	import Mathlib.Data.Set.Card
5	import Mathlib.ModelTheory.Order
6	import Mathlib.ModelTheory.Semantics
7	import Mathlib.ModelTheory.Complexity
8	import Mathlib.Tactic.FinCases
9	import Mathlib.Order.Lattice.Nat
10	import Mathlib.Data.Fintype.EquivFin
11	import Mathlib.Logic.Equiv.Fin.Basic
12	import Mathlib.Data.Finite.Sigma
13	import Mathlib.Data.Fintype.Lattice
14	import Mathlib.Data.Fintype.Pigeonhole
15	import Mathlib.Dynamics.FixedPoints.Basic
16	import Mathlib.Algebra.Order.BigOperators.Group.Finset
17	import Mathlib.ModelTheory.Syntax
18	import Mathlib.Data.Fintype.Card
19	import Mathlib.SetTheory.Cardinal.Finite
20	import Lax366625.CountingProblems
21	import Lax535992.HornFragment
22	import Lax535992.LeastFixedPoint
23	import Lax895169.BitPredicate
24	import Lax904597.SecondOrder
25	import Lax366625.CountingClasses
26
27	/-!
28	---
29	title: The class FP, by quantitative first-order logic with least fixed points
30	type: definition
31	---
32	The terms of quantitative first-order logic QFO are built from first-order
33	formulas, read as $1$ or $0$ , and constants, by addition, multiplication,
34	and sums and products over tuples of elements. A definition in QFO(LFP)
35	over $L$ is a rule system defining a least fixed point, as in FO(LFP), and a
36	closed QFO term over $L \cup \{\le\}$ expanded by the relation variables,
37	read at the fixed point. A counting problem is in FP when some definition
38	takes the value $C(A)$ on every nonempty finite $L$ -structure $A$ , for every
39	linear order on $A$ ; this is the logic of polynomial-time computable
40	functions of Arenas, Muñoz, and Riveros. FP is the counting class of these
41	problems.
42
43	A digit definition is a least fixed point together with relation variables
44	of a common arity holding the binary digits of a number: the digit of
45	weight $2^r$ is $1$ when the tuple of rank $r$ in the lexicographic order is
46	in its relation. A counting problem is digit-definable when its value is
47	given by such a definition.
48	-/
49
50	namespace Lax366625.QuantitativeLogic
51
52	open Lax366625.CountingProblems Lax535992.HornFragment Lax535992.LeastFixedPoint
53	open Lax895169.BitPredicate Lax904597.SecondOrder
54
55	open FirstOrder
56
57	open Language Structure
58
59	/-- A definition of a number by its binary digits: a least fixed point, as for
60	`LFPDef`, and the relation variables holding the
61	digits. -/
62	structure DigitLFPDef (L : Language.{0, 0}) : Type 1 where
63	/-- The relation variables computed by the fixed point. -/
64	B : SOBlock
65	/-- The number of first-order variables shared by the rules. -/
66	k : ℕ
67	/-- The rules defining the variables. -/
68	rules : List (HornClause (L.sum Language.order) B k)
69	/-- The number of relation variables holding digits. -/
70	c : ℕ
71	/-- There is at least one. -/
72	c_pos : 0 < c
73	/-- Their common arity. -/
74	ℓ : ℕ
75	/-- The relation variables holding the digits, the least significant
76	first. -/
77	bit : Fin c → B.ι
78	/-- They are distinct. -/
79	bit_injective : Function.Injective bit
80	/-- They have the same arity. -/
81	arity_bit : ∀ τ, B.arity (bit τ) = ℓ
82
83	namespace DigitLFPDef
84
85	variable {L : Language.{0, 0}} (d : DigitLFPDef L) (A : Type) [L.Structure A] [LinearOrder A]
86
87	/-- The digit at a position is `1`: the tuple is in the relation of its
88	group. -/
89	def Holds (q : Fin d.c ×ₗ Lex (Fin d.ℓ → A)) : Prop :=
90	lfpAssign d.rules (d.bit (ofLex q).1)
91	fun k => ofLex (ofLex q).2 (Fin.cast (d.arity_bit (ofLex q).1) k)
92
93	open Classical in
94	/-- The value of a definition on an ordered structure: the number whose digit
95	of weight `2 ^ r` is `1` exactly when the position of rank `r` is in its
96	relation of the least fixed point. -/
97	noncomputable def value : ℕ :=
98	∑ᶠ q : Fin d.c ×ₗ Lex (Fin d.ℓ → A), if d.Holds A q then 2 ^ orank q else 0
99
100	end DigitLFPDef
101
102	/-- A counting problem is digit-definable when, on nonempty finite
103	structures, its binary digits are relations of a least fixed point, whatever
104	the linear order. -/
105	def DigitDefinable {L : Language.{0, 0}} [L.IsRelational] (C : CountingProblem L) : Prop :=
106	∃ d : DigitLFPDef L, ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
107	C A = d.value A
108
109	open FirstOrder
110
111	open Language Structure
112
113	/-- The terms of quantitative first-order logic over a Boolean layer of
114	first-order formulas, with free variables in `α`, after Arenas, Muñoz, and
115	Riveros, restricted to first-order quantifiers. A quantifier binds a block of
116	`n` variables at once, the variables `Sum.inr i` of `α ⊕ Fin n`; the
117	quantifiers `Σx` and `Πx` of their logic are the case `n = 1`. -/
118	inductive QTerm (L : Language.{0, 0}) : Type → Type 1
119	/-- A formula: `1` when it holds, `0` when it does not. -/
120	\| ind {α : Type} (φ : L.Formula α) : QTerm L α
121	/-- A constant. -/
122	\| const {α : Type} (s : ℕ) : QTerm L α
123	/-- A sum. -/
124	\| add {α : Type} (s t : QTerm L α) : QTerm L α
125	/-- A product. -/
126	\| mul {α : Type} (s t : QTerm L α) : QTerm L α
127	/-- `Σx̄. t`: the sum over the `n`-tuples of elements of the structure. -/
128	\| sum {α : Type} (n : ℕ) (t : QTerm L (α ⊕ Fin n)) : QTerm L α
129	/-- `Πx̄. t`: the product over the `n`-tuples of elements of the structure. -/
130	\| prod {α : Type} (n : ℕ) (t : QTerm L (α ⊕ Fin n)) : QTerm L α
131
132	namespace QTerm
133
134	variable {L L' : Language.{0, 0}}
135
136	open Classical in
137	/-- The value of a term in a structure, under a valuation. -/
138	noncomputable def eval {A : Type} [L.Structure A] : ∀ {α : Type}, QTerm L α → (α → A) → ℕ
139	\| _, ind φ, v => if φ.Realize v then 1 else 0
140	\| _, const s, _ => s
141	\| _, add s t, v => s.eval v + t.eval v
142	\| _, mul s t, v => s.eval v * t.eval v
143	\| _, sum _ t, v => ∑ᶠ w : Fin _ → A, t.eval (Sum.elim v w)
144	\| _, prod _ t, v => ∏ᶠ w : Fin _ → A, t.eval (Sum.elim v w)
145
146	/-- The value of a closed term. -/
147	noncomputable def value (t : QTerm L Empty) (A : Type) [L.Structure A] : ℕ :=
148	t.eval (A := A) default
149
150	end QTerm
151
152	/-- A definition in QFO(LFP): a least fixed point, as for
153	`LFPDef`, and a quantitative term over the vocabulary
154	expanded by its relations, read at the fixed point. -/
155	structure QLFPDef (L : Language.{0, 0}) : Type 1 where
156	/-- The relation variables computed by the fixed point. -/
157	B : SOBlock
158	/-- The number of first-order variables shared by the rules. -/
159	k : ℕ
160	/-- The rules defining the variables. -/
161	rules : List (HornClause (L.sum Language.order) B k)
162	/-- The quantitative output. -/
163	out : QTerm ((L.sum Language.order).sum B.lang) Empty
164
165	/-- The value of a definition on an ordered structure: the output, read at
166	the least fixed point of the rules. -/
167	noncomputable def QLFPDef.value {L : Language.{0, 0}} (d : QLFPDef L) (A : Type)
168	[L.Structure A] [LinearOrder A] : ℕ :=
169	@QTerm.value ((L.sum Language.order).sum d.B.lang) d.out A
170	(@sumStructure _ _ A _ (d.B.structure (lfpAssign d.rules)))
171
172	variable {L : Language.{0, 0}} [L.IsRelational]
173
174	/-- A counting problem is in FP when, on nonempty finite structures, it is
175	the value of a definition in QFO(LFP), whatever the linear order. -/
176	def FPDefinable (C : CountingProblem L) : Prop :=
177	∃ d : QLFPDef L, ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
178	C A = d.value A
179
180	open Lax366625.CountingClasses
181
182	/-- FP: the class of the counting problems definable in QFO(LFP). -/
183	def FP : CountingClass :=
184	CountingClass.ofMem fun C => FPDefinable C
185
186	end Lax366625.QuantitativeLogic
187

Builds on

Used by

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

The class FP, by quantitative first-order logic with least fixed points

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments