2

I have also provided my own examples and I am wondering if they are correct.

Example 1: $A = x$ and $B = x$, they are both typeable but $A B = x x$ which are not typeable(?)

Example 2: $A = \lambda x.x$ and $B = x$ so they are both typeable but $A B = \lambda x.x x$ which are not typeable (?)

Can you answer me whether are my answers correct and are there any other examples out there that fulfill the constraints above?

Mrcrg
  • 2,767
Anon1995
  • 21

1 Answers1

2

Yes, this is possible.

Your example 1 is correct, and all the standard examples of untypeable terms eventually boil down to this kind of self-application.

Your example 2 is incorrect. $A = \lambda x.x$ will have a function type $\sigma \to \sigma$, and combined with a suitable term $B = x$ of type $\sigma$ yields the application term $(\lambda x.x)x$ with type $\sigma$. Because note that $AB = (\lambda x.x)(x)$, not $\lambda x. (xx)$.

The general pattern is that type assignment fails when running into loops, when a type wants to be assigned in terms of itself. In the example of , the whole term will have some type $\rho$; and since it is an application term, the functor $x$ must have a function type with input and output $\rho$; that is, : $\sigma = \tau \to \rho$. But the input to this function is again, so the type of the input must be the same as the type of the functor itself: We have =, and hence : $\sigma = \sigma \to \rho$. The fact that occurs on the right-hand side of the equation is precisely the problem. Attempting to assign a simple type to $x$ in this occurrence context will trigger an infinite loop, so $xx$ is not typeable, and neither is any term that contains, or beta-reduces to a term that contains, $xx$ as a subterm. All untypeable terms will have this pattern, where in the type equation =..., occurs again on the right-hand side.

You may want to look into the type assignment algorithm, which has rules to perform certain manipulations on these kinds of type equations. The algorithm will either terminate with a suitable type, if the term is typeable, or with $\mathrm{fail}$, if the term is not typeable, which happens precisely when this sort of loop-structure type assignment is encountered. For the details see e.g. H. Barendregt (1992), Lambda calculi with types, ch. 4.4.

Natalie Clarius
  • 10,530
  • is there a general formula so that I can get two terms A and B which are typeable but when apply they are not? I noticed that my example 1 are two free variables, are there examples in which A and B only involve bound variables? I always like to revise with textbook but the textbook does not give any concrete examples andI am not used to it. – Anon1995 Jun 08 '20 at 22:05
  • 1
    I don't know about a general formula. You certainly don't need free variables to create typeable $A$ and $B$ such that $A,B$ is untypable.. E.g. if $A = \lambda g.\lambda x.g x x$ and $B = \lambda x . x$, then $A$ and $B$ are typable but $A,B$ is not. – Rob Arthan Jun 08 '20 at 22:27
  • The general rule is that type assignment fails when running into loops, when a type wants to be assigned in terms of itself. In the example of $xx$, if we try to assign a type $\sigma$ to $x$, it must be a function type with input $\tau$ and output $\rho$; that is, $xx: \sigma = \tau \to \rho$. But the input will be $x$ again, so the type of the input must be the same as the type of the functor itself: We have $\tau = \sigma$, and hence $xx: \sigma = \sigma \to \rho$. The fact that $\sigma$ occurs on the right-hand side of the equation is precisely the problem. – Natalie Clarius Jun 08 '20 at 22:34
  • All untypeable terms will have this form where in the type equation $\sigma = ...$, $\sigma$ occurs again on the right-hand side. You may want to look into the type assignment algorithm, which makes use of these equations and has a rule fail that fires precisely these loops, indicating that a term is not typeabble. – Natalie Clarius Jun 08 '20 at 22:39
  • Rob Arthan's example will also fall into the category of such loop-structured type assignments, after resolving the application term $AB$ into appropriate type equations. – Natalie Clarius Jun 08 '20 at 22:46
  • Sorry, in my first comment, replace "$xx$" by just "$x$". The type of $xx$ would be $\rho$, the output type of the functor, but the fact that the type of $x$ can not be resolved makes the whole thing untypeable. – Natalie Clarius Jun 08 '20 at 22:53
  • @DanielV No. Typeability in the simply-typed lambda calculus is decidable. The mentioned algorithm exists. See e.g. H. Barendregt's (1992) Lambda calculi with types, ch. 4.4. – Natalie Clarius Jun 09 '20 at 00:57
  • @lemontree Oh thanks. They must be a small enough subset of convergent turing machines that the general restriction doesn't apply. – DanielV Jun 09 '20 at 01:36
  • @DanielV If I am not mistaken (but no warranty on the second part), the situation is: All typeable functions halt, because the typeable terms are strongly normalizing, but not all halting functions are typeable, namely those that are only weakly normalizable, and the functions that don't halt are those that are not normalizable. – Natalie Clarius Jun 09 '20 at 11:02
  • @lemontree Maybe I'm misunderstanding you, isn't $x~x$ strongly normalizing (actually not even containing a redex) but not typeable ? – DanielV Jun 09 '20 at 11:47
  • @DanielV Yes, but there is no contradiction: All typeable terms are strongly normalizable, but not all strongly normalizable terms necessarily are typeable. – Natalie Clarius Jun 09 '20 at 20:47