Extensions to Lambda Calculus

Introduction

In the previous chapter we looked at how Church encoding could be used as a foundation for boolean and natural number operations. The final language even supported addition and multiplication, but you may have noticed that it had a couple of features missing — notably subtraction and comparison. The reason we left these out is that they are quite complicated to encode into plain lambda calculus.

To demonstrate, although we wont be using Church encoding in this chapter, to get subtraction, one would begin by defining the “predecessor” function The predecessor pred returns , and as we are working in natural numbers, the predecessor of is natural to define as . Applying the predecessor to times we get . Together these are the following lambda terms:

Here is the Wikipedia explanation of pred if you are interested.

Using minus and is_zero it would be now easy to check if one number is less than or equal to another.

Instead of continuing this route, we will be adding so called extensions to lambda calculus which which are like primitive types and their operations.

Boolean Extension

We start by extending the notion of a lambda term with the terms True, False and Ite.

#[derive(Debug, Clone)]
pub enum Term {
    // Core lambda calculus
    Var(String),
    Abs { var: String, body: Box<Term> },
    App(Box<Term>, Box<Term>),

    // Boolean extension
    True,
    False,
    Ite {
        cond: Box<Term>,
        if_true: Box<Term>,
        if_false: Box<Term>,
    },
}

This time, instead of desugaring to core untyped lambda caclulus, we extend the -reduction so that it works with the boolean extension. As there is nothing to reduce in True and False, they are considered normal forms or values by themselves. However, an if-then-else needs reduction rules.

Just like the App1/2 rules reduce the subterms in applications

we have Ite1/2/3 rules for reducing the subterms inside an if-then-else term

Now for the core functionality of an if-then-else: If the condition is true, we reduce the Ite to the “if true” branch, and likewise if it’s false.

As we have changed the terms of our language, we need to also make adjustments to various functions:

• True and False don’t contain any free variables
• To compute the set of free variables, we need to also take the union of free variables in subterms of if-then-else:
• Substitution and renaming need to recursively go through if-then-else subterms

Finally, -equivalence needs a similar update. Luckily this is not a big deal as the boolean fragment doesn’t include any new variable binding sites.

Natural Numbers

With booleans it was quite easy to decide which primitive operations to include, namely if-then-else. However, when it comes to natural numbers, we are not going to add numerals, addition, subtraction, etc. but a set of primitives that can be used to define almost every¹ function we need:

1. Zero
2. Successor
3. Primitive recursion (i.e. the recursor)

Now is a good time to recap the contents of Objects and Compatibility and specifically what the recursor is. Here is what the new terms Zero, Succ and Rec look like in Rust

#[derive(Debug, Clone)]
pub enum Term {
    // Core lambda calculus
    // ...

    // Boolean extension
    // ...

    // Natural number extension
    Zero,
    Succ(Box<Term>),
    /// Recursor for natural numbers. Takes in the scrutinee, and two branches: the zero case and the successor case.
    /// `rec : forall T, Nat -> T -> (Nat -> T -> T) -> T`
    ///
    /// If the scrutinee is `zero`, reduces to the zero case.
    /// If the scrutinee is `succ(n)`, reduces to the successor case applied to `n` and the "induction hypothesis" `rec n if_zero if_succ`.
    Rec {
        scrutinee: Box<Term>,
        if_zero: Box<Term>,
        if_succ: Box<Term>,
    },
}

The adjustments to FV and substitution are as follows

-equivalence is adjusted in the straight-forward way as there are no variable binding sites:

Reduction

Extending -reduction for the natural number fragment is also straight-forward. We add a rule for reducing the inner subterm of .

Next, we add rules to reduce a rec-term where the scrutinee is zero or a successor of some term. Let’s start by looking at the type of the recursor in the implementation presented in part 1.

//    any type  scrutinee zero case   successor case     output
//    |         |         |           |                  |
rec : forall T, Nat ->    T        -> (Nat -> T -> T) -> T
//                                      |     |
//                                      |     result from recursive call with p
//                                      predecessor p of the scrutinee

The zero case is straight-forward:

The successor case is more interesting. When the scrutinee is a successor of some term (for predecessor), we can create the term that calls the recursor for , which is . This term represents the “recursive call” to the function to get the previous result (also called the induction hypothesis or ih for short).

As is a function that takes a natural number, we give it the predecessor and the induction hypothesis as arguments. So its -reduction rule is the following rule that has no premises.

Finally, we want -reduction to reduce all subterms, so we add a rule for every subterm of rec