Skip to main content

Posts

Showing posts from 2008

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 …

Verifying the Monad Laws with Supercompilation

A while ago I wrote a post about how one can use coq to make a proper monad module. I was just thinking today that it would be nice to have a tool for haskell that would allow one to write down conjectures and discharge them automatically with a theorem prover. Supercompilation makes a nice clean theorem prover for haskell since one could express the equations of interest in haskell itself. Below is an example of the list monad, and then the 3 monad laws written as conj1,conj2 and conj3. I prove the first law by manual supercompilation. The next two are left as an exercise for the interested reader.

equal xs ys = case xs of [] -> case ys of [] -> True _ -> False (x:xs') -> case ys of [] -> False (y:ys') -> case (eq x y) of False -> False …

Proof by Program Transformation

Program transformation is a sort of meta-compilation where the source and target languages are the same. In this sense it can be seen as an automorphism on the set of programs in a language.

As was pointed out by Turchin, it is sometimes possible to prove properties of programs simply by performing a program transformation. Basically a program, and a program which verifies it's behaviour (a predicate) can be replaced with a truth value if the program transformation is sufficiently powerful. An obvious example of course, which can be calculated using partial evaluation would be something like (max (< 3) (1::2::1::nil)). In fact very complex properties can be proved automatically by Distillation, a particularly powerful program transformation system.

In my research I've been working with the μ-Calculus, which is a type of temporal logic that is very powerful (LTL, CTL, CTL* can all be embedded in the μ-Calculus) and good for describing reactive systems. It uses a notion…

Supercompiltation

I've lately been working on my disertation concering a program transformation technique known as Distillation. Distillation is a technique inspired by supercompilation.

Supercompilation involves mapping terms from a particular language to other terms of the same language. It can be though of as a semantics preserving rewriting system, or a function which maps terms to other terms which are equal modulo some semantic interpretation relation. A really strait-forward description of supercompilation is given by XXX on his paper on supercompilation for Haskell. This work leverages work by Gluck and Sorenson but presents generalisation in a very clear and declarative way, which is a notable exception to most of the literature in this field. Generalisation is actually quite a tricky problem. Generalisation has some of the same problems as the old problem with standards. That is, the thing about standards is that there are so many to chose from. It takes quite a bit of effort to c…