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$

Question

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.

What's the reason for the downvoting? – Taroccoesbrocco May 25 '22 at 13:38 — Taroccoesbrocco, May 25 '22 at 13:38

score 2 · Accepted Answer · answered May 27 '22 at 03:39

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.

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$

1 Answers1