# Are there strongly normalizing lambda terms that cannot be given a System F type?

I know that all well-typed System F terms are strongly normalizing, but is the converse true as well? In other words, does System F typeability precisely characterize program termination? (And if so, how to prove it?) Or are there lambda terms that are strongly normalizing but cannot be given a System F type?

A System F interpreter cannot be implemented in System F. On the other hand, a System F interpreter can be implemented in untyped lambda calculus, but that's not enough. Can a strongly normalizing System F interpreter be implemented in untyped lambda calculus? If yes, this answers our question positively, but I am not sure about it.

• The answer to your last 2 questions are both "yes", though you seem to be conflating "strongly normalizing term" and "term that is strongly normalizing when applied to well-formed inputs". However this question is more suited to cs.stackexchange. – cody Apr 30 at 16:17
• No, no, I was not conflating them, although I understand tat you might suspect so. But I don't think what I wrote implies such a conflation. Anyway, sorry for asking on the wrong site! – LP_ Apr 30 at 18:42
• @cody I would greatly appreciate a concrete example or argument for the fact that the answers are "yes". – LP_ Apr 30 at 18:57
• System F is strongly-normalizing. You can write an typechecker/interpreter for System F in Haskell, you can erase Haskell to the untyped lambda calculus. I believe you can write an interpreter for System F in the Calculus of Constructions as well. – Labbekak May 1 at 6:59
• @Labbekak writing a System F interpreter in Haskell does not answer my question, as its erasure to lambda calculus will probably include something like a fixed point combinator, which is not strongly normalizing! I am much more interested in a CoC implementation of such interpreters. Do you have any sources on their existence? – LP_ May 1 at 7:06

As you found out yourself, the answer to your question is yes. You found a rather convoluted example, a much simpler example is the following:

$$(\lambda zy.y(zI)(zK))(\lambda x.xx)$$

where $$I$$ and $$K$$ are the identity and first-projection combinators. This may be found at p. 204 of Sørensen and Urzyczyn's Lectures on the Curry-Howard Isomoprphism. They attribute it to Ronchi Della Rocca and Giannini, and also give a seemingly even simpler example, which is $$c_2c_2K$$, where $$c_2$$ is, I believe, the Church integer 2 (I'm not sure about their notation so I may be wrong).

• Amazing, that's exactly what I was looking for. Thanks! I've switched the accepted answer to your answer, since it's a simple concrete example. The provided source even contains good insights about why the example works. – LP_ May 3 at 11:05

So, after some research, I found that someone has formalized a proof of strong normalization of System F using the Calculus of Constructions + inductive types (see: A formalization of the strong normalization proof for System F in LEGO). This strongly suggests that one could write a System F interpreter in Coq. Erasing that interpreter to untyped lambda calculus would yield a strongly normalizing term that cannot possibly be typed in System F, since System F cannot implement a self-interpreter.

PS: By self-interpreter, I mean something taking a plain string-based term representation and returning a string of the normalized term. Typed meta-circular self-recognizers (abusively called "self-interpreters") can actually be defined, but that's a whole other thing.

• Again, worth noting that any Curry style term in normal form can be typed. However the type of that term would preclude it from being applied to an arbitrary code for a system F term. – cody May 1 at 22:03
• @cody Ok, but there are infinitely many unrelated types that can be assigned to such a Curry-style term f. So "the type of that term" is not well-defined. Also, even the question of whether there exist System F arguments a that no typing of f can possibly accommodate is not very interesting, as we already know of straightforward examples. For instance, self-application is a normal form and is typeable, but its self application is neither normalizable nor typeable. As far as I know, that fact says nothing about my original question. – LP_ May 2 at 8:39
• I think your answer is wrong though: an evaluator for system F could be typed! Just not applied to a term of type nat. – cody May 3 at 20:14