Field note
Language Classes: Ask What the Checker Must Remember
The Chomsky hierarchy becomes easier to remember when treated as a hierarchy of scratch space. The important question is not how clever a recognizer is, but what memory shape it may use while reading the input.
Finite state: a bounded summary
A finite automaton remembers only which of finitely many states it occupies. It can recognize an even number of a characters or whether 0101 occurred, because each needs only a fixed summary of the prefix.
It cannot recognize aⁿbⁿ. When the b characters begin, the machine must remember an unbounded n. Myhill–Nerode makes this exact: two prefixes share a state only when no future suffix can distinguish them. The prefixes a, aa, aaa, and so on are all distinguishable, so no finite set of states is enough.
One stack: nesting with destructive recall
A pushdown automaton adds an unbounded stack. It handles aⁿbⁿ by pushing for each a and popping for each b. This is why context-free grammars naturally represent nested parentheses and syntax trees.
But the access pattern matters. Reading the stack consumes its top. After comparing the as with the bs, nothing remains to compare with a third block of cs, so aⁿbⁿcⁿ is not context-free. A stack reverses, which makes wwᴿ natural and an exact copy ww impossible in general.
Linear tape: revisit the input
A linear-bounded machine may read, write, and revisit O(n) cells. It can cross off one a, one b, and one c repeatedly, or compare two distant regions without destroying the first one. This is the territory of context-sensitive languages and semantic checks such as “every identifier was declared before use.”
Non-contracting context-sensitive grammar rules never make an intermediate form shorter. For a target of length n, the relevant search stays within a finite bounded space, so membership remains decidable.
Unrestricted grammars remove that bound. A recognizer may need unbounded intermediate storage or run forever. That is the line between recognizing a yes-instance eventually and deciding every instance.
The circuit-design lesson
An AIR constrains local relations between adjacent trace rows. Its local rule looks finite-state; its computational reach comes from the committed trace length and auxiliary memory arguments. A STARK proves one bounded execution. It cannot promise that an arbitrary program eventually halts without a bound or a separate termination proof.
The practical question comes first: what must the checker remember, and in what order must it read that information? Use a finite automaton for bounded history, a parser for nesting, a symbol table or memory-consistency argument for revisitable relationships, and an explicit execution bound when general computation enters the picture.
Read how Stwo proves a bounded trace → · Return to the architecture →