haskell - 在类型化 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 (类型 A)和 b (类型 B)。我们从一个洞开始:

_

最后使用的证明规则是→-E(箭头消除)；在 lambda 演算中，这对应于函数应用。

_ _

由于第二个洞的证明项较小，让我们从那个洞开始。该规则是∧-I(连词介绍)；相应的 lambda 项是 (,) .

_ (_, _)

连词介绍使用的假设是B和 A ;我们对应的 lambda 项是 b和 a .所以:

_ (b, a)

证明项的这一分支到此结束。现在我们必须上升到左分支。用于提供函数的规则是→-Iδ(使用变量δ的箭头引入)；在 lambda 演算中，对应的项是 lambda。

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

接下来是连词介绍。和以前一样，对应的术语是(,) .

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

这里的证明分支。为了与我们之前的操作保持一致，我们将首先遵循右分支，然后是左分支。右分支的下一条规则是∧-E1(合取消元1)； lambda 演算中的对应项是 fst .

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

这个分支的最后一个规则是δ(变量δ的变量消除)；相应的 lambda 演算项是 δ .

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

现在遵循证明的左分支，使用的下一个规则是∧-E2(联合消元2)--snd在 lambda 演算中。

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

使用的最终规则再次是变量消除(再次使用变量 δ )。

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

我们现在已经到达了证明项的每个分支的顶部(并填充了所有漏洞)，因此我们完成了 lambda 演算项的构建。看起来它对应于您的(1)!您能看到证明项必须如何更改才能与您的 (2) 相对应吗？