lemmaroutine

Contour tours of tree components without counters

Halt's tree component has counter-free forward and backward contour tours
enumerates canonical initiations for cap and rank
Lemma·lem:ctrl-tour·§11.3 Contours and incoming operations

Statement (paper)

Let a finite deterministic graph of the form in Lemma  have a specified canonical success halt. Its undirected component is a tree directed toward that halt. There are mutually inverse next-mark and previous-mark operations on its contour, where the marks are the root sentinel and one distinguished occurrence of each canonical initiation in the component. These operations require the current program state and bounded incidence control, but no saved root or contour-length counter.

In plain English

For a finite deterministic guarded local graph with a chosen canonical success halt, the undirected component of that halt is a tree directed toward it. Its contour has mutually inverse next-mark and previous-mark operations, over marks given by the root sentinel and one distinguished occurrence of each canonical initiation. These use only the current program state and bounded incidence control, with no saved root or contour-length counter.

Why it's here

Since the graph has outdegree at most one and success states have no successor, the component is a tree rooted at the halt. Because predecessors and ordered incidences are locally computable (Lemma 11.4), the contour can be walked in either direction by local rules alone. This gives the counter-free forward and backward tours that the capped-port and rank wrappers and the realization theorem use to enumerate canonical initiations.
Classified routine:
This is an adaptation of the standard Euler-tour or contour traversal of trees via local successor/predecessor rules, as in Cook–McKenzie tree traversal in logspace and Sipser's reversible-space technique. It applies that traversal to the outdegree-at-most-one graph of Lemma 11.4.

Uses

lemGuarded local graph for terminal recipes

Used by

thmController interfaces have restoring O(B)-space implementationslemCapped incoming ports give restoring paired motionsclaimContours implement cap and rank wrappersclaimDecreasing-value contour tours count rank

Sources

PaperOpen
Section
§11.3 Contours and incoming operations
Page
—
Label
lem:ctrl-tour
Line
sections/implementation.tex:453
Leannot aligned

Phase 2 aligns this node to a Lean declaration.