$\lambda$-Calculus

box

Lambda Calculus (LC) is a rigorious mathematical system. It's quite unique, and surprisingly powerful. So much of modern functional programming languages are directly based on LC.

LC is a system that describes functions and their actions.

Definition

We need to begin with a formal definition of LC expressions. The definition is recursive.

• Expression:

  $\mathbf{expression}$ can be a $\mathbf{name}$, $\mathrm{function}$ or $\mathbf{application}$.

• Names:

  Names can be any thing: $\mathrm{fred}$, $\mathrm{12}$, $x$, $y$, $\dots$.

• Function Abstraction:

  $\mathbf{function}$ is of the form $\lambda \mathbf{name}.\mathbf{expression}$.

  The bound variable and body of the function expression are defined as:

  $$\lambda\underbrace{\mathbf{name}}_\mathrm{bound\ variable}.\ \underbrace{\mathbf{expression}}_\mathrm{body}$$

• Function Application:

  $\mathbf{application} : (\mathbf{function}\ \ \mathbf{expression})$

Some examples

Here are some examples of LC expressions.

• Just a name: $x$

• An expression that is a function expression: $\lambda x. x$. It's built using the abstraction rule.

• An expression that is an application: $(x\ y)$. It's built using the application rule.

• More application expression:

  • $((\lambda x. (x\ y))\ y)$
  • $\lambda\mathsf{first}.\lambda\mathsf{second}.\mathsf{first}$

Semantics

• Lambda expressions in the form of $\lambda x. e$, built by the abstraction rule, describe functions that accept one argument named $x$, and return the expression $e$.

• Application $(e_1 e_2)$ will evaluate the function represented by $e_1$ when its argument is $e_2$.

Important properties:

1. All expressions are functions.

2. All functions accept exactly one input.

Currying

• Currying in Python

  Currying is a technique that allows us to implement functions with multiple inputs using nested single-input functions. This is best explained by the followin Python code:

  split

  def add(x,y):
      return x + y
  
  add(1, 2) # => 3
  

  def add(x):
      def f(y):
          return x + y
      return f
  
  add(1)(2) # => 3
  

• Definition of currying

  box

  Currying is to construct nested functions, each is taking only one argument, but the body of the inner functions depend on the arguments of the outter functions. This can be done in $\lambda$-calculus with function abstractions.

  For example: $$ \lambda x.\lambda y. (x\ y)$$

• Functions with multiple inputs in $\lambda$-calculus.

  When dealing with multiple inputs done via currying, for readability, we will drop the parentheses.

  Suppose we have $f$ is a function with three inputs: $f = \lambda x.\lambda y.\lambda z.\mathrm{body}$. $$ (((f\ x)\ y)\ z) \Rightarrow (f\ x\ y\ z) $$

Evaluation

Let's describe how a complex expression is evaluated by $\lambda$-Calculus.

Free vs bound variable occurrences

• Let $e$ be an expression. A variable occurrence is a name at a specific position that is not following $\lambda$.

  Consider $e = (x\ \lambda x.x)$. There are two variable occurrences, both of the name $x$. To distinguish the two occurrences, we will use subscripts: $$ e = (x_1\ \lambda x.x_2) $$

• Free and bound occurrences:

  box

  Definition: Free occurrences

  Let $\mathrm{Var}(e)$ be all the variable occurrences in $e$. We define the free occurrences $\mathrm{Free}(e)$ by induction:

  • $\mathrm{Free}(x) = \{x\}$

  • $\mathrm{Free}(\lambda x.\ e) = \mathrm{Free}(e) - \{x\}$

  • $\mathrm{Free}(e_1 e_2) = \mathrm{Free}(e_1) \cup \mathrm{Free}(e_2)$

  box

  Definition: Bound occurrences

  $$\mathrm{Bound}(e) = \mathrm{Var}(e) - \mathrm{Free}(e)$$

Some examples

• $\mathrm{Free}(y) = \{y\}$

• $\mathrm{Free}(x) = \{x\}$

• $\mathrm{Free}((x\ y)) = \mathrm{Free}(x) \cup \mathrm{Free}(y) = \{x\}\cup\{y\} = \{x, y\}$

• $\mathrm{Free}(z) = \{z\}$

• $\mathrm{Free}(\lambda z. z) = \mathrm{Var}(z) - \{z\} = \emptyset$

• $\mathrm{Free}(z_1\ \lambda z. z_2) = \mathrm{Free}(z_1)\cup\mathrm{Free}(\lambda z. z_2) = \{z_1\}\cup\emptyset = \{z_1\}$

  Note: since there are two occurrences of $z$, we need to distinguish them by the subscripts $z_1$ and $z_2$. Only the first occurrence $z_1$ is free.

• $\mathrm{Free}((x\ y)\ (z_1\ \lambda z.z_2)) = \{x,y\}\cup\{z_1\} = \{x, y, z_1\}$

• $\mathrm{Free}(\lambda y.((x\ y)\ (z_1\ \lambda z.z_2))) = \mathrm{Free}((x\ y)\ (z_1\ \lambda z.z_2)) - \{y\} = \{x, z_1\}$

• $\mathrm{Free}(\lambda x.\lambda y.(x\ y)\ (z_1\ \lambda z.z_2)) = \mathrm{Free}(\lambda y.(x\ y)\ (z_1\ \lambda z.z_2)) - \{x\} = \{z_1\}$

• $\mathrm{Free}(x\ \lambda x.\lambda y.(x\ y)\ (z_1\ \lambda z.z_2)) = ?$

  There are two occurrences of $x$, so we need to disambiguate them. $$\begin{eqnarray} && \mathrm{Free}((x_1\ (\lambda x.\lambda y.(x_2\ y)\ (z_1\ \lambda z.z_2)))) \\ &=& \mathrm{Free}(x_1)\cup\mathrm{Free}(\lambda x.\lambda y.(x_2\ y)\ (z_1\ \lambda z.z_2)) \\ &=& \{x_1\} \cup \{z_1\} \\ &=& \{x_1, z_1\} \end{eqnarray}$$

  Thus the first $x$ and the first $z$ are free.

Parameter substitution

• Substitution in expression:

  box

  Definition: substitution

  Let $e$ be an expression, and $x_i\in\mathrm{Var}(e)$ be an occurrence. The new expression $e[x_i/e']$ is the expression that replaces $x_i$ with $e'$.

• Parameter renaming:

  We observe that $\lambda x. x$ and $\lambda z.z$ are identifical functions. Both describe the same identity function. The only difference is what name is used for the parameter.

  This suggest that we can rename the parameter of function expressions as long as the new paramter name is not free in the body.

  box

  Given a function expression $\lambda x.e$, if $z\not\in\mathrm{Free}(e)$, we have: $$\lambda z.e[x/z] = \lambda x.e$$

  This is historically known as the $\alpha$ (alpha) conversion.

• Function application

  box

  Consider function application $((\lambda x. \mathrm{body})\ e_2)$.
  If we have $\mathrm{Var}(e_2)\cap\mathrm{Bound}(\mathrm{body}) = \emptyset$, then we can perform the following transformation:

  $$ ((\lambda x.\mathrm{body})\ e_2) = \mathrm{body}[x/e_2] $$

  This is historically known as the $\beta$ (beta) conversion.

• Ensuring correctness in function application

  So what happens the names in the input $e_2$ appears as a bound occurrence in $\mathrm{body}$?

  • A naive substitution will yield an incorrect computation.
  • We can always use $\alpha$ conversion to rename the bound name to something else.

• Code optimization with $\eta$-conversion

  One final expression rewrite rule deals with code optimization. Consider the expression:

  $$ (\lambda x. (f\ x)) $$

  It's easy to convince yourself that it can be simplified to just $f$.

  box

  The $\eta$ conversion:

  For any expression $e$, we have: $$ (\lambda x. (e\ x)) = e $$

Computation with $\lambda$-Calculus

box

$\lambda$-Calculus applies the three conversion rules to simplify expressions.

1. $\alpha$ conversion: parameter renaming
2. $\beta$ conversion: parameter substitution
3. $\eta$ conversion: cancel out abstraction over application

Normal form

• Application of conversion

  Given an expression $e$, there may be multiple conversions that can happen. We would write:

  $e \underset{\alpha}{\longrightarrow} e'$ to indicate that $e'$ is obtained from $e$ via an alpha conversion.

  We successively generate sequences of expression rewrites:

  $e_1 \underset{\dots}\longrightarrow e_2 \longrightarrow e_3 \dots$

• Normal form

  box

  Definition: normal form

  An expression $e$ is in the normal form if no $\beta$ conversion can be applied. Namely, all function applications that can be resolved are resolved.

  We will denote the normal form of some expression $e$ as ${e}^*$.

Computation

• We can use the expression rewrite as a mechanism for computation.

• Encoding

  Given a problem $\mathbf{P}$, we need to design an encoding function that maps instances of $\mathbf{P}$ to $\lambda$-Calculus expression, denoted as $\mathbf{LC}$: $$\mathbf{Encode} : \mathbf{P} \to \mathbf{LC}: I \mapsto\mathbf{Encode}(I)$$

• Decoding

  We also need a decoding function that can convert an expression to a solution of $\mathbf{P}$.

  $$\mathbf{Decode}: \mathbf{LC}\to\mathrm{Sol}(\mathbf{P})$$

• Rewriting

  Use expression rewriting to obtain a normal form $\mathbf{Encode}(I)^*\in\mathbf{LC}$

• Interpret result

  Apply the decoding function to obtain the solution: $\mathbf{Decode}(\mathbf{Encode}(I)^*)$.