Post-processing terms and one-call reductions

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

definition

Loading review…

Natural Language Statement

Definition

A polynomial term over $L$ denotes a number computed from an ordered $L$ -structure: a numeral, the number of elements of a definable relation, a sum, or a product. A post-processing term also uses the answer of an oracle, powers of two with a polynomial exponent, and the operations $+$ , $\times$ , truncated subtraction, division, and remainder of natural numbers.

A one-call reduction from $C$ to $D$ is a relativized ordered first-order interpretation $I$ , nonempty on nonempty structures, and a post-processing term $t$ such that $C(A) = t(A, D(I(A)))$ for every nonempty finite structure $A$ and every linear order on it: a restricted form of the metric reductions of Krentel, in the statement of Faliszewski and Hemaspaandra. A counting problem is in the one-call closure of a class when it reduces with one call to a member of the class, one-call hard when every member reduces to it with one call, and one-call complete when both hold. The closure, rather than the class, is the right notion: as Toda and Watanabe showed, #P is presumably not closed under such reductions.

Concept map

6 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.SetTheory.Cardinal.Finite
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.Tactic.FinCases
9	import Mathlib.Logic.Equiv.Fin.Basic
10	import Mathlib.Data.Fintype.Lattice
11	import Mathlib.Data.Finite.Sigma
12	import Mathlib.Order.Lattice.Nat
13	import Mathlib.Data.Set.Card
14	import Mathlib.Data.Fintype.Pigeonhole
15	import Mathlib.Dynamics.FixedPoints.Basic
16	import Mathlib.ModelTheory.Syntax
17	import Mathlib.Algebra.Order.BigOperators.Group.Finset
18	import Mathlib.Data.Fintype.Card
19	import Lax366625.CountingProblems
20	import Lax904597.Relativized
21	import Lax366625.CountingClasses
22
23	/-!
24	---
25	title: Post-processing terms and one-call reductions
26	type: definition
27	---
28	A polynomial term over $L$ denotes a number computed from an ordered
29	$L$ -structure: a numeral, the number of elements of a definable relation, a
30	sum, or a product. A post-processing term also uses the answer of an oracle,
31	powers of two with a polynomial exponent, and the operations $+$ , $\times$ ,
32	truncated subtraction, division, and remainder of natural numbers.
33
34	A one-call reduction from $C$ to $D$ is a relativized ordered first-order
35	interpretation $I$ , nonempty on nonempty structures, and a post-processing
36	term $t$ such that $C(A) = t(A, D(I(A)))$ for every nonempty finite
37	structure $A$ and every linear order on it: a restricted form of the metric
38	reductions of Krentel, in the statement of Faliszewski and Hemaspaandra. A
39	counting problem is in the one-call closure of a class when it reduces with
40	one call to a member of the class, one-call hard when every member reduces
41	to it with one call, and one-call complete when both hold. The closure,
42	rather than the class, is the right notion: as Toda and Watanabe showed, #P
43	is presumably not closed under such reductions.
44	-/
45
46	namespace Lax859101.OneCallReductions
47
48	open Lax366625.CountingProblems Lax904597.Relativized
49
50	open FirstOrder
51
52	open Language Structure
53
54	/-- Terms denoting numbers polynomial in the size of the instance: numerals,
55	definable cardinalities, sums and products. -/
56	inductive PolyTerm (L : Language.{0, 0}) : Type 1
57	/-- A numeral. -/
58	\| num (k : ℕ) : PolyTerm L
59	/-- The number of tagged tuples satisfying their tag's domain formula, i.e.,
60	the size of the universe of a relativized interpretation. -/
61	\| card {Tag : Type} [Finite Tag] {dim : ℕ}
62	(J : RelFOInterpretation (L.sum Language.order) Language.empty Tag dim) : PolyTerm L
63	/-- A sum. -/
64	\| add (p q : PolyTerm L) : PolyTerm L
65	/-- A product. -/
66	\| mul (p q : PolyTerm L) : PolyTerm L
67
68	namespace PolyTerm
69
70	variable {L L₁ L₂ : Language.{0, 0}}
71
72	/-- The value of a polynomial term at an ordered structure. -/
73	noncomputable def eval (A : Type) [L.Structure A] [LinearOrder A] : PolyTerm L → ℕ
74	\| num k => k
75	\| card J => Nat.card (J.MapRel A)
76	\| add p q => p.eval A + q.eval A
77	\| mul p q => p.eval A * q.eval A
78
79	end PolyTerm
80
81	/-- The arithmetic applied to the answer of an oracle call: polynomial terms,
82	powers of two with a polynomial exponent, and the operations `+`, `*`,
83	truncated `-`, `/` and `%` of the natural numbers. -/
84	inductive PostTerm (L : Language.{0, 0}) : Type 1
85	/-- The answer of the oracle. -/
86	\| oracle : PostTerm L
87	/-- A polynomial term. -/
88	\| poly (p : PolyTerm L) : PostTerm L
89	/-- Two to the power of a polynomial term. -/
90	\| pow2 (p : PolyTerm L) : PostTerm L
91	/-- A sum. -/
92	\| add (s t : PostTerm L) : PostTerm L
93	/-- A product. -/
94	\| mul (s t : PostTerm L) : PostTerm L
95	/-- A truncated difference. -/
96	\| sub (s t : PostTerm L) : PostTerm L
97	/-- A quotient. -/
98	\| div (s t : PostTerm L) : PostTerm L
99	/-- A remainder. -/
100	\| mod (s t : PostTerm L) : PostTerm L
101
102	namespace PostTerm
103
104	variable {L L₁ L₂ : Language.{0, 0}}
105
106	/-- The value of a post-processing term at an ordered structure, given the
107	answer `c` of the oracle. -/
108	noncomputable def eval (A : Type) [L.Structure A] [LinearOrder A] (c : ℕ) : PostTerm L → ℕ
109	\| oracle => c
110	\| poly p => p.eval A
111	\| pow2 p => 2 ^ p.eval A
112	\| add s t => s.eval A c + t.eval A c
113	\| mul s t => s.eval A c * t.eval A c
114	\| sub s t => s.eval A c - t.eval A c
115	\| div s t => s.eval A c / t.eval A c
116	\| mod s t => s.eval A c % t.eval A c
117
118	end PostTerm
119
120	open FirstOrder
121
122	open Language Structure
123
124	variable {L L' : Language.{0, 0}}
125
126	/-- A one-call counting reduction: a relativized ordered interpretation and a
127	post-processing term recovering the count of the source from the count of the
128	interpreted instance. -/
129	structure OneCallReduction [L.IsRelational] [L'.IsRelational]
130	(C : CountingProblem L) (D : CountingProblem L') where
131	/-- The tags used by the underlying interpretation. -/
132	Tag : Type
133	/-- Tags are finite, so that finite structures map to finite structures. -/
134	[tagFinite : Finite Tag]
135	/-- The dimension of the underlying interpretation. -/
136	dim : ℕ
137	/-- The underlying relativized interpretation, over the ordered expansion. -/
138	toRelInterpretation : RelFOInterpretation (L.sum Language.order) L' Tag dim
139	/-- The definable domain is inhabited. -/
140	dom_nonempty : ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
141	∃ (t : Tag) (w : Fin dim → A), (toRelInterpretation.domFormula t).Realize w
142	/-- The arithmetic applied to the answer of the oracle. -/
143	post : PostTerm L
144	/-- The count of the source is the post-processed count of the interpreted
145	instance, whatever the linear order. -/
146	correct : ∀ (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A],
147	C A = post.eval A (D (toRelInterpretation.MapRel A))
148
149	open Lax366625.CountingProblems Lax366625.CountingClasses
150
151	/-- A counting problem is in the one-call closure of a class when it reduces
152	with one call to a problem of the class. -/
153	def OneCallMem (K : CountingClass) {L : Language.{0, 0}} [L.IsRelational] (C : CountingProblem L) :
154	Prop :=
155	∃ (L'' : Language.{0, 0}) (_ : L''.IsRelational) (D : CountingProblem L''),
156	K.Mem D ∧ Nonempty (OneCallReduction C D)
157
158	/-- A counting problem is one-call hard for a class when every problem of the
159	class reduces to it with one call. -/
160	def OneCallHard (K : CountingClass) {L : Language.{0, 0}} [L.IsRelational] (C : CountingProblem L) :
161	Prop :=
162	∀ {L'' : Language.{0, 0}} [L''.IsRelational] (D : CountingProblem L''),
163	K.Mem D → Nonempty (OneCallReduction D C)
164
165	/-- A counting problem is one-call complete for a class when it is in the
166	one-call closure of the class and one-call hard for it. -/
167	def OneCallComplete (K : CountingClass) {L : Language.{0, 0}} [L.IsRelational]
168	(C : CountingProblem L) : Prop :=
169	OneCallMem K C ∧ OneCallHard K C
170
171	end Lax859101.OneCallReductions
172

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

Post-processing terms and one-call reductions

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments