Calculation and Proof

The essence of this chapter is to cover how programs are evaluated, and how that relates to calculation in mathematics. We also define a function more rigorously and finally discuss program correctness from a functional point-of-view.

Functions, Sets and Defining Equations

A function maps elements from its domain to elements in its codomain . The image of a function is the set of all outputs it actually produces — a subset of the codomain. Given a subset , we write to mean the image of under , i.e. in set-builder notation.

Let’s consider the following function from integers to integers

f : Int -> Int
f = fun x : Int, 2 * x

We can look at the image of the function acting on any subset of the domain. For example

The defining equation of the function is for all .

f : Int -> Int
f = fun x : Int, 2 * (x - x)

The above function takes each integer to . By calculating, we can see that , and so on, but we can even prove that for all . To do this we can employ simplification.

Simplification

Simplification is a mathematical process most people learn early in their education. More precisely, simplification is the process of transforming a term into an equivalent term using a set of simplification rules. The terms are equal if they evaluate to the same value.

For example, in a context where , we can simplify into . Because of referential transparency, this means that everywhere where we can “replace” by without affecting the behavior of the code.

Using this simplification rule, we can rewrite the defining equation of as follows

If the simplification rules are correct, this proves that for all .

f : Int -> Int
f = fun x : Int, x * x / x

let mut delay: u32 = 0xffffff;
while delay > 0 {
    delay -=  1
}

The next chapter goes into more detail on simplification.

Calculation

Simplification is not the only way to reduce a term to another equal term. When all variables are realized to concrete values, we can just calculate the result. The process of calculating a resulting value from a term is quite simple and fundamentally recursive: we look at every subterm and calculate their value.

For example, the subterms of 2 * (5 + 1) are 2 and 5 + 1. We first calculate the value of 2 which, because it’s an atomic term, is . However, 5 + 1 is not atomic, so we proceed recursively, calculating the value of its subterms and adding them to get . The result of the calculation is therefore .

Reminder: atomic terms are characterized by not consisting of subterms. For example, variable names and other literals are atomic terms.

Calculation, like simplification, creates a chain of equal terms: 2 * (5 + 1) = 2 * 6 = 12. The terms are equal because they have the same value.

Clearly the process of calculating went from left to right, so the rightmost term¹ should be the atomic term whose value is what we are looking for. Therefore we can even say that calculating a term results in another term — which is akin to simplification. This realization lifts the concept of a value to the term level, and is done in lambda calculus to make calculation purely syntactic: the underlying meaning of terms like 2 and 5 + 1 is almost made invisible. Of course the underlying values are still present in defining the operators such as + and *.

Arithmetic is not the heart of functional programming — rather functions and function applications are. Next, let’s look at how calculating with functions works in the spirit of lambda calculus.

Calculating with Functions

Let’s look at a simple function add1.

To understand how we get add1 5 = 6, we need to understand how to calculate with functions. As we are in the realm of programming, we prefer to use the word evaluate instead of calculate, although they effectively mean the same thing.

From the defining equation of add1 we get add1 5 = (fun x : Int, x + 1) 5. Now we have an application of two terms. As with arithmetic operators, we recursively evaluate the values of both sides — but this immediately leads to the following question: what is the value of a function?

The standard answer in lambda calculus and functional programming is: every function is a value²!

Now we are in a similar situation as when evaluating 1 + 5: both subterms are values. The next step is to perform syntactic substitution: we substitute the function’s parameter by the right-hand-side value in the function’s body.

Skipping some details regarding substitution, we observe that substituting x by 5 in x + 1 results in 5 + 1. Therefore

Let’s frame this cornerstone of functional programming in a definition.

Notice that the definition says nothing about the types involved. This is because type checking is a pre-condition to evaluation — i.e. the code must type check before it’s run. Therefore we can (and do) assume that the types match, i.e. is a function type and is in the domain of .

In untyped programming languages, including the untyped lambda calculus, there is no type checker, but pretty much the same definition for function applications is still used.

Next, let’s look at a function called twice : (Int -> Int) -> Int -> Int. Looking at its signature, it takes an integer function as input and returns an integer function as output (remember that -> associates to the right).

Applying twice to the add1 function creates a function which adds 2 to the argument.

We want to evaluate the value of main, so we start with its definition: twice add1 10. Function application associates left, so we first evaluate twice add1:

The second equality comes from the definition of function application: add1, a value, is substituted in place of f. We don’t unfold the definition of add1 to keep the calculation cleaner.

As fun x : Int, add1 (add1 x) is a function, it’s a value, and therefore we are ready to evaluate the outer application.

Here, the second equality comes from the function application and the third comes from calculating the subterm add1 10 which we have skipped for brevity.

In lambda calculus, each of the above equals signs is called a -reduction, and its rules will be covered in detail later on this course.

Predicates and Relations

Let’s establish some mathematical notions and vocabulary that helps us reason about programs. These concepts are very important and used throughout the course.

As shown in the previous chapter, we can write predicates on a type by writing functions from to booleans.

Here are some examples of predicates:

• is a predicate on integers, and defined as follows: .
• is a predicate on integers, and can be defined recursively (as shown next), or by using the remainder operator: .
• is a predicate on lists, and defined as follows: is true if and only if .

In , predicates are written as functions returning Bool:

positive : Int -> Bool
positive = fun n : Int, n > 0

even : Int -> Bool
even = fun n : Int, let n = int.abs n in
    if n == 0 then true else ! (even (n - 1))

empty : [Int] -> Bool
empty = fun xs : [Int], lcase xs of
    | nil => true
    | cons _ _ => false

A similar concept, where instead of one variable we have two, is a relation.

Here are some familiar relations.

• Let be a set. Equality () is a relation on : is true (i.e. ), but is not
• Less than () is a relation on : holds, but does not
• Set membership () is a relation between elements³ and sets: holds

To express relations in code, we write them with a function of type .

lt : Int -> Int -> Bool
lt = fun x : Int, fun y : Int, x < y

contains : Int -> [Int] -> Bool
contains = fun x : Int, fun xs : [Int], lcase xs of
    | nil => false
    | cons y xs => if x == y then true else contains x xs

As contains is a relation, it’s mathematically a set of pairs. For example, the following are true statements about contains:

Sometimes predicates and relations end up mixed together. The convention used on this course is that a predicate is a statement over one free variable, and relation over at least two variables:

• When writing , we can think of as just the predicate .
• A relation can be thought of as a predicate over a pair: , and is mathematically equivalent to a relation.
• Likewise for any triple , we can think of it as a predicate over a triple, which is equivalent to a relation over , and .

Functionality and Totality in Depth

So far we have been talking about both functionality and totality quite informally. Let’s now give the definition of a function, and after that conceptualize those ideas using programming.

A functional relation is also known as a partial function, denoted , as it doesn’t require the following ingredient.