Skip to main content

The Co-Natural Numbers in Haskell and Coq

I was playing around with the Peano numerals in Haskell (as I often do), because I remember briefly reading about a generalisation of exponentiation in a paper once when I didn't have time to read it. I decided I'd quickly look at it again now that I was in a mood to procrastinate.

> data Nat = Z | S Nat deriving Show
This data type is usually identified with the peano numerals. In fact as we will see, in haskell it isn't quite the natural numbers. We take Z to mean 0 and take (Sn Z) or (S (S (S ... Z))) n times, to mean n. It's basically a unary number system where the length of the string gives us the number.

It is pretty straightforward to write the basic arithmetic operations on the peano numerals.

> add x Z = x
> add x (S y) = S (add x y)
> mult x Z = Z
> mult x (S y) = add x (mult x y)
> expt x Z = (S Z)
> expt x (S y) = mult x (expt x y)
Here we can see an extension of this series fairly easily. The only real question we might have is what to do with the base case. It turns out that (S Z) or 1 is a good choice.

> exptexpt x Z = (S Z)
> exptexpt x (S y) = expt x (exptexpt x y)
Playing with exptexpt got me thinking about the fact that I wasn't dealing with natural numbers and I was curious what I could prove about them. In order to see that we don't actually have the natural numbers we can define the following:

> inf :: Nat
> inf = S (inf)
This element is clearly not a natural number since it is not a valid recursive equation in the sense that there is no decreasing quantity. It is however a valid corecursive equation. It is always productive in the sense that it always has it's recursive reference inside of a constructor. We will always be able to "peel" something away from this function in order to reason about it. This will become obvious when we start looking at equational reasoning with infinity.

So this leads us to the question: what does inf+x equal? I'll prove it in pseudo-Coq. Let us make the following conjecture:

∀ x, inf + x = inf

Theorem : ∀ x, inf + x = inf.
  By coinduction:

  case x = 0: 
    1a) inf + 0 = inf 
    2a) inf = inf
    * true by the reflexive property of =
  case x = S x'
    1b) inf + S x' = inf
    2b) S (inf + x') = inf
    3b) S (inf + x') = S inf
    4b) inf + x' = inf
    * true as this is the coinductive hypothesis!

Now the equality that we are using here is actually not term based equality. It is a coinductive type of equality known as bisimulation. It also must follow the rule that we can never use recursion unless we are inside a constructor for the type of the function we are using. The recursion is the coinductive hypothesis. The constructor prior to the use of the coinductive hypothesis is from the definition of bisimulation. Namely:

∀ x y, x = y → S x = S y.

The full definition in Coq of the bisimulation which we denote above as "=" and below as "CoEq" is:
CoInductive CoEq : CoNat -> CoNat -> Prop := 
| coeq_base : forall x, CoEq Z Z
| coeq_next : forall x y, CoEq x y -> CoEq (S x) (S y).

The constructor coeq_next, which is used between step 3b and 4b above ensures that we satisfy our guardedness, or productivity condition and can safely "call" the coinductive hypothesis. What do I mean "call" and how is the "constructor" being used? We can see exactly by printing out the term in Coq that proves inhabitation of the type for our proposition.

add_x_inf = 
cofix add_x_inf (x : CoNat) : x + inf ~= inf :=
  eq_ind_r (fun c : CoNat => x + c ~= c)
    (eq_ind_r (fun c : CoNat => c ~= S inf)
       (coeq_next (x + inf) inf (add_x_inf x)) (add_x_s x inf))
    (decomp_eql inf)
     : forall x : CoNat, x + inf ~= inf

Here we see in gory detail a corecursive function that allows us to show this type is inhabited along with the corecursive call shown embedded in the constructor coeq_next. Sorry if it isn't very readable, it was constructed automagically from the proof script.

To see how this is all done in detail, check out the Coq proof script for the co-naturals. This might be interesting to those of you who want to see how to use coinductive reasoning on simple examples and how setoids work in Coq. You'll notice that the reasoning is slightly more cumbersome then what I've used here. I think this mostly comes down to the "cofix" tactic being unwieldy in coq, and making automation a hassle. I'm going to think about ways to fix this since it really is unnecessarily inconvenient.

Here are some helper functions which convert from positive integers into our representation so you can play with the code more easily.

> to 0 = Z
> to (n+1) = (S (to n))
> from Z = 0
> from (S x) = 1+(from x)


Popular posts from this blog

Generating etags automatically when needed

Have you ever wanted M-. (the emacs command which finds the definition of the term under the cursor) to just "do the right thing" and go to the most current definition site, but were in a language that didn't have an inferior process set-up to query about source locations correctly (as is done in lisp, ocaml and some other languages with sophisticated emacs interfaces)?

Well, fret no more. Here is an approach that will let you save the appropriate files and regenerate your TAGS file automatically when things change assuring that M-. takes you to the appropriate place.

You will have to reset the tags-table-list or set it when you first use M-. and you'll want to change the language given to find and etags in the 'create-prolog-tags function (as you're probably not using prolog), but otherwise it shouldn't require much customisation.

And finally, you will need to run etags once manually, or run 'M-x create-prolog-tags' in order to get the initia…

Managing state in Prolog monadically, using DCGs.

Prolog is a beautiful language which makes a lot of irritating rudimentary rule application and search easy. I have found it is particularly nice when trying to deal with compilers which involve rule based transformation from a source language L to a target language L'.

However, the management of these rules generally requires keeping track of a context, and this context has to be explicitly threaded through the entire application, which involves a lot of irritating and error prone sequence variables. This often leads to your code looking something a bit like this:

compile(seq(a,b),(ResultA,ResultB),S0,S2) :- compile(a,ResultA,S0,S1), compile(b,ResultB,S1,S2).
While not the worst thing, I've found it irritating and ugly, and I've made a lot of mistakes with incorrectly sequenced variables. It's much easier to see sequence made explicitly textually in the code.

While they were not designed for this task, but rather for parsing, DCGs turn out to be a convenient …

Formalisation of Tables in a Dependent Language

I've had an idea kicking about in my head for a while of making query plans explicit in SQL in such a way that one can be assured that the query plan corresponds to the SQL statement desired. The idea is something like a Curry-Howard in a relational setting. One could infer the plan from the SQL, the SQL from the plan, or do a sort of "type-checking" to make sure that the plan corresponds to the SQL.

The devil is always in the details however. When I started looking at the primitives that I would need, it turns out that the low level table joining operations are actually not that far from primitive SQL statement themselves. I decided to go ahead and formalise some of what would be necessary in Agda in order get a better feel for the types of objects I would need and the laws which would be required to demonstrate that a plan corresponded with a statement.

Dependent types are very powerful and give you plenty of rope to hang yourself. It's always something of…