We establish a general framework for reasoning about the relationship between call-by-value and call-by-name. In languages with side-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 side-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 these properties. 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 side-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 side-effects that imply these maps form a Galois connection. These properties hold for some side-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 side-effects including divergence and nondeterminism.

翻译：我们建立了一个通用框架，用于推理传值调用与传名调用之间的关系。在具有副作用（side-effects）的语言中，传值调用与传名调用的程序执行通常会产生不同但相关的可观察行为（observable behaviours）。例如，若一个程序可能发散（diverge）但除此之外无其他副作用，那么当其以传值调用方式终止时，以传名调用方式也将终止并得到相同结果。我们提出了一套陈述和证明这些属性的技术。关键要素是Levy的传值推送演算（call-by-push-value calculus），我们将其作为推理求值顺序的框架。我们证明，在特定副作用条件下，表达式在传值调用与传名调用下翻译为传值推送演算后，具有相关的可观察行为，这些条件已被我们识别。进而利用这一事实构造类型在传值调用与传名调用解释之间的映射，并识别出使这些映射构成Galois连接的副作用进一步属性。这些属性对某些副作用（如发散）成立，但对另一些副作用（如可变状态）则不成立。由此给出一个连接传值调用与传名调用的通用推理原理。我们将该原理应用于包括发散和非确定性在内的示例副作用。