Skip to content

Commit a14056d

Browse files
milesroutmilesrout
committed
Free monad approach
1 parent 4a0cae9 commit a14056d

File tree

4 files changed

+166
-86
lines changed

4 files changed

+166
-86
lines changed

‎app/NewMain.hs‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
module Equivalences where
2+
3+
import Control.Monad
4+
import Data.List
5+
import qualified Data.Set as Set
6+
import Data.Set (Set)
7+
8+
import Minimal
9+
import Model
10+
11+
--doubleNegElim :: Deduction -> Proof
12+
--doubleNegElim dNNP = case conclusion dNNP of
13+
-- (Not (Not f)) -> return $ Deduction assumps f
14+
-- where assumps = aDNE `Set.insert` assumptions dNNP
15+
-- aDNE = Not (Not f) #> f
16+
-- _ -> throwError "DNE must only be applied to double negations"
17+
--
18+
--phi :: Formula
19+
--phi = Proposition "phi"
20+
--
21+
--dneImplAristotle :: Deduction
22+
--dneImplAristotle = evalProof $ do
23+
-- d1 <- assume (Not phi)
24+
-- d2 <- implIntro phi d1
25+
-- d3 <- assume (Not (phi #> Not phi))
26+
-- d4 <- implElim d2 d3
27+
-- d5 <- implIntro (Not phi) d4
28+
-- d6 <- doubleNegElim d5
29+
-- d7 <- implIntro (Not (phi #> Not phi)) d6
30+
-- return d7
31+
--
32+
--aristotleImplDne :: Deduction
33+
--aristotleImplDne = evalProof $ do
34+
-- d1 <- assume phi
35+
-- d2 <- assume (phi #> Not phi)
36+
-- d3 <- implElim d1 d2
37+
-- d4 <- assume (Not (Not phi))
38+
-- d5 <- implElim d3 d4
39+
-- d6 <- implIntro phi d5
40+
-- d7 <- implElim d6 d4
41+
-- d8 <- implIntro (phi #> Not phi) d7
42+
-- d9 <- assume (Not (phi #> Not phi) #> phi)
43+
-- d10 <- implElim d8 d9
44+
-- d11 <- implIntro (Not (Not phi)) d10
45+
-- return d11
46+
47+
main :: IO ()
48+
main = putStrLn "Hello, world!"

‎minimal-logic.cabal‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,12 @@ library
1818
, containers
1919
, mtl
2020
, pipes
21+
, free
2122
default-language: Haskell2010
2223

2324
executable minimal-logic-exe
2425
hs-source-dirs: app
25-
main-is: Equivalences.hs
26+
main-is: NewMain.hs
2627
ghc-options: -threaded -rtsopts -with-rtsopts=-N
2728
build-depends: base
2829
, containers

‎src/Minimal.hs‎

Lines changed: 48 additions & 85 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,24 @@
11
{-# LANGUAGE ViewPatterns, PatternSynonyms #-}
2-
3-
module Minimal (
4-
Formula(..),
5-
(#&), (#|), (#>),
6-
bot,
7-
pattern Bottom,
8-
pattern Not,
9-
Deduction(..),
10-
Proof(..),
11-
runProof, evalProof, throwError,
12-
assume,
13-
implIntro, implElim,
14-
conjIntro, leftConjElim, rightConjElim,
15-
disjElim, leftDisjIntro, rightDisjIntro,
16-
) where
2+
{-# LANGUAGE DeriveFunctor #-}
3+
4+
module Minimal where
5+
--module Minimal (
6+
-- Formula(..),
7+
-- (#&), (#|), (#>),
8+
-- bot,
9+
-- pattern Bottom,
10+
-- pattern Not,
11+
-- Deduction(..),
12+
-- Proof(..),
13+
-- runProof, evalProof, throwError,
14+
-- assume,
15+
-- implIntro, implElim,
16+
-- conjIntro, leftConjElim, rightConjElim,
17+
-- disjElim, leftDisjIntro, rightDisjIntro,
18+
-- ) where
1719

1820
import Control.Monad.Except
21+
import Control.Monad.Free
1922
import Data.Set (Set, (\\))
2023
import qualified Data.Set as Set
2124
import Text.Printf (printf)
@@ -52,73 +55,33 @@ instance Show Formula where
5255
show (Disjunction a b) = printf "(%s \x2228 %s)" (show a) (show b)
5356
show (Implication a b) = printf "(%s \x2192 %s)" (show a) (show b)
5457

55-
data Deduction = Deduction { assumptions :: Set Formula
56-
, conclusion :: Formula
57-
} deriving (Show)
58-
59-
-- Except is like Either (sum type) but explicitly for representing errors.
60-
type Proof = Except String Deduction
61-
62-
runProof :: Proof -> Either String Deduction
63-
runProof = runExcept
64-
65-
evalProof :: Proof -> Deduction
66-
evalProof p = case runProof p of
67-
(Right d) -> d
68-
_ -> error "evalProof run on invalid Proof"
69-
70-
-- The quoted versions of these functions are ones that can't fail, so return
71-
-- Deduction instead of Proof. Unquoted versions are defined below that return
72-
-- a Proof for consistency.
73-
74-
assume :: Formula -> Proof
75-
assume f = return (Deduction (Set.singleton f) f)
76-
77-
implIntro :: Formula -> Deduction -> Proof
78-
implIntro f d = return (Deduction (Set.delete f a) (f #> c))
79-
where a = assumptions d
80-
c = conclusion d
81-
82-
implElim :: Deduction -> Deduction -> Proof
83-
implElim (Deduction aA a') (Deduction aAtoB (Implication a b))
84-
| (a' == a) = return (Deduction (Set.union aA aAtoB) b)
85-
| otherwise = throwError "conclusion of first argument must be the antecedent of the conclusion of the second argument"
86-
implElim _ _ = throwError "second argument to implElim must be an implication"
87-
88-
conjIntro :: Deduction -> Deduction -> Proof
89-
conjIntro l r = return (Deduction (Set.union al ar) (cl #& cr))
90-
where al = assumptions l
91-
ar = assumptions r
92-
cl = conclusion l
93-
cr = conclusion r
94-
95-
leftDisjIntro :: Formula -> Deduction -> Proof
96-
leftDisjIntro f d = return (Deduction (assumptions d) (f #| r))
97-
where r = conclusion d
98-
99-
rightDisjIntro :: Deduction -> Formula -> Proof
100-
rightDisjIntro d f = return (Deduction (assumptions d) (l #| f))
101-
where l = conclusion d
102-
103-
leftConjElim :: Deduction -> Proof
104-
leftConjElim d = case (conclusion d) of
105-
(Conjunction _ r) -> return d { conclusion = r }
106-
_ -> throwError "argument must be a conjunction"
107-
108-
rightConjElim :: Deduction -> Proof
109-
rightConjElim d = case (conclusion d) of
110-
(Conjunction l _) -> return d { conclusion = l }
111-
_ -> throwError "argument must be a conjunction"
112-
113-
disjElim :: Deduction -> Deduction -> Deduction -> Proof
114-
-- matches if the conclusion of the first argument is a disjunction.
115-
-- then binds the whole deduction to `aOrB'.
116-
disjElim aOrB@(conclusion -> (Disjunction a b)) aToC bToC
117-
| conclusion aToC == conclusion bToC = return (Deduction assums conc)
118-
| otherwise = throwError "conclusion of second arg and conclusion of third arg must be equal"
119-
where aAorB = assumptions aOrB
120-
aAtoC = a `Set.delete` assumptions aToC
121-
aBtoC = b `Set.delete` assumptions bToC
122-
assums = Set.unions [aAorB, aAtoC, aBtoC]
123-
conc = conclusion aToC
124-
disjElim _ _ _ = throwError "conclusion of first arg must be a disjunction"
58+
data Proof = Proof { assumptions :: Set Formula
59+
, conclusion :: Formula
60+
} deriving (Show)
61+
62+
data DeductionF next
63+
= Assume Formula (Proof -> next)
64+
| ImplElim Proof Proof (Proof -> next)
65+
| ImplIntro Formula Proof (Proof -> next)
66+
deriving (Functor)
67+
68+
type Deduction = Free DeductionF
69+
70+
assume :: Formula -> Deduction Proof
71+
assume f = liftF (Assume f id)
72+
73+
implElim :: Proof -> Proof -> Deduction Proof
74+
implElim maj min = liftF (ImplElim maj min id)
75+
76+
implIntro :: Formula -> Proof -> Deduction Proof
77+
implIntro f prem = liftF (ImplIntro f prem id)
78+
79+
blah :: Deduction Proof
80+
blah = do
81+
dA <- assume (Proposition "A")
82+
dNA <- assume (Not (Proposition "A"))
83+
dB <- implElim dNA dA
84+
implIntro (Not (Proposition "A")) dB
85+
86+
showDeduction :: (Show a, Show r) => Free (DeductionF a) r -> String
87+
showDeduction (Free (Assume f x)) = printf "assume %s\n %s"

‎src/OldMinimal.hs‎

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
2+
3+
-- -- Except is like Either (sum type) but explicitly for representing errors.
4+
-- type Proof = Except String Deduction
5+
--
6+
-- runProof :: Proof -> Either String Deduction
7+
-- runProof = runExcept
8+
--
9+
-- evalProof :: Proof -> Deduction
10+
-- evalProof p = case runProof p of
11+
-- (Right d) -> d
12+
-- _ -> error "evalProof run on invalid Proof"
13+
--
14+
-- -- The quoted versions of these functions are ones that can't fail, so return
15+
-- -- Deduction instead of Proof. Unquoted versions are defined below that return
16+
-- -- a Proof for consistency.
17+
--
18+
-- assume :: Formula -> Proof
19+
-- assume f = return (Deduction (Set.singleton f) f)
20+
--
21+
-- implIntro :: Formula -> Deduction -> Proof
22+
-- implIntro f d = return (Deduction (Set.delete f a) (f #> c))
23+
-- where a = assumptions d
24+
-- c = conclusion d
25+
--
26+
-- implElim :: Deduction -> Deduction -> Proof
27+
-- implElim (Deduction aA a') (Deduction aAtoB (Implication a b))
28+
-- | (a' == a) = return (Deduction (Set.union aA aAtoB) b)
29+
-- | otherwise = throwError "conclusion of first argument must be the antecedent of the conclusion of the second argument"
30+
-- implElim _ _ = throwError "second argument to implElim must be an implication"
31+
--
32+
-- conjIntro :: Deduction -> Deduction -> Proof
33+
-- conjIntro l r = return (Deduction (Set.union al ar) (cl #& cr))
34+
-- where al = assumptions l
35+
-- ar = assumptions r
36+
-- cl = conclusion l
37+
-- cr = conclusion r
38+
--
39+
-- leftDisjIntro :: Formula -> Deduction -> Proof
40+
-- leftDisjIntro f d = return (Deduction (assumptions d) (f #| r))
41+
-- where r = conclusion d
42+
--
43+
-- rightDisjIntro :: Deduction -> Formula -> Proof
44+
-- rightDisjIntro d f = return (Deduction (assumptions d) (l #| f))
45+
-- where l = conclusion d
46+
--
47+
-- leftConjElim :: Deduction -> Proof
48+
-- leftConjElim d = case (conclusion d) of
49+
-- (Conjunction _ r) -> return d { conclusion = r }
50+
-- _ -> throwError "argument must be a conjunction"
51+
--
52+
-- rightConjElim :: Deduction -> Proof
53+
-- rightConjElim d = case (conclusion d) of
54+
-- (Conjunction l _) -> return d { conclusion = l }
55+
-- _ -> throwError "argument must be a conjunction"
56+
--
57+
-- disjElim :: Deduction -> Deduction -> Deduction -> Proof
58+
-- -- matches if the conclusion of the first argument is a disjunction.
59+
-- -- then binds the whole deduction to `aOrB'.
60+
-- disjElim aOrB@(conclusion -> (Disjunction a b)) aToC bToC
61+
-- | conclusion aToC == conclusion bToC = return (Deduction assums conc)
62+
-- | otherwise = throwError "conclusion of second arg and conclusion of third arg must be equal"
63+
-- where aAorB = assumptions aOrB
64+
-- aAtoC = a `Set.delete` assumptions aToC
65+
-- aBtoC = b `Set.delete` assumptions bToC
66+
-- assums = Set.unions [aAorB, aAtoC, aBtoC]
67+
-- conc = conclusion aToC
68+
-- disjElim _ _ _ = throwError "conclusion of first arg must be a disjunction"

0 commit comments

Comments
 (0)