Morphism.hs revision e7cd36335f0f7be9ed5005e71d94c2856b588d62
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherModule : $Header$
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherDescription : Morphisms in Propositional logic
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherCopyright : (c) Dominik Luecke, Uni Bremen 2007
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherLicense : GPLv2 or higher, see LICENSE.txt
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherMaintainer : luecke@informatik.uni-bremen.de
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherStability : experimental
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherPortability : portable
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherDefinition of morphisms for propositional logic
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher What is a Logic?.
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher ( Morphism (..) -- datatype for Morphisms
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , pretty -- pretty printing
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce , idMor -- identity morphism
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce , isLegalMorphism -- check if morhpism is ok
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce , composeMor -- composition
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , inclusionMap -- inclusion map
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , mapSentence -- map of sentences
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , mapSentenceH -- map of sentences, without Result type
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , applyMap -- application function for maps
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , applyMorphism -- application function for morphism
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , morphismUnion
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherimport qualified Data.Map as Map
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherimport qualified Data.Set as Set
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherimport qualified Common.Result as Result
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashovimport qualified Propositional.AS_BASIC_Propositional as AS_BASIC
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | The datatype for morphisms in propositional logic as
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- maps of sets
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherdata Morphism = Morphism
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher { source :: Sign
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , target :: Sign
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce , propMap :: Map.Map Id Id
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher } deriving (Eq, Ord, Show)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherinstance Pretty Morphism where
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher pretty = printMorphism
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Constructs an id-morphism
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagheridMor :: Sign -> Morphism
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagheridMor a = inclusionMap a a
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov-- | Determines whether a morphism is valid
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherisLegalMorphism :: Morphism -> Result ()
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherisLegalMorphism pmor =
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher let psource = items $ source pmor
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov ptarget = items $ target pmor
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher pdom = Map.keysSet $ propMap pmor
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher pcodom = Set.map (applyMorphism pmor) psource
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher in if Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher then return () else fail "illegal Propositional morphism"
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Application funtion for morphisms
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai KondrashovapplyMorphism :: Morphism -> Id -> Id
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherapplyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Application function for propMaps
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai KondrashovapplyMap :: Map.Map Id Id -> Id -> Id
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherapplyMap pmap idt = Map.findWithDefault idt idt pmap
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Composition of morphisms in propositional Logic
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai KondrashovcomposeMor :: Morphism -> Morphism -> Result Morphism
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghercomposeMor f g =
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher let fSource = source f
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher gTarget = target g
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher fMap = propMap f
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher gMap = propMap g
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher in return Morphism
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher { source = fSource
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , target = gTarget
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , propMap = if Map.null gMap then fMap else
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher if i == j then id else Map.insert i j)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Map.empty $ items fSource }
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Pretty printing for Morphisms
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherprintMorphism :: Morphism -> Doc
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherprintMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher <> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher <> pretty y <> rparen) $ Map.assocs $ propMap m)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | Inclusion map of a subsig into a supersig
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherinclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherinclusionMap s1 s2 = Morphism
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | sentence translation along signature morphism
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- here just the renaming of formulae
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghermapSentence :: Morphism -> AS_BASIC.FORMULA -> Result.Result AS_BASIC.FORMULA
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghermapSentence mor = return . mapSentenceH mor
21d485184df986e1a123f70c689517386e51a5ceMichal ZidekmapSentenceH :: Morphism -> AS_BASIC.FORMULA -> AS_BASIC.FORMULA
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai KondrashovmapSentenceH mor frm = case frm of
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek AS_BASIC.Negation form rn -> AS_BASIC.Negation (mapSentenceH mor form) rn
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher AS_BASIC.Conjunction (map (mapSentenceH mor) form) rn
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher AS_BASIC.Disjunction (map (mapSentenceH mor) form) rn
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce AS_BASIC.Implication form1 form2 rn -> AS_BASIC.Implication
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce (mapSentenceH mor form1) (mapSentenceH mor form2) rn
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher AS_BASIC.Equivalence form1 form2 rn -> AS_BASIC.Equivalence
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov (mapSentenceH mor form1) (mapSentenceH mor form2) rn
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov AS_BASIC.True_atom rn -> AS_BASIC.True_atom rn
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher AS_BASIC.False_atom rn -> AS_BASIC.False_atom rn
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher AS_BASIC.Predication predH -> AS_BASIC.Predication
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher $ id2SimpleId $ applyMorphism mor $ Id.simpleIdToId predH
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghermorphismUnion :: Morphism -> Morphism -> Result.Result Morphism
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo SorcemorphismUnion mor1 mor2 =
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce let pmap1 = propMap mor1
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher pmap2 = propMap mor2
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov p1 = source mor1
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov p2 = source mor2
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher up1 = Set.difference (items p1) $ Map.keysSet pmap1
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher up2 = Set.difference (items p2) $ Map.keysSet pmap2
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher (pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Nothing -> (ds, Map.insert i j m)
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce Just k -> if j == k then (ds, m) else
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov ("incompatible mapping of prop " ++ showId i " to "
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek ++ showId j " and " ++ showId k "")
21d485184df986e1a123f70c689517386e51a5ceMichal Zidek nullRange : ds, m)) ([], pmap1)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher (Map.toList pmap2 ++ map (\ a -> (a, a))
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher in if null pds then return Morphism
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher { source = unite p1 p2
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce , target = unite (target mor1) $ target mor2
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , propMap = pmap } else Result pds Nothing