1,721,220 research outputs found
An Algebraic Presentation of Term Graphs, via GS-Monoidal Categories
No full textWe present a categorical characterization of term graphs (i.e., finite, directed acyclic graphs labeled over a signature) that parallels the well-known characterization of terms as arrows of the algebraic theory of a given signature (i.e., the free Cartesian category generated by it). In particular, we show that term graphs over a signature Σ are one-to-one with the arrows of the free gs-monoidal category generated by Σ. Such a category satisfies all the axioms for Cartesian categories but for the naturality of two transformations (the discharger ! and the duplicator ▽), providing in this way an abstract and clear relationship between terms and term graphs. In particular, the absence of the naturality of ▽ and ! has a precise interpretation in terms of explicit sharing and of loss of implicit garbage collection, respectively
Rewriting on cyclic structures : equivalence between the operational and the categorical description
Get PDFWe present a categorical formulation of the rewriting of possibly cyclic term graphs, based on a variation of algebraic 2-theories. We show that this presentation is equivalent to the well-accepted operational definition proposed by Barendregt et al. - but for the case of circular redexes, for which we propose (and justify formally) a different treatment. The categorical framework allows us to model in a concise way also automatic garbage collection and rules for sharing/unsharing and folding/unfolding of structures, and to relate term graph rewriting to other rewriting formalisms
A functorial semantics for multi-algebras and partial algebras, with applications to syntax
No full textMulti-algebras allow for the modelling of nondeterminism in an algebraic framework by interpreting operators as functions from individual arguments to sets of possible results. We propose a functorial presentation of various categories of multi-algebras and partial algebras, analogous to the classical presentation of algebras over a signature Σ as cartesian functors from the algebraic theory over Σ to Set. We introduce two different notions of theory over a signature, both having a structure weaker than cartesian, and we consider functors from them to Rel or Pfn, the categories of sets and relations or partial functions, respectively. Next we discuss how the functorial presentation provides guidelines when choosing syntactical notions for a class of algebras, and as an application we argue that the natural generalization of usual terms are "conditioned terms" for partial algebras, and "term graphs" for multi-algebras
A Completeness result for equational deduction in coalgebraic specification
No full textThe use of coalgebras for the specification of dynamical systems with a hidden state space is receiving more and more attention in the years, as a valid alternative to algebraic methods based on observational equivalences. However, to our knowledge, the coalgebraic framework is still lacking a complete equational deduction calculus which enjoys properties similar to those stated in Birkhoff's completeness theorem for the algebraic case.
In this paper we present a sound and complete equational calculus for a restricted class of coalgebras. We compare our notion of coalgebraic equation to others in the literature, and we hint at possible extensions of our framework
Concurrent Graph and Term Graph Rewriting
No full textGraph Rewriting Systems are a powerful formalism for the specification of parallel and distributed systems, and the corresponding theory is rich of results concerning parallelism and concurrency. I will review the main results of the theory of concurrency for the algebraic approach to graph rewriting, emphasizing the relationship with the theory of Petri nets. In fact, graph rewriting systems can be regarded as a proper generalization of Petri nets, where the current state of a system is described by a graph instead of by a collection of tokens. Recently, this point of view allowed for the generalization to graph rewriting of some interesting results and constructions of the concurrent semantics of nets, including processes, unfoldings, and categorical semantics based on pair of adjoint functors
Functorial semantics for multi-algebras
No full textMulti-algebras allow to model nondeterminism in an algebraic framework by interpreting operators as functions from individual arguments to sets of possible results. We propose a functorial presentation of various categories of multi-algebras and partial algebras, analogous to the classical presentation of algebras over a signature Sigma as cartesian functors from the algebraic theory of Sigma, Th(Sigma), to Set. The functors we introduce are based on variations of the notion of theory, having a structure weaker than cartesian, and their target is Rel, the category of sets and relations. We argue that this functorial presentation provides an original abstract syntax for partial and multi-algebras
Rational Term Rewriting
No full textRational terms (possibly infinite terms with finitely many subterms) can be represented in a finite way via mu-terms, that is, terms over a signature extended with self-instantiation operators. For example, f(omega) = f(f(f(...))) can be represented as mu(x).f(x) (or also as mu(x).f(f(x)), f(mu x.f(x)),...). Now, if we reduce a mu-term t to s via a rewriting rule using standard notions of the theory of Term Rewriting Systems, how are the rational terms corresponding to t and to s related? We answer to this question in a satisfactory way, resorting to the definition of infinite parallel rewriting proposed by Corradini. We also provide a simple, algebraic description of mu-term rewriting through a variation of Meseguer's Rewriting Logic formalism
On term graphs as an adhesive category
No full textThe recent interest in bisimulation congruences for reduction systems, stimulated by the research on general (often graphical) frameworks for nominal calculi, has brought forward many proposals for categorical formalisms where relevant properties of observational equivalences could be auto- matically verified.
Interestingly, some of these formalisms also identified suitable categories where the standard tools and techniques developed for the double-pushout approach to graph transformation could be recast, thus providing a valid alternative to the High-Level Replacement Systems paradigm.
In this paper we consider the category of term graphs, and we prove that it (partly) fits in the general framework for adhesive categories. The main technical achievement concerns the proof that the category of term graphs is actually quasi-adhesive, obtained by proving the existence of suitable Van Kampen squares
A 2-Categorical Presentation of Term Graph Rewriting
No full textIt is well-known that a term rewriting system can be faithfully described by a cartesian 2-category, where horizontal arrows represent terms, and cells represent rewriting sequences. In this paper we propose a similar, original 2-categorical presentation for term graph rewriting. Building on a recente result, which shows that term graphs over a given signature are in one-to-one correspondence with arrows of a gs-monoidal category freely generated from the signature, we associate with a term graph rewriting system a gs-monoidal 2-category, and show that cells faithfully represent its rewriting sequences. We exploit the categorical framework to relate term graph rewriting and term rewriting, since gs-monoidal (2-)categories can be regarded as “weak” cartesian (2-) categories, where certain (2-)naturality axioms have been dropped
Term Rewriting in CT-Sigma
No full textWe extend the classical theory of term rewriting systems to infinite and partial terms (i.e., to the elements of algebra CT ∑ ), fully exploiting the complete partially ordered structure of CT ∑ . We show that redexes and rules, as well as other operations on terms, can be regarded as total functions on CT ∑ . As a consequence, we can study their properties of monotonicity and continuity. For rules, we show that nonleft-linear rules are in general not. monotonic, and that left-infinite rules are in general not continuous. Moreover, we show that the well-known Church-Rosser property of non-overlapping redexes holds for monotonic redexes. This property allows us to define a notion of parallel application of a finite set of monotonie redexes, and, using standard algebraic techniques, we extend the definition to the infinite case. We also suggest that infinite parallel term rewriting has interesting potential applications in the semantics of cyclic term, graph rewriting
- …
