In Phillip Wadler's "Monads and composable continuations" (published in Lisp and Symbolic Computation, 1994, doi.org/10.1007/BF01019944) the following rules (amongst others) are listed as being part of the Lambda calculus:
- $\hspace{0.2cm}d + e$
- $\hspace{0.2cm} \text{if}\hspace{0.2cm} c \hspace{0.2cm} \text{then} \hspace{0.2cm} d \hspace{0.2cm} \text{else} \hspace{0.2cm} e$
- $\hspace{0.2cm}\text{let} \hspace{0.2cm} x = d \hspace{0.2cm} \text{in} \hspace{0.2cm} e$
- $\hspace{0.2cm}\text{letrec} \hspace{0.2cm} f = (\lambda x . d) \hspace{0.2cm} \text{in} \hspace{0.2cm}e$
However, I do not know what their precise interpretation in the Lambda calculus is. Can anyone provide me with their interpretations?
Your examples are not lambda calculus; citing the document you linked:
While the first 2 examples can be expressed in pure lambda calculus (e.g. using the Church encoding), it is impossible with the latter 2, as it only has anonymous functions.