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.

翻译：我们建立了一个通用框架，用于推理按值调用与按名调用之间的关系。在具有计算效应的语言中，程序的按值调用与按名调用执行通常具有不同但相关的可观察行为。例如，若程序可能发散但无其他效应，则在按值调用下终止时，在按名调用下也会以相同结果终止。我们提出了一种陈述并证明此类性质的技术。关键要素是Levy的按值调用-按名调用演算，我们将其作为推理求值顺序的框架。我们证明，在满足特定条件的计算效应下，表达式按值调用与按名调用到按值调用-按名调用演算的翻译具有相关的可观察行为，并进一步确定了这些条件。进而利用这一事实构造类型在按值调用与按名调用解释之间的映射，并识别出能使这些映射构成伽罗瓦联络的效应的附加性质。这些性质对某些计算效应（如发散）成立，但对其他效应（如可变状态）不成立。由此得到一个通用的推理原则，用以关联按值调用与按名调用。我们将该推理原则应用于发散与非确定性等示例性计算效应。