Documentation

DescriptiveComplexity.Problems.Wide.DrawOrd

The order the reduction puts on the points #

DescriptiveComplexity.PFPDefinable quantifies over every linear order on the expanded universe, so the EXPSPACE reduction may choose the one its machine can compare: the pullback of the binary block-value order along the encoding (DescriptiveComplexity.Draw.encOrder). An order atom on two points is then exactly the comparison of their encodings in the machine's own reading – DescriptiveComplexity.WMSetLe at the lexicographic order on tuples, the order the register file walks – which is DescriptiveComplexity.Draw.encOrder_le_iff.

The junction between the two languages for orders on block values – the address layer's DescriptiveComplexity.WMSetLe tupLeLex and the library's DescriptiveComplexity.setLinearOrder – is DescriptiveComplexity.Draw.wmSetLe_iff_setLe: both say at the most significant differing tuple, the second contains it, with most significant = lexicographically least.

(The library's canonical order on the expanded universe, DescriptiveComplexity.ExpExpansion.mapLinearOrder, orders by tag first and padded atoms second; nothing here conflicts with it – the reduction simply instantiates the definition's order quantifier differently.)

The two readings of the binary order on block values #

source
theorem DescriptiveComplexity.Draw.wmSetLe_iff_setLe {dd : ℕ} {A : Type} [LinearOrder A] [Finite A] (S T : (Fin dd → A) → Prop) :
WMSetLe tupLeLex S T ↔ S ≤ T

The two readings of the binary order on block values agree: the address layer's DescriptiveComplexity.WMSetLe at the lexicographic tuple order is the library's DescriptiveComplexity.setLinearOrder on subsets of the Lex tuples.

Dependency graph

The pulled-back order on the points #

source
@[instance_reducible]
noncomputable def DescriptiveComplexity.Draw.encOrder {L : FirstOrder.Language} {X : ExpExpansion L} {dd : ℕ} (ly : EncLayout (PtCode X) (blockArityBound X.B) dd) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (zero one : A) (hne : zero ≠ one) :
LinearOrder (X.Map A)

The order the reduction puts on the expanded universe: the pullback of the binary block-value order along the encoding. An order atom on two points is then the comparison of their encodings, which the machine can run on its register file.

Equations
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.Draw.encOrder_le_iff {L : FirstOrder.Language} {X : ExpExpansion L} {dd : ℕ} (ly : EncLayout (PtCode X) (blockArityBound X.B) dd) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] (zero one : A) (hne : zero ≠ one) (m m' : X.Map A) :
    m ≤ m' ↔ WMSetLe tupLeLex (encMap ly zero one m) (encMap ly zero one m')

    What the chosen order says: the machine's own comparison of the two encodings.

    Dependency graph