 | hets -- a heterogenous Specification (CASL) tool set | Contents | Index |
|
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 {} | | 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 | |
|
|
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 | |
|
|
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 | |
|
|
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 | |
|
|
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 | |
|
|
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 | |
|
|
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 | |
|
|
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 | |
|
|
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 | |
|
|
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 | |
|
|
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 | |
|
|
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 | |
|
|
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 | |
|
|
compComorphism :: AnyComorphism -> AnyComorphism -> Result AnyComorphism |
Compose comorphisms |
|
data LogicGraph |
|
|
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 | |
|
|
data 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 |