Encoding the points of an expansion as block values #
A point of an exponential expansion is a tag together with an assignment of
the expansion's block – an exponential object. The EXPSPACE reduction stores
one point per argument block of a machine address, so it needs an injective
encoding of points as block values, the subsets of the tuple space
Fin dd → A an address holds at one tag.
The encoding is a set of tuples, each carrying a discrete code and a
payload laid out at fixed coordinates (DescriptiveComplexity.Draw.EncLayout
fixes the coordinates, DescriptiveComplexity.Draw.encTup writes one tuple):
- the tag witness
encTup (t, none) 0⃗, present in every encoding – without it, the empty assignments at two different tags would collide; - one member tuple
encTup (t, some i) (pad w)per tuplewthe assignment puts in its relation variablei, the payload canonically padded to the block's arity bound.
The discrete code is one-hot in the two designated elements, so
DescriptiveComplexity.Draw.encTup_code_inj reads the code back and
DescriptiveComplexity.Draw.encPt_injective makes the whole encoding injective;
DescriptiveComplexity.Draw.mem_encPt_asg reads one bit of the assignment off
one membership question, which is the form the machine's register lookups take.
DescriptiveComplexity.Draw.IsEnc – being the encoding of a point of the
expanded universe – is the condition the relativization lemma of
DescriptiveComplexity.Problems.Wide.DrawRel asks for
(DescriptiveComplexity.Draw.isEnc_iff).
The layout of one tuple #
The coordinates of an encoded tuple: where the discrete code sits, where the payload sits, disjointly. The reduction instantiates this once, with explicit arithmetic; everything else reads the coordinates through it.
- cIx : D → Fin dd
The coordinate of each component of the one-hot discrete code.
The coordinate of each payload position.
- cInj : Function.Injective self.cIx
Code coordinates are distinct.
- pInj : Function.Injective self.pIx
Payload coordinates are distinct.
Code and payload coordinates are disjoint.
Instances For
Dependency graph
One encoded tuple: the one-hot code of the discrete datum at the code
coordinates, the payload at the payload coordinates, the designated zero
everywhere else.
Equations
- DescriptiveComplexity.Draw.encTup ly zero one d pay = Function.extend ly.cIx (fun (q : D) => if q = d then one else zero) (Function.extend ly.pIx pay fun (x : Fin dd) => zero)
Instances For
Dependency graph
The code coordinates of an encoded tuple spell the one-hot code.
Dependency graph
The payload coordinates of an encoded tuple spell the payload.
Dependency graph
The remaining coordinates of an encoded tuple hold the designated zero.
Dependency graph
The code reads back: two encoded tuples that are equal carry the same discrete datum.
Dependency graph
The payload reads back: two encoded tuples that are equal carry the same payload.
Dependency graph
The encoding of a point #
The discrete data an encoded tuple can carry: either the witness of a tag – the tuple every encoding carries, and the only place a tag appears – or the relation variable of the block whose tuple the payload is.
The tag is deliberately not in a member's code. It is what makes «this block value is well-shaped» a question about one cell and nothing else, so the machine's gate can ask it of every cell by a file test: a member of a foreign tag is not merely rejected, it does not exist. What is left for the control is «exactly one witness», and the machine reads every tag's witness cell anyway.
Instances For
Dependency graph
One member tuple of an encoded point: the relation variable in the code, the variable's tuple in the payload, canonically padded to the block's arity bound.
Equations
- DescriptiveComplexity.Draw.encAsgTup ly zero one i w = DescriptiveComplexity.Draw.encTup ly zero one (Sum.inr i) (DescriptiveComplexity.Draw.pad zero w)
Instances For
Dependency graph
The tag witness of an encoded point: the one tuple that carries the tag.
Equations
- DescriptiveComplexity.Draw.encTagTup ly zero one t = DescriptiveComplexity.Draw.encTup ly zero one (Sum.inl t) fun (x : Fin (DescriptiveComplexity.blockArityBound X.B)) => zero
Instances For
Dependency graph
The encoding of a point as a block value: the tag witness, plus one member tuple per tuple of the assignment.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
An encoding is never everything: every member of it carries a one-hot
code, so the all-zero tuple is not one. This is what puts a tuple's address
strictly below the logical top – the top's blocks are full.
Dependency graph
The tag witness belongs to the encoding.
Dependency graph
A membership question at a tag witness reads the tag: the tag witness of
t belongs to the encoding of p exactly when p carries the tag t.
Dependency graph
A membership question at a member tuple reads one bit of the assignment:
the member tuple of (t, i, w) belongs to the encoding of p exactly when p
carries the tag t and its assignment holds of w at i. This is the form
the machine's register lookups take.
Dependency graph
The encoding is injective on points.
Dependency graph
The gate #
The encoding of a point of the expanded universe: the domain condition is carried by the subtype, so this is the map whose image the machine's gates carve out.
Equations
- DescriptiveComplexity.Draw.encMap ly zero one m = DescriptiveComplexity.Draw.encPt ly zero one ↑m
Instances For
Dependency graph
Being an encoding: the gate of the relativization – a block value passes exactly when it encodes a point of the expanded universe, domain condition included.
Equations
- DescriptiveComplexity.Draw.IsEnc ly zero one S = ∃ (m : X.Map A), S = DescriptiveComplexity.Draw.encMap ly zero one m
Instances For
Dependency graph
The encoding of the expanded universe is injective.
Dependency graph
The gate is the image of the encoding, in the orientation the relativization lemma asks for.