TY - GEN

T1 - Formal verifications of call-by-need and call-by-name evaluations with mutual recursion

AU - Mizuno, Masayuki

AU - Sumii, Eijiro

N1 - Funding Information:
We thank the anonymous reviewers for valuable comments and suggestions. This work was partially supported by JSPS KAKENHI Grant Numbers JP19J11926, JP15H02681, JP16K12409 and the Asahi Glass Foundation.
Publisher Copyright:
© Springer Nature Switzerland AG 2019.

PY - 2019

Y1 - 2019

N2 - We present new proofs—formalized in the Coq proof assistant—of the correspondence among call-by-need and (various definitions of) call-by-name evaluations of λ-calculus with mutually recursive bindings. For non-strict languages, the equivalence between high-level specifications (call-by-name) and typical implementations (call-by-need) is of foundational interest. A particular milestone is Launchbury’s natural semantics of call-by-need evaluation and proof of its adequacy with respect to call-by-name denotational semantics, which are recently formalized in Isabelle/HOL by Breitner (2018). Equational theory by Ariola et al. is another well-known formalization of call-by-need. Mutual recursion is especially challenging for their theory: reduction is complicated by the traversal of dependency (the “need” relation), and the correspondence of call-by-name and call-by-need reductions becomes non-trivial, requiring sophisticated structures such as graphs or infinite trees. In this paper, we give arguably simpler proofs solely based on (finite) terms and operational semantics, which are easier to handle for proof assistants (Coq in our case). Our proofs can be summarized as follows: (1) we prove the equivalence between Launchbury’s call-by-need semantics and heap-based call-by-name natural semantics, where we define a sufficiently (but not too) general correspondence between the two heaps, and (2) we also show the correspondence among three styles of call-by-name semantics: (i) the natural semantics used in (1); (ii) closure-based natural semantics that informally corresponds to Launchbury’s denotational semantics; and (iii) conventional substitution-based semantics.

AB - We present new proofs—formalized in the Coq proof assistant—of the correspondence among call-by-need and (various definitions of) call-by-name evaluations of λ-calculus with mutually recursive bindings. For non-strict languages, the equivalence between high-level specifications (call-by-name) and typical implementations (call-by-need) is of foundational interest. A particular milestone is Launchbury’s natural semantics of call-by-need evaluation and proof of its adequacy with respect to call-by-name denotational semantics, which are recently formalized in Isabelle/HOL by Breitner (2018). Equational theory by Ariola et al. is another well-known formalization of call-by-need. Mutual recursion is especially challenging for their theory: reduction is complicated by the traversal of dependency (the “need” relation), and the correspondence of call-by-name and call-by-need reductions becomes non-trivial, requiring sophisticated structures such as graphs or infinite trees. In this paper, we give arguably simpler proofs solely based on (finite) terms and operational semantics, which are easier to handle for proof assistants (Coq in our case). Our proofs can be summarized as follows: (1) we prove the equivalence between Launchbury’s call-by-need semantics and heap-based call-by-name natural semantics, where we define a sufficiently (but not too) general correspondence between the two heaps, and (2) we also show the correspondence among three styles of call-by-name semantics: (i) the natural semantics used in (1); (ii) closure-based natural semantics that informally corresponds to Launchbury’s denotational semantics; and (iii) conventional substitution-based semantics.

UR - http://www.scopus.com/inward/record.url?scp=85076706625&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85076706625&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-34175-6_10

DO - 10.1007/978-3-030-34175-6_10

M3 - Conference contribution

AN - SCOPUS:85076706625

SN - 9783030341749

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 181

EP - 201

BT - Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Proceedings

A2 - Lin, Anthony Widjaja

PB - Springer

T2 - 17th Asian Symposium on Programming Languages and Systems, APLAS 2019

Y2 - 1 December 2019 through 4 December 2019

ER -