Computation history of a Turing machine

A computation history of M on w is the full sequence of configurations the TM passes through, written as a single string with separators:

Each configuration C_i records the entire state of the computation at one moment: the tape contents, the head position, and the current control state. Convention (Sipser §5.1): write the state symbol inside the tape, immediately to the left of the head cell. So if M is in state q₃ with head at position 4 on tape "01100", we write C = 0110 q₃ 0. State + head + tape, all encoded in one string of constant local width.

Why this matters: humble machine models (LBAs, CFGs, even some restricted NFAs) can perform local checks. They cannot simulate a full TM, but they can verify that someone's claimed computation history is genuine. This is the engine behind E_LBA undecidability (Problem 10) and ALL_CFG undecidability (Problem 11).

This is the "local checkability" claim made concrete. A change of configuration affects at most three cells (one head cell plus its two neighbours, since the head can move left or right). Verifying a step means reading those three cells in C_i, checking that the corresponding three cells in C_i+1 match what δ prescribes. No global memory needed.

• The state inside the tape is part of the string. Encoding C_i = 0110q₃0 means the q₃ symbol literally appears in σ between the 4th and 5th tape symbols. The alphabet of σ is Γ ∪ Q (tape symbols + state symbols).
• "Computation history" implies halting. If M loops on w, there's no accepting computation history — the string σ doesn't exist. Reductions exploit exactly this: M accepts w iff some valid σ exists.
• Local checks ignore time order direction. The 2×3 window check works left-to-right or right-to-left — the constraint is symmetric. That's why CFGs (which can derive in any order) and LBAs (which can scan in any direction) can verify them.
• Don't confuse "verify" with "produce." An LBA or CFG can verify someone hands you a candidate history. It cannot generate all histories without knowing how to simulate M — but it doesn't need to, because the existence of any accepting history is enough.

• Q1. Why insert the state inside the tape?
  A configuration must capture tape contents, head position, and state in one string. Writing the state symbol immediately before the head cell encodes all three compactly and lets the 2×3 window detect head movement directly — the state symbol shifts left or right between C_i and C_i+1.
• Q2. Why is local checkability so powerful?
  It bridges Turing power and humbler models. LBAs / CFGs can verify a 2×3 window but cannot count globally. Local checking is in their power; full TM simulation isn't. Computation histories let undecidable TM questions hide inside emptiness or universality questions about LBAs and CFGs.
• Q3. Why doesn't this trick make A_TM decidable?
  The verification direction goes outward, not inward. We don't decide A_TM by checking histories — we reduce from A_TM to LBA/CFG questions. The undecidability of A_TM flows into the LBA/CFG questions, making them undecidable too.
• Q4. What if M loops on w?
  No finite accepting computation history exists. The reduction's target language is empty in that case (no history to accept), which is exactly the information we want — "M loops or rejects on w" corresponds to "the LBA accepts no history."
• Q5. Could we use a different separator instead of #?
  Yes — any symbol not in Γ ∪ Q works. # is convention because it's visually clean. The choice doesn't affect the construction.

Sipser: §5.1 introduces computation histories formally; Theorem 5.10 (E_LBA) and Theorem 5.13 (ALL_CFG) apply them. Lecture notes: Module 3 slides 1–4 use the same picture. Companion problems: P10 (E_LBA) and P11 (ALL_CFG) are direct applications of this technique.