Isabelle/HOL 基金会

Question

我看过很多关于 Isabelle 的语法和证明策略的文档。然而，我对它的基础知之甚少。我有几个问题，如果有人能花时间回答，我将不胜感激:

为什么 Isabelle/HOL 不承认不终止的函数？许多其他语言(例如 Haskell)确实承认非终止函数。

哪些符号是伊莎贝尔元语言的一部分？我读到元语言中有通用量化 ( /\ ) 和蕴涵 ( ==> ) 的符号。然而，这些符号在对象级语言中有它们的对应物(∀ 和 -->)。我明白 -->是类型 bool => bool => bool 的对象级函数.然而，∀ 和 ∃ 是如何定义的？它们是对象级 bool 函数吗？如果是这样，则它们不可计算(考虑无限域)。我注意到我可以用 ∀ 和 ∃ 的形式编写 bool 函数，但它们不可计算。那么什么是∀和∃？它们是对象级的一部分吗？如果有，它们是如何定义的？

Isabelle 定理只是 bool 表达式吗？那么 bool 值是元语言的一部分吗？

据我所知，Isabelle 是一种严格的编程语言。如何使用无限对象？比方说，无限列表。 Isabelle/HOL 可以吗？

对不起，如果这些问题是非常基本的。我似乎没有找到关于伊莎贝尔元理论的好教程。如果有人可以向我推荐有关这些主题的好教程，我会很高兴。

非常感谢你。

Answer 1

1) 您可以在 Isabelle 中定义非终止(即部分)函数(参见 Function package manual (section 8))。然而，偏函数更难推理，因为无论何时你想使用它的定义方程(psimps 规则，它取代了正常函数的 simps 规则)，你必须证明函数终止于首先是特定的输入。

一般来说，诸如非定义性和非终止性之类的东西在逻辑中总是有问题的——例如，考虑函数“定义”f x = f x + 1 .如果我们将其作为ℤ(整数)上的等式，我们可以减去f x从两边得到0 = 1 .在 Haskell 中，通过说这不是 ℤ 上的方程，而是 ℤ ∪ ⊥(整数加底数)和非终止函数 f 上的方程，这个问题得到了“解决”。计算结果为 ⊥，并且'⊥ + 1 = ⊥'，所以一切正常。

但是，如果您的逻辑中的每个表达式都可能计算为 ⊥ 而不是“正确的”值，则此逻辑中的推理将变得非常乏味。这就是为什么 Isabelle/HOL 选择将自己限制在全部功能上的原因；必须用 undefined 之类的东西来模仿偏心之类的东西(这是一个您一无所知的任意值)或选项类型。

2)我不是 Isabelle/Pure(元逻辑)的专家，但最重要的符号肯定是

⋀ (通用元量词)

⟹ (元含义)

≡ (元平等)

&&& (元连词，根据 ⟹ 定义)

Pure.term , Pure.prop , Pure.type , Pure.dummy_pattern , Pure.sort_constraint ，它实现了某些我不太了解的内部内部功能。

您可以在 Isabelle/Isar Reference Manual 中找到有关此的一些信息。在第 2.1 节中，可能在手册的其他地方更多。

其他所有内容(包括 ∀ 和 ∃，它们确实对 bool 表达式进行操作)都在对象逻辑中定义(通常为 HOL)。您可以在 ~~/src/HOL/HOL.thy 中找到定义，而不是公理化。 (其中 ~~ 表示 Isabelle 根目录):

All_def:      "All P     ≡ (P = (λx. True))"
Ex_def:       "Ex P      ≡ ∀Q. (∀x. P x ⟶ Q) ⟶ Q"

另请注意，许多(如果不是大多数)Isabelle 函数通常是不可计算的。伊莎贝尔是 不是 一种编程语言，尽管它确实有一个代码生成器，它允许将 Isabelle 函数作为代码导出到编程语言，只要您可以为所有涉及的函数提供代码方程。

3)
伊莎贝尔定理是一种复杂的数据类型(参见 ~~/src/Pure/thm.ML)，其中包含大量信息，但最重要的部分当然是命题。命题是来自 Isabelle/Pure 的东西，它实际上只有命题和函数。 (还有 itself 和 dummy ，但你可以忽略它们)。

命题不是 bool 值——事实上，甚至没有办法声明一个命题在 Isabelle/Pure 中不成立。

HOL 然后定义(或者更确切地说是公理化) bool 值，并且还公理化了从 bool 值到命题的强制转换: Trueprop :: bool ⇒ prop
4) 伊莎贝尔是 不是 一种编程语言，除此之外，整体性并不意味着您必须将自己限制在有限的结构中。即使在完整的编程语言中，您也可以拥有无​​限列表。 (参见 idris 的 codata)

Isabelle 是定理证明者，从逻辑上讲，可以通过公理化它们然后使用您拥有的公理和规则对它们进行推理来处理无限对象。

例如，HOL 假设存在无限类型并在其上定义自然数。这已经使您可以访问功能 nat ⇒ 'a ，它们本质上是无限列表。

您还可以使用 (co-)datatype package 将无限列表和其他无限数据结构定义为辅助数据类型。 ，它基于有界自然仿函数。