Is there a lambda calculus term $s$ such that $s(tu)$ is $\beta$-equal to $u$ for all untyped lambda calculus terms $u$ and $t$

76 Views Asked by At

Is it possible to find a lambda term $s$ such that for all terms $t$ and $u$ (of untyped lambda calculus) , $s(tu) = u $ where the equality refers to $\beta$-equality?

I thought that no such $s$ should exist since I don't see how any beta reduction rules would allow us to peel away the brackets so to speak.

1

There are 1 best solutions below

0
On BEST ANSWER

Suppose that such a thing existed. Then if we pick:

$$t = λx. λy. y$$

We have:

$$t\ u =_β λ y. y$$

for all $u$. This would mean that:

$$s\ (λ y. y) =_β u$$

for all $u$. However, there are many (β) distinct lambda terms $u$, so this is impossible.