Abstract
In this paper I distinguish two (pre)congruence requirements for semantic equivalences and preorders on processes given as closed terms in a system description language with a recursion construct. A lean congruence preserves equivalence when replacing closed subexpressions of a process by equivalent alternatives. A full congruence moreover allows replacement within a recursive specification of subexpressions that may contain recursion variables bound outside of these subexpressions. I establish that bisimilarity is a lean (pre)congruence for recursion for all languages with a structural operational semantics in the ntyft/ntyxt format. Additionally, it is a full congruence for the tyft/tyxt format.
Original language | English |
---|---|
Title of host publication | 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
Publisher | Institute of Electrical and Electronics Engineers |
Number of pages | 11 |
ISBN (Electronic) | 978-1-5090-3018-7 |
ISBN (Print) | 978-1-5090-3019-4 |
DOIs | |
Publication status | Published - 10 Aug 2017 |
Event | 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science - Reykjavik, Reykjavik, Iceland Duration: 20 Jun 2017 → 23 Jun 2017 http://lics.siglog.org/lics17/ |
Conference
Conference | 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science |
---|---|
Abbreviated title | LICS 2017 |
Country/Territory | Iceland |
City | Reykjavik |
Period | 20/06/17 → 23/06/17 |
Internet address |