Preample

Haven’t updated this blog in a reeeally long time, not that anybody is reading it. I was making a game, but then due to copyright reasons I had to stop. Isn’t it funny how people say they’re gonna do something and then proceed to not do it? Anyway since nobody is expecting anything from us, it’s not that hard to raise the bar.

Introduction

Rea Code: https://github.com/lackhoa/rea-engine

I spent more than half a year building a theorem prover using C++, and that was about it really. Probably you don’t know what a theorem prover is, which is fine since I’m gonna tell you in this post.

The problem

So in mathematics we want to prove things, like this: “for any integer a, b and c, a+b+c = c+a+b”. This desire is epitomized in Euclid. There are many ways to write the proof of “for any integer a, b and c, a+b+c = c+a+b”, one of which is like this.

(a+b)+c
= (b+a)+c   (due to commutativity of addition)
= c+(b+a)   (due to commutativity of addition)
= (c+b)+a   (due to associativity of addition)
Qed!

Well that was long-winded, can we do a shorter proof?

a+b+c = c+a+b
Qed!

Better! (But is it really “legal”?)

So the problems I wanted to solve are these:

we want to encode proofs precisely (ie as data that can be read by a computer program).
we want the program that can read proofs (while also rejecting invalid ones).
we want a convenient way for humans to provide proofs to computers.

The hardest problem that motivated me is illustrated by this: suppose you wanna prove “a+b+c+d+e = a+b+e+d+c”. The “textbook” argument style is no longer practical for this case

(((a+b)+c)+d)+e
= ((a+b)+c)+(d+e) (due to associativity of addition)
= (a+b)+(c+(d+e)) (due to associativity of addition)
= (a+b)+(c+(e+d)) (due to commutativity of addition)
= (a+b)+((e+d)+c) (due to commutativity of addition)
= ((a+b)+(e+d))+c (due to associativity of addition)
= (((a+b)+e)+d)+c (due to associativity of addition)
Qed!

Luckily, I can write that down but you’d have a hard time figuring out what to do without experience (don’t believe me? Please try to recreate the above proof yourself). Meanwhile, any elementary school student would be able to write this

a+b+c+d+e = a+b+e+d+c (explanation: swapped e and c)
Qed!

It’s reasonable to require that our computer system accepts “short” proofs like above. When I first thought of this problem, I thought “Wow, I don’t see a way for computers to follow that kind of reasoning”. But actually there is a way, which will unfold as we proceed through the series.

The drive: Why would you wanna solve this problem?

Now that’s a hard question to answer.

If you have a bit of interest of mathematics, then there is an easy answer. The answer is that I wanted to get to the “post-rigorous” stage of my mathematical education. You can read more about the stages from Terry Tao’s blog, but basically I want to understand exactly what a mathematical proof is. What better way to understand something than to program it?

But let’s zoom out a bit and address the readers who don’t care much about mathematical proofs to begin with. Well I don’t think most people should obsess over proofs (even engineers who use a lot of maths every single day). I’d say in my case, the drive is a bit primal. When I watch a movie, I want every character to behave according to their personality, situation as well as background. Every event should be a logical continuation of the previous events. Of course there can be some slack for creative freedom, but obviously most people wouldn’t want to see a movie where literally anything can happen: everyone does whatever they want and the protagonist can just win whenever he feels like it. What’s the fun in that?

It should be noted that this problem has been solved before. I personally learned a lot from the Coq theorem prover. You might ask “Why would you roll your own then?”, there are two issues:

I don’t understand how it works
Theorem provers are created based on a lot of underlying logical framework. The problem with frameworks is that there are a lot of ways to construct a framework, and I’m not willing to adopt any of them without prior exploration.

Hence I created my own original theorem prover, called “Rea” (short for “reasoning”).

Why should you read this series?

Was Rea good? Well it depends on what you mean by “good”, I was able to use it just fine. However, I don’t develop or even use it anymore, because it stopped being helpful. I found that once you’ve gotten to the third stage, you don’t ever wanna go back down.

I’m writing about the project right now because I wanna get back into writing. Sharing is fun, and hopefully I can provide useful information about math, programming languages, as well as programming in general. I don’t assume any prior knowledge beyond middle school math, but you’ll need to know some programming.

A little orientation before we get into the weeds

So we have the problem, next is figuring out what to do. We want to build a language to communicate with the computer. I will show you that this language isn’t much different from typed programming languages like C or Java (at least with our approach).

Suppose we have this mathematical statement

forany x: int, x+0 = x

it’s read like this: “for any integer x, x+0 = x”.

Say we wanna prove the above statement using these facts

forany x:   int, 0+x = x
forany x,y: int, x+y = y+x

It’s not hard to see this chain of informal reasoning as the proof

x+0 = 0+x = x

Please don’t be concerned about how to convert this reasoning into a precise proof just yet. Suppose our computer already has this proof, the question is what does it mean? Well, it means that we can prove, say, 5+0=5. And the specific proof would be this

5+0 = 0+5 = 0

You can clearly see that this is just the original general proof, but with “5” substituted for “x”.

All that sounded trivial, right? I mean you already knew that, right? Quite the contrary, I claim that most people (including my past self) don’t know this. The reason boils down to a modern indoctrination they taught you in school, namely “set theory”. If you believe in set theory, you’d make a statement like this

forall x: int, x+0 = x

It’s the exact statement, only replacing “forany” with “forall” (read “for all”). This, however, is a massive leap of logic. Suppose now I tell you to prove 5+0=5, you’d say

we've already proven x+0=x for all the integers that you can substitute for x, therefore 5+0=5.

Furhtermore, we also have 6+0=6, 69+0=69, and 100^100 + 0=100^100, etc. I say that is a bad way to think. We can’t even imagine all the intergers, much less claim anything about them.

Really, try imagining all the integers, call me back when you’re done.

The magical object that is the set of all integers doesn’t exist in our universe, so we don’t wanna have anything to do with them (because I don’t know about you, but I don’t wanna study magic). To us, a general proof is just a means to obtain more specific proofs. Specific proofs have to be obtained from computation, using the method described by the general proof.

Note that this is NOT a philosophical debate, if you think in terms of set theory, you won’t understand what we’re doing in this theorem prover.

With that in mind, now we’ve got all the ingredients needed to convince ourselves that we need a typed programming language. Let me reiterate those once again in a more succint manner:

Call “P” a proof of the statemnet “forany x: int, x+0 = x”.
Then, “P(5)” is a proof of “5+0 = 0”

If you write it like that, it’s plain to see that the proof “P” is actually a function (in the sense of programming language). This function takes an integer “x”, and returns a proof that “x+0 = x”. Any proof of “forany x: int, x+0 = x” had better be a function that does the same thing. Furthermore, “forany x: int, x+0 = x” is the function signature of “P”.

So there you have it! Now we just need to create a typed programming language, then we can state mathematical proofs as functions. We know that the proof is valid when the type checker approves of the program (in other words, the program doesn’t have any “compiler error”, not that we’re compiling anything).

Neat, isn’t it? This idea is called the Curry-Howard correspondence. I probably learned about it from this talk by Philip Wadler.

Now that the framework has been established, we’ll talk about specific details of the language in the next post.

Debug builds are slow, so let's make them even slower

Rea: a theorem prover written in C++ (Part 2: Lexing and Parsing)