A note on guarded recursion
Résumé
We introduce a logical notion of well-guardedness for recursive terms on arbitrary signatures defined in Plotkin's framework of structural operational specifications, restricted by de Simone's realizability requirements. We then 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. For well-guarded terms, the simplified rule is logically equivalent to the general rule, but is has not the draw-back to ask for premises more complex that consequences.