-1
$\begingroup$

I was given an exercise that asked me to assign a simple type to the lambda term: $$ \lambda a.a(\lambda yt.t)(ya) $$ but I couldn't find one, furthermore, the lambda term seems untypable to me because of the double reference to $a$.

This is my reasoning:

  • let $t$ be of type $\alpha$, then $\lambda t.t$ has type $\alpha \rightarrow \alpha$;
  • let then $y$ have type $\beta$, and so $\lambda yt.t$ has type $\beta \rightarrow \alpha \rightarrow \alpha$;
  • let now give $a$ the type $\beta \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha$, in order for the term $a(\lambda yt.t)$ to be of type $\alpha \rightarrow \alpha$.

From here I want $(ya)$ to be of type $\alpha$, so that the final term $a(\lambda yt.t)(ya)$ has a well-defined type, but the problem is that $y$ and $a$ both have already some defined types, which are not compatible (I cannot apply $a$ to $y$). However I assign types to $y$ and $a$, and I cannot find a type compatibility.

Can you please help me out? Is the lambda term typable in the first place? And if so, where am I wrong?

$\endgroup$
2
  • $\begingroup$ As a gentle suggestion, any Haskell or OCaml compiler will be able to find any simple type, should one exist. $\endgroup$
    – cody
    Sep 9, 2023 at 2:38
  • 1
    $\begingroup$ There's also the matter of that $y$ variable which seems to be out of scope in your term. $\endgroup$
    – cody
    Sep 9, 2023 at 2:40

1 Answer 1

1
$\begingroup$

Be careful: the two $y$ aren't “the same”, there's a bound one and a free one. You should first perform an α-equivalence step to rename the former: $$\lambda a.a(\lambda yt.t)(ya) =_α λa.a(λzt.t)(ya). $$

Also, in the third step you make an erroneous assumption: by assigning to $a$ the type $\beta \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha$, you assume that $(ya)$ is of type $α$ and that the whole term is also of type $α$ (ie. have the same type as $t$). There is no reason why this should be the case.

Let's start again from the beginning:

  • $λzt.t$ is of type $β\to α\to α$ for some $α,β$,
  • $(ya)$ is of type $\delta$, where $y$ is of type $\gamma \to \delta$ and $a$ is of type $\gamma$, for somme $\gamma,\delta$,
  • then $a(λzt.t)$ must be of type $\delta\to\epsilon$, for some $\epsilon$,
  • then $a$ must be of type $(β\to α\to α)\to \delta \to \epsilon$, for some $\epsilon$,
  • and finally the whole term is of type $((β\to α\to α)\to \delta \to \epsilon) \to \epsilon$.

$\gamma$ disappeared but we know it is equal to $((β\to α\to α)\to \delta \to \epsilon) \to \delta$.

However, instead of writing the proof like this, you should write a derivation tree which would enable you to keep better track of the context (ie. the type of the free variables in subterms).

$\endgroup$
1
  • $\begingroup$ Thanks so much for the answer. Yes, I know about the tree structure to solve the problem but I didn't know how to write it here. I didn't think about the two y as different variables, but now everything makes sense. Thanks again! $\endgroup$ Sep 9, 2023 at 9:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.