First-order reductions are computable

The last step of the bridge that does not need a machine: a first-order interpretation induces a computable map of concrete structures, so ¬ComputablePred transfers backwards along every reduction notion of the library – ≤ᶠᵒ, ≤ᶠᵒ[≤] and ≤ʳᶠᵒ[≤].

Everything is proved for the most general notion, the relativized ordered reduction; the other two are special cases of it (DescriptiveComplexity.FOReduction.toOrdered, DescriptiveComplexity.OrderedFOReduction.toRel).

What has to be computed

Three things, in this order.

• The order. An ordered reduction reads its input over L.sum Language.order. The universe of a concrete instance is Fin (n + 1), which is already linearly ordered, so the ordered expansion is built by appending one row to the table (DescriptiveComplexity.ordStruct) – there is no order to choose and none to encode.
• The renumbering. The target universe of a relativized interpretation is the subtype of Tag × (Fin dim → A) cut out by the domain formula, so the surviving points have to be listed (DescriptiveComplexity.goodList) and re-indexed into an initial segment of ℕ. This is where the Primrec work concentrates, exactly as the design predicted.
• The tags. A defining formula depends on the tags of its arguments, which are known only at run time. There are finitely many tag tuples, so the row of a target symbol evaluates all |Tag|ⁿ fixed formulas and selects by an index computed from the decoded tags.

The defining formulas have free variables indexed by Fin n × Fin dim, while the evaluator of DescriptiveComplexity.Computability.Eval is written for sentences; DescriptiveComplexity.flatFormula flattens the former into the latter through Fin.finProdFinEquiv and FirstOrder.Language.BoundedFormula.relabel.

The ordered expansion of an instance, as data

def DescriptiveComplexity.orderVocab : FirstOrder.Language.order.FinVocab

The one-symbol vocabulary of the order, presented.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.rowsOf {L : FirstOrder.Language} (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) : List (List Bool)

The rows of the table of an instance, cut to exactly one row per symbol. Appending anything to a raw table could otherwise be read as the row of a symbol whose row was missing.

Equations

• DescriptiveComplexity.rowsOf V s = List.map (fun (k : ℕ) => s.table.getD k []) (List.range V.numSyms)

theorem DescriptiveComplexity.getD_rowsOf {L : FirstOrder.Language} (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) {k : ℕ} (hk : k < V.numSyms) : (rowsOf V s).getD k [] = s.table.getD k []

@[simp]

theorem DescriptiveComplexity.length_rowsOf {L : FirstOrder.Language} (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) : (rowsOf V s).length = V.numSyms

def DescriptiveComplexity.ordStruct {L : FirstOrder.Language} (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) : FirstOrder.Language.FinStruct (V.sum orderVocab)

The ordered expansion of an instance, as data: the same universe, the same rows, and one more row for the order of Fin (n + 1).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DescriptiveComplexity.univSize_ordStruct {L : FirstOrder.Language} (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) : (ordStruct V s).univSize = s.univSize

@[simp]

theorem DescriptiveComplexity.card_ordStruct {L : FirstOrder.Language} (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) : (ordStruct V s).card = s.card

theorem DescriptiveComplexity.relMapBool_ordStruct_inl {L : FirstOrder.Language} (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) {n : ℕ} (r : L.Relations n) (x : Fin n → (ordStruct V s).Univ) : (ordStruct V s).relMapBool (Sum.inl r) x = s.relMapBool r x

theorem DescriptiveComplexity.relMapBool_ordStruct_le {L : FirstOrder.Language} (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) (x : Fin 2 → (ordStruct V s).Univ) : (ordStruct V s).relMapBool (Sum.inr FirstOrder.Language.orderRel.le) x = decide (x 0 ≤ x 1)

def DescriptiveComplexity.ordIso {L : FirstOrder.Language} [L.IsRelational] (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) : (L.sum FirstOrder.Language.order).Equiv (ordStruct V s).Univ s.Univ

The data is the ordered expansion: the identity is an isomorphism from the encoded ordered expansion to the instance's universe with its own linear order.

Equations

• DescriptiveComplexity.ordIso V s = { toEquiv := Equiv.refl (DescriptiveComplexity.ordStruct V s).Univ, map_fun' := ⋯, map_rel' := ⋯ }

theorem DescriptiveComplexity.primrec_ordStruct {L : FirstOrder.Language} (V : L.FinVocab) : Primrec fun (s : FirstOrder.Language.FinStruct V) => ordStruct V s

Numbering the tagged tuples

A point of the target universe of an interpretation is a tag together with a dim-tuple of elements of the instance. It is numbered by putting the tag in the units digit, base |Tag|, and the tuple above it.

def DescriptiveComplexity.ptIdx {L : FirstOrder.Language} {V : L.FinVocab} {Tag : Type} {dim : ℕ} (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (s : FirstOrder.Language.FinStruct V) (p : Tag × (Fin dim → s.Univ)) : ℕ

The number of a tagged tuple.

Equations

• DescriptiveComplexity.ptIdx T tagEq s p = ↑(tagEq.symm p.1) + (T + 1) * FirstOrder.Language.tupleIdx s.card (List.ofFn fun (j : Fin dim) => ↑(p.2 j))

def DescriptiveComplexity.ptOfIdx {L : FirstOrder.Language} {V : L.FinVocab} {Tag : Type} (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (dim : ℕ) (s : FirstOrder.Language.FinStruct V) (u : ℕ) : Tag × (Fin dim → s.Univ)

The tagged tuple with a given number.

Equations

• DescriptiveComplexity.ptOfIdx T tagEq dim s u = (tagEq ⟨u % (T + 1), ⋯⟩, fun (j : Fin dim) => ⟨FirstOrder.Language.digitAt s.card (u / (T + 1)) ↑j, ⋯⟩)

theorem DescriptiveComplexity.ptIdx_lt {L : FirstOrder.Language} {V : L.FinVocab} {Tag : Type} {dim : ℕ} (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (s : FirstOrder.Language.FinStruct V) (p : Tag × (Fin dim → s.Univ)) : ptIdx T tagEq s p < (T + 1) * s.card ^ dim

theorem DescriptiveComplexity.ptOfIdx_ptIdx {L : FirstOrder.Language} {V : L.FinVocab} {Tag : Type} {dim : ℕ} (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (s : FirstOrder.Language.FinStruct V) (p : Tag × (Fin dim → s.Univ)) : ptOfIdx T tagEq dim s (ptIdx T tagEq s p) = p

theorem DescriptiveComplexity.ptIdx_ptOfIdx {L : FirstOrder.Language} {V : L.FinVocab} {Tag : Type} {dim : ℕ} (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (s : FirstOrder.Language.FinStruct V) {u : ℕ} (hu : u < (T + 1) * s.card ^ dim) : ptIdx T tagEq s (ptOfIdx T tagEq dim s u) = u

Flattening the defining formulas

The evaluator of DescriptiveComplexity.Computability.Eval is written for formulas with no free variables, while a defining formula has free variables indexed by Fin n × Fin dim and a domain formula by Fin dim. Both are relabelled into bound variables, the pairs through finProdFinEquiv.

def DescriptiveComplexity.flatRel {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) {n : ℕ} (R : L'.Relations n) (τ : Fin n → Tag) : (L.sum FirstOrder.Language.order).BoundedFormula Empty (n * dim)

A defining formula, with its free variables turned into bound ones.

Equations

• DescriptiveComplexity.flatRel I R τ = FirstOrder.Language.BoundedFormula.relabel Sum.inr (FirstOrder.Language.Formula.relabel (⇑finProdFinEquiv) (I.relFormula R τ))

def DescriptiveComplexity.flatDom {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (t : Tag) : (L.sum FirstOrder.Language.order).BoundedFormula Empty dim

A domain formula, with its free variables turned into bound ones.

Equations

• DescriptiveComplexity.flatDom I t = FirstOrder.Language.BoundedFormula.relabel Sum.inr (I.domFormula t)

theorem DescriptiveComplexity.realize_flatRel {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) {M : Type} [(L.sum FirstOrder.Language.order).Structure M] {n : ℕ} (R : L'.Relations n) (τ : Fin n → Tag) (v : Empty → M) (x : Fin (n * dim) → M) : (flatRel I R τ).Realize v x ↔ (I.relFormula R τ).Realize (x ∘ ⇑finProdFinEquiv)

theorem DescriptiveComplexity.realize_flatDom {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) {M : Type} [(L.sum FirstOrder.Language.order).Structure M] (t : Tag) (v : Empty → M) (x : Fin dim → M) : (flatDom I t).Realize v x ↔ (I.domFormula t).Realize x

Evaluating the defining formulas at numbered points

theorem DescriptiveComplexity.evalBF_ord_iff {L : FirstOrder.Language} [L.IsRelational] (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) {l : ℕ} (φ : (L.sum FirstOrder.Language.order).BoundedFormula Empty l) (xs : List ℕ) (h : xs.length = l) : FirstOrder.Language.FinStruct.evalBF (V.sum orderVocab) φ (ordStruct V s) xs = true ↔ φ.Realize Empty.elim fun (i : Fin l) => (ordStruct V s).valOf xs ↑i

Evaluating a formula on the encoded ordered expansion is realizing it on the instance's universe with its own linear order.

theorem DescriptiveComplexity.valOf_ofFn_digitAt {L : FirstOrder.Language} (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) {d : ℕ} (v : ℕ) (i : Fin d) : (ordStruct V s).valOf (List.ofFn fun (j : Fin d) => FirstOrder.Language.digitAt s.card v ↑j) ↑i = ⟨FirstOrder.Language.digitAt s.card v ↑i, ⋯⟩

The valuation read off a list of digits is the tuple those digits are.

def DescriptiveComplexity.domBool {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) (u : ℕ) : Bool

Does the point numbered u survive the domain formula? The tag is only known at run time, so all |Tag| domain formulas are evaluated and the right one is selected.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.domBool_iff {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) (u : ℕ) : domBool I T tagEq V s u = true ↔ (I.domFormula (ptOfIdx T tagEq dim s u).1).Realize (ptOfIdx T tagEq dim s u).2

def DescriptiveComplexity.relBool {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) {n : ℕ} (R : L'.Relations n) (p : List ℕ) : Bool

The value of a defining formula at a tuple of numbered points. The tags are only known at run time, so all |Tag|ⁿ instances of the formula are evaluated and the right one is selected.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.valOf_ofFn_pair {L : FirstOrder.Language} {dim : ℕ} (T : ℕ) (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) {n : ℕ} (p : List ℕ) (q : Fin n × Fin dim) : (ordStruct V s).valOf (List.ofFn fun (q' : Fin (n * dim)) => FirstOrder.Language.digitAt s.card (p.getD (↑(finProdFinEquiv.symm q').1) 0 / (T + 1)) ↑(finProdFinEquiv.symm q').2) ↑(finProdFinEquiv q) = ⟨FirstOrder.Language.digitAt s.card (p.getD (↑q.1) 0 / (T + 1)) ↑q.2, ⋯⟩

The valuation read off the pair-indexed list of digits.

theorem DescriptiveComplexity.relBool_iff {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) {n : ℕ} (R : L'.Relations n) (p : List ℕ) : relBool I T tagEq V s R p = true ↔ (I.relFormula R fun (i : Fin n) => (ptOfIdx T tagEq dim s (p.getD (↑i) 0)).1).Realize fun (q : Fin n × Fin dim) => (ptOfIdx T tagEq dim s (p.getD (↑q.1) 0)).2 q.2

The surviving points, and the image instance

def DescriptiveComplexity.goodList {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) : List ℕ

The numbers of the points that survive the domain formula, in increasing order: the renumbering of the target universe is the position in this list.

Equations

• DescriptiveComplexity.goodList I T tagEq V s = List.filter (DescriptiveComplexity.domBool I T tagEq V s) (List.range ((T + 1) * s.card ^ dim))

theorem DescriptiveComplexity.mem_goodList {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) (u : ℕ) : u ∈ goodList I T tagEq V s ↔ u < (T + 1) * s.card ^ dim ∧ domBool I T tagEq V s u = true

theorem DescriptiveComplexity.nodup_goodList {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) : (goodList I T tagEq V s).Nodup

theorem DescriptiveComplexity.getD_goodList_mem {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) (s : FirstOrder.Language.FinStruct V) {j : ℕ} (hj : j < (goodList I T tagEq V s).length) : (goodList I T tagEq V s).getD j 0 ∈ goodList I T tagEq V s

noncomputable def DescriptiveComplexity.mapStruct {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) (V' : L'.FinVocab) (s : FirstOrder.Language.FinStruct V) : FirstOrder.Language.FinStruct V'

The image of an instance under a relativized interpretation, as data. The universe is the list of surviving points, renumbered by position; a relation holds of a tuple exactly when the defining formula does of the points it names.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DescriptiveComplexity.card_mapStruct {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) (V' : L'.FinVocab) (s : FirstOrder.Language.FinStruct V) : (mapStruct I T tagEq V V' s).card = (goodList I T tagEq V s).length - 1 + 1

theorem DescriptiveComplexity.relMapBool_mapStruct {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) (V' : L'.FinVocab) (s : FirstOrder.Language.FinStruct V) {a : ℕ} (R' : L'.Relations a) (x : Fin a → (mapStruct I T tagEq V V' s).Univ) : (mapStruct I T tagEq V V' s).relMapBool R' x = relBool I T tagEq V s R' (List.ofFn fun (j : Fin a) => (goodList I T tagEq V s).getD (↑(x j)) 0)

Everything above is primitive recursive

theorem DescriptiveComplexity.filter_eq_flatMap (p : ℕ → Bool) (l : List ℕ) : List.filter p l = List.flatMap (fun (a : ℕ) => bif p a then [a] else []) l

theorem DescriptiveComplexity.primrec_domBool {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) : Primrec fun (q : FirstOrder.Language.FinStruct V × ℕ) => domBool I T tagEq V q.1 q.2

theorem DescriptiveComplexity.primrec_relBool {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) {n : ℕ} (R : L'.Relations n) : Primrec fun (q : FirstOrder.Language.FinStruct V × List ℕ) => relBool I T tagEq V q.1 R q.2

theorem DescriptiveComplexity.primrec_goodList {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) : Primrec fun (s : FirstOrder.Language.FinStruct V) => goodList I T tagEq V s

theorem DescriptiveComplexity.primrec_mapStruct {L L' : FirstOrder.Language} [L.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) (V' : L'.FinVocab) : Primrec fun (s : FirstOrder.Language.FinStruct V) => mapStruct I T tagEq V V' s

The data is the image structure

theorem DescriptiveComplexity.getD_ofFn_nat {a : ℕ} (g : Fin a → ℕ) (i : Fin a) : (List.ofFn g).getD (↑i) 0 = g i

noncomputable def DescriptiveComplexity.mapIso {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {Tag : Type} {dim : ℕ} (I : RelFOInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (T : ℕ) (tagEq : Fin (T + 1) ≃ Tag) (V : L.FinVocab) (V' : L'.FinVocab) (s : FirstOrder.Language.FinStruct V) (hne : 0 < (goodList I T tagEq V s).length) : L'.Equiv (mapStruct I T tagEq V V' s).Univ (I.MapRel s.Univ)

The renumbering is an isomorphism: the encoded image of an instance is the relativized interpretation of that instance.

Equations

• One or more equations did not get rendered due to their size.

Decidability transfers along reductions

theorem DescriptiveComplexity.computablePred_of_relOrderedReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : RelOrderedFOReduction P Q) (V : L.FinVocab) (V' : L'.FinVocab) (hQ : ComputablePred (Q.toPred V')) : ComputablePred (P.toPred V)

A relativized ordered reduction is a computable many-one reduction of the induced sets of concrete instances: if the target is decidable, so is the source.

The renumbering forced by the definable domain is the whole content; the interpretation itself is an evaluation of fixed formulas, primitive recursive by FirstOrder.Language.FinStruct.primrec_evalBF.

theorem DescriptiveComplexity.not_computablePred_of_relOrderedReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : RelOrderedFOReduction P Q) (V : L.FinVocab) (V' : L'.FinVocab) (hP : ¬ComputablePred (P.toPred V)) : ¬ComputablePred (Q.toPred V')

¬ComputablePred transfers backwards along a relativized ordered reduction.

theorem DescriptiveComplexity.not_computablePred_of_orderedReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : OrderedFOReduction P Q) (V : L.FinVocab) (V' : L'.FinVocab) (hP : ¬ComputablePred (P.toPred V)) : ¬ComputablePred (Q.toPred V')

The same for an ordered reduction.

theorem DescriptiveComplexity.not_computablePred_of_foReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : FOReduction P Q) (V : L.FinVocab) (V' : L'.FinVocab) (hP : ¬ComputablePred (P.toPred V)) : ¬ComputablePred (Q.toPred V')

The same for a plain first-order reduction.