Isabelle/HOL基础

Question

我看过很多有关Isabelle语法和证明策略的文档，但是很少找到关于它基础的资料。我有一些问题，如果有人能抽出时间回答，我会非常感激：

1. 为什么Isabelle/HOL不允许不终止的函数？许多其他语言，如Haskell，允许非终止函数。

2. 哪些符号是Isabelle元语言的一部分？我读到元语言中有全称量词（/\）和蕴含符号（==>），但这些符号在对象级语言中也有对应物（∀和-->）。我理解-->是一个类型为bool => bool => bool的对象级函数。但是，∀和∃是如何定义的呢？它们是对象级布尔函数吗？如果是，它们是不可计算的（考虑无限域）。我注意到我可以用∀和∃编写布尔函数，但它们是不可计算的。那么∀和∃是什么？它们是否是对象级的一部分？如果是，它们是如何定义的？

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

4. 据我所知，Isabelle是一种严格的编程语言。我该如何使用无限对象？比如，无限列表。在Isabelle/HOL中是否可能实现？

如果这些问题太基础，请原谅。我似乎找不到关于Isabelle元理论的好教程。如果有人能向我推荐关于这些主题的好教程，我会非常感激。

非常感谢！

- Martin Copes

---

这听起来像是许多不同的问题。您应该逐个提出它们。 - dfeuer

首先，如果你想要一个证明助手，那么你不能同时拥有它；可以参考类型和定理、程序和证明之间的关系。 - Random Dev

参见命题即类型，“无类型λ演算或带有一种用于一般递归的构造的类型化λ演算（有时称为不动点运算符）允许定义任何有效计算函数，但具有不可解的停机问题。” - Random Dev

@Carsten 确实如此，但是Isabelle不允许空类型--一个有效的Isabelle术语undefined可以居住在任何类型中。因此，标准的类型理论论证“如果我们有完全递归，我们将能够居住一切，从而证明一切”是不足够的。我对Isabelle知之甚少，但从类型理论的角度来看，它在某些方面看起来相当遥远。 - chi

@Carsten Isabelle在“作弊”时使用sorry，而Coq中使用Admitted。据我所知，仅使用undefined不会导致Isabelle中的不一致性，因为所有类型都必须被占用。我对Isabelle<->类型理论之间的确切关系感到非常不确定，但看起来命题在Isabelle中不是类型。希望一些Isabelle专家能够澄清一些问题。 - chi

Answer 1

1. 在Isabelle中，你可以定义非终止（即部分）函数（详见Function package manual（第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参考手册的第2.1节中找到有关此信息的一些内容，并且可能还可以在手册的其他地方找到更多信息。

其他所有内容（包括∀和∃，它们确实操作布尔表达式）都是在对象逻辑（通常是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并不是一种编程语言，尽管它有一个代码生成器，允许将Isabelle函数导出为代码到编程语言，只要你可以为涉及的所有函数提供代码方程。

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

命题不是布尔值——事实上，在Isabelle/Pure中没有一种方法声明命题不成立。

然后，HOL定义（或者说公理化）了布尔值，并且也公理化了从布尔值到命题的强制转换：Trueprop :: bool ⇒ prop

4. Isabelle不是一种编程语言，除此之外，全局性并不意味着你必须限制自己在有限结构上。即使在总体程序设计语言中，你也可以拥有无限列表。（参见Idris的codata）

Isabelle是一个定理证明器，从逻辑上讲，无限对象可以通过对它们进行公理化，然后使用你拥有的公理和规则来推断这些对象。

例如，HOL假设存在一个无限类型并在其上定义了自然数。那已经给你访问nat ⇒ 'a函数，这些函数本质上是无限列表。

你也可以使用（协同）数据类型包将无限列表和其他无限数据结构定义为有界自然函子。

- Manuel Eberl

Answer 2

让我为您的两个问题补充一些内容。

1）为什么Isabelle/HOL不允许不终止的函数？像Haskell这样的许多其他语言确实允许非终止函数。

简而言之：Isabelle/HOL不需要终止，但需要函数的完全性（即每个输入都有一个特定的结果）。完全性并不意味着将函数转录到（函数式）编程语言后实际上会终止甚至根本无法计算。

因此，谈论终止有点误导人，尽管它受到鼓励，因为Isabelle/HOL的函数包使用关键字termination来证明一些属性P，我将在下面稍微讲解一下。

一方面，“终止”这个词可能对更广泛的受众听起来更直观。另一方面，对P进行更精确的描述将是函数调用图的良好基础性。

别误会，termination对于属性P来说并不是一个真正的坏名称，甚至可以证明，函数包中实现的许多技术与术语重写或函数式编程（如大小变化原则、依赖对、词典顺序等）非常接近终止技术。

我只是说它可能会误导人。为什么这种情况也触及到了OP的第4个问题。

4）据我所知，Isabelle是一种严格的编程语言。我怎样才能使用无限的对象？比如，无限列表。在Isabelle/HOL中是否有可能？ Isabelle/HOL不是编程语言，特别是它没有任何评估策略（我们可以选择说：它有您喜欢的任何评估策略）。

而这就是为什么“终止”这个词很容易引起误解的原因（鼓掌声）：如果没有评估策略并且我们有一个函数f的终止，人们可能期望f会在独立于所使用的策略的情况下终止。但事实并非如此。函数f的termination证明确保f是定义良好的。即使f是可计算的，P的证明也仅确保存在一种评估策略，使得f终止。

（顺便说一句：我在这里所说的“策略”通常受到Isabelle/HOL中所谓的cong规则（即一致性规则）的影响。）

举个例子，可以轻松证明这个函数（请见函数包文档中的第10.1节同余规则和求值顺序）：

fun f' :: "nat ⇒ bool"
where
  "f' n ⟷ f' (n - 1) ∨ n = 0"

在添加了cong规则后，终止（按照“终止”的定义）的意思是：

lemma [fundef_cong]:
  "Q = Q' ⟹ (¬ Q' ⟹ P = P') ⟹ (P ∨ Q) = (P' ∨ Q')"
by auto

基本上，这个说法是逻辑或应该从右向左“评估”。然而，如果你用OCaml写同样的函数，它会导致堆栈溢出...

- chris

Answer 3

编辑：这个答案并不完全正确，请查看下面Lars的评论。

很遗憾，我没有足够的声望将其发布为评论，所以我试着回答一下（请记住，我不是Isabelle专家，但我曾经有过类似的问题）：

1）思路是证明关于已定义函数的陈述。我不确定您对可计算性理论有多熟悉，但想想停机问题以及大多数不可判定问题的根源（例如接受问题）。想象一下定义一个你不能证明其终止的函数。当给出输入“ABC”且不进入无限循环时，你如何证明它仍然返回数字42？

如果您限制自己使用终止函数，则可以更多地证明它们，从本质上讲进行权衡（或者至少这是我看到的方式）。

这些思想源于建构主义和直觉主义，我建议您查看Robert Harper非常有趣的讲座系列：https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_YncjXRzdGq2SjKv5F2J8HUFeqN 关于类型论。您应该特别关注排中律的缺失部分：http://youtu.be/3JHTb6b1to8?t=15m34s。

2）请参考Manuel的答案。

3,4）再次参考Manuel的答案，牢记直觉主义逻辑：“基本实体不是布尔值，而是证明某些东西为真”。

对我来说，调整到这种思考方式花了很长时间，而且我仍然不确定自己是否理解它。但我认为关键是要理解这是一种完全不同的思考方式。

- Eduard Nicodei

---

限制Isabelle/HOL的逻辑与停机问题或构造主义无关。HOL不是直觉主义逻辑！相反，非终止函数很容易使逻辑不一致，从而允许用户证明错误。考虑由“f n = 1 + f n”定义的f。通过在两侧减去“f n”，我们证明了“0 = 1”。有办法解决这个问题（例如，通过为非终止添加单独的值），但推理变得更加麻烦。LCF或Isabelle的HOLCF是允许非终止函数的逻辑的示例。 - Lars Noschinski

@LarsNoschinski 哦，好的，那非常有帮助，谢谢你的澄清！ - Eduard Nicodei