3
$\begingroup$

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.

Improve this question
$\endgroup$
7
  • $\begingroup$ 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. $\endgroup$
    – cody
    Commented Apr 30, 2021 at 16:17
  • $\begingroup$ 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! $\endgroup$
    – Lionel Parreaux
    Commented Apr 30, 2021 at 18:42
  • $\begingroup$ @cody I would greatly appreciate a concrete example or argument for the fact that the answers are "yes". $\endgroup$
    – Lionel Parreaux
    Commented Apr 30, 2021 at 18:57
  • $\begingroup$ 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. $\endgroup$
    – Labbekak
    Commented May 1, 2021 at 6:59
  • $\begingroup$ @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? $\endgroup$
    – Lionel Parreaux
    Commented May 1, 2021 at 7:06

2 Answers 2

Reset to default
8
$\begingroup$

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).

Improve this answer
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – Lionel Parreaux
    Commented May 3, 2021 at 11:05
4
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$
    – cody
    Commented May 1, 2021 at 22:03
  • $\begingroup$ @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. $\endgroup$
    – Lionel Parreaux
    Commented May 2, 2021 at 8:39
  • $\begingroup$ I think your answer is wrong though: an evaluator for system F could be typed! Just not applied to a term of type nat. $\endgroup$
    – cody
    Commented May 3, 2021 at 20:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.