基于伽罗瓦连接刻画传值调用与传名调用

我们建立了一个用于推理传值调用（call-by-value）与传名调用（call-by-name）之间关系的通用框架。在具有计算效应的语言中，程序的传值调用与传名调用执行通常具有不同但相关的可观察行为。例如，若一个程序可能发散但无其他效应，则每当它在传值调用下终止时，它在传名调用下以相同结果终止。我们提出了一种陈述并证明此类性质的技术。其核心要素是 Levy 的传值传名推演演算（call-by-push-value calculus），我们将其用作推理求值序的框架。我们表明，在某些我们所确定的计算效应条件下，表达式到传值传名推演的传值调用与传名调用翻译具有相关的可观察行为。随后我们利用这一事实构造类型之传值调用与传名调用解释之间的映射，并确定效应的进一步性质，这些性质蕴含这些映射构成伽罗瓦连接（Galois connection）。这些性质对部分计算效应（如发散）成立，但对其他（如可变状态）不成立。这给出了一个关联传值调用与传名调用的通用推理原理。我们将该推理原理应用于包括发散与非确定性在内的示例计算效应。