Often called the c. elegans of 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 , the variable is considered free while is closed.
- Free variables are defined in an outer scope. We don’t know what will be yet.
- Bound variables are defined in the function. Here, binds , and it is considered in scope in the body .
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 are considered singletons. Not free nor closed.
Alpha equivalence
and 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 with 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 is intentional. The intuition is that an outside scope may define a variable named , 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 for some variable in an expression . This is how function application works: replace all free occurrences of in with . Mathematical notation for this is . Some properties:
- . We’re replacing with .
- , assuming that . Nothing changes because the expression doesn’t have in the first place.
- . does not replace because it’s already bound in the function definition.
- . We pass the substitution into the expression given by the function definition. This assumes that .
- . We pass the substitution on to the two expressions.
Capture-avoiding substitution
Consider . might mention a variable that is already bound in . 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 ‘s to so that when we replace with , the in this function cannot possibly conflict with .
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.