<p>Be careful: the two <span class="math-container">$y$</span> aren't “the same”, there's a bound one and a free one. You should first perform an α-equivalence step to rename the former:
<span class="math-container">$$\lambda a.a(\lambda yt.t)(ya) =_α λa.a(λzt.t)(ya). $$</span></p>
<p>Also, in the third step you make an erroneous assumption: by assigning to <span class="math-container">$a$</span> the type <span class="math-container">$\beta \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha$</span>, you assume that <span class="math-container">$(ya)$</span> is of type <span class="math-container">$α$</span> and that the whole term is also of type <span class="math-container">$α$</span> (<em>ie.</em> have the same type as <span class="math-container">$t$</span>). There is no reason why this should be the case.</p>
<p>Let's start again from the beginning:</p>
<ul>
<li><span class="math-container">$λzt.t$</span> is of type <span class="math-container">$β\to α\to α$</span> for some <span class="math-container">$α,β$</span>,</li>
<li><span class="math-container">$(ya)$</span> is of type <span class="math-container">$\delta$</span>, where <span class="math-container">$y$</span> is of type <span class="math-container">$\gamma \to \delta$</span> and <span class="math-container">$a$</span> is of type <span class="math-container">$\gamma$</span>, for somme <span class="math-container">$\gamma,\delta$</span>,</li>
<li>then <span class="math-container">$a(λzt.t)$</span> must be of type <span class="math-container">$\delta\to\epsilon$</span>, for some <span class="math-container">$\epsilon$</span>,</li>
<li>then <span class="math-container">$a$</span> must be of type <span class="math-container">$(β\to α\to α)\to \delta \to \epsilon$</span>, for some <span class="math-container">$\epsilon$</span>,</li>
<li>and finally the whole term is of type <span class="math-container">$((β\to α\to α)\to \delta \to \epsilon) \to \epsilon$</span>.</li>
</ul>
<p><span class="math-container">$\gamma$</span> disappeared but we know it is equal to <span class="math-container">$((β\to α\to α)\to \delta \to \epsilon) \to \delta$</span>.</p>
<p>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 (<em>ie.</em> the type of the free variables in subterms).</p>

CC BY-SA 4.0
2023-09-09T09:57:13.910Z
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!
Domiziano Scarcelli
CC BY-SA 4.0
2023-09-09T09:28:40.937Z
2023-09-09T09:28:40.937Z
sparusaurata
<p>I was given an exercise that asked me to assign a simple type to the lambda term:
<span class="math-container">$$
\lambda a.a(\lambda yt.t)(ya)
$$</span>
but I couldn't find one, furthermore, the lambda term seems untypable to me because of the double reference to <span class="math-container">$a$</span>.</p>
<p>This is my reasoning:</p>
<ul>
<li>let <span class="math-container">$t$</span> be of type <span class="math-container">$\alpha$</span>, then <span class="math-container">$\lambda t.t$</span> has type <span class="math-container">$\alpha \rightarrow \alpha$</span>;</li>
<li>let then <span class="math-container">$y$</span> have type <span class="math-container">$\beta$</span>, and so <span class="math-container">$\lambda yt.t$</span> has type <span class="math-container">$\beta \rightarrow \alpha \rightarrow \alpha$</span>;</li>
<li>let now give <span class="math-container">$a$</span> the type <span class="math-container">$\beta \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha$</span>, in order for the term <span class="math-container">$a(\lambda yt.t)$</span> to be of type <span class="math-container">$\alpha \rightarrow \alpha$</span>.</li>
</ul>
<p>From here I want <span class="math-container">$(ya)$</span> to be of type <span class="math-container">$\alpha$</span>, so that the final term <span class="math-container">$a(\lambda yt.t)(ya)$</span> has a well-defined type, but the problem is that <span class="math-container">$y$</span> and <span class="math-container">$a$</span> both have already some defined types, which are not compatible (I cannot apply <span class="math-container">$a$</span> to <span class="math-container">$y$</span>). However I assign types to <span class="math-container">$y$</span> and <span class="math-container">$a$</span>, and I cannot find a type compatibility.</p>
<p>Can you please help me out? Is the lambda term typable in the first place? And if so, where am I wrong?</p>

CC BY-SA 4.0
2023-09-09T02:38:09.687Z
As a gentle suggestion, any Haskell or OCaml compiler will be able to find any simple type, should one exist.
cody
CC BY-SA 4.0
2023-09-09T02:40:43.937Z
There's also the matter of that $y$ variable which seems to be out of scope in your term.
cody
<lambda-calculus><typed-lambda-calculus>
What is the type of the lambda term $\lambda a.a(\lambda yt.t)(ya)$?
Domiziano Scarcelli
# What is the type of the lambda term $\lambda a.a(\lambda yt.t)(ya)$?

(Asked by: username_0 on 2023-09-08)

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?

**Tags:** lambda-calculus, typed-lambda-calculus
> **Comments:**
> **username_1**: As a gentle suggestion, any Haskell or OCaml compiler will be able to find any simple type, should one exist.  
> **username_1**: There's also the matter of that $y$ variable which seems to be out of scope in your term.  

---

## 1 answers

### Answer by username_2 on 2023-09-09. Score: 1 | Accepted answer

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).

> **Comments:**
> **username_0**: 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!  

---

