کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
431939 | 1441246 | 2014 | 17 صفحه PDF | دانلود رایگان |
• 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.
Journal: The Journal of Logic and Algebraic Programming - Volume 83, Issue 1, January 2014, Pages 64–80