Reading The Little Prover — Chapter 1

This is my first and hopefully not the last post about the book “The Little Prover”. Over the next few weeks, I will write about what I have learned from each chapter.

Why write it down?

Simple, so that I can remember what I’ve learned. I’ve read a lot this year but I can’t say with certainty that I’ve learned a lot from reading them. I think that I can safely say that I’ve learned something only when I’ve managed to articulate my thoughts by writing it down. I find that writing things down helps me to organize the information and it allows me to have confidence to say that I have truly mastered the subject.

Why The Little Prover?

Learning about theorem provers has always been on my mind. I had the chance to take a class that uses it back in NUS but I dropped it two weeks into it. An act that I still regret till this day. The class in NUS teaches logic and formal systems and it uses coq to reinforce the concepts. The module code for the class is CS3234 and it’s still taught by Aquinas Hobor, I believe. Anyway, back to the book.

The book uses J-Bob as its proof assistant. It is a lisp and it’s implemented in both Scheme. Needless to say, you need to know a bit of lisp to understand the examples in the book. However, not a lot of prior Scheme or lisp programming experience is required. You just have to know that lisp uses prefix-notation and its expressions are evaluated inside out. In other words, you evaluate or solve the inner parentheses first, before solving the outer ones. For example, for the expression (+ 1 2 (- 2 3), you first solve for (- 2 3), the subtraction, before solving for the addition in the outer parentheses.

Apart from using an esoteric language like lisp, the book also uses an unique question and answer style to teach concepts. Don’t expect long paragraphs of text and large sections of code in this book. Most of the questions and answers uses less than 50 words. Think of it like you’re overhearing a conversation between two witty professors over breakfast (yes, the book uses breakfast as its examples). As a Confessional Christian, it reminds me of the Catechists, more specifically the Geneva Catechism. Here’s a taste of the way doctrine is taught in the Catechism:

Q1: What is the chief end of human life?

A: To know God by whom men were created.

Q2: What reason have you for saying so?

A: Because he created us and placed us in this world to be glorified in us. And it is indeed right that our life, of which himself is the beginning, should be devoted to his glory.

Q3: What is the highest good of man?

A: The very same thing.

But I digress, and of course, this is not a post on the Christian Catechists. Though, I might write one about it in the future. ;)

Chapter 1 — Old Games, New Rules

The chapter starts off with an introduction to the basic functions in scheme. Namely cons, car, cdr, and atom?.

cons produces a cons cell. It’s typically used to join the head and the tail of a list together.

(cons 'ham '(eggs))
=> '(ham eggs).

A list in lisp is basically a bunch of cons cell joined together by cons . '(ham spam eggs) is equivalent to (cons 'ham (cons 'spam (cons '(eggs))).

car returns the first element of a cons cell.

(car (cons 'ham '(eggs))
=> 'ham

cdr returns the second part of a cons cell. It is typically used to retrieve the list without its first element.

(cdr (cons 'ham '(eggs))
=> '(eggs)

atom? returns 't if the argument is not an empty cons cell. 't is simply the Scheme version of the true value.

(atom? a)
=> 't
(atom? '())
=> 't
(atom? (cons 'ham '(eggs))
=> 'nil

After introducing the basic operations or functions of Scheme, the chapter introduces axioms to define things that are presumed to be true regardless of its arguments. For example, (car (cons a b)) would always return a regardless of the value of a and b. It then introduces dethm to define these axioms.

(defthm atom/cons (x y)
  (equal (atom (cons x y)) 'nil)
(defthm car/cons (x y)
  (equal (car (cons x y)) x)
(defthm equal-same (x)
  (equal (equal x x) 't)
(defthm equal-swap (x y)
  (equal (equal x y) (equal y x)) 

defthm means define theorem. It looks almost like a function definition but it’s used to define expressions can be rewritten. What’s interesting is that the theorems can be used both ways as a result of equal-swap. For example,

(car (cons a b))

is equal to a and apart from that, there are also infinitely different ways to rewrite that expression. For example, it is also equals to

(car (cons
       (car (cons a '(ham)))
       b))

That’s because a can be rewritten into (car (cons a '(ham)) due to equal-swap .

That’s all folks!

That’s it for this chapter.