Last active
July 6, 2017 13:39
-
-
Save gelisam/585fa054b56bb379e4b8 to your computer and use it in GitHub Desktop.
Encoding provability logic and Löb's theorem in Haskell.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- | 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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment