Rubrication

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 (S n 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 easil...

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 ...

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 noti...