I'm exploring the concept of untyped lambda calculus and I'm facing a challenge with defining the isempty function. I have a few definitions that I'm working with, which are:
true = λ xy. x
false = λ xy. y
nil = λ x. x
pair = λ xyb. b x y
Based on these definitions, a list is constructed by combining nil (e.g. (pair x nil)) and pair (e.g. (pair x (pair y nil))). I initially thought that I could define isempty as (λ x. x True ???) since nil evaluates to true. However, the resulting list from a non-empty list would be in the form (True x y), which makes it unclear what to do when neither true nor false can be assigned to x and y.
I'm hoping to get some guidance on how to approach defining the isempty function within the context of untyped lambda calculus.
Given the definitions of $\mathsf{true}, \ \mathsf{false}, \ \mathsf{nil}, \ \mathsf{pair}$ in the OP, a $\lambda$-term representing the function that tests if a list is empty is the following:
$$\mathsf{isempty} = \lambda l. l \, (\lambda x \lambda y.\mathsf{true}) \,\mathsf{false} \, \mathsf{false}$$
Indeed, when $\mathsf{isempty}$ is applied to the empty list, that is, to the $\lambda$-term $\mathsf{nil}$, then $\mathsf{isempty} \, \mathsf{nil} \to_\beta^* \mathsf{true}$ because
\begin{align} \mathsf{isempty} \, \mathsf{nil} &= (\lambda l. l \, (\lambda x \lambda y.\mathsf{true}) \,\mathsf{false} \, \mathsf{false}) \, \mathsf{nil} \\ &\to_\beta \mathsf{nil} \, (\lambda xy.\mathsf{true}) \, \mathsf{false} \, \mathsf{false} \\ &= (\lambda x.x) \, (\lambda xy.\mathsf{true}) \, \mathsf{false} \, \mathsf{false} \\ &\to_\beta (\lambda xy.\mathsf{true}) \, \mathsf{false} \, \mathsf{false} \\ &\to_\beta (\lambda y.\mathsf{true}) \, \mathsf{false} \\ &\to_\beta \mathsf{true} \end{align}
When $\mathsf{isempty}$ is instead applied to a non-empty list, that is, to a $\lambda$-term of the form $\mathsf{pair} \, M \, N$, then $\mathsf{isempty} \, (\mathsf{pair} \, M \, N) \to_\beta^* \mathsf{false}$ because
\begin{align} \mathsf{isempty} \, (\mathsf{pair} \, M \, N) &= (\lambda l. l \, (\lambda x \lambda y.\mathsf{true}) \,\mathsf{false} \, \mathsf{false}) \, (\mathsf{pair} \, M \, N) \\ &\to_\beta (\mathsf{pair} \, M \, N) \, (\lambda xy.\mathsf{true}) \, \mathsf{false} \, \mathsf{false} \\ &= ((\lambda xyb.bxy) \, M \, N)\, (\lambda xy.\mathsf{true}) \, \mathsf{false} \, \mathsf{false} \\ &\to_\beta ((\lambda yb.b\, My) \, N)\, (\lambda xy.\mathsf{true}) \, \mathsf{false} \, \mathsf{false} \\ &\to_\beta (\lambda b.b \, MN)\, (\lambda xy.\mathsf{true}) \, \mathsf{false} \, \mathsf{false} \\ &\to_\beta (\lambda xy.\mathsf{true}) \, M N \, \mathsf{false} \, \mathsf{false} \\ &\to_\beta (\lambda y.\mathsf{true}) \, N\, \mathsf{false} \, \mathsf{false} \\ &\to_\beta \mathsf{true} \, \mathsf{false} \, \mathsf{false} \\ &= (\lambda x y. x) \, \mathsf{false} \, \mathsf{false} \\ &\to_\beta (\lambda y. \mathsf{false} )\, \mathsf{false} \\ &\to_\beta \mathsf{false} \end{align}