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
Gaps may be prepended to a frame region wholesale.
Dependency graph
A top frame is in particular a frame region.
Dependency graph
Pass lemmas for the pops #
Dependency graph
Dependency graph
Dependency graph
Dependency graph
Dependency graph
Dependency graph
Dependency graph
Dependency graph
Dependency graph
Dependency graph
Dependency graph
Dependency graph
Dependency graph
fxDropR re-crosses the gap blanks.
Dependency graph
fxOnes erases the digits of the head block, walking left.
Dependency graph
ppFind crosses the gap blanks.
Dependency graph
ppScan passes the frame content.
Dependency graph
ppScan stops on the first letter that is not frame content.
Dependency graph
ppKill erases the spent frame content, walking left.
Dependency graph
swScan passes the frame content.
Dependency graph
swScan stops on the first letter that is not frame content.
Dependency graph
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.
A frame region followed by mid starts with a letter that is not frame
content.
Dependency graph
A blank run in front preserves the shape of the stop letter.
Dependency graph
Popping a comp frame: seek the top frame, erase its header, and
walk to the dispatch point of its code. The header cell joins the gap.
Dependency graph
The empty continuation accepts: the frame region is a bare blank gap,
so the wake-up walk crosses it, meets mid and accepts.
Dependency graph
Dropping a spent fix frame: from fxDropL on endL, re-cross the
gap, erase the kept header stepping left, and walk home to rest – the header
cell joins the gap.
Dependency graph
Popping a fix frame, zero or empty flag: the wake-up walk keeps the
header and fxGo inspects the last letter of the value at endR – a blank
for the empty value, restored after a probe step, or the head block's lone
separator, consumed as the new endR – then fxDropL/fxDropR drop the
kept frame and return to rest over the tail of the value.
Dependency graph
Popping a fix frame, positive flag: fxGo finds a digit at endR,
fxOnes erases the head block down to its separator – which becomes the new
endR – and nSeekL walks back to mid to dispatch the body over the tail
of the value, the frame kept in place.
Dependency graph
Merging two adjacent blank runs – the shape the frame erasures leave.
Dependency graph
One round of the cons₂ transfer: from the header, scan to the end
of the remaining content, step back onto its last digit, erase it, carry it
to endR, append it by the endR-shift and walk back to the header. The
erased zone right of the content – abstracted, with the letter after it, into
x :: Y' – grows by one blank, the appended run by one digit.
Dependency graph
The cons₂ transfer loop: the rounds of
DescriptiveComplexity.HaltHard.pp_iter, iterated over the digits of the
head block – the rightmost content letters, the frame being mirrored.
Dependency graph
Discarding the spent cons₂ frame: the digits gone, the scan finds
the head block's separator last; ppLast erases it, ppKill sweeps the rest
of the content into blanks, erases the header, and retL walks home.
Dependency graph
Popping a cons₂ frame: the wake-up walk keeps the header; ppGo
appends the new block's separator at endR and ppBack/ppFind return to
the header; the transfer loop moves the digits of the frame's head block –
the rightmost content letters, the frame being mirrored – one by one to
endR; and once the separator is reached the rest of the frame is swept into
blanks and the machine returns to rest, the head of the stored value now
prepended to the value.
Dependency graph
One round of the value move: swGo sits on endR; the marker is
erased, the last value letter peeked, endR slides onto its cell, the letter
is carried over the whole tape – the middle abstracted into M – to endL
and written by the endL-shift, and swGo walks back onto endR. Stated over
an abstract carry state so the digit and separator instances share the
proof.
Dependency graph
The value move, iterated: the whole value crosses into the region at
endL, mirrored – consumed at endR, written by endL-shifts – while the
left blanks shrink and the right pad grows by its length.
Dependency graph
One round of the stored-value move: swOut finds the old header past
the new frame – its content and the gap abstracted into DN – swScan
crosses the remaining content, swLast steps back onto its last letter,
erases it, and the carry appends it at endR by the endR-shift before
swBack/swOut re-enter. Stated over an abstract carry state so the digit
and separator instances share the proof.
Dependency graph
The stored-value move, iterated: the stored value crosses out to the value region, mirrored – consumed at the content's right end, appended by endR-shifts – while the erased zone between the old header and what follows grows by its length.
Dependency graph
Popping a cons₁ frame: phase one moves the value into a fresh
cons₂ frame at endL – consumed at endR, so the frame stores it
mirrored – and closes it with its header; phase two finds the old cons₁
header – the first such header right of endL – and moves its stored value
out to endR the same way, so the value region receives it mirrored; the old
header erased, nSeekR walks to mid to dispatch the body of the pending
fix.