Simple and Inductive Types

Big Integer Optimization

Learning Objectives

You know how natural numbers can be implemented more efficiently with big integers.

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 .

Efficient External Natural Numbers

0 / 90 points

In this assignment, you will implement an efficient representation for natural numbers using the num_bigint Rust library. Implement type inference and call-by-value reduction according to the mathematical description.

Hints:

To implement the Sub rule, have a look at BigUint::checked_sub

It’s more convenient to combine all the subterm reduction rules into one method. The following code demonstrates how to reduce the left subterm for arithmetic and comparison operators

pub fn arith_cmp1(&self) -> Option<Term> {
    match self {
        Add(t1, t2) => Some(Add(Box::new(t1.step_cbv()?), t2.clone())),
        Mul(t1, t2) => Some(Mul(Box::new(t1.step_cbv()?), t2.clone())),
        Pow(t1, t2) => Some(Pow(Box::new(t1.step_cbv()?), t2.clone())),
        Sub(t1, t2) => Some(Sub(Box::new(t1.step_cbv()?), t2.clone())),
        Div(t1, t2) => Some(Div(Box::new(t1.step_cbv()?), t2.clone())),
        Le(t1, t2) => Some(Le(Box::new(t1.step_cbv()?), t2.clone())),
        Eq(t1, t2) => Some(Eq(Box::new(t1.step_cbv()?), t2.clone())),
        _ => None,
    }
}

Implement Example Terms

Implement the following terms as top-level functions:

Function	Type	Description
`fact`	`Nat → Nat`	Factorial function
`not`	`Bool → Bool`	Boolean negation function
`gt`	`Nat → Nat → Bool`	Greater than function
`pow`	`Nat → Nat → Nat`	Power function

Grading

Only infer_type is tested, the individual typing rules are not.
Only step_cbv and multistep_cbv are tested, the individual reduction rules are not.
The example terms are tested for both correct typing and correct behavior. The behavior is tested only via multistep_cbv. The terms can be defined in various different, but correct ways.

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.

← The Natural Numbers Type

Pairs and The Product Type →