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...

Full description

Bibliographic Details
Main Author: van Glabbeek, Rob
Format: Text
Language:unknown
Published: 2017
Subjects:
Computer Science - Logic in Computer Science
F.3.2
Iceland
Online Access:http://arxiv.org/abs/1704.03160
id ftarxivpreprints:oai:arXiv.org:1704.03160
record_format openpolar
spelling ftarxivpreprints:oai:arXiv.org:1704.03160 2023-09-05T13:20:30+02:00 Lean and Full Congruence Formats for Recursion van Glabbeek, Rob 2017-04-11 http://arxiv.org/abs/1704.03160 unknown http://arxiv.org/abs/1704.03160 Computer Science - Logic in Computer Science F.3.2 text 2017 ftarxivpreprints 2023-08-16T14:21:19Z 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. Comment: To appear in: Proc. LICS'17, Reykjavik, Iceland, IEEE Text Iceland ArXiv.org (Cornell University Library)
institution Open Polar
collection ArXiv.org (Cornell University Library)
op_collection_id ftarxivpreprints
language unknown
topic Computer Science - Logic in Computer Science
F.3.2
spellingShingle Computer Science - Logic in Computer Science
F.3.2
van Glabbeek, Rob
Lean and Full Congruence Formats for Recursion
topic_facet Computer Science - Logic in Computer Science
F.3.2
description 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. Comment: To appear in: Proc. LICS'17, Reykjavik, Iceland, IEEE
format Text
author van Glabbeek, Rob
author_facet van Glabbeek, Rob
author_sort van Glabbeek, Rob
title Lean and Full Congruence Formats for Recursion
title_short Lean and Full Congruence Formats for Recursion
title_full Lean and Full Congruence Formats for Recursion
title_fullStr Lean and Full Congruence Formats for Recursion
title_full_unstemmed Lean and Full Congruence Formats for Recursion
title_sort lean and full congruence formats for recursion
publishDate 2017
url http://arxiv.org/abs/1704.03160
genre Iceland
genre_facet Iceland
op_relation http://arxiv.org/abs/1704.03160
_version_ 1776201176302223360

Similar Items