Lean and full congruence formats for recursion

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publication2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
PublisherInstitute of Electrical and Electronics Engineers
Number of pages11
ISBN (Electronic)978-1-5090-3018-7
ISBN (Print)978-1-5090-3019-4
DOIs
Publication statusPublished - 10 Aug 2017
Event2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science - Reykjavik, Reykjavik, Iceland
Duration: 20 Jun 201723 Jun 2017
http://lics.siglog.org/lics17/

Conference

Conference2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS 2017
Country/TerritoryIceland
CityReykjavik
Period20/06/1723/06/17
Internet address

Fingerprint

Dive into the research topics of 'Lean and full congruence formats for recursion'. Together they form a unique fingerprint.

Cite this