The pop phase of the simulation #
The second half of the simulation: from the resting configuration of a
continuation, the machine finds the top frame and performs the pop that
Turing.ToPartrec.stepRet prescribes – accepting on the empty continuation,
erasing a comp header, inspecting the flag of a fix, transferring the
stored head of a cons₂, or exchanging value and stored value of a cons₁.
The frame region is taken apart by
DescriptiveComplexity.HaltHard.FrameSeg.gap_split: a leading blank gap,
then the top frame (DescriptiveComplexity.HaltHard.TopSeg). Each pop lemma
ends either back at rest – for the pops that consume no code – or at the
dispatch point of a child, where DescriptiveComplexity.HaltHard.sim_norm
takes over.
The top frame #
The frame region with its leading gap peeled: the top frame comes first.
- halt
{c : Turing.ToPartrec.Code}
: TopSeg PCont.halt []
The empty continuation: nothing at all.
- cons₁
{c : Turing.ToPartrec.Code}
{p : CPos c}
{as : List ℕ}
{k : PCont c}
{w : List (SimSym c)}
: FrameSeg k w → TopSeg (PCont.cons₁ p as k) (SimSym.hCons₁ p :: (encVal as ++ w))
A
cons₁frame on top. - cons₂
{c : Turing.ToPartrec.Code}
{ns : List ℕ}
{k : PCont c}
{w : List (SimSym c)}
: FrameSeg k w → TopSeg (PCont.cons₂ ns k) (SimSym.hCons₂ :: ((encVal ns).reverse ++ w))
A
cons₂frame on top. - comp
{c : Turing.ToPartrec.Code}
{p : CPos c}
{k : PCont c}
{w : List (SimSym c)}
: FrameSeg k w → TopSeg (PCont.comp p k) (SimSym.hComp p :: w)
A
compframe on top. - fix
{c : Turing.ToPartrec.Code}
{p : CPos c}
{k : PCont c}
{w : List (SimSym c)}
: FrameSeg k w → TopSeg (PCont.fix p k) (SimSym.hFix p :: w)
A
fixframe on top.
Instances For
Dependency graph
A frame region splits into its leading gap and its top frame.
Dependency graph
Pass lemmas for the pops #
Where a content scan stops #
Whatever follows a frame region starts with a header, a blank or mid, never
a content letter – frames start with headers – so a rightward scan over
one/com stops deterministically. The two splits below extract that stop
letter, absorbing an erased zone of blanks in front.