Programs from Proofs via the Curry-Howard Correspondence

Last time we wrote a theorem prover for intuitionistic propositional logic. This time I want to use it to explore the Curry-Howard correspondence, which is the idea that propositions in logic are like types in functional programming. The basic correspondence goes like this:
PropositionType
Implication
a->b		Function
a->b
Conjunction
a&b		Product type
(a,b)
Disjunction
a|b		Sum type
Either a b

(If this seems strange at first, think about it this way: The product type (a,b) is an a and a b. The sum type Either a b is an a or a b. The function type a->b means that if you give me an a, then I can give you back a b, so an a implies a b.)

So far so good. But the Curry-Howard correspondence goes further. First of all, it says that if there is a Haskell function having a particular (polymorphic) type, then the corresponding proposition is provable in intuitionistic logic. For example: 

> :t fst
fst :: (a,b) -> a
> proofG4ip $ [] |- [a*b-->a]
Just
    a,b |- a    (Axiom)
  (a&b) |- a    (LeftConj)
 |- ((a&b)->a)    (RightImpl)

(In Hugs and GHCi, :t tells you the type of an expression. We find that the type of "fst" - when translated into a proposition using the Curry-Howard correspondence - is provable in intuitionistic logic.)

A function of a given type is called an inhabitant of that type, and a witness for the corresponding proposition. The second part of the Curry-Howard correspondence says that if a proposition is provable in intuitionistic logic, then it has a witness - there is a function with the corresponding type. For example, we can prove that a&b -> b&a : 

> proofG4ip $ [] |- [a*b --> b*a]
Just 
      a,b |- b    (Axiom)
      a,b |- a    (Axiom)
    a,b |- (b&a)    (RightConj)
  (a&b) |- (b&a)    (LeftConj)
 |- ((a&b)->(b&a))    (RightImpl)

So there must be a function having the corresponding type. In this case, it is easy to see what it is: 

swap :: (a,b) -> (b,a)
swap (x,y) = (y,x)

Now, it turns out that we can automate the process of finding witnesses. There is a Haskell program by Lennart Augustsson called Djinn (available here). You give it a type, and it finds a function of that type, if there is one, or tells you if there isn't. Here's an example session: 

Djinn> swap ? (a,b) -> (b,a)
swap :: (a, b) -> (b, a)
swap (a, b) = (b, a)
Djinn> distrR ? (a, Either b c) -> Either (a,b) (a,c)
distrR :: (a, Either b c) -> Either (a, b) (a, c)
distrR (a, b) =
         case b of
         Left c -> Left (a, c)
         Right d -> Right (a, d)
Djinn> cast ? a -> b
-- cast cannot be realized.

Pretty amazing isn't it. But how does it work? Well, that's what I want to find out. So, what follows is my attempt to do what Djinn does. (However, I may as well admit in advance, it won't be as polished.)

The engine behind Djinn is an intuitionistic theorem prover - in fact the documentation says that it uses LJT, which is another name for the G4ip system that we looked at last time. The basic idea is pretty simple - you just interpret the inference rules as typing rules instead. For example, here are some rules for axiom and conjunction. 

Axiom     ------------  (p atomic)
          A,x:p |- x:p

           A,x:p,y:q |- m:r                            A |- m:p    A |- n:q
LeftConj  ------------------                RightConj  --------------------
          A,(x,y):p&q |- m:r                           A |- (m,n):p&q
The expressions with colons are term:type. For example, in Axiom, x:p means x is a variable of type p. Thus, the axiom rule says that if you assume a variable x of type p, then it is provable that x is a term of type p. Both conjunction rules basically say that if you have terms x of type p and y of type q, then you can form a term (x,y) of type p&q.

Notice that if you ignore the terms to the left of the colons and just look at the types to the right, then these rules are just the same as the G3ip inference rules that we looked at last time.

The rules for disjunction and implication are similar, but need a bit more explanation: 

           A,x:p |- m:r    A,y:q |- n:r                   A |- m:p          A |- m:q
LeftDisj  ------------------------------    RightDisj  --------------    --------------
          A,z:p|q |- case(z,x->m,y->n):r               A |- inl m:p|q    A |- inr m:p|q

          A |- m:p    A,x:q |- n:r                       A,x:p |- m:q
LeftImpl  ------------------------          RightImpl  ---------------
          A,y:p->q |- n[x:=y m]:r                      A |- \x->m:p->q
In the disjunction rules, "inl" and "inr" are the left and right injections into the sum type (called Left and Right in Haskell's Either type). "case(z,x->m,y->n)" is the expression "case z of Left x -> m; Right y -> n". In the left implication rule, "n[x:=y m]" means "let x = y m in n" - in other words substitute y m for x in n.

Okay, so how do we use these rules to find functions for a given type? Well, we take the (proposition corresponding to the) type as the root of a proof tree. Then we build the proof tree upwards as before, working just with propositions (types). Then, starting at the top(s) of the proof tree, we add in the terms, and work our way downwards until we end up back at the root.

For example, here's the proof of p&q -> q&p, now written out in tree form: 

--------    --------  (Axiom)
p,q |- q    p,q |- p
--------------------  (RightConj)
     p,q |- q&p
     ----------  (LeftConj)
     p&q |- q&p
     -----------  (RightImpl)
     |- p&q->q&p
Now, starting at the top, we add in the terms, and work our way downwards using the typing rules: 
-----------------    -----------------  (Axiom)
x1:p,x2:q |- x2:q    x1:p,x2:q |- x1:p
--------------------------------------  (LeftConj)
       x1:p,x2:q |- (x2,x1):q&p
      --------------------------  (RightConj)
      (x1,x2):p&q |- (x2,x1):q&p
     -----------------------------  (RightImpl)
     |- \(x1,x2)->(x2,x1):p&q->q&p

Time for some Haskell. The first thing we need to do is define a datatype for typed lambda calculus with sums and products: 

import Gentzen
import List (delete, (\\), sort, insert)
import Maybe (fromJust)

data Term = Var Int |
            Lambda Term Term |                   -- \x -> t - where x is usually a variable but sometimes a pair
            Apply Term Term |
            Pair Term Term |                     -- (t,u)
            Case Term (Term,Term) (Term,Term) |  -- case x of Left l -> t; Right r -> u
            Inl Term |                           -- Left t
            Inr Term                             -- Right t
            deriving (Eq,Ord)

We'd like a show function which will output valid Haskell - that way we can use the :t command to check our answers. 

instance Show Term where
    show s = case s of
             Var i              -> "x" ++ show i
             Lambda x t         -> case t of
                                   Lambda _ _ -> "\\" ++ show x ++ " " ++ tail (show t)
                                   otherwise  -> "\\" ++ show x ++ " -> " ++ show t
             Apply t u          -> brackets t ++ " " ++ brackets u
             Pair t u           -> "(" ++ show t ++ "," ++ show u ++ ")"
             Case t (x,u) (y,v) -> "case " ++ show t ++ " of Left " ++ show x ++ " -> " ++ show u ++ "; Right " ++ show y ++ " -> " ++ show v
             Inl t              -> "Left " ++ brackets t
             Inr t              -> "Right " ++ brackets t

brackets t = case t of
             Var _     -> show t
             Pair _ _  -> show t
             otherwise -> "(" ++ show t ++ ")"

> Lambda 1 (Lambda 2 (Pair (Var 1) (Var 2)))
\x1 x2 -> (x1,x2)

Now, for the LeftImpl rule, we need to be able to substitute a term for a variable in another term. It will turn out to be useful, given a term t, to be able to replace all occurrences of a term u in it by another term u': 

subst t (u,u')
    | t == u    = u'
    | otherwise = case t of
        Var n      -> Var n
        Lambda x v -> Lambda x (v `subst` (u,u'))
        Apply v w  -> Apply (v `subst` (u,u')) (w `subst` (u,u'))
        Pair v w   -> Pair (v `subst` (u,u')) (w `subst` (u,u'))
        Case s (x,v) (y,w) -> Case (s `subst` (u,u')) (x `subst` (u,u'), v `subst` (u,u')) (y `subst` (u,u'), w `subst` (u,u'))
        Inl v      -> Inl (v `subst` (u,u'))
        Inr v      -> Inr (v `subst` (u,u'))

To build the proof tree upwards, we need tactics for the inference rules, as before. If you compare the typing rules above (ignoring the terms) with the inference rules from last time, you'll see that the typing rules are the same as the G3ip rules, except for LeftImpl. (More on this later.) Therefore, we need to write a new tactic for this rule: 

leftImplCH (Seq as [r]) = zip [ let as' = delete f as in [Seq as' [p], Seq (q:as') [r]] | f@(Impl p q) <- as] (repeat LeftImpl)

tacticsCH = axiomG3ip +++ leftConjG3ip +++ rightConjG3ip +++ leftDisjG3ip +++ rightDisjG3ip +++ leftImplCH +++ rightImplG3ip

proofCH = proof tacticsCH

So we can build proof trees upwards. Now, starting at the top, we need to add terms going downwards. The code is a bit fiddly, so I'll just give a couple of examples. 

termFromProof (PT (Seq as [p]) Axiom [], i) =
    let as' = zip (sort as) (map Var [i..])
        Just v = lookup p as'
        p' = (p,v)
    in (Seq as' [p'], i + length as)

What this code says is, if we're asked to find terms from a proof involving just an Axiom inference, it's easy. First, for each proposition appearing as an assumption on the left of the sequent, generate a new variable. (The i parameter to the function is a counter to help us do this.) Now, find which assumption led to the conclusion on the right of the sequent. Then the corresponding variable is a term of the required type. 

termFromProof (proof@(PT (Seq as [r]) LeftConj [child@(PT (Seq bs _) _ _)]), i) =
    let Conj p q = head (as \\ bs) -- the principal formula
        (Seq as' [(_,m)],j) = termFromProof (child,i)
        Just x = lookup p as'
        as'' = delete (p,x) as' -- we must delete first result before doing second lookup, in case p==q
        Just y = lookup q as''
        as''' = insert (Conj p q, Pair x y) $ delete (q,y) as''
    in ( Seq as''' [(r, m)], j)

If the bottom rung of our proof ladder uses LeftConj, then the first thing we need to do is make a recursive call to termFromProof to get the terms which have come down from the proof tree above. Then we identify the p&q that has been used in the rule, by taking the set difference between the assumption lists on top and bottom of the rule. Now, look up the terms x:p and y:q coming from the tree above. Finally, remove x:p, y:q from the assumptions, and add (x,y):p&q. 

termFromProof (PT (Seq as [Conj p q]) RightConj [first,second], i) =
    let (Seq as' [p'@(_,m)],j) = termFromProof (first,i)
        (Seq bs' [q'@(_,n)],k) = termFromProof (second,j)
        n' = foldl subst n (zip (map snd bs') (map snd as'))
    in (Seq as' [(Conj p q, Pair m n')], k)

If the bottom step of our proof tree uses RightConj, we have one more problem to contend with. The two branches of the proof tree above will have topped out in different Axiom inferences, in which different variables will have been generated for the same types. We need to rename the variables from one branch to bring them into line with the other.

The code for the other rules is basically more of the same. See ProgramsFromProofs.hs for the full code.

Okay, so let's see what it can do. 

witness p = case proofCH ([] |- [p]) of
                   Just proof -> let (Seq _ [(p',t)], _) = termFromProof (proof,1) in Just t
                   Nothing    -> Nothing

> witness (a*b-->b*a)
Just \(x1,x2) -> (x2,x1)
> witness (a*(b+c)-->a*b+a*c)
Just \(x1,x9) -> case x9 of Left x2 -> Left (x1,x2); Right x6 -> Right (x1,x6)
> witness (a-->b)
Nothing

It works! We can use the :t command to confirm that the result has the required type. For example: 

> :t \(x1,x9) -> case x9 of Left x2 -> Left (x1,x2); Right x6 -> Right (x1,x6)
\(x1,x9) -> case x9 of {...} :: (a,Either b c) -> Either (a,b) (a,c)

A few closing remarks are in order.

First, I mentioned that Djinn uses G4ip. If you look at our rules, you'll see that we're not using G4ip or even G3ip. Our LeftImpl rule is weaker than the G3ip rule. (In all other cases, we're using the G3ip/G4ip rules.) In theory then, that means that there are some theorems of intuitionistic propositional logic that we can't prove, and hence some programs that we can't find. So far, I haven't managed to work out what they are.

Second, it's worth saying a bit more about typed lambda calculus with sums and products. This is a subset of Haskell, but it's actually quite a large subset. If you think about it, arbitrary tuples can be built up out of pairs, and arbitrary variant types can be built up out of Either. The general Haskell datatype, as defined in a "data" declaration, is just a sum of products (modulo some syntactic sugar).

Where next? Well, the reason I got interested in this in the first place is because Dan Piponi pointed out a similarity between some propositions in modal logic and the types of some functions involving monads. Could this work be extended to an inference system for modal logic, that would be able to write monadic functions for you?

The full code is in ProgramsFromProofs.hs. (Note that I also had to make a couple of minor changes to Gentzen.hs.)

Sources

Sorenson, Urzyczyn, Lectures on the Curry-Howard Isomorphism
(Available here or here.)

Copyright (c) David Amos, 2007
polyomino (at) f2s (dot) com