Theory of Lambda Calculi

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.

Loading Exercise...

Loading Exercise...

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.

Loading Exercise...

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

Let’s look at how to define the predecessor function first. It’s straight-forward and uses the fact that recursor provides the predecessor of in the successor case

Now, we can express the addition and multiplication functions as follows

Loading Exercise...

Loading Exercise...

Loading Exercise...

Now that the set of booleans is disjoint from the set of natural numbers, which was not the case with Church encoded terms ( is the same as false), we can decide whether to decode the result as a boolean or a natural number based on its shape.

Now that we have built the backend for the language, let’s add a nice frontend with a parser and syntax sugar. We will also refactor the code into modules as we are approaching 1000 lines of code.

Loading Exercise...

Loading Exercise...

Loading Exercise...

General Recursion

We are going to take a peek at the world of recursion with infinities. The examples here should work in the provided REPL. As a note: if the REPL gets stuck, press Ctrl-C to stop.

Note: step should attempt the AppAbs, Ite and Rec rules before every other rule.

The fixed-point or Y combinator in lambda calculus is the following term

We can use it to implement general recursion, which enables us to write functions that are not primitive recursive¹.

The fixed-point combinator doesn’t have a normal form, as it infinitely expands by composing with itself

Start by typing the following declaration into the REPL. It should get stuck because it tries to normalize the term, so press Ctrl-C right after pressing enter.

Y = g => (x => g (x x)) (x => g (x x))

The Y declaration was saved as a global (which you can list with :env), so we can try to define the factorial function using it:

Y (fact => n => if n == 0 then 1 else fact (n - 1) * n) 4

Likewise we could define the ordinal as follows:

omega = Y succ

Now, try evaluating the following term

0 * omega

It should not get stuck if the main rule of recursor is applied before Rec1, Rec2 or Rec3.

Loading Exercise...

Loading Exercise...

Footnotes

Footnotes

1. See Wikipedia: Primitive recursive function. The Ackermann function is a well-known example of a non-primitive recursive function which nevertheless is total and computable. ↩ ↩²