Reduction and Evaluation
Learning Objectives
- You know what a value is in lambda calculus.
- You know the evaluation rules of lambda calculus, and -reduction.
- You can extend lambda calculus with simple constructions such as let expressions.
Here, we focus on the heart of lambda calculus called reduction. Specifically, we talk about -reduction, which encodes computation.
Other reductions have also been studied. We briefly mentioned -reduction in the previous chapter, but -reduction is not used for the dynamics of programming languages, instead, -reduction is.
Reduction
Reduction is a process which turns lambda terms to other lambda terms maintaining the meaning of the term in the process. -reduction is the process of reducing a lambda term step by step towards some value.
Values
The concept of a value is different from part 4, where values had a distinct data type. Instead, in lambda calculus, being a value is just a property of a term. For simplicity, we consider that only an abstraction is a value of lambda calculus, whether or not its body is a value (or even whether it’s complete or not).
Let’s now invent a notation for -reduction. If the term reduces to the term we write .
Here are some examples for -reduction of lambda terms.
- where
We also decide that variables should not reduce to anything, and instead should lead to an error. This is because only complete programs should be evaluated in the first place as complete programs remain complete under -reduction.
-Reduction Rules
We will use the informal lambda calculus notation, but the reader is expected to understand it as just “syntax sugar” for the formal lambda terms defined earlier.
Here is a reminder of the formal definition of lambda terms:
As with any relation, we can express -reduction using a set of inference rules. -reduction is defined as the smallest closure of the following rules:
As usual, we tacitly assume that are lambda terms and is a string.
The purpose of the rule is to reduce the “function term” until it is a value, and reduces the argument until it’s a value. Once the function term has been (hopefully) reduced to an abstraction and the argument to a value, substitutes the variable parameter by the value inside the function body . These rules a written in a way that ensures there’s at most one term that a term can reduce to. Notably this requires that values don’t evaluate to anything, because otherwise could be used with and the same value.
The notation stands for exists unique.
Note that we give no rules for reducing values. This is because a term should not be reduced after it has reached its final value.
Small-step Semantics
The semantics, or more precisely, the dynamics of lambda calculus are described in small-step style, which means that evaluation works one step at a time by doing -reduction repeatedly.
Using the -reduction defined above (along with substitution), we are ready to implement the step function. This is the topic of the next exercise.
Multi-Step Evaluation
The big-step evaluation is typically equivalent to .
Next, implement multistep which applies step repeatedly until reaching a value.
Base Types
So far, we haven’t seen any base types, such as integers or booleans in the lambda calculus, so let’s add them next.
In theory, the theory of integers and booleans is expressible in plain untyped lambda calculus with simply adding syntax sugar for representing them. However, like parsing directly to AST, we can just work and reason with the sugared language and skip the translation/lowering process entirely. This way we need to write more code for type checking and evaluation, but the features of the language are immediately expressible without encoding and decoding. Also then the evaluated terms actually resemble booleans etc. rather than some hard-to-read encoded versions making a REPL for the language more usable.
We will not actually implement booleans in this chapter, but in the next chapter instead.
Let Expressions
Let’s add let expressions, like , to the language.
A note about the syntax: changing to be
;or even just a new line would make the syntax look much more imperative while still being a functional language. Consider trying different variations in your own project.
First, we need to extend the set (type) of terms to include let expressions:
The name is called the “value” assigned to the variable , even though it might not actually be a value and is reducible. The evaluation needs to reduce it to a value before substituting in the .
Now, substitution needs to be changed. Let expressions should have similar semantics as abstractions, so we only substitute in the body if the variables don’t match.
Also, we consider let expressions not values as intuitively we know they can always be reduced.
Evaluation
Evaluation of let expressions works by first reducing the to a value, and then substituting the variable by that value in the .
This can be expressed using the following rules: