On Coevaluation Behavior and Equivalence

Angel Zúñiga () and Gemma Bel-Enguix
Additional contact information
Angel Zúñiga: Instituto de Ingeniería, Universidad Nacional Autónoma de México, Mexico City 04510, Mexico
Gemma Bel-Enguix: Instituto de Ingeniería, Universidad Nacional Autónoma de México, Mexico City 04510, Mexico

Mathematics, 2022, vol. 10, issue 20, 1-32

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 (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2022
References: View references in EconPapers View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/10/20/3800/pdf (application/pdf)
https://www.mdpi.com/2227-7390/10/20/3800/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:10:y:2022:i:20:p:3800-:d:942924

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().