Subtractive reductions

Lax859101.SubtractiveReductions · concepts/Lax859101/SubtractiveReductions.lean · lax-859101

definition

Loading review…

Natural Language Statement

Definition

A strong subtractive reduction from $C$ to $D$ , after Durand, Hermann, and Kolaitis, presents $D$ as the witness count of a kernel and draws two instances of $D$ from an instance $A$ of $C$ by two first-order interpretations with the same tags and dimension, a subtrahend and a minuend, such that every witness at the subtrahend is a witness at the minuend and $C(A) + D(I_s(A)) = D(I_m(A))$ . Subtractive reducibility is a finite chain of strong subtractive and relativized ordered parsimonious steps. A counting problem is hard for a class when every member of the class subtractively reduces to it, and complete when it is moreover a member.

Concept map

8 concepts; 13 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Tactic.FinCases
2	import Mathlib.Order.PiLex
3	import Mathlib.Data.Prod.Lex
4	import Mathlib.Data.Fintype.EquivFin
5	import Mathlib.ModelTheory.Order
6	import Mathlib.ModelTheory.Semantics
7	import Mathlib.ModelTheory.Complexity
8	import Mathlib.Logic.Equiv.Fin.Basic
9	import Mathlib.Data.Fintype.Lattice
10	import Mathlib.Data.Finite.Sigma
11	import Mathlib.Order.Lattice.Nat
12	import Mathlib.Data.Set.Card
13	import Mathlib.Data.Fintype.Pigeonhole
14	import Mathlib.Dynamics.FixedPoints.Basic
15	import Mathlib.ModelTheory.Syntax
16	import Mathlib.Algebra.Order.BigOperators.Group.Finset
17	import Mathlib.Data.Fintype.Card
18	import Mathlib.SetTheory.Cardinal.Finite
19	import Lax366625.CountingProblems
20	import Lax366625.WitnessCounting
21	import Lax904597.Interpretations
22	import Lax904597.SecondOrder
23	import Lax366625.CountingClasses
24
25	/-!
26	---
27	title: Subtractive reductions
28	type: definition
29	---
30	A strong subtractive reduction from $C$ to $D$ , after Durand, Hermann, and
31	Kolaitis, presents $D$ as the witness count of a kernel and draws two
32	instances of $D$ from an instance $A$ of $C$ by two first-order
33	interpretations with the same tags and dimension, a subtrahend and a
34	minuend, such that every witness at the subtrahend is a witness at the
35	minuend and $C(A) + D(I_s(A)) = D(I_m(A))$ . Subtractive reducibility is a
36	finite chain of strong subtractive and relativized ordered parsimonious
37	steps. A counting problem is hard for a class when every member of the class
38	subtractively reduces to it, and complete when it is moreover a member.
39	-/
40
41	namespace Lax859101.SubtractiveReductions
42
43	open Lax366625.CountingProblems Lax366625.WitnessCounting Lax904597.Interpretations
44	open Lax904597.SecondOrder
45
46	open FirstOrder
47
48	open Language Structure
49
50	variable {L L' : Language.{0, 0}}
51
52	open FirstOrder
53
54	open Language Structure BoundedFormula
55
56	section LexFormulas
57
58	variable {L : Language.{0, 0}}
59
60	/-- `x = y`, as a formula over the ordered expansion. -/
61	def oEqF {α : Type} (x y : α) : (L.sum Language.order).Formula α :=
62	Term.equal (Term.var x) (Term.var y)
63
64	/-- `x ≤ y`, as a formula over the ordered expansion. -/
65	def oLeF {α : Type} (x y : α) : (L.sum Language.order).Formula α :=
66	Relations.formula₂ leSymb (Term.var x) (Term.var y)
67
68	/-- `x < y`, as a formula over the ordered expansion. -/
69	def oLtF {α : Type} (x y : α) : (L.sum Language.order).Formula α :=
70	oLeF x y ⊓ ∼(oEqF x y)
71
72	variable {A : Type} [L.Structure A] [LinearOrder A] {α : Type} {v : α → A}
73
74	variable (L) in
75	/-- Lexicographic comparison of two `d`-tuples (the two arguments of a binary
76	relation), as a formula over the ordered expansion. -/
77	noncomputable def lexTupleLeF (d : ℕ) : (L.sum Language.order).Formula (Fin 2 × Fin d) :=
78	(Formula.iInf fun i : Fin d => oEqF (0, i) (1, i)) ⊔
79	Formula.iSup fun j : Fin d =>
80	(Formula.iInf fun i : {i : Fin d // i < j} => oEqF (0, i.1) (1, i.1)) ⊓
81	oLtF (0, j) (1, j)
82
83	open Classical in
84	variable (L) in
85	/-- The full lexicographic comparison of tagged tuples, as a formula over the
86	ordered expansion: the tags are compared statically. -/
87	noncomputable def lexLeF {Tag : Type} [LinearOrder Tag] (d : ℕ) (t₁ t₂ : Tag) :
88	(L.sum Language.order).Formula (Fin 2 × Fin d) :=
89	if t₁ = t₂ then lexTupleLeF L d else if t₁ < t₂ then ⊤ else ⊥
90
91	end LexFormulas
92
93	section OrdExtend
94
95	variable {L₁ L₂ : Language.{0, 0}} [L₂.IsRelational]
96
97	variable {T : Type} [LinearOrder T] {d : ℕ}
98
99	/-- Extension of an interpretation over an ordered base to one whose target
100	carries the order vocabulary, interpreted by the lexicographic order on
101	tagged tuples. -/
102	noncomputable def FOInterpretation.ordExtend
103	(I : FOInterpretation (L₁.sum Language.order) L₂ T d) :
104	FOInterpretation (L₁.sum Language.order) (L₂.sum Language.order) T d where
105	relFormula {n} R :=
106	match n, R with
107	\| _, Sum.inl r => I.relFormula r
108	\| _, Sum.inr .le => fun t => lexLeF L₁ d (t 0) (t 1)
109
110	end OrdExtend
111
112	section WitAt
113
114	variable [L'.IsRelational] {Tag : Type} [LinearOrder Tag] {dim : ℕ}
115
116	/-- The assignment `ρ` is a witness of the kernel `φ` at the instance drawn by
117	the interpretation `I`, ordered lexicographically. The universe of that
118	instance is `Tag × A ^ dim` whatever `I` is, so the witnesses at two
119	interpretations with the same tags and dimension are comparable. -/
120	def FOInterpretation.WitAt (I : FOInterpretation (L.sum Language.order) L' Tag dim)
121	(B : SOBlock) (φ : ((L'.sum Language.order).sum B.lang).Sentence) (A : Type)
122	[L.Structure A] [LinearOrder A] (ρ : B.Assignment (Tag × (Fin dim → A))) : Prop :=
123	@Sentence.Realize ((L'.sum Language.order).sum B.lang) ((FOInterpretation.ordExtend I).Map A)
124	(@sumStructure (L'.sum Language.order) B.lang ((FOInterpretation.ordExtend I).Map A)
125	(FOInterpretation.mapStructure (FOInterpretation.ordExtend I) A)
126	(B.structure ρ)) φ
127
128	end WitAt
129
130	/-- A strong subtractive reduction: the target is presented as the witness
131	count of a kernel, two interpretations with the same tags and dimension draw a
132	subtrahend and a minuend, every witness at the first is a witness at the
133	second, and the count of the source is the difference of the two counts. -/
134	structure StrongSubtractiveReduction [L.IsRelational] [L'.IsRelational]
135	(C : CountingProblem L) (D : CountingProblem L') where
136	/-- The tags used by the two interpretations. -/
137	Tag : Type
138	/-- Tags are finite, so that finite structures map to finite structures. -/
139	[tagFinite : Finite Tag]
140	/-- Tags are nonempty, so that nonempty structures map to nonempty ones. -/
141	[tagNonempty : Nonempty Tag]
142	/-- Tags are linearly ordered: the order of the drawn instances is the
143	lexicographic one. -/
144	[tagOrder : LinearOrder Tag]
145	/-- The dimension of the two interpretations. -/
146	dim : ℕ
147	/-- The second-order block of the presentation of the target. -/
148	block : SOBlock
149	/-- The first-order kernel of the presentation of the target. -/
150	kernel : ((L'.sum Language.order).sum block.lang).Sentence
151	/-- The target counts the witnesses of its presentation, whatever the linear
152	order. -/
153	present : ∀ (A : Type) [L'.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
154	D A = witnessCount block kernel A
155	/-- The interpretation drawing the subtrahend. -/
156	subtrahend : FOInterpretation (L.sum Language.order) L' Tag dim
157	/-- The interpretation drawing the minuend. -/
158	minuend : FOInterpretation (L.sum Language.order) L' Tag dim
159	/-- Every witness at the subtrahend is a witness at the minuend. -/
160	witness_le : ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A]
161	(ρ : block.Assignment (Tag × (Fin dim → A))),
162	FOInterpretation.WitAt subtrahend block kernel A ρ →
163	FOInterpretation.WitAt minuend block kernel A ρ
164	/-- The count of the source and the count at the subtrahend add up to the
165	count at the minuend. -/
166	correct : ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
167	C A + D (subtrahend.Map A) = D (minuend.Map A)
168
169	/-- Subtractive reducibility, `C ≤ˢ D`: a finite chain of steps, each a
170	strong subtractive reduction or a relativized ordered parsimonious
171	reduction. -/
172	inductive SubtractiveReducible : ∀ {L L' : Language.{0, 0}} [L.IsRelational] [L'.IsRelational],
173	CountingProblem L → CountingProblem L' → Prop
174	/-- The empty chain. -/
175	\| refl {L : Language.{0, 0}} [L.IsRelational] (C : CountingProblem L) :
176	SubtractiveReducible C C
177	/-- A strong subtractive step, then a chain. -/
178	\| strong {L₁ L₂ L₃ : Language.{0, 0}} [L₁.IsRelational] [L₂.IsRelational]
179	[L₃.IsRelational] {C : CountingProblem L₁} {D : CountingProblem L₂}
180	{E : CountingProblem L₃} (f : StrongSubtractiveReduction C D)
181	(h : SubtractiveReducible D E) : SubtractiveReducible C E
182	/-- A parsimonious step, then a chain. -/
183	\| parsimonious {L₁ L₂ L₃ : Language.{0, 0}} [L₁.IsRelational] [L₂.IsRelational]
184	[L₃.IsRelational] {C : CountingProblem L₁} {D : CountingProblem L₂}
185	{E : CountingProblem L₃} (f : RelOrderedParsimoniousReduction C D)
186	(h : SubtractiveReducible D E) : SubtractiveReducible C E
187
188	open Lax366625.CountingProblems Lax366625.CountingClasses
189
190	/-- A counting problem is hard for a class when every problem of the class
191	reduces to it by a subtractive reduction. -/
192	def SubtractiveHard (K : CountingClass) {L : Language.{0, 0}} [L.IsRelational]
193	(C : CountingProblem L) : Prop :=
194	∀ {L'' : Language.{0, 0}} [L''.IsRelational] (D : CountingProblem L''),
195	K.Mem D → SubtractiveReducible D C
196
197	/-- A counting problem is complete for a class when it belongs to it and is
198	hard for it, under subtractive reductions. -/
199	def SubtractiveComplete (K : CountingClass) {L : Language.{0, 0}} [L.IsRelational]
200	(C : CountingProblem L) : Prop :=
201	K.Mem C ∧ SubtractiveHard K C
202
203	end Lax859101.SubtractiveReductions
204

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

Subtractive reductions

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments