Resetting the working cell to the bottom

A random access starts at the checkpoint: marker and mirror at the empty address. Getting there from wherever the marker is – DescriptiveComplexity.Draw.Prog.reaches_reset – is the one itinerary of the program that runs down the working area: erase the marker and step right (never left, so the empty address needs no special case), scan left to the cell the permanent bot mark identifies, write the marker there stepping right, and bounce back left onto it. The mirror is cleared by a separate DescriptiveComplexity.Draw.ClearKit trip afterwards.

DescriptiveComplexity.Draw.ResetKit is the kit: the scan and the two bounce steps; the erasing entry is the caller's rule, and the landing phase hosts nothing – the machine arrives exactly once, at the bottom cell, where the caller's exit fires.

theorem DescriptiveComplexity.Draw.Prog.reaches_reset {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {t bt wk : W} (hnebt : bt ≠ t) (hnewk : wk ≠ t) {v : Univ A R P K dd → Prop} (hv : ∃ (x : Univ A R P K dd), ¬v x) {m : I → Prop} {restA restN restB : (Univ A R P K dd → Prop) → W → A} (hAN : ∀ (r : Univ A R P K dd → Prop), r ≠ v → restN r = restA r) (hNB : ∀ (r : Univ A R P K dd → Prop), (r ≠ fun (x : Univ A R P K dd) => False) → restB r = restN r) (hbtN : ∀ (r : Univ A R P K dd → Prop), restN r bt = bitVal PR.zero PR.one (r = fun (x : Univ A R P K dd) => False)) (hwkB : ∀ (r : Univ A R P K dd → Prop), restB r wk = bitVal PR.zero PR.one (r = fun (x : Univ A R P K dd) => False)) (hNBslot : ∀ (s : W), s ≠ wk → restB (fun (x : Univ A R P K dd) => False) s = restN (fun (x : Univ A R P K dd) => False) s) {p₀ pScan pB pDone : P} {fc : Q → A} (h₀ : PR.HasRight p₀ fc (PR.passTracksAt RF.cell t restA m v) pScan fc (PR.passTracksAt RF.cell t restN m v)) (hdown : ∀ (g : W → A), g bt ≠ PR.one → PR.HasLeft pScan fc g pScan fc g) (hput : ∀ (g : W → A), g bt = PR.one → PR.HasRight pScan fc g pB fc (Function.update g wk PR.one)) (hback : ∀ (g : W → A), PR.HasLeft pB fc g pDone fc g) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt p₀ fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t restA m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt pDone fc), head := Sum.inl fun (x : Univ A R P K dd) => False, tape := wideTape (PR.trackTapeAt RF.cell t restB m) (PR.syElt PR.blank) }

The reset, the budget forgotten.

The reset kit

inductive DescriptiveComplexity.Draw.ResetPh : Type

The phases of a reset: the down-scan, the bounce, and the landing – which hosts no rule, the caller's exit firing on arrival.

• scan : ResetPh

  Scanning left to the bottom cell.

• b : ResetPh

  The marker written, bouncing back.

• done : ResetPh

  At the bottom cell, marker set.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqResetPh : DecidableEq ResetPh

Equations

• DescriptiveComplexity.Draw.instDecidableEqResetPh x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteResetPh : Finite ResetPh

inductive DescriptiveComplexity.Draw.ResetRule : Type

The rule families of a reset.

• down : ResetRule

  Scan left while the bottom mark is clear.

• put : ResetRule

  At the bottom cell: write the marker, step right.

• back : ResetRule

  Bounce back left onto the marker.

@[instance_reducible]

instance DescriptiveComplexity.Draw.instDecidableEqResetRule : DecidableEq ResetRule

Equations

• DescriptiveComplexity.Draw.instDecidableEqResetRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.instFiniteResetRule : Finite ResetRule

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

A reset kit: the walked track, the bottom-mark and marker slots, and the phases.

• t : W

  The walked track (rides along unchanged).

• bt : W

  The bottom mark, planted at the empty address at startup.

• wk : W

  The working-cell marker slot.

• emb : ResetPh → P

  The kit's phases in the program.

noncomputable def DescriptiveComplexity.Draw.ResetKit.rule {A Q W P : Type} [DecidableEq W] (κ : ResetKit A Q W P) (one : A) : ResetRule → Rule A Q W P

The kit's rules.

Equations

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

Going home

After a plain sweep the machine stands at the top of the stretch while the marker never moved: getting back is a scan, not a reset. One phase, one rule – walk left unless the marker is under the head – and the caller's exit fires on arrival.

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

A home kit: one phase, one rule – walk left unless the marker is under the head. The caller's exit, guarded wk = one ∧ rg ≠ one, is disjoint by construction.

• t : W

  The walked track (rides along unchanged).

• wk : W

  The working-cell marker slot.

• ph : P

  The kit's phase in the program.

inductive DescriptiveComplexity.Draw.HomeKit.HomeRule : Type

The rule of a home kit.

• down : HomeRule

  Walk left unless the marker is under the head.

@[instance_reducible]

instance DescriptiveComplexity.Draw.HomeKit.instDecidableEqHomeRule : DecidableEq HomeRule

Equations

• DescriptiveComplexity.Draw.HomeKit.instDecidableEqHomeRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance DescriptiveComplexity.Draw.HomeKit.instFiniteHomeRule : Finite HomeRule

def DescriptiveComplexity.Draw.HomeKit.rule {A Q W P : Type} (κ : HomeKit A Q W P) (one : A) : HomeRule → Rule A Q W P

The kit's rule.

Equations

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