On Coevaluation Behavior and Equivalence

Abstract

Coevaluation, the coinductive interpretation of standard big-step evaluation rules, is a concise form of semantics, with the same number of rules as in evaluation, which intends to simultaneously describe finite and infinite computations. However, it is known that it is only able to express an infinite computations subset, and, to date, it remains unknown exactly what this subset is. More precisely, coevaluation behavior has several unusual features: there are terms for which evaluation is infinite but that do not coevaluate, it is not deterministic in the sense that there are terms which coevaluate to any value v, and there are terms for which evaluation is infinite but that coevaluate to only one value. In this work, we describe the infinite computations subset which is able to be expressed by coevaluation. More importantly, we introduce a coevaluation extension that is well-behaved in the sense that the finite computations coevaluate exactly as in evaluation and the infinite computations coevaluate exactly as in divergence. Consequently, no unusual features are presented; in particular, this extension captures all infinite computations (not only a subset of them). In addition, as a consequence of thiswell-behavior, we present the expected equivalence between (extended) coevaluation and evaluation union divergence.

Keywords

• big-step semantics
• natural semantics
• coinduction
• coevaluation
• operational semantics
• Coq proof assistant