Lean and Full Congruence Formats for Recursion
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...
| Main Author: | |
|---|---|
| Format: | Report |
| Language: | unknown |
| Published: |
arXiv
2017
|
| Subjects: | |
| Online Access: | https://dx.doi.org/10.48550/arxiv.1704.03160 https://arxiv.org/abs/1704.03160 |
| Summary: | 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. : To appear in: Proc. LICS'17, Reykjavik, Iceland, IEEE |
|---|