E_LBA is undecidable

An LBA (linear bounded automaton) is a TM restricted to use only the cells of its input — no scratch space outside the original |w| cells. Two surprising facts sit side by side:

• A_LBA = {⟨B, w⟩ : LBA B accepts w} is decidable. Because B is space-bounded by |w|, only finitely many distinct configurations exist. Simulate B and if you see a config repeat, B is looping — reject. Otherwise B halts.
• E_LBA = {⟨B⟩ : L(B) = ∅} is undecidable. Emptiness asks "is there any input B accepts?" — that's a quantifier over all strings, including very long ones with their correspondingly large state spaces.

The reduction A_TM ≤_m ¬E_LBA exploits computation histories from Problem 9.

Key claim: L(B_M,w) ≠ ∅ iff M accepts w. The forward direction is direct — if M accepts w, write down its accepting computation history σ, and B_M,w(σ) succeeds. The reverse direction uses determinism: any string x accepted by B_M,w is the genuine accepting history of M on w, which witnesses ⟨M, w⟩ ∈ A_TM.

Each sweep is a finite-state walk across the input. The hard work — producing the history — is offloaded onto whoever provides x. B_M,w only validates. That is exactly the LBA's job description.

• The construction is f, not the LBA's execution. The reduction is a syntactic transformation: given ⟨M, w⟩, write down the description of B_M,w. We're not running anything during the reduction. The actual LBA run only happens later if an E_LBA-oracle is invoked.
• L(B_M,w) ≠ ∅ is the answer. The reduction goes to ¬E_LBA. ⟨M, w⟩ ∈ A_TM ⇔ ⟨B_M,w⟩ ∉ E_LBA. Don't lose the negation.
• The hard part is M's history, but B doesn't pay for it. Generating an accepting computation history requires simulating M — which an LBA can't do in general. But the LBA doesn't generate; it only checks. The input x is given. This separation is the whole technique.
• "Linear bounded" means linear in the input. B_M,w's tape size scales with the size of the candidate history x, not with anything fixed at construction time. A long-running M produces long histories — but those long histories are themselves long inputs x, so the LBA still has enough space (proportional to |x|).

• Q1. Why CAN an LBA check accepting computation histories?
  Each of the four checks is local: parsing the # separators, matching the start config (a constant-size pattern at the beginning), validating each (C_i, C_i+1) δ-step in a 2×3 window, and checking the accept state at the end. Local checks fit in finite-state control plus a few sweeps over the original tape — that is exactly the LBA budget.
• Q2. Why is A_LBA decidable but E_LBA isn't?
  A_LBA takes a specific input w and asks whether B accepts that specific w. Because B is space-bounded by |w|, only finitely many distinct configurations exist on that input — at most |Q| · |w| · |Γ|^|w|. Simulate and detect cycles. E_LBA asks whether B accepts any input — a quantifier over infinitely many strings, with no a-priori space bound to fall back on.
• Q3. What's the bound on an LBA computation history size?
  An LBA on input of length n has at most |Q| · n · |Γ|ⁿ distinct configurations. If any repeats, the LBA is in a loop — that's how A_LBA's decider catches non-halters. The exponential dependence on n is fine; it's still finite for each fixed n.
• Q4. Does this also prove ALL_LBA undecidable?
  Yes. Take the same reduction and complement the LBA — accept the strings B_M,w rejects. Then "language is everything" replaces "language is empty" with the negation flowing through. Many natural LBA properties (regularity, finiteness) collapse this way; this is the LBA analog of Rice's theorem.
• Q5. Why does the reduction use B_M,w instead of just simulating M?
  An LBA cannot simulate an arbitrary TM — that would require unbounded scratch space. The LBA verifies a candidate history, which lives entirely within the input length. The crucial separation: compute vs verify.

Sipser: §5.1, Theorem 5.10 (E_LBA is undecidable). Lecture notes: Module 3 slides 2–3 (LBA definition, B_M,w construction). Companion problems: P9 (computation histories — prerequisite), P11 (ALL_CFG — sibling technique using CFGs instead of LBAs), P62 (A_LBA vs E_LBA).