The names a trip walks to are definable #
Every trip of the program is aimed by a naming guard: this cell is the
canonically padded cell of the element whose block is b and whose first ddâ‚€
coordinates spell a given tuple. The coordinate loops spell it from the control
directly (DescriptiveComplexity.Draw.Data.nameG); the leaf reads of the
element loops spell an encoded tuple
(DescriptiveComplexity.Draw.Data.encCoord), and this file says that is a
naming guard the interpretation can write down too.
The reason is the layout, not the data: at each coordinate an encoded tuple
holds a component of the one-hot code – one of the two designated elements – or
a payload position, or the clear element, and which it holds is decided by
DescriptiveComplexity.Draw.EncLayout when the formula is built. So an encoded
coordinate is DescriptiveComplexity.Draw.UReadable as soon as the payload is,
and every payload the program spells is a control slot or the clear element.
An encoded coordinate #
The naming guard, from readable coordinates #
The payload a read leaf spells #
The well-shapedness questions #
The gates' file test asks of a cell that its name slots spell an encoded tuple: the witness of some tag, or a member of some relation variable. The first is a disjunction over a finite type of tags; the second quantifies a tuple of the instance, which no combinator covers – so the existential has to go, and the layout is what removes it. At a coordinate the encoding does not read from the payload the value is pinned; at one it does, the tuple is free, and a witness can be read straight off the cell.