6
$\begingroup$

The untyped language of System-F and similar is the λ-calculus. That language has terms that can't be typed on System-F, λx.(x x) λx.(x x) being the most obvious example. The λEA-calculus, as described here, and its variants, has an interesting property that all stratified terms of the untyped language are total and strongly normalizing. That raises 2 questions:

  1. Does that mean that, for all terms of λEA, there is a valid type derivation?

  2. Is this a common phenomena, i.e., are there other systems with this same characteristic, or is it something particular of linear logic based proof languages?

$\endgroup$
  • $\begingroup$ The link to the paper doesn't work for me. $\endgroup$ – Andrej Bauer Aug 31 '17 at 5:55
  • $\begingroup$ @AndrejBauer really? Just tested it and it works. It is "Principal Typing for Lambda Calculus in Elementary Affine Logicl", Paolo Coppola and Simona Ronchi della Rocca. Pretty much any paper on light logics defines the same system or a very similar variant. $\endgroup$ – MaiaVictor Aug 31 '17 at 6:03
  • 1
    $\begingroup$ Strange, now it works. $\endgroup$ – Andrej Bauer Aug 31 '17 at 6:53
9
$\begingroup$

For question 1, the answer is no, and is no for almost any type discipline (except certain intersection types): the fact that a term is (strongly or weakly) normalizable does not imply in general that it is typable. Typability implies termination, not the other way around.

The specific case of of $\lambda EA$, however, brings up another issue which may be the object of confusion, so let me discuss it. Let us start with a counter-example for your question 1: the term $$[M]_{\lambda x.N=y,z}$$ is not typable. This is because the construct $[M]_{P=y,z}$ represents contraction of variables $y$ and $z$ in $M$ (i.e., $y$ and $z$ are morally equated in $M$ and $P$ is "plugged in" on them), so for such a term to be typable $P$ must have type $!A$, i.e., it must be duplicable. Now, in my example, $P$ is an abstraction and can never receive type $!A$ (its type will always have the form $B\multimap C$).

There are many more examples like this in $\lambda EA$. Intuitively, typability ensures more than termination: it also avoids "clashes", i.e., a term may stop its reduction because it "gets stuck". Typically, this happens when a destructor of a certain form meets a constructor of a different form (e.g., a head::tail pattern that is matched, i don't know, against a binary tree). For example, in the above case, the constructor matching the destructor $[M]_{P=y,z}$ is $!(-)$, not $\lambda$, i.e., if $P$ ever reduces to something with a constructor at the root, one expects $P=!(N)[\ldots]$, not $P=\lambda x.N$.

In truth, typability is orthogonal to termination. There may be a misunderstanding about this because, in the context of the pure $\lambda$-calculus, which is the one used for showcasing type disciplines to a beginner, there are no "clashes" (there is only one constructor and one destructor), so clash-avoidance is completely hidden and only termination shows up. But as soon as one spices things up a bit, adding more constructors and destructors, the distinction between termination and clash-avoidance arises, and types are seen to actually ensure the latter more than the former (for instance, PCF is a typed language which does not terminate, as is every real-world functional programming language). Mor precisely, types always ensure clash-avoidance and might, in many cases of interest, also ensure termination.

Regarding your question 2, I am guessing that by "same characteristic" you mean the fact that the untyped calculus terminates? In this case, it may not be very common for the programming languages one considers in practice, but it is not very hard to come up with examples, which must not necessarily have anything to do with linearity (for instance: consider any programming language with no gotos and having a distiction between "for" and "while" loops; eliminate while loops; the language you obtain terminates, whether you have types or not). The interest of $\lambda EA$ is not that it terminates but that it does so with an interesting complexity bound (elementary).

$\endgroup$

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.