W07: The reach and limits of computational proof

Prerequisites and observable goals#

The central question: which class of objects is being decided?#

A program that checks every state of a finite model may prove a property of that model. It does not thereby decide the property for every unbounded program. A language that cannot be recognized by a finite automaton may still have a simple stack algorithm. A problem believed computationally difficult can still be decidable. These distinctions matter in compiler tooling, protocol verification, security review, and algorithm selection.

State the input class, acceptance condition, and resource measure before using a word such as “impossible.” Three claims are different: no machine of a specified restricted kind solves the task; no algorithm always decides the task for arbitrary inputs; and no known efficient algorithm solves the task under a specified complexity model. A finite counterexample can refute a universal claim; a million successful cases cannot establish an arbitrary universal statement without a covering argument.

A finite automaton carries only a finite summary#

A deterministic finite automaton (DFA) consists of a finite state set $Q$, finite alphabet $\Sigma$, total transition function $\delta:Q\times\Sigma\to Q$, start state $q_0$, and accepting set $F\subseteq Q$. After a word $w$, its current state summarizes all relevant history for future acceptance. Two prefixes ending in the same state cannot be distinguished by any common continuation.

For parity of the number of ones in a binary string, two states suffice: even and odd. A 0 leaves the state unchanged and a 1 toggles it. If the start and accepting state are even, the empty string is accepted. That last case must be tested; a word of length zero is not the same object as “no result found.”

Equivalence becomes reachability in a product graph#

Given DFAs $A$ and $B$ over the same alphabet, form states $(q_A,q_B)$. Start at the pair of start states. A symbol advances both machines. A reachable pair where exactly one component accepts is a distinguishing state: the word used to reach it is accepted by exactly one automaton. If no such pair is reachable, they accept the same language.

The proof is induction on word length. The empty word leaves the start pair. Appending a symbol applies exactly the paired transition, so the product’s state is always the pair of individual states after that word. Every possible word corresponds to a path. Breadth-first search explores reachable pairs in nondecreasing path length, so the first acceptance mismatch gives a shortest distinguishing word. Exhausting the finite graph proves no word distinguishes them, not merely no short word in a sampled list.

If there are $n$ and $m$ states, at most $nm$ pairs exist. With alphabet size $k$, a direct BFS examines at most $knm$ transitions. A shortest path to a mismatching reachable state need not repeat a product state, so its length is at most $nm-1$. This is a finite automaton result; a similar claim for arbitrary program states would lack the finite bound.

A proof that finite states are insufficient for one language#

Consider $L=\{a^n b^n:n\ge0\}$. Suppose some DFA with $p$ states recognizes it. While reading the first $p$ copies of $a$ in $a^p b^p$, the machine visits $p+1$ prefix states including the start. By the pigeonhole principle, two states coincide after $i$ and $j$ letters with $0\le i<j\le p$. The segment of $j-i$ copies of $a$ forms a loop. Repeating that loop once leaves the machine in the same state before the remaining input, so it must also accept $a^{p+(j-i)}b^p$. The counts differ, contradicting the definition of $L$. Therefore no DFA recognizes $L$.

This does not prove that $L$ is undecidable. A stack machine can push for each $a$, then pop for each $b$, reject an $a$ after the $b$ phase or an unmatched pop, and accept exactly when the input ends with an empty stack. The grammar $S\to aSb\mid\varepsilon$ generates the same language. More memory changes what the model can express. The proof is a concrete pumping argument, not permission to “pump any chosen substring” without connecting it to repeated states.

Why a universal halting decider leads to contradiction#

Assume an algorithm $H(P,x)$ always terminates and correctly decides whether program $P$ halts on input $x$. Programs are encoded as finite strings, so one program can receive another’s encoding. Construct $D(y)$: ask $H(y,y)$; if it predicts halting, loop forever; otherwise halt. Now run $D$ on its own encoding. If $H$ predicts that $D(D)$ halts, its definition makes it loop. If $H$ predicts nonhalting, its definition makes it halt. Both predictions contradict correctness, so the assumed universal decider cannot exist.

The argument does not say we can never prove that a particular program terminates. The binary search variant in W02 and the forward-only bytecode verifier in GP1 provide such proofs within bounded or structured classes. A timeout does not decide the universal question: after the deadline an uncompleted execution might halt later or never halt. A tool may also conservatively answer “unknown.” That is not the always-correct yes/no decider assumed in the contradiction.

Reductions transfer a problem, not an adjective#

To show that solving $B$ would solve $A$, construct a transformation $f$ such that $x\in A$ exactly when $f(x)\in B$. Then a hypothetical solver for $B$ applied to $f(x)$ solves $A$. To transfer undecidability from a known undecidable $A$ to $B$, reduce $A$ to $B$, not the reverse. A simple problem reducing to $B$ does not establish that $B$ is difficult.

For complexity reductions, also bound the transformation’s resources. Polynomial-time many-one reductions preserve a particular computational relationship. A decision problem is in NP when yes instances have polynomial-size certificates verifiable in polynomial time, under the standard model. NP does not mean “not polynomial.” Every problem in P is in NP. NP-hardness says every NP problem reduces to the target under the chosen reduction notion; NP-completeness adds that the target itself lies in NP. The general equality P=NP remains unresolved; using these distinctions does not assume an answer. [PNP]

A shortest-path certificate and a maximum-flow/minimum-cut certificate show how existence and optimality can have checkable evidence. Not every optimization task has a similarly simple known optimality certificate. When presenting a heuristic, separate “found a feasible result,” “proved the optimum,” and “measured useful performance on this distribution.”

Independent practice#

F foundation C standard course work T transfer S optional stretch L runnable lab or project. Attempt the complete set before opening its solutions.

Complete solutions: W07#

Compare the first step where your work differs. A corrected answer is not yet an independent success.

Open every solution

"""W07: a complete DFA comparison, not an arbitrary program-equivalence solver."""
from collections import deque


def validate(machine,alphabet):
    if type(machine) is not dict or set(machine)!={'states','start','accept','transition'}:
        raise ValueError("wrong DFA schema")
    n=machine['states']
    if type(n) is not int or not 1<=n<=100 or type(machine['start']) is not int or not 0<=machine['start']<n:
        raise ValueError("bounded state count and valid start required")
    if any(type(q) is not int or not 0<=q<n for q in machine['accept']):raise ValueError("bad accepting state")
    expected={(q,a) for q in range(n) for a in alphabet}
    if set(machine['transition'])!=expected:raise ValueError("complete transition table required")
    if any(type(q) is not int or not 0<=q<n for q in machine['transition'].values()):raise ValueError("bad target")


def distinguishing_word(left,right,alphabet=('a','b')):
    alphabet=tuple(alphabet)
    if not alphabet or len(set(alphabet))!=len(alphabet) or any(type(a) is not str or len(a)!=1 for a in alphabet):
        raise ValueError("unique one-character alphabet symbols required")
    validate(left,alphabet);validate(right,alphabet)
    start=(left['start'],right['start'])
    parent={start:None};todo=deque([start])
    while todo:
        pair=todo.popleft()
        if (pair[0] in left['accept']) != (pair[1] in right['accept']):
            symbols=[]
            while parent[pair] is not None:
                previous,symbol=parent[pair];symbols.append(symbol);pair=previous
            return ''.join(reversed(symbols))
        for symbol in alphabet:
            nxt=(left['transition'][pair[0],symbol],right['transition'][pair[1],symbol])
            if nxt not in parent:
                parent[nxt]=pair,symbol;todo.append(nxt)
    return None


def accepts(machine,word):
    state=machine['start']
    for symbol in word:state=machine['transition'][state,symbol]
    return state in machine['accept']


if __name__=='__main__':
    even={'states':2,'start':0,'accept':{0},
          'transition':{(0,'a'):1,(1,'a'):0,(0,'b'):0,(1,'b'):1}}
    everything={'states':1,'start':0,'accept':{0},'transition':{(0,'a'):0,(0,'b'):0}}
    print(repr(distinguishing_word(even,everything)))

Retention and readiness#

Explain nonregular, undecidable, and NP-hard using different examples. Draw the direction of a reduction before stating the conclusion. When a verification tool says “proved,” ask what model, assumptions, and state-space bound its proof concerns.