SOS rule formats for idempotent terms and idempotent unary operators

•This paper presents a rule format for Structural Operational Semantics that guarantees that a unary operator be idempotent modulo bisimilarity.•The rule format for idempotent unary operations relies on a companion one ensuring that certain terms are idempotent with respect to some binary operator.•The applicability and generality of the rule formats are witnessed by a variety of examples from the literature.

A unary operator f   is idempotent if the equation f(x)=f(f(x))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⊙aa=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. This study also offers a variety of examples showing the applicability of both formats.