Morphism.hs revision 1a38107941725211e7c3f051f7a8f5e12199f03a
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh{-# LANGUAGE DeriveDataTypeable #-}
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh{- |
4a13940dc2990df0a798718d3a3f9cf1566c2217bjhModule : $Header$
4a13940dc2990df0a798718d3a3f9cf1566c2217bjhDescription : Morphisms in Propositional logic
4a13940dc2990df0a798718d3a3f9cf1566c2217bjhCopyright : (c) Dominik Luecke, Uni Bremen 2007
4a13940dc2990df0a798718d3a3f9cf1566c2217bjhLicense : GPLv2 or higher, see LICENSE.txt
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh
4a13940dc2990df0a798718d3a3f9cf1566c2217bjhMaintainer : luecke@informatik.uni-bremen.de
4a13940dc2990df0a798718d3a3f9cf1566c2217bjhStability : experimental
4a13940dc2990df0a798718d3a3f9cf1566c2217bjhPortability : portable
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh Definition of morphisms for propositional logic
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh copied to "Temporal.Morphism"
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh Ref.
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh What is a Logic?.
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh 2005.
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh-}
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh
4a13940dc2990df0a798718d3a3f9cf1566c2217bjhmodule Propositional.Morphism
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh ( Morphism (..) -- datatype for Morphisms
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh , pretty -- pretty printing
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh , idMor -- identity morphism
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh , isLegalMorphism -- check if morhpism is ok
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh , composeMor -- composition
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh , inclusionMap -- inclusion map
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh , mapSentence -- map of sentences
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh , mapSentenceH -- map of sentences, without Result type
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh , applyMap -- application function for maps
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh , applyMorphism -- application function for morphism
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh , morphismUnion
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh ) where
4a13940dc2990df0a798718d3a3f9cf1566c2217bjh
4a13940dc2990df0a798718d3a3f9cf1566c2217bjhimport Data.Data
4a13940dc2990df0a798718d3a3f9cf1566c2217bjhimport qualified Data.Map as Map
4a13940dc2990df0a798718d3a3f9cf1566c2217bjhimport qualified Data.Set as Set
import Propositional.Sign as Sign
import qualified Propositional.AS_BASIC_Propositional as AS_BASIC
import Common.Id as Id
import Common.Result
import Common.Doc
import Common.DocUtils
import qualified Common.Result as Result
import Control.Monad (unless)
{- | The datatype for morphisms in propositional logic as
maps of sets -}
data Morphism = Morphism
{ source :: Sign
, target :: Sign
, propMap :: Map.Map Id Id
} deriving (Show, Eq, Ord, Typeable, Data)
instance Pretty Morphism where
pretty = printMorphism
-- | Constructs an id-morphism
idMor :: Sign -> Morphism
idMor a = inclusionMap a a
-- | Determines whether a morphism is valid
isLegalMorphism :: Morphism -> Result ()
isLegalMorphism pmor =
let psource = items $ source pmor
ptarget = items $ target pmor
pdom = Map.keysSet $ propMap pmor
pcodom = Set.map (applyMorphism pmor) psource
in unless (Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource) $
fail "illegal Propositional morphism"
-- | Application funtion for morphisms
applyMorphism :: Morphism -> Id -> Id
applyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
-- | Application function for propMaps
applyMap :: Map.Map Id Id -> Id -> Id
applyMap pmap idt = Map.findWithDefault idt idt pmap
-- | Composition of morphisms in propositional Logic
composeMor :: Morphism -> Morphism -> Result Morphism
composeMor f g =
let fSource = source f
gTarget = target g
fMap = propMap f
gMap = propMap g
in return Morphism
{ source = fSource
, target = gTarget
, propMap = if Map.null gMap then fMap else
Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
if i == j then id else Map.insert i j)
Map.empty $ items fSource }
-- | Pretty printing for Morphisms
printMorphism :: Morphism -> Doc
printMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
<> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
<> pretty y <> rparen) $ Map.assocs $ propMap m)
-- | Inclusion map of a subsig into a supersig
inclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
inclusionMap s1 s2 = Morphism
{ source = s1
, target = s2
, propMap = Map.empty }
{- | sentence translation along signature morphism
here just the renaming of formulae -}
mapSentence :: Morphism -> AS_BASIC.FORMULA -> Result.Result AS_BASIC.FORMULA
mapSentence mor = return . mapSentenceH mor
mapSentenceH :: Morphism -> AS_BASIC.FORMULA -> AS_BASIC.FORMULA
mapSentenceH mor frm = case frm of
AS_BASIC.Negation form rn -> AS_BASIC.Negation (mapSentenceH mor form) rn
AS_BASIC.Conjunction form rn ->
AS_BASIC.Conjunction (map (mapSentenceH mor) form) rn
AS_BASIC.Disjunction form rn ->
AS_BASIC.Disjunction (map (mapSentenceH mor) form) rn
AS_BASIC.Implication form1 form2 rn -> AS_BASIC.Implication
(mapSentenceH mor form1) (mapSentenceH mor form2) rn
AS_BASIC.Equivalence form1 form2 rn -> AS_BASIC.Equivalence
(mapSentenceH mor form1) (mapSentenceH mor form2) rn
AS_BASIC.True_atom rn -> AS_BASIC.True_atom rn
AS_BASIC.False_atom rn -> AS_BASIC.False_atom rn
AS_BASIC.Predication predH -> AS_BASIC.Predication
$ id2SimpleId $ applyMorphism mor $ Id.simpleIdToId predH
morphismUnion :: Morphism -> Morphism -> Result.Result Morphism
morphismUnion mor1 mor2 =
let pmap1 = propMap mor1
pmap2 = propMap mor2
p1 = source mor1
p2 = source mor2
up1 = Set.difference (items p1) $ Map.keysSet pmap1
up2 = Set.difference (items p2) $ Map.keysSet pmap2
(pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
Nothing -> (ds, Map.insert i j m)
Just k -> if j == k then (ds, m) else
(Diag Error
("incompatible mapping of prop " ++ showId i " to "
++ showId j " and " ++ showId k "")
nullRange : ds, m)) ([], pmap1)
(Map.toList pmap2 ++ map (\ a -> (a, a))
(Set.toList $ Set.union up1 up2))
in if null pds then return Morphism
{ source = unite p1 p2
, target = unite (target mor1) $ target mor2
, propMap = pmap } else Result pds Nothing