Automata and computability bridge
Prerequisites: sets and functions, induction and contradiction, recursive programs, and this module's reduction-direction lesson. Repair those specific skills before continuing. This bridge supplies a missing link between executable algorithms and limits on algorithms; it is not a full theory-of-computation course.
Required additional effort: 20–30 hours: finite-state and language reasoning 5–7; decidability and reduction proofs 5–8; implementation and independent comparison 6–9; assessment, changed case and delayed repair 4–6. Module 6 is now 45–65 hours, retaining its original 25–35-hour complexity package. Estimates await learner pilots.
Lesson 1: state means the history still matters
A language is a set of finite strings over an alphabet. A deterministic finite automaton (DFA) has a finite state set, start state, accepting states and a total transition function from state/symbol pairs to states. It accepts only if its state after the entire input is accepting. The empty string therefore tests the start state; it does not mean a missing input.
For binary strings ending in 01, use three states: q0 means no useful suffix, q1 means the current suffix is 0, q2 means the current suffix is 01. Starting in q0, on 0 every state goes to q1. On 1, q1 goes to q2 while q0 and q2 go to q0. Only q2 accepts. These states summarize exactly what a future suffix needs to know, not the full previous input.
Trace 001, 010 and the empty string. Prove by induction that each transition preserves the stated suffix meaning; concluding acceptance then follows from the invariant. An accepting prefix is not enough: 01 accepts, but 011 rejects. A recognizer returning immediately at q2 is wrong.
A DFA consumes one transition per symbol and has constant state storage; the input representation may itself occupy linear memory. Validate the alphabet separately: malformed input should not silently acquire a new transition. Many practical regex engines add features outside regular languages, so do not infer the engine's expressive power or running time solely from the word “regex.”
Practice: construct the four-state product machine that accepts binary strings with an even number of 0s and an even number of 1s. State the meaning of each parity pair, start/accepting state and all eight transitions. Check 00, 01, 0011 and the empty string before proving its invariant.
Lesson 2: why nesting needs growing memory
Consider L consisting of a^n b^n for n at least zero. Suppose a DFA with N states recognizes it. Among N+1 prefixes a^0 through a^N, two distinct lengths i<j reach the same state. Append b^i to both. Determinism gives identical final states, yet a^i b^i belongs to L and a^j b^i does not. This contradiction proves no finite DFA recognizes L. Testing a million examples would not prove that statement.
A recognizer with an unbounded counter can decide this particular language: count initial a symbols, then decrement for b symbols, reject negative counts or any a after a b, and accept only at zero after all input. Each finite input terminates. In a bit-cost model the counter needs logarithmically many bits in the input length; it is not a fixed finite-state machine.
For nested parentheses of two types, counts alone lose ordering and type. ([)] has matching counts but is invalid nesting. A stack records pending openers; each closer must match the top. A grammar describing exactly these strings is S -> (S)S | [S]S | epsilon. Each production creates one correctly matched outer pair followed by another balanced string. An implementation must also reject unmatched openers at end of input.
The stack algorithm takes linear time under constant-cost stack operations and up to linear stack space. A fixed depth limit changes the accepted language; do not call rejection at that limit a proof of invalid unrestricted nesting. Hardware memory is finite, while the mathematical language ranges over arbitrarily long finite strings.
Practice: explain why equal opener/closer totals fail on )( and why ignoring bracket type fails on ([)]. Transfer the grammar and stack invariant to a third bracket type. Preserve the distinction between a mathematical limit and an implementation resource guard.
Lesson 3: termination is a separate question from speed
A decider halts on every input and returns membership yes or no. A recognizer must halt and accept members; on a nonmember it may reject or run forever. “The program has not accepted yet” is not a negative answer. Our DFA and bracket checker are deciders because they finish a finite scan.
Assume a total algorithm H(P,x) decides whether program P eventually halts on input x. Construct D(y): if H(y,y) says halts, loop forever; otherwise halt. Since programs have encodings, run D on its own encoding d. If H(d,d) says halts, D loops; if it says does not halt, D halts. Both contradict correctness. Thus no such universal total H exists in the general computation model. This does not prevent proving termination of many particular programs or deciding bounded execution questions.
For a reduction, suppose R decides whether an arbitrary program ever prints the marker READY. Given P,x, construct Q that simulates P(x), discards its output, and prints READY only if the simulation halts. Q prints READY if and only if P(x) halts. The transformation is computable and a call to R would decide halting, so universal R cannot exist. Both implications and the discarded output matter; otherwise P might print READY before looping and break the construction.
SAT and finite Vertex Cover are decidable: enumerate finitely many assignments or subsets and check them. NP-completeness is not undecidability. Polynomial-time hardness reductions in the earlier lessons also carry cost constraints; this computability argument only needs a total computable transformation. A timeout in exact search means unresolved, not infeasible and not “proven undecidable.”
Practice: critique a tool promising to correctly classify every arbitrary program as “never divides by zero” or “will divide by zero,” always terminating. Reduce halting by simulating P(x) safely and deliberately dividing by zero only after it halts. State the general-program assumptions and why practical restricted analyzers can still be useful.
Runnable language laboratory
Download the original reference experiment. Extract it and run python3 experiment.py. Python 3.9+ and the standard library suffice; no external service is used. It checks a suffix DFA and two-type bracket stack against independent bounded oracles. Read the README for contracts and limits. The reference is an example, not learner evidence.
Before looking at implementation, write predictions for the named boundary strings. Then implement your own parity-product DFA and three-bracket checker. Build an independent oracle, enumerate all short strings with a declared length bound, and preserve mismatches and corrections. Test invalid alphabet/type cases separately. Report number of strings, maximum length, costs and what these finite checks cannot establish. Re-run from a fresh directory with documented commands.
Independent gates and calibration
Use the existing 0–3 rubric: 0 invalid/missing; 1 assisted/incomplete; 2 independently correct with assumptions and evidence; 3 also adapts and defends a changed case. All AC1–AC4 require 2, in addition to CA1–CA6. Store attempts before opening the reference/calibration. After 7–14 days repeat one language proof and one limits question with changed inputs; this is included in the 4–6-hour assessment allowance.
- AC1, finite state: implement the parity-product DFA, defend state meanings and induction, and trace a fresh input. Calibration: start and sole accept state (even,even); reading 0 toggles only the first parity, reading 1 only the second. Four parity states suffice. “Tests pass” without an invariant is level 1 at best.
- AC2, language boundary: reproduce the distinct-prefix argument for a^n b^n; implement the three-bracket transfer with independent checks. Calibration: choose N+1 prefixes for N states and append the SAME b^i suffix; mismatched closer and nonempty final stack both reject. A different suffix for each prefix does not establish the contradiction.
- AC3, impossibility: reconstruct the diagonal argument and marker reduction, with both directions and effective construction. Calibration: suppress simulated output; only halting triggers the marker. A finite test corpus cannot certify an impossibility theorem, and proof by “programs are complicated” is invalid.
- AC4, engineering interpretation: classify DFA membership, SAT, unrestricted halting and a solver timeout; explain what a restricted analyzer can honestly guarantee. Calibration: first two decidable, third undecidable, timeout unresolved. NP-hard is not synonymous with impossible. Fresh transfer: a depth-limited bracket service must distinguish its documented domain/resource limit from unrestricted grammatical validity.
For a failure, repair only the affected invariant, proof direction or contract, then attempt a fresh task without the key. Label solo scoring self-assessed; technical review, reviewer agreement and timing pilots remain pending. The semester project reuses this packet rather than inventing an unrelated parser in the planner.
Selective resources
Use MIT 6.045J lecture notes: lectures 3–5 for finite automata/nonregularity, 6–9 for machines, decidability and mapping reductions. Read the relevant section after a specific failed task; the entire course is optional depth. These primary course materials were checked on 2026-10-23.
Optional book: Michael Sipser, Introduction to the Theory of Computation, sections on regular languages, context-free languages, decidability and reducibility in the edition you have. Borrow or use existing lawful access; purchase is not required. The free course and original local lessons suffice. No book transcription or full-book reading is assigned. NFA-to-DFA conversion, pumping-lemma practice, general parsing and Rice's theorem are later depth, not silently claimed as completed here.