# Is the expression (λx.xx)(λy.y) typeable in the following system?

We are given a simple functional language:

$$e ::= x | n | e_{1}e_{2}|\lambda(x:\tau).e$$

with types:

$$\tau ::= \text{int} | \tau_{1} \rightarrow \tau_{2}| \tau_{1} \land \tau_{2}$$

Is the expression $$(\lambda x.xx) (\lambda y . y)$$ typeable in this system?

Let's denote $$x:\tau_{x}, xx : \tau_{xx}$$. I'm rookie in the field and so far I have only dealt with very simple systems where type equations as the one we get for left subterm: $$\tau_{x} = \tau_{x} \rightarrow \tau_{xx}$$ indicated a term analyzed is not typeable . The type $$\tau_{1} \land \tau_{2}$$ is something new to me and I don't have intuition what can or cannot be done here.

• Search "intersection types" on this site, I think you'll find useful information. The answer is yes because all strongly normalizing terms are typable. – Gilles Jun 15 at 15:29