Reducibility & Undecidability

A reduction from problem A to problem B is a way of converting instances of A into instances of B such that the answer is preserved. Informally: if you have a black box that solves B, you can use it to solve A.

The formal definition: A mapping reduction (also called many-one reduction) from A to B, written A ≤_m B, is a computable function f such that for every string w:

w ∈ A ⟺ f(w) ∈ B

The function f is called the reduction function. It transforms instances of A into instances of B, preserving membership. Crucially, f must itself be computable — a Turing machine that always halts.

Intuition via analogy. Imagine you can only buy postage stamps, but you need to buy a bus ticket. If there exists a store that sells bus tickets in exchange for stamps at a fixed rate, you have 'reduced' the bus-ticket-buying problem to the stamp-buying problem. The reduction is the exchange rate. If you know stamp-buying is impossible (say, stamps no longer exist), then bus-ticket-buying via that mechanism is also impossible.

The key logical direction for undecidability:

• If A ≤_m B and A is undecidable, then B is undecidable.
• Equivalently (contrapositive): if B is decidable and A ≤_m B, then A is decidable.

The second form is the useful direction for proofs: to show B is undecidable, find a known-undecidable A and exhibit a computable f with the membership-preserving property above.

Do not confuse the direction. A ≤_m B means 'A reduces to B', meaning 'B is at least as hard as A'. The subscript 'm' stands for 'many-one': many inputs to A can map to the same input of B.

# Pseudocode: what a reduction LOOKS like as code
# We want to show PROBLEM_B is undecidable.
# We already know HALTING_PROBLEM is undecidable.
#
# Strategy: build a computable function f such that:
#   (P, x) halts  <=>  f(P, x) is in PROBLEM_B
#
# If PROBLEM_B were decidable by machine M_B, then:
def decide_halting(P, x):
    y = f(P, x)       # computable reduction
    return M_B(y)     # call the hypothetical decider
#
# But decide_halting cannot exist (Halting Problem is undecidable),
# so M_B cannot exist either. QED.

Before we can reduce other problems to known-undecidable ones, we need at least one undecidable problem as an anchor. That anchor is HALT_TM: the language of all pairs ⟨M, w⟩ where Turing machine M halts on input w.

Theorem (Turing, 1936): HALT_TM is undecidable.

The proof is the famous diagonalization argument. Suppose for contradiction there exists a TM H that decides HALT_TM. Construct a machine D:

D on input ⟨M⟩:
  Run H on ⟨M, ⟨M⟩⟩   (does M halt on its own description?)
  If H says HALT:  loop forever
  If H says LOOP:  accept (halt)

Now ask: what does D do on input ⟨D⟩?

• If D halts on ⟨D⟩, then H says HALT, so D loops — contradiction.
• If D loops on ⟨D⟩, then H says LOOP, so D halts — contradiction.

Both cases lead to contradiction, so H cannot exist.

A_TM (the acceptance problem) is equally important: does TM M accept input w? A_TM = {⟨M, w⟩ | M accepts w}. This is also undecidable (proved similarly). A_TM is actually Turing-recognizable (we can simulate M and accept if it accepts) but not decidable (we might run forever if M loops). Both HALT_TM and A_TM serve as starting anchors for future reductions.

The arithmetic analogy. Diagonalization is like Cantor's proof that the reals are uncountable. You construct something that 'disagrees with every row in an infinite table'. The table here is: row i = the i-th TM, column j = input j. D disagrees with every diagonal entry.

# Simulation: A_TM is Turing-recognizable but not decidable.
# This recognizer accepts <M, w> iff M accepts w.
# It may loop forever if M loops on w.

def recognize_ATM(M_description, w):
    """Turing-recognizable but NOT decidable."""
    # Run a universal TM simulator
    result = universal_simulator(M_description, w)
    # result is 'accept', 'reject', or (never returns) 'loop'
    if result == 'accept':
        return True
    # if M rejects, we reject; if M loops, we loop too
    return False

# There is NO algorithm that always terminates and correctly
# decides A_TM. The recognizer above can loop.

Let's walk through a complete, detailed reduction proof from scratch. Consider:

E_TM = {⟨M⟩ | M is a TM and L(M) = ∅}

That is: the set of TM descriptions whose language is empty (they accept nothing). We want to prove E_TM is undecidable.

Strategy: Reduce A_TM to E_TM. We'll show A_TM ≤_m E_TM by constructing a computable f such that:

⟨M, w⟩ ∈ A_TM ⟺ f(⟨M, w⟩) ∉ E_TM

(Note: here ⟨M, w⟩ ∈ A_TM means M accepts w, and f(⟨M, w⟩) ∉ E_TM means the resulting machine has a nonempty language. We need a gadget that 'encodes the acceptance question into the language'.)

The construction. Given ⟨M, w⟩, define a new TM M_w as follows:

M_w on input x:
  (Ignore x entirely)
  Simulate M on w
  If M accepts w: accept
  If M rejects w: reject

Now observe:

• If M accepts w: M_w accepts every input x (since it ignores x and accepts). So L(M_w) = Σ* ≠ ∅.
• If M does not accept w: M_w accepts no input. So L(M_w) = ∅.

Therefore: ⟨M, w⟩ ∈ A_TM ⟺ L(M_w) ≠ ∅ ⟺ ⟨M_w⟩ ∉ E_TM.

The reduction function f maps ⟨M, w⟩ ↦ ⟨M_w⟩. This is computable: given the description of M and the string w, we can write down the description of M_w (it's just 'hardcode w into the description, then simulate M on w, ignoring actual input'). The function f always terminates.

Conclusion: If E_TM were decidable, we could decide A_TM by: compute f(⟨M, w⟩) = ⟨M_w⟩, then call the E_TM decider, flip the answer. Since A_TM is undecidable, E_TM must be undecidable too.

Key lesson: The machine M_w is a gadget — a constructed machine that encodes the original question (does M accept w?) into its own language. Constructing clever gadgets like this is the core skill of reduction proofs.

# Pseudocode for the reduction function f
# Input: description <M> and string w (as a pair)
# Output: description of a new TM M_w

def reduction_f(M_description, w):
    """
    Builds the TM M_w that:
      - ignores its actual input x
      - runs M on the hardcoded w
      - accepts iff M accepts w
    """
    # We don't RUN M on w here — we just WRITE THE CODE for M_w.
    # M_w is a TM description (a string), not an execution.
    M_w_description = f"""
    TM M_w:
      ignore input
      simulate {M_description!r} on {w!r}
      if simulation accepts: accept
      if simulation rejects: reject
      (if simulation loops: loop)
    """
    return M_w_description  # computable, always terminates

# If decide_ETM existed:
def decide_ATM(M_description, w):
    M_w = reduction_f(M_description, w)
    return not decide_ETM(M_w)  # flip: E_TM decider flipped = A_TM decider
# But A_TM is undecidable => E_TM is undecidable.

Not all undecidable languages are equally 'hard'. There is a useful hierarchy:

1. Decidable (recursive): Some TM M always halts and correctly decides membership.
2. Turing-recognizable (recursively enumerable, r.e.): Some TM M halts and accepts if w ∈ L, but may loop or reject if w ∉ L.
3. Co-Turing-recognizable (co-r.e.): The complement of L is Turing-recognizable.
4. Neither: Some languages are not even recognizable.

Key theorem: L is decidable ⟺ L is both Turing-recognizable and co-Turing-recognizable.

Proof sketch: If L is decidable, run the decider; it always halts, so both L and its complement are recognizable. Conversely, if M_1 recognizes L and M_2 recognizes the complement, run both in parallel (interleave steps). Exactly one will eventually accept, telling you the answer.

A_TM is Turing-recognizable but NOT decidable. We can simulate M on w and accept if M accepts. But we can't always reject (we might loop).

The complement of A_TM (written Ā_TM) is NOT Turing-recognizable. Since A_TM is recognizable but not decidable, its complement cannot be recognizable (if it were, A_TM would be decidable by the theorem above). This means Ā_TM is 'harder' than A_TM in a precise sense.

Practical implication: E_TM is actually not Turing-recognizable (its complement EQ_TM is not recognizable either). These live at different levels of the arithmetical hierarchy — a topic that extends this module into graduate territory.

The complement trick for reductions: If A ≤_m B, then Ā ≤_m B̄ (complement both sides). This lets us transfer non-recognizability results. E_TM is co-Turing-recognizable (its complement — non-empty languages — is recognizable by dovetailing) but not recognizable, placing it outside the class of r.e. languages.

# Demonstrating the parallel-simulation trick that makes decidable = rec ∩ co-rec

def decide_if_both_recognizers_exist(M1, M2, w):
    """
    M1 recognizes L, M2 recognizes complement of L.
    We run both in parallel (round-robin simulation).
    One will eventually accept, giving us the answer.
    """
    for steps in range(1, float('inf')):
        # Simulate M1 for 'steps' steps on w
        if simulate(M1, w, max_steps=steps) == 'accept':
            return True   # w in L
        # Simulate M2 for 'steps' steps on w
        if simulate(M2, w, max_steps=steps) == 'accept':
            return False  # w not in L (complement recognized w)
    # One of them MUST accept eventually (they cover all cases)

Rice's Theorem is one of the most powerful and surprising results in all of theoretical computer science.

Definition. A semantic property of TMs (or programs) is one that depends only on the language that the TM computes — i.e., on L(M) — rather than on the mechanical details of how M is built. Examples of semantic properties:

• 'M accepts the string "hello"'
• 'L(M) is finite'
• 'L(M) = ∅'
• 'L(M) contains a prime-length string'
• 'M computes the same function as some fixed TM M_0'

A trivial property is one that is either true for ALL TMs or false for ALL TMs. A non-trivial property is one where some TMs have it and some don't.

Rice's Theorem: Every non-trivial semantic property of Turing machines is undecidable.

Equivalently: Let P be any non-trivial property of languages. The set {⟨M⟩ | L(M) ∈ P} is undecidable.

Proof sketch. Let P be a non-trivial semantic property. WLOG assume the TM T_∅ (which accepts nothing) does NOT have property P (if it does, use the complement). Since P is non-trivial, there exists some TM T that DOES have property P.

We reduce A_TM to the property-P language. Given ⟨M, w⟩, construct:

M_w on input x:
  Simulate M on w
  If M accepts w: simulate T on x (accept iff T accepts)
  If M rejects w: reject

Now:

• If M accepts w: M_w behaves exactly like T, so L(M_w) = L(T). Since T has property P, so does M_w.
• If M does not accept w: M_w accepts nothing, so L(M_w) = ∅. Since T_∅ does NOT have property P, M_w does not have property P.

So ⟨M, w⟩ ∈ A_TM ⟺ ⟨M_w⟩ ∈ {⟨M'⟩ | L(M') ∈ P}.

This is a valid mapping reduction A_TM ≤_m P_language. Since A_TM is undecidable, P_language is undecidable.

Scope of the theorem. The theorem applies to ALL semantic properties simultaneously. You cannot write an algorithm that correctly detects any non-trivial behavior of an arbitrary program. This is why:

• Perfect virus detection is impossible (virus behavior is semantic)
• Perfect termination analysis is impossible
• Perfect equivalence checking is impossible
• Any complete, sound static analyzer for non-trivial properties must approximate

What Rice's Theorem does NOT say: It does NOT say we can learn nothing about programs. Syntactic properties (like 'the source code contains the word "goto"') CAN be decided. Approximations (sound over-approximations or under-approximations) CAN be computed. It only says exact, complete semantic decisions are impossible.

# Rice's Theorem: proof gadget (same structure as E_TM proof, generalized)
# P is any non-trivial semantic property
# T is a TM with property P
# T_empty has no property P (WLOG)

def reduction_for_rice(M_description, w, T_description):
    """
    Builds TM M_w such that:
      L(M_w) has property P  <=>  M accepts w
    """
    M_w_description = f"""
    TM M_w on input x:
      Step 1: Simulate {M_description!r} on {w!r}
              (ignore x during this simulation)
      Step 2: If simulation accepted:
                simulate {T_description!r} on x
                accept/reject as T does
              If simulation rejected:
                reject x unconditionally
    """
    # L(M_w) = L(T) if M accepts w  [has property P]
    # L(M_w) = {} if M rejects w   [no property P]
    return M_w_description

# CONSEQUENCE: No program can decide any non-trivial semantic property.
# This is why static analyzers must use approximation (abstract interpretation,
# type systems, model checking with bounds, etc.).

Once we have A_TM and HALT_TM as anchors, and the proof technique in hand, we can show that a rich ecosystem of natural problems is undecidable. Here is the standard canon, organized by the reduction technique used:

Problems about TM languages:

The Post Correspondence Problem (PCP): Given two lists of strings (A = [a1,...,ak], B = [b1,...,bk]), does there exist a nonempty sequence of indices i1, i2, ..., im such that a_{i1}a_{i2}...a_{im} = b_{i1}b_{i2}...b_{im}? PCP is undecidable, proved by reducing A_TM to it. PCP is famously useful as an intermediate in other reductions (e.g., proving ambiguity of CFGs is undecidable).

Hilbert's Tenth Problem: Given a polynomial with integer coefficients in multiple variables, does it have an integer solution? Undecidable (Matiyasevich, 1970), after 23 years of work by Davis, Putnam, and Robinson. This was Hilbert's 10th problem from 1900.

Program equivalence: Given two programs P1 and P2 (both taking no input), do they always produce the same output? Undecidable by Rice's Theorem.

The reduction diagram (see diagram section) shows how these reductions flow: A_TM is at the base, and everything else is reached by reduction chains.

A note on historical context: All of these results were proved in the 1930s-1970s, during the founding era of theoretical computer science. Turing, Church, Gödel, Post, and Rice established the landscape of what is and is not computable before modern computers were even built.

# Post Correspondence Problem — a classic undecidable problem
# Easy to state, hard to solve, proves many other things undecidable

from itertools import product

def try_pcp(dominos, max_len=10):
    """
    Dominos: list of (top, bottom) string pairs.
    Tries to find a sequence of indices (with repetition)
    such that concatenating tops == concatenating bottoms.
    This is NOT a decider — it may miss solutions or loop.
    """
    # Example: dominos = [('ab','a'), ('b','abab'), ('aba','b')]
    # Solution: indices [2,1,2,0,0] -> 'aba'+'ab'+'aba'+'ab'+'ab'
    #                                  = 'b'+'a'+'b'+'abab'+'a'
    #                                  Hmm, need to verify...
    for length in range(1, max_len + 1):
        for indices in product(range(len(dominos)), repeat=length):
            top = ''.join(dominos[i][0] for i in indices)
            bot = ''.join(dominos[i][1] for i in indices)
            if top == bot:
                return True, list(indices)
    return None, []  # may not mean NO solution exists!

# The point: No algorithm can always correctly decide PCP.

Let's prove HALT_TM is undecidable from scratch using a reduction from A_TM. This full proof illustrates every step of the template.

Theorem: HALT_TM is undecidable.

Proof. Assume for contradiction that TM R decides HALT_TM. We build a TM S that decides A_TM:

S on input ⟨M, w⟩:
  1. Run R on ⟨M, w⟩
  2. If R says 'does not halt': reject (M can't accept if it doesn't halt)
  3. If R says 'halts': simulate M on w until it halts
     - If M accepts: accept
     - If M rejects: reject

Analysis:

• If M accepts w: M halts on w (since acceptance implies halting), so R says 'halts'. We simulate M and it halts accepting. S accepts. Correct: ⟨M,w⟩ ∈ A_TM.
• If M rejects w: M halts on w rejecting. R says 'halts'. We simulate M and it halts rejecting. S rejects. Correct: ⟨M,w⟩ ∉ A_TM.
• If M loops on w: M does not halt. R says 'does not halt'. S rejects. Correct: ⟨M,w⟩ ∉ A_TM.

In all cases S correctly decides A_TM. But A_TM is undecidable. Contradiction. So R cannot exist.

The template, explicitly:

1. State what you're proving: HALT_TM is undecidable.
2. Assume the opposite: Assume R decides HALT_TM.
3. Construct a machine for the known-undecidable problem using R as a subroutine.
4. Verify the construction is correct (case analysis).
5. Apply contradiction with the known undecidability result.

Important distinction: The reduction here goes A_TM ≤_m HALT_TM, meaning we reduced from A_TM to HALT_TM. This means HALT_TM is at least as hard as A_TM. Both are undecidable. The direction of the arrow tells you what follows: if HALT_TM were easy (decidable), then A_TM would be easy too. It is not, so HALT_TM is not.

# The HALT_TM undecidability proof, as executable pseudocode

# Assume for contradiction:
def decide_HALT(M_description, w) -> bool:
    """Hypothetical decider: returns True iff M halts on w."""
    pass  # Does not exist, but assume it does for contradiction

# Then we could build:
def decide_ATM(M_description, w) -> bool:
    """Supposedly decides A_TM using decide_HALT."""
    if not decide_HALT(M_description, w):
        # M doesn't halt on w => can't accept
        return False
    # M halts on w — now simulate it (safe: guaranteed to terminate)
    result = simulate_until_halt(M_description, w)
    return result == 'accept'

# But decide_ATM cannot exist (A_TM is undecidable by diagonalization)
# Therefore decide_HALT cannot exist either.
# QED.

One important and elegant proof technique is using computation histories. A computation history of TM M on input w is the sequence of configurations:

C_0, C_1, C_2, ..., C_halt

where C_0 is the initial configuration, each C_{i+1} follows from C_i by one step of M's transition function, and C_halt is an accepting or rejecting configuration.

Why are computation histories useful? They let us encode the entire execution of a TM into a string, and then check properties of that execution using simpler computational models like CFGs or LBAs.

The key undecidability result via histories: A_LBA (does LBA M accept input w?) is decidable — because an LBA on an input of length n can only be in finitely many configurations (bounded by n × |states| × |tape alphabet|^n), so we can bound the simulation. But E_LBA (does LBA M have empty language?) is undecidable — proved by encoding A_TM computation histories into the LBA's language.

All_CFG and EQ_CFG: Using computation histories, we can show:

• ALL_CFG = {⟨G⟩ | L(G) = Σ*} is undecidable (every string is in the CFG's language).
• EQ_CFG = {⟨G1, G2⟩ | L(G1) = L(G2)} is undecidable.

The proof: given ⟨M, w⟩, build a CFG G_{M,w} that generates ALL strings EXCEPT valid accepting computation histories of M on w. Then L(G_{M,w}) = Σ* iff M does NOT accept w. So if ALL_CFG were decidable, we could decide A_TM.

Lesson: Computation histories bridge the gap between TM undecidability and context-free / bounded-memory models. They show that even seemingly 'smaller' formalisms encode enough TM behavior to inherit undecidability for certain questions.

# A computation history encoded as a string:
# Configuration format: (state, tape_content, head_position)
# History: C0 # C1 # C2 # ... # Cacc
# where # is a separator not in the tape alphabet

# Example: TM that moves right once and accepts
# Input: 'ab'
# History might look like:
# q0 a b  #  a q1 b  #  a b q_acc
#
# Checking if a string is a VALID accepting computation history
# can be done by a deterministic TM (check each step follows rules)
# But checking if ANY valid accepting history EXISTS for (M, w)
# is equivalent to asking if M accepts w — undecidable in general.

def is_valid_history(history_string, M_description, w):
    """
    Checks if history_string is a valid accepting computation
    history for M on w. This specific function IS decidable —
    we just check each step.
    But: 'does there EXIST a valid history?' is A_TM — undecidable.
    """
    configs = history_string.split('#')
    if not is_initial_config(configs[0], M_description, w):
        return False
    for i in range(len(configs) - 1):
        if not is_valid_step(configs[i], configs[i+1], M_description):
            return False
    return is_accepting_config(configs[-1], M_description)

Undecidable problems are not all equally 'hard'. The study of their relative difficulty is called computability theory or recursion theory, and it reveals a rich, infinite hierarchy.

The arithmetical hierarchy classifies problems by the number of alternating quantifiers needed to express them:

• Σ_1^0 (recursively enumerable, r.e.): Problems of the form ∃x. R(w, x) where R is decidable. Equivalently: Turing-recognizable. Examples: A_TM, HALT_TM.
• Π_1^0 (co-r.e.): Complements of r.e. sets. Examples: Ā_TM.
• Σ_2^0: Problems of the form ∃x ∀y. R(w, x, y). Example: TOTAL_TM = {⟨M⟩ | M halts on all inputs}.
• Π_2^0: ∀x ∃y. R(w, x, y). Example: HALT-on-all = complement of TOTAL.
• And so on, infinitely many levels.

Turing reducibility (≤_T) is more general than mapping reduction (≤_m): A ≤_T B if there is a TM with oracle for B that decides A. Turing reductions give a finer hierarchy (the Turing degrees or Degrees of Unsolvability). Turing himself introduced this in 1939, followed by Post's work on intermediary degrees.

The Halting Problem is Turing-complete for r.e. sets: Every Turing-recognizable set reduces to HALT_TM by a mapping reduction. HALT_TM is thus a 'hardest' r.e. set.

Why this matters practically: The arithmetical hierarchy explains why some static analysis tools are 'more approximate' than others. Questions at the Σ_2^0 level (like 'does this program halt on ALL inputs?') are provably harder than questions at Σ_1^0 (like 'does this program halt on THIS input?'), requiring strictly more quantifier alternation to even express.

Gödel's incompleteness theorems are closely related: the undecidability of A_TM implies the first incompleteness theorem — any consistent, sufficiently powerful formal system cannot prove all true statements about Turing machines. Undecidability and unprovability are two sides of the same coin.

# The arithmetical hierarchy, visually
#
# Level    Complexity class    Example problem
# ------   ----------------    ---------------
# Σ_1^0    RE (r.e.)           A_TM, HALT_TM  (recognizable)
# Π_1^0    co-RE               complement of A_TM (co-recognizable)
# Σ_2^0    RE relative to 0'   TOTAL_TM (halts on all inputs)
# Π_2^0    co-RE relative to 0'  complement of TOTAL_TM
# Δ_1^0    Decidable           All decidable problems
# Δ_2^0    TM w/ Halting oracle  0' (the halting set)
#
# TOTAL_TM = { <M> | M halts on every input w }
# This is Π_2^0: ∀w ∃t. M halts on w within t steps
# Two alternating quantifiers => harder than A_TM
#
# This is why testing 'does my program terminate on all inputs'
# is STRICTLY harder than testing 'does it terminate on this input'

Undecidability and Rice's Theorem are not merely theoretical curiosities. They have direct, concrete implications for software development, security, and AI.

Static analysis and compilers: Every production static analyzer (clang-tidy, ESLint, mypy, FindBugs, etc.) is an approximation. It cannot be both sound (never misses a real bug) AND complete (never flags a non-bug) for any non-trivial property. This is Rice's Theorem. In practice, most tools choose to be sound (may over-approximate: report false positives) or complete (may under-approximate: miss some bugs), but not both.

Type systems: Type systems are decidable approximations of semantic properties. A type system that rejects a program is saying 'I can't prove this is safe', not 'this is definitely unsafe'. The soundness/completeness tradeoff is exactly the approximation forced by undecidability.

Antivirus and malware detection: Detecting whether an arbitrary program is a virus is a semantic property (it concerns behavior, not structure). By Rice's Theorem, it is undecidable. This is why antivirus tools use heuristics, signatures (syntactic), and sandboxing (empirical execution) rather than proofs.

Program verification (formal methods): Tools like Coq, Lean, TLA+, and Dafny can prove properties of specific programs, but they require human guidance (proof writing) precisely because the automatic version is undecidable. The human provides the 'oracle' that circumvents undecidability for specific instances.

AI code analysis: AI tools that claim to detect bugs in arbitrary code are — by Rice's Theorem — necessarily making approximations or only working on specific, bounded instances. Any claim of completeness and soundness for a non-trivial semantic property is mathematically impossible.

The 'silver lining' of approximation: Undecidability does not mean 'hopeless'. Abstract interpretation (Cousot & Cousot, 1977) gives a rigorous framework for sound approximations. SAT-based bounded model checking can prove properties for bounded execution lengths. These are principled, theoretically-grounded approximations that are extremely valuable in practice — they just cannot be exact.

# Abstract interpretation: a principled approximation of undecidable properties
# Example: sign analysis (is this variable always positive/negative/zero?)
# This is an APPROXIMATION of the actual runtime value

# The abstract domain: {POS, NEG, ZERO, TOP, BOT}
# TOP means 'could be anything' (safe over-approximation)
# BOT means 'unreachable'

def abstract_add(sign1, sign2):
    """Approximate addition in the sign domain."""
    if sign1 == 'BOT' or sign2 == 'BOT': return 'BOT'
    if sign1 == 'TOP' or sign2 == 'TOP': return 'TOP'
    if sign1 == 'POS' and sign2 == 'POS': return 'POS'
    if sign1 == 'NEG' and sign2 == 'NEG': return 'NEG'
    if sign1 == 'ZERO': return sign2
    if sign2 == 'ZERO': return sign1
    return 'TOP'  # POS+NEG, etc. — could be anything

# SOUND: if concrete value is +5, abstract value is POS.
# NOT COMPLETE: x=5+(-5)=0 gives TOP, not ZERO.
# Rice's Theorem guarantees we cannot do better in general.
# But for MANY programs, this approximation proves useful properties.