Abstract
The paper proposes a variant of sesqui-pushout rewriting (SqPO) that allows one to develop the theory of nested application conditions (NACs) for arbitrary rule spans; this is a considerable generalisation compared with existing results for NACs, which only hold for linear rules (w.r.t. a suitable class of monos). Besides this main contribution, namely an adapted shifting construction for NACs, the paper presents a uniform commutativity result for a revised notion of independence that applies to arbitrary rules; these theorems hold in any category with (enough) stable pushouts and a class of monos rendering it weak adhesive HLR. To illustrate results and concepts, we use simple graphs, i.e. the category of binary endorelations and relation preserving functions, as it is a paradigmatic example of a category with stable pushouts; moreover, using regular monos to give semantics to NACs, we can shift NACs over arbitrary rule spans.
This research was sponsored by the European Research Council (ERC) under grants 587327 “DOPPLER” and 320823 “RULE”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baldan, P., Corradini, A., Heindel, T., König, B., Sobociński, P.: Unfolding Grammars in Adhesive Categories. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 350–366. Springer, Heidelberg (2009)
Braatz, B., Golas, U., Soboll, T.: How to delete categorically Two pushout complement constructions. Journal of Symbolic Computation 46(3), 246–271 (2011); Applied and Computational Category Theory
Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R., Löwe, M.: Algebraic Approaches to Graph Transformation. Part I: Basic Concepts and Double Pushout Approach. In: Handbook of Graph Grammars and Computing by Graph Transformation, pp. 163–245. World Scientific Publishing Co., Inc., River Edge (1997)
Corradini, A., Heindel, T., Hermann, F., König, B.: Sesqui-pushout Rewriting. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 30–45. Springer, Heidelberg (2006)
Danos, V., Feret, J., Fontana, W., Harmer, R., Krivine, J.: Abstracting the differential semantics of rule-based models: Exact and automated model reduction. In: 2010 25th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 362–381 (July 2010)
Danos, V., Feret, J., Fontana, W., Harmer, R., Hayman, J., Krivine, J., Thompson-Walsh, C.D., Winskel, G.: Graphs, rewriting and pathway reconstruction for rule-based models. In: D’Souza, D., Kavitha, T., Radhakrishnan, J. (eds.) FSTTCS. LIPIcs, vol. 18, pp. 276–288. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)
Duval, D., Echahed, R., Prost, F.: Graph rewriting with polarized cloning. CoRR abs/0911.3786 (2009)
Dyckhoff, R., Tholen, W.: Exponentiable morphisms, partial products and pullback complements. Journal of Pure and Applied Algebra 49(1-2), 103–116 (1987)
Ehrig, H., Golas, U., Hermann, F.: Categorical Frameworks for Graph Transformation and HLR Systems Based on the DPO Approach. Bulletin of the EATCS 102, 111–121 (2010)
Ehrig, H., Habel, A., Lambers, L.: Parallelism and concurrency theorems for rules with nested application conditions. ECEASST 26 (2010)
Garner, R., Lack, S.: On the axioms for adhesive and quasiadhesive categories. Theory and Applications of Categories 27(3), 27–46 (2012)
Habel, A., Müller, J., Plump, D.: Double-pushout Graph Transformation Revisited. Mathematical Structures in Computer Science 11(5), 637–688 (2001)
Habel, A., Pennemann, K.H.: Correctness of high-level transformation systems relative to nested conditions. Mathematical Structures in Computer Science 19(2), 245–296 (2009)
Hayman, J., Heindel, T.: Pattern graphs and rule-based models: The semantics of kappa. In: Pfenning, F. (ed.) FOSSACS 2013. LNCS, vol. 7794, pp. 1–16. Springer, Heidelberg (2013)
Heindel, T., Sobociński, P.: Being Van Kampen is a universal property. Logical Methods in Computer Science 7(1) (2011)
Lack, S., Sobociński, P.: Adhesive and quasiadhesive categories. RAIRO – Theoretical Informatics and Applications 39(3), 511–545 (2005)
Löwe, M.: Refined graph rewriting in span-categories: A framework for algebraic graph transformation. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2012. LNCS, vol. 7562, pp. 111–125. Springer, Heidelberg (2012)
Monserrat, M., Rosselló, F., Torrens, J., Valiente, G.: Single-pushout rewriting in categories of spans I: The general setting. Tech. rep., Informe d’investigació, Department of Software (LSI) Universitat Politècnica de Catalunya (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Danos, V., Heindel, T., Honorato-Zimmer, R., Stucki, S. (2014). Reversible Sesqui-Pushout Rewriting. In: Giese, H., König, B. (eds) Graph Transformation. ICGT 2014. Lecture Notes in Computer Science, vol 8571. Springer, Cham. https://doi.org/10.1007/978-3-319-09108-2_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-09108-2_11
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-09107-5
Online ISBN: 978-3-319-09108-2
eBook Packages: Computer ScienceComputer Science (R0)