Rubrication

I’ve been working with System F quite a bit lately, as it has a complicated enough typing system to be interesting, without having the full insanity of dependent types. I’ve been working with System F including sums products and recursive types. However, all of these can actually be encoded directly in System F. At first I thought this was merely a curiosity. It turns out however that for recursive types, the built in variety has some serious advantages.

System F allows you to take types as arguments as well as terms. From this system you can weave together an impressive array of very expressive types. First I’ll define a few of these, and then I’ll further describe what I find really fascinating.

The basic idea is that we can apply a function such as (Λ X . λ f : X→X, x : X. f x) to some types and terms and we evaluate in a way analogous to the λ-Calculus:

(Λ X . λ f : X→X, x : X. f x) [T] g t ⇒ g t

Now lets look at how we can spin some basic datatypes directly from such a simple calculus.

∀ X. X

This is the type 0. We can think of it as an encoding of False. It is a type which has no inhabitants. If we try to make one, we find we have no way to return a term of an arbitrary type X. Try filling in the question mark: Λ X. ?

0 → 0

This is the type 1. We can think of it as representing True. It has one inhabitant (that is, all terms that fill this type normalise to the same expression). It’s fairly obvious how to write this one:

λ x:0. x

Now we’ll move on to some standard language features in functional programming languages:

∀ X. (A→B→X) → X

This is the type of pairs (A,B). For any two types, A and B we can produce a pairing. The inhabitants of this are a bit more interesting:

pair :: ∀ A B. A→B→(A,B)
pair = Λ A B. λ a: A, b : B. Λ X. λ p : A→B→X. p x y

fst :: ∀ A B. (A,B)→A
fst = Λ A B. λ p : ∀ X. (A→B→X)→X . p [A] (λ x : A, y : B.x)

snd :: ∀ A B. (A,B)→B
snd = Λ A B. λ p : ∀ X. (A→B→X)→X . p [B] (λ x : A, y : B.y)

The constructors and destructors just fall out naturally. You hardly have to think at all about what to produce, just follow the type discipline. This is part of the beauty of parametricity.

∀ X. (A→X)→(B→X)→X

This is the type of sums A+B. If you look closely, you’ll see that there is a pattern developing. Constructors for a datatype have the form (K1→…→X). See if the pattern is more obvious from the code below.

inl :: ∀ A B . A→A+B
inl = Λ A B . λ a:A. Λ X . λ left : A→X, right B→X. left a

inr :: ∀ A B . B→A+B
inr = Λ A B . λ b:B. Λ X . λ left : A→X, right B→X. right b

case :: ∀ A B C. A+B→(A→C)→(B→C)→C
case = Λ A B C.
              λ c : ∀ X. (A→X)→(B→X)→X.
                λ f: A→C, g:B→C
                        c [C] f g

If you look closely at the way case was defined, you’ll see that we didn’t actually do anything. It turns out that inhabitants of the data act as their own case selector. If you try writing down Bool:

∀ X. X→X→X

You’ll find a similar thing is true for if-then-else, which turns out to be superfluous. This is great! So we can get “case” for free from the data type. It turns out this works in general for inductive types.

Now, for something really amazing. It turns out that recursive types are present as well. The data type Nat, which is often written as μ X. 1+X, can be written down as follows:

∀ X. X→(X→X)→X

If you’ve been paying attention, you’ll note the correspondence between the first X and Zero, and the second (X→X) and Succ. Well it turns out μ X. F X can be encode itself as follows:

μ X. F X = ∀ X. (F X→X)→X

Ok great. That’s fairly interesting. Now comes the part that had me floored with the beauty of System F. It is typical in programming languages to have an explicit constructor which allows us to inject into a type. For fun we can write the following type, which simulates the domain equation of the untyped lambda calculus:

data D = InD D→D

This turns out to be somewhat interesting, in that we can produce non-terminating computations with the type, without ever using explicit recursion. Witness the following code*:

omega = ( x -> case x of
                     InD g -> g (InD g))
               (InD ( x -> case x of
                         InD g -> g (InD g)))

Great! We can write down silly terms that don’t terminate. What’s the point you ask? Well, we can write down this type in System F. But System F is strongly normalising (it will always evaluate to a normal form, so it can’t just compute forever). Something seems fishy here, how can this possibly be? Let us look at this datatype in System F.

∀ X . (X→X)→X

So far so good. Now, let’s try to make the constructor:

omega = Λ X . λ f : X→X. ???

We can’t find one! What happened? It turns out that this type is not inhabited in System F. When we wrote the constructor in Haskell, we were LYING!!! That constructor doesn’t actually exist, because that type has no valid inhabitants.

It’s often the case that in proof assistants recursive types are restricted, often with a positivity restriction on the functor F such that such we don’t end up lying about what constructors are actually possible. However, in System F, where we are asked to provide the constructors, this problem never occurs. It seems likely to me that since Mendler style induction schemes are more general than induction with functors restricted to positivity, that there are many types which have inhabitants in System F, which are thrown out by proof assistants such as Coq, despite being perfectly O.K. In addition, there are all sorts of silly types that are allowed in a language like Haskell, despite the fact that they have no realistic inhabitants.

I hope you found this as amazing as I did.

* Note: you might have to add some arbitrary show instance to get haskell to allow you run omega. Don’t worry about how you define “show” since omega never returns!

Standard functional programming languages like Haskell and SML use polymorphic type systems. These type systems however, are not sound. What this means is that the type-systems themselves can not be used to prove properties of the software in the sense of “total correctness”. To see that this is true, we can get a “proof” (read program) of inhabitation of any arbitrary type A, by simply using the program:

data Bot {- Look Ma! No constructors! -}
bot :: Bot
bot = bot

Clearly when we say that bot is an inhabitant of Bot, we dont mean that it actually produces a value of type Bot, since there aren’t any as Bot has no constructors! We can easily use this type of proof to prove something like A ∧ ¬A which leads to a pretty degenerate logic. However, the type system is still *useful* in the sense that if the program ever *does* terminate, it’s sure to do so with the appropriate type. This means we can get the full class of Turing complete programs, a very useful benefit.

In Constructive Type Theory, we need to keep stronger guarantees. For programming languages such as Coq, we use syntactic restrictions to ensure that programs terminate (or coterminate). This however has the annoying feature that a lot of programs which are obviously (co)terminating will be rejected simply because of syntax.

Cyclic proofs give a method of describing inductive or coinductive proofs without requiring that we demonstrate the fact that our term (co)terminates up front. We can defer the proof until later. The huge advantage to this is that we can use ideas from supercompilation, as a form of proof normalisation and then show that the syntactic termination criteria are satisfied for the resulting transformed proof, rather than for the original.

As an example, take the following program (with the usual list, cons notation from Haskell):

 codata CoNat = Z | S CoNat
 data List = [] | (:) CoNat List

 plus :: CoNat -> CoNat
 plus Z y = y
 plus (S x) y = S (plus x y)

 sum :: List -> CoNat
 sum [] = Z
 sum (x:xs) = plus x (sum xs)

Now, we can associate with this the following (infered) pre-proof type tree:

Now, we can use the usual super-compilation manipulations on this type tree, including beta-reduction, etc. to arrive at this new tree:

This is actually a proof, rather than a pre-proof as can be verified syntactically. It satisfies the guardedness condition of coinduction, and the structural recursion condition for induction.

From the proof above, we can derive the following program, which is syntactically sound.

 sum [] = Z
 sum (Z:xs) = sum xs
 sum (S:xs) = S(f x xs)

 f Z xs = sum xs
 f (S x) xs = S(f x xs)

This process is basically an extended form of cut-elimination where we can extend the applicability of cut-elimination since we don’t directly use induction rules, but instead we use cycles in the proof. We can then work with transformations over a larger class of things which are similar to normalisation.

There are a lot of advantages to this approach. In the first program our function ’sum’ did not meet the guardedness condition, which means it would not be admissible in Coq, despite being perfectly correct (as it is in fact productive). Using pre-proofs we can defer proof, which gives us better compositionality. We can even use higher order functions which are not in general correct, on particular functions to derive programs which are totally correct.

In addition, we can decide only to show total correctness for regions of a program, rather than the entire program. We could decide that only certain regions require total correctness, and freely mix total correctness with partial correctness.

There is still a ton of work to be done in this area. It would be nice to know what proof transformation rules coupled with which algorithms can solve various classes of problems. Kamendantskaya has a very interesting class of productive functions which, I believe, could be found using a particular proof transformation algorithm. I’d like to have this algorithm and a proof that it works. In addition, I’d like to have more examples where this can be used to enhance compositionality (I’m thinking of filter functions in particular, where this might come in handy).

Sorry if this blog post is a bit “whirl-wind”. I intend to lay out the entire theory in a slower and better motivated way later.

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ⁿ 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!
Qed.

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)

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
                                          True ->  equal xs' ys'

bind [] f = []
bind (h:t) f = (f h)++(bind t f)

ret a = [a]

conj1 a f = equal (bind (ret a) f) (f a)
conj2 m = equal (bind m (\a -> ret a)) m
conj3 m f g = equal (bind (bind m f) g) (bind m (\x -> (bind (f x) g)))

In order to define equality on lists we had to make reference to a different equality predicate on the elements of the list. We will make the assumption that this equality is decidable and supercompilation can prove the reflexive property for this equality predicate, that is “eq x x = True” will be taken as an assumption. It is somewhat hard to imagine a case where supercompilation would have a hard time with this because of the case substitution rule.

Now we take conj1 and attempt to prove it by semantics preserving transformations of the source code [1]. I’ve been brutally explicit in the steps used so that people who are interested can see exactly how to do these sorts of things themselves. I’ve found that program transformation techniques can be extremely useful in reasoning about code. Of course, it helps to assume that all functions are total, and I’ll be doing just that. I use the notation M[x:=y] to mean the substitution of y for x in M. Aside from that everything is just Haskell.

conj1 a f = equal (bind (ret a) f) (f a)

{- unfold equal -}
conj1 a f = case (bind (ret a) f) of
              [] -> case (f a) of
                      [] -> True
                      _ -> False
              (x:xs') -> case (f a) of
                           [] -> False
                           (y:ys') -> case eq x y of
                                        False -> False
                                        True -> equal xs' ys'

{- unfold bind -}
conj1 a f = case (case (ret a) of
                    [] -> []
                    (z:zs) -> (f h)++(bind zs f))
              [] -> case (f a) of
                      [] -> True
                      _ -> False
              (x:xs') -> case (f a) of
                           [] -> False
                           (y:ys') -> case eq x y of
                                        False -> False
                                        True -> equal xs' ys'

{- case distribution -}
conj1 a f = case (ret a) of
              [] -> case (f a) of
                      [] -> True
                      _ -> False
              (z:zs) -> case ((f h)++(bind zs f)) of
                          [] -> case (f a) of
                                  [] -> True
                                  _ -> False
                          (x:xs') -> case (f a) of
                                       [] -> False
                                       (y:ys') -> case eq x y of
                                                    False -> False
                                                    True -> equal xs' ys'

{- unfold ret -}
conj1 a f = case [a] of
              [] -> case (f a) of
                      [] -> True
                      _ -> False
              (z:zs) -> case ((f h)++(bind zs f)) of
                          [] -> case (f a) of
                                  [] -> True
                                  _ -> False
                          (x:xs') -> case (f a) of
                                       [] -> False
                                       (y:ys') -> case eq x y of
                                                    False -> False
                                                    True -> equal xs' ys'

{- case selection -}
conj1 a f = (case ((f z)++(bind zs f)) of
                      [] -> case (f a) of
                              [] -> True
                              _ -> False
                      (x:xs') -> case (f a) of
                                   [] -> False
                                   (y:ys') -> case eq x y of
                                                False -> False
                                                True -> equal xs' ys')
                                     [z := a,  zs := []]

{- substitution -}
conj1 a f = case ((f a)++(bind [] f)) of
              [] -> case (f a) of
                      [] -> True
                      _ -> False
              (x:xs') -> case (f a) of
                           [] -> False
                           (y:ys') -> case eq x y of
                                        False -> False
                                        True -> equal xs' ys'

{- unfold bind  -}
conj1 a f = case (case (f a) of
                    [] -> []
                    (z:zs') -> z:(zs'++[])) of
              [] -> case (f a) of
                      [] -> True
                      _ -> False
              (x:xs') -> case (f a) of
                           [] -> False
                           (y:ys') -> case eq x y of
                                        False -> False
                                        True -> equal xs' ys' 

{- case selection, substitution -}
conj1 a f = case (f a) of
              [] -> True
              (z:zs') -> case eq z z of
                           False -> False
                           True -> equal (zs'++[]) zs'

{- Assumption: eq z z = True -}
 conj1 a f = case (f a) of
              [] -> True
              (z:zs') -> equal (zs'++[]) zs'

{- unfold of equal and ++ -}
conj1 a f = case (f a) of
              [] -> True
              (z:zs') -> case (case zs' of
                                 [] -> []
                                 (w:ws) -> w:(ws++[]) of
                           [] -> case zs' of
                                   [] -> True
                                   (y:ys) -> False
                           (x:xs) -> case zs' of
                                       [] -> False
                                       (y:ys) -> case (eq x y) of
                                                   False -> False
                                                   True -> equal xs ys

{- case selection -}
conj1 a f = case (f a) of
              [] -> True
              (z:zs') -> case zs' of
                           [] -> True
                           (w:ws) -> case (eq w w) of
                                       False -> False
                                       True -> equal (ws++[]) ws

{- Assumption: eq w w = True -}
conj1 a f = case (f a) of
              [] -> True
              (z:zs') -> case zs' of
                           [] -> True
                           (w:ws) -> equal (ws++[]) ws

{- fold, (we encountered a repeated instance of 'equal (ws++[]) ws') -}
conj1 a f = case (f a) of
              [] -> True
              (z:zs') -> let g = \ xs ->
                                 case xs of
                                   [] -> True
                                   (y:ys') -> g ys'
                         in g zs'

Now we have a function that can only return true, regardless of the value of (f a) and assuming that f is total, we can replace this term with True. The proof of this is simply by induction on (f a), but the principle can be built into a checker and is the principle used in the Poitín [3] theorem prover.

Something along these lines would be very light-weight in comparison to using a full theorem prover and could just issue a warning if some laws couldn’t be proved. The proof of this in Coq is actually more work and requires lemmas about the list type to be proven. I did in fact fudge the ((f a)++[]) situation there by replacing with (f a), and I’m not entirely sure what supercompilation does with it if you leave it in. I’ll have to try it later. UPDATE: This is fixed in the code above.

If we want to prove this result by hand we can also derive it in a much simpler way by not following the supercompilation method verbatim:

conj1 a f = equal (bind [a] f) (f a)
conj1 a f = equal (append (f a) (bind [] f)) (f a)
conj1 a f = equal (append (f a) []) (f a)
conj1 a f = equal (f a) (f a)

The advantage of the former is of course that it is entirely mechanical.

UPDATE: I went ahead and incorporated the definition of append and supercompiled it (by hand) with this definition and it reduces to exactly the same term, so in fact supercompilation, without any special knowledge, is capable of proving the conjecture. This is a real win over most proof assistants which would require this append lemma to be proved separately, or incorporated into the knowledge base. For a more visual and more compact depiction of the derivation we can draw a partial process tree with the append function definition included in the derivation.

And indeed the second monad law:

Is the third monad law for the list monad provable using supercompilation? I expect it is, but since I don’t have a supercompiler, and it is a bit of a bear to do by hand, I’m not sure.

Incidently, there is already a supercompiler being developed for haskell called Supero [2]. It probably wouldn’t be too much work to extend this with theorem proving capabilities using ideas from [3].

[1] A Transformation System for Developing Recursive Programs
[2] A Supercompiler for Core Haskell
[3] Poitın: Distilling Theorems From Conjectures

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 of least and greatest fixed-points in order to describe temporal properties. This lead me to consider infinite proofs, bi-simulation and co-induction in the context of distillation.

I was reading a paper [1], which lead me to wonder if Distillation couldn’t be used as a means of determining if two programs bi-simulate in a very simple way. Distillation can be viewed as a relation between programs, such that a program a and a program b are related by a D b iff a Distils to b (that is b is the result of running the distillation algorithm on b). If the bi-simulation relation is called ~ then we have trivially that:

∀ a b c ∈ PROG. a D c ∧ b D c → a~b

This is obvious since D is semantics preserving, and c must have the same semantics as both a and b. So this looks a little bit silly at first, what good can this possibly be? Can we ever expect this to happen? Well, I was a little bit surprised to find that it does work for simple examples that I tried on paper. For instance, let us take the following program.

iterate f x = x:(iterate f (f x))
map f (h:tl) = (f h):(map f tl)
cofix f = f (cofix f)

conjecture_1 f x = iterate f (f x)
conjecture_2 f x = map f (iterate f x)

We will assume that the “:” constructor is for a type of lists with no “nil” terminator, that is, we are only dealing with infinite lists. Supercompilation is strictly less powerful than Distillation, but sufficient for this example, and simpler to do on paper. We will therefore supercompile the two halves of the conjecture:

∀ f x. iterate f (f x) ~ map f (iterate f x)

to yield:

conjecture_1 f x = iterate f (f x)
-- unfold iterate
conjecture_1 f x = (f x):(iterate f (f (f x))
-- generalise [iterate f (f x), iterate f (f (f x))] =>
--  iterate f (f x) which is just conjecture_1
conjecture_1 f x = (f x):(conjecture_1 f (f x))
conjecture_1 = cofix ( g f x -> (f x):(g f (f x)))

conjecture_2 f x = map f (iterate f x)
-- unfold map
conjecture_2 f x = case (iterate f x) of h:tl => (f h):(map f tl)
-- unfold iterate
conjecture_2 f x = case (x:(iterate f (f x)) of h:tl => (f h):(map f tl)
-- case law, [h:=x, tl:=(iterate f (f x))]
conjecture_2 f x = (f x):(map f (iterate f (f x))
-- generalise [map f (iterate f (f x)), map f (iterate f x)] =>
-- map f (iterate f x), which is just conjecture_2
conjecture_2 f x = (f x):(conjecture_2 f (f x))
conjecture_2 = cofix ( g f x -> (f x):(g f (f x)))

So we can see that conjecture_1 and conjecture_2 are syntactically identical modulo alpha-conversion. The cofix was added just so that the function name didn’t obscure the equality. In fact we could also go to some De Bruijn representation as well, to get rid of the need for alpha-conversion equivalence, but I think you get the picture. In addition, it is trivial to verify that this is a valid co-recursive program satisfying the guard condition that the recursive call happens under the constructor of the co-inductive type which is the co-domain of the co-recursive function (look at all those “co”s!).

The point is though that we have derived a syntactically identical program, and hence proved bi-simulation, using a completely automated procedure!

So the obvious question of course is, how often will this work? The technique relies on finding a canonical form. For non-recursive (NOREC) programs, we can probably always find a canonical form using supercompilation (the S relation, a subset of D). That is, I expect that:

∀ p,q,r,s ∈ NOREC. p D r ∧ q D s → r=s

This is probably obviously true to someone who understands better about normal forms in the lambda calculus, but I haven’t yet proved it for the language over which distillation is defined.

For recursively defined programs, it can’t be the case that we can always find a canonical form. This is the undecidability of equivalence for the lambda calculus. However, I’ll stick my neck out and conjecture that it will work for all programs of suitably low complexity (PRIMREC, ELEMENTARY maybe? [3]). This doesn’t tell us anything about bi-simulation however, since co-recursive programs don’t have a complexity. Is there a co-complexity we could use? It would be really nice to have some class we could show is definitely canonisable.

And while I’m on a roll playing fast and loose, I’ll say that I think that Distillation represents “the right way” of going about finding “proof-net” like structures for intuitionistic logic. That is, internal to the distillation algorithm we actually form a graph, and in the case of conjecture_1 and conjecture_2 the graphs are identical. The internal representation used for distillation then is actually the form in which we remove “The bureaucracy of syntax” [2] for some subset of possible proofs.

For further reading on some of these ideas:

[1] Proof Methods for Corecursive Programs
[2] Down with the bureaucracy of syntax!
[3] The Expressive Power of Higher-order Types or, Life without CONS
[4] Deforestation, program transformation, and cut-elimination

I’ve mentioned a number of times that given a sufficiently rich type theory we can use the type to provide a specification for the function, such that the function is correct by construction. I’d like to give a simple example of how this works in the Coq proof assistant.

The following code is an illustration of how the type theory of Coq allows you to fully specify the behaviour of functions. Kragen Sitaker made the comment that there weren’t too many reasonable interpretations of the function of the type given to the assoc function:

A -> list (A * B) -> option B

that is, a function taking an element of type A, a list of pairs of A and B, to the possibility of a B (and possible failure). That got me wondering how hard it would be to tighten the noose so that there was only one way to interpret the type but still possibly many implementations that satisfy the type, all of which will yield the same result.

The following code illustrates that this is indeed possible to do in Coq.

Require Import List.
Parameter A : Set.
Parameter B : Set.
Definition assoc_list := list (A * B)%type.
Parameter eq_dec : forall (x:A) (y:A),{x=y}+{x<>y}.

Theorem assoc :
  forall (x:A) (l: assoc_list),
    {y | In (x,y) l} + {forall (y:B), ~In (x,y) l}.
  refine
    (fix assoc (x:A) (l:assoc_list) {struct l}
      : {y | In (x,y) l} + {forall (y:B), ~In (x,y) l}
      := match l
           return {y | In (x,y) l} + {forall (y:B), ~In (x,y) l}
           with
           | nil => inright _ (fun y => (fun p : In (x,y) nil => _))
           | ((x',y)::t) =>
             match eq_dec x x' with
               | left lft => inleft _ (exist _ y _)
               | right rgt => match assoc x t with
                                | inleft (exist y p) => inleft _ (exist _ y _)
                                | inright inrgt => inright _ _
                              end
             end
         end) ; clear assoc ; eauto ; subst. constructor. reflexivity.
  firstorder. intros. intro. inversion H ; clear H. firstorder. congruence.
  apply (inrgt y0). assumption.
Defined.

This isn’t the most beautiful code but what it lacks in beauty of implementation it makes up for in ease of reading. There are only a couple of lines that you need to understand to be assured that this is in fact the correct implementation.

Theorem assoc :
  forall (x:A) (l: assoc_list),
    {y | In (x,y) l} + {forall (y:B), ~In (x,y) l}.

This function has a type that takes an “x” of type “A”, a list of pairs and supplies a value “y” of type “B” with a proof that it came from a pair in which the x provided occurs *AND* that that pair exists in the list l. If the function can’t find a pair from which to supply a y, it must supply a proof that no such pair exists in the list.

First a bit of the notation so you can read this theorem properly

{ y | P y }

Can be read: “there exists a y such that the property P holds of y”.

The notation:

A + {B}

Means that we must supply an A or a proof of B.

The “In” predicate is an inductive predicate which specifies membership in a list and is provided by the Coq library.

With a little practice reading types, we can see that the two lines are correct. We can then run Coq on this code to check that the proof is correct and we can be assured of the correctness of the implementation WITHOUT EVER READING THE CODE! This means we have reduced the problem of correctness to two simple lines of completely declarative statements.

This function is more complicated than a normal assoc function because it carries all of these proof terms along with it. However, because of the clever people involved in writing Coq we have actually mixed two different type universes together. One (called Set) for values and one (called Prop) for proofs. Coq uses this fact to do something very clever. The {y|P y} existential type and the A+{B} type are designed such that the “P y” proof and the {B} proof disappear when we extract (compile) our code. As an illustration of this amazing fact look at the following ocaml code which has been automatically extracted from our definition:

let rec assoc x = function
  | Nil -> Inright
  | Cons (p, t) ->
      let Pair (x', y) = p in
      (match eq_dec x x' with
         | Left -> Inleft y
         | Right -> assoc x t)

Voila! Not only are the proof terms gone, but this is pretty much the code you probably would have written yourself. Notice that “Inright” is a constructor with no information (other than failure), basically implementing the “Nothing” of a Maybe type, and the “Inleft” as the “Just” of a Maybe type.

We have extracted a provably terminating, well specified, totally correct function that runs in ocaml! And to top it off we can also compile to Haskell!!

assoc :: A -> Assoc_list -> Sumor B
assoc x l =
  case l of
    Nil -> Inright
    Cons p t ->
      (case p of
         Pair x' y ->
           (case eq_dec x x' of
              Left -> Inleft y
              Right -> assoc x t))

So it isn’t as if this isn’t without some cost. There is a huge learning curve on Coq and I’m by no means an expert. The proofs can be arduous, and although this one only took me a couple of minutes, it took far longer than it would have to implement the function directly in ocaml. However as I gain experience with Coq, I increasingly believe the approach will scale better than traditional approaches to software design.

In addition to these caveats there is more than one function that satisfies this type. Namely there is an assoc which starts returning from the end of the list, instead of the beginning. We could get rid of this problem by specifying which of the elements should be returned, returning all of them, or restricting formation of assoc’s such that they are mappings. The latter is very elegant, but somewhat more involved than what we have done.

Functional programming reduces the difficulty of writing correct software by reducing the ways in which bugs can occur. However, most functional programming languages are unable to put complex constraints like “this is a sorted list” or “implements an assoc function” into the language. When other functions rely on the behaviour all kinds of funny things can happen.

I recently had a nasty non-termination bug in SML because a function *required* that the input list be sorted or the function wouldn’t terminate. My sort routine made use of a bogus less-than-equal predicate over a data-type which I had neglected to write properly. This caused hours of very difficult debugging.

I’m acting on the thesis that I can avoid these problems and I am rewriting a large program in Coq as an experiment. I’ll let you know how it goes.

I’ve been playing with the Coq proof assistant over the past few days, following closely on some frustrations that I’ve been having with using SML’s module system and a bit of toying with type-classes in Haskell.

The gist of the problem is this. Although you can define type-classes and modules such that external users of these modules/type-classes see a uniform interface, consistency is left as an exercise for the implementer. This is not really acceptable in my view. When you are writing software, often times *you* are the implementer. What you really want is for these modules not just to provide a consistent interface to outsiders, but to guarantee the correctness of the implementation! Isn’t that the whole point of types? If we can’t do that, why are we using types?

Ok, so in Coq I *can* get the properties I’ve been wanting out of SML’s module system. For instance take the following implementation of the Monad signature:

Module Type MONAD.
Set Implicit Arguments. 

Parameter M : forall (A : Type), Type.
Parameter bind : forall (A B : Type),
  M A -> (A -> M B) -> M B.
Parameter ret : forall (A : Type),
  A -> M A.

Infix ">>=" := bind (at level 20, left associativity) : monad_scope.
Open Scope monad_scope.

Axiom left_unit : forall (A B : Type) (f : A -> M B) (a : A),
  (ret a) >>= f = f a.
Axiom right_unit : forall (A B : Type) (m : M A),
  m >>= (fun a : A => ret a) = m.
Axiom bind_assoc : forall (A B C : Type) (m : M A) (f : A -> M B) (g : B -> M C) (x : B),
  (m >>= f) >>= g = m >>= (fun x => (f x) >>= g).

End MONAD.

This signature describes something much like the monad that is given by the type-class in haskell. I neglected some stuff like implementing join from bind etc, but we can safely ignore that for now. The point is that users of the MONAD signature can’t just fake a monad by supplying an implementation that is nominally the same. i.e. In order to implement this MONAD you actually have to have the right signature for “>>=” *AND* you have to satisfy the monad laws. So what does an implementation look like? Here is an example:

Module ListMonad < : MONAD. 

Require Import List.

Set Implicit Arguments.

Definition M := list.

Fixpoint bind (A : Type) (B : Type) (l : M A) (f : A -> M B) {struct l} : M B :=
  match l with
    | nil => nil
    | h::t => (f h)++(bind t f)
  end.

Infix “>>=” := bind (at level 20, left associativity) : monad_scope.
Open Scope monad_scope.

Definition ret (A : Type) := fun a : A => a::nil.

Lemma left_unit : forall (A B : Type) (f : A -> M B) (a : A),
 (ret a) >>= f = f a.
Proof.
  intros. simpl. rewrite app_nil_end. reflexivity.
Defined. 

Lemma right_unit : forall (A B : Type) (m : M A),
  m >>= (fun a : A => ret a) = m.
Proof.
  simple induction m.
    simpl. reflexivity.
    intros. simpl.
    cut (bind l (fun a0 : A => ret a0) = l).
      intros. rewrite H0. reflexivity.
      exact H.
Defined. 

Lemma bind_assoc : forall (A B C : Type) (m : M A) (f : A -> M B) (g : B -> M C) (x : B),
  (m >>= f) >>= g = m >>= (fun x => (f x) >>= g).
Proof.
  simple induction m.
    intros. simpl. reflexivity.
    intros. simpl.
    cut (l >>= f >>= g = l >>= (fun x0 : A => f x0 >>= g)).
      intros. rewrite < - H0.
      induction (f a).
        simpl. reflexivity.
        simpl. rewrite IHm0. rewrite app_ass. reflexivity.
      apply H. exact x.
Defined.

End ListMonad.

(* Example *)
Import ListMonad.
Require Import Peano.
Require Import List.

Fixpoint downfrom (n : nat) {struct n} : (list nat) :=
  match n with
    | 0 => n::nil
    | S m => n::(downfrom m)
  end.

Eval compute in (1::2::3::4::nil) >>= downfrom.
  = 1 :: 0 :: 2 :: 1 :: 0 :: 3 :: 2 :: 1 :: 0 :: 4 :: 3 :: 2 :: 1 :: 0 :: nil
     : M nat

Ok, That took me about an hour to write. I’m not really that good at using Coq, so presumably you could do this more elegantly and in less time. In any case it would be nice if the proofs could be automated a bit more. That aside this is a *much* better situation than we have in SML and Haskell. We have provided a monad that is guaranteed to actually be one!

I’m of the growing opinion that software that is forced to meet specifications will end up being less trouble in the end than the current state of free-wheeling wild-west style implementation.

Coq gives a civilized alternative to the current free-for-all. Coq can help us make good on the promise that “well typed programs can’t go wrong”.

A few months ago I started messing around with The Coq Proof Assistant to figure out what exactly it was, and proceeded to go through the tutorial.

Coq provides a nice interface for doing proofs in an interactive session. It was a lot of fun but didn’t seem particularly useful for my research.

As I’ve been playing with the notion of Total Functional Programming, I ended up reading (and actually doing homework) from a book entitled “Type Theory and Functional Programming”. This book is excellent by the way! I highly recommend it to anyone interested in dependent types/proof theory/type theory. It has a very lucid style and makes a lot of complex notions in type theory very easy to understand. I even got to find an error in one of the homework examples (now listed in the errata) which is always fun.

After working through the first 5 chapters I started looking around for a system that would let me apply some of the principles that I had learned.

As it turns out Coq is really a dependently typed functional programming language masquerading as a proof assistant! I’ve spent quite a lot of time over the past few weeks writing total functional programs in Coq and proving properties about them. I’ve done a bunch of simple things so far, including a proof of correctness for various properties of insertion sort. I started with merge sort, but stalled when it got too complicated. I’m starting to get a feel for using Coq however and large proofs are getting much easier.

In my research I’ve been working on the implementation of the distillation algorithm (a form of super-compilation) for logic programming. As it turns out
the distillation algorithm as described by Geoff Hamilton could be a real boon to total functional programming in Coq.

In Coq all functions and other values are terms that represent witnesses of a proof. Inhabitation of types is proved exactly by creating a term of the appropriate type. The “tactic” system in Coq is basically a library that helps you build appropriate terms. Alternately you can supply the proofs directly by writing in the functional programming language that acts as the witness terms of the types.

In order to avoid inconsistency functions are not capable of general recursion or errors or exceptions, as this can immediately lead to proofs of propositions which are not actually inhabited. A simple example (in psuedo-haskell) would be a function with the following structure.

loop :: int -> arbitrary
loop x = loop x

Clearly “int -> arbitrary” is not actually the type of this function. It doesn’t terminate and so has type _|_. Types in languages like ML and haskell aren’t actually just as they are written, but include the possibilities of non-termination or errors into the type implicitly. This (arguably) works out alright if you expect to run your program, but if you are trying to prove useful properties in your type system it turns out to be pretty worthless.

Syntactic restrictions are therefor necessary to avoid including non-terminating functions in Coq. The method chosen is to accept only structurally recursive functions, which can be checked with simple syntactic criterion. In fact the functions require you to specify *which* argument of a function is structurally recursive. This works out surprisingly well but can occasionally be a real pain (try working out a unification algorithm without using anything but structural recursion).

In Coq 8.1 they include a way to define functions that include a measure function which provably decreases or to use a well-founded relation (in conjunction with a proof) to show that the function terminates.

Distillation likes to take functions from general recursion to structural tail recursion. If you could define functions in Coq such that they were then processed by distillation, it would be very useful!

If you haven’t tried Coq yet, you should. And if you haven’t tried total functional programming yet, I suggest trying it in Coq.

The following is some SML code that implements the natural numbers using peano arithmetic in the SML type system. These numbers can be used to protect access to list functions. I haven’t yet figured out if addition is possible, but I’m hoping that it is. It could be really handy!

signature SLIST =
sig
    type 'a nat
    type Z
    type 'a S
    val S : 'a nat -> 'a S nat
    val P : 'a S nat -> 'a nat
    val Z : unit -> Z nat
    val zerop : 'a nat -> bool
    val toInt : 'a nat -> int 

    type ('elt,'n) slist

    val snil : unit -> ('elt, Z nat) slist
    val scons : 'elt -> ('elt, 'n nat) slist -> ('elt, 'n S nat) slist
    val :+: : 'elt * ('elt, 'n nat) slist -> ('elt, 'n S nat) slist
    val shd : ('elt, 'n S nat) slist -> 'elt
    val stl : ('elt, 'n S nat) slist -> ('elt, 'n nat) slist
    val slen : ('elt, 'n S nat) slist -> int

end

structure SList :> SLIST =
struct
    (* encode integer types *)
    type 'a nat = int
    type Z = unit
    type 'a S = unit
    fun S i = i+1;
    fun P i = i-1;
    fun Z () = 0
    fun zerop 0 = true
      | zerop _ = false
    fun toInt d = d

    type ('elt, 'n) slist = 'elt list * 'n

    fun snil () = ([],0)

    fun scons elt sl =
	let val (l,i) = sl
	in ((elt::l),S i)
	end    

    infixr :+:
    fun x :+: y = scons x y

    fun shd sl =
	let val (h::t,i) = sl
	in h
	end

    fun stl sl  =
	let val (h::t,i) = sl
	in (t,P i)
	end

    fun slen sl =
	let val (_,i) = sl
	in i
	end

end 

open SList
infixr :+:

val mylist = 1 :+: 2 :+: 3 :+: snil();
val the_head = shd mylist;
val the_tail = stl mylist;
val the_next_head = shd the_tail;
(*
This doesn't even compile!
val head_of_nil = shd (snil())
*)

I just got “ML for the working programmer” in the mail a few days ago,
and worked through it at a breakneck pace since receiving it. It
turns out that a lot of the stuff from the “Total Functional
Programming” book is also in this one. Paulson goes through the use
of structural recursion and extends the results by showing techniques
for proving a large class of programs to be terminating. Work with
co-algebras and bi-simulation didn’t quite make it in, except for a
brief mention about co-variant types leading to the possibility of a
type: D := D → D which is the type of programs in the untyped lambda
calculus, and hence liable to lead one into trouble.

I have to say that having finished the book, this is the single most
interesting programming book that I’ve read since “Paradigms of
Artificial Intelligence Programming” and “Structure and Interpretation
of Computer Programs”. In fact, I would rate this one above the other
two, though I think it might be because of my current interests.

The conjunction of “Total Functional Programming” and “ML for the
Working Programmer” have completely changed my world view of automated
deduction. Interestingly, my advisers work looks even more appealing
from this perspective.

The basic crux of the issue is this. Given that we restrict ourselves
to total functional programming, as described in the aforementioned
article, we will have the ability to prove theorems directly by
manipulation of the program source.

My adviser told me about this the first time that I met him. It at
first seemed like a curiosity. It has however, blossomed into a
completely different way of thinking about how proofs should be
performed.

I’ve spent the last few days converting proofs into program source,
which I then manipulate equationally. I have a few examples of
inductive proofs that can be written quite naturally as structurally
recursive functions.

datatype nat = Z | S of nat

fun lt n m =
    case m of
	Z => false
      | (S m') =>
	case n of
	    Z => true
	  | (S n') => lt n' m'

fun divide n d =
    case n of
	Z => (Z,Z)
      | (S n') =>
	let val (q',r') = divide n' d in
	    case lt (S r') d of
		true => (q',S r')
	      | false => (S q',Z)
	end

Both of these functions are direct “extractions” of a program from a
proofs that I wrote. The second one is a proof with two existential
variables. The two existential variables present themselves as return
values. In the case of “lt” it simply computes a truth value.

The datatype nat = Z | S of nat defines natural numbers with the
correspondence Z=0, S(Z)=1, S(S(Z))=2 etc…

The proof is a proposition that goes like this:

∀n,d:nat. d>0 ∃q,r:nat. n=dq+r ∧ 0≤r<d

You might notice I dropped the restriction on d in the actual source
code. That can be encoded with an auxiliary function in any case.

The proof proceeds inductively, basically you can turn the divide
function inside out to recover the inductive proof.

The base case is n=0 which gives 0=dq+r which gives r=0 and q=0 (since
d is greater than 0). The first case is exemplified in the case
structure above. (Z,Z) = (q,r) the two existential variables are
returned with a valid result for n=0.

The inductive case is this.

n: ∃q,r. n=dq+r ∧ 0≤r<d
(n+1): ∃q’,r’. n+1=dq’+r’ ∧ 0≤r’<d
if(r+1)<d
then n+1=dq+r+1

We see that this gives us that r’=r+1, q’=q giving us a solution to r’ and q’ from r and q (and hence solving the n case, gives us some information about n+1)

else n+1 = d(q+1)+r’

which we can rewrite as: n+1 = d(q+1)+r’ = dq+d+r’=dq+r+1 so d+r’=r+1,
but r+1 must be at least d otherwise we wouldn’t have failed the test
r+1<d, and r’ can be no less than zero, so we must choose r’=0
this results in (finally!)

n+1 = d(q+1) with r’=0,q’=q+1

We have a proof! For the extracted program you can look at the source
and see that in fact it mirrors the proof directly, short of a few
simplifications done by hand. Making use of the r,q in the proof of
r’ and q’ is the same as my use of r and q in my proof of the n+1 case.

I’m looking forward to a deeper understanding of the correspondences
between proofs and programs with my new found capacity to produce actual functional program proofs by extraction manually. I’m also
curious to try my hand at generating termination proofs directly, and
also at making a syntax that more directly supports total functional
programming.