The clocked program of a reduction into the register channel

DescriptiveComplexity.Draw.Data.nexProg is the clocked program of a reduction that lays its own file: it carries a coordinate map, and the sweep that lays the file carries a pointer as wide as an address – which no wide machine's control can hold (DescriptiveComplexity.Problems.Wide.Limits).

This file is the program of a reduction into DescriptiveComplexity.WideRegAccept, which is handed its file. It is the same program with two changes, and both remove something:

• the file-laying sweep is nullSpec, so there is no pointer and no coordinate map – the phase is two steps and writes nothing;
• the channel writes for the argument elements and for one element below them (regFileMarkArg), which is what puts the file inside the working region and directly above it – and the mark it writes is regSlotMark, whose regFirst slot names that element rather than the least of the universe.

Everything else – the guess, the walks home, the evaluation, the accepting predicate – is nexProg's own, so its definability, its separation and its runs serve unchanged.

What is here is the program, the two legs of a clocked run packaged as a yes-instance (wideRegAccept_of_legs, at an arbitrary program), and the rule-level facts a determinism argument is built from: separation after the guess and the accepting phase no rule fires from.

noncomputable def DescriptiveComplexity.Draw.Data.nexProgHanded {L : FirstOrder.Language} (dt : Data L) {A G : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] (zero one : A) [LinearOrder dt.NexRIx] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) (γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G) (args : (v : dt.VarIx) → dt.VarArgs v) (bot : Option dt.KIx) : Prog A dt.NexRIx (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd

The clocked program of a reduction into the register channel: the outer layer at the sweep that lays nothing and the region-guessing one, over the shared tower's evaluation, with the input written on the argument elements' file. Its pointer starts clear – there is no file-laying pointer to set – and its channel writes for the argument elements alone.

Equations

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

theorem DescriptiveComplexity.Draw.Data.nexProgHanded_rules {L : FirstOrder.Language} {dt : Data L} {A G : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] {zero one : A} [LinearOrder dt.NexRIx] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {args : (v : dt.VarIx) → dt.VarArgs v} {bot : Option dt.KIx} (i : NexSite dt.SEF) (ρ : NexSh dt.SEF (Option dt.KIx) G dt.NexSESh i) : (dt.nexProgHanded zero one hzo hpl γ args bot).rules ⟨i, ρ⟩ = dt.nexRule one (dt.nullSpec (Option dt.KIx)) γ (dt.nexEvalRuleF zero one args) (EvalPh.chk 0) bot i ρ

The handed program's rules, at a rule name: what every run lemma's rule hypothesis is discharged by.

The two legs, at any program that reads the same rules

theorem DescriptiveComplexity.Draw.Data.wideRegAccept_of_legs {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [Finite A] [Finite dt.KIx] [LinearOrder R'] [Finite R'] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [Finite (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hmk : ∀ (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), PR.mark x Slot.mir = PR.zero) (hbl : PR.blank Slot.mir = PR.zero) {I : Type} {F : LaidFile dt A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) I} {st : TapeSt dt A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) I} (hmir : st.mir = fun (x : I) => False) {evalEntry : EvalPh dt.nv dt.PMF} {f₁ : dt.CtlIx → A} {w : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} {o e : ℕ} (hopen : (wideData (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn o { state := Sum.inr (PR.stElt PR.startPh PR.startSt), head := Sum.inl fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False, tape := wideTape (PR.trackTapeAt F.cell Slot.mir PR.initBackReg fun (x : I) => False) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt (NexPh.evalP evalEntry) f₁), head := Sum.inl w, tape := wideTape (PR.trackTapeAt F.cell Slot.mir (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) fun (x : I) => False) (PR.syElt PR.blank) }) {cT : Config (WPoint (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd))} (heval : (wideData (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)).ReachesIn e { state := Sum.inr (PR.stElt (NexPh.evalP evalEntry) f₁), head := Sum.inl w, tape := wideTape (PR.trackTapeAt F.cell Slot.val (dt.ixBack F.toLayout PR.zero PR.one ⋯ st) st.val) (PR.syElt PR.blank) } cT) {a b k j m : ℕ} (hk : 1 ≤ k) (hkj : k + 1 < j) (hm : 0 < m) (hcard : (k + j) * m ≤ Nat.card (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (he : e ≤ a * b) (ha : a ≤ 2 ^ (k * m)) (hb : b ≤ 2 ^ (k * m)) (hopenle : o + 1 ≤ 2 ^ ((k + 1) * m)) {p : NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)} {fq : dt.CtlIx → A} (hstate : cT.state = Sum.inr (PR.stElt p fq)) (hacc : PR.accept p fq) : WideRegAccept.Holds (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)

A program accepts, from its opening and its evaluation – stated of any program whose channel writes nothing on the walked track, so that the padded program and the program itself are two instances of one statement. It is The two legs of a clocked run, at an arbitrary program: the adjustment between them (config_openingEnd_eq_evalStart), the file the initial tape is presented along (trackTape_empty_congr) and the clock.

The handed program is deterministic after its guess

The three facts a backward reading needs, at the handed program: it separates after the guess, so a run from a post-guess configuration is unique, and its accepting phase is stuck. All three are nexProg_sepOn's, nexProg_uniqueFrom's and nexProg_stuck_acceptP's at the rule set that lays no file – the rules being the same function of the rule name (nexProgHanded_rules), the sweep the only thing that changed, and neither the sweep nor the channel entering any of the three proofs.

theorem DescriptiveComplexity.Draw.Data.nexProgHanded_sep_rules {L : FirstOrder.Language} {dt : Data L} {A G : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [LinearOrder dt.NexRIx] {zero one : A} (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {args : (v : dt.VarIx) → dt.VarArgs v} {bot : Option dt.KIx} (r r' : dt.NexRIx) (f : dt.CtlIx → A) (g : dt.SlotIx → A) : ((dt.nexProgHanded zero one hzo hpl γ args bot).rules r).srcPh.PostGuess → ((dt.nexProgHanded zero one hzo hpl γ args bot).rules r).guard f g → ((dt.nexProgHanded zero one hzo hpl γ args bot).rules r').guard f g → ((dt.nexProgHanded zero one hzo hpl γ args bot).rules r).srcPh = ((dt.nexProgHanded zero one hzo hpl γ args bot).rules r').srcPh → r = r'

The handed program separates after its guess: two of its rules firing in the same post-guess phase on the same data are the same rule. Across sites that is the owner map (nexOwner_nexRule); within a site it is nexSep_postGuess, and the guess site is where the two are allowed to differ – which is why the phase restriction is there.

theorem DescriptiveComplexity.Draw.Data.nexProgHanded_srcPh_ne_acceptP {L : FirstOrder.Language} {dt : Data L} {A G : Type} [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] [LinearOrder A] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [LinearOrder dt.NexRIx] {zero one : A} (hzo : zero ≠ one) (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) {γ : GuessSpec A dt.CtlIx dt.SlotIx (Option dt.KIx) G} {args : (v : dt.VarIx) → dt.VarArgs v} {bot : Option dt.KIx} (r : dt.NexRIx) : (dt.nexProgHanded zero one hzo hpl γ args bot).table.srcPh r ≠ NexPh.acceptP

No rule of the handed program fires from its accepting phase: the accepting phase is owned by the accepting site (nexOwner), and that site has no rules at all – its shape is Empty.