Encoding provability logic and Löb's theorem in Haskell.

Loeb.hs

-- | A proof of Löb's theorem in Haskell, in reply to [1].
-- 
-- Like Dan Piponi's post on the subject [2], we end up with a function which is
-- basically a spreadsheet evaluator.
-- 
-- Unlike Dan's post, our proof of Löb's theorem follows the Wikipedia
-- proof [3] very closely. Since the proof is using provability logic, we
-- need to encode the rules of provability logic inside Haskell.
-- In particular, we avoid the common mistake of representing the rule
-- 
--    ⊢ A
--   -----
--   ⊢ □ A
-- 
-- as a function of type "a -> □ a". This encoding would not match the
-- semantics of the rule in provability logic, where the rule can only be
-- applied with an empty context. A function of type "a -> □ a", on the other
-- hand, can be applied in any context, and would represent the following
-- rule instead:
-- 
--    Γ ⊢ A
--   -------
--   Γ ⊢ □ A
-- 
-- [1] http://www.reddit.com/r/haskell/comments/2gy4la/a_proof_of_l%C3%B6bs_theorem_in_haskell/
-- [2] http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet.html
-- [3] http://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L.C3.B6b.27s_theorem

{-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables #-}
{-# LANGUAGE BangPatterns, FlexibleInstances, TupleSections #-}
module Loeb where


-- Common rules of logic, such as modus ponens, which are not explicitly listed
-- as rules on the Wikipedia page but which are nevertheless used by the proof
-- on that page.
class Logic t where
  logic1 :: t (a -> b) -> t a -> t b
  logic2 :: t (a -> b) -> t (b -> c) -> t (a -> c)
  logic3 :: t (a -> b -> c) -> t (a -> b) -> t (a -> c)

-- The three inference rules of provability logic, as documented on wikipedia.
-- The type "t a" represents the judgement "⊢ A", and the type "p a" represents
-- the formula "□ A".
class Logic t => ProvabilityLogic t p where
  rule1 :: t a -> t (p a)
  rule2 :: t (p a -> p (p a))
  rule3 :: t (p (a -> b) -> p a -> p b)

-- One slight difference from Wikipedia's proof is that Wikipedia assumes that
-- fixed points exist for all formulas of one argument, whereas we only assume
-- that it exists for
-- 
--   f(x) = □ x -> a
-- 
-- which is the only formula at which the Wikipedia proof uses fixed points.
-- 
-- The numbering of the steps is the same as in the Wikipedia proof, which
-- should be used as a reference when reading this code.
loeb :: forall t p psi a. ProvabilityLogic t p
     => (t (psi -> (p psi -> a)))
     -> (t ((p psi -> a) -> psi))
     -> t (p a -> a)
     -> t a
loeb psi1 psi2 premise = step14
  where
    step3 :: t (psi -> p psi -> a)
    step3 = psi1
    
    step4 :: t (p (psi -> p psi -> a))
    step4 = rule1 step3
    
    step5 :: t (p psi -> p (p psi -> a))
    step5 = logic1 rule3 step4
    
    step6 :: t (p (p psi -> a) -> p (p psi) -> p a)
    step6 = rule3
    
    step7 :: t (p psi -> p (p psi) -> p a)
    step7 = logic2 step5 step6
    
    step8 :: t (p psi -> p (p psi))
    step8 = rule2
    
    step9 :: t (p psi -> p a)
    step9 = logic3 step7 step8
    
    step10 :: t (p psi -> a)
    step10 = logic2 step9 premise
    
    step11 :: t ((p psi -> a) -> psi)
    step11 = psi2
    
    step12 :: t psi
    step12 = logic1 step11 step10
    
    step13 :: t (p psi)
    step13 = rule1 step12
    
    step14 :: t a
    step14 = logic1 step10 step13


-- Now, let's apply our proof to something! To do this, we need to find types
-- "t", "p", "psi" and "a" which satisfy all the hypotheses.

-- Any type former F which is an instance of Applicative will easily satisfy
-- all the rules for Logic and ProvabilityLogic, but in order to demonstrate
-- that our proof works even when there are no functions of type "a -> p a",
-- let's pick a type former for "p" which is not an Applicative.

data Pair w a = Pair !w a deriving (Show, Eq)

-- cannot be defined:
--pure :: a -> Pair w a
--pure x = Pair ? x


-- To avoid the temptation to fill this question mark with mempty, let's also
-- choose a type for "w" which is not a Monoid.

type NonEmpty a = (a,[a])

nappend :: NonEmpty a -> NonEmpty a -> NonEmpty a
nappend (x,xs) (x',xs') = length rhs `seq` (x,rhs)
  where
    rhs = xs ++ (x':xs')


type NString = NonEmpty Char

nString :: String -> NString
nString = (';',)

writing :: String -> a -> Pair NString a
writing s = Pair (nString s)


-- We are now ready to implement all the axioms. You can think of the type
-- "Pair (NonEmpty w) a" as the type "Writer [w] a" minus the effect-free
-- actions constructed by "pure" and "return".
-- 
-- For the axioms of ProvabilityLogic, for example, each rule writes its name.

instance Logic (Pair (NonEmpty w))
  where
    logic1 (Pair ws f) (Pair ws' x) = Pair (ws `nappend` ws') (f x)
    logic2 (Pair ws f) (Pair ws' g) = Pair (ws `nappend` ws') (g . f)
    logic3 (Pair ws f) (Pair ws' g) = Pair (ws `nappend` ws') (\x -> f x (g x))

instance ProvabilityLogic (Pair (NonEmpty Char))
                          (Pair (NonEmpty Char))
  where
    rule1 (Pair ws x) = Pair (ws `nappend` nString "Rule1") (Pair ws x)
    rule2 = writing "Rule2" go
      where
        go (Pair ws x) = Pair ws (Pair ws x)
    rule3 = writing "Rule3" go
      where
        go (Pair ws f) (Pair ws' x) = Pair (ws `nappend` ws') (f x)


-- We now need to find types "psi" and "a" which satisfy the fixed point laws.
-- User /u/want_to_want helpfully provided the following implementation:

data Fix t = MkFix (t (Fix t))
data PrePsi p a x = MkPrePsi (p x -> a)
type Psi p a = Fix (PrePsi p a)

psi1 :: Psi p a -> (p (Psi p a) -> a)
psi1 (MkFix (MkPrePsi f)) = f

psi2 :: (p (Psi p a) -> a) -> Psi p a
psi2 f = MkFix (MkPrePsi f)


-- Let's also have those laws write their names.

tPsi1 :: Pair NString (Psi p a -> (p (Psi p a) -> a))
tPsi1 = writing "Psi1" psi1

tPsi2 :: Pair NString ((p (Psi p a) -> a) -> Psi p a)
tPsi2 = writing "Psi2" psi2


-- Finally, we need to write an implementation of loeb's premise, "p a -> a".
-- Since a "Pair w a" contains an "a", it doesn't sound to hard...

premise0 :: Pair NString a -> a
premise0 (Pair _ x) = x

tPremise0 :: Pair NString (Pair NString a -> a)
tPremise0 = writing "Premise0" premise0


-- Unfortunately, that implementation causes loeb to loop forever :(

-- >>> loop
-- [loops forever]
loop :: Pair NString (Pair NString Int)
loop = loeb tPsi1 tPsi2 tPremise0


-- In retrospect, it shouldn't be too surprising that the implementation loops,
-- because the type of "loeb tPsi1 tPsi2 tPremise0" promises to be able to
-- produce a value of type "Pair NString (Pair NString a)" for any type "a",
-- including Void.

-- To avoid the infinite loop, we can give loeb the same kind of argument as
-- Dan gives in his post, namely an argument whose carefully-arranged
-- dependencies allows the argument to be defined in terms of itself.

premise :: Pair NString [Int] -> [Int]
premise (Pair _ xs) = [length xs, xs !! 0]

tPremise :: Pair NString (Pair NString [Int] -> [Int])
tPremise = writing "Premise" premise


-- When we call loeb with this argument, we get [2,2], just like in Dan's
-- post, plus a long sequence of rule names written by each rule as it got
-- applied by our proof.

-- |
-- >>> main
-- Pair (';',"Rule3;Psi1;Rule1;Rule3;Rule2;Premise;Psi2;Rule3;Psi1;Rule1;Rule3;Rule2;Premise;Rule1") [2,2]
main :: IO ()
main = print $ loeb tPsi1 tPsi2 tPremise


-- I hope that by picking other types for "t", "p", "psi" and "a", one might be
-- able to obtain something more useful. Until such a use is found, I would
-- stick with Dan's version, as it has a lot fewer premises and does basically
-- the same thing.