Abstract GSOS rules and a modular treatment of recursive definitions

DOI10.2168/LMCS-9(3:28)2013zbMATH Open1307.68051arXiv1307.2538MaRDI QIDQ2850841FDOQ2850841

Authors: Stefan Milius, Lawrence S. Moss, Daniel Schwencke 

Publication date: 1 October 2013

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: Terminal coalgebras for a functor serve as semantic domains for state-based systems of various types. For example, behaviors of CCS processes, streams, infinite trees, formal languages and non-well-founded sets form terminal coalgebras. We present a uniform account of the semantics of recursive definitions in terminal coalgebras by combining two ideas: (1) abstract GSOS rules l specify additional algebraic operations on a terminal coalgebra; (2) terminal coalgebras are also initial completely iterative algebras (cias). We also show that an abstract GSOS rule leads to new extended cia structures on the terminal coalgebra. Then we formalize recursive function definitions involving given operations specified by l as recursive program schemes for l, and we prove that unique solutions exist in the extended cias. From our results it follows that the solutions of recursive (function) definitions in terminal coalgebras may be used in subsequent recursive definitions which still have unique solutions. We call this principle modularity. We illustrate our results by the five concrete terminal coalgebras mentioned above, e.,g., a finite stream circuit defines a unique stream function.

Full work available at URL: https://arxiv.org/abs/1307.2538

Recommendations

• scientific article; zbMATH DE number 7318985
• scientific article; zbMATH DE number 2086418
• Axiomatizing GSOS with termination
• GSOS and finite labelled transition systems
• Recursive rules with aggregation: a simple unified semantics (extended abstract)
• A Generalized Modality for Recursion
• Recursive rules with aggregation: a simple unified semantics
• Recursive rules with aggregation: a simple unified semantics
• An abstract decision procedure for satisfiability in the theory of recursive data types

zbMATH Keywords

distributive lawcompletely iterative algebraterminal coalgebrassemantics of recursive definitions

Mathematics Subject Classification ID

Theories (e.g., algebraic theories), structure, and semantics (18C10) Abstract data types; algebraic specification (68Q65)

Cited In (14)

• Unguarded recursion on coinductive resumptions
• Corecursion up-to via causal transformations
• Bisimulation and coinduction enhancements: a historical perspective
• Unguarded recursion on coinductive resumptions
• Equations, contractions, and unique solutions
• The Microcosm Principle and Compositionality of GSOS-Based Component Calculi
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• Structural congruence for bialgebraic semantics
• On the key dependent message security of the Fujisaki-Okamoto constructions
• A model of guarded recursion via generalised equilogical spaces
• CIA structures and the semantics of recursion
• Product rules and distributive laws
• Friends with benefits. Implementing corecursion in foundational proof assistants
• Companions, codensity and causality

This page was built for publication: Abstract GSOS rules and a modular treatment of recursive definitions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2850841)