1,721,035 research outputs found
Deriving Bisimulation Congruences using 2-Categories
No full textWe introduce G-relative-pushouts (GRPO) which are a 2-categorical generalisation of relative-pushouts (RPO). They are suitable for deriving labelled transition systems (LTS) for process calculi where terms are viewed modulo structural congruence. We develop their basic properties and show that bisimulation on the LTS derived via GRPOs is a congruence, provided that sufficiently many GRPOs exist. The theory is applied to a simple subset of CCS and the resulting LTS is compared to one derived using a procedure proposed by Sewell
A Survey of Compositional Signal Flow Theory
No full textSignal flow graphs are combinatorial models for linear dynamical systems, playing a foundational role in control theory and engineering. In this survey, we overview a series of works [3, 10, 11, 13, 15–18, 31, 51, 63] that develop a compositional theory of these structures, and explore several striking insights emerging from this approach. In particular, the use of string diagrams, a categorical syntax for graphical models, allows to switch from the traditional combinatorial treatment of signal flow graphs to an algebraic characterisation. Within this framework, signal flow graphs may then be treated as a fully-fledged (visual) programming language, and equipped with important meta-theoretical properties, such as a complete axiomatisation and a full abstraction theorem. Moreover, the abstract viewpoint offered by string diagrams reveals that the same algebraic structures modelling linear dynamical systems may also be used to interpret diverse kinds of models, such as electrical circuits and Petri nets. In this respect, our work is a contribution to compositional network theory (see e.g., [1, 2, 4–6, 9, 12, 20, 21, 23, 24, 26, 28–30, 32, 37, 49, 59], ?), an emerging multidisciplinary research programme aiming at a uniform compositional study of different sorts of computational models
Syntactic formats for free: an abstract approach to process equivalence
No full textA framework of Plotkin and Turi's, originally aimed at providing an abstract notion of bisimulation, is modified to cover other operational equivalences and preorders. Combined with bialgebraic methods, it yields a technique for the derivation of syntactic formats for transition system specifications which guarantee that various operational preorders are precongruences. The technique is applied to the trace preorder, the completed trace preorder and the failures preorder. In the latter two cases, new syntactic formats guaranteeing precongruence properties are introduced
A categorical semantics of signal flow graphs
No full textWe introduce , double-struck IH a sound and complete graphical theory of vector subspaces over the field of polynomial fractions, with relational composition. The theory is constructed in modular fashion, using Lack's approach to composing PROPs with distributive laws. We then view string diagrams of double-struck IHas generalised stream circuits by using a formal Laurent series semantics. We characterize the subtheory where circuits adhere to the classical notion of signal flow graphs, and illustrate the use of the graphical calculus on several examples. © 2014 Springer-Verlag
Lawvere categories as composed PROPs
No full textPROPs and Lawvere categories are related notions adapted to the study of algebraic structures borne by an object in a category, but whereas PROPs are symmetric monoidal, Lawvere categories are cartesian. This paper formulates the connection between the two notions using Lack's technique for composing PROPs via distributive laws. We show Lawvere categories can be seen as resulting from a distributive law of two PROPs - one expressing the algebraic structure in linear form and the other expressing the ability of copying and discarding variables
Full Abstraction for Signal Flow Graphs
No full textNetwork theory uses the string diagrammatic language of monoidal categories to study graphical structures formally, eschewing specialised translations into intermediate formalisms. Recently, there has been a concerted research focus on developing a network theoretic approach to signal flow graphs, which are classical structures in control theory, signal processing and a cornerstone in the study of feedback. In this approach, signal flow graphs are given a relational denotational semantics in terms of formal power series.Thus far, the operational behaviour of such signal flow graphs has only been discussed at an intuitive level. In this paper we equip them with a structural operational semantics. As is typically the case, the purely operational picture is too concrete - two graphs that are denotationally equal may exhibit different operational behaviour. We classify the ways in which this can occur and show that any graph can be realised - rewritten, using the graphical theory, into an executable form where the operational behavior and the denotation coincides
Interacting Hopf algebras
No full textWe introduce the theory IHR of interacting Hopf algebras, parametrised over a principal ideal domain R. The axioms of IHR are derived using Lack's approach to composing PROPs: they feature two Hopf algebra and two Frobenius algebra structures on four different monoid–comonoid pairs. This construction is instrumental in showing that IHR is isomorphic to the PROP of linear relations (i.e. subspaces) over the field of fractions of R
Deconstructing Lawvere with distributive laws
No full textPROs, PROPs and Lawvere categories are related notions adapted to the study of algebraic structures borne by an object in a category: PROs are monoidal, PROPs are symmetric monoidal and Lawvere categories are cartesian. This paper connects the three notions using Lack's technique for composing PRO(P)s via distributive laws. We show that Lawvere categories can be seen as the composite PROP CCm;T, where T expresses the algebraic structure in linear form and CCm express the ability of copying and discarding them. In turn the PROP T can be decomposed in terms of PROs as P;S where P expresses the ability of permuting variables and S is the PRO encoding the syntactic structure without permutations
CARTOGRAPHER: A tool for string diagrammatic reasoning
Full text linkWe introduce cartographer, a tool for editing and rewriting string diagrams of symmetric monoidal categories. Our approach is principled: the layout exploits the isomorphism between string diagrams and certain cospans of hypergraphs; the implementation of rewriting is based on the soundness and completeness of convex double-pushout rewriting for string diagram rewriting
- …
