Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion
Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion
复制标题
使用相互递归的 Call-by-Need 和 Call-by-Name 评估的形式验证
DOI：
10.1007/978-3-030-34175-6_10
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Eijiro Sumii
中科院分区：
文献类型：
--
作者：
Masayuki Mizuno;Eijiro Sumii
本文提出了一种新的证明--在Coq proof assistant-of中形式化了--演算的按需调用和按名调用求值之间的对应关系.对于非严格语言，高层规范（按名调用）和典型实现（按需调用）之间的等价性是一个基础性的问题.一个特别的里程碑是Launchbury对按需调用评估的自然语义，以及其对按名称调用指称语义的充分性的证明，这些语义最近由Breitner（2018）在Isabelle/HOL中正式化。Ariola等人的等式理论是另一个著名的按需调用的形式化。互递归对他们的理论来说尤其具有挑战性：通过遍历依赖关系，（“需要”关系），并且按名称调用和按需要调用的约简的对应变得不平凡，需要复杂的结构，例如图或无限树。我们给出了可以说更简单的证明，仅仅基于（有限）术语和操作语义，这对于证明助手（在我们的例子中是Coq）来说更容易处理。我们的证明可以概括如下：（1）我们证明了Launchbury的按需调用语义和基于堆的按名调用自然语义之间的等价性，其中我们定义了一个充分的（但不是太）两个堆之间的一般对应关系，以及（2）我们还显示了三种风格的按名称调用语义之间的对应关系：（i）（1）中使用的自然语义;（ii）非正式地对应于Launchbury的指称语义的基于闭包的自然语义;以及（iii）常规的基于替换的语义。
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-calculuswith 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 recursionis 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.