Morphism.hs revision b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58
f90884915ff10ae83f59e709c68824de834e64f5Dominik LueckeModule : $Header$
9eb6a481980d81a55898ba418fba72fc3c09d8c8Dominik LueckeDescription : Morphisms in Propositional logic
f90884915ff10ae83f59e709c68824de834e64f5Dominik LueckeCopyright : (c) Dominik Luecke, Uni Bremen 2007
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : luecke@informatik.uni-bremen.de
b72a390042c19e630cf221494b60c9df2a60d187Dominik LueckeStability : experimental
b72a390042c19e630cf221494b60c9df2a60d187Dominik LueckePortability : portable
f90884915ff10ae83f59e709c68824de834e64f5Dominik LueckeDefinition of morphisms for propositional logic
2af38fde95f93562f2124ec615fba0e509c8202eDominik Luecke Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
2af38fde95f93562f2124ec615fba0e509c8202eDominik Luecke What is a Logic?.
926b3c5491f1c608f5b79e2d8014d7a1385558c3Dominik Luecke In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder ( Morphism (..) -- datatype for Morphisms
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , pretty -- pretty printing
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , idMor -- identity morphism
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , isLegalMorphism -- check if morhpism is ok
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , composeMor -- composition
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , inclusionMap -- inclusion map
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , mapSentence -- map of sentences
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , mapSentenceH -- map of sentences, without Result type
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , applyMap -- application function for maps
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , applyMorphism -- application function for morphism
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder , morphismUnion
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Lueckeimport qualified Data.Map as Map
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Lueckeimport qualified Data.Set as Set
5b9f5c1b3592b99fc74d3438740ebcf9eb4c94beDominik Lueckeimport qualified Common.Result as Result
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik Lueckeimport qualified Propositional.AS_BASIC_Propositional as AS_BASIC
da955132262baab309a50fdffe228c9efe68251dCui Jian-- | The datatype for morphisms in propositional logic as
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder-- maps of sets
f90884915ff10ae83f59e709c68824de834e64f5Dominik Lueckedata Morphism = Morphism
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder { source :: Sign
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , target :: Sign
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , propMap :: Map.Map Id Id
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder } deriving (Eq, Ord, Show)
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Lueckeinstance Pretty Morphism where
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder pretty = printMorphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder-- | Constructs an id-morphism
b72a390042c19e630cf221494b60c9df2a60d187Dominik LueckeidMor :: Sign -> Morphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederidMor a = inclusionMap a a
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke-- | Determines whether a morphism is valid
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian MaederisLegalMorphism :: Morphism -> Result ()
da955132262baab309a50fdffe228c9efe68251dCui JianisLegalMorphism pmor =
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder let psource = items $ source pmor
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke ptarget = items $ target pmor
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke pdom = Map.keysSet $ propMap pmor
0b53895114b00141ec17ffdc7e26acded4487328Christian Maeder pcodom = Set.map (applyMorphism pmor) psource
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder in if Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder then return () else fail "illegal Propositional morphism"
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke-- | Application funtion for morphisms
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckeapplyMorphism :: Morphism -> Id -> Id
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckeapplyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke-- | Application function for propMaps
5b2e9f4673599e1bc6e18a43ad615da28305b8e1Christian MaederapplyMap :: Map.Map Id Id -> Id -> Id
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckeapplyMap pmap idt = Map.findWithDefault idt idt pmap
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke-- | Composition of morphisms in propositional Logic
08056875f5f633ef432598d5245ea41c112d2178Dominik LueckecomposeMor :: Morphism -> Morphism -> Result Morphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedercomposeMor f g =
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder let fSource = source f
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke gTarget = target g
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke fMap = propMap f
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke gMap = propMap g
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder in return Morphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder { source = fSource
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , target = gTarget
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , propMap = if Map.null gMap then fMap else
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder if i == j then id else Map.insert i j)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder Map.empty $ items fSource }
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke-- | Pretty printing for Morphisms
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik LueckeprintMorphism :: Morphism -> Doc
0859769b65851f4c06d6d32fac084b0f4db56c94Christian MaederprintMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
da955132262baab309a50fdffe228c9efe68251dCui Jian <> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke <> pretty y <> rparen) $ Map.assocs $ propMap m)
5b9f5c1b3592b99fc74d3438740ebcf9eb4c94beDominik Luecke-- | Inclusion map of a subsig into a supersig
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederinclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederinclusionMap s1 s2 = Morphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder { source = s1
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , target = s2
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik Luecke-- | sentence translation along signature morphism
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik Luecke-- here just the renaming of formulae
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik LueckemapSentence :: Morphism -> AS_BASIC.FORMULA -> Result.Result AS_BASIC.FORMULA
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedermapSentence mor = return . mapSentenceH mor
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik LueckemapSentenceH :: Morphism -> AS_BASIC.FORMULA -> AS_BASIC.FORMULA
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedermapSentenceH mor frm = case frm of
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder AS_BASIC.Negation form rn -> AS_BASIC.Negation (mapSentenceH mor form) rn
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder AS_BASIC.Conjunction (map (mapSentenceH mor) form) rn
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder AS_BASIC.Disjunction (map (mapSentenceH mor) form) rn
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder AS_BASIC.Implication form1 form2 rn -> AS_BASIC.Implication
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder (mapSentenceH mor form1) (mapSentenceH mor form2) rn
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder AS_BASIC.Equivalence form1 form2 rn -> AS_BASIC.Equivalence
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder (mapSentenceH mor form1) (mapSentenceH mor form2) rn
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder AS_BASIC.True_atom rn -> AS_BASIC.True_atom rn
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder AS_BASIC.False_atom rn -> AS_BASIC.False_atom rn
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder AS_BASIC.Predication predH -> AS_BASIC.Predication
0b53895114b00141ec17ffdc7e26acded4487328Christian Maeder $ id2SimpleId $ applyMorphism mor $ Id.simpleIdToId predH
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaedermorphismUnion :: Morphism -> Morphism -> Result.Result Morphism
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaedermorphismUnion mor1 mor2 =
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder let pmap1 = propMap mor1
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder pmap2 = propMap mor2
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder p1 = source mor1
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder p2 = source mor2
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder up1 = Set.difference (items p1) $ Map.keysSet pmap1
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder up2 = Set.difference (items p2) $ Map.keysSet pmap2
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder (pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder Nothing -> (ds, Map.insert i j m)
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder Just k -> if j == k then (ds, m) else
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder ("incompatible mapping of prop " ++ showId i " to "
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder ++ showId j " and " ++ showId k "")
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder nullRange : ds, m)) ([], pmap1)
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder (Map.toList pmap2 ++ map (\ a -> (a, a))
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder in if null pds then return Morphism
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder { source = unite p1 p2
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder , target = unite (target mor1) $ target mor2
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder , propMap = pmap } else Result pds Nothing