Often called the

c. elegansof programming languages: an extremely well-studied “model organism” in biology. Important for its minimal, but still extensive properties.

Created by Alonzo Church in the 1930s. A minimal programming language. It only has variables, functions, and function application. Even while untyped, it is still Turing complete. In OCaml syntax:

## Free and bound variables, scoping

In the expression $funy→x+y$, the variable $x$ is considered *free* while $y$ is *closed*.

- Free variables are defined in an outer scope. We don’t know what $x$ will be yet.
- Bound variables are defined in the function. Here, $funy$ binds $y$, and it is considered in scope in the body $x+y$.

Terms that have only have bound variables are considered closed, and terms that have free variables are called open.

Expressions that are just a variable like $x$ are considered singletons. Not free nor closed.

### Alpha equivalence

$funx→y+x$ and $funz→y+z$ are equivalent and only differ in variable naming. Here, both functions use the name consistently and therefore have the same meaning.

They are considered *alpha equivalent* because if we consistently replaced every instance of $x$ with $z$ in the first function, they would be the exact same.

Students who cheat by renaming variables are exploiting alpha equivalence…

However, *the naming of free variables does matter*. Above, naming $y$ is intentional. The intuition is that an outside scope may define a variable named $y$, so naming it something else changes the way the function works.

## Values and substitution

The only values in lambda calculus are *closed* functions.

We can *substitute* a closed value $v$ for some variable $x$ in an expression $e$. This is how function application works: replace all *free* occurrences of $x$ in $e$ with $v$. Mathematical notation for this is $e{v/x}$. Some properties:

- $x{v/x}=v$. We’re replacing $x$ with $v$.
- $y{v/x}=y$, assuming that $y=x$. Nothing changes because the expression doesn’t have $x$ in the first place.
- $(funx→exp){v/x}=(funx→exp)$. $v$ does not replace $x$ because it’s
*already bound*in the function definition. - $(funy→exp){v/x}=(funy→exp{v/x})$. We pass the substitution into the expression given by the function definition. This assumes that $y=x$.
- $(e_{1}e_{2}){v/x}=(e_{1}{v/x}e_{2}{v/x})$. We pass the substitution on to the two expressions.

### Capture-avoiding substitution

Consider $e_{1}{e_{2}/x}$. $e_{2}$ might mention a variable that is already bound in $e_{1}$. This behavior is usually not intentional (some languages implement this as a feature, e.g. Emacs Lisp), so we can rename conflicting variables by *picking an alpha equivalent version*. We respect scope:

Here, we consistently rename all $x$‘s to $x_{′}$ so that when we replace $y$ with $funz→x$, the $x$ in this function cannot possibly conflict with $x_{′}$.

## Implementing first-class functions

Applying lambda calculus, many programming languages (e.g. OCaml, Haskell, Scheme, Python, C#, Java, Swift) allow functions to be passed as arguments, returned as values, and nested within each other. There are many ways to implement this in a compiler.

### Environment-based interpreter, closures

When evaluating, we also interact with an *environment*, which simply maps variables to their values. Extend and remove bindings from the environment as we execute function calls.

A **closure** is a pair of an environment and a code pointer.

- The environment can be implemented as a map of variables to values.
- A
*code pointer*is the first-class function, modified to take an additional argument for the environment. If we have a function`A -> B`

, in OCaml syntax we can have a function pointer type of`(Env * A -> B)`

To apply a closure, we simply invoke the environment associated with it and then call the function with the environment and its other, “real” arguments.

Since the first-class function now has all the context it needs to operate (contained within the environment data structure), we’re able to *hoist* it out and lift it to the top level.