Transitive closures with parameters, as relations a formula may read

DescriptiveComplexity.TCSpec defines a sentence: a walk on tuples, and the question whether an accepting node is reachable from a starting one. A reduction needs more than that – its defining formulas have free variables, so what they may consult is a relation, not an answer. This file provides it: a DescriptiveComplexity.ParamTCSpec is a walk whose step formula may mention par parameters besides its two tuples, and the relation it defines is reachability itself,

R[m,m'](x̄, ȳ, z̄) – “from the node (m, x̄) the node (m', ȳ) is reachable, the parameters being z̄” –

one relation per ordered pair of modes. A finite family of such walks (DescriptiveComplexity.TCFamily) is a block of relation variables (DescriptiveComplexity.TCFamily.block) whose assignment is fixed, not guessed: DescriptiveComplexity.TCFamily.reachAssign. A structure expanded by it is what the formulas of an FO(TC) reduction are read over (DescriptiveComplexity.TransitiveClosureReduction).

Reachability is an inflationary induction

The theorem of this file is DescriptiveComplexity.TCFamily.inflLimit_toStepDef: the reachability relations of a family are the value of one simultaneous inflationary induction (DescriptiveComplexity.TCFamily.toStepDef), namely the rules

• R[m,m](x̄, x̄, z̄), and
• R[m,m'](x̄, ȳ, z̄) ← R[m,m''](x̄, ȳ', z̄) ∧ step[m'',m'](ȳ', ȳ, z̄).

They are positive in the relation variables, so the inflationary iteration computes the least fixed point, which is Relation.ReflTransGen of the step – the mode pairs being static, each rule is one step formula, and no clausal apparatus is needed.

That theorem is what makes an FO(TC) reduction an FO(LFP) reduction, and so what gives the FO(TC) reductions their closure properties without a second development. It is also the honest statement of where FO(TC) sits: a walk is a fixed point of a very restricted shape.

Reading an FO(TC) sentence off the relations

DescriptiveComplexity.TCSpec.acceptsF turns any existing DescriptiveComplexity.TCSpec into a formula over the expansion by its own reachability relations: “some accepting node is reachable from some starting node”, with the walk itself now an atom rather than an operator (DescriptiveComplexity.TCSpec.realize_acceptsF). Every FO(TC) definable property is thereby available to an FO(TC) reduction as a formula, which is how DescriptiveComplexity.EVEN enters DescriptiveComplexity.TCReduction.

Walks with parameters

structure DescriptiveComplexity.ParamTCSpec (L : FirstOrder.Language) : Type 1

A parameterized transitive-closure specification: a walk on k-tuples carrying a finite mode, whose step formula may mention par parameters beside the current and the next tuple. Unlike DescriptiveComplexity.TCSpec it has no src/tgt formulas: what it defines is the reachability relation, and where a sentence is wanted the endpoints are supplied by the formula that reads it.

The vocabulary is a parameter, not the ordered expansion: the ordered reading is the instance L := L₀.sum Language.order, as for DescriptiveComplexity.StepDef.

• Mode : Type

  The modes: the finite control the walk carries beside its tuple.

• modeFinite : Finite self.Mode

  Modes are finite.

• k : ℕ

  The walk runs on k-tuples of elements.

• par : ℕ

  The number of parameters the step formula may mention.

• step : self.Mode → self.Mode → L.Formula ((Fin self.k ⊕ Fin self.k) ⊕ Fin self.par)

  The step formula, one per pair of modes: the current tuple, the next tuple, then the parameters.

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.Node {L : FirstOrder.Language} (s : ParamTCSpec L) (A : Type) : Type

A node of the walk: a mode together with a k-tuple.

Equations

• s.Node A = (s.Mode × (Fin s.k → A))

def DescriptiveComplexity.ParamTCSpec.StepAt {L : FirstOrder.Language} (s : ParamTCSpec L) {A : Type} [L.Structure A] (z : Fin s.par → A) (a b : s.Node A) : Prop

One step of the walk, at a valuation of the parameters.

Equations

• s.StepAt z a b = (s.step a.1 b.1).Realize (Sum.elim (Sum.elim a.2 b.2) z)

@[reducible, inline]

abbrev DescriptiveComplexity.ParamTCSpec.ReachAt {L : FirstOrder.Language} (s : ParamTCSpec L) {A : Type} [L.Structure A] (z : Fin s.par → A) : s.Node A → s.Node A → Prop

Reachability in the walk, at a valuation of the parameters.

Equations

• s.ReachAt z = Relation.ReflTransGen (s.StepAt z)

Packing a tuple, two endpoints and the parameters

def DescriptiveComplexity.ParamTCSpec.leftIx {L : FirstOrder.Language} (s : ParamTCSpec L) (i : Fin s.k) : Fin (s.k + s.k + s.par)

The position of the i-th coordinate of the first tuple.

Equations

• s.leftIx i = ⟨↑i, ⋯⟩

def DescriptiveComplexity.ParamTCSpec.rightIx {L : FirstOrder.Language} (s : ParamTCSpec L) (i : Fin s.k) : Fin (s.k + s.k + s.par)

The position of the i-th coordinate of the second tuple.

Equations

• s.rightIx i = ⟨s.k + ↑i, ⋯⟩

def DescriptiveComplexity.ParamTCSpec.parIx {L : FirstOrder.Language} (s : ParamTCSpec L) (j : Fin s.par) : Fin (s.k + s.k + s.par)

The position of the j-th parameter.

Equations

• s.parIx j = ⟨s.k + s.k + ↑j, ⋯⟩

def DescriptiveComplexity.ParamTCSpec.pack {L : FirstOrder.Language} {s : ParamTCSpec L} {V : Type} (x y : Fin s.k → V) (z : Fin s.par → V) : Fin (s.k + s.k + s.par) → V

The tuple assembled from two endpoints and a valuation of the parameters.

Equations

• DescriptiveComplexity.ParamTCSpec.pack x y z j = if h : ↑j < s.k then x ⟨↑j, h⟩ else if h2 : ↑j < s.k + s.k then y ⟨↑j - s.k, ⋯⟩ else z ⟨↑j - (s.k + s.k), ⋯⟩

@[simp]

theorem DescriptiveComplexity.ParamTCSpec.pack_left {L : FirstOrder.Language} {s : ParamTCSpec L} {V : Type} (x y : Fin s.k → V) (z : Fin s.par → V) (i : Fin s.k) : pack x y z (s.leftIx i) = x i

@[simp]

theorem DescriptiveComplexity.ParamTCSpec.pack_right {L : FirstOrder.Language} {s : ParamTCSpec L} {V : Type} (x y : Fin s.k → V) (z : Fin s.par → V) (i : Fin s.k) : pack x y z (s.rightIx i) = y i

@[simp]

theorem DescriptiveComplexity.ParamTCSpec.pack_par {L : FirstOrder.Language} {s : ParamTCSpec L} {V : Type} (x y : Fin s.k → V) (z : Fin s.par → V) (j : Fin s.par) : pack x y z (s.parIx j) = z j

theorem DescriptiveComplexity.ParamTCSpec.pack_eta {L : FirstOrder.Language} {s : ParamTCSpec L} {V : Type} (w : Fin (s.k + s.k + s.par) → V) : (pack (fun (i : Fin s.k) => w (s.leftIx i)) (fun (i : Fin s.k) => w (s.rightIx i)) fun (j : Fin s.par) => w (s.parIx j)) = w

Every tuple is packed from its three parts.

theorem DescriptiveComplexity.ParamTCSpec.pack_comp {L : FirstOrder.Language} {s : ParamTCSpec L} {V W : Type} (f : V → W) (x y : Fin s.k → V) (z : Fin s.par → V) : (fun (j : Fin (s.k + s.k + s.par)) => f (pack x y z j)) = pack (fun (t : Fin s.k) => f (x t)) (fun (t : Fin s.k) => f (y t)) fun (t : Fin s.par) => f (z t)

Post-composing a packed tuple with a function packs the components.

A family of walks, as a block of relation variables

structure DescriptiveComplexity.TCFamily (L : FirstOrder.Language) : Type 1

A finite family of parameterized walks. Its relation variables – one per walk and ordered pair of that walk's modes – are what an FO(TC) reduction's formulas may read.

• Ix : Type

  The index type of the family.

• ixFinite : Finite self.Ix

  The family is finite.

• spec : self.Ix → ParamTCSpec L

  The walk of each index.

def DescriptiveComplexity.TCFamily.block {L : FirstOrder.Language} (F : TCFamily L) : SOBlock

The block of relation variables of a family: one variable per walk and ordered pair of modes, of arity “two tuples and the parameters”.

Equations

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

def DescriptiveComplexity.TCFamily.reachAssign {L : FirstOrder.Language} (F : TCFamily L) (A : Type) [L.Structure A] : F.block.Assignment A

The assignment the block has, as opposed to one a second-order quantifier would guess: each variable holds the reachability relation of its walk, at the parameters read off the tuple.

Equations

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

theorem DescriptiveComplexity.TCFamily.reachAssign_iff {L : FirstOrder.Language} {F : TCFamily L} {A : Type} [L.Structure A] (q : F.block.ι) (w : Fin (F.block.arity q) → A) : F.reachAssign A q w ↔ (F.spec q.fst).ReachAt (fun (t : Fin (F.spec q.fst).par) => w ((F.spec q.fst).parIx t)) (q.snd.1, fun (t : Fin (F.spec q.fst).k) => w ((F.spec q.fst).leftIx t)) (q.snd.2, fun (t : Fin (F.spec q.fst).k) => w ((F.spec q.fst).rightIx t))

The reachability assignment, unfolded at a tuple.

theorem DescriptiveComplexity.TCFamily.reachAssign_pack {L : FirstOrder.Language} {F : TCFamily L} {A : Type} [L.Structure A] (q : F.block.ι) (x y : Fin (F.spec q.fst).k → A) (z : Fin (F.spec q.fst).par → A) : F.reachAssign A q (ParamTCSpec.pack x y z) ↔ (F.spec q.fst).ReachAt z (q.snd.1, x) (q.snd.2, y)

The induction that computes reachability

noncomputable def DescriptiveComplexity.TCFamily.diagF {L : FirstOrder.Language} (F : TCFamily L) (q : F.block.ι) : (L.sum F.block.lang).Formula (Fin (F.block.arity q))

The reflexivity rule, as a formula: the two tuples agree – and the two modes, which is decided statically.

Equations

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

noncomputable def DescriptiveComplexity.TCFamily.reachAtomF {L : FirstOrder.Language} (F : TCFamily L) (q : F.block.ι) (m : (F.spec q.fst).Mode) : (L.sum F.block.lang).Formula (Fin (F.block.arity q) ⊕ Fin (F.spec q.fst).k)

The atom “the first tuple reaches the freshly quantified one, in mode m”.

Equations

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

noncomputable def DescriptiveComplexity.TCFamily.lastStepF {L : FirstOrder.Language} (F : TCFamily L) (q : F.block.ι) (m : (F.spec q.fst).Mode) : (L.sum F.block.lang).Formula (Fin (F.block.arity q) ⊕ Fin (F.spec q.fst).k)

The last step of the walk: from the freshly quantified tuple, in mode m, to the second tuple, in the variable's second mode.

Equations

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

noncomputable def DescriptiveComplexity.TCFamily.stepF {L : FirstOrder.Language} (F : TCFamily L) (q : F.block.ι) : (L.sum F.block.lang).Formula (Fin (F.block.arity q))

The step formula of a relation variable: reflexivity, or one more step after a shorter walk. Both disjuncts are positive in the relation variables, so the inflationary iteration computes the least fixed point.

Equations

• F.stepF q = F.diagF q ⊔ FirstOrder.Language.Formula.iExs (Fin (F.spec q.fst).k) (FirstOrder.Language.Formula.iSup fun (m : (F.spec q.fst).Mode) => F.reachAtomF q m ⊓ F.lastStepF q m)

noncomputable def DescriptiveComplexity.TCFamily.toStepDef {L : FirstOrder.Language} (F : TCFamily L) : StepDef L

The induction of a family: one simultaneous inflationary induction whose relation variables are the family's, and whose value is its reachability relations (DescriptiveComplexity.TCFamily.inflLimit_toStepDef). Its output sentence is never read.

Equations

• F.toStepDef = { B := F.block, step := F.stepF, out := ⊤ }

Realization of the step formulas

theorem DescriptiveComplexity.TCFamily.realize_diagF {L : FirstOrder.Language} {F : TCFamily L} {A : Type} [L.Structure A] (ρ : F.block.Assignment A) (q : F.block.ι) (w : Fin (F.block.arity q) → A) : (F.diagF q).Realize w ↔ q.snd.1 = q.snd.2 ∧ ∀ (t : Fin (F.spec q.fst).k), w ((F.spec q.fst).leftIx t) = w ((F.spec q.fst).rightIx t)

theorem DescriptiveComplexity.TCFamily.realize_reachAtomF {L : FirstOrder.Language} {F : TCFamily L} {A : Type} [L.Structure A] (ρ : F.block.Assignment A) (q : F.block.ι) (m : (F.spec q.fst).Mode) (w : Fin (F.block.arity q) → A) (y : Fin (F.spec q.fst).k → A) : (F.reachAtomF q m).Realize (Sum.elim w y) ↔ ρ ⟨q.fst, (q.snd.1, m)⟩ (ParamTCSpec.pack (fun (t : Fin (F.spec ⟨q.fst, (q.snd.1, m)⟩.fst).k) => w ((F.spec q.fst).leftIx t)) y fun (t : Fin (F.spec ⟨q.fst, (q.snd.1, m)⟩.fst).par) => w ((F.spec q.fst).parIx t))

theorem DescriptiveComplexity.TCFamily.realize_lastStepF {L : FirstOrder.Language} {F : TCFamily L} {A : Type} [L.Structure A] (ρ : F.block.Assignment A) (q : F.block.ι) (m : (F.spec q.fst).Mode) (w : Fin (F.block.arity q) → A) (y : Fin (F.spec q.fst).k → A) : (F.lastStepF q m).Realize (Sum.elim w y) ↔ (F.spec q.fst).StepAt (fun (t : Fin (F.spec q.fst).par) => w ((F.spec q.fst).parIx t)) (m, y) (q.snd.2, fun (t : Fin (F.spec q.fst).k) => w ((F.spec q.fst).rightIx t))

theorem DescriptiveComplexity.TCFamily.realize_stepF {L : FirstOrder.Language} {F : TCFamily L} {A : Type} [L.Structure A] (ρ : F.block.Assignment A) (q : F.block.ι) (w : Fin (F.block.arity q) → A) : (F.stepF q).Realize w ↔ (q.snd.1 = q.snd.2 ∧ ∀ (t : Fin (F.spec q.fst).k), w ((F.spec q.fst).leftIx t) = w ((F.spec q.fst).rightIx t)) ∨ ∃ (y : Fin (F.spec q.fst).k → A) (m : (F.spec q.fst).Mode), ρ ⟨q.fst, (q.snd.1, m)⟩ (ParamTCSpec.pack (fun (t : Fin (F.spec ⟨q.fst, (q.snd.1, m)⟩.fst).k) => w ((F.spec q.fst).leftIx t)) y fun (t : Fin (F.spec ⟨q.fst, (q.snd.1, m)⟩.fst).par) => w ((F.spec q.fst).parIx t)) ∧ (F.spec q.fst).StepAt (fun (t : Fin (F.spec q.fst).par) => w ((F.spec q.fst).parIx t)) (m, y) (q.snd.2, fun (t : Fin (F.spec q.fst).k) => w ((F.spec q.fst).rightIx t))

The value of the induction is the reachability relations

theorem DescriptiveComplexity.TCFamily.inflLimit_toStepDef {L : FirstOrder.Language} {F : TCFamily L} {A : Type} [L.Structure A] [Finite A] : F.toStepDef.inflLimit A = F.reachAssign A

Reachability is an inflationary induction: the value of DescriptiveComplexity.TCFamily.toStepDef is the family's reachability relations.

An FO(TC) sentence, as a formula over the reachability relations

@[reducible]

noncomputable def DescriptiveComplexity.TCSpec.toParam {L₀ : FirstOrder.Language} (spec : TCSpec L₀) : ParamTCSpec (L₀.sum FirstOrder.Language.order)

A DescriptiveComplexity.TCSpec read as a parameterized walk with no parameters, over the ordered expansion its formulas already live in.

Reducible, so that the modes and the arity of the reading are those of the specification transparently – a node of one is a node of the other.

Equations

• spec.toParam = { Mode := spec.Mode, modeFinite := ⋯, k := spec.k, par := 0, step := fun (m m' : spec.Mode) => FirstOrder.Language.Formula.relabel Sum.inl (spec.step m m') }

@[reducible]

noncomputable def DescriptiveComplexity.TCSpec.toFamily {L₀ : FirstOrder.Language} (spec : TCSpec L₀) : TCFamily (L₀.sum FirstOrder.Language.order)

The one-element family of walks of a DescriptiveComplexity.TCSpec.

Equations

• spec.toFamily = { Ix := Unit, ixFinite := ⋯, spec := fun (x : Unit) => spec.toParam }

theorem DescriptiveComplexity.TCSpec.stepAt_toParam {L₀ : FirstOrder.Language} (spec : TCSpec L₀) {A : Type} [L₀.Structure A] [LinearOrder A] (z : Fin 0 → A) (a b : spec.Node A) : spec.toParam.StepAt z a b ↔ spec.Step a b

theorem DescriptiveComplexity.TCSpec.reachAt_toParam {L₀ : FirstOrder.Language} (spec : TCSpec L₀) {A : Type} [L₀.Structure A] [LinearOrder A] (z : Fin 0 → A) (a b : spec.Node A) : spec.toParam.ReachAt z a b ↔ spec.Reach a b

noncomputable def DescriptiveComplexity.TCSpec.reachAtomAcc {L₀ : FirstOrder.Language} (spec : TCSpec L₀) (p : spec.Mode × spec.Mode) : ((L₀.sum FirstOrder.Language.order).sum spec.toFamily.block.lang).Formula (Empty ⊕ Fin spec.k ⊕ Fin spec.k)

The reachability atom of the walk, with both endpoints quantified.

Equations

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

theorem DescriptiveComplexity.TCSpec.realize_reachAtomAcc {L₀ : FirstOrder.Language} (spec : TCSpec L₀) {A : Type} [L₀.Structure A] [LinearOrder A] (p : spec.Mode × spec.Mode) (v : Empty ⊕ Fin spec.k ⊕ Fin spec.k → A) : (spec.reachAtomAcc p).Realize v ↔ spec.Reach (p.1, fun (t : Fin spec.k) => v (Sum.inr (Sum.inl t))) (p.2, fun (t : Fin spec.k) => v (Sum.inr (Sum.inr t)))

noncomputable def DescriptiveComplexity.TCSpec.acceptsF {L₀ : FirstOrder.Language} (spec : TCSpec L₀) : ((L₀.sum FirstOrder.Language.order).sum spec.toFamily.block.lang).Sentence

The walk as an atom: “some accepting node is reachable from some starting node”, written over the vocabulary expanded by the walk's own reachability relations. This is what makes every FO(TC) definable property available to an FO(TC) reduction.

Equations

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

theorem DescriptiveComplexity.TCSpec.realize_acceptsF {L₀ : FirstOrder.Language} (spec : TCSpec L₀) {A : Type} [L₀.Structure A] [LinearOrder A] : A ⊨ spec.acceptsF ↔ spec.Accepts A

The walk-as-an-atom formula says acceptance, when the relation variables hold the reachability relations they are meant to.