重访计算的二元性：经典可实现性模型的代数分析

在上个十年的尾声，Krivine 在一系列令人印象深刻的论文中展示了经典可实现性如何提供一种令人惊讶的技术来构建经典理论的模型。特别地，他证明了经典可实现性包含了 Cohen 的力迫法，甚至更进一步，产生了意想不到的集合论模型。延续 Streicher 最初开展的对这些模型的代数分析，Miquel 最近提出在被称为蕴涵代数的新结构内奠定经典可实现性与力迫法的代数基础。这些结构是基于表示蕴涵的内部律的布尔代数的推广。值得注意的是，蕴涵代数允许在同一结构中对程序（即证明）及其类型（即公式）进行恰当解释。蕴涵代数的确切定义立足于通过全称量化与蕴涵呈现逻辑，并且在计算上依赖于按名调用（call-by-name）$\lambda$-演算。在本文中，我们通过引入两种类似结构来考察这一选择的合理性。一方面，我们定义析取代数，其依赖于否定与析取的内部律，并且我们证明它们是蕴涵代数的特例。另一方面，我们引入合取代数，其将焦点置于合取与按值调用（call-by-value）求值策略。我们最终展示了析取代数与合取代数如何在代数上反映按名调用与按值调用之间众所周知的计算二元性。