Exercise Sheet 3:

Teacher: Delia Kesner

\[\newcommand\n{\mathrm{n}}\]

TD 3

Exercise 1 (Relation between $λ$ and $λlxr$)

1.

\[t = (λx.xy)(λz.y)\\ A((λx.xy)(λz.y)) = C^{y_1, y_2}_y ((λx. xy_1) (λz.W_z \, y_2))\]

2.

NB: $C^{y_1, y_2}_y ((λx. xy_1) (λz.W_z \, y_2)) ∈ SN^{λlxr}$ since $(λx.xy)(λz.y) ∈ SN^β$

\[\begin{align*} C^{y_1, y_2}_y ((λx. xy_1) (λz.W_z \, y_2)) & ⟶_B C^{y_1, y_2}_y ((xy_1) [x/ (λz.W_z \, y_2)]) \\ & ⟶_{App_1} C^{y_1, y_2}_y ((x [x/ (λz.W_z \, y_2)]) y_1)\\ & ⟶_{Var} C^{y_1, y_2}_y ((λz.W_z \, y_2) y_1)\\ & ⟶_B C^{y_1, y_2}_y ((W_z \, y_2) [z/y_1])\\ & ⟶_{Weak_1} C^{y_1, y_2}_y (W_{y_1} \, y_2)\\ & ⟶_{Merge} R^{y_2}_y (y_2) = y \end{align*}\]

3. Exhibit a term $t_1$ such that $t_1 = A(B(t_1))$

\[t_1 =\]