Graph Algebras and Derived Graph Operations
Abstract
:1. Introduction
- Model theory:
- In [7], we coined the concept of graph algebra, introduced graph terms, and showed that graph term algebras are free graph algebras. There was, however, no model theory in the sense of traditional Universal Algebra. As a kind of “proof of concept”, we therefore generalize some basic model-theoretic concepts and results from traditional algebras to graph algebras. We concentrate on the concept of “generated subalgebra” and the related problem of characterizing monomorphic and epimorphic homomorphisms.To tackle this task, we make a substantial effort in Section 3 to revise and reformulate traditional set-theoretic definitions, constructions and proofs in Universal Algebra by means of more category-theoretic concepts and constructions. Relying on this reformulation, we can in Section 4 smoothly transfer concepts, definitions and results from traditional algebras to graph algebras. In particular, we prove that all monomorphic homomorphisms between graph algebras are regular.In [7], we adapted the original idea of sketch operations [4] and defined the arity of a graph operation as a single graph inclusion. This definition does not allow us, however, to consider projections as legal graph operations. To be closer to the traditional concept of operation in Universal Algebra, and to be able to define an appropriate concept of a derived graph operation, we therefore declare in this paper the arity of a graph operation as a span of graph inclusions. In Section 4.2, we clarify the relation between both versions and discuss to what extent they are equivalent.To prove that all monomorphic homomorphisms between graph algebras are regular, we also introduce partial graph algebras in Section 4.4. We define a so-called term completion procedure transforming partial graph algebras into total graph algebras. This procedure provides for each signature a free functor from the corresponding category of partial graph algebras to the corresponding category of graph algebras. The construction of graph term algebras turns out to be just a special case of this new procedure.
- Derived graph
- operations: To understand why the strong interconnection between “representation of data” and “representation of derived operations” breaks down in the case of graph operations and to find out how to define derived graph operations in an appropriate way, we include in the paper a more in-depth analysis of the concept term and discuss substitution calculi in general in Section 3.4.In Section 3.7, we recall the construction of syntactic Lawvere theories as it is described in [8], for example. In Section 5.1, we discuss finite product categories and elucidate that terms can be characterized as normal forms for finite product expressions; thus, Lawvere’s original slogan “composition is substitution” can be turned into the slogan “substitution is symbolic composition plus normalization”.Reviewing the relationship between finite products and tensor products, we identify copying in Section 5.2 as the cause of the problem. We argue that, in the case of graph operations, “copying of data”, as a computation of its own, has to be replaced by the “soldering” of input and (!) output ports of computations.In such a way, we end up in Section 5.3 with three mechanisms to construct new graph operations out of given ones: parallel composition, instantiation (“soldering” of input and output ports), and sequential composition.Finally, we introduce in Section 5.4 graph operation expressions with a structure as close as possible to the structure of terms. We define their semantics, i.e., the derived graph operations we have been looking for, by means of the three mechanisms of parallel composition, instantiation and sequential composition.
2. Notations and Preliminaries
- and
- for all .
- We consider any (total) map as a partial map with .
3. Algebras and Term Algebras
3.1. Signatures, Algebras and Homomorphisms
- A setof operation symbols,
- A map assigning to each operation symbol as its arity a pair of finite sets with for some , and .
- A set A, called the carrier of , and
- A familyof maps called operations.
3.2. Subalgebras
“If M is a family of closed subsets in , then its intersection is closed as well”
- 1.
- is accessible via a map if .
- 2.
- If is accessible via an inclusion map , i.e., if , we also say that is generated by A.
- 3.
- is said to be generated if it is generated by the empty set, i.e., accessible via the unique map from the initial object ∅ in to B.
- Case 1
- factors through : There exists a map such that (see the right diagram above). is unique since is a monomorphism. We simply set
- Case 2
- factors through : Analogous to Case 1.
- Case 3
- Overlapping of Case 1 and 2: There exist maps such that . Due to the pullback property of the square, there exists a unique such that . The homomorphism property of ensures and we obtain, finally, . That is, in the event of an overlapping, Case 1 and Case 2 define the same output . Note that there will always be an overlapping for constant symbols!
- Case 4
- factors neither through nor through : This can only happen if with . Utilizing the operations in to a maximal extent, Cases 1 and 2 define a partial map from to . However, since we restrict ourselves to total operations, we have to find an ad hoc totalization trick to turn into a total operation. Employing (7), we may decide to utilize the operations in to produce outputs in the left copy of B in . We set
3.3. Terms and Term Algebras
- Variables:
- , for all ;
- Constants:
- , for all with ;
- Operations:
- , for all with , and all maps in .
- Variables:
- , for all ;
- Constants:
- , for all ;
- Operations:
- , for all .
- Constants:
- , for all with , and
- Operations:
- , for all with , and all maps in .
- Constants:
- , for all ;
- Operations:
- , for all where is the map in defined by .
3.4. Substitutions
3.4.1. Substitution Calculi
In Universal Algebra, we can formalize substitutions as maps . For finite sets we may simply declare a substitution by listing the corresponding assignments .(1) Substitution (declaration), i.e., an assignment of expressions to variables.
A common practice in Universal Algebra [14] is to denote the resulting term in of applying a finite substitution to a term t in by(2) Substitution application, i.e., the replacement of occurrences of variables in a given expression by the expressions assigned to the variables by a substitution.
In the case of terms, “well-formedness” simply means that we consider only those strings of symbols as terms that can be generated inductively by the three rules in Definition 3.8.(3) Preservation of well formedness; i.e., replacing variables in a well-formed expression by well-formed expressions should result in a well-formed expression.
The composition of the two linkable finite substitutions from to and from to results, for example, in the finite substitution(4) Composition of linkable substitutions.
For the two linkable finite substitutions above, this requirement can be expressed by the equation(5) The composition of substitutions is compatible with substitution application.
(6) The composition of substitutions is associative.
In Universal Algebra, we work exclusively with variables ranging over elements in sets, and thus variable assignments can be defined as maps from a set of variables into the carrier set of a -algebra , as in Definition 3.9.(7) Variable assignments, i.e., assignments of semantic items to variables.
Definition 3.9 presents, for example, an inductive definition of the evaluation of -terms into elements in the carrier A of a -algebra induced by a variable assignment .(8) evaluation of expressions, computing for each expression a unique semantic item or truth value.
For both new kinds of composition, it is desirable to have(9) The composition of substitutions with variable assignments as well as The composition of variable assignments with homomorphisms.
Finally, it would be reasonable to require(10) Compatibility with respect to substitution application and/or evaluation.
(11) Associativity for the three new possible combinations of the four kinds of composition, i.e., substitution–substitution–assignment, substitution–assignment–homomorphism, and assignment–homomorphism–homomorphism.
3.4.2. Substitutions by Algebraic Extensions
- Feature (1):
- Substitutions simply become a special case of variable assignments and
- Feature (2):
- Substitution applications appear as a special case of term evaluations, namely as algebraic extensions . Applying a substitution to a -term means nothing but to compute the -term . As mentioned before, it is also common to use instead of the more informative notation in (10) in the case of finite sets of variables.
- Feature (3):
- Preservation of well formedness is implicitly ensured by the fact that the structures we define in Definition 3.10 (Term algebra) are indeed -algebras.
for example, is simply given by the compatibility of substitution application and evaluation, as well as associativity of map composition: for arbitrary substitutions , and assignments .substitution; (substitution; assignment) = (substitution; substitution); assignment,
- Variables:
- , for all ;
- Constants:
- , for all ;
- Operations:
- , for all .
3.5. Two Model-Theoretic Implications of the Existence of a Free Functor
- 1.
- is accessible via .
- 2.
- is accessible via .
- 3.
- is an epimorphism in .
- 4.
- is an epimorphism in , i.e., surjective.
3.6. Terms and Derived Operations
- Variables:
- for all , the (projection) map is defined by for all ;
- Constants:
- , for all ;
- Operations:
- , for all , .
3.7. Syntactic Lawvere Theories
3.7.1. Construction of Lawvere Theories
- Objects:
- As objects, we choose canonical finite sets of variablesFor all , we assume to be equipped with a fixed total order ; thus, we can reuse the tuple notation to represent maps as discussed in Section 2.
- Morphisms:
- Morphisms are all tuples representing a substitution (declaration) .
- Identities:
- The identity on is the tuple representing the substitution .
- Composition:
- The composition of two tuples and is the tuple representing the substitution where is the application of the substitution according to Definition 3.11 (compare also (11)).
- Laws:
- Identity and associativity law are ensured by Feature (5), composition of substitutions is compatible with substitution application (compare also (12)).
3.7.2. Properties of Lawvere Theories
- The product of two objects and is defined by with projections and .
- The tuple of two morphisms and in is given by
4. Graph Algebras and Graph Term Algebras
4.1. Graph Signatures, Graph Algebras, and Homomorphisms
- Two
- different kinds of input items. This is evident due to working with graphs that consist of both vertices and edges. Instead of a single set, we therefore declare a graph as the input arity.
- Arbitrarily
- many output items. A single output is assumed for algebraic operations, but graph operations can produce arbitrarily large finite graphs as output. Similar to the input, the output arity is chosen to be a graph.
- Output
- is often related to the input. In the case of the composition operation above, the relation between the two arity graphs and is clear from the labelling: the output edge has the same source and target as the input edges and , respectively. Instead of always requiring coherent labeling, we introduce a third arity graph , called the boundary of , to encompass the connection between input and output in a fitting way.
- A set of operation symbols,
- A map assigning to each operation symbol in its arity span , i.e., a span of inclusion graph homomorphisms between finite graphs such that the sets and as well as the sets and are disjoint. The graphs , , and are referred to as the input arity, boundary arity, and output arity of , respectively.
- By a graph, called the carrier of , and
- By a familyof maps such that the following diagram commutes for allinand all graph homomorphisms.
4.2. Comparison with the Old Definitions
4.2.1. Comparison of Arity Declarations
4.2.2. Equivalence of Graph Operations
4.2.3. Equivalence of Homomorphism Conditions
4.3. Graph Subalgebras
- 1.
- is accessible via a graph homomorphism if .
- 2.
- Ifis accessible via an inclusion graph homomorphism, i.e., if, we say also thatis generated by .
- 3.
- is said to be generated if it is generated by the empty graph, i.e., accessible via the unique graph homomorphism from the initial object in to .
4.4. Partial Graph Algebras and Their Term Completion
- By a graph, called the carrier of , and
- By a familyof partial maps such that the following diagram commutes for allinand all graph homomorphisms.
- Generators:
- Constants:
- For all constantsin, such that, the graphcontains
- as a vertex, for each vertexin;
- as an edge, for each edgein, whereand
- Operations:
- For allinwithand anysuch that there is nowith,contains
- as a vertex, for each vertexin;
- as an edge, for each edgein, where
- 1.
- The term notation provides a uniform mechanism to create unique identifiers for the new graph items introduced by applying a non-deleting injective graph -transformation rule [9].
- 2.
- At the same time, the term notation encodes all the information necessary to uniquely identify the pushout that has been creating the new items.
- Constants:
- For all constantsin:
- Utilizing:
- Ifis defined, we simply reuse it:
- Completion:
- Ifis not defined, i.e.,we set
- for each vertexinand
- for each edgein.
- Operations:
- For allinwithand any:
- Utilizing:
- If there is awith, we reuse:
- Completion:
- If there is nowith, we set
- Generators:
- In this base case, the defining condition forces for all and for all .
- Constants:
- In the second base case, we have, for all constants in :
- Utilizing:
- If is defined, the definition of operations in , the defining condition and the assumption that is a -homomorphism ensure that satisfies the homorphism condition for the constant :
- Completion:
- If is not defined, the definition of operations in and the required homomorphism condition for forces for each vertex in
- Operations:
- We have, for all in with and any ,
- Utilizing:
- If there is a with , then the definition of operations in , the defining condition and the assumption that is a -homomorphism ensure that satisfies the homomorphism condition for :
- Completion:
- If there is no with , the induction hypothesis is that is already defined on a subgraph and that . This ensures . In the induction step, we extend to the graph . The definition of operations in and the required homomorphism condition for forces for each vertex in
4.5. Graph Terms and Graph Term Algebras
- Graph terms
- : We denote the graph, according to Definition 4.9, also byand call it the graph of all (graph) -terms on .
- Graph term algebra
- : We denote the term completion-algebra, due to Definition 4.10, also byand call it the-term graph algebra on .
- Substition Calculus:
- Graph term algebras manifest the “internalization approach” in the case of graph algebras. Relying on Proposition 4.6, we can indeed obtain a fully fledged substitution calculus, meeting the requirements formulated in Section 3.4.1. Based on the idea that a substitution (declaration) is now given by a graph homomorphism and that a variable assignment is a graph homomorphism for a -algebra , we can simply transfer all the discussions, definitions and results from Section 3.4.2 to graph algebras. We will spare the reader this copy–paste exercise.
- No appropriate concept of Derived Operation:
- In traditional Universal Algebra, we do have a one-to-one correspondence between the “internal view” of terms as elements of free algebras and the “external view” of terms as an appropriate representation of derived operations (compare Definitions 3.12 and 3.14). It took us a while to realize that this one-to-one correspondence breaks down when it comes to graph algebras and even longer to understand the reasons. We discuss and address this problem in the next section.
5. Derived Graph Operations
5.1. Reconstruction of Syntactic Lawvere Theories
5.1.1. Categories with Finite Products
- has an empty product (terminal object) , i.e., for any object A in there is a morphism such that
- For any family , of objects, there is an object together with projections , such that
- For any object B and any family , of morphisms, there is a morphism with
- Finally, for all morphisms , the following equation holds
5.1.2. Categories Based on Finite Product Expressions
- Objects:
- As objects, we choose the same canonical finite sets of variables as for
- Morphisms:
- Morphisms are all finite product expressions inductively defined as follows
- Symbolic Projections:
- is an fp-expression for all , .
- Constant and Operation Symbols:
- with is an fp-expression if is an n-ary operation symbol in .
- Empty Symbolic Tuples:
- is an fp-expression for all .
- Non-empty Symbolic Tuples:
- is an fp-expression for all , and all families , of fp-expressions.
- Symbolic Sequential Composition:
- is an fp-expression for all and all fp-expressions , .
- Symbolic Identities:
- is the identity on for all and is the identity on .
- Variables:
- , for all, .
- Constants:
- , for all.
- Operations:
- , for all, .
5.1.3. Substitutions Revisited
This perception may open a path to develop, in the future, an appropriate substitution calculus for derived graph operations.substitution application ≅ symbolic composition plus normalization.
5.2. Analysis of Finite Product Expressions
5.2.1. Finite Products vs. Tensor Products
5.2.2. Copying vs. Soldering
5.3. Three Mechanisms to Construct New Graph Operations
5.3.1. Parallel Composition
5.3.2. Instantiation
5.3.3. Sequential Composition
- For canonical arity spans and , we can have an equality only if is a built-in projection.
- There are two kinds of output items produced via the sequential composition of two graph operations. First, the output items produced by . Second, the output items produced by and implicitly transferred by , i.e., the items in . In other words, the resulting arity will not satisfy the disjointness condition in Definition 4.1 if is non-empty!
- We obtain an epi-mono factorization of by constructing the image of with respect to . The resulting restriction of becomes an isomorphism since is an isomorphism.
- The boundary arity of can now be constructed by simple intersection (pullback): and .
- To be able to define as an extension of such that consists of canonical sets of output vertices and output edges, according to Remark 4.2, we first have to reindex the output vertices/edges in . We construct a graph , isomorphic to with and , where and for and .
- We can define an isomorphism that is the identity on such that, in addition, restricted to is an order-preserving map from to while restricted to is an order-preserving map from to . The construction ensures that becomes an inclusion graph homomorphism .
- We construct via a pushout of the span with where is constructed by “index shifting” and where is also constructed by “index shifting”.
- The construction ensures and that becomes an isomorphism. We set and obtain a canonical arity span as required.
5.4. Graph Operation Expressions and Derived Graph Operations
- Projections:
- with arity span for any finite canonical input arity graph and any subgraph .is called a projection expression.
- Constants:
- with arity for any constant symbol and any finite canonical input arity graph .Moreover,with arity for any non-empty subgraph .Both expressions and are declared as single -expressions.
- Operations:
- for any operation symbol , any finite canonical input arity graph , and any graph homomorphism where the arity is constructed as an instance of the arity by means of and a pushout as in (31).Moreover, for any non-empty subgraph such that is non-empty with arity .Both expressions and are called basic -expressions and are declared as single -expressions.
- Multi expressions:
- for any family , , of single -expressions or projection expressions with, at least, one single -expression. The arity is constructed as described in Remark 5.2.Moreover, for any finite canonical input arity graph , and any graph homomorphism with arity constructed as an instance of the arity by means of and a pushout as performed in (31).Both expressions and are declared as multi -expressions.
- Symbolic composition:
- for any single or multi -expression with arity , any basic -expression with arity , and any graph isomorphism .is declared as a single -expressions.
- Constants:
- In the case , we will just write instead of and instead of .
- Operations:
- In the case , we will just write instead of and instead of .
- Projections:
- , according to (17), for all .
- Constants:
- for all .for all.
- Operations:
- , according to Section 5.3.2, for all .for all.
- Multi expressions:
- , according to Section 5.3.1, for all ., according to Section 5.3.1 and Section 5.3.2, for all .
- Symbolic composition:
- , according to Section 5.3.3, for all .
- 1.
- By means of the restriction expressions and , we can simulate the “pseudo operation symbols” , , , and their semantics by choosing to be the single output vertex or the single output edge (together with its source and target).
- 2.
- Once we have been able to represent all the single vertices and edges in a subgraph by corresponding graph operation expressions, we can combine them into one graph operation expression using the trick used in Conjecture 5.3 to define the graph operation expression . All the single output arities will be soldered together resulting in a graph isomorphic to .
6. Operations in Topoi
7. Related Work
- Input and output arity graphs are not described with concrete syntactic identifiers but are implicitly considered as being given by “equivalence up to arity renaming”.
- There are no boundaries and thus no systematic treatment of “preservation conditions” as we formalized them by means of the commutativity condition in (16).
- In the examples, preservation conditions are expressed by means of ad hoc equations between vertices and/or edges, respectively.
- There is no explicit notion of “derived graph operation”, and the issue of “graph operation expressions” is not addressed at all.
- Derived graph operations, in our sense, appear only implicitly when properties of graph operations are described by means of equations between vertices and/or edges.
- However, the authors do not follow the tradition in Universal and Categorical Algebra of defining algebras as “indexed structures” [26] where sort symbols are interpreted by sets and operation symbols by maps from finite Cartesian products of sets into sets. Instead, they describe algebras as “fibred structures” utilizing so-called “m-graphs”.
- m-graphs can encode the “graphs” of operations in traditional “indexed -algebras”. That is, each element of the graph of an n-ary operation in an “indexed -algebra” can be represented by a designated m-edge e with source and target .
- The discussion in Remark 4.4 concerning “graphs of graph operations” also applies to graphs of algebraic operations. There are no boundaries in the case of algebraic operations, and thus we have for each n-ary operation symbol in the signature . Remark 4.4 proposes to represent the elements in by maps with for all and . Due to the notational conventions in Section 2, we would, however, denote those mappings simply by -tuples .
- The set of all pairs with in and for an “indexed -algebra” constitutes the disjoint union of the graphs of all operations in and can obviously serve as the set E of m-edges of an “m-graph encoding” of the “indexed -algebra” . The carrier set A of is thereby the set of vertexes of the m-graph encoding of .
- For many-sorted signatures we can construct m-graph encodings of “indexed -algebras” that are fully analogous.
- It is obvious that the m-graph encodings of terminal “indexed -algebras”, where each sort in a many-sorted signature is interpreted by a singleton, exactly correspond to the m-graphs serving as signatures in [23,24]. Thus, there is indeed a unique m-graph homomorphism from the m-graph encoding of any “indexed -algebra” into the corresponding signature in the sense of [23,24].
- Traditional monoidal categories and string diagrams only deal with single isolated items as the input and output of operations.
- This manifests itself in the absence of boundaries.
- The essential difference is that the presence of boundaries forces us to replace “internal copying of items in diagrams” with “soldering of input and output ports of diagrams”, i.e., by constructing instances of diagrams as a whole.
8. Conclusions
Author Contributions
Funding
Acknowledgments
Conflicts of Interest
References
- Wolter, U. Logics of Statements in Context—Category Independent Basics. Mathematics 2022, 10, 1085. [Google Scholar] [CrossRef]
- Makkai, M. Generalized Sketches as a Framework for Completeness Theorems. J. Pure Appl. Algebra 1997, 115, 49–79, 179–212, 214–274. [Google Scholar]
- Cadish, B.; Diskin, Z. Heterogeneous View Integration via Sketches and Equations. In Proceedings of the ISMIS, Zakopane, Poland, 9–13 June 1996; Volume 1079, pp. 603–612. [Google Scholar]
- Diskin, Z. Databases as Diagram Algebras: Specifying Queries and Views Via the Graph-Based Logic of Sketches; Technical Report 9602; Frame Inform Systems: Riga, Latvia, 1996. [Google Scholar]
- Diskin, Z.; Kadish, B. A Graphical Yet Formalized Framework for Specifying View Systems. In Proceedings of the First East-European Symposium on Advances in Databases and Information Systems, Nevsky Dialect, St. Petersburg, Russia, 2–5 September 1997; pp. 123–132. [Google Scholar]
- Burroni, A. Algèbres graphiques (sur un concept de dimension dans les langages formels). Cah. Topol. Géom. Différ. Catég. 1981, 22, 249–265. [Google Scholar]
- Wolter, U.; Diskin, Z.; König, H. Graph Operations and Free Graph Algebras. In Graph Transformation, Specifications, and Nets: In Memory of Hartmut Ehrig; Heckel, R., Taentzer, G., Eds.; Springer: Berlin/Heidelberg, Germany, 2018; pp. 313–331. [Google Scholar] [CrossRef]
- Poigné, A. Algebra categorically. In Category Theory and Computer Programming; Pitt, D., Abramsky, S., Poigné, A., Rydeheard, D., Eds.; Springer: Berlin/Heidelberg, Germany, 1986; pp. 76–102. [Google Scholar] [CrossRef]
- Ehrig, H.; Ehrig, K.; Prange, U.; Taentzer, G. Fundamentals of Algebraic Graph Transformation; Monographs in Theoretical Computer Science; An EATCS Series; Springer: Berlin/Heidelberg, Germany, 2006. [Google Scholar] [CrossRef]
- Barr, M.; Wells, C. Category Theory for Computing Science; Series in Computer Science; Prentice Hall International: London, UK, 1990. [Google Scholar]
- Pierce, B.C. Basic Category Theory for Computer Scientists; The MIT Press: Cambridge, MA, USA; London, UK, 1991. [Google Scholar]
- Wolter, U. Cogenerated Quotient Coalgebras; Technical Report Report No 299; Department of Informatics, University of Bergen: Bergen, Norway, 2005. [Google Scholar]
- Ehrig, H.; Mahr, B. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics; EATCS Monographs on Theoretical Computer Science 6; Springer: Berlin/Heidelberg, Germany, 1985. [Google Scholar]
- Wechler, W. Universal Algebra for Computer Scientists; Monographs in Theoretical Computer Science; An EATCS Series; Springer: Berlin/Heidelberg, Germany, 1992; Volume 25, p. 339. [Google Scholar] [CrossRef]
- MacLane, S. Categories for the Working Mathematician; Graduate Texts in Mathematics Volume 5; Springer: New York, NY, USA, 1978; pp. xii+318. [Google Scholar]
- Goldblatt, R. Topoi: The Categorial Analysis of Logic; Dover Publications: New York, NY, USA, 1984. [Google Scholar]
- Reichel, H. Initial Computability, Algebraic Specifications, and Partial Algebras; Oxford University Press: Oxford, UK, 1987. [Google Scholar]
- Wolter, U. An Algebraic Approach to Deduction in Equational Partial Horn Theories. J. Inf. Process. Cybern. EIK 1990, 27, 85–128. [Google Scholar]
- Claßen, I.; Große-Rhode, M.; Wolter, U. Categorical concepts for parameterized partial specifications. Math. Struct. Comput. Sci. 1995, 5, 153–188. [Google Scholar] [CrossRef]
- Corradini, A.; Gadducci, F. An Algebraic Presentation of Term Graphs, via GS-Monoidal Categories. Appl. Categ. Struct. 1999, 7, 299–331. [Google Scholar] [CrossRef]
- Selinger, P. A Survey of Graphical Languages for Monoidal Categories. In New Structures for Physics; Coecke, B., Ed.; Springer: Berlin/Heidelberg, Germany, 2011; pp. 289–355. [Google Scholar] [CrossRef]
- Makkai, M. First Order Logic with Dependent Sorts, with Applications to Category Theory. Available online: https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf (accessed on 10 September 2023).
- Sernadas, A.; Sernadas, C.; Rasga, J.; Coniglio, M. A Graph-theoretic Account of Logics. J. Log. Comput. 2009, 19, 1281–1320. [Google Scholar] [CrossRef]
- Sernadas, A.; Sernadas, C.; Rasga, J.; Coniglio, M. On Graph-theoretic Fibring of Logics. J. Log. Comput. 2009, 19, 1321–1357. [Google Scholar] [CrossRef]
- Wolter, U.; Martini, A.; Häusler, E. Indexed and fibered structures for partial and total correctness assertions. Math. Struct. Comput. Sci. 2022, 32, 1145–1175. [Google Scholar] [CrossRef]
- Wolter, U. Indexed vs. fibred structures—A field report. Rom. J. Pure Appl. Math. 2020, 66, 813–830. [Google Scholar]
Disclaimer/Publisher’s Note: The statements, opinions and data contained in all publications are solely those of the individual author(s) and contributor(s) and not of MDPI and/or the editor(s). MDPI and/or the editor(s) disclaim responsibility for any injury to people or property resulting from any ideas, methods, instructions or products referred to in the content. |
© 2023 by the authors. Licensee MDPI, Basel, Switzerland. This article is an open access article distributed under the terms and conditions of the Creative Commons Attribution (CC BY) license (https://creativecommons.org/licenses/by/4.0/).
Share and Cite
Wolter, U.; Truong, T.T. Graph Algebras and Derived Graph Operations. Logics 2023, 1, 182-239. https://doi.org/10.3390/logics1040010
Wolter U, Truong TT. Graph Algebras and Derived Graph Operations. Logics. 2023; 1(4):182-239. https://doi.org/10.3390/logics1040010
Chicago/Turabian StyleWolter, Uwe, and Tam T. Truong. 2023. "Graph Algebras and Derived Graph Operations" Logics 1, no. 4: 182-239. https://doi.org/10.3390/logics1040010
APA StyleWolter, U., & Truong, T. T. (2023). Graph Algebras and Derived Graph Operations. Logics, 1(4), 182-239. https://doi.org/10.3390/logics1040010