Documentation

DescriptiveComplexity.Problems.Machine.Interp

The transcription: `SAT ≤ᶠᵒ[≤] NTMAccept` #

The first-order half of the reduction. The machine of a CNF formula was built semantically in DescriptiveComplexity.Problems.Machine.Hardness – plain predicates on tagged tuples, with its correctness DescriptiveComplexity.satMachine_accepts_iff_satisfiable proved there. This file writes the defining formulas of an interpretation of Language.turing in ordered CNF instances, shows each formula realizes exactly the corresponding predicate of the machine, and bundles the result as the ordered first-order reduction DescriptiveComplexity.SatTM.sat_ordered_fo_reduction_ntmAccept.

Method #

Everything is arranged so that no simp call ever faces a tag match:

the binary symbols' formulas are written through two shape helpers – cstF s (“the second argument is the constant element pinned to the minima”) and oneF s x (“the second argument carries the tag s and the payload held by the variable x”) – matching the two shapes DescriptiveComplexity.cst and DescriptiveComplexity.one every state, symbol and transition of the machine has; each has one realization lemma, so each defining formula needs a match on its first tag only;
realization lemmas take the valuation abstractly, with the values of the needed variables as equation hypotheses; at the call sites these are discharged by rfl, since the interpreted valuation reduces definitionally on concrete tags.

The transfer to DescriptiveComplexity.NTMAccept is then a fieldwise DescriptiveComplexity.TMData.Agree along the identity equivalence: the machine the interpreted structure describes agrees with DescriptiveComplexity.satMachine, so acceptance and well-formedness transport, and correctness is inherited from the semantic layer.

Formulas for the clause order #

noncomputable def DescriptiveComplexity.SatTM.minClF {α : Type} (c : α) :

SatOcc.satOrd.Formula α

c is the lowest clause, as a formula.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.maxClF {α : Type} (c : α) :

SatOcc.satOrd.Formula α

c is the highest clause, as a formula.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.nextClF {α : Type} (c c' : α) :

SatOcc.satOrd.Formula α

c' is the clause immediately above c, as a formula.

Equations

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

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.noClF {α : Type} :

SatOcc.satOrd.Formula α

There is no clause at all, as a formula.

Equations

DescriptiveComplexity.SatTM.noClF = FirstOrder.Language.Formula.iAlls Unit (FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.SatOcc.clF (Sum.inr ())))

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.varF {α : Type} (x : α) :

SatOcc.satOrd.Formula α

x is a variable of the instance – it occurs in some clause –, as a formula.

Equations

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

Instances For

Dependency graph

The two shapes of the machine's elements, as formulas #

noncomputable def DescriptiveComplexity.SatTM.cstF (s t' : SatTag) :

SatOcc.satOrd.Formula (Fin 2 × Fin 2)

The second argument of a binary symbol is the constant element cst s: its tag is s – checked statically – and its payload is the pair of minima.

Equations

DescriptiveComplexity.SatTM.cstF s t' = if t' = s then DescriptiveComplexity.minF (1, 0) ⊓ DescriptiveComplexity.minF (1, 1) else ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.oneF (s : SatTag) (x : Fin 2 × Fin 2) (t' : SatTag) :

SatOcc.satOrd.Formula (Fin 2 × Fin 2)

The second argument of a binary symbol is one s (v x): its tag is s, its payload carries the value of the variable x and the minimum.

Equations

DescriptiveComplexity.SatTM.oneF s x t' = if t' = s then DescriptiveComplexity.SatOcc.eqF (1, 0) x ⊓ DescriptiveComplexity.minF (1, 1) else ⊥

Instances For

Dependency graph

The defining formulas #

noncomputable def DescriptiveComplexity.SatTM.chkLitF (b : Bool) :

SatOcc.satOrd.Formula (Fin 2 × Fin 2)

The literal test on the source structure, for the statically known truth value v: this is where the transition relation reads the input formula.

Equations

DescriptiveComplexity.SatTM.chkLitF b = if b = true then DescriptiveComplexity.SatOcc.posF (0, 0) (0, 1) else DescriptiveComplexity.SatOcc.negF (0, 0) (0, 1)

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.posnF :

SatTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for posn.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.trF :

SatTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for tr: the payload promises of DescriptiveComplexity.SatTr.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.startF :

SatTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for start.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.accF :

SatTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for acc: any payload – acceptance is read off the tag alone, exactly as DescriptiveComplexity.SatAcc does.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.blankF :

SatTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for blank.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.rightF :

SatTag → SatOcc.satOrd.Formula (Fin 1 × Fin 2)

Defining formula for right: a static condition on the tag.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.inpF :

SatTag → SatTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for inp, the initial tape.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.tsrcF :

SatTag → SatTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for tsrc.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.treadF :

SatTag → SatTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for tread.

Equations

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.tdstF :

SatTag → SatTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for tdst: the one place the instance is consulted, in the check clause, through DescriptiveComplexity.SatTM.chkLitF.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.SatTM.tdstF DescriptiveComplexity.SatTag.tGuessStart x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.qGuess x✝
DescriptiveComplexity.SatTM.tdstF (DescriptiveComplexity.SatTag.tGuessVal b) x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.qGuess x✝
DescriptiveComplexity.SatTM.tdstF DescriptiveComplexity.SatTag.tGuessEndAcc x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.qAcc x✝
DescriptiveComplexity.SatTM.tdstF DescriptiveComplexity.SatTag.tGuessEndChk x✝ = DescriptiveComplexity.SatTM.oneF (DescriptiveComplexity.SatTag.qChk false false) (0, 0) x✝
DescriptiveComplexity.SatTM.tdstF (DescriptiveComplexity.SatTag.tTurnNext d) x✝ = DescriptiveComplexity.SatTM.oneF (DescriptiveComplexity.SatTag.qChk false !d) (0, 1) x✝
DescriptiveComplexity.SatTM.tdstF (DescriptiveComplexity.SatTag.tTurnAcc d) x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.qAcc x✝
DescriptiveComplexity.SatTM.tdstF x✝¹ x✝ = ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.twriteF :

SatTag → SatTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

Defining formula for twrite.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.SatTM.twriteF DescriptiveComplexity.SatTag.tGuessStart x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.sStart x✝
DescriptiveComplexity.SatTM.twriteF DescriptiveComplexity.SatTag.tGuessEndAcc x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.sEnd x✝
DescriptiveComplexity.SatTM.twriteF DescriptiveComplexity.SatTag.tGuessEndChk x✝ = DescriptiveComplexity.SatTM.cstF DescriptiveComplexity.SatTag.sEnd x✝
DescriptiveComplexity.SatTM.twriteF x✝¹ x✝ = ⊥

Instances For

Dependency graph

noncomputable def DescriptiveComplexity.SatTM.satTuringInterp :

FOInterpretation SatOcc.satOrd FirstOrder.Language.turing SatTag 2

The interpretation of machine instances in ordered CNF instances. The order is DescriptiveComplexity.lexLeF, so its linearity comes from DescriptiveComplexity.tagTupleOrder with no tag-pair analysis; every other symbol matches on its first tag only, the shape of the second being delegated to DescriptiveComplexity.SatTM.cstF and DescriptiveComplexity.SatTM.oneF.

Equations

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

Instances For

Dependency graph

The realization lemmas #

One per symbol of Language.turing, each saying its defining formula defines the corresponding predicate of DescriptiveComplexity.satMachine. The universe of the interpreted structure is definitionally DescriptiveComplexity.SatV A; DescriptiveComplexity.SatTM.satMapEquiv names the identity equivalence, along which the machines will be shown to agree.

def DescriptiveComplexity.SatTM.satMapEquiv {A : Type} :

SatV A ≃ satTuringInterp.Map A

The identity equivalence between the tagged tuples and the interpreted universe.

Equations

DescriptiveComplexity.SatTM.satMapEquiv = Equiv.refl (DescriptiveComplexity.SatV A)

Instances For

Dependency graph

theorem DescriptiveComplexity.SatTM.relMap_posn {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : SatV A) :

TMPosn (satMapEquiv p) ↔ SatPosn p

Dependency graph

theorem DescriptiveComplexity.SatTM.relMap_tr {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : SatV A) :

TMTr (satMapEquiv p) ↔ SatTr p

Dependency graph

theorem DescriptiveComplexity.SatTM.relMap_start {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : SatV A) :

TMStart (satMapEquiv p) ↔ SatStart p

Dependency graph

theorem DescriptiveComplexity.SatTM.relMap_acc {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : SatV A) :

TMAcc (satMapEquiv p) ↔ SatAcc p

Dependency graph

theorem DescriptiveComplexity.SatTM.relMap_blank {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : SatV A) :

TMBlank (satMapEquiv p) ↔ SatBlank p

Dependency graph

theorem DescriptiveComplexity.SatTM.relMap_right {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : SatV A) :

TMRight (satMapEquiv p) ↔ SatRight p

Dependency graph

theorem DescriptiveComplexity.SatTM.relMap_le {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p q : SatV A) :

TMLe (satMapEquiv p) (satMapEquiv q) ↔ tagTupleLe p q

Dependency graph

theorem DescriptiveComplexity.SatTM.satInp_pCell_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {w : Fin 2 → A} {a : SatV A} :

SatInp (SatTag.pCell , w) a ↔ a = one SatTag.sU (w 0)

Dependency graph

theorem DescriptiveComplexity.SatTM.satInp_pEnd_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {w : Fin 2 → A} {a : SatV A} :

SatInp (SatTag.pEnd , w) a ↔ a = symEnd

Dependency graph

The machines agree, and the reduction #