Documentation

DescriptiveComplexity.EqPattern

Data read only through its equality pattern is first-order definable #

The keystone of every “write the program down as an interpretation” step, and the one a machine emitted rule by rule needs.

A transition table's attributes – when a rule applies, what state it moves to, what symbol it writes – are functions of its data, and an interpretation can only emit them if they are first-order. Asking each rule for a formula is one way; this file is the other, and the cheaper one:

a rule may read its data only through the equality pattern of that data – which coordinates hold the least element, which hold the greatest, and which two coordinates are equal – and any such reading is first-order definable, once and for all.

The pattern type DescriptiveComplexity.EqPat is finite, so a predicate that factors through it is the disjunction, over the finitely many patterns it admits, of the conjunction of equalities and disequalities that pins a pattern (DescriptiveComplexity.patSetF, DescriptiveComplexity.realize_patSetF_of_factors).

What it does and does not cover. The pattern is what a machine's own bookkeeping reads – flags, markers, which slot holds which designated element – and the whole write side of a rule, since everything a program stores is a copy, a designated element or a successor. It is not the whole guard language of a program that evaluates a logic: such a program eventually compares two of its slots in the order, or asks a relation of the source vocabulary of them, and neither is a function of the pattern. DescriptiveComplexity.Draw.UGDefinable therefore carries a formula, with the disjunction below as one way of building it.

Uniformity in the structure is the point. An interpretation carries one formula for every instance, so the factoring function must not depend on the structure: what a caller owes is a single Q : EqPat c → Prop and, for every A and every tuple, P w ↔ Q (patOf bot top w). That is a Prop about the attribute, provable where it is defined, rather than a syntax tree threaded through every abstraction the program is built from – which is what makes this affordable for a program assembled out of parameterized kits.

The two designated elements are the order's least and greatest, because those are the only elements an interpretation can name; DescriptiveComplexity.botF is Padding's and DescriptiveComplexity.topF is its mirror.

The pattern of a tuple #

@[reducible, inline]

abbrev DescriptiveComplexity.EqPat (c : ℕ) :

The equality pattern of a tuple, against two designated elements: which coordinates hold the first, which hold the second, and which two coordinates are equal. A plain product, so that it is finite and has decidable equality without ceremony.

Equations

DescriptiveComplexity.EqPat c = ((Fin c → Bool) × (Fin c → Bool) × (Fin c → Fin c → Bool))

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.patOf {A : Type} {c : ℕ} (bot top : A) (w : Fin c → A) :

The pattern a tuple has.

Equations

DescriptiveComplexity.patOf bot top w = (fun (i : Fin c) => decide (w i = bot), fun (i : Fin c) => decide (w i = top), fun (i j : Fin c) => decide (w i = w j))

Instances For

Dependency graph

theorem DescriptiveComplexity.patOf_fst {A : Type} {c : ℕ} {bot top : A} {w : Fin c → A} (i : Fin c) :

(patOf bot top w).1 i = true ↔ w i = bot

Dependency graph

theorem DescriptiveComplexity.patOf_snd {A : Type} {c : ℕ} {bot top : A} {w : Fin c → A} (i : Fin c) :

(patOf bot top w).2.1 i = true ↔ w i = top

Dependency graph

theorem DescriptiveComplexity.patOf_same {A : Type} {c : ℕ} {bot top : A} {w : Fin c → A} (i j : Fin c) :

(patOf bot top w).2.2 i j = true ↔ w i = w j

Dependency graph

The greatest element, as a formula #

DescriptiveComplexity.botF says a coordinate is a minimum; this is its mirror, and the two are the only elements an interpretation can name.

noncomputable def DescriptiveComplexity.topF {L : FirstOrder.Language} {γ : Type} (x : γ) :

(L.sum FirstOrder.Language.order).Formula γ

x is a maximum of the order, as a formula.

Equations

DescriptiveComplexity.topF x = FirstOrder.Language.Formula.iAlls (Fin 1) (FirstOrder.Language.leSymb.formula₂ (FirstOrder.Language.var (Sum.inr 0)) (FirstOrder.Language.var (Sum.inl x)))

Instances For

Dependency graph

theorem DescriptiveComplexity.realize_topF {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {x : γ} :

(topF x).Realize v ↔ IsTop (v x)

Dependency graph

The successor of an element #

The one thing a program writes that is neither a copy nor a designated element: a loop variable advanced. In a finite linear order the cover of a non-maximal element exists and is unique, so “the next element” is a total function, first-order definable and – what matters here – a function of a single coordinate, hence usable as the source of an output slot.

theorem DescriptiveComplexity.exists_covBy_of_not_isTop {A : Type} [LinearOrder A] [Finite A] {a : A} (h : ¬IsTop a) :

∃ (b : A), a ⋖ b

In a finite linear order, an element that is not a maximum is covered.

Dependency graph

theorem DescriptiveComplexity.covBy_unique {A : Type} [LinearOrder A] {a b b' : A} (h : a ⋖ b) (h' : a ⋖ b') :

b = b'

Covers are unique in a linear order.

Dependency graph

noncomputable def DescriptiveComplexity.ordSucc {A : Type} [Preorder A] (a : A) :

A

The next element: the cover, where there is one, and the element itself at the top – so that a loop variable at the end of its range simply stands still, which is what DescriptiveComplexity.Draw.tupNext does.

Equations

DescriptiveComplexity.ordSucc a = if h : ∃ (b : A), a ⋖ b then h.choose else a

Instances For

Dependency graph

theorem DescriptiveComplexity.covBy_ordSucc {A : Type} [Preorder A] {a : A} (h : ∃ (b : A), a ⋖ b) :

a ⋖ ordSucc a

Dependency graph

theorem DescriptiveComplexity.ordSucc_of_not_covBy {A : Type} [Preorder A] {a : A} (h : ¬∃ (b : A), a ⋖ b) :

Dependency graph

theorem DescriptiveComplexity.eq_ordSucc_of_covBy {A : Type} [LinearOrder A] {a b : A} (h : a ⋖ b) :

The cover is the next element.

Dependency graph

The formula of a pattern #

noncomputable def DescriptiveComplexity.covByF {L : FirstOrder.Language} {γ : Type} (x y : γ) :

(L.sum FirstOrder.Language.order).Formula γ

x is covered by y, as a formula: below it, and nothing strictly between.

Equations

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

Instances For

Dependency graph

def DescriptiveComplexity.litF {L : FirstOrder.Language} {γ : Type} (b : Bool) (φ : (L.sum FirstOrder.Language.order).Formula γ) :

(L.sum FirstOrder.Language.order).Formula γ

A literal: a formula or its negation, by a bit.

Equations

DescriptiveComplexity.litF b φ = if b = true then φ else FirstOrder.Language.BoundedFormula.not φ

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.patF {L : FirstOrder.Language} {γ : Type} {c : ℕ} (p : EqPat c) (x : Fin c → γ) :

(L.sum FirstOrder.Language.order).Formula γ

A pattern, as a formula: each coordinate is or is not the least element, is or is not the greatest, and each pair of coordinates is or is not equal – one literal per decision the pattern records.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.patSetF {L : FirstOrder.Language} {γ : Type} {c : ℕ} (Q : EqPat c → Prop) (x : Fin c → γ) :

(L.sum FirstOrder.Language.order).Formula γ

A predicate on patterns, as a formula: the disjunction of the patterns it admits, which is a finite disjunction because the pattern type is.

Equations

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

Instances For

Dependency graph

Having a pattern #

def DescriptiveComplexity.HasPat {A : Type} {c : ℕ} (bot top : A) (p : EqPat c) (w : Fin c → A) :

A tuple has a pattern: the three families of decisions, read as conditions on the tuple.

Equations

DescriptiveComplexity.HasPat bot top p w = ((∀ (i : Fin c), w i = bot ↔ p.1 i = true) ∧ (∀ (i : Fin c), w i = top ↔ p.2.1 i = true) ∧ ∀ (i j : Fin c), w i = w j ↔ p.2.2 i j = true)

Instances For

Dependency graph

theorem DescriptiveComplexity.hasPat_patOf {A : Type} {c : ℕ} (bot top : A) (w : Fin c → A) :

HasPat bot top (patOf bot top w) w

Every tuple has the pattern it is read off.

Dependency graph

theorem DescriptiveComplexity.eq_patOf_of_hasPat {A : Type} {c : ℕ} {bot top : A} {p : EqPat c} {w : Fin c → A} (h : HasPat bot top p w) :

p = patOf bot top w

And it has only that one.

Dependency graph

Their realization #

theorem DescriptiveComplexity.realize_litF {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {b : Bool} {φ : (L.sum FirstOrder.Language.order).Formula γ} :

(litF b φ).Realize v ↔ (φ.Realize v ↔ b = true)

Dependency graph

theorem DescriptiveComplexity.realize_covByF {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {x y : γ} :

(covByF x y).Realize v ↔ v x ⋖ v y

Dependency graph

theorem DescriptiveComplexity.realize_patF {L : FirstOrder.Language} {γ : Type} {c : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {bot top : A} (hb : IsBot bot) (ht : IsTop top) (p : EqPat c) (x : Fin c → γ) :

(patF p x).Realize v ↔ HasPat bot top p fun (i : Fin c) => v (x i)

A pattern's formula holds exactly of the tuples that have it.

Dependency graph

theorem DescriptiveComplexity.realize_patSetF {L : FirstOrder.Language} {γ : Type} {c : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {bot top : A} (hb : IsBot bot) (ht : IsTop top) (Q : EqPat c → Prop) (x : Fin c → γ) :

(patSetF Q x).Realize v ↔ Q (patOf bot top fun (i : Fin c) => v (x i))

A predicate on patterns is defined by its disjunction.

Dependency graph

Writing a tuple, slot by slot #

The other half of what a machine's rules do: a rule not only fires on its data, it also writes. Everything the EXPSPACE program writes is a copy of one of its input slots or one of the two designated elements, chosen by the input's pattern – so one more builder finishes the toolbox.

inductive DescriptiveComplexity.SlotVal (c : ℕ) :

Where an output slot's value comes from: a slot of the input, one of the two designated elements, or the next element after a slot of the input – which is what a loop variable being advanced needs, and the only source that reads the order.

copy {c : ℕ} : Fin c → SlotVal c
Copy this coordinate of the input.
bot {c : ℕ} : SlotVal c
The clear element.
top {c : ℕ} : SlotVal c
The set element.
succ {c : ℕ} : Fin c → SlotVal c
The element after this coordinate of the input.

Instances For

Dependency graph

def DescriptiveComplexity.instDecidableEqSlotVal.decEq {c✝ : ℕ} (x✝ x✝¹ : SlotVal c✝) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqSlotVal {c✝ : ℕ} :

DecidableEq (SlotVal c✝)

Equations

DescriptiveComplexity.instDecidableEqSlotVal = DescriptiveComplexity.instDecidableEqSlotVal.decEq

Dependency graph

noncomputable def DescriptiveComplexity.SlotVal.eval {A : Type} {c : ℕ} [LinearOrder A] (bot top : A) (w : Fin c → A) :

SlotVal c → A

What a source names, at a tuple.

Equations

DescriptiveComplexity.SlotVal.eval bot top w (DescriptiveComplexity.SlotVal.copy k) = w k
DescriptiveComplexity.SlotVal.eval bot top w DescriptiveComplexity.SlotVal.bot = bot
DescriptiveComplexity.SlotVal.eval bot top w DescriptiveComplexity.SlotVal.top = top
DescriptiveComplexity.SlotVal.eval bot top w (DescriptiveComplexity.SlotVal.succ k) = DescriptiveComplexity.ordSucc (w k)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.slotValF {L : FirstOrder.Language} {γ : Type} {c : ℕ} (u : Fin c → γ) (y : γ) :

SlotVal c → (L.sum FirstOrder.Language.order).Formula γ

A slot's source, as a formula: the target variable is that coordinate of the input, or a minimum, or a maximum.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.slotValF u y (DescriptiveComplexity.SlotVal.copy k) = (FirstOrder.Language.var y).equal (FirstOrder.Language.var (u k))
DescriptiveComplexity.slotValF u y DescriptiveComplexity.SlotVal.bot = DescriptiveComplexity.botF y
DescriptiveComplexity.slotValF u y DescriptiveComplexity.SlotVal.top = DescriptiveComplexity.topF y

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.writeTupF {L : FirstOrder.Language} {γ : Type} {c : ℕ} (G : EqPat c → Fin c → SlotVal c) (u y : Fin c → γ) :

(L.sum FirstOrder.Language.order).Formula γ

A tuple written slot by slot from another, as a formula: for the pattern the input has, each output coordinate is what that pattern's source names. A disjunction over the patterns, as everything here is.

Equations

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

Instances For

Dependency graph

theorem DescriptiveComplexity.realize_slotValF {L : FirstOrder.Language} {γ : Type} {c : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {bot top : A} [Finite A] (hb : IsBot bot) (ht : IsTop top) (u : Fin c → γ) (y : γ) (sv : SlotVal c) :

(slotValF u y sv).Realize v ↔ v y = SlotVal.eval bot top (fun (k : Fin c) => v (u k)) sv

Dependency graph

theorem DescriptiveComplexity.realize_patSetF_of_factors {L : FirstOrder.Language} {γ : Type} {c : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {bot top : A} (hb : IsBot bot) (ht : IsTop top) {P : (Fin c → A) → Prop} {Q : EqPat c → Prop} (hP : ∀ (w : Fin c → A), P w ↔ Q (patOf bot top w)) (x : Fin c → γ) :

(patSetF Q x).Realize v ↔ P fun (i : Fin c) => v (x i)

A predicate that reads its data only through the equality pattern is first-order definable, by one formula for every structure – which is what an interpretation needs, since it carries one formula for all of them. This is what a transition table's guard has to offer, and what a program assembled out of parameterized kits can afford to offer: a Prop about the attribute where it is defined, rather than syntax threaded through every abstraction.

Dependency graph