On guarded recursion (Q805246)

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.