We establish a general framework for reasoning about the relationship between call-by-value and call-by-name. In languages with computational effects, call-by-value and call-by-name executions of programs often have different, but related, observable behaviours. For example, if a program might diverge but otherwise has no effects, then whenever it terminates under call-by-value, it terminates with the same result under call-by-name. We propose a technique for stating and proving properties like these. The key ingredient is Levy's call-by-push-value calculus, which we use as a framework for reasoning about evaluation orders. We show that the call-by-value and call-by-name translations of expressions into call-by-push-value have related observable behaviour under certain conditions on computational effects, which we identify. We then use this fact to construct maps between the call-by-value and call-by-name interpretations of types, and identify further properties of effects that imply these maps form a Galois connection. These properties hold for some computational effects (such as divergence), but not others (such as mutable state). This gives rise to a general reasoning principle that relates call-by-value and call-by-name. We apply the reasoning principle to example computational effects including divergence and nondeterminism.

翻译：我们建立了一个通用框架，用于推理按值调用与按名调用之间的关系。在具有计算效应的语言中，程序的按值调用和按名调用执行通常会产生不同但相关的可观察行为。例如，如果一个程序可能发散（diverge）但无其他效应，那么当它在按值调用下终止时，在按名调用下也会以相同结果终止。我们提出了一种用于陈述和证明此类性质的技术，其关键要素是Levy的按值推送调用（call-by-push-value）演算，我们将其用作推理求值顺序的框架。我们证明，在满足特定计算效应条件（我们已识别出这些条件）的情况下，按值调用和按名调用表达式到按值推送调用的翻译具有相关的可观察行为。基于此，我们构建了按值调用与按名调用类型解释之间的映射，并进一步识别出使这些映射构成伽罗瓦联系（Galois connection）的效应性质。这些性质对某些计算效应（如发散）成立，但对其他效应（如可变状态）不成立。由此产生了一个关联按值调用与按名调用的通用推理原则。我们将此推理原则应用于包括发散和非确定性在内的示例计算效应。