When is a pumping argument worth spending on a claim that a format is not finite-state checkable, and what does a failed attempt prove?

## The asymmetry that governs the decision The pumping lemma is a **necessary** condition, not a characterisation. Written honestly: if a language is accepted by some finite automaton, then it has the pumping property. The converse does not hold. Languages exist that satisfy the pumping property for accidental structural reasons — every long member happens to carry a repeatable block — and are nonetheless not accepted by any finite automaton. Consequently: - **A successful pumping argument is conclusive.** It rules out every finite-state recogniser at once, so no amount of pattern cleverness reopens the question. - **A failed pumping argument is worth nothing in either direction.** It says this witness did not work. It does not say the language is finite-state checkable, and a lead who treats it as such has taken a design decision on no evidence. - **The positive direction needs a construction.** To claim a rule *is* checkable by a pattern or a finite machine, exhibit one, or show the state is a bounded tuple — a depth capped at a fixed number, a remainder, a fixed-width flag set. That is a review artefact anyone can check. There is a second family of arguments, owned elsewhere in this subject, that does characterise the class exactly and can therefore prove both directions. It is the right tool when you need the positive answer and no construction is obvious; it is not what a candidate reaches for to refute a pattern in a code review. ## When the argument earns its cost Spend it when the conclusion changes something expensive: 1. **The format is about to be published.** Once third parties implement validators, a rule that cannot be checked incrementally is imposed on all of them forever, in every language they use. The argument belongs in the specification review, not after. 2. **The proposal keeps coming back.** If three reviews in a row have produced a cleverer pattern for the same rule, the argument is cheaper than the fourth review. It converts a recurring opinion into a settled fact. 3. **The validator sits on a hot path.** "No pattern exists" changes the performance conversation from tuning to redesign — buffering, a counter, or a two-stage validator with different cost characteristics. 4. **Correctness is load-bearing.** Where a validator is the boundary between trusted and untrusted input, a rule that only *looks* checkable tends to ship as a pattern that is subtly wrong on deep inputs. Skip it when the rule can be **bounded** instead. A nesting cap, a length cap, or a remainder rule turns the question from impossible to arithmetic, and the argument you were about to write becomes moot. Bounding is usually the cheaper engineering answer, and proposing it is a better review comment than a proof. ## Reading the result correctly | what happened | what you may conclude | what you may not | |---|---|---| | a witness pumps out of the language, all splits covered | no finite automaton and no regular pattern accepts it | nothing about how expensive the alternative validator is | | one witness survives pumping | this witness is unhelpful | that the language is finite-state checkable | | every witness you tried survived | you have not found an argument | that no argument exists, or that a machine exists | | you exhibited a machine or a bounded state encoding | the rule is finite-state checkable | that the pattern implementing it is small or readable | The third row is the one that costs teams money. "We could not prove it impossible" reads, in a design document three months later, as "it is possible", and the pattern that was written on that basis fails on the first deeply nested input from a real client. ## What a principal-level answer adds The judgment is not about proof technique for its own sake; it is about which claims a team is allowed to assert without an artefact. A reasonable standard: an impossibility claim needs a witness and a case analysis that a colleague can check in the review; a possibility claim needs a construction or a bound. Anything else — including "we tried and could not break it" — is an opinion and should be labelled as one in the document. That standard costs little, it is teachable in an afternoon, and it removes an entire class of format decisions that would otherwise be made by whoever argued longest. Finally, keep the scope honest. The argument settles what a finite-state recogniser can decide. It says nothing about whether the alternative validator is fast, whether the format is a good one, or whether the rule should exist at all — those are separate conversations, and a proof is not a licence to skip them.