Theory of Lambda Calculi

Big Steps, Small Steps

Learning Objectives

  • You understand big-step call-by-name evaluation semantics for lambda calculus.
  • You can derive evaluation trees using the call-by-name rules.
  • You understand single-step Ξ²-reduction and weak-head normal forms.
  • You can implement call-by-name evaluation and Ξ²-reduction step functions in code.

Introduction

Now that we understand and have implemented capture-avoiding substitution, we can define and implement the semantics of lambda calculus. As there are only three kinds of terms, the semantics are really simple on the surface. In fact, most of the complexity lies in the capture-avoiding substitution.

In Variables and Abstraction we briefly mentioned evaluation in lambda calculus. We begin by defining big-step operational semantics and then move to defining small-step semantics for lambda calculus.

From now on, we use the convention that lambda terms are equal, if they are equal up to 𝛼-equivalence. This means that when we are working with the term πœ†π‘₯.π‘₯ it is the same as πœ†π‘¦.𝑦 β€” we say they are mathematically equal.

Big-Step Semantics for Lambda Calculus

Unlike the languages studied in the previous chapter, lambda terms don’t evaluate to an integer or a Value. Instead, lambda terms evaluate to lambda terms, and being a value, almost self-referentially, means being the outcome of evaluation.

To actually make any sense of this idea, let’s look at some examples next. We denote big-step evaluation by the usual ⇓ symbol. The statements have a β€œRust analog” using closures next to them.

Exampleπ‘₯⇓π‘₯x=xπœ†π‘₯.π‘₯β‡“πœ†π‘₯.π‘₯|x| x=|x| x(πœ†π‘₯.π‘₯)𝑦⇓𝑦(|x| x) y=y(πœ†π‘₯.π‘₯)(π‘Žπ‘π‘)β‡“π‘Žπ‘π‘(|x| x) med (a(b)(c))=a(b)(c)(πœ†π‘₯.π‘₯π‘₯)𝑦⇓𝑦𝑦(|x| x(x)) y=y(y)(πœ†π‘₯.πœ†π‘¦.π‘₯)π‘§β‡“πœ†π‘¦.𝑧(|x| |y| x) z=|y| z

Now, let’s define the semantics of lambda calculus. As there are a lot of different ways to define semantics for the lambda calculus, called reduction strategies1 we opt for one of the simplest: call-by-name or CBN.

As we saw in the example, variables don’t evaluate, or rather they evaluate to themselves β€” variables only play a role in substitution. In fact, if the term is β€œwell-typed” we should never need to evaluate a free variable. This is because values are always closed when evaluating well-typed terms.

What it means for a term to be well-typed is defined in the next chapter on the simply typed lambda calculus. For now you can think of well-typed terms primarily as closed terms.

As abstractions house an inner term, we could have a rule to evaluate inside the abstraction. However, this is unnecessary, and done in normalization strategies (which we study in the next chapter) as opposed to the call-by-name strategy.

We will have the following two base rules for the call-by-name evaluation.

π‘₯⇓π‘₯πœ†π‘₯.π‘‘β‡“πœ†π‘₯.𝑑

They state that any variable or abstraction evaluates to itself.

Another evaluation rule in CBN is one that involves both an abstraction and an application. This is where the β€œmagic” happens. If 𝑑1 evaluates to an abstraction, we have an abstraction applied to a term β€” so we can perform a substitution!

π‘“β‡“πœ†π‘₯.𝑓1[π‘₯β†¦π‘Ž]𝑓1β‡“π‘£π‘“π‘Žβ‡“π‘£

Take a moment to read what the rule actually says. Are all the assumptions necessary? It’s important that the substitution is capture-avoiding β€” why?

Finally, we add an evaluation rule to use the result of evaluating 𝑓 in the previous rule. This rule can only be used if 𝑓 doesn’t evaluate to an abstraction (or rather evaluates to a nonabstraction), which we denote with π‘“β‡“π‘“β€²β‰ πœ†π‘₯.βˆ’.

π‘“β‡“π‘“β€²β‰ πœ†π‘₯.βˆ’π‘“π‘Žβ‡“π‘“β€²π‘Ž

As an example, let’s write down the evaluation tree of an identity function applied to the identity function

(πœ†π‘¦.𝑦)(πœ†π‘₯.π‘₯)β‡“πœ†π‘₯.π‘₯ Exampleπœ†π‘¦.π‘¦β‡“πœ†π‘¦.π‘¦πœ†π‘₯.π‘₯β‡“πœ†π‘₯.π‘₯[π‘¦β†¦πœ†π‘₯.π‘₯]π‘¦β‡“πœ†π‘₯.π‘₯(πœ†π‘¦.𝑦)(πœ†π‘₯.π‘₯)β‡“πœ†π‘₯.π‘₯The first and second subderivations are instances of the base rule. As [π‘¦β†¦πœ†π‘₯.π‘₯]𝑦=πœ†π‘₯.π‘₯, the rightmost subderivation is also an instance of the base rule. Therefore the derivation is valid.

As πœ†π‘₯.π‘₯ is 𝛼-equivalent with πœ†π‘¦.𝑦, it doesn’t matter what the actual bound variables are. Of course a computational implementation has to decide which bound variables to use (or which fresh variables to use in capture-avoiding substitution), but that’s just an implementation detail which has no effect on the theory.

Here are some more examples of call-by-name evaluation:

Example(πœ†π‘₯.πœ†π‘¦.π‘₯)(πœ†π‘¦.πœ†π‘§.𝑦)β‡“πœ†π‘¦.πœ†π‘¦.πœ†π‘§.𝑦(πœ†π‘₯.π‘₯)((πœ†π‘₯.π‘₯)𝑦)⇓𝑦(πœ†π‘₯.πœ†π‘¦.π‘₯)(𝑧𝑦)β‡“πœ†π‘¦β€².𝑧𝑦(πœ†π‘₯.πœ†π‘¦.π‘₯)(πœ†π‘§.𝑦)β‡“πœ†π‘¦β€².πœ†π‘§.𝑦((πœ†π‘₯.π‘₯)𝑦)(πœ†π‘§.𝑧)⇓𝑦(πœ†π‘§.𝑧)(πœ†π‘₯.π‘₯𝑦)(πœ†π‘§.𝑧)⇓𝑦

Notice that in the examples, evaluating terms that contain free variables may result in a term which is a variable or even an application. The set of terms that result from CBN evaluation are said to be in weak-head normal form.

ExampleThe following terms are in weak-head normal form as they evaluate to themselves.πœ†π‘₯.π‘₯πœ†π‘₯.πœ†π‘¦.π‘₯π‘₯(πœ†π‘¦.𝑦)π‘₯𝑦𝑧π‘₯((πœ†π‘¦.𝑦)𝑧)(π‘₯𝑧)(πœ†π‘¦.𝑦)

Implementing Call-By-Name Evaluation

As the call-by-name evaluation is just a relation, we would like to turn it into at least a partial function.

The function, called cbn evaluates a term 𝑑 by computing the value of ? that 𝑑 evaluates to:

𝑑⇓?

This makes us ask a couple of important questions about the ⇓ relation:

  1. Does ? always exist? If so, ⇓ is left-total.
  2. Is the value of ? unique for a given 𝑑? If so, ⇓ is functional.
  3. Can we write an algorithm to compute ??

We put questions 1 and 2 aside for now and instead focus on question 3 by implementing an algorithm that does call-by-name evaluation.

Big-Step Call-By-Name Evaluation

0 / 5 points

Which of the following statements about big-step call-by-name evaluation are true?

Call-By-Name Evaluation (Big-Step)

0 / 30 points

Implement cbn according to the call-by-name semantics described in the material.

Examples

For example, the following terms should evaluate to the results on the right (up to alpha-equivalence).

(x => y => x) (y => z => y) ⇓ y => y => z => y
      (x => x) ((x => x) y) ⇓ y
        (x => y => x) (z y) ⇓ y_ => z y
     (x => y => x) (z => y) ⇓ y_ => z => y
        (x => y x) (z => z) ⇓ y (z => z)
        (x => x y) (z => z) ⇓ y

Grading

Only the cbn function is tested. The term it returns is compared to the expected term up to alpha-equivalence, i.e. you can use any fresh variables you want as long as the result is alpha-equivalent with the correct term.

t! Macro

A macro t! is provided to make it much more convenient to write lambda terms in Rust. For example t!(x => y => x) expands to the lambda term Ξ»x. Ξ»y. x.

The macro also supports embedding an external lambda term using an exclamation mark. For example, if t is the lambda term Ξ»y. x then t!(x => !t) expands to the lambda term Ξ»x. Ξ»y. x.

Single-Step Semantics

Now that we have a basic understanding of evaluation of lambda terms, we expand it with the notion of small-step semantics by studying the single-step 𝛽-reduction. Instead of evaluating the whole term at once, 𝛽-reduction happens step-by-step. 𝛽-reduction also tends to be nonfunctional meaning that a term can take different reduction steps, e.g. reducing the function or the argument position in an application β€” or any reducible subterm. We denote (single-step) 𝛽-reduction using an arrow symbol ⟢.

𝛽-reduction has many slightly different formulations1 and has a lot of literature written about it. We highly recommend reading chapters 2.4 and 2.5 from Selinger: Lecture Notes on the Lambda Calculus.

Weak 𝛽-Reduction

The notion of 𝛽-reduction is much more general than defined here. We will learn another, stronger version of it in the next chapter.

Our first version will be like the call-by-name evaluation studied earlier as it doesn’t evaluate the arguments at all. It gets the name weak, because it doesn’t reduce under abstractions and produces weak-head normal forms when reducing until no reductions can be made.

The first, and most important, rule called AppAbs is the β€œheart of the lambda calculus”. Let’s go over it thoroughly. The rule states that an application term (πœ†π‘₯.𝑑1)𝑑2 where the left-hand-side is an abstraction reduces to the substitution of π‘₯ by 𝑑2 in 𝑑1 which is the term [π‘₯↦𝑑2]𝑑1. Here it is written as an inference base rule without premises:

AppAbs(πœ†π‘₯.𝑑1)𝑑2⟢[π‘₯↦𝑑2]𝑑1 ExampleEach of the following is a valid instance of the AppAbs rule.(πœ†π‘₯.π‘₯)(πœ†π‘§.𝑧)βŸΆπœ†π‘§.𝑧(πœ†π‘₯.π‘₯)(πœ†π‘§.𝑧)βŸΆπœ†π‘¦.𝑦(=π›Όπœ†π‘§.𝑧)(πœ†π‘₯.πœ†π‘¦.π‘₯)(πœ†π‘¦.πœ†π‘§.𝑦)βŸΆπœ†π‘¦.πœ†π‘¦.πœ†π‘§.𝑦(πœ†π‘₯.π‘₯)((πœ†π‘₯.π‘₯)𝑦)⟢(πœ†π‘₯.π‘₯)𝑦(πœ†π‘₯.πœ†π‘¦.π‘₯)(𝑧𝑦)βŸΆπœ†π‘¦β€².𝑧𝑦(πœ†π‘₯.π‘₯𝑦)(πœ†π‘§.𝑧)⟢(πœ†π‘§.𝑧)𝑦

Notice that the AppAbs rule allows us to only perform one substitution at a time, so e.g.

(πœ†π‘₯.π‘₯𝑦)(πœ†π‘§.𝑧)⟢(πœ†π‘§.𝑧)π‘¦βŸΆπ‘¦

but (πœ†π‘₯.π‘₯𝑦)(πœ†π‘§.𝑧)βŸΆπ‘¦ is not a 𝛽-reduction step directly.

Next, we explore the other single-step 𝛽-reduction rules. These rules are like β€œadapters” that let us reduce subterms. For 𝛽-reduction to do anything useful, we need a way to reduce the left subterm of an application:

𝑑1βŸΆπ‘‘β€²1App1𝑑1𝑑2βŸΆπ‘‘β€²1𝑑2

This is because the only other rule AppAbs requires an abstraction as the left subterm of an application. Reducing the right subterm does not get us any closer to being able to use AppAbs.

One can think of AppAbs as the rule that drives progress. Every other rule is there to get us closer to using AppAbs or to simplify the lambda term to a nicer form.

Valid AppAbs Instances

0 / 5 points

Which of the following are instances of the AppAbs rule?

Valid App1 Instances

0 / 5 points

Which of the following are conclusions of an instance of the App1 rule whose premises are valid?

Weak Single-Step Beta-Reduction (Small-Step)

0 / 45 points
  • First, fill in your previous implementation.
  • Next, implement app_abs, app1 such that app_abs attempts to apply the AppAbs rule, app1 attempts to apply the App1 rule.
  • Finally, implement step which attempts to reduce using either app_abs or app1.

If any application of a rule fails, return None.

Note: app1 should use step to reduce the inner term.

Hint: use Option::or_else to combine the results from self.app_abs() and self.app1().

Examples

(x => y => x) (y => z => y) --> y => y => z => y
      (x => x) ((x => x) y) --> (x => x) y
        (x => y => x) (z y) --> y_ => z y
     (x => y => x) (z => y) --> y_ => z => y
        (x => y x) (z => z) --> y (z => z)
        (x => x y) (z => z) --> (z => z) y
                 x (z => z) --> None

Grading

Only the app_abs, app1, and step functions are tested. The terms these functions return are compared to the expected terms up to alpha-equivalence.

Now that you hopefully found a working implementation, the following quizzes will probe your understanding a bit further. A key detail to unlock the correct answers is to think about the relationship between the AppAbs and App1 rules. For example, is it possible for 𝑑1 to be an abstraction in the premise 𝑑1βŸΆπ‘‘β€²1 of App1?


Order of Rules in Implementation

0 / 5 points

What happens if the order in which App1 and AppAbs are attempted is swapped in the implementation of step?

Weak Beta-Reduction

0 / 8 points

Which of the following statements are true?

Footnotes

Footnotes

  1. See for example Sestoft: Demonstrating Lambda Calculus Reduction or Wikipedia: reduction strategy. ↩ ↩2

← Alpha Equivalence and Capture-Avoiding Substitution
Multiple Steps and Normalization →