Counting problems and parsimonious reductions

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

definition

Loading review…

Natural Language Statement

Definition

A counting problem over a relational vocabulary $L$ attaches a natural number $C(A)$ to every $L$ -structure $A$ , the same on isomorphic structures. Its support is the decision problem whose yes-instances are the structures with a positive count. A problem can be given by any number attached to structures: its value on $A$ is the least of the numbers attached to the structures isomorphic to $A$ , which is the number itself when that is invariant.

A parsimonious reduction from $C$ to $D$ , a notion due to Simon, is a first-order interpretation under which the counts agree: $C(A) = D(I(A))$ for every nonempty finite $A$ . In an ordered parsimonious reduction the interpretation reads the ordered expansion and the equation holds for every linear order on $A$ ; in a relativized one, the interpreted universe is a definable subset of the tagged tuples, nonempty on nonempty structures.

Concept map

4 concepts; 21 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Order.PiLex
2	import Mathlib.Data.Prod.Lex
3	import Mathlib.Data.Fintype.EquivFin
4	import Mathlib.ModelTheory.Order
5	import Mathlib.ModelTheory.Semantics
6	import Mathlib.ModelTheory.Complexity
7	import Mathlib.Tactic.FinCases
8	import Mathlib.Logic.Equiv.Fin.Basic
9	import Lax904597.Interpretations
10	import Lax904597.Problems
11	import Lax904597.Relativized
12	import Mathlib.Order.Lattice.Nat
13
14	/-!
15	---
16	title: Counting problems and parsimonious reductions
17	type: definition
18	---
19	A counting problem over a relational vocabulary $L$ attaches a natural
20	number $C(A)$ to every $L$ -structure $A$ , the same on isomorphic structures.
21	Its support is the decision problem whose yes-instances are the structures
22	with a positive count. A problem can be given by any number attached to
23	structures: its value on $A$ is the least of the numbers attached to the
24	structures isomorphic to $A$ , which is the number itself when that is
25	invariant.
26
27	A parsimonious reduction from $C$ to $D$ , a notion due to Simon, is a
28	first-order interpretation under which the counts agree: $C(A) = D(I(A))$
29	for every nonempty finite $A$ . In an ordered parsimonious reduction the interpretation reads the
30	ordered expansion and the equation holds for every linear order on $A$ ; in
31	a relativized one, the interpreted universe is a definable subset of the
32	tagged tuples, nonempty on nonempty structures.
33	-/
34
35	namespace Lax366625.CountingProblems
36
37	open Lax904597.Interpretations Lax904597.Problems Lax904597.Relativized
38
39	open FirstOrder
40
41	open Language Structure
42
43	variable (L : Language.{0, 0})
44
45	/-- A counting problem: an isomorphism-invariant natural number attached to
46	every `L`-structure. Only the values on finite structures are ever read. -/
47	structure CountingProblem [L.IsRelational] where
48	/-- The count: `C A` (through the function coercion) is the number attached
49	to the structure `A`. -/
50	Count : ∀ (A : Type) [L.Structure A], ℕ
51	/-- Counting problems do not distinguish isomorphic structures. -/
52	iso_invariant : ∀ {A B : Type} [L.Structure A] [L.Structure B],
53	(A ≃[L] B) → Count A = Count B
54
55	namespace CountingProblem
56
57	variable {L} [L.IsRelational]
58
59	instance instCoeFun : CoeFun (CountingProblem L) fun _ => ∀ (A : Type) [L.Structure A], ℕ :=
60	⟨Count⟩
61
62	/-- The counting problem given by a number attached to every structure: the
63	least value it takes on the structures isomorphic to a given one, which is
64	invariant by construction. When the number is itself invariant, this is the
65	number. -/
66	noncomputable def ofFun (f : ∀ (A : Type) [L.Structure A], ℕ) : CountingProblem L where
67	Count := fun A _ =>
68	sInf {n : ℕ \| ∃ (B : Type) (i : L.Structure B) (_ : @Language.Equiv L B A i _), @f B i = n}
69	iso_invariant := fun e =>
70	congrArg sInf (Set.ext fun _ =>
71	⟨fun ⟨B, i, g, h⟩ => ⟨B, i, e.comp g, h⟩, fun ⟨B, i, g, h⟩ => ⟨B, i, e.symm.comp g, h⟩⟩)
72
73	/-- The decision problem underneath a counting problem: is the count
74	positive? -/
75	def support (C : CountingProblem L) : DecisionProblem L where
76	Holds := fun A inst => 0 < @Count L _ C A inst
77	iso_invariant := fun e => by rw [C.iso_invariant e]
78
79	end CountingProblem
80
81	variable {L} {L' : Language.{0, 0}}
82
83	/-- A parsimonious first-order reduction from the counting problem `C` to the
84	counting problem `D`: a first-order interpretation under which the two counts
85	agree. -/
86	structure ParsimoniousReduction [L.IsRelational] [L'.IsRelational] (C : CountingProblem L)
87	(D : CountingProblem L') where
88	/-- The tags (copies of `A^dim`) used by the underlying interpretation. -/
89	Tag : Type
90	/-- Tags are finite, so that finite structures map to finite structures. -/
91	[tagFinite : Finite Tag]
92	/-- Tags are nonempty, so that nonempty structures map to nonempty
93	structures. -/
94	[tagNonempty : Nonempty Tag]
95	/-- The dimension of the underlying interpretation. -/
96	dim : ℕ
97	/-- The underlying first-order interpretation. -/
98	toInterpretation : FOInterpretation L L' Tag dim
99	/-- The counts agree, on the finite nonempty structures. -/
100	correct : ∀ (A : Type) [L.Structure A] [Finite A] [Nonempty A],
101	C A = D (toInterpretation.Map A)
102
103	/-- An ordered parsimonious reduction: a first-order interpretation over the
104	ordered expansion of the source vocabulary under which the two counts agree,
105	for every linear order of the (finite) input structure. -/
106	structure OrderedParsimoniousReduction [L.IsRelational] [L'.IsRelational]
107	(C : CountingProblem L) (D : CountingProblem L') where
108	/-- The tags (copies of `A^dim`) used by the underlying interpretation. -/
109	Tag : Type
110	/-- Tags are finite, so that finite structures map to finite structures. -/
111	[tagFinite : Finite Tag]
112	/-- Tags are nonempty, so that nonempty structures map to nonempty
113	structures. -/
114	[tagNonempty : Nonempty Tag]
115	/-- The dimension of the underlying interpretation. -/
116	dim : ℕ
117	/-- The underlying first-order interpretation, over the ordered expansion. -/
118	toInterpretation : FOInterpretation (L.sum Language.order) L' Tag dim
119	/-- The counts agree, whatever the linear order. -/
120	correct : ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
121	C A = D (toInterpretation.Map A)
122
123	open FirstOrder
124
125	open Language Structure
126
127	variable {L L' : Language.{0, 0}}
128
129	/-- An ordered parsimonious reduction through a relativized
130	interpretation: the two counts agree, the target structure being carried by
131	the definable subset of `Tag × A^dim` that the domain formula carves out. -/
132	structure RelOrderedParsimoniousReduction [L.IsRelational] [L'.IsRelational]
133	(C : CountingProblem L) (D : CountingProblem L') where
134	/-- The tags used by the underlying interpretation. -/
135	Tag : Type
136	/-- Tags are finite, so that finite structures map to finite structures. -/
137	[tagFinite : Finite Tag]
138	/-- The dimension of the underlying interpretation. -/
139	dim : ℕ
140	/-- The underlying relativized interpretation, over the ordered expansion. -/
141	toRelInterpretation : RelFOInterpretation (L.sum Language.order) L' Tag dim
142	/-- The definable domain is inhabited. -/
143	dom_nonempty : ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
144	∃ (t : Tag) (w : Fin dim → A), (toRelInterpretation.domFormula t).Realize w
145	/-- The counts agree, whatever the linear order. -/
146	correct : ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
147	C A = D (toRelInterpretation.MapRel A)
148
149	end Lax366625.CountingProblems
150

Discussion

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

Loading discussion…

Lax Lean Archive

Counting problems and parsimonious reductions

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments