寻找等效的程序来验证类型化Lambda演算

Question

我有以下证明，假设A和B，可以得出A？B：

我正在尝试使用Haskell风格的语法对来键入lambda演算中找到与此证明等效的程序。假定a：A和b：B。

将这种证明转换为类型，可以得出：假设x ::（B，A），则想构造（A，B）。

我为此陷入两个选择之间：

（1）（？x。（x，x））（b，a）

（2）（（b，a），（b，a））

我相信选项（2）是正确的，因为它不是被证明的暗示（转换为函数）。但是，我不确定我的推理是否正确。由于我们正在根据类型考虑此证明，因此x ::（B，A）在哪里更合适（1）？任何见解都表示赞赏。

Answer 1

这是正确的推理路线。我们将从一个“洞”开始，然后根据下一个证明规则慢慢扩大该洞。我将跟随您的a思路，并假设范围内有两个术语，分别命名为（type A）和b（type of B）。我们从一个洞开始：

_

最后使用的证明规则是？-E（消除箭头）；在lambda演算中，这对应于功能应用程序。

_ _

由于第二个孔的证明项较小，因此我们从第一个开始。那个规则是？-I（连词介绍）；相应的lambda项是(,)。

_ (_, _)

并列介绍使用的假设是B和A; 我们相应的lambda项是b和a。所以：

_ (b, a)

证明项的这一分支到此结束。现在我们必须上升左分支。提供功能的规则是？-I ^？（使用变量？的箭头介绍）；在lambda演算中，相应的术语是lambda。

(\? -> _) (b, a)

接下来是合取介绍。和以前一样，对应的项是(,)。

(\? -> (_, _)) (b, a)

证明在这里分支。为了与上一步保持一致，我们将首先沿右分支，然后沿左分支。右分支中的下一个规则是？-E ₁（连接消除1）；Lambda演算中的对应项是fst。

(\? -> (_, fst _)) (b, a)

该分支的最后一条规则是？（变量消除变量？）；相应的lambda演算项为?。

(\? -> (_, fst ?)) (b, a)

现在遵循证明的左分支，在lambda演算中使用的下一个规则是？-E ₂（合取消除2）snd。

(\? -> (snd _, fst ?)) (b, a)

最终使用的规则还是变量消除（再次使用variable ?）。

(\? -> (snd ?, fst ?)) (b, a)

现在，我们到达了证明项每个分支的顶部（并填补了所有空白），因此我们完成了lambda演算项的构建。看起来它与您的（1）相对应！您能看到证明项将如何更改以与您的（2）相对应吗？