Post #2142730

2026-05-03 03:50 UTC

Today I finally finished formalizing the proof that a term is typable in intersection type theory if and only if it is strongly normalizing! Intersection type theory is simply typed λ-calculus with a binary intersection type (and no subtyping relation or anything fancy). A term has an intersection type iff the same term inhabits both types.

Replies (2)

@trebor@types.pl 2026-05-03 03:54

This proof is especially tricky because it needs a lot of inversion on typing derivations, and inversions generally don't work. It's nontrivial even to show if λx.t has a function type, then t has the codomain type assuming x has the domain type! In fact, the proof in the paper I referenced happens to contain a bug. There is a lemma without proof, and the paper it cited has a corrected version where the lemma got replaced. I'm not sure if a complete correct proof has been written down anywhere (though I'm sure experts know the proof), since for example the even the corrected version claim that if a function applied to N arguments have a type, then the function itself has a N-fold curried function type. This is false without subtyping rules.

Open ##2191763
@trebor@types.pl 2026-05-03 03:58

By the way, every untyped *normal* term can be typed in system F (for example λx. xx can be given the type Unit -> Unit where Unit = forall T. T -> T). And as a corollary, there exists an interpreter of system F in untyped lambda calculus operating on Godel encoded Church numerals, that can be given a type in system F itself.

Open ##2191764