Algorithmic typing lacks subject reduction

Proved

LeanTT2.algo_no_subject_reduction

by Lucas · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

algorithmictypingcounterexamplesubjectreductiontypetheory

For every extended fragment, context, and terms α, β, γ, e such that the algorithmic equality relates α to β and β to γ but not α to γ, and e is algorithmically typed at γ: the identity application at β applied to e is algorithmically typed at β, because the application forces checking that β is algorithmically equal to γ; the identity application at α applied to that term is algorithmically typed at α, since it forces checking α against β; the identity application at β applied to e reduces to e; but the identity application at α applied to e is not algorithmically typed at α, because that would require α to be algorithmically equal to γ. Reduction does not preserve algorithmic typing: subject reduction fails for the algorithmic typing judgment.

Preamble

import Mathlib
import Definitions.Def_LeanTT2_frag
import Definitions.Def_LeanTT2_spec
import Definitions.Def_LeanTT2_counter

Formal statement

universe u

/-!
# Algorithmic typing lacks subject reduction

Thesis section 3.1.2 (page 17): the algorithmic typing judgment, the
variant of typing that uses the algorithmic equality in the conversion
rule, fails subject reduction, directly from the failure of
transitivity. If the algorithmic equality relates α to β and β to γ but
not α to γ, and `e` is algorithmically typed at γ, then:
the identity application at β applied to `e` is algorithmically typed
at β, because the application forces checking that β is algorithmically
equal to γ; the identity application at α applied to that term is
algorithmically typed at α, since it forces checking α against β; but
the identity application at α applied to `e` is not algorithmically
typed at α, because that would require α to be algorithmically equal to
γ. Since the identity application reduces to its argument, this is a
counterexample to subject reduction.
-/

namespace LeanTT2

/-- For every extended fragment, context, and terms `α`, `β`, `γ`, `e`
such that the algorithmic equality relates `α` to `β` and `β` to `γ`
but not `α` to `γ`, and `e` is algorithmically typed at `γ`: the
identity application at `β` applied to `e` is algorithmically typed at
`β`; the identity application at `α` applied to that term is
algorithmically typed at `α`; the identity application at `β` applied
to `e` reduces to `e`; but the identity application at `α` applied to
`e` is not algorithmically typed at `α`. Reduction does not preserve
algorithmic typing. -/
theorem algo_no_subject_reduction (F : Frag.{u}) (Γ : F.Ctx)
    (α β γ e : F.E)
    (hab : F.alg Γ α β) (hbc : F.alg Γ β γ) (hnac : ¬ F.alg Γ α γ)
    (he : F.aty Γ e γ) :
    F.aty Γ (F.app (F.idf β) e) β ∧
    F.aty Γ (F.app (F.idf α) (F.app (F.idf β) e)) α ∧
    F.red Γ (F.app (F.idf β) e) e ∧
    ¬ F.aty Γ (F.app (F.idf α) e) α := by sorry

end LeanTT2

Source

M. Carneiro, The Type Theory of Lean, 2019, section 3.1.2 (p. 17).

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: given types α, β, γ with the algorithmic equality holding for α with β and β with γ but not α with γ, and a term e algorithmically typed at γ, the terms id_β e and id_α (id_β e) are algorithmically typed at β and α respectively, the term id_β e reduces to e, and yet id_α e is not algorithmically typed at α: subject reduction fails.

View graph