Simple and Inductive Types

Big Integer Optimization

---

Introduction

The Peano-style natural number implementation is horrendously inefficient — it’s practically using long linked lists for basic arithmetic. In this chapter we optimize this by extending STLC directly with big integers instead.

When evaluating a term whose type is Nat, we get the term’s canonical form. The set of canonical forms, or values, of natural numbers is

The set is really an encoding (embedding) of the set in to the language of STLC with natural numbers. Our goal is to redefine the semantics to directly work with natural numbers, and provide an efficient “runtime representation” for it.

In the implementation we use a big integer type from the num_bigint library instead of a machine integer u64 to keep the language type safe. If we used u64, then our implementation would not be a faithful representation of the dynamics because e.g. overflowing addition causes a panic (or wraps around).

First, let’s extend STLC (with booleans) with the terms for “big unsigned integers” or “external natural numbers”, and also add basic arithmetic and comparison operators which are provided by the library.

In Rust, the Term enum would have the following new constructors

Uint(BigUint),
RecNat {
    scrutinee: Box<Term>,
    if_zero: Box<Term>,
    if_succ: Box<Term>,
},
Add(Box<Term>, Box<Term>),
Mul(Box<Term>, Box<Term>),
Pow(Box<Term>, Box<Term>),
Sub(Box<Term>, Box<Term>),
Div(Box<Term>, Box<Term>),
Le(Box<Term>, Box<Term>),
Eq(Box<Term>, Box<Term>),

Type Checking

Type checking the natural number terms is straight-forward. Any term has type Nat.

The arithmetic and comparison operators are typed as follows

The typing rule for RecNat remains the same.

CBV-Reduction

The call-by-value reduction rules for arithmetic and comparison operators reduce subterms. To keep the rules deterministic, the left subterm is reduced until it’s a value, only then can the right subterm reduce.

The rules for the other operators are similar. Notably underflowing subtraction saturates at zero and division returns the integer quotient.

The RecNat rules require some changes now that we don’t have and terms anymore. Notably the RecNatS rule has the assumption that is the predecessor of , i.e. , where .

Loading Exercise...

Integers

It would be easy to extend the language with also an integer type () using the signed BigInt type from the num_bigint library. Doing this is a good exercise, but instead of doing that, we continue straight into the next topic which is pairs and the product type.