If every legal expression can normalize, every reduction strategy terminates

← All digests

Family 245 · Mathematical logic
Importance 4/5 · Provisional editorial rating
Sources consulted 2026-10-21

1. The question

A symbolic expression can often be simplified in several orders. One strategy may reach a final answer, while another keeps reducing a subexpression forever. Finding one terminating route is therefore weaker than proving that every route terminates.

Type systems can rule out such behavior. The question in family 245 is whether, for the broad framework of pure type systems, a system-wide guarantee of some terminating route already forces termination under every sequence of beta reductions.

The manuscript, dated 25 September 2026, claims that it does. It resolves the beta-reduction version of the Barendregt–Geuvers–Klop conjecture for arbitrary pure type specifications, without requiring unique sort assignments or product rules. Reductions inside types and annotations are included.

The universal hypothesis is essential: every legal expression in every valid context must have a normal form. The theorem is not a claim that an individual expression with one terminating reduction has no infinite reduction.

2. Background and essential definitions

Beta reduction

In lambda notation, $\lambda x.M$ is a function with input $x$ and body $M$. Applying it to $N$ permits the beta step

$$(\lambda x.M)N\longrightarrow_\beta M[x:=N],$$

where substitution replaces free occurrences of $x$ while avoiding accidental variable capture.

A normal form has no remaining beta redex, or reducible application, anywhere. Weak normalization means that at least one finite sequence reaches a normal form. Strong normalization means that no infinite sequence of beta reductions begins at the expression.

The distinction is visible in the untyped calculus. Let

$$\Omega=(\lambda z.zz)(\lambda z.zz).$$

It reduces to itself. The raw expression $(\lambda x.y)\Omega$ can immediately reduce to $y$, but a strategy that keeps reducing its argument runs forever. This is an illustration in untyped syntax, not a counterexample to the manuscript’s system-wide typed theorem.

Pure type systems

A pure type system, or PTS, is specified by three sets of data:

$$\mathcal P=(S,\mathcal A,\mathcal R).$$

The set $S$ contains sorts, the classifications of types. An axiom $(s_1,s_2)\in\mathcal A$ permits the typing judgment $s_1:s_2$. A product rule $(s_1,s_2,s_3)\in\mathcal R$ permits a dependent function type with domain sort $s_1$, codomain sort $s_2$, and resulting sort $s_3$.

The dependent product

$$\Pi x:A.B$$

is the type of functions whose output type $B$ may depend on the input $x$. When it does not depend on $x$, this is an ordinary function type $A\to B$.

Expressions include variables, sorts, applications, annotated abstractions $\lambda x:A.M$, and dependent products. A context $\Gamma$ is a finite list of variable declarations. The judgment $\Gamma\vdash M:A$ says that $M$ has type $A$ under those declarations.

A specification is functional when the relevant sort outputs are uniquely determined. The new theorem allows nonfunctional specifications: one sort or pair of product sorts may admit more than one output classification.

Full annotated reduction

The manuscript reduces inside annotations as well as computational bodies. If $A\to_\beta A'$, then

$$\lambda x:A.M\longrightarrow_\beta\lambda x:A'.M$$

is an allowed step. Both components of a dependent product can also reduce.

A legal expression is either the subject or expected type in a derivable judgment. Valid context declarations are included through their own typing requirements. Reduction acts on the expression itself; it does not unfold declarations in the external context as if they were definitions.

3. Development history and previous partial results

Normalization proofs are central to typed lambda calculus and proof theory. Under the propositions-as-types viewpoint, a term can represent a proof, and reduction simplifies that proof. Strong normalization ensures that arbitrary reduction choices cannot lead to an infinite simplification process.

Geuvers’s 1993 thesis formulated the system-wide Barendregt–Geuvers–Klop conjecture for beta reduction and for beta-eta reduction. The manuscript addresses the beta version only.

One major line of earlier work translated terms so that an infinite reduction in the source would contradict weak normalization of a translated term. The translation must preserve typing, and that requirement depends on which product rules the source system actually provides.

Sørensen’s continuation-passing method established the implication for generalized nondependent systems with specific cleanliness and negatability conditions. Barthe, Hatcliff and Sørensen developed a uniform treatment of a class of nondependent pure type systems. Mull’s later thesis weakened some restrictions within the nondependent tiered setting, where sorts form a finite axiom chain and products inherit the codomain’s sort.

Structural transformations supplied another approach. Roux and van Doorn proved preservation results for disjoint sums and certain added product rules. Mull showed that the normalization implication transfers from an irrelevance reduction to the original tiered system. These are valuable reductions, but retain hypotheses on the source specification or on the transformed system.

Annotations introduce an additional problem. Barthe and Coquand showed that erasing lambda-domain annotations can identify terms that are not beta-convertible in nonnormalizing systems. One cannot simply discard annotations, prove a statement about the remaining bodies and assume that it controls every reduction in the original calculus.

The new paper claims a structural argument that does not require the products used by those translations. It tracks all possible sort assignments and retains type annotations throughout, including in the auxiliary labelled calculus used to exclude a problematic configuration.

4. What the new manuscripts claim

Write $\operatorname{WN}(\mathcal P)$ to mean that every legal expression in every valid context is weakly beta-normalizing. Write $\operatorname{SN}(\mathcal P)$ for the corresponding statement with strong beta-normalization. For every pure type system $\mathcal P$, the manuscript asserts

$$\operatorname{WN}(\mathcal P)\quad\Longrightarrow\quad\operatorname{SN}(\mathcal P).$$

The statement includes open expressions, meaning expressions with free variables declared in the context. It includes types and the reductions inside their annotations. The axiom and product relations need not be functional, and the overall specification need not have a finite hierarchy of sorts.

A finite derivation uses only finitely many sorts and rules. The proof exploits this to reduce the relevant argument to finite pieces of a possibly infinite specification. It does not impose finiteness as an extra hypothesis on the theorem.

The result concerns beta reduction. Eta reduction, which simplifies a function that merely applies another function to its argument, is not included in the claim. Nor does the theorem automatically apply after adding arbitrary rewrite rules, recursion operators or extra computational equations.

The paper’s proof may use weak normalization of newly constructed legal expressions other than the expression whose strong normalization is under consideration. This explains why replacing the system-wide premise by a premise about one term would change the theorem fundamentally.

5. Why the advance matters

Importance: 4/5, provisional. The theorem would settle a longstanding normalization conjecture across the general PTS framework, including dependent and nonfunctional cases outside earlier translation methods.

Its practical proof-theoretic consequence is a simplification of what must be established about a system. If one proves that every legal expression has some beta-normal form, the claimed theorem supplies termination under all beta-reduction choices.

That is particularly relevant when types themselves compute. A body may already look like a result while reductions remain possible in its annotations. The full-syntax convention ensures that the conclusion controls those reductions too.

The score reflects a broad foundational result within type theory. It does not claim that a weak-normalization proof is always easy, that every PTS satisfies the premise, or that normalization becomes efficient. Systems permitting nonterminating legal expressions remain outside the hypothesis.

6. The main idea

Track every possible sort

Under weak normalization and confluence, each legal expression has a unique beta-normal form up to bound-variable renaming. For a normal type, the manuscript records its sort profile: the set of all sorts at which it can be typed.

A profile is needed because a nonfunctional specification does not provide a unique sort. The proof studies how these sets behave under substitution, rather than relying on uniqueness of typing that is unavailable in the stated generality.

The finite profiles form a dependency graph. Dependent products introduce signed dependencies: candidate inclusion reverses in the domain and preserves direction in the codomain, just as a function space is contravariant in its input and covariant in its output.

Build semantic sets of terminating terms

The proof follows the Tait–Girard reducibility tradition. A candidate is a carefully closed collection of strongly normalizing terms. Interpreting a type by such a collection lets one prove that every legal term of that type belongs to it.

For function types, the interpretation tests application to suitable argument stacks. A stack is a finite list of successive arguments. The target property says that a strongly normalizing function, applied to a correctly typed stack of strongly normalizing arguments, remains strongly normalizing.

If that property holds throughout the system, a smallest nonnormalizing application cannot exist. This converts the candidate construction into strong normalization for all legal expressions.

The signed graph is processed component by component. When signs are consistent, an ordered fixed-point construction using Tarski’s theorem supplies candidates. A second construction handles products with at most one child in the current component.

Handle circular dependencies with observations

The remaining components can involve negative cycles and more complicated mutual dependence. Defining the candidate for one type can require knowing the candidate for another that depends back on the first.

The manuscript introduces observation tables indexed by stacks of normal arguments and auxiliary values. Some profiles are handled by well-founded recursion, others by alternating finite stages. A central claim is a bound uniform over all observations of a fixed typed expression, even though possible arguments and stack lengths are unbounded.

Substitution stability is indispensable. In a dependent application, replacing a variable by an argument changes the output type. The interpretation must commute with that substitution closely enough to justify the application step.

This construction works provided one specific graph configuration is absent. Establishing its absence is the second major part of the proof.

A forbidden configuration would violate weak normalization

The paper shows that the problematic profile pattern would supply enough product rules for a small typed formula calculus. Inside that calculus it builds a guarded version of the diagonal argument associated with Hurkens’s simplification of Girard’s paradox.

This is not an appeal to an untyped paradox. Every quantifier and data channel must be supported by product rules actually available in the profile graph. Explicit validity and extensionality conditions control which substitutions preserve the observations used by the diagonal.

The auxiliary syntax labels expressions as proof mode or data mode. The resulting diagonal constructs a proof-mode term of a designated terminal formula. A separate syntactic descent argument says that no proof-mode term of that terminal can have a beta-normal erasure in the specified context.

Erasure removes only these mode labels; it keeps every type annotation. Moreover, ordinary typed beta steps of an erased term lift to labelled steps. System-wide weak normalization would therefore normalize the constructed erased proof, producing exactly the normal erasure that the syntactic lemma forbids.

This contradiction excludes the graph configuration. The remaining candidate construction then completes the strong-normalization argument.

7. Scope, limitations, and open questions

The premise applies to all legal subjects and expected types in all valid contexts. A single weakly normalizing term, or a system whose closed programs normalize while some open types do not, does not meet the stated hypothesis.

The theorem uses full beta reduction, including annotation positions. An argument about erased computational bodies alone would not establish this conclusion. The auxiliary erasure in the source is explicitly designed to retain those positions.

No functionality assumption is imposed, but the system must still be a pure type system with the specified typing and conversion rules. Extensions by new computational mechanisms require their own analysis.

The beta-eta version of the conjecture is not claimed. The result also supplies no bound on reduction lengths and no efficient strategy for finding normal forms. Strong normalization guarantees finiteness of every sequence, not a small running time.

The proof’s paradox-based exclusion should be read as a conditional structural argument: if the forbidden profile configuration existed, it would produce a legal term contradicting the global weak-normalization premise. It does not claim that every nonfunctional or dependent type system is inconsistent.

8. Sources and further reading

Geuvers, Logics and Type Systems, doctoral thesis (1993), Conjecture 8.1.2, gives the system-wide conjecture. Barthe, Hatcliff and Sørensen, Weak normalization implies strong normalization in a class of non-dependent pure type systems, Theoretical Computer Science 269 (2001), 317–361, is a main translation-based predecessor.

Roux and van Doorn, The structural theory of pure type systems, Lecture Notes in Computer Science 8560 (2014), 364–378, develops structural reductions. Mull, An irrelevancy-eliminating translation of pure type systems, LIPIcs 269 (2023), 7:1–7:21, and his 2023 thesis on tiered systems give more recent reductions and partial results.

Girard, Proofs and Types (1989), provides background on reducibility candidates. Hurkens, A simplification of Girard’s paradox, Lecture Notes in Computer Science 902 (1995), 266–278, is the diagonal predecessor. Barthe and Coquand, Remarks on the equational theory of non-normalizing pure type systems, Journal of Functional Programming 16 (2006), 137–155, explains the annotation-erasure issue.

Source manuscripts

• M1. OpenAI, Weak and strong normalization in pure type systems (September 25, 2026).

Sources consulted on 21 October 2026 at repository revision 1581d4c. Download the manuscript citations.