On guarded recursion

DOI10.1016/0304-3975(91)90231-PMaRDI QIDQ805246zbMATH OpenFDO

Authors Eric Badouel, Philippe Darondeau

Publication date 1991

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(91)90231-P

zbMATH Keywords

process algebrasrecursive terms

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Review text

This paper presents the new logical notion of well-guardedness for recursive terms on arbitrary signatures in process algebras of structural operational semantics. Then the authors suggest a simpler form for the logical rule that gives the behaviour of a recursively defined expression in terms of the behaviour of its unfoldings. The logically equivalence between the simplified rule and the general rule for well-guardedness terms is proved. Finally, an important feature of this simplified rule, that the terms appearing in the premises are always simpler than the terms appearing in the consequence, is discussed.

Recommendations

• Unguardedness mostly means many solutions
• Process expressions and Hoare's logic: Showing and irreconcilability of context-free recursion with Scott's induction rule
• A proof rule for fair termination of guarded commands
• Command algebras, recursion and program transformation
• Guard your daggers and traces: properties of guarded (co-)recursion

Cites work

• A calculus of communicating systems
• A structural approach to operational semantics
• scientific article; zbMATH DE number 3926231 (Why is no real title available?)

Cited in

(8)

• GSOS and finite labelled transition systems
• Vertical implementation
• Bisimulation on speed: a unified approach
• scientific article; zbMATH DE number 1254010 (Why is no real title available?)
• Bisimulation on speed: Lower time bounds
• Unguardedness mostly means many solutions
• Bisimulation on speed: Worst-case efficiency
• Codifying guarded definitions with recursive schemes

This page was built for publication: On guarded recursion

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