Documentation

DescriptiveComplexity.Problems.Wide.Instance

A wide machine that accepts #

The three wide problems fold their promises into their yes-instances, and a membership theorem about a vacuous problem would say nothing. This file closes that gap by exhibiting one instance, the smallest there is, and proving all three problems hold of it:

two elements – one that is both a start state and an accepting state, one that is the blank – no transitions at all, and the order they come in.

Its machine starts on the empty address in an accepting state, so it accepts in no steps; having no transitions it is deterministic, so the deterministic space-bounded problem holds of it too. Nothing about addresses is used beyond DescriptiveComplexity.isInit_wide – the head starts on the empty address and the tape is blank – which is the point: the promises reduce to conditions on the instance (DescriptiveComplexity.wideData_wellFormed_iff, DescriptiveComplexity.wideData_deterministic_iff) and those conditions are satisfiable.

The instance is also the smallest exercise of the interface a hardness reduction will use, so it is worth reading as a template: a FirstOrder.Language.wide structure is eleven relations on a finite type, and the two promises are then four conditions and four more.

@[instance_reducible]

instance DescriptiveComplexity.WideSmoke.structure₂ :

FirstOrder.Language.wide.Structure (Fin 2)

The smallest wide-machine instance: 0 is a start state and an accepting state, 1 is the blank, there are no transitions, and wmLe is the order of Fin 2.

Equations

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

Dependency graph

@[simp]

theorem DescriptiveComplexity.WideSmoke.wmLe_iff (a b : Fin 2) :

WMLe a b ↔ a ≤ b

Dependency graph

@[simp]

theorem DescriptiveComplexity.WideSmoke.wmTr_iff (a : Fin 2) :

WMTr a ↔ False

Dependency graph

@[simp]

theorem DescriptiveComplexity.WideSmoke.wmStart_iff (a : Fin 2) :

WMStart a ↔ a = 0

Dependency graph

@[simp]

theorem DescriptiveComplexity.WideSmoke.wmAcc_iff (a : Fin 2) :

WMAcc a ↔ a = 0

Dependency graph

@[simp]

theorem DescriptiveComplexity.WideSmoke.wmBlank_iff (a : Fin 2) :

WMBlank a ↔ a = 1

Dependency graph

@[simp]

theorem DescriptiveComplexity.WideSmoke.wmInp_iff (a b : Fin 2) :

WMInp a b ↔ False

Dependency graph

@[simp]

theorem DescriptiveComplexity.WideSmoke.wmDst_iff (a b : Fin 2) :

WMDst a b ↔ False

Dependency graph

@[simp]

theorem DescriptiveComplexity.WideSmoke.wmWrite_iff (a b : Fin 2) :

WMWrite a b ↔ False

Dependency graph

The three problems are not vacuous #

theorem DescriptiveComplexity.wideAccept_nonvacuous :

WideAccept.Holds (Fin 2)

DescriptiveComplexity.WideAccept has a yes-instance, so the membership DescriptiveComplexity.wideAccept_mem_NEXPTIME is not about an empty problem. Registered in the Lax archive as Lax822549.WideMachinesComplete.wideAccept_nonvacuous.

Dependency graph

theorem DescriptiveComplexity.wideAcceptSpace_nonvacuous :

WideAcceptSpace.Holds (Fin 2)

DescriptiveComplexity.WideAcceptSpace has a yes-instance. Registered in the Lax archive as Lax822549.WideMachinesComplete.wideAcceptSpace_nonvacuous.

Dependency graph

theorem DescriptiveComplexity.dwideAcceptSpace_nonvacuous :

DWideAcceptSpace.Holds (Fin 2)

DescriptiveComplexity.DWideAcceptSpace has a yes-instance: the instance has no transitions, so it is deterministic. Registered in the Lax archive as Lax822549.WideMachinesComplete.dwideAcceptSpace_nonvacuous.

Dependency graph