Skip to content

Language-Fragment Restriction

Restriction method — instantiates Computability Boundary Mapping

Regains a terminating decision procedure by narrowing the language problems are stated in to a syntactic fragment known to be decidable, trading expressive power for a guaranteed answer.

Language-Fragment Restriction buys back a terminating decision procedure by shrinking the language in which problems are stated down to a syntactic fragment known to be decidable. The full language may be undecidable — first-order logic, general arithmetic, an unrestricted query or type system — but a carefully drawn sub-language (only these connectives, only linear arithmetic, only these quantifier patterns) can carry a complete decision procedure. Its defining move is syntactic: it does not restrict which inputs you care about — that is a promise — but which sentences are expressible at all, redrawing the problem class so that every well-formed question inside the fragment is guaranteed answerable.

Example

A policy-as-code platform lets teams write authorization rules and wants to guarantee that any rule set can be checked for internal conflicts in bounded time. Expressed in full first-order logic over the data, consistency-checking would be undecidable, so the platform admits only a decidable fragment: linear arithmetic over the integers with quantifiers — essentially Presburger arithmetic — plus a fixed vocabulary of relations, and it forbids multiplying two variables together or writing unrestricted recursion. Inside that fragment a complete decision procedure exists, so the platform can make a hard promise: every rule set that type-checks is guaranteed a terminating conflict verdict. A team that needs variable-by-variable multiplication is told at authoring time that it has stepped outside the decidable fragment — a designed boundary, announced up front, not a runtime surprise. Expressiveness was spent deliberately to purchase a total guarantee.

How it works

  • Map the decidable fragments of the host language and the decision procedure each one admits.
  • Define the fragment syntactically — a grammar or type discipline a parser can enforce mechanically — so membership is checkable by inspection.
  • Redraw the problem-class specification to that fragment, so "the problem" the system solves is the guaranteed-answerable sub-language.
  • Reject or quarantine anything outside the fragment at authoring time, before it can pose an unanswerable question.

Because fragment-membership is itself syntactic, it is decidable: the system always knows whether a given question is inside the safe zone.

Tuning parameters

  • Fragment size — how much of the language you admit; a larger fragment expresses more but risks crossing back over the decidability line — or into infeasible complexity.
  • Filter placement — enforce the restriction at parse time, type-check time, or runtime; earlier is a stronger guarantee, later is more permissive.
  • Escape policy — whether out-of-fragment constructs are rejected outright or routed to a fallback mode; strict rejection preserves the guarantee, routing preserves expressiveness.
  • Choice among decidable fragments — several decidable fragments may exist with wildly different complexity; pick for the cost you can actually afford, not decidability alone.

When it helps, and when it misleads

Its strength is a guarantee by construction: it converts an undecidable problem into one with a total decision procedure, and because the safe zone is syntactically checkable, users get a crisp up-front contract about exactly what the system will always answer.

Its failure modes turn on expressiveness and cost. Cut the fragment too tight and the very thing users need is missing, so they abandon it for an undecidable escape hatch; and decidability is not feasibility — some decidable fragments carry towering complexity, so a "guaranteed answer" can still be unaffordable.[1] The classic misuse is advertising the whole language as checkable when only the fragment is, or drawing the fragment to fit a demo rather than the real workload. The discipline is to choose the fragment against measured usage and to pass every decidable fragment through a Complexity Follow-On Gate before promising it.

How it implements the components

Language-Fragment Restriction fills the decidable-subclass side of the archetype — the components a syntactic retreat to safety produces:

  • decidable_subclass_map — it is built on a map of which syntactic fragments of the host language are decidable and by what procedure; that map is the mechanism's core asset.
  • problem_class_specification — it redraws the specification of the problem class down to the fragment, so the problem the system actually solves is redefined to the guaranteed-answerable sub-language.

It restricts the language, not the inputs — narrowing which inputs the solver is accountable for is Promise-Problem Restriction — and it does not prove the underlying full language undecidable, which is Halting-Problem Reduction's job.

Notes

Because fragment-membership is syntactic and therefore decidable, this restriction is self-policing in a way an input-promise is not: the system can always tell whether a question is inside the guarantee, with no separate checker and no trust in the caller. That is the reason to prefer a language fragment whenever the restriction you need can be expressed syntactically — and to reach for a promise only when it cannot.

References

[1] Presburger arithmetic — the first-order theory of the integers with addition and order but no multiplication — is decidable, whereas adding multiplication yields full arithmetic, which is undecidable. It is the standard illustration of buying a total decision procedure by giving up expressive power. ↩