Some simple operators in the Lambda calculus and their interpretation

84 Views Asked by At

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:

  1. $\hspace{0.2cm}d + e$
  2. $\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$
  3. $\hspace{0.2cm}\text{let} \hspace{0.2cm} x = d \hspace{0.2cm} \text{in} \hspace{0.2cm} e$
  4. $\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?

1

There are 1 best solutions below

2
On

Your examples are not lambda calculus; citing the document you linked:

the work presented here demonstrates the utility of a functional language as a ‘power tool’ for performing experiments in theoretical computer science. At various points we will need to know the most general type of a given form that can be assigned to a lambda expression. This was easily computed using an implementation of a functional language that encorporates the Hindley-Milner type reconstruction algorithm [7, 1]. The implementation used was Gofer, a dialect of Haskell implemented by Mark Jones.

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.