We have some cases that we say lambda term is not typable
for example $Ω=(λx.xx)(λx.xx)$.
I got a question about type of the term
$λxab.xa(xb)$
Here, the first occurrence of $x$ receive $a$ and $(xb)$
and the second occurrence of $x$ receive $(b)$.
I assumed that i can't give a type because of this.
Is it correct ? If not the what's the type of it ?
Best Answer
Your intuition is correct, but you need a proof of it: you can find it below.
The term $λxab.xa(xb)$ is not typable with simple types (which is the type system you are considering). Indeed, if the term $λxab.xa(xb)$ were typable, the first occurrence of $x$ (from the left) should have type $A \to (C \to D)$, where $A$ is the type of $a$ (the first argument of $x$) and $C$ is the type of $xb$ (the second argument of $x$). Then, the second occurrence of $x$ (from the left) should have type $B \to C$ where $B$ is the type of $b$.
Summing up, the variable $x$ should have at the same time the types $A \to (C \to D)$ and $B \to C$, but $x$ can have only one type. Therefore, it should be $A \to (C \to D) = B \to C$, which would imply $A = B$ and $C \to D = C$. Now, there is no type $C$ such that $C \to D = C$, so it is impossible that $A \to (C \to D) = B \to C$ and hence there is no type for $x$, thus the term $λxab.xa(xb)$ is not typable.