The rounds of the evaluation, counted over the handed file #
DescriptiveComplexity.Draw.Data.exists_valEnum builds the VAL loop's enumeration over
the universe, where a space-bounded machine's registers are the elements
themselves. A clocked machine counts the same rounds over the index of its
file, so this file rebuilds the enumeration there: a chain of increments in the
file's own order, from the empty address to the registers standing for inner
elements.
Everything it needs is generic (DescriptiveComplexity.exists_wmChainOf,
wmChainOf_lt) or a fact about the tags: the inner blocks are a final segment
(DescriptiveComplexity.Draw.kinSeg), so above a register standing for an inner
element every register does, and a marked address holds inner elements alone –
which is what the semantic layer reads a round through.
The registers the rounds end at: those standing for an element of an inner block.
Equations
Instances For
Dependency graph
A register of an inner block stands for an inner argument element.
Dependency graph
The inner registers are upward closed: the inner blocks are a final
segment of the tag order (DescriptiveComplexity.Draw.kinSeg), so above a
register of an inner block every register is one.
Dependency graph
The rounds of the evaluation, over the handed file: a chain of increments in the file's own order from the empty address to the inner registers, in exactly the forms the clocked run demands – the covers are increments, the last round passes the exhaustion test everywhere, every earlier one fails it somewhere, every round holds inner registers alone, and every register it marks is one the addresses use.
Dependency graph
How many elements there are, and how many the channel marks #
The clock is met by comparing three numbers with 2 ^ (k · m), and two of them
are sizes of the drawing: how many elements the universe has, and how many the
channel writes for. Both are counted here, once, so that a reduction choosing
k, j and m argues about its own tags and nothing else.
The universe's size: a tag and a tuple.
Dependency graph
The tags: one per rule name, one per phase, one per argument block, and the alphabet's own.
Dependency graph
The channel writes for the argument elements and one more: so the file
has at most as many registers as there are argument elements, plus one, and the
bound the walks are charged against is 2 ^ that.
Dependency graph
The file has at least one register per padded argument cell: the channel writes for every argument element, and the padded tuples of the encoding's width are that many. This is the lower bound the clock's exponent is measured against – the record's tuple counts are below the register count, so they are below the file's own bound.
Dependency graph
The drawing has at least one tag per assignment of the guessed block: the guessing site's rule names carry a block of the sweep and a certificate value, so the assignments of the block inject into the rule names.
This is the lower bound the clock's counting hypothesis is met by, and it is
why a reduction can buy tags by padding its kernel's block
(DescriptiveComplexity.SOBlock.pad): one extra relation variable doubles the
count.
Dependency graph
The clock's exponent, counted: every dimension the evaluation's width is
measured against is under a power of two whose exponent is linear in the number
of registers, with the kernel's own dimensions as the additive constant. The
file's widths give 4 N + 14 (regWidthBd_le_two_pow), the padded cells give
N – a register per cell, card_regIx_ge – and the loop budget gives
eDim · N, the universe being no bigger than the file.
This is where the clock stops depending on the instance: N grows with
|A| ^ dd, and so does the drawing, so what a reduction owes is a comparison
between two constants.
Dependency graph
And its logarithm, which is the number the clock actually compares.
Dependency graph
The clock's one inequality, met by a constant of the kernel. The
exponent is linear in the register count (log_evalQ_le), the register count is
linear in |A| ^ dd (card_regIx_le), and the universe is |Tag| · |A| ^ dd
– so the two sides scale together and what is left is a comparison between the
drawing's rule names and a number built from the kernel alone: its guessed
variables' arities and counts (dimC), its loop budget (eDim) and its argument
blocks (KIx).
A reduction meets it by padding its kernel's block until the rule names clear
that number, each extra variable doubling them
(two_pow_card_le_card_nexRIx).