Isabelle/HOL 基金会
Isabelle/HOL foundations
我看过很多关于 Isabelle 的语法和证明策略的文档。然而，我对它的基础知之甚少。我有几个问题，如果有人能花时间回答，我将不胜感激：
为什么 Isabelle/HOL 不接受不终止的函数？ Haskell 等许多其他语言确实承认非终止函数。
哪些符号是伊莎贝尔元语言的一部分？我读到元语言中有用于通用量化 (/\) 和暗示 (==>) 的符号。然而，这些符号在对象级语言中有它们的对应物（∀和-->）。我知道 --> 是类型 bool => bool => bool 的对象级函数。但是，∀和∃是怎么定义的呢？它们是对象级布尔函数吗？如果是这样，它们是不可计算的（考虑无限域）。我注意到我可以用 ∀ 和 ∃ 的热函数编写布尔函数，但它们不可计算。那么∀和∃是什么？它们是对象级的一部分吗？如果有，它们是如何定义的？
伊莎贝尔定理只是布尔表达式吗？那么布尔值是元语言的一部分吗？
据我所知，Isabelle 是一门严格的编程语言。如何使用无限对象？比方说，无限列表。 Isabelle/HOL可以吗?
抱歉，如果这些问题很基础。我似乎没有找到关于伊莎贝尔元理论的好教程。如果有人可以向我推荐有关这些主题的优秀教程，我会很高兴。
非常感谢。
- 您可以在 Isabelle 中定义非终止（即部分）函数（参见 Function package manual (section 8)）。然而，部分函数更难推理，因为无论何时你想使用它的定义方程（
psimps 规则，它取代了普通函数的 simps 规则），你必须证明函数首先终止于该特定输入。
一般来说，非定义和非终止之类的东西在逻辑中总是有问题的——例如，考虑函数“定义”f x = f x + 1。如果我们将其作为ℤ（整数）的等式，我们可以从两边减去 f x 并得到 0 = 1。在 Haskell 中，这个问题通过说这不是 ℤ 上的方程式，而是 ℤ ∪ {⊥}（整数加底）和非终止函数 f 求值来“解决”到⊥，和'⊥ + 1 = ⊥'，所以一切正常。
但是，如果您逻辑中的每个表达式都可能计算为 ⊥ 而不是“正确”值，则此逻辑中的推理将变得非常乏味。这就是为什么 Isabelle/HOL 选择将自己限制在总函数；偏爱之类的东西必须用 undefined（这是一个你一无所知的任意值）或选项类型来模拟。
- 我不是Isabelle/Pure（元逻辑）方面的专家，但最重要的符号肯定是
⋀（通用元量词）⟹（元含义）≡（元相等）&&&（元连词，根据⟹定义）Pure.term、Pure.prop、Pure.type、Pure.dummy_pattern、Pure.sort_constraint，实现了一些我不太了解的内部功能
您可以在第 2.1 节的 Isabelle/Isar Reference Manual 中找到一些相关信息，并且可能在手册的其他地方找到更多信息。
其他所有内容（包括∀和∃，它们确实在布尔表达式上运行）都在对象逻辑（通常是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)
伊莎贝尔定理是一个复杂的数据类型（参见~~/src/Pure/thm.ML），包含大量信息，但最重要的部分当然是命题。命题是Isabelle/Pure里的东西，其实只有命题和函数。 （还有 itself 和 dummy，但你可以忽略它们）。
命题 不是 布尔值——事实上，甚至没有一种方法可以说明命题在 Isabelle/Pure.
中不成立
HOL 然后定义（或者说公理化）布尔值并且公理化从布尔值到命题的强制转换：Trueprop :: bool ⇒ prop
- Isabelle 不是 一种编程语言，除此之外，整体性并不意味着您必须将自己限制在有限的结构中。即使在完整的编程语言中，您也可以拥有无限的列表。 (cf. Idris 的
codata)
Isabelle 是定理证明者，从逻辑上讲，无限对象可以通过公理化处理，然后使用您拥有的公理和规则对其进行推理。
例如，HOL 假定存在无限类型并在其上定义自然数。这已经让您可以访问函数 nat ⇒ 'a，它们本质上是无限列表。
您还可以使用基于有界自然函子的 (co-)datatype package 将无限列表和其他无限数据结构定义为共数据类型。
编辑：这个答案不太正确，请查看下面 Lars 的评论。
不幸的是，我没有足够的声誉 post 作为评论，所以这是我的答案（请记住我不是伊莎贝尔的专家，但我也有类似的问题一次):
1) 想法是证明关于定义函数的陈述。我不确定您对可计算性理论有多熟悉，但请考虑一下停机问题以及大多数不可判定性问题源于它的事实（例如验收问题）。想象一下定义一个你无法证明它终止的函数。当给定输入 "ABC" 并且它不会进入无限循环时，你如何仍然证明它 returns 数字 42？
如果你将自己限制在终止函数上，你可以证明更多关于它们的信息，本质上是一种权衡（或者至少我是这样看的）。
这些想法源于建构主义和直觉主义，我建议您查看 Robert Harper 非常有趣的讲座系列：https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_YncjXRzdGq2SjKv5F2J8HUFeqN 关于类型理论
你应该特别看看关于排中律不存在的部分：http://youtu.be/3JHTb6b1to8?t=15m34s
2) 查看 Manuel 的回答。
3,4) 再次查看 Manuel 的回答，牢记直觉逻辑："the fundamental entity is not the boolean, but rather the proof that something is true".
对我来说，我花了很长时间才适应这种思维方式，但我仍然不确定自己是否理解它。我认为关键是要理解它是一种或多或少完全不同的思维方式。
让我对你的两个问题补充几点。
1) Why doesn't Isabelle/HOL admit functions that do not terminate? Many other languages such as Haskell do admit non-terminating functions.
简而言之：Isabelle/HOL不需要终止，但总（即每个都有一个特定的结果函数的输入）。整体性并不意味着函数在转录为（函数式）编程语言时实际上正在终止，甚至它根本是可计算的。
因此，谈论终止有点误导，尽管Isabelle/HOL的功能包使用关键字termination这一事实令人鼓舞为了证明一些 属性 P 我将在下面多说一点。
一方面，"termination" 一词对于更广泛的听众来说可能听起来更直观。另一方面，P 的更精确描述是 函数调用图的有根据性 .
不要误会我的意思，termination 对于 属性 P 来说并不是一个坏名字，它甚至可以通过以下事实来证明：函数包非常接近术语重写或函数式编程的终止技术（如大小变化原则、依赖对、词典顺序等）。
我只是说这可能会产生误导。为什么会这样的答案也涉及到 OP 的问题 4。
4) As far as I know Isabelle is a strict programming language. How can I use infinite objects? Let's say, infinite lists. Is it possible in Isabelle/HOL?
Isabelle/HOL 不是一种编程语言，具体来说不是有任何评估策略（我们也可以说：它有任何你喜欢的评估策略）。
这就是 termination 这个词具有误导性的原因（鼓声）：如果没有评估策略而我们有函数终止 f，人们可能期望 f 终止 独立于使用的策略 。但这种情况并非如此。 function 的 termination 证明可以确保 f 是明确定义的。即使 f 是可计算的，P 的证明也只是确保 存在一个评估策略 ，f 终止。
（顺便说一句：我在这里所说的 "strategy" 通常受到 [=83= 中所谓的 cong 规则（即同余规则）的影响].)
举个例子，证明函数很简单（参见函数包文档中的第 10.1 同余规则和求值顺序）：
fun f' :: "nat ⇒ bool"
where
"f' n ⟷ f' (n - 1) ∨ n = 0"
在添加 cong-rule 后终止（在 termination 定义的意义上）：
lemma [fundef_cong]:
"Q = Q' ⟹ (¬ Q' ⟹ P = P') ⟹ (P ∨ Q) = (P' ∨ Q')"
by auto
这基本上说明逻辑或应该从右到左 "evaluated"。但是，如果您编写相同的函数，例如在 OCaml 中它会导致堆栈溢出 ...
我看过很多关于 Isabelle 的语法和证明策略的文档。然而，我对它的基础知之甚少。我有几个问题，如果有人能花时间回答，我将不胜感激：
为什么 Isabelle/HOL 不接受不终止的函数？ Haskell 等许多其他语言确实承认非终止函数。
哪些符号是伊莎贝尔元语言的一部分？我读到元语言中有用于通用量化 (
/\) 和暗示 (==>) 的符号。然而，这些符号在对象级语言中有它们的对应物（∀和-->）。我知道-->是类型bool => bool => bool的对象级函数。但是，∀和∃是怎么定义的呢？它们是对象级布尔函数吗？如果是这样，它们是不可计算的（考虑无限域）。我注意到我可以用 ∀ 和 ∃ 的热函数编写布尔函数，但它们不可计算。那么∀和∃是什么？它们是对象级的一部分吗？如果有，它们是如何定义的？伊莎贝尔定理只是布尔表达式吗？那么布尔值是元语言的一部分吗？
据我所知，Isabelle 是一门严格的编程语言。如何使用无限对象？比方说，无限列表。 Isabelle/HOL可以吗?
抱歉，如果这些问题很基础。我似乎没有找到关于伊莎贝尔元理论的好教程。如果有人可以向我推荐有关这些主题的优秀教程，我会很高兴。
非常感谢。
- 您可以在 Isabelle 中定义非终止（即部分）函数（参见 Function package manual (section 8)）。然而，部分函数更难推理，因为无论何时你想使用它的定义方程（
psimps规则，它取代了普通函数的simps规则），你必须证明函数首先终止于该特定输入。
一般来说，非定义和非终止之类的东西在逻辑中总是有问题的——例如，考虑函数“定义”f x = f x + 1。如果我们将其作为ℤ（整数）的等式，我们可以从两边减去 f x 并得到 0 = 1。在 Haskell 中，这个问题通过说这不是 ℤ 上的方程式，而是 ℤ ∪ {⊥}（整数加底）和非终止函数 f 求值来“解决”到⊥，和'⊥ + 1 = ⊥'，所以一切正常。
但是，如果您逻辑中的每个表达式都可能计算为 ⊥ 而不是“正确”值，则此逻辑中的推理将变得非常乏味。这就是为什么 Isabelle/HOL 选择将自己限制在总函数；偏爱之类的东西必须用 undefined（这是一个你一无所知的任意值）或选项类型来模拟。
- 我不是Isabelle/Pure（元逻辑）方面的专家，但最重要的符号肯定是
⋀（通用元量词）⟹（元含义）≡（元相等）&&&（元连词，根据⟹定义）Pure.term、Pure.prop、Pure.type、Pure.dummy_pattern、Pure.sort_constraint，实现了一些我不太了解的内部功能
您可以在第 2.1 节的 Isabelle/Isar Reference Manual 中找到一些相关信息，并且可能在手册的其他地方找到更多信息。
其他所有内容（包括∀和∃，它们确实在布尔表达式上运行）都在对象逻辑（通常是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)
伊莎贝尔定理是一个复杂的数据类型（参见~~/src/Pure/thm.ML），包含大量信息，但最重要的部分当然是命题。命题是Isabelle/Pure里的东西，其实只有命题和函数。 （还有 itself 和 dummy，但你可以忽略它们）。
命题 不是 布尔值——事实上，甚至没有一种方法可以说明命题在 Isabelle/Pure.
中不成立HOL 然后定义（或者说公理化）布尔值并且公理化从布尔值到命题的强制转换：Trueprop :: bool ⇒ prop
- Isabelle 不是 一种编程语言，除此之外，整体性并不意味着您必须将自己限制在有限的结构中。即使在完整的编程语言中，您也可以拥有无限的列表。 (cf. Idris 的
codata)
Isabelle 是定理证明者，从逻辑上讲，无限对象可以通过公理化处理，然后使用您拥有的公理和规则对其进行推理。
例如，HOL 假定存在无限类型并在其上定义自然数。这已经让您可以访问函数 nat ⇒ 'a，它们本质上是无限列表。
您还可以使用基于有界自然函子的 (co-)datatype package 将无限列表和其他无限数据结构定义为共数据类型。
编辑：这个答案不太正确，请查看下面 Lars 的评论。
不幸的是，我没有足够的声誉 post 作为评论，所以这是我的答案（请记住我不是伊莎贝尔的专家，但我也有类似的问题一次):
1) 想法是证明关于定义函数的陈述。我不确定您对可计算性理论有多熟悉，但请考虑一下停机问题以及大多数不可判定性问题源于它的事实（例如验收问题）。想象一下定义一个你无法证明它终止的函数。当给定输入 "ABC" 并且它不会进入无限循环时，你如何仍然证明它 returns 数字 42？
如果你将自己限制在终止函数上，你可以证明更多关于它们的信息，本质上是一种权衡（或者至少我是这样看的）。
这些想法源于建构主义和直觉主义，我建议您查看 Robert Harper 非常有趣的讲座系列：https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_YncjXRzdGq2SjKv5F2J8HUFeqN 关于类型理论
你应该特别看看关于排中律不存在的部分：http://youtu.be/3JHTb6b1to8?t=15m34s
2) 查看 Manuel 的回答。
3,4) 再次查看 Manuel 的回答，牢记直觉逻辑："the fundamental entity is not the boolean, but rather the proof that something is true".
对我来说，我花了很长时间才适应这种思维方式，但我仍然不确定自己是否理解它。我认为关键是要理解它是一种或多或少完全不同的思维方式。
让我对你的两个问题补充几点。
1) Why doesn't Isabelle/HOL admit functions that do not terminate? Many other languages such as Haskell do admit non-terminating functions.
简而言之：Isabelle/HOL不需要终止，但总（即每个都有一个特定的结果函数的输入）。整体性并不意味着函数在转录为（函数式）编程语言时实际上正在终止，甚至它根本是可计算的。
因此，谈论终止有点误导，尽管Isabelle/HOL的功能包使用关键字termination这一事实令人鼓舞为了证明一些 属性 P 我将在下面多说一点。
一方面，"termination" 一词对于更广泛的听众来说可能听起来更直观。另一方面，P 的更精确描述是 函数调用图的有根据性 .
不要误会我的意思，termination 对于 属性 P 来说并不是一个坏名字，它甚至可以通过以下事实来证明：函数包非常接近术语重写或函数式编程的终止技术（如大小变化原则、依赖对、词典顺序等）。
我只是说这可能会产生误导。为什么会这样的答案也涉及到 OP 的问题 4。
4) As far as I know Isabelle is a strict programming language. How can I use infinite objects? Let's say, infinite lists. Is it possible in Isabelle/HOL?
Isabelle/HOL 不是一种编程语言，具体来说不是有任何评估策略（我们也可以说：它有任何你喜欢的评估策略）。
这就是 termination 这个词具有误导性的原因（鼓声）：如果没有评估策略而我们有函数终止 f，人们可能期望 f 终止 独立于使用的策略 。但这种情况并非如此。 function 的 termination 证明可以确保 f 是明确定义的。即使 f 是可计算的，P 的证明也只是确保 存在一个评估策略 ，f 终止。
（顺便说一句：我在这里所说的 "strategy" 通常受到 [=83= 中所谓的 cong 规则（即同余规则）的影响].)
举个例子，证明函数很简单（参见函数包文档中的第 10.1 同余规则和求值顺序）：
fun f' :: "nat ⇒ bool"
where
"f' n ⟷ f' (n - 1) ∨ n = 0"
在添加 cong-rule 后终止（在 termination 定义的意义上）：
lemma [fundef_cong]:
"Q = Q' ⟹ (¬ Q' ⟹ P = P') ⟹ (P ∨ Q) = (P' ∨ Q')"
by auto
这基本上说明逻辑或应该从右到左 "evaluated"。但是，如果您编写相同的函数，例如在 OCaml 中它会导致堆栈溢出 ...