Abstract
A unary operator f is idempotent if the equation f(x) = f(f(x)) holds. On the other end, an element a of an algebra is said to be an idempotent for a binary operator ⊙ if a = a ⊙ a. This paper presents a rule format for Structural Operational Semantics that guarantees that a unary operator be idempotent modulo bisimilarity. The proposed rule format relies on a companion one ensuring that certain terms are idempotent with respect to some binary operator.
The authors have been partially supported by the project ‘Meta-theory of Algebraic Process Theories’ (No. 100014021) of the Icelandic Research Fund. Eugen-Ioan Goriac is also funded by the project ‘Extending and Axiomatizing Structural Operational Semantics: Theory and Tools’ (No. 1102940061) of the Icelandic Research Fund.
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
Aceto, L., Birgisson, A., Ingólfsdóttir, A., Mousavi, M.R., Reniers, M.A.: Rule formats for determinism and idempotence. Science of Computer Programming 77(7-8), 889–907 (2012)
Aceto, L., Cimini, M., Ingólfsdóttir, A., Mousavi, M.R., Reniers, M.A.: SOS rule formats for zero and unit elements. Theoretical Computer Science 412(28), 3045–3071 (2011)
Aceto, L., Cimini, M., Ingólfsdóttir, A., Mousavi, M.R., Reniers, M.A.: Rule formats for distributivity. Theoretical Computer Science 458, 1–28 (2012)
Aceto, L., Fokkink, W., Verhoef, C.: Structural operational semantics. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, ch. 3, pp. 197–292. Elsevier Science, Dordrecht (2001)
Aceto, L., Goriac, E.I., Ingólfsdóttir, A.: SOS rule formats for idempotent terms and idempotent unary operators (2012), http://www.ru.is/faculty/luca/PAPERS/idemop.pdf
Aceto, L., Ingólfsdóttir, A., Mousavi, M.R., Reniers, M.A.: Algebraic properties for free! Bulletin of the European Association for Theoretical Computer Science 99, 81–104 (2009)
Baeten, J., Bergstra, J., Klop, J.W.: Syntax and defining equations for an interrupt mechanism in process algebra. Fundamenta Informaticae IX(2), 127–168 (1986)
Baeten, J., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories of Communicating Processes. Cambridge Tracts in Theoretical Computer Science, vol. 50. Cambridge University Press (2009)
Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. Journal of the ACM 42(1), 232–268 (1995)
Cranen, S., Mousavi, M.R., Reniers, M.A.: A Rule Format for Associativity. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 447–461. Springer, Heidelberg (2008)
Engelfriet, J., Gelsema, T.: Multisets and structural congruence of the pi-calculus with replication. Theoretical Computer Science 211(1-2), 311–337 (1999)
Fokkink, W.: A complete equational axiomatization for prefix iteration. Information Processing Letters 52(6), 333–337 (1994)
Fokkink, W.: Axiomatizations for the Perpetual Loop in Process Algebra. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 571–581. Springer, Heidelberg (1997)
van Glabbeek, R.J.: The linear time - branching time spectrum I. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, ch. 1, pp. 3–100. Elsevier Science, Dordrecht (2001)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall (1985)
Kleene, S.: Representation of events in nerve nets and finite automata. In: Shannon, C., McCarthy, J. (eds.) Automata Studies, pp. 3–41. Princeton University Press (1956)
Milner, R.: Calculi for synchrony and asynchrony. Theoretical Computer Science 25, 267–310 (1983)
Milner, R.: Communication and Concurrency. Prentice Hall (1989)
Mousavi, M.R., Reniers, M.A., Groote, J.F.: A syntactic commutativity format for SOS. Information Processing Letters 93, 217–223 (2005)
Mousavi, M.R., Reniers, M.A., Groote, J.F.: SOS formats and meta-theory: 20 years after. Theoretical Computer Science 373, 238–272 (2007)
Park, D.M.: Concurrency and Automata on Infinite Sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60, 17–139 (2004)
Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2011)
Sangiorgi, D., Walker, D.: The π-Calculus: A Theory of Mobile Processes. Cambridge University Press (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aceto, L., Goriac, EI., Ingólfsdóttir, A. (2013). SOS Rule Formats for Idempotent Terms and Idempotent Unary Operators. In: van Emde Boas, P., Groen, F.C.A., Italiano, G.F., Nawrocki, J., Sack, H. (eds) SOFSEM 2013: Theory and Practice of Computer Science. SOFSEM 2013. Lecture Notes in Computer Science, vol 7741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35843-2_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-35843-2_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35842-5
Online ISBN: 978-3-642-35843-2
eBook Packages: Computer ScienceComputer Science (R0)