what are the cases that we can say that the lambda term is not typable?

191 Views Asked by At

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 ?

1

There are 1 best solutions below

0
On 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.