The outer program: every call site but the evaluation #

The EXPSPACE program factors as an outer loop – startup, the sweep's advance, the convergence test, the copy-back, the output dispatch – around a per-address evaluation whose internals (gates, the VAL loop, the atom subroutines) are an order of magnitude larger. This file is the outer loop, with the evaluation abstract: its phase type PE, its site family and its boundary rules are parameters, exactly as DescriptiveComplexity.Draw.Prog.reaches_fileRoundTrip abstracts the middle of a trip.

The control flow:

start – one rule: plant bot and the marker at the empty address, step into the pattern write.
tgtTop – load TARGET with the logical-top pattern (DescriptiveComplexity.Draw.MapKit); exit into the startup seek.
seek1 – seek the marker to the logical top (DescriptiveComplexity.Draw.SeekKit); its exit plants the permanent ltp mark while erasing the marker, entering the reset.
reset1/clearMir1 – marker and mirror back to the empty address; exit into the evaluation of the first address.
sweepAdv – one round of the sweep (DescriptiveComplexity.Draw.AdvKit); its landing exit re-enters the evaluation. The evaluation's own boundary rules dispatch back: to the advance below the ltp cell, to reset2 at it.
reset2/clearMir2 – marker and mirror home after a completed sweep; clearMir2's two exits ask COMPARE's question at the empty address and enter the passing or failing phase accordingly (a sweep's first step happens in the entering rule – there is no cell to the left to enter from).
compare – the convergence test (DescriptiveComplexity.Draw.FlagSweepKit); at the ltp cell its verdict exits leave: passing to the output evaluation's walk home, failing to the copy-back's.
homeCmp/copy/homeCopy – walk home, copy the next stage over the current one (DescriptiveComplexity.Draw.WriteSweepKit, its first step in homeCmp's exit), walk home, and re-enter the evaluation for the next sweep.
homeOut – walk home and enter the output evaluation; its accepting exit is the program's single accepting phase, its failing verdict halts (no rule), which is a correct no.

Everything here is rules and shapes; the runs are DrawRun's.

The outer phases #

source

inductive DescriptiveComplexity.Draw.OuterPh (PE : Type) :

Type

The phases of the outer program: one copy of its kit's phase shape per call site, the four bespoke phases, and the evaluation's phases.

start {PE : Type} : OuterPh PE
The initial phase.
tgtTopP {PE : Type} : TrackPh → OuterPh PE
Loading TARGET with the logical-top pattern.
seek1P {PE : Type} : SeekPh → OuterPh PE
The startup seek to the logical top.
reset1P {PE : Type} : ResetPh → OuterPh PE
The startup reset.
clearMir1P {PE : Type} : TrackPh → OuterPh PE
Clearing the mirror after the startup reset.
advP {PE : Type} : AdvPh → OuterPh PE
One round of the sweep.
reset2P {PE : Type} : ResetPh → OuterPh PE
The reset after a completed sweep.
clearMir2P {PE : Type} : TrackPh → OuterPh PE
Clearing the mirror before the convergence test.
cmpP {PE : Type} : SweepPh → OuterPh PE
The convergence test.
homeCmpP {PE : Type} : OuterPh PE
Walking home after a failed test.
copyP {PE : Type} : OuterPh PE
The copy-back.
homeCopyP {PE : Type} : OuterPh PE
Walking home after the copy-back.
homeOutP {PE : Type} : OuterPh PE
Walking home after a passed test.
acceptP {PE : Type} : OuterPh PE
The accepting phase: no rule leaves it.
evalP {PE : Type} : PE → OuterPh PE
A phase of the evaluation.

Instances For

Dependency graph

source

instance DescriptiveComplexity.Draw.instFiniteOuterPh {PE : Type} [Finite PE] :

Finite (OuterPh PE)

Dependency graph

The outer sites #

source

inductive DescriptiveComplexity.Draw.OuterSite (SE : Type) :

Type

The call sites of the outer program, plus the evaluation's.

start {SE : Type} : OuterSite SE
The initial step.
tgtTop {SE : Type} : OuterSite SE
The pattern write of startup.
seek1 {SE : Type} : OuterSite SE
The startup seek.
reset1 {SE : Type} : OuterSite SE
The startup reset.
clearMir1 {SE : Type} : OuterSite SE
The startup mirror clear.
sweepAdv {SE : Type} : OuterSite SE
The sweep's advance.
reset2 {SE : Type} : OuterSite SE
The post-sweep reset.
clearMir2 {SE : Type} : OuterSite SE
The pre-compare mirror clear.
compare {SE : Type} : OuterSite SE
The convergence test.
homeCmp {SE : Type} : OuterSite SE
The walk home before the copy-back.
copy {SE : Type} : OuterSite SE
The copy-back.
homeCopy {SE : Type} : OuterSite SE
The walk home after the copy-back.
homeOut {SE : Type} : OuterSite SE
The walk home before the output evaluation.
accept {SE : Type} : OuterSite SE
The accepting phase's site: no rules.
eval {SE : Type} : SE → OuterSite SE
An evaluation site.

Instances For

Dependency graph

source

def DescriptiveComplexity.Draw.OuterSh (SE : Type) (ShE : SE → Type) :

OuterSite SE → Type

The rule shape of each outer site: the kit's rules, summed with the site's exit rules.

Equations

Instances For

Dependency graph

source

def DescriptiveComplexity.Draw.Data.exitG {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) (g : dt.SlotIx → A) :

Prop

The standard exit guard at a kit end phase: at the marker, which is nobody's register.

Equations

dt.exitG one g = (g DescriptiveComplexity.Draw.Slot.wk = one ∧ g DescriptiveComplexity.Draw.Slot.reg ≠ one)

Instances For

Dependency graph

source

def DescriptiveComplexity.Draw.Data.cmpG {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) (g : dt.SlotIx → A) :

Prop

COMPARE's per-cell question, shared by the test's rules and the entering exits.

Equations

dt.cmpG one g = ∀ (i : dt.d.B.ι), g (DescriptiveComplexity.Draw.Slot.old i) = one ↔ g (DescriptiveComplexity.Draw.Slot.new i) = one

Instances For

Dependency graph

source

noncomputable def DescriptiveComplexity.Draw.Data.outerRule {L : FirstOrder.Language} (dt : Data L) {A Q PE SE : Type} (zero one : A) {ShE : SE → Type} (ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (OuterPh PE)) (evalEntry evalEntryOut : PE) (i : OuterSite SE) :

OuterSh SE ShE i → Rule A Q dt.SlotIx (OuterPh PE)

The rules of the outer program: each site's kit rules at its phase copy, and its exit rules. The evaluation's rules – including its boundary rules into sweepAdv's and reset2's entries – are the parameter ruleE.

Equations

One or more equations did not get rendered due to their size.
dt.outerRule zero one ruleE evalEntry evalEntryOut DescriptiveComplexity.Draw.OuterSite.tgtTop (Sum.inl ρ) = (dt.tgtTopKit one DescriptiveComplexity.Draw.OuterPh.tgtTopP).rule zero one ρ
dt.outerRule zero one ruleE evalEntry evalEntryOut DescriptiveComplexity.Draw.OuterSite.seek1 (Sum.inl ρ) = (dt.seekKit DescriptiveComplexity.Draw.OuterPh.seek1P).rule zero one ρ
dt.outerRule zero one ruleE evalEntry evalEntryOut DescriptiveComplexity.Draw.OuterSite.clearMir1 (Sum.inl ρ) = (dt.clearMirKit DescriptiveComplexity.Draw.OuterPh.clearMir1P).rule zero one ρ
dt.outerRule zero one ruleE evalEntry evalEntryOut DescriptiveComplexity.Draw.OuterSite.sweepAdv (Sum.inl ρ) = (dt.advKit DescriptiveComplexity.Draw.OuterPh.advP).rule zero one ρ
dt.outerRule zero one ruleE evalEntry evalEntryOut DescriptiveComplexity.Draw.OuterSite.clearMir2 (Sum.inl ρ) = (dt.clearMirKit DescriptiveComplexity.Draw.OuterPh.clearMir2P).rule zero one ρ
dt.outerRule zero one ruleE evalEntry evalEntryOut DescriptiveComplexity.Draw.OuterSite.compare (Sum.inl ρ) = (dt.compareKit one DescriptiveComplexity.Draw.OuterPh.cmpP).rule one ρ
dt.outerRule zero one ruleE evalEntry evalEntryOut DescriptiveComplexity.Draw.OuterSite.copy (Sum.inl ρ) = (dt.copyKit DescriptiveComplexity.Draw.OuterPh.copyP).rule one ρ
dt.outerRule zero one ruleE evalEntry evalEntryOut DescriptiveComplexity.Draw.OuterSite.accept e = Empty.elim e
dt.outerRule zero one ruleE evalEntry evalEntryOut (DescriptiveComplexity.Draw.OuterSite.eval e) ρ = ruleE e ρ

Instances For

Dependency graph

source

def DescriptiveComplexity.Draw.Data.outerOwner {PE SE : Type} (ownE : PE → SE) :

OuterPh PE → OuterSite SE

The owner of each phase: the site whose copy of a phase shape it is; the evaluation's phases are owned through the parameter.

Equations

Instances For

Dependency graph

The in-shape separation, site by site #

source

theorem DescriptiveComplexity.Draw.Data.outerSep {L : FirstOrder.Language} (dt : Data L) {A Q PE SE : Type} (zero one : A) {ShE : SE → Type} (hzo : zero ≠ one) {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (OuterPh PE)} {evalEntry evalEntryOut : PE} (hsepE : ∀ (e : SE) (ρ ρ' : ShE e) (f : Q → A) (g : dt.SlotIx → A), (ruleE e ρ).guard f g → (ruleE e ρ').guard f g → (ruleE e ρ).srcPh = (ruleE e ρ').srcPh → ρ = ρ') (i : OuterSite SE) (ρ ρ' : OuterSh SE ShE i) (f : Q → A) (g : dt.SlotIx → A) :

(dt.outerRule zero one ruleE evalEntry evalEntryOut i ρ).guard f g → (dt.outerRule zero one ruleE evalEntry evalEntryOut i ρ').guard f g → (dt.outerRule zero one ruleE evalEntry evalEntryOut i ρ).srcPh = (dt.outerRule zero one ruleE evalEntry evalEntryOut i ρ').srcPh → ρ = ρ'

Each outer site separates in-shape: the kit's separation on its own rules, its exit-disjointness against the exits, and the exits' guards or target phases against each other. This is the hsep field of the program's DescriptiveComplexity.Draw.Assembly.

Dependency graph

Ownership, and the assembly #

source

theorem DescriptiveComplexity.Draw.Data.outerHowner {L : FirstOrder.Language} (dt : Data L) {A Q PE SE : Type} (zero one : A) {ShE : SE → Type} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (OuterPh PE)} {evalEntry evalEntryOut : PE} {ownE : PE → SE} (hosrcE : ∀ (e : SE) (ρ : ShE e), ∃ (p : PE), (ruleE e ρ).srcPh = OuterPh.evalP p ∧ ownE p = e) (i : OuterSite SE) (ρ : OuterSh SE ShE i) :

outerOwner ownE (dt.outerRule zero one ruleE evalEntry evalEntryOut i ρ).srcPh = i

Every rule fires from a phase its site owns.

Dependency graph

source

noncomputable def DescriptiveComplexity.Draw.Data.outerAsm {L : FirstOrder.Language} (dt : Data L) {A Q PE SE : Type} (zero one : A) {ShE : SE → Type} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (OuterPh PE)} {evalEntry evalEntryOut : PE} {ownE : PE → SE} (hosrcE : ∀ (e : SE) (ρ : ShE e), ∃ (p : PE), (ruleE e ρ).srcPh = OuterPh.evalP p ∧ ownE p = e) [Fintype Q] [Fintype dt.SlotIx] (hzo : zero ≠ one) (hsepE : ∀ (e : SE) (ρ ρ' : ShE e) (f : Q → A) (g : dt.SlotIx → A), (ruleE e ρ).guard f g → (ruleE e ρ').guard f g → (ruleE e ρ).srcPh = (ruleE e ρ').srcPh → ρ = ρ') :

Assembly A Q dt.SlotIx (OuterPh PE) (OuterSite SE)

The outer program, assembled: the sites, their rules, ownership and in-shape separation, ready for DescriptiveComplexity.Draw.Assembly.prog and its Table.Sep. The evaluation contributes its site family, its boundary data and its own separation as parameters.

Equations

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

Instances For

Dependency graph

Documentation

DescriptiveComplexity.Problems.Wide.DrawOuter

The outer program: every call site but the evaluation #

The outer phases #

The outer sites #

The in-shape separation, site by site #

Ownership, and the assembly #