A gated position's semantic pack, at an arbitrary file and phase #
What a leg of the evaluation is run with is a pack per position and VAL
content: the points the position's argument blocks encode. This file builds
them – it does not assume them – from the two bridges a coarse file needs
(hpassEnc, hgateEnc) and nothing else, so the space-bounded program and the
clocked one get their packs from the same place.
The construction is one step: a gated position's blocks are encodings
(ixIsEnc_of_gatedAt, the bridge read forwards), and ixPassSem turns
encodings into a pack. ixGatedSem is that pack at the state the matrix's
atoms run at, ixGatedSem₀ at the round's own, and ixGatedSem_eq_semCastT
says the first is the second transported – which is what the VAL loop's bridge
asks of a threaded family. The transport lemmas under them
(ixPassW_congr, ixKindSemCast_passSem, and the one-pack family) say the same
thing once: a pack sees the state through the mirror and VAL alone.
A passing round's valuation depends on the registers alone: both states' choices encode the same block value, and the encoding is injective.
Dependency graph
The pass's pack transports to the pass's pack: what a spine
position's hsem is discharged by, when its pack is the entry state's
carried forward by ixKindSemCast.
Dependency graph
One pack, carried to every position of the spine: the packs of the positions are the entry state's, transported. This is what makes the per-position family definable – the recursion that builds the tape family needs a pack at each of its own states, and here it has one as soon as the mirror rides.
Equations
- dt.ixSpineSem F zero one vi mV sem₀ hmir a hp b = dt.ixKindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi b) (sem₀ a ⋯ b)
Instances For
Dependency graph
One pack, carried to every round of every position – threaded: as
DescriptiveComplexity.Draw.Data.ixSpineSem, at the states the VAL loop's
own thread produces. Those differ from the position's entry state in the
two scratch registers and the register they enumerate, and a pack reads
the state through the mirror and VAL alone, so the entry state's pack
transports to all of them.
Equations
- dt.ixSpineSemT F zero one vi mV sem₀ hmir p a hp b = dt.ixKindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi b) (dt.ixKindSemCast zero one vi ⋯ ⋯ (dt.kindOf vi b) (sem₀ a ⋯ b))
Instances For
Dependency graph
What a gated position knows #
The branch DescriptiveComplexity.Draw.Data.ixGatedAt takes is not merely
the one where the machine runs the machinery: it is the one where the
argument blocks are encodings, which is what a semantic pack needs to
exist at all. DescriptiveComplexity.Draw.Data.gate_trichotomy says the
three legs are exhaustive; read in the other direction it says a gated
position's blocks encode points.
A gated position's argument blocks are encodings – the converse of
testOf_of_encMap/wit_of_encMap/domHolds_of_encMap, off the
trichotomy. This is what makes a position's semantic pack constructible
rather than assumed: at a junk position no pack exists, and at a gated one
the points are the blocks' own.
Dependency graph
A gated position's semantic pack, built – not assumed. The blocks
are encodings (ixIsEnc_of_gatedAt), so their points are the valuation the
pass decodes, and ixPassSem builds the pack there; ixKindSemCast carries it
to the state the matrix's atoms run at, which differs from it in the two
scratch registers alone. This is what a branched leg's semT is.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The gated position's pack at the round state – the same points, at
the state the semantics names. ixGatedSem is this pack transported
(ixGatedSem_eq_semCastT), which is what the VAL loop's bridge asks of a
threaded family.
Equations
- dt.ixGatedSem₀ F hpassEnc hgateEnc _hzo _hlin mV j st hg a hp b = dt.ixPassSem F hpassEnc (dt.varAt j) (dt.ixRoundSt st (mV a)) hp (fun (ℓ : Fin (dt.arOf (dt.varAt j))) => Exists.choose ⋯) ⋯ b
Instances For
Dependency graph
A gated position's pack is one pack transported: its points are the
address's blocks, which the scratch registers do not touch, so the family
the machinery is run with is ixSemCastT at
DescriptiveComplexity.Draw.Data.ixGatedSem₀ – the hypothesis the VAL
loop's bridge (ixVarFMT_eq_varFM) is stated under.
Dependency graph
The gates' bridge, proved #
hgateEnc is a hypothesis of the layers above because an arbitrary file need
not have a register for every element it is asked about. Where it does – any
file laid by blocks and tuples – the bridge is the elementwise one
(gate_trichotomy and testOf_of_encMap) read through
DescriptiveComplexity.Draw.Data.wellShapedG_ixBack_iff.
The gates' bridge at a coarse file, proved: a position is gated exactly
when the blocks of its mirror's address below the variable's arity are
encodings. This is hgateEnc, at any file whose registers stand for elements,
whose tuples are their elements' (hargP). Nothing has to be said about which
elements have registers: a failing element is one the address holds, hence a
register's already.
Dependency graph
The inner gates' bridge at a coarse file, proved: a level's gate passes
exactly when the block of VAL's address is an encoding. This is hpassEnc,
and it asks less than the gates' bridge did: only that the registers stand for
elements and that their tuples are their elements'. Nothing has to be said about
which elements have registers, because the members of the block are the marked
registers' own tuples. The verdict half is
DescriptiveComplexity.Draw.Data.igVerdict_iff_isEnc, which asks only that
the block's members be encoding-shaped, and that is what the shape test says.