A unary operator / is idempotent if the equation 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 ⊙ 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 idem-potent with respect to some binary operator.
展开▼
