2
$\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.

$\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
    Apr 30 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$
    – LP_
    Apr 30 at 18:42
  • $\begingroup$ @cody I would greatly appreciate a concrete example or argument for the fact that the answers are "yes". $\endgroup$
    – LP_
    Apr 30 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
    May 1 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$
    – LP_
    May 1 at 7:06
6
$\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).

$\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$
    – LP_
    May 3 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.

$\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
    May 1 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$
    – LP_
    May 2 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
    May 3 at 20:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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