# Lean and Full Congruence Formats for Recursion

## TL;DR

This paper distinguishes between lean and full congruence formats for recursion in process semantics, proving bisimilarity's congruence properties in various structural operational semantics formats.

## Contribution

It introduces a formal distinction between lean and full congruence formats and proves bisimilarity's congruence properties within these frameworks.

## Key findings

- Bisimilarity is a lean congruence for recursion in ntyft/ntyxt formats.
- Bisimilarity is a full congruence in tyft/tyxt formats.
- The paper clarifies the conditions under which bisimilarity preserves process equivalence.

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