<p>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 href="https://link.springer.com/chapter/10.1007%2FBFb0037095" rel="nofollow noreferrer">A formalization of the strong normalization proof for System F in LEGO</a>). 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.</p>
<p>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 &quot;self-interpreters&quot;) <a href="https://dl.acm.org/doi/abs/10.1145/2837614.2837623" rel="nofollow noreferrer">can actually be defined</a>, but that's a whole other thing.</p>

CC BY-SA 4.0
2021-05-01T22:03:56.480Z
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
CC BY-SA 4.0
2021-05-02T08:39:37.823Z
@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.
Lionel Parreaux
CC BY-SA 4.0
2021-05-03T20:14:28.323Z
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
CC BY-SA 4.0
2021-05-01T11:35:48.657Z
2021-05-01T19:19:38.233Z
2021-05-01T19:19:38.233Z
Lionel Parreaux
<p>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:</p>
<p><span class="math-container">$$(\lambda zy.y(zI)(zK))(\lambda x.xx)$$</span></p>
<p>where <span class="math-container">$I$</span> and <span class="math-container">$K$</span> are the identity and first-projection combinators.  This may be found at p. 204 of Sørensen and Urzyczyn's <a href="https://disi.unitn.it/%7Ebernardi/RSISE11/Papers/curry-howard.pdf" rel="noreferrer"><em>Lectures on the Curry-Howard Isomoprphism</em></a>.  They attribute it to Ronchi Della Rocca and Giannini, and also give a seemingly even simpler example, which is <span class="math-container">$c_2c_2K$</span>, where <span class="math-container">$c_2$</span> is, I believe, the Church integer 2 (I'm not sure about their notation so I may be wrong).</p>

CC BY-SA 4.0
2021-05-03T11:05:46.220Z
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.
Lionel Parreaux
CC BY-SA 4.0
2021-05-02T21:29:03.023Z
2021-05-02T21:29:03.023Z
Damiano Mazza
<p>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?</p>
<p>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 <em>strongly normalizing</em> System F interpreter be implemented in untyped lambda calculus? If yes, this answers our question positively, but I am not sure about it.</p>

CC BY-SA 4.0
2021-04-30T16:17:26.610Z
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
CC BY-SA 4.0
2021-04-30T18:42:38.027Z
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!
Lionel Parreaux
CC BY-SA 4.0
2021-04-30T18:57:53.710Z
@cody I would greatly appreciate a concrete example or argument for the fact that the answers are "yes".
Lionel Parreaux
CC BY-SA 4.0
2021-05-01T06:59:37.827Z
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
CC BY-SA 4.0
2021-05-01T07:06:29.600Z
@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?
Lionel Parreaux
CC BY-SA 4.0
2021-05-01T10:19:04.660Z
The comment about CoC was more of a guess, sorry. I think System F only supports primitive recursion? Other methods of termination checking (Walther recursion for example) allow more functions to be written. That would imply there are functions that terminate but cannot be written in System F. (I'm not an expert by any means by the way, but maybe my thoughts can help you further)
Labbekak
CC BY-SA 4.0
2021-05-01T11:38:39.183Z
@Labbekak thanks for the insights, it does help! I have since answered my own question by following the CoC interpreter approach (see below).
Lionel Parreaux
<lambda-calculus><typed-lambda-calculus>
Are there strongly normalizing lambda terms that cannot be given a System F type?
Lionel Parreaux
# Are there strongly normalizing lambda terms that cannot be given a System F type?

(Asked by: username_0 on 2021-04-30)

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.

**Tags:** lambda-calculus, typed-lambda-calculus

> **Comments:**
> **username_1**: 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.  
> **username_0**: 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!  
> **username_0**: @username_1 I would greatly appreciate a concrete example or argument for the fact that the answers are "yes".  
> **username_2**: 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.  
> **username_0**: @username_2 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?  
> **username_2**: The comment about CoC was more of a guess, sorry. I think System F only supports primitive recursion? Other methods of termination checking (Walther recursion for example) allow more functions to be written. That would imply there are functions that terminate but cannot be written in System F. (I'm not an expert by any means by the way, but maybe my thoughts can help you further)  
> **username_0**: @username_2 thanks for the insights, it does help! I have since answered my own question by following the CoC interpreter approach (see below).  

---

## 2 answers

### Answer by username_3 on 2021-05-02. Score: 8 | Accepted answer

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*](https://disi.unitn.it/%7Ebernardi/RSISE11/Papers/curry-howard.pdf). 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).

> **Comments:**
> **username_0**: 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.  

---

### Answer by username_0 on 2021-05-01. Score: 4

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](https://link.springer.com/chapter/10.1007%2FBFb0037095)). 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](https://dl.acm.org/doi/abs/10.1145/2837614.2837623), but that's a whole other thing.

> **Comments:**
> **username_1**: 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.  
> **username_0**: @username_1 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.  
> **username_1**: I think your answer is wrong though: an evaluator for system F *could* be typed! Just not applied to a term of type `nat`.  

---

