Intro to Proofs-as-Programs

Foreword

This post is meant as a very basic introduction to the notion of Proofs-as-Programs. Like many fields, herein lie simple concepts that are obscured by notation and vocabulary, so I try to point out synonyms where possible to avoid future confusion. Agda is used to explain these concepts as realized in an actual programming language.

Proofs-as-Programs

Proofs are a formal topic requiring a lot of background knowledge and experience in math and logic. Due to this, many programmers get turned off when the word proof is uttered. As it turns out, an elegant analogy exists called the Curry-Howard Isomorphism. The basic idea is that values are to types as proofs are to formulae. With this stunningly simple correspondence, it is possible to reuse years of programmer experience in typed languages and get those programmers on the path to theorem proving. What follows explains a different way to think about programming, from the eyes of a theorem prover. However, take notice that only basic standard programming concepts are utilized!

Getting Started

Programming is done in a logical system, therefore almost no functions or types exist at the onset. Proofs rely on incrementally building up knowledge from previous knowledge, therefore we must define all types and functions used ourselves in the language we are using (of course, source code for common types and functions can come as part of the language in its standard library). The canonical domain we will be using is that of natural numbers (integers from zero to infinity).

Defining Types

data Nat : Set where

We start with the code above by creating a new type called Nat representing the type of natural numbers. Nat is assigned a new unique value of type Set. If you think about it, a type is a set whose elements are values of said type. Because of this, Agda uses Set as the base type from which other types are born.

Defining Values For Types

data Nat : Set where
  zero : Nat

Just as we created a new value of Set called Nat, we now create a new value of Nat called zero. In other words, zero is a value whose type is Nat. For all intents and purposes, you can think of this zero as an atom in other programming languages. For now we will use this partial definition of the natural numbers set, consisting only of zero.

Value Judgments

A judgment/assertion is a value/type pair, which asserts that the value is of its pairs type. It is the compiler’s job to check if the value/type assertion is correct. If we adopt the mindset of proofs-as-programs, then a type is some formula that we wish to derive with some proof in the form of a value.

natsExist : Nat
natsExist = {!!}

Here we would like to prove the existence of natural numbers. We represent this as a variable with a type of Nat that we must assign to some unknown. In other words, the goal is to prove the existence of Nat by assigning a value that matches the type of Nat. Agda uses {!!} as notation for a thus far unproven goal that you may use a placeholder when constructing your proofs.

natsExist : Nat
natsExist = zero

With the completion of our goal, we now have a judgment. In order to see if a proof “checks”, the compiler makes use of what are called inference rules. An inference rule can have 0 or more premises/pre-conditions that must be met to imply/prove/derive some conclusion. In our case the zero : Nat judgment is derived by the zero : Nat data type that we defined earlier, which acts as an inference rule with 0 premises. When this happens the compiler determines that our proof “checked” and natsExist is assigned to a trusted proof of Nat. In effect, it has itself become a new inference rule.

Teatime

Take a moment to pause and reflect on the fact that we are merely discussing simple static type checking. Nevertheless, thinking of these things from the point of view of a theorem prover is a fun and enlightening exercise. However, this isn’t just fun and games, as the simple analogy will let you make powerful claims once you learn more. Another insight to ponder is that the relationship between proofs and formulae is many-to-one. This is an important observation because it means that there are many ways to prove the same thing, making your chances of finding just 1 proof (that’s all you need) greater.

Function Judgments

Proving a value judgment was pretty easy, so let’s try proving a function judgment. For this we will attempt to create a judgment add representing the addition of 2 natural numbers.

add : Nat -> Nat -> Nat
add = {!!}

As before, we start off with a type declaration and a goal. The type of add indicates that it is a function which accepts a Nat, which returns a function that again accepts a Nat, which finally returns another Nat. Before we go on, realize that the ultimate intent of this judgment is to prove the existence of Nat (the same goal as the previous value judgment!)

add : Nat -> Nat -> Nat
add = \(x : Nat) -> {!!}

After compiling, we are assured that the first premise has been proved via an anonymous function that accepts a Nat as an argument. In order for this typed lambda judgment to be proved by the compiler, several built-in inference rules are used that correspond to the typed lambda calculus (although it’s not necessary to understand these in detail, as the rules are intuitive… no pun intended =).

add : Nat -> Nat -> Nat
add = \(x : Nat) -> \(y : Nat) -> {!!}

Once again, the second typed lambda judgment we presented is verified by the compiler. Take a second to think about what this function has verified so far. One may jump to a conclusion and think that we already proved Nat in the first argument, so why even prove it in the second argument and result? However, even at this step we haven’t proved Nat. Arguments in functions correspond to premises in induction rules (see the next paragraph).

add : Nat -> Nat -> Nat
add = \(x : Nat) -> \(y : Nat) -> natsExist

Here we finally prove the conclusion (the return value), and we get to do it with the natsExist proof we wrote earlier (zero would have worked just as well)! But, realize that what we’ve really done is created a new inference rule with 2 premises. Therefore, our proof of the conclusion is not valid unless 2 proofs for each premise are supplied. In this simplistic case all 3 judgments prove the same formula. Thus getting access to the return value proof is not particularly appealing as you already have at least 1 proof of the same formula supplied as the first argument of the function (recount that proofs to formulae are many-to-one).

A Step Back

The power of proofs-as-programs is that you can encode more powerful constraints of functions and values into their types. The canonical example is (using dependent types, a subject of a future post) a sorted list insertion function that guarantees that the returned list remains sorted (along with other properties you may want to ensure such as the size being preserved, elements being preserved, etc). That said, addition is simple enough that we merely want to use its return value for computation rather than for a proof of Nat. The good thing is that you can decide where the boundaries lie between simple functions and types, and complicated functions that require type-based constraints (e.g. remaining DRY through the use of various complex combinators, but ensuring the function does what you want in its type.

Completing Nat

So far we’ve worked with Nat as an incomplete set (it only contains zero), so let’s fill the rest in.

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

The rest of Nat is achieved via an inductive type definition, yielding an inductive type. The similarity to mathematical induction should make sense to anyone with a CS background, but basically you can think of it like a recursive definition. So, succ accepts another Nat which may be zero or another nested succ, e.g. succ (succ (succ zero)) representing the natural number 3. The addition function we defined earlier still works because we chose a general type, but let’s make it return what we intended. Before we do that, we will first rewrite the function to use a syntax sugared version that performs pattern matching on the lambda arguments.

add : Nat -> Nat -> Nat
add x y = natsExist

Coverage Checking

add : Nat -> Nat -> Nat
add x zero = {!!}

If you attempt to compile the above you get an error, but why? When we defined Nat with the data directive, we once and for all defined all possible values. Agda requires functions to be coverage complete with respect to type values! Now that we switched to pattern matching on the specific value zero, Nat coverage checking fails and the compiler tells us to also define the function for the succ case.

add : Nat -> Nat -> Nat
add x zero = {!!}
add x (succ y) = {!!}

With coverage checking you are not only assured of compile-time type safety (only Nats), but also that functions are defined for all possible values of a type (you can still encode type-level restrictions as long as all cases are accounted for, but that is again a subject of another post).

Completing add

The actual function implementation isn’t the purpose of the post, so I’ll quickly list it here.

add : Nat -> Nat -> Nat
add x zero = x
add x (succ y) = succ (add x y)

Axioms

You may have noticed something fishy about the data type definitions. In particular, the definition for zero is similar to natsExist, but there is one key difference. Namely, zero does not provide a proof/value of its formula/type. Defining something this way creates an axiom/postulate. Using data actually creates a restricted postulate that does not allow types like Nat to have additional values defined in them later (if this were allowed, any coverage-based reasoning would no longer be true). Additionally, the property of coverage is enforced in future functions (with respect to the values of the newly defined type) when you use data.

Q.E.D.

I hope you enjoyed this post, as that’s it for now. Once again, the example code produced is trivial but necessarily so to explain the concepts. Proofs-as-programs starts to be a very powerful concept with the introduction of Dependent types… be patient as that post will come later =)

Bonus: Syntax Sugar

Agda also let’s us write prettier code with unicode and mixfix operators. I left this out until now to avoid cluttering the explanation of more important concepts.

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
x + zero = x
x + succ y = succ (x + y)

succ2 : ℕ → ℕ
succ2 = λ x → x + (succ (succ zero))

larrλtheliquid -> Lemma the Ultimate