1

假设我已经在 Isabelle/HOL 中证明了直觉命题逻辑的一些基本命题：

theorem ‹(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))›
proof -
  {
    assume ‹A ⟶ B›
    {
      assume ‹B ⟶ C›
      {
        assume ‹A›
        with ‹A ⟶ B› have ‹B› by (rule mp)
        with ‹B ⟶ C› have ‹C› by (rule mp)
      }
      hence ‹A ⟶ C› by (rule impI)
    }
    hence ‹(B ⟶ C) ⟶ (A ⟶ C)› by (rule impI)
  }
  thus ?thesis by (rule impI)
qed

我从 Curry-Howard 对应关系中知道，命题对应于某种类型(a -> b) -> ((b -> c) -> (a -> c))，而证明对应于某个术语，都在某种类型理论中（例如，在简单类型的 λ 演算中）。从证明的结构，我知道对应的简单类型 λ-项是λf:a→b. λg:b→c. λx:a. f(g(x))。

有没有办法让伊莎贝尔为我建造这个？

我在 Isabelle 中查找了程序提取，据我所知，它主要指的是其他东西：你在 Isabelle 中编写函数式程序，证明关于它们的事情，然后它提供某种对 Haskell 或 ML 的翻译。

我也知道 HOL 与依赖类型理论不同，我理解它具有更强的 Curry-Howard 风格。我知道 HOL 本身在概念上有点像多态 λ-演算，并且我发现了一些关于 HOL 如何是类型论中逻辑的浅层编码的简要说明，但如果能提供更多上下文将不胜感激。我几乎无法将所有这些不同的证明助手及其相关基础如何联系在一起，也许更多的历史背景也会有所帮助。不幸的是，围绕 Isabelle、Coq 等的文档似乎有点乱。特别是对于伊莎贝尔，我似乎经常发现已经过时 20 年的信息。

4

0 回答 0