1,721,193 research outputs found
Graph rewriting for the π-calculus
No full textWe propose a graphical implementation for (possibly recursive) processes of the pi-calculus, encoding each process into a graph. Our implementation is sound and complete with respect to the structural congruence for the calculus: two processes are equivalent if and only if they are mapped into graphs with the same normal form. Most importantly, the encoding allows the use of standard graph rewriting mechanisms for modelling the reduction semantics of the calculus
Rewriting on cyclic structures : equivalence between the operational and the categorical description
Full text linkWe 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 note on an old-fashioned algebra for (disconnected) graphs
No full textGraphs with interfaces are a simple and intuitive tool for allowing a graph G to interact with the environment, by equipping it with two morphisms J → G, I → G. These “handles” were used to define graphical operators, and to provide an inductive presentation of graph rewriting. A main feature of graphs with interfaces is their characterization as terms of a free algebra. So far, this was possible only with discrete interfaces, i.e., containing no edge. This note shows that a similar free construction can be performed also with disconnected interfaces, i.e., containing only nodes connected to at most one edge
Term graph rewriting for the π-calculus
No full textWe propose a graphical implementation for (possibly) recursive processes of the pi-calculus, encoding each process into a term graph. Our implementation is sound and complete with respect to the standard structural congruence for the calculus: Two processes are equivalent if and only if they are mapped into isomorphic term graphs. Most importantly, the encoding allows for using standard graph rewriting mechanisms in modelling the reduction semantics of the calculus
Residuation for bipolar preferences in soft constraints
Full text linkSoft constraint formalisms are an abstract representation of Constraint Satisfaction Problems (CSPs): the set of preferences is now parametric, often forming (a variety of) an absorptive semiring. However, the latter is suitable only for negative preferences, i.e., such that the combination of constraints worsens the quality of the solution. This work comments on related work and exploits residuated semirings in order to lift the Local Consistency heuristics that hold for classical CSPs. As a result, we merge and generalise existent formalisms for modelling soft CSPs with bipolar (positive and negative) preferences
Distributivity and residuation for lexicographic orders
No full textResiduation theory concerns the study of partially ordered algebraic structures, most often just monoids, equipped with a weak inverse for the monoidal operator. One of its areas of application is constraint programming, whose key requirement is the presence of a distributive operator for combining preferences. The key result of the paper shows how, given a residuated monoid of preferences, to build a new residuated monoid of (possibly infinite) tuples based on lexicographic order
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
Processes as formal power series: A coinductive approach to denotational semantics
No full textWe characterize must testing equivalence on CSP in terms of the unique homomorphism from the Moore automaton of CSP processes to the final Moore automaton of partial formal power series over a certain semiring. The final automaton is then turned into a CSP-algebra: operators and fixpoints are defined, respectively, via behavioural differential equations and simulation relations. This structure is then shown to be preserved by the final homomorphism. As a result, we obtain a fully abstract compositional model of CSP phrased in purely set-theoretical terms
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
- …
