A program, written rule by rule

DescriptiveComplexity.Draw.Table is a transition table stated the way a finished table wants to be stated: every attribute a function of the rule and of the rule's data, with the data a bare tuple. That presentation is wrong for writing a program, where one wants to say

in this phase, standing on a symbol whose tracks are g, with the pointer f in the control: go to that phase, write these tracks, and move left.

This file is that presentation, and the translation into a table.

The data of a rule is a state and a symbol

The one decision the layer rests on. A transition's data must carry both payloads – the state's and the symbol's – because neither determines the other: the symbol under the head cannot name the register the head is on (the registers are anonymous, DescriptiveComplexity.Problems.Wide.Marks), and the state cannot name the symbol it is about to read. So the slots of a rule's data are Q ⊕ W: the control slots Q, which a state uses and a symbol leaves at the designated element, and the track slots W, the other way round (DescriptiveComplexity.Draw.stVec, DescriptiveComplexity.Draw.syVec).

Two things fall out of that, and they are the point of the file.

• Firing a rule needs no equations. The data of the rule that fires is Sum.elim f g – the pointer and the tracks side by side – so DescriptiveComplexity.Draw.Prog.fire_left and its rightward twin hand a program its six attributes at the elements it named, with no payload arithmetic anywhere.
• Determinism reduces to a statement about rules. The state and the symbol occupy disjoint coordinates, so a transition's data is recovered from the two of them; DescriptiveComplexity.Draw.Table.Sep therefore reduces to DescriptiveComplexity.Draw.Prog.sep_of: two rules that fire on the same symbol from the same state must be the same rule. That is a check on pairs of rule families, which is what a program can actually carry out.

Control slots and track slots

def DescriptiveComplexity.Draw.stVec {A Q W : Type} (zero : A) (f : Q → A) : Q ⊕ W → A

The data a state occupies: its own slots, the designated element in the track slots.

Equations

• DescriptiveComplexity.Draw.stVec zero f = Sum.elim f fun (x : W) => zero

def DescriptiveComplexity.Draw.syVec {A Q W : Type} (zero : A) (g : W → A) : Q ⊕ W → A

The data a symbol occupies: the track slots, the designated element in the control slots.

Equations

• DescriptiveComplexity.Draw.syVec zero g = Sum.elim (fun (x : Q) => zero) g

@[simp]

theorem DescriptiveComplexity.Draw.stVec_inl {A Q W : Type} {zero : A} (f : Q → A) (q : Q) : stVec zero f (Sum.inl q) = f q

@[simp]

theorem DescriptiveComplexity.Draw.syVec_inr {A Q W : Type} {zero : A} (g : W → A) (s : W) : syVec zero g (Sum.inr s) = g s

theorem DescriptiveComplexity.Draw.stVec_injective {A Q W : Type} {zero : A} : Function.Injective (stVec zero)

theorem DescriptiveComplexity.Draw.syVec_injective {A Q W : Type} {zero : A} : Function.Injective (syVec zero)

noncomputable def DescriptiveComplexity.Draw.stPl {A Q W : Type} [Fintype Q] [Fintype W] (zero : A) (f : Q → A) : Fin (Fintype.card (Q ⊕ W)) → A

The payload of a state.

Equations

• DescriptiveComplexity.Draw.stPl zero f = DescriptiveComplexity.Draw.slotPl (DescriptiveComplexity.Draw.stVec zero f)

noncomputable def DescriptiveComplexity.Draw.syPl {A Q W : Type} [Fintype Q] [Fintype W] (zero : A) (g : W → A) : Fin (Fintype.card (Q ⊕ W)) → A

The payload of a symbol.

Equations

• DescriptiveComplexity.Draw.syPl zero g = DescriptiveComplexity.Draw.slotPl (DescriptiveComplexity.Draw.syVec zero g)

theorem DescriptiveComplexity.Draw.stPl_injective {A Q W : Type} {zero : A} [Fintype Q] [Fintype W] : Function.Injective (stPl zero)

theorem DescriptiveComplexity.Draw.syPl_injective {A Q W : Type} {zero : A} [Fintype Q] [Fintype W] : Function.Injective (syPl zero)

Rules

structure DescriptiveComplexity.Draw.Rule (A Q W P : Type) : Type

One rule of a program: what it applies to, where it goes, what it writes and which way it moves. The guard sees the pointer and the tracks separately, and so do the two things the rule computes.

• guard : (Q → A) → (W → A) → Prop

  When the rule applies: at this pointer, reading these tracks.

• srcPh : P

  The phase the rule applies in.

• dstPh : P

  The phase the rule moves to.

• dstSt : (Q → A) → (W → A) → Q → A

  The pointer the rule leaves in the control.

• wr : (Q → A) → (W → A) → W → A

  The tracks the rule writes.

• moveRight : Prop

  Whether the rule moves the head right.

structure DescriptiveComplexity.Draw.Prog (A R P Q W K : Type) (dd : ℕ) [Fintype Q] [Fintype W] : Type

A program: the two designated elements, a rule for each rule name, and the machine's constants – where it starts, which states accept, what the blank is, and the mark each element's register cell holds at time zero.

• zero : A

  The designated element a track holds when its bit is clear.

• one : A

  The designated element a track holds when its bit is set.

• zero_ne_one : self.zero ≠ self.one

  The two designated elements differ.

• payload_le : Fintype.card (Q ⊕ W) ≤ dd

  The slots fit in the tuples of the universe.

• rules : R → Rule A Q W P

  The rules.

• startPh : P

  The phase the machine starts in.

• startSt : Q → A

  The pointer the machine starts with.

• accept : P → (Q → A) → Prop

  Which states accept.

• blank : W → A

  The tracks of the blank.

• mark : Univ A R P K dd → W → A

  The tracks of the mark in the cell of an element.

• marked : Univ A R P K dd → Prop

  Which elements the channel writes for. Every one of them by default – the channel of DescriptiveComplexity.WideAccept writes for all – and a program emitted into the register channel of DescriptiveComplexity.WideRegAccept restricts it, the elements it leaves out having no register in the file it is handed.

noncomputable def DescriptiveComplexity.Draw.Prog.stElt {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] (PR : Prog A R P Q W K dd) (p : P) (f : Q → A) : Univ A R P K dd

A state of the program, as an element of the emitted universe.

Equations

• PR.stElt p f = DescriptiveComplexity.Draw.stateElt PR.zero p (DescriptiveComplexity.Draw.stPl PR.zero f)

noncomputable def DescriptiveComplexity.Draw.Prog.syElt {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] (PR : Prog A R P Q W K dd) (g : W → A) : Univ A R P K dd

A symbol of the program, as an element of the emitted universe.

Equations

• PR.syElt g = DescriptiveComplexity.Draw.symElt PR.zero (DescriptiveComplexity.Draw.syPl PR.zero g)

noncomputable def DescriptiveComplexity.Draw.Prog.table {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] (PR : Prog A R P Q W K dd) : Table A R P K (Fintype.card (Q ⊕ W)) dd

The table a program is. Every attribute is read off the rule of the tag and the two halves of the data.

Equations

• One or more equations did not get rendered due to their size.

Firing a rule

The data of the rule that fires is the pointer and the tracks side by side, so each of the table's six attributes is what the rule says at the elements the program named.

theorem DescriptiveComplexity.Draw.Prog.fire_left {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] (PR : Prog A R P Q W K dd) [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] (hR : PR.table.Reads) (r : R) (f : Q → A) (g : W → A) (hg : (PR.rules r).guard f g) (hd : ¬(PR.rules r).moveRight) : ∃ (τ : Univ A R P K dd), WMTr τ ∧ WMSrc τ (PR.stElt (PR.rules r).srcPh f) ∧ WMRead τ (PR.syElt g) ∧ WMDst τ (PR.stElt (PR.rules r).dstPh ((PR.rules r).dstSt f g)) ∧ WMWrite τ (PR.syElt ((PR.rules r).wr f g)) ∧ ¬WMRight τ

A rule fires, moving left: the shape every subroutine of the address layer asks for, at the state and the symbol the rule names.

theorem DescriptiveComplexity.Draw.Prog.fire_right {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] (PR : Prog A R P Q W K dd) [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] (hR : PR.table.Reads) (r : R) (f : Q → A) (g : W → A) (hg : (PR.rules r).guard f g) (hd : (PR.rules r).moveRight) : ∃ (τ : Univ A R P K dd), WMTr τ ∧ WMSrc τ (PR.stElt (PR.rules r).srcPh f) ∧ WMRead τ (PR.syElt g) ∧ WMDst τ (PR.stElt (PR.rules r).dstPh ((PR.rules r).dstSt f g)) ∧ WMWrite τ (PR.syElt ((PR.rules r).wr f g)) ∧ WMRight τ

A rule fires, moving right.

Determinism, as a check on pairs of rules

theorem DescriptiveComplexity.Draw.Prog.sep_of {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] (PR : Prog A R P Q W K dd) (h : ∀ (r r' : R) (f : Q → A) (g : W → A), (PR.rules r).guard f g → (PR.rules r').guard f g → (PR.rules r).srcPh = (PR.rules r').srcPh → r = r') : PR.table.Sep

The separation condition of a program: two rules that fire in the same phase, at the same pointer, reading the same tracks, are the same rule. The control slots and the track slots being disjoint is what turns DescriptiveComplexity.Draw.Table.Sep into this – a check a program can carry out rule family by rule family, with no payload in sight.

theorem DescriptiveComplexity.Draw.Prog.sepOn_of {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] (PR : Prog A R P Q W K dd) {Ph : P → Prop} (h : ∀ (r r' : R) (f : Q → A) (g : W → A), Ph (PR.rules r).srcPh → (PR.rules r).guard f g → (PR.rules r').guard f g → (PR.rules r).srcPh = (PR.rules r').srcPh → r = r') : PR.table.SepOn Ph

Separation at some phases only, the same reading of a rule set at a program that guesses: the two halves of the data are recovered from the injections exactly as above, and the phase restriction is carried through untouched.

The tape of a register pass

The tape all three passes of DescriptiveComplexity.Problems.Wide.Mirror and DescriptiveComplexity.Problems.Wide.Test run over: at the slot being walked the symbol carries the digit of the track there as a bit (DescriptiveComplexity.regBit, set only at the register cells); every other slot holds whatever element the program keeps at that cell – the marks of the register file carry elements, not bits – and rides along untouched.

noncomputable def DescriptiveComplexity.Draw.Prog.trackTapeAt {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] (PR : Prog A R P Q W K dd) [DecidableEq W] {I : Type} (cell : I → Univ A R P K dd → Prop) (t : W) (rest : (Univ A R P K dd → Prop) → W → A) (m : I → Prop) (r : Univ A R P K dd → Prop) : Univ A R P K dd

The tape a program presents while it walks a track, over an arbitrary register file. The walked slot holds the track's digit as a bit; the background is element-valued, so it can carry the name marks of a file whose cells are recognized by an element rather than by a bit.

The file enters as its cells and not as a DescriptiveComplexity.RegFile, since a tape is a definition and a file carries proofs; the proofs are wanted only in the three lemmas below. What indexes the cells is a parameter for the same reason it is one in DescriptiveComplexity.IxFile: a program on a clock cannot give every element of the universe a register, and a tape does not care which does.

Equations

• PR.trackTapeAt cell t rest m r = PR.syElt fun (s : W) => if s = t then DescriptiveComplexity.Draw.bitVal PR.zero PR.one (DescriptiveComplexity.bitAtOf cell m r) else rest r s

theorem DescriptiveComplexity.Draw.Prog.trackTapeAt_coh {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] (PR : Prog A R P Q W K dd) [DecidableEq W] {I : Type} (cell : I → Univ A R P K dd → Prop) (t : W) (rest : (Univ A R P K dd → Prop) → W → A) (m m' : I → Prop) (u : I) (hag : ∀ (v : I), v ≠ u → (m v ↔ m' v)) (r : Univ A R P K dd → Prop) (hr : r ≠ cell u) : PR.trackTapeAt cell t rest m r = PR.trackTapeAt cell t rest m' r

The coherence condition of the three register passes, discharged, at an arbitrary file: two tracks agreeing off one element present the same symbol at every cell but that element's register. The track enters the tape only through DescriptiveComplexity.bitAtOf, and DescriptiveComplexity.bitAtOf_congr says that does not move. Every caller of the register passes is given this and owes nothing.

theorem DescriptiveComplexity.Draw.Prog.trackTape_coh {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] (PR : Prog A R P Q W K dd) [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [DecidableEq W] (t : W) (rest : (Univ A R P K dd → Prop) → W → A) (m m' : Univ A R P K dd → Prop) (u : Univ A R P K dd) (hag : ∀ (v : Univ A R P K dd), v ≠ u → (m v ↔ m' v)) (r : Univ A R P K dd → Prop) (hr : r ≠ wmSeg u) : PR.trackTapeAt wmSeg t rest m r = PR.trackTapeAt wmSeg t rest m' r

The coherence condition of the three register passes, discharged.