hets -- a heterogenous Specification (CASL) tool setContentsIndex
Logic.Grothendieck
Portability non-portable (overlapping instances, dynamics, existentials)
Stability provisional
Maintainer till@tzi.de
Description

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.

References:

R. Diaconescu: Grothendieck institutions J. applied categorical structures 10, 2002, p. 383-402.

T. Mossakowski: Heterogeneous development graphs and heterogeneous borrowing Fossacs 2002, LNCS 2303, p. 326-341

T. Mossakowski: Foundations of heterogeneous specification Submitted

T. Mossakowski: Relating CASL with Other Specification Languages: the Institution Level Theoretical Computer Science 286, 2002, p. 367-475

Todo:

Synopsis
data G_basic_spec = 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 => G_basic_spec lid basic_spec
data G_sentence = 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 => G_sentence lid sentence
data G_l_sentence_list = 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 => G_l_sentence lid [Named sentence]
data G_sign = 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 => G_sign lid sign
tyconG_sign :: TyCon
langNameSig :: G_sign -> String
data G_sign_list = 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 => G_sign_list lid [sign]
data G_ext_sign = 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 => G_ext_sign lid sign (Set symbol)
tyconG_ext_sign :: TyCon
langNameExtSig :: G_ext_sign -> String
data G_symbol = 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 => G_symbol lid symbol
data G_symb_items_list = 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 => G_symb_items_list lid [symb_items]
data G_symb_map_items_list = 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 => G_symb_map_items_list lid [symb_map_items]
data G_diagram = 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 => G_diagram lid (Diagram sign morphism)
data G_sublogics = 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 => G_sublogics lid sublogics
data G_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 => G_morphism lid morphism
data AnyComorphism = forall 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 . 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 => Comorphism cid
compComorphism :: AnyComorphism -> AnyComorphism -> Result AnyComorphism
data LogicGraph = LogicGraph {
logics :: (Map String AnyLogic)
comorphisms :: (Map String AnyComorphism)
inclusions :: (Map (String, String) AnyComorphism)
}
lookupLogic :: String -> String -> LogicGraph -> AnyLogic
lookupComorphism :: String -> LogicGraph -> Result AnyComorphism
data AnyComorphismAux 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 = forall cid . 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 => ComorphismAux cid lid1 lid2 sign1 morphism2
tyconAnyComorphismAux :: TyCon
data GMorphism = forall 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 . 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 cid sign1 morphism2
data Grothendieck = Grothendieck
gEmbed :: G_morphism -> GMorphism
gsigLeftUnion :: LogicGraph -> Pos -> G_sign -> G_sign -> Result G_sign
homogeneousGsigUnion :: Pos -> G_sign -> G_sign -> Result G_sign
homogeneousGsigManyUnion :: Pos -> [G_sign] -> Result G_sign
homogeneousMorManyUnion :: Pos -> [G_morphism] -> Result G_morphism
ginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism
Documentation
data G_basic_spec
Grothendieck basic specifications
Constructors
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 => G_basic_spec lid basic_spec
Instances
ATermConvertible G_basic_spec
Show G_basic_spec
PrettyPrint G_basic_spec
data G_sentence
Grothendieck sentences
Constructors
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 => G_sentence lid sentence
Instances
ATermConvertible G_sentence
Show G_sentence
data G_l_sentence_list
Grothendieck sentence lists
Constructors
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 => G_l_sentence lid [Named sentence]
Instances
ATermConvertible G_l_sentence_list
Show G_l_sentence_list
Eq G_l_sentence_list
data G_sign
Grothendieck signatures
Constructors
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 => G_sign lid sign
Instances
ATermConvertible G_sign
Typeable G_sign
Eq G_sign
Show G_sign
PrettyPrint G_sign
Category Grothendieck G_sign GMorphism
tyconG_sign :: TyCon
langNameSig :: G_sign -> String
data G_sign_list
Grothendieck signature lists
Constructors
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 => G_sign_list lid [sign]
Instances
ATermConvertible G_sign_list
data G_ext_sign
Grothendieck extended signatures
Constructors
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 => G_ext_sign lid sign (Set symbol)
Instances
ATermConvertible G_ext_sign
Typeable G_ext_sign
Eq G_ext_sign
Show G_ext_sign
PrettyPrint G_ext_sign
tyconG_ext_sign :: TyCon
langNameExtSig :: G_ext_sign -> String
data G_symbol
Grothendieck symbols
Constructors
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 => G_symbol lid symbol
Instances
ATermConvertible G_symbol
Show G_symbol
Eq G_symbol
data G_symb_items_list
Grothendieck symbol lists
Constructors
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 => G_symb_items_list lid [symb_items]
Instances
ATermConvertible G_symb_items_list
Show G_symb_items_list
PrettyPrint G_symb_items_list
Eq G_symb_items_list
data G_symb_map_items_list
Grothendieck symbol maps
Constructors
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 => G_symb_map_items_list lid [symb_map_items]
Instances
ATermConvertible G_symb_map_items_list
Show G_symb_map_items_list
PrettyPrint G_symb_map_items_list
Eq G_symb_map_items_list
data G_diagram
Grothendieck diagrams
Constructors
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 => G_diagram lid (Diagram sign morphism)
Instances
ATermConvertible G_diagram
data G_sublogics
Grothendieck sublogics
Constructors
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 => G_sublogics lid sublogics
Instances
ATermConvertible G_sublogics
Show G_sublogics
data G_morphism
Homogeneous Grothendieck signature morphisms
Constructors
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 => G_morphism lid morphism
Instances
ATermConvertible G_morphism
Show G_morphism
data AnyComorphism
Existential type for comorphisms
Constructors
forall 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 . 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 => Comorphism cid
Instances
ATermConvertible AnyComorphism
compComorphism :: AnyComorphism -> AnyComorphism -> Result AnyComorphism
Compose comorphisms
data LogicGraph
Logic graph
Constructors
LogicGraph
logics :: (Map String AnyLogic)
comorphisms :: (Map String AnyComorphism)
inclusions :: (Map (String, String) AnyComorphism)
lookupLogic :: String -> String -> LogicGraph -> AnyLogic
find a logic in a logic graph
lookupComorphism :: String -> LogicGraph -> Result AnyComorphism
find a comorphism in a logic graph
data AnyComorphismAux 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
auxiliary existential type needed for composition of comorphisms
Constructors
forall cid . 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 => ComorphismAux cid lid1 lid2 sign1 morphism2
Instances
Typeable (AnyComorphismAux 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)
Show (AnyComorphismAux 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)
tyconAnyComorphismAux :: TyCon
data GMorphism
Grothendieck signature morphisms
Constructors
forall 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 . 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 cid sign1 morphism2
Instances
ATermConvertible GMorphism
Eq GMorphism
Show GMorphism
PrettyPrint GMorphism
Category Grothendieck G_sign GMorphism
data Grothendieck
Constructors
Grothendieck
Instances
ATermConvertible Grothendieck
Language Grothendieck
Category Grothendieck G_sign GMorphism
Show Grothendieck
gEmbed :: G_morphism -> GMorphism
Embedding of homogeneous signature morphisms as Grothendieck sig mors
gsigLeftUnion :: LogicGraph -> Pos -> G_sign -> G_sign -> Result G_sign
heterogeneous union of two Grothendieck signatures the left signature determines the result logic
homogeneousGsigUnion :: Pos -> G_sign -> G_sign -> Result G_sign
homogeneous Union of two Grothendieck signatures
homogeneousGsigManyUnion :: Pos -> [G_sign] -> Result G_sign
homogeneous Union of a list of Grothendieck signatures
homogeneousMorManyUnion :: Pos -> [G_morphism] -> Result G_morphism
homogeneous Union of a list of morphisms
ginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism
inclusion morphism between two Grothendieck signatures
Produced by Haddock version 0.6