Morphism.hs revision da955132262baab309a50fdffe228c9efe68251d
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu{-# OPTIONS -fallow-undecidable-instances #-}
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu{- |
734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel ManceModule : $Header$
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae BungiuDescription : Morphisms in Propositional logic
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae BungiuCopyright : (c) Dominik Luecke, Uni Bremen 2007
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae BungiuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae BungiuMaintainer : luecke@informatik.uni-bremen.de
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae BungiuStability : experimental
c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel MancePortability : portable
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu
15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel ManceDefinition of morphisms for propositional logic
734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel Mance-}
c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mance{-
c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mance Ref.
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu What is a Logic?.
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
ed1b8e97e72b2e3e92edaf2eb22a4b5373d705f1Felix Gabriel Mance 2005.
5180a08007989fd364622fc9bc01f82141643f7bFelix Gabriel Mance-}
ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu
734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel Mancemodule Propositional.Morphism
c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mance (
0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Mance Morphism (..) -- datatype for Morphisms
0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Mance ,pretty -- pretty printing
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance ,idMor -- identity morphism
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance ,isLegalMorphism -- check if morhpism is ok
0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Mance ,composeMor -- composition
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance ,inclusionMap -- inclusion map
0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Mance ,mapSentence -- map of sentences
0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Mance ,applyMap -- application function for maps
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance ) where
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Manceimport qualified Data.Map as Map
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Manceimport qualified Data.Set as Set
dec48ce9576469185a15c3c58258032823a9c536Felix Gabriel Manceimport Propositional.Sign as Sign
0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Manceimport qualified Common.Result as Result
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Manceimport qualified Propositional.AS_BASIC_Propositional as AS_BASIC
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Manceimport Common.Id as Id
0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Manceimport Common.Result
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Manceimport Common.Doc
3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Manceimport Common.DocUtils
3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance
9c3f6477a95da46a907326206673b4a5c2164164Felix Gabriel Mance-- Maps are simple maps between elements of sets
3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance-- By the definition of maps in Data.Map
3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance-- these maps are injective
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mancetype PropMap = Map.Map Id Id
3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance
3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance-- | The datatype for morphisms in propositional logic as
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance-- | simple injective maps of sets
9c3f6477a95da46a907326206673b4a5c2164164Felix Gabriel Mance
316ef492799cd45fea0f5c26932f49adddfda3f7Felix Gabriel Mancedata Morphism = Morphism
3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance {
31a5ba51cd6d24e28a23abf64ce4043a45eabbefFelix Gabriel Mance source :: Sign
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance , target :: Sign
3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance , propMap :: PropMap
316ef492799cd45fea0f5c26932f49adddfda3f7Felix Gabriel Mance } deriving (Eq, Show)
316ef492799cd45fea0f5c26932f49adddfda3f7Felix Gabriel Mance
316ef492799cd45fea0f5c26932f49adddfda3f7Felix Gabriel Manceinstance Pretty Morphism where
316ef492799cd45fea0f5c26932f49adddfda3f7Felix Gabriel Mance pretty = printMorphism
31a5ba51cd6d24e28a23abf64ce4043a45eabbefFelix Gabriel Mance
0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Mance-- | Constructs an id-morphism as the diagonal
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance
734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel ManceidMor :: Sign -> Morphism
734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel ManceidMor a = Morphism
31a5ba51cd6d24e28a23abf64ce4043a45eabbefFelix Gabriel Mance { source = a
3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance , target = a
e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance , propMap = makeIdMor $ items a
15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance }
15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance where
c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance makeIdMor :: (Ord b) => Set.Set b -> Map.Map b b
dda7065c0c0f383558d7d4e8072969c8c41a8ed7Francisc Nicolae Bungiu makeIdMor b = Set.fold (\x -> Map.insert x x) Map.empty b
15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance
e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- | Determines whether a morphism is valid
e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceisLegalMorphism :: Morphism -> Bool
dda7065c0c0f383558d7d4e8072969c8c41a8ed7Francisc Nicolae BungiuisLegalMorphism pmor =
734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel Mance let
c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance psource = items $ source pmor
30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance ptarget = items $ target pmor
pdom = Map.keysSet $ propMap pmor
pcodom = Set.map (applyMorphism pmor) $ psource
in
Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource
-- | Application funtion for morphisms
applyMorphism :: Morphism -> Id -> Id
applyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
-- | Application function for propMaps
applyMap :: PropMap -> Id -> Id
applyMap pmap idt = Map.findWithDefault idt idt pmap
-- | Composition of morphisms in propositional Logic
composeMor :: Morphism -> Morphism -> Result Morphism
composeMor f g
| fTarget /= gSource = fail "Morphisms are not composable"
| otherwise = 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
}
where
fSource = source f
fTarget = target f
gSource = source g
gTarget = target g
fMap = propMap f
gMap = propMap g
-- | 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 -> Result Morphism
inclusionMap s1 s2
|isSub = Result.Result
{
diags = [Diag
{
Result.diagKind = Result.Debug
, Result.diagString = "All fine"
, diagPos = Id.nullRange
}]
, maybeResult = Just $ Morphism
{
source = s1
, target = s2
, propMap = Set.fold (\x -> Map.insert x x)
Map.empty (Sign.items s1)
}
}
| otherwise = Result.Result
{
diags = [Diag
{
Result.diagKind = Result.Error
, Result.diagString = errorStr
, diagPos = Id.nullRange
}]
, maybeResult = Nothing
}
where
isSub = Sign.isSubSigOf s1 s2
errorStr = (show $ pretty s1) ++ " is not subset of " ++ (show $ pretty s2)
-- | gets simple Id
getSimpleId :: Id.Id -> [Id.Token]
getSimpleId (Id toks _ _) = toks
-- | sentence translation along signature morphism
-- here just the renaming of formulae
mapSentence :: Morphism -> AS_BASIC.FORMULA -> Result.Result AS_BASIC.FORMULA
mapSentence mor form = Result.Result
{
diags = [Diag
{
Result.diagKind = Result.Debug
, Result.diagString = "All fine mapSentence"
, diagPos = Id.nullRange
}]
, maybeResult = Just $ mapSentenceH mor form
}
mapSentenceH :: Morphism -> AS_BASIC.FORMULA -> AS_BASIC.FORMULA
mapSentenceH mor (AS_BASIC.Negation form rn) = AS_BASIC.Negation (mapSentenceH mor form) rn
mapSentenceH mor (AS_BASIC.Conjunction form rn) = AS_BASIC.Conjunction (map (mapSentenceH mor) form) rn
mapSentenceH mor (AS_BASIC.Disjunction form rn) = AS_BASIC.Disjunction (map (mapSentenceH mor) form) rn
mapSentenceH mor (AS_BASIC.Implication form1 form2 rn) = AS_BASIC.Implication (mapSentenceH mor form1)
(mapSentenceH mor form2) rn
mapSentenceH mor (AS_BASIC.Equivalence form1 form2 rn) = AS_BASIC.Equivalence (mapSentenceH mor form1)
(mapSentenceH mor form2) rn
mapSentenceH _ (AS_BASIC.True_atom rn) = AS_BASIC.True_atom rn
mapSentenceH _ (AS_BASIC.False_atom rn) = AS_BASIC.False_atom rn
mapSentenceH mor (AS_BASIC.Predication predH) = AS_BASIC.Predication (head $ getSimpleId $
(applyMorphism mor $ Id.simpleIdToId predH))