PQ-Haskellized.lhs

This is a hybrid markdown and Literate Haskell document.  It's a blog post that I converted to pure html and posted <a href="http://blog.gallabytes.com/2014/03/isomorphism-equality-pq-and-other-ways.html">here</a>

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, <a href="http://blog.gallabytes.com/2014/03/miu-haskellized.html">MIU</a> 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:
<ol>
<li> The only valid characters are -, P, and Q</li>
<li> -P-Q-- is a theorem</li>
<li> $\forall x.$ $x$P -Q -$x$ is a theorem</li>
<li> $\forall x y z.$ if $x$P $y$Q $z$ is a theorem, then $x$P -$y$Q -$z$ is a theorem</li>
</ol>
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:
<ul>
<li>We've got an infinite list of theorems, generated by some recursive rules</li>
<li>Our job is to somehow figure out if any given (valid) string is going to be somewhere in that list</li>
<li>There are two recursive rules doing the generating, so we can't even do a linear scan through the infinite set</li>
<li>And, most algorithms to do diagonal scans are annoyingly complicated for what should be a simple test</li>
<li>Neither of those "full scan" approaches can ever give us certainty that something is a nontheorem - just that we haven't found it yet</li>
</ul>
Well, the simplest way is to exploit an isomorphism between PQ and arithmetic.  You can see this if you interpret $x$P $y$Q $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 <a href="https://en.wikipedia.org/wiki/Peano_axioms">Peano Axioms</a>, 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 S(n), n1*S(n) = n1 + n1*n

>   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