definitionroutine

Regenerable local records

Defines regenerable local records rebuildable from root data and active records
form of control data assumed by the replay lemma
Definition·def:ctrl-record·§11.2 Program states and record bounds

Statement (paper)

A local record is a delimited binary word with a tag from a fixed finite alphabet. It may contain immediate descriptor choices, bounded port or copy symbols, offsets, Boolean evaluation paths and pending bits, and the early numerical words permitted by Theorem . Head positions in such words are marked locally. A root tuple, a root operation and its numerical clock, together with the active records, determine every descendant tuple and clock by a scratch computation. This computation does not call a graph procedure and does not use a cursor that has been left behind. We call such records regenerable.

In plain English

A local record is a delimited binary word with a tag from a fixed finite alphabet, holding things like descriptor choices, port or copy symbols, offsets, Boolean evaluation paths, pending bits and permitted early numerical words, with head positions marked locally. Records are called regenerable when a root tuple, root operation and numerical clock, together with the active records, determine every descendant tuple and clock by a scratch computation that calls no graph procedure and uses no abandoned cursor.

Why it's here

This definition fixes the form of the control information that a space-bounded simulation stores, and requires that it can be rebuilt from the root data and the active records alone. That rebuilding property is what lets later results, such as the parameter replay lemma, recompute descendant parameters instead of storing them, which keeps the records small.
Classified routine:
A bookkeeping definition that fixes the format of the stored control records for the space-bounded simulation. It follows the standard logspace practice of keeping only constant-size local state and recomputing everything else from root data, as in composition of logspace transducers.

Uses

Nothing else in the paper

Used by

lemControl records replay with later-salt independence

Sources

PaperOpen
Section
§11.2 Program states and record bounds
Page
—
Label
def:ctrl-record
Line
sections/implementation.tex:169
Leannot aligned

Phase 2 aligns this node to a Lean declaration.