# Is $\Gamma \vdash x x : T$ possible in the simply typed lambda calculus?

Is $$\Gamma \vdash x x : T$$ possible?

This problem appears on page 104 of Benjamin Pierce's "Types and Programming Languages".

My conclusion is that it is was the case then we would get $$x: T_1 \to T_2$$ and $$x: T_1$$ and by some axiom, these types are not equal.

The problem is identifying this axiom but I fear it might be possible to have this equality...

Any hints?

• There's no way to unify $T_1 \to T_2$ and $T_1$ which means (by the typing rule for variables) we would have $x:\tau \in \Gamma \wedge x:\sigma \in \Gamma$ with $\tau \neq \sigma$, which would mean $x$ is not well-typed. Oct 1, 2019 at 20:46

You are on the right track. The argument you would use is on the lines of size of types defined below: (I am assuming you are in the world of simply typed $$\lambda$$-calculus)
$$size(T) = 1$$
$$size(T \to T') = size(T) + size(T')$$
Unification will only work if the size of types is equal, and in this case $$size(T \to T') > size(T)$$ hence there cannot be such a term.
However, if you add recursion/non-termination in the type system. You can indeed have such a term. $$\vdash (\lambda x. x x) (\lambda x. x x):\bot$$
$$\bot$$ is the type that represents non-termination.