The file of the register channel, laid out #
DescriptiveComplexity.Draw.Data.diagLaid reads the segment channel's ruler
as a DescriptiveComplexity.Draw.LaidFile: one register per element of the
universe, in the universe's own order, each naming its own tag's block and its
own tuple. This file does the same for the register channel, whose file has
one register per element the channel writes for.
Everything the evaluation asks of a layout is the elementwise one's, restricted:
- a register is an element, so the block and the named coordinates spell it
(
nameSep_regLaid); - every block and named tuple has a register, provided the reduction writes for
the argument elements – which is what it does, and what makes its file lie in
the working region (
hasName_regLaid); - the registers grow with the elements (
wmSetLt_wmRegSeg), which is the one property the singleton channel could not give.
The index of the register channel's file: the elements it writes for.
Equations
- dt.RegIx = { x : DescriptiveComplexity.Draw.Univ A R' P' dt.KIx dt.dd // DescriptiveComplexity.WMHasInp x }
Instances For
Dependency graph
The register channel's file, laid out: one register per element the channel writes for, in the universe's own order, each naming its own tag's block and its own tuple.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The file's layout order is linear, being the universe's own read on a subtype.
Dependency graph
The file's marks tell its registers apart: a register is an element, so its block and its named coordinates spell it.
Dependency graph
The file has a register for every name, provided the channel writes for
the argument elements: a register is an element, and a name is one of them. This
is the one thing the reduction has to arrange about its channel, and arranging
it is what puts the file in the working region – the argument tags are the
greatest (DescriptiveComplexity.Draw.lt_arg).
Dependency graph
The evaluation's working area lies below the file. A logical address is
made of argument elements; the file's registers all hold the least marked
element, which the reduction places below the argument tags. So no address the
evaluation manipulates ever reaches into the file, and the walks that assume it
(DescriptiveComplexity.Draw.Data.nexIxEvalB_reachesIn's hwork) apply
unchanged.
This is the one thing the reduction owes its own marking, and the reason the marks are «the argument elements and one element below them» rather than the argument elements alone: with the latter the least marked element would itself be an argument element, and an address holding it would be a register's neighbor instead of lying under the file.
Dependency graph
The coherences the evaluation asks of a file #
The registers an address uses: the ones standing for argument elements. The register below them – the one the reduction marks so that the file lies above the working area – is never part of a logical address.
Equations
- dt.RegUse u = ∃ (i : dt.KIx), (↑u).1 = DescriptiveComplexity.Draw.Tag.arg i
Instances For
Dependency graph
A named register stands for the element it names: the heltP
coherence.
Dependency graph
A register's block is the block of the element it stands for: the
hblkP coherence, both sides being the tag's own block.
Dependency graph
The registers are ordered like the elements they stand for: the hmono
coherence, which at this file is the channel's own agreement between the tag
order and the address order.
Dependency graph
Nothing above a used register escapes the file: the argument tags come
last, so an element above an argument element is an argument element, and the
reduction marks all of them. This is the hup coherence.
Dependency graph
A logical address is held by the file's registers: the hvh
coherence.
Dependency graph
A named register is a used one: it stands for an argument element. This
is the hxdUse the stage atom's destination registers ask for.
Dependency graph
What the file costs to walk #
The number the register channel's walks are charged against: 2 ^ the
number of registers, which is the size of the working region and the bound every
address of the file is under.
Instances For
Dependency graph
Every register of the file lies below the bound: its address is supported on the elements the channel writes for, and so is every address below it once those are upward closed.
Dependency graph
A step of a walk over the file costs at most the bound: consecutive
registers differ by one bit of the address, and the whole file is below the
bound. This is the w of every budgeted walk, where a file laid on consecutive
addresses has w = 1 and pays the difference in the number of registers
instead.
Dependency graph
The width a walk to a register is charged: twice the bound, plus two.
Instances For
Dependency graph
The width of the pass over the whole file: the file's two ends, the walk between them at one bound a step, and the marker's own address.
Instances For
Dependency graph
The width of a read below the file: an address under the first register is under the bound.
Instances For
Dependency graph
The width of a stage's inner loop: a pass per bit of the address it
carries, each pass priced as regWP.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The pass over the file fits regWP.
Dependency graph
A read below the file fits regWR.
Dependency graph
A stage's inner loop fits regWK.
Dependency graph
A walk to a register fits regW.
Dependency graph
The file's two ends #
The file has a greatest register, the marked elements being finitely many and linearly ordered.
Dependency graph
The file has a least register, the one the reduction places below the argument elements.