LogicRepr.hs revision 880b4b90f01052cddc0858548f5909db93057b62
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder-- needs ghc -fglasgow-exts -package data
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder Till Mossakowski, Christian Maeder
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maeder Provides data structures logic representations.
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder Logic representations are just collections of
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder functions between (some of) the types of logics.
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder References: see Logic.hs
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Weak amalgamability, also for reprs
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski reprs out of sublogic relationships
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedermodule LogicRepr where
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Maybe(catMaybes)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- Simple logic representations (possibly also morphisms via adjointness)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederdata (Logic lid1 sublogics1
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign1 morphism1 symbol1 raw_symbol1,
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Logic lid2 sublogics2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign2 morphism2 symbol2 raw_symbol2) =>
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder LogicRepr lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign1 morphism1 symbol1 raw_symbol1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign2 morphism2 symbol2 raw_symbol2
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder LogicRepr {repr_name :: String,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski source :: lid1, source_sublogic :: sublogics1,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski target :: lid2, target_sublogic :: sublogics2,
922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder -- the translation functions are partial
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder -- because the target may be a sublanguage
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -- map_basic_spec :: basic_spec1 -> Maybe basic_spec2,
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder map_sign :: sign1 -> Maybe (sign2,[sentence2]),
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder projection:: Maybe (-- the right adjoint functor Psi
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder sign2 -> sign1, morphism2 -> morphism1,
24a0fbb77b860bc28d25be37ba555fd5746cb6d6Christian Maeder -- the counit
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder sign2 -> morphism2,
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder -- basic_spec2 -> basic_spec1,
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder -- corresponding symbol translation
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder symbol2 -> Maybe symbol1),
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder map_morphism :: morphism1 -> Maybe morphism2,
63324a97283728a30932828a612c7b0b0f687624Christian Maeder map_sentence :: sign1 -> sentence1 -> Maybe sentence2,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- also covers semi-representations
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder -- with no sentence translation
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_symbol :: symbol1 -> Set symbol2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- codings may be more complex
53310804002cd9e3c9c5844db3b984abcf001788Christian Maederinstance (Logic lid1 sublogics1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid2 sublogics2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Eq (LogicRepr lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
3a87487c048b275c56e502c4a933273788e8d0bbChristian Maeder sign1 morphism1 symbol1 raw_symbol1
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu sign2 morphism2 symbol2 raw_symbol2)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski r1==r2 = repr_name r1 == repr_name r2 &&
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder language_name (source r1) == language_name (source r2) &&
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder language_name (target r1) == language_name (target r2) &&
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski coerce (source r1) (source r2) (source_sublogic r1) ==
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski Just (source_sublogic r2) &&
d97cb7d1c9beadc4d9102738da0a88c4efcf8fddChristian Maeder coerce (target r1) (target r2) (target_sublogic r1) ==
24a0fbb77b860bc28d25be37ba555fd5746cb6d6Christian Maeder Just (target_sublogic r2)
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder Logic lid sublogics
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder basic_spec sentence symb_items symb_map_items
bba825b39570777866d560bfde3807731131097eKlaus Luettich sign morphism symbol raw_symbol =>
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder LogicRepr lid sublogics basic_spec sentence symb_items symb_map_items
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder sign morphism symbol raw_symbol
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder lid sublogics basic_spec sentence symb_items symb_map_items
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder sign morphism symbol raw_symbol
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder LogicRepr {repr_name = "id_"++language_name lid,
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder source = lid, source_sublogic = top,
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder target = lid, target_sublogic = top,
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder map_sign = \sigma -> Just(sigma,[]),
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder projection= Just (-- the right adjoint functor Psi
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder -- the counit
3d86f079b07a6a058cdd6c112d287e01a69d9c0cChristian Maeder -- corresponding symbol translation
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder map_morphism = Just,
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder map_sentence = \sigma -> Just,
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder map_symbol = unitSet
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder-- composition of logic representations (diagrammatic order)
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder (Logic lid1 sublogics1
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder sign1 morphism1 symbol1 raw_symbol1,
63324a97283728a30932828a612c7b0b0f687624Christian Maeder Logic lid2 sublogics2
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu sign2 morphism2 symbol2 raw_symbol2,
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder Logic lid3 sublogics3
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder basic_spec3 sentence3 symb_items3 symb_map_items3
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder sign3 morphism3 symbol3 raw_symbol3
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder LogicRepr lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu sign1 morphism1 symbol1 raw_symbol1
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu sign2 morphism2 symbol2 raw_symbol2
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu -> LogicRepr lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski sign2 morphism2 symbol2 raw_symbol2
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder sign3 morphism3 symbol3 raw_symbol3
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder LogicRepr lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign1 morphism1 symbol1 raw_symbol1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign3 morphism3 symbol3 raw_symbol3 )
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maedercomp_repr r1 r2 = if target_sublogic r1 <= source_sublogic r2 then
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder Just(LogicRepr{
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder repr_name = repr_name r1++";"++repr_name r2,
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder source = source r1, target = target r2,
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder source_sublogic = source_sublogic r1,
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder target_sublogic = target_sublogic r2,
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder map_sentence =
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder do (si2,_) <- map_sign r1 si1
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder se2 <- map_sentence r1 si1 se1
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder map_sentence r2 si2 se2 ,
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder do (si2, se2s) <- map_sign r1 si1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (si3, se3s) <- map_sign r2 si2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder return (si3, se3s ++ catMaybes
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (map (map_sentence r2 si2) se2s)) ,
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder projection = undefined ,
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder map_morphism = \ m1 -> map_morphism r1 m1 >>= map_morphism r2 ,
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder map_symbol = \ s1 -> unionManySets
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (map (map_symbol r2) (setToList (map_symbol r1 s1)))
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder }) else Nothing