The wide machine with a register channel

DescriptiveComplexity.WideAccept writes the input symbol of an element x at the address {y | y ≤ x}, the initial segment x cuts. The order on addresses reads the least element as the most significant digit, so that address is above 2 ^ (n − 1) whatever x is: the input lies on a geometric ruler in the top half of the tape. A machine with space to spare walks there as often as it likes, and the EXPSPACE build does; a machine on a clock can go there once and never return, and it cannot lay a file of its own either (DescriptiveComplexity.Problems.Wide.Limits).

This file adds a second problem – it changes nothing, and both existing completeness theorems stand – whose channel writes the input of x at the segment x cuts among the elements the channel writes for:

wmRegSeg x = {y | y ≤ x ∧ y carries an input symbol}.

Two properties, and they are exactly the two a register file has to have.

• It is monotone: below a greater element the file has strictly more, and what it gains is greater than everything the two share, so the address grows (wmSetLt_wmRegSeg). The whole walk, mirror and increment layer is stated for a file whose registers grow with the elements they stand for, so it applies here unchanged – which is what the singleton channel {x} would not give: its cells shrink as the elements grow.
• It is low: every cell is supported on the elements that carry input, so it lies below 2 ^ t with t their number (wideRank_wmRegSeg_lt). A reduction that gives input symbols to its argument elements alone therefore has its file inside the working region, where the segment channel's ruler is in the top half.

The cell of an element, at the register channel

def DescriptiveComplexity.WMHasInp {A : Type} [FirstOrder.Language.wide.Structure A] (x : A) : Prop

An element the channel writes for: one that carries an input symbol. These are the elements the file has registers for.

Equations

• DescriptiveComplexity.WMHasInp x = ∃ (a : A), DescriptiveComplexity.WMInp x a

def DescriptiveComplexity.wmRegSeg {A : Type} [FirstOrder.Language.wide.Structure A] (x : A) : A → Prop

The cell of an element at the register channel: the elements that carry input, up to x.

Equations

• DescriptiveComplexity.wmRegSeg x y = (DescriptiveComplexity.WMLe y x ∧ DescriptiveComplexity.WMHasInp y)

def DescriptiveComplexity.WMRegSeg {A : Type} [FirstOrder.Language.wide.Structure A] (s : A → Prop) (x : A) : Prop

Being the cell of an element at the register channel, as the model reads it off an address.

Equations

• DescriptiveComplexity.WMRegSeg s x = ∀ (y : A), s y ↔ DescriptiveComplexity.WMLe y x ∧ DescriptiveComplexity.WMHasInp y

theorem DescriptiveComplexity.wmRegSeg_nonempty {A : Type} [FirstOrder.Language.wide.Structure A] (h : IsLinOrd WMLe) {x : A} (hx : WMHasInp x) : ∃ (y : A), wmRegSeg x y

The cell of an element the channel writes for is not empty: the element is in its own cell.

theorem DescriptiveComplexity.wmSetLt_wmRegSeg {A : Type} [FirstOrder.Language.wide.Structure A] (h : IsLinOrd WMLe) [Finite A] {x y : A} (hlt : WMLt WMLe x y) (hy : WMHasInp y) : WMSetLt WMLe (wmRegSeg x) (wmRegSeg y)

The cells grow with the elements: what the greater cell gains is greater than everything the two share, and the order on addresses weighs the least element most.

theorem DescriptiveComplexity.wideRank_wmRegSeg_lt {A : Type} [FirstOrder.Language.wide.Structure A] [Finite A] (h : IsLinOrd WMLe) (hup : ∀ (x y : A), WMLe x y → WMHasInp x → WMHasInp y) (x : A) : wideRank (wmRegSeg x) < 2 ^ Nat.card { y : A // WMHasInp y }

Where a cell lies: it is supported on the elements the channel writes for, and – when those are upward closed, which is what a reduction arranges by giving input to its greatest tags – so is every address below it. Its rank is then below 2 ^ their number, which is what puts the file inside a clocked program's working region.

theorem DescriptiveComplexity.wmRegSeg_least {A : Type} [FirstOrder.Language.wide.Structure A] (h : IsLinOrd WMLe) {bot : A} (hbot : WMHasInp bot) (hleast : ∀ (y : A), WMHasInp y → WMLe bot y) : wmRegSeg bot = fun (y : A) => y = bot

The bottom register is the marked element's own singleton: the least marked element cuts nothing below itself, so the file starts at the address that holds it alone.

The file the channel hands over

The machine an instance describes, at the register channel

def DescriptiveComplexity.wpInpReg {A : Type} [FirstOrder.Language.wide.Structure A] : WPoint A → WPoint A → Prop

The initial tape of the register channel: the cell of x holds the input symbol of x.

Equations

• DescriptiveComplexity.wpInpReg (Sum.inl s) (Sum.inr y) = ∃ (x : A), DescriptiveComplexity.WMRegSeg s x ∧ DescriptiveComplexity.WMInp x y
• DescriptiveComplexity.wpInpReg x✝¹ x✝ = False

def DescriptiveComplexity.wideRegData (A : Type) [FirstOrder.Language.wide.Structure A] : TMData (WPoint A)

The wide machine an instance describes, at the register channel: the machine of DescriptiveComplexity.wideData with its input written on the file of the elements that carry input, instead of on the ruler of all the segments. Every other field is the same one.

Equations

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

@[simp]

theorem DescriptiveComplexity.wideRegData_inp {A : Type} [FirstOrder.Language.wide.Structure A] (x y : WPoint A) : (wideRegData A).Inp x y ↔ wpInpReg x y

Isomorphism-invariance

theorem DescriptiveComplexity.wideRegData_agree {A B : Type} [FirstOrder.Language.wide.Structure A] [FirstOrder.Language.wide.Structure B] (e : FirstOrder.Language.wide.Equiv A B) : TMData.Agree (wpointEquiv e) (wideRegData A) (wideRegData B)

An isomorphism makes the two register-channel machines agree: every field but the channel is DescriptiveComplexity.wideData_agree's, and the channel transports because both what it compares and what it marks do.

The problems

def DescriptiveComplexity.WideRegAccept : DecisionProblem FirstOrder.Language.wide

Wide machine acceptance at the register channel: the question DescriptiveComplexity.WideAccept asks, of the machine whose input is written on the file of the elements that carry it. The clock is the same, the universe is the same, and what a reduction gains is a file it can reach.

Equations

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

def DescriptiveComplexity.WideRegAcceptSpace : DecisionProblem FirstOrder.Language.wide

Wide machine acceptance at the register channel, in bounded space.

Equations

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