Note: this whole document is literate code generated by a workflow I'll talk a bit more about tomorrow. It's a short shell script that's quite useful. You can find the program as a gist on
github.
So we’ll first take as an axiom that math is based on axioms. So far so good? Well, an important thing to note with this is that it’s really easy for axioms to have different significance - it all comes down to what metaphor you use in your brain to describe the axiomset
For example,
MIU seems wholly abstract, but it turned out to be isomorphic to some operations on the integers modulo 3. And that isomorphism allowed some things to be made clear about it that weren’t otherwise.
In Chapter 2, Hofstadter defines some axioms that he calls the “PQ system”. These axioms are:
-
The only valid characters are -, P, and Q
-
-P-Q-- is a theorem
-
∀x. xP -Q -x is a theorem
-
∀xyz. if xP yQ z is a theorem, then xP -yQ -z is a theorem
First lets define our types Hyphen strings are essentially equivalent to natural numbers, so we’ll make that explicit
> data Nat = Zero | S Nat deriving (Show, Read)
> data Str = PQ Nat Nat Nat deriving (Show, Read)
Next we’ll define a few numbers for convenience
> one = S Zero
> two = S one
And this is all we really need Now let’s define the basic axiomset
> a1 = PQ one one two
> a2 (PQ a1 a2 s) = PQ (S a1) a2 (S s)
> a3 (PQ a1 a2 s) = PQ a1 (S a2) (S s)
Now we generate a list of all the theorems by iterating a2 starting from a1, and then mapping and iterating a3 over that list. Isn't it wonderful what you can do with lazy evaluation?
> theorems = map (iterate a3) $ iterate a2 a1
Now this is great if we just want the list of all axioms, but not really that useful if we want to check if something’s in there. You know, given the infinite axiom space and all. So right now checking for theoremhood is actually really computationally difficult - you have to produce all axioms and just check if something’s in there. Now, there are some strings where it’s obvious that it’s not a theorem - P-Q-PPP is malformed, like 3$&*(! So, how would we go about making a deterministic test that finishes in finite time?
This is your cue to try and solve the problem yourself before spoilers.
So, to review:
-
We’ve got an infinite list of theorems, generated by some recursive rules
-
Our job is to somehow figure out if any given (valid) string is going to be somewhere in that list
-
There are two recursive rules doing the generating, so we can’t even do a linear scan through the infinite set
-
And, most algorithms to do diagonal scans are annoyingly complicated for what should be a simple test
-
Neither of those “full scan” approaches can ever give us certainty that something is a nontheorem - just that we haven’t found it yet
Well, the simplest way is to exploit an isomorphism between PQ and arithmetic. You can see this if you interpret
xP
yQ
z as
"\(x + y = z\)". Hofstadter tried to make it clear with the suggestive names P and Q. I tried to make the hint stronger, by defining PQ in terms of natural numbers. But, to do a good theoremhood check, we first need to actually write out the code for natural number arithmetic
Just for kicks, lets actually implement the
Peano Axioms, or at least the ones we need.
First, let’s define equality
> instance Eq Nat where
First, m = n iff S(m) = S(n) (Peano Axiom 8) An equivalent to the above is that S(m) = S(n) iff m = n
> (S n1) == (S n2) = n1 == n2
Equality is reflexive (Peano Axiom 1)
> Zero == Zero = True
Now that we’ve defined both our truth patterns, we can rest assured that every other case will turn out false
> _ == _ = False
Next we’ll define all the arithmetic required by the Num typeclass
> instance Num Nat where
Zero is the additive identity, and this definition of addition actually looks about the same as Peano Addition If we’re adding Zero, then we can just return the other number And, S(n) + a = S(n + a). The pattern match to S(n1) + S(n2) is just a way of increasing the speed at which the recursion terminates
> (S n1) + (S n2) = S . S $ n1 + n2
> n + Zero = n
> Zero + n = n
Next we’ve got multiplication, if only because it’s required by the typeclass. It’s just repeated addition, so this is pretty simple. The first rule is that anything multiplied by Zero is Zero. The second rule is that for any n1*S(n2) = n1 + n1*n2.
> n1 * (S n2) = n1 + n1 * n2
> Zero * _ = Zero
> _ * Zero = Zero
More num class fillers
> negate = undefined
> abs = id
> signum _ = one
> fromInteger 0 = Zero
> fromInteger n = S $ fromInteger $ n - 1
So now we’ve got the tools to create a function that would test axiomhood, but it’d be horribly inefficient. It’d look something like this:
isTheorem (PQ a1 a2 s) = a1 + a2 == s
Now, that’s all well and good, but it first has to do the O(n) addition of
a1 and
a2, then the O(n) equality of
a1 +
a2 and
s. Surely we can make this into one n, instead of two? Well, the way to do so is actually really easy - we just exploit the isomorphism between addition and subtraction.
First, we define our recursive rule
> (S n1) - (S n2) = n1 - n2
Next, our base cases. Subtracting Zero from anything is just a null op, and we don’t have a clear definition in PQ of negative numbers - you can’t have -5 hyphens
> n - Zero = n
> Zero - _ = undefined
So from there our work is really easy - we can just recurse down once The algorithm below will take exactly
(a1 + a2) iterations to check for theoremhood
> isTheorem (PQ a1 a2 s) = s - a1 - a2 == Zero
And with that we’re done - we’ve defined the PQ system, written out something to list all the theorems, discovered some novel properties of it, and leveraged those to write a quick theoremhood tester. Not bad, eh?
