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 ^ twithttheir 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 #
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
Instances For
Dependency graph
The cell of an element at the register channel: the elements that carry
input, up to x.
Equations
Instances For
Dependency graph
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
Instances For
Dependency graph
Dependency graph
An address is a cell exactly when it is that segment, so WMRegSeg
never has to be unfolded again.
Dependency graph
The cell of an element the channel writes for is not empty: the element is in its own cell.
Dependency graph
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.
Dependency graph
Distinct elements the channel writes for have distinct cells.
Dependency graph
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.
Dependency graph
The working area lies below the file, at the register channel too – but
for a different reason, and under a condition the reduction has to arrange. A
cell is the down-set of a marked element, so every cell holds the least
marked element bot, which is the most significant digit any of them has. An
address is therefore below every cell exactly when it stays strictly above
bot.
This is the geometry that decides where a reduction may put its marks. Marking
the argument elements alone would not do: a logical address is a set of argument
elements, so it would hold the least marked element itself and land among the
registers. Marking one further element below the argument tags fixes it: no
logical address reaches down to it, every cell does, and the file sits in a band
of its own directly above the working area – while staying inside 2 ^ the
number of marks, which is what
DescriptiveComplexity.wideRank_wmRegSeg_lt bounds.
Dependency graph
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.
Dependency graph
The file the channel hands over #
The machine an instance describes, at the register channel #
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
Instances For
Dependency graph
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.
Instances For
Dependency graph
Dependency graph
Isomorphism-invariance #
The cell of an element transports along an equivalence of instances.
Dependency graph
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.
Dependency graph
The problems #
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.
Instances For
Dependency graph
Wide machine acceptance at the register channel, in bounded space.
Equations
- One or more equations did not get rendered due to their size.