Copyright | (c) Till Mossakowski and Uni Bremen 2002-2006 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | till@informatik.uni-bremen.de |
Stability | provisional |
Portability | non-portable (overlapping instances, dynamics, existentials) |
Safe Haskell | None |
Logic.Grothendieck
Description
Grothendieck logic (flattening of logic graph to a single logic)
The Grothendieck logic is defined to be the heterogeneous logic over the logic graph. This will be the logic over which the data structures and algorithms for specification in-the-large are built.
This module heavily works with existential types, see http://haskell.org/hawiki/ExistentialTypes and chapter 7 of /Heterogeneous specification and the heterogeneous tool set/ (http://www.informatik.uni-bremen.de/~till/papers/habil.ps).
References:
R. Diaconescu: Grothendieck institutions J. applied categorical structures 10, 2002, p. 383-402.
T. Mossakowski: Comorphism-based Grothendieck institutions. In K. Diks, W. Rytter (Eds.), Mathematical foundations of computer science, LNCS 2420, pp. 593-604
T. Mossakowski: Heterogeneous specification and the heterogeneous tool set.
- data G_basic_spec = Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_basic_spec lid basic_spec
- data G_sign = Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_sign {
- gSignLogic :: lid
- gSign :: ExtSign sign symbol
- gSignSelfIdx :: SigId
- newtype SigId = SigId Int
- startSigId :: SigId
- isHomSubGsign :: G_sign -> G_sign -> Bool
- isSubGsign :: LogicGraph -> G_sign -> G_sign -> Bool
- logicOfGsign :: G_sign -> AnyLogic
- symsOfGsign :: G_sign -> Set G_symbol
- data G_symbolmap a = Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symbolmap lid (Map symbol a)
- data G_mapofsymbol a = Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_mapofsymbol lid (Map a symbol)
- data G_symbol = Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symbol lid symbol
- data G_symb_items_list = Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symb_items_list lid [symb_items]
- data G_symb_map_items_list = Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symb_map_items_list lid [symb_map_items]
- data G_sublogics = Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_sublogics lid sublogics
- isSublogic :: G_sublogics -> G_sublogics -> Bool
- isProperSublogic :: G_sublogics -> G_sublogics -> Bool
- joinSublogics :: G_sublogics -> G_sublogics -> Maybe G_sublogics
- data G_morphism = Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_morphism {
- gMorphismLogic :: lid
- gMorphism :: morphism
- gMorphismSelfIdx :: MorId
- newtype MorId = MorId Int
- startMorId :: MorId
- mkG_morphism :: forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree. Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> morphism -> G_morphism
- lessSublogicComor :: G_sublogics -> AnyComorphism -> Bool
- data LogicGraph = LogicGraph {
- logics :: Map String AnyLogic
- currentLogic :: String
- currentSyntax :: Maybe IRI
- currentSublogic :: Maybe G_sublogics
- currentTargetBase :: Maybe (LibName, String)
- sublogicBasedTheories :: Map AnyLogic SublogicBasedTheories
- comorphisms :: Map String AnyComorphism
- inclusions :: Map (String, String) AnyComorphism
- unions :: Map (String, String) (AnyComorphism, AnyComorphism)
- morphisms :: Map String AnyMorphism
- modifications :: Map String AnyModification
- squares :: Map (AnyComorphism, AnyComorphism) [Square]
- qTATranslations :: Map String AnyComorphism
- prefixes :: Map String IRI
- dolOnly :: Bool
- setCurLogic :: String -> LogicGraph -> LogicGraph
- setSyntax :: Maybe IRI -> LogicGraph -> LogicGraph
- setCurSublogic :: Maybe G_sublogics -> LogicGraph -> LogicGraph
- emptyLogicGraph :: LogicGraph
- lookupLogic :: Monad m => String -> String -> LogicGraph -> m AnyLogic
- lookupCurrentLogic :: Monad m => String -> LogicGraph -> m AnyLogic
- lookupCurrentSyntax :: Monad m => String -> LogicGraph -> m (AnyLogic, Maybe IRI)
- lookupCompComorphism :: Monad m => [String] -> LogicGraph -> m AnyComorphism
- lookupComorphism :: Monad m => String -> LogicGraph -> m AnyComorphism
- lookupModification :: Monad m => String -> LogicGraph -> m AnyModification
- data GMorphism = Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => GMorphism {
- gMorphismComor :: cid
- gMorphismSign :: ExtSign sign1 symbol1
- gMorphismSignIdx :: SigId
- gMorphismMor :: morphism2
- gMorphismMorIdx :: MorId
- isHomogeneous :: GMorphism -> Bool
- data Grothendieck = Grothendieck
- gEmbed :: G_morphism -> GMorphism
- gEmbed2 :: G_sign -> G_morphism -> GMorphism
- gEmbedComorphism :: AnyComorphism -> G_sign -> Result GMorphism
- homGsigDiff :: G_sign -> G_sign -> Result G_sign
- gsigUnion :: LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
- gsigManyUnion :: LogicGraph -> [G_sign] -> Result G_sign
- gsigManyIntersect :: LogicGraph -> [G_sign] -> Result G_sign
- homogeneousMorManyUnion :: [G_morphism] -> Result G_morphism
- logicInclusion :: LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
- logicUnion :: LogicGraph -> AnyLogic -> AnyLogic -> Result (AnyComorphism, AnyComorphism)
- updateMorIndex :: MorId -> GMorphism -> GMorphism
- toG_morphism :: GMorphism -> G_morphism
- gSigCoerce :: LogicGraph -> G_sign -> AnyLogic -> Result (G_sign, AnyComorphism)
- ginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism
- compInclusion :: LogicGraph -> GMorphism -> GMorphism -> Result GMorphism
- findComorphismPaths :: LogicGraph -> G_sublogics -> [AnyComorphism]
- logicGraph2Graph :: LogicGraph -> Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism
- findComorphism :: Monad m => G_sublogics -> [AnyComorphism] -> m AnyComorphism
- isTransportable :: GMorphism -> Bool
- data Square = Square {}
- data LaxTriangle = LaxTriangle {}
- mkIdSquare :: AnyLogic -> Square
- mkDefSquare :: AnyComorphism -> Square
- mirrorSquare :: Square -> Square
- lookupSquare :: AnyComorphism -> AnyComorphism -> LogicGraph -> Result [Square]
Documentation
data G_basic_spec Source #
Grothendieck basic specifications
Constructors
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_basic_spec lid basic_spec |
Instances
Grothendieck signatures with an lookup index. Zero indices indicate unknown ones. It would be nice to have special (may be negative) indices for empty signatures (one for every logic).
Constructors
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_sign | |
Fields
|
index for signatures
Constructors
SigId Int |
startSigId :: SigId Source #
isHomSubGsign :: G_sign -> G_sign -> Bool Source #
prefer a faster subsignature test if possible
isSubGsign :: LogicGraph -> G_sign -> G_sign -> Bool Source #
logicOfGsign :: G_sign -> AnyLogic Source #
symsOfGsign :: G_sign -> Set G_symbol Source #
data G_symbolmap a Source #
Grothendieck maps with symbol as keys
Constructors
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symbolmap lid (Map symbol a) |
Instances
(Typeable * a, Ord a) => Eq (G_symbolmap a) Source # | |
(Typeable * a, Ord a) => Ord (G_symbolmap a) Source # | |
Show a => Show (G_symbolmap a) Source # | |
(Ord a, ShATermLG a) => ShATermLG (G_symbolmap a) Source # | |
data G_mapofsymbol a Source #
Grothendieck maps with symbol as values
Constructors
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_mapofsymbol lid (Map a symbol) |
Instances
(Typeable * a, Ord a) => Eq (G_mapofsymbol a) Source # | |
(Typeable * a, Ord a) => Ord (G_mapofsymbol a) Source # | |
Show a => Show (G_mapofsymbol a) Source # | |
(Ord a, ShATermLG a) => ShATermLG (G_mapofsymbol a) Source # | |
Grothendieck symbols
data G_symb_items_list Source #
Grothendieck symbol lists
Constructors
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symb_items_list lid [symb_items] |
data G_symb_map_items_list Source #
Grothendieck symbol maps
Constructors
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symb_map_items_list lid [symb_map_items] |
data G_sublogics Source #
Grothendieck sublogics
Constructors
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_sublogics lid sublogics |
Instances
Eq G_sublogics Source # | |
Ord G_sublogics Source # | |
Show G_sublogics Source # | |
ShATermLG G_sublogics Source # | |
isSublogic :: G_sublogics -> G_sublogics -> Bool Source #
isProperSublogic :: G_sublogics -> G_sublogics -> Bool Source #
joinSublogics :: G_sublogics -> G_sublogics -> Maybe G_sublogics Source #
data G_morphism Source #
Homogeneous Grothendieck signature morphisms with indices. For the domain index it would be nice it showed also the emptiness.
Constructors
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_morphism | |
Fields
|
Instances
index for morphisms
Constructors
MorId Int |
startMorId :: MorId Source #
mkG_morphism :: forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree. Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> morphism -> G_morphism Source #
lessSublogicComor :: G_sublogics -> AnyComorphism -> Bool Source #
check if sublogic fits for comorphism
data LogicGraph Source #
Logic graph
Constructors
LogicGraph | |
Fields
|
Instances
Show LogicGraph Source # | |
Pretty LogicGraph Source # | |
setCurLogic :: String -> LogicGraph -> LogicGraph Source #
setSyntax :: Maybe IRI -> LogicGraph -> LogicGraph Source #
setCurSublogic :: Maybe G_sublogics -> LogicGraph -> LogicGraph Source #
lookupLogic :: Monad m => String -> String -> LogicGraph -> m AnyLogic Source #
find a logic in a logic graph
lookupCurrentLogic :: Monad m => String -> LogicGraph -> m AnyLogic Source #
lookupCurrentSyntax :: Monad m => String -> LogicGraph -> m (AnyLogic, Maybe IRI) Source #
lookupCompComorphism :: Monad m => [String] -> LogicGraph -> m AnyComorphism Source #
find a comorphism composition in a logic graph
lookupComorphism :: Monad m => String -> LogicGraph -> m AnyComorphism Source #
find a comorphism in a logic graph
lookupModification :: Monad m => String -> LogicGraph -> m AnyModification Source #
find a modification in a logic graph
Grothendieck signature morphisms with indices
Constructors
Comorphism cid lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => GMorphism | |
Fields
|
isHomogeneous :: GMorphism -> Bool Source #
gEmbed :: G_morphism -> GMorphism Source #
Embedding of homogeneous signature morphisms as Grothendieck sig mors
gEmbed2 :: G_sign -> G_morphism -> GMorphism Source #
Embedding of homogeneous signature morphisms as Grothendieck sig mors
gEmbedComorphism :: AnyComorphism -> G_sign -> Result GMorphism Source #
Embedding of comorphisms as Grothendieck sig mors
gsigUnion :: LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign Source #
heterogeneous union of two Grothendieck signatures
gsigManyUnion :: LogicGraph -> [G_sign] -> Result G_sign Source #
union of a list of Grothendieck signatures
gsigManyIntersect :: LogicGraph -> [G_sign] -> Result G_sign Source #
intersection of a list of Grothendieck signatures
homogeneousMorManyUnion :: [G_morphism] -> Result G_morphism Source #
homogeneous Union of a list of morphisms
logicInclusion :: LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism Source #
inclusion between two logics
logicUnion :: LogicGraph -> AnyLogic -> AnyLogic -> Result (AnyComorphism, AnyComorphism) Source #
union to two logics
toG_morphism :: GMorphism -> G_morphism Source #
gSigCoerce :: LogicGraph -> G_sign -> AnyLogic -> Result (G_sign, AnyComorphism) Source #
ginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism Source #
inclusion morphism between two Grothendieck signatures
compInclusion :: LogicGraph -> GMorphism -> GMorphism -> Result GMorphism Source #
Composition of two Grothendieck signature morphisms with intermediate inclusion
findComorphismPaths :: LogicGraph -> G_sublogics -> [AnyComorphism] Source #
Find all (composites of) comorphisms starting from a given logic
logicGraph2Graph :: LogicGraph -> Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism Source #
graph representation of the logic graph
findComorphism :: Monad m => G_sublogics -> [AnyComorphism] -> m AnyComorphism Source #
finds first comorphism with a matching sublogic
isTransportable :: GMorphism -> Bool Source #
check transportability of Grothendieck signature morphisms (currently returns false for heterogeneous morphisms)
Constructors
Square | |
Fields |
data LaxTriangle Source #
Constructors
LaxTriangle | |
Fields |
Instances
Eq LaxTriangle Source # | |
Ord LaxTriangle Source # | |
Show LaxTriangle Source # | |
mkIdSquare :: AnyLogic -> Square Source #
mkDefSquare :: AnyComorphism -> Square Source #
mirrorSquare :: Square -> Square Source #
lookupSquare :: AnyComorphism -> AnyComorphism -> LogicGraph -> Result [Square] Source #