Documentation

DescriptiveComplexity.OrderedReorder

Replacing the order of an ordered structure by a definable one #

An ordered reduction is correct for every linear order of its input, which it has no say over. What it may do is replace that order, before anything else, by any linear order it can define: DescriptiveComplexity.FOInterpretation.reorder is the one-dimensional interpretation of the ordered expansion in itself that keeps every symbol and interprets the order symbol by a given formula, and DescriptiveComplexity.FOInterpretation.reorderLEquiv says that, when the formula defines a linear order ord' of the structure, the interpreted structure is the input structure ordered by ord'.

This is how a reduction into a problem that reads its output in the order of the universe – the tape order of DescriptiveComplexity.DTMNumber – can be composed after one that produces the order of significance as a relation of the instance: the second reduction reorders its input so that the two agree.

source
noncomputable def DescriptiveComplexity.FOInterpretation.reorder {L : FirstOrder.Language} (φ : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin 1)) :
FOInterpretation (L.sum FirstOrder.Language.order) (L.sum FirstOrder.Language.order) Unit 1

Reordering: the identity interpretation of the ordered expansion in itself, with the order symbol interpreted by the formula φ (its two free variables being the two arguments).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    noncomputable def DescriptiveComplexity.FOInterpretation.reorderLEquiv {L : FirstOrder.Language} [L.IsRelational] (φ : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin 1)) (A : Type) [L.Structure A] [LinearOrder A] {Le' : A → A → Prop} (h : IsLinOrd Le') (hφ : ∀ (v : Fin 2 × Fin 1 → A), φ.Realize v ↔ Le' (v (0, 0)) (v (1, 0))) :
    (L.sum FirstOrder.Language.order).Equiv ((reorder φ).Map A) A

    When φ defines a relation Le' that is a linear order, the reordered structure is the input structure ordered by Le' (DescriptiveComplexity.IsLinOrd.toLinearOrder). The new order is passed as a relation rather than as a LinearOrder so that it does not shadow the order of the input in the statement.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Dependency graph