Decidability, Reductions & Rice's Theorem

Decidability theory draws a sharp line: some problems have no algorithmic solution, not because we haven't found one yet, but because it's been mathematically PROVEN that none can exist.

Key decidability results:

DECIDABLE (algorithms exist):
- ATM complement: is this DFA equivalent to that DFA? → YES, decidable
- Does this CFG generate the empty language? → decidable
- Does this DFA accept any strings? → decidable (check if accept state reachable)
- Is this number prime? → decidable (Miller-Rabin, AKS)
- Does this regex match this string? → decidable

UNDECIDABLE (proven impossible):
- ATM = {⟨M, w⟩ | TM M accepts input w} — the ACCEPTANCE problem. Recognizable but not decidable.
- HALTTM = {⟨M, w⟩ | TM M halts on w} — the HALTING problem.
- ETM = {⟨M⟩ | L(M) = ∅} — does TM accept NO strings?
- EQTM = {⟨M1,M2⟩ | L(M1) = L(M2)} — do two TMs accept same language?
- REGULARTM = {⟨M⟩ | L(M) is regular} — undecidable!
- Does program P have a bug? → undecidable in general

Mapping Reductions (A ≤m B — A reduces to B):
A computable function f such that: w ∈ A ↔ f(w) ∈ B
- If B is decidable and A ≤m B → A is decidable
- If A is undecidable and A ≤m B → B is undecidable
- Standard technique: to prove X is undecidable, show ATM ≤m X

Rice's Theorem — the most powerful undecidability result:
"Any non-trivial property of the language recognized by a TM is undecidable."
Non-trivial: some TMs have it, some don't.
Examples of non-trivial properties:
- Does TM accept the empty string?
- Does TM accept any string?
- Does TM accept all strings?
- Is the language regular? Context-free? Finite?
- Does TM halt in fewer than 1000 steps on some input?
ALL of these are undecidable by Rice's Theorem.

Practical implications:
- No perfect static analysis tool (cannot detect all bugs)
- No perfect malware detector (malware detection reduces to halting problem)
- No perfect type inference for all programs (some type systems undecidable)
- No perfect program equivalence checker
- Software verification is fundamentally limited

What we CAN do (approximations):
- Bounded model checking: check for bugs up to depth k
- Abstract interpretation: over-approximate program behavior (may have false positives)
- Type systems: conservative — reject some correct programs but catch many bugs
- Fuzzing: find bugs probabilistically, not exhaustively

1# Exploring decidability limits
2
3# ── Semi-decision: recognize but not decide ────────────
4def attempt_acceptance(program_str, input_str, max_steps=1000):
5    """
6    Simulates trying to decide if a program accepts input.
7    Returns True if accepted, None if exceeded max_steps (may loop).
8    This is the BEST we can do — we can never return False with certainty.
9    """
10    # In reality we'd simulate a TM — here we simulate symbolically
11    print(f"Running program on '{input_str}' for up to {max_steps} steps...")
12    # We cannot know if it will EVER halt...
13    return None   # "I don't know" is the honest answer
14
15# ── Rice's Theorem demonstration ──────────────────────
16print("Rice's Theorem — undecidable program properties:
17")
18
19# These LOOK like they should be analyzable — but they're not
20programs = {
21    "def f(x): return x + 1":                 "Computes x+1?",
22    "def f(x):
23  while x>0: x-=1
24  return 0": "Halts on positive input?",
25    "def f(x): return x % 2 == 0":            "Returns True for even numbers?",
26    "def f(x):
27  while True: pass":          "Ever returns?",
28}
29
30for prog, question in programs.items():
31    print(f"  Q: {question}")
32    print(f"  Program: {prog[:50]}...")
33    print(f"  Decidable in general? NO — Rice's Theorem applies")
34    print()
35
36# ── What static analysis CAN do (approximations) ──────
37print("What we CAN do (conservative approximations):
38")
39
40import ast
41import sys
42
43def static_checks(code: str):
44    """Conservative checks — may have false positives, no false negatives"""
45    issues = []
46    try:
47        tree = ast.parse(code)
48    except SyntaxError as e:
49        return [f"Syntax error: {e}"]
50
51    for node in ast.walk(tree):
52        # Check for division by zero (simple case only)
53        if isinstance(node, ast.BinOp) and isinstance(node.op, ast.Div):
54            if isinstance(node.right, ast.Constant) and node.right.value == 0:
55                issues.append("Possible division by zero")
56
57        # Check for undefined variable (very simplified)
58        if isinstance(node, ast.Name) and isinstance(node.ctx, ast.Load):
59            pass  # real analysis needs scope tracking
60
61        # Detect obvious infinite loop
62        if isinstance(node, ast.While):
63            if isinstance(node.test, ast.Constant) and node.test.value:
64                issues.append("Possible infinite loop: while True")
65
66    return issues or ["No obvious issues found"]
67
68test_codes = [
69    "x = 1 / 0",
70    "while True:
71    pass",
72    "x = 5
73y = x + 1",
74]
75
76for code in test_codes:
77    issues = static_checks(code)
78    print(f"  Code: {code!r[:40]}")
79    for issue in issues:
80        print(f"  ⚠ {issue}")
81    print()
82
83print("Key insight: these checks are SOUND (no false negatives for what they check)")
84print("but INCOMPLETE (they miss many real bugs) — Rice's Theorem explains why.")