Daniel P. Friedman has authored or co-authored an alarming number of Computer Science books that Programming Language enthusiasts would consider classics. Among them are a few members of the series of "Little" books, which started in the 70s with "The Little LISPer," and continues 40 years later, with 2015's "The Little Prover," co-authored with Carl Eastlund.
All of the "Little" books follow a similar structure and embrace a similar pedagogy: concepts are taught through a series of questions and answers side by side, presented in "frames" separated by lines. I have studied some of the other books before, particularly "The Reasoned Schemer" (which doesn't have the word "Little" in it but is still a part of the 'series'), but have never really clicked with how the information is presented.
Probably because I had a good reason to feel that I needed to understand what they were presenting, the technique finally worked for me with "The Little Prover." Reading the pages over and over again I got into a rhythm and started to absorb the information. Another thing that was blocking me before was a lack of intuitive understanding of Scheme (pairs and lists everywhere confused me,
cdr irked me). For some reason, that vanished for me too when I started with this book, so yay! It only took me around 8 years to be able to digest Scheme properly. Not too shabby, mrb, not too shabby.
Why was I so compelled to grok this stuff? I committed myself to presenting about Phillip Wadler's "Propositions as Types" at the New York City chapter of Papers We Love, and I wanted to have a concrete, interactive experience to go along with the theory and mechanics I was trying to grasp from the paper. "The Little Prover" coming out around the same time as I was preparing seemed serendipitous - it describes a theorem prover written in Scheme and shows how theorem proving and writing Scheme code can actually be the same thing.
To put a finer point it, I love this book and highly recommend it. It has lots of lessons to teach, which aren't limited to theorem provers. What the authors can do with a 'simple' system written in Scheme is phenomenal and very deep, and importantly, challenging concepts are made fun and easy to access given enough time and patience. I found pieces of some of my favorite aspects of philosophy, math, and Computer Science in the book, and think you can make connections to:
And I'm pretty sure if you're reading this, you like at least some of those things.
I decided to write down some notes and musings from each of the 10 chapters in the book in order to bolster my understanding, provide an artifact of my learning in case anything becomes fuzzy to me later (which it certainly will, given historical evidence), and to prove to myself that I can explain this stuff in the context of Wadler's paper. This post covers the first 5 chapters. For each one, I've written down what the "Big ideas" were for me - what resonated, what I think the authors were after, and what I could take away. Here we go!
Note: There is some Scheme code below that is illustrative, and some that is meant to be executed by the J-Bob proof assistant, the design and implementation of which is one of the central focuses of the book. Understanding which is which is a little bit confusing, but check out The J-Bob Source Code on GitHub for some clues.
The Scheme code
(car (cons 'ham '(eggs))) is equal to to
Each of the following lines of Scheme code are also equal to
The Scheme code
(car (cons 'ham '(eggs))) is equal to the value
'ham. It is not equal to any other value.
What value is the Scheme code
(cons a b) equal to? We don't know what
b are, so we can't know the value of
(cons a b).
atom in Scheme is defined as anything that is not a
pair, and a
pair is something that is produced with
cons. This should give you the idea:
Play around in your friendly Scheme REPL if you feel like testing more expressions. I've certainly spent long enough doing so, I wouldn't want to begrudge you the fun!
So, back to the question "What is the value of
(atom? (cons a b))?"
Even though we don't know what
b are, we know the value of
(atom? (cons a b)) - why?
Because we know the definition of
atom?, which returns
'nil for anything that is the result of a
So the value of
(atom? (cons a b)) is
'nil, regardless of the values of
b. This is cool, and reminds me of static analysis.
Does the expression
(equal? 'flapjack (atom? (cons a b))) have a value?
If we know that
(atom? (cons a b)) is
'nil, does that help us? It does! We can substitute
'nil for any instance of
(atom? (cons a b)) that we come across. That seems useful.
(equal? 'flapjack (atom? (cons a b))) becomes
(equal? 'flapjack 'nil) which is
The big idea here is that:
We can know interesting things about a program without executing it.
The authors are also introducing the idea of a focus within a piece of code that is being transformed/evaluated in this strange new way.
Our attention is drawn to the fact that this transformation happens in discrete steps and rewriting is applied to specific, addressable subexpressions of the term at hand. To follow these steps:
(equal? 'flapjack (atom? (cons a b))), the focus is
(atom? (cons a b)), which we can rewrite to
(equal? 'flapjack 'nil). We know this is equal to
So two steps and two focuses later, we have reduced the original expression to a value without having to know everything about that program, e.g. the values of
We relied on certain known facts in order to execute the above transformation. These facts are called axioms.
"An axiom is a basic assumption that is presumed to be true."
Here are some axioms:
(atom? (cons x y))is always equal to
(car (cons x y))is always equal to
(cdr (cons x y))is always equal to
Stated in code, using the
When axioms are built up to prove things, that's called a theorem:
"A theorem is an expression that is always true."
And to put a finer point on it:
"Axioms are theorems that are assumed to be true, whereas other theorems must be shown to be true."
Here are the steps of rewriting the following expression until it becomes
We notice that
(equal (cons x y) (cons x y)) will always be
't, regardless of what
y are. So, we can replace it with
Likewise, the static values
'(and crumpets) can be collapsed using
'('t and crumpets) will always be
't. So we arrive at:
Without executing the code, we know that it will always evaluate to
The Law of Dethm (initial):
"For any theorem
(dethm name (x1...xn) body-x), the variables
body-xcan be replaced with any corresponding expressions
e1...en. The result,
body-e, can be used to rewrite a focus
(equal? p q)or
(equal? q p)."
e1 -> (car a) e2 -> (cdr b)
body-e -> (equal (car (cons (car a) (cdr b))) (car a))
p -> (car (cons (car a) (cdr b))) q -> (car a)
(atom? (car a))
That's what it looks like to apply the Law of Dethm to some functions. We're also told that J-Bob, an assistant in the form of a computer program, can help us automatically do some of these transformations.
Law of Dethm
(car (cons a b)) in this code equal to?
a, since the
(cons a b) is always
a. This is the result:
We know we can do that because of the axiom of
car/cons. What is the expression above equal to?
The result is
c, regardless of
a. Chapter 2 introduces axions around
if to help us rewrite
if code the same way that we rewrote with
The axioms of If:
(dethm if-false (x y) (equal (if 'nil x y) y))
(dethm if-same (x y) (equal (if x y y) y))
These axioms each represent very simple ideas that turn out to have very powerful implications.
if expression has three parts:
(if Q A E): The Question, the Answer, and the Else.
The axioms of Equal:
The Law of Dethm (final)
(dethm name (x1...xn) body-x):
body-xcan be replaced with any corresponding expressions
body-e, can be used to rewrite a focus as follows:
body-emust contain the conclusion
E, then the focus must be found in an
Ewith the same
Explaining the "Law of Dethm" with the Jabberwocky example:
"Sometimes our intuitions get in the way."
if-nest axioms are amazing:
(dethm if-nest-E (x y z) (if x (equal (if x y z) z) 't))
Reminds me of the first time I realized that statically typing terms of certain dynamic languages was possible. Consider the following snippet:
Think about it long enough and you can see that there are both assumptions that can be made about the types in this function, and also some things you know. An assumption is that
foo is a number. We test it against
3 using the
> operator, which we know operates on numbers.
Something we know for sure is that this function returns a
String. Regardless of the value of
if expression returns a
Start to stack these assumptions up, dream of an interactive tool that can tell you the types of these expressions without having to know them, and throw in a type checker that can assert what you annotate, and you can get a sense of a pathway from dynamic to statically typed programming.
In this chapter we also get
The Axioms of Cons,
(dethm car/cons (x y) (equal (car (cons x y)) x))
(dethm cdr/cons (x y) (equal (cdr (cons x y)) y)
More intuitive but not intuitive facts about list construction in Scheme than you knew were useful. This chapter really nails the fluid, bizarre methods of applying rules and rewriting code that goes into creating mechanized proofs on a computer using a programming language.
Through applying some sensical and some nonsensical techniques, the authors illustrate that like programming, you can gain an intuition for the idioms of theorem proving through repetition and deep understanding. Write and read enough programs and you'll learn how to write programs properly. Write and read enough proofs, it seems, and the same will happen. An interesting perspective on the correspondences that make the ideas in this book possible.
The value of the Scheme code
(pair 'sharp 'cheddar) is
The value of
(first-of (pair 'sharp 'cheddar)) is
The value of
(second-of (pair 'sharp 'cheddar)) is
pair is written like this:
(define (second-of y) (car (cdr x)))
Here's a claim about
"A claim is an as-yet unproven theorem."
We can make a claim into a theorem! By proving it!
"A proof is a sequence of rewriting steps that ends in
't. If we can rewrite a claim, step by step, to
't, then that claim is a theorem."
(pair a b) -> (cons a (cons b '()))
Defun: Given the non-recursive function
(defun name (x1...xn) body),
(name e1...en) = body where
e1,...xn is en.
In other words, for a non-recursive function, you can replace the
function call with the
function definition, substituting the arguments from the definition with those of the function you're proving.
first-of-pair is a theorem, by
Law of Defun,
second-of-pair a theorem?
For the first three chapters, the authors cleverly use colors in the printed text to show the "focus" of an expression as it is being rewritten.
When you are using the J-Bob prover that the book introduces and shows you how to use and implement, you describe these focuses using a query language of sorts describing the "path" to the part of the expression that needs to be rewritten.
This works because all code is a list. "Code as data" in the Lisp tradition has a lot of awesome applications and the authors of this book, one of whom is easily one of the deepest functional programming thinkers of all time, leverage this property to the fullest in this text.
"If we can find a proof one way, we can always find it in another. If the second way goes wrong, we can 'back up' to where we started and do it the first way again. But some approaches will find a proof faster than others."
Let's look at
in-pair?. What does it do?
It determines whether the two-element list
'?. Let's try to prove this claim!
in-first-of-pair a theorem? Yes! By
"Skip irrelevant examples: Rewriting a claim to 't does not have to go in any particular order."
This chapter shows us the mechanics of using code to prove theorems, which are expressed as code. These proofs happen by rewriting code using pre-defined rules to begin with a conjecture and then end with
't, which completes the proof.
sizefunction, and is a neat way to prove totality
We meet a new function -
list0?. Here's how it works:
list0? do? It looks like it tells you if something is an empty list. Here is the definition:
list0? total? What does total mean?
list0?is total means that no matter what value
vis passed to
list0?, the expression
(list0? v)has a value."
In other words a function
f composed of functions
x1...xn and if statements
if1...ifn can be total if all of the outcomes of
if1...ifn produce a value and
x1...xn are all total.
We learn that, somewhat surprisingly, all built in operators are total. When we're trying to determine if a function is total, we know that all functions used in a function must be total for a function to be total. For example:
Is total because
cdr are all total, and the if statements
E produce a value. Now that we know what totality is, we can learn about the final
Law of Defun:
"Given the total function (defun name (x1...xn) body), (name e1...en) = body where x1 is e1, ..., xn is en."
In other words, we can replace a function's use with it's body (once variable substitutions are performed) if the function is total. Why does it matter if it is total? If it isn't, a function can be used to prove a contradiction. Let's take a look.
We go through the process of trying to prove
list3?, etc. as total. There must be an easier way, and it sounds like a job for recursion. Can we use recursion like that? What would that look like? How about like this:
list? function produces
't if its argument is a list, otherwise it produces
'nil. So, is
It looks like in order to know if
list? is total, we need to know if
list? is total, because the function is recursive. So what can we know about how
list? is called from within
We see that
list? is always called with
(cdr x) as its argument. That means that by definition, calls to
list? from within
list? always have fewer
conses than the function started with.
The way that we use this fact to prove that
list? is total is with a mechanism known as the
measure of a function.
"The measure is an expression that is included with a function definition. It may only refer to previously defined, total functions and to the function definition's formal arguments. The measure must produce a natural number that decreases for every recursive call to the function."
So if we definte
list? with a measure, J-Bob will know how to measure whether or not recursive calls to a function will actually cause the function to terminate and produce a value.
measure: (size x)
size function measures the size of a function's measure. Counting
cons cells, for example:
The way that we make the totality claim for
list? using a measure is by expressing "If x is not an atom, than
(size x (cdr x)) must be smaller than
We are introduced to some
Axioms of Size which give us certain truths upon which we can rest the burden of our totality claims! Handy.
(dethm size/car (x) (if (atom x) 't (equal (< (size (car x)) (size x)) 't)))
(dethm size/cdr (x) (if (atom x) 't (equal (< (size (cdr x)) (size x)) 't)))
So using these rules and the rules we've seen before, we can indeed reduce the totality claim above to
't. Here's how it looks using J-Bob:
The totality claim for
partial is as follows:
Which can be reduced to:
Which can't go any further - certainly
(< (size x) (size x)) could never be true or reconciled within a consistent system. That's why
partial is partial, and why totality matters - because partial functions can introduce inconsistencies into our system.
We start out looking at
memb?, a function which looks for
'? in a list, and
remb, which removes the first instance of
'? from a list. Are they total? Let's look at
memb? with a measure:
measure: (size xs)
You can determine if
memb? is total by proving its totality claim:
It is total, and so is
remb, so we should be able to build theorems out of these functions. Which is exactly what we do next, with
memb?/remb0, which states that
'? from a 0-element list. Here's the
We can try to prove this using the axioms we've learned so far. The bit to focus on is:
The first thing we should do is use the definition of
remb, which we know to be total. We'll replace the
xs in the definition of
What can be simplified from this? Quite a bit, it turns out. This expression becomes:
'() is an atom. Now, let's use
memb?, again replacing
Again we see the expression
atom '(), which we know is true. So the above becomes:
And we know that
memb?/remb0 is indeed a theoreom, by
equal-same. Here's how the above explanation looks when it's written in J-Bob:
This is an executable program that will prove that this function is a theorem - cool!
The authors take us through a similar procedure to prove successive functions on top of
memb?/remb2, etc. They lead up to the question that would occur to anyone paying attention to the book up until this point - couldn't this be generalized? What techniques can we use to perform recursion like proofs? The answer is induction, and it is the big idea for the second half of the book.
While we're shown how proving the successive functions to
memb?/remb0 isn't exactly as straightforward as you'd think, we're given some nice insights into how to effectively write proofs with our system:
Rewrite from the Inside Out
Start with the statements "inside" the code, the things that are nested and squirreled away. Simplify them and then the entire proof will become simpler
We're shown this technique which really resonated with me as a programmer, because again it reminds me of the kinds of insights you form about programs in a certainly language after writing with it for a decent amount of time. Most experienced programmers will be able to recognize certain simplifications that can be made to code that will preserve its meaning but make its intent clearer, improve performance, etc. Similarly, we're given techniques that simplify proofs without changing their meaning. Pretty sweet.
Pull Ifs Outward
This is a piece of wisdom based on the mechanic provided above - that is, use if lifting! It can simplify what you're trying to prove radically.
Keep Theorems in Mind
Another piece of advice from the authors which I can't help but draw a parallel to software engineering about. Keeping theorems in mind is about recognizing the patterns in your code that can be simplified using axioms, but also about recognizing when you're close to a pattern. When you're close to a pattern, make some minor changes around your statements, and you might reveal that pattern. This reminds me a lot of the ways that software developers apply patterns, and look for "smells" or clues that they might be doing something wrong, or every once in a while, something right.