我已经看过很多关于Isabelle的语法和证明策略的文档.然而,我几乎找不到它的基础.我有几个问题,如果有人能抽出时间回答,我将非常感激:
为什么Isabelle/HOL不接受不终止的功能？许多其他语言(如Haskell)都承认非终止函数.
什么符号是伊莎贝尔的元语言的一部分？我读到在通用量化(/\)和暗示(==>)的元语言中有符号.但是,这些符号在对象级语言(∀和-->)中具有对应的符号.我知道这-->是一个类型的对象级函数bool => bool => bool.但是,∀和how是如何定义的？它们是对象级布尔函数吗？如果是这样,它们是不可计算的(考虑无限域).我注意到我能够在∀和ther中编写布尔函数,但它们不可计算.那么∀和what是什么？它们是对象级别的一部分吗？如果是这样,他们是如何定义的？
Isabelle定理只是布尔表达式吗？然后布尔是元语言的一部分？
据我所知,Isabelle是一种严格的编程语言.我怎样才能使用无限对象？比方说,无限列表.Isabelle/HOL有可能吗？
对不起,如果这些问题非常基础.我似乎没有找到关于伊莎贝尔元理论的好教程.我很乐意,如果有人可以推荐我这些主题的好教程.
非常感谢你.
Man*_*erl 11
1)您可以在Isabelle中定义非终止(即部分)功能(参见功能包手册(第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,它的履行我不知道很多关于某些内部内部功能.您可以在2.1节中的Isabelle/Isar参考手册中找到相关信息,本手册的其他部分可能更多.
其他所有(包括∀和∃,它们确实对布尔表达式进行操作)都是在对象逻辑中定义的(通常是HOL).您可以在~~/src/HOL/HOL.thy(其中~~表示Isabelle根目录)中找到定义,而不是axiomatisations :
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)
伊莎贝尔是一个定理证明者,从逻辑上讲,无限的物体可以通过对它们进行公理化来对待,然后使用你所拥有的公理和规则对它们进行推理.
例如,HOL假设存在无限类型并定义其上的自然数.这已经允许您访问函数nat ? 'a,这些函数本质上是无限列表.
您还可以使用(co-)数据类型包定义无限列表和其他无限数据结构作为codatatypes ,它基于有界自然仿函数.
让我对你的两个问题补充几点。
\n\n\n\n\n1) 为什么 Isabelle/HOL 不承认不终止的函数？许多其他语言（例如 Haskell）确实承认非终止函数。
\n
简而言之：Isabelle/HOL 不需要终止，而是要求函数的整体性（即函数的每个输入都有一个特定的结果）。整体性并不意味着函数在转录为（函数式）编程语言时实际上正在终止，甚至并不意味着它根本是可计算的。
\n\n因此，谈论终止有点误导，尽管 Isabelle/HOL\ 的函数包使用关键字来termination证明某些属性P这一事实鼓励了这一点，我将在下面多说一些属性。
一方面，“终止”一词对于更广泛的受众来说可能听起来更直观。另一方面，更精确的描述P将是函数调用图的有根据的。
不要误会我的意思，这termination对于属性来说并不是一个坏名字P，甚至可以通过以下事实来证明它是合理的：在函数包中实现的许多技术非常接近术语重写或函数式编程的终止技术（例如大小变化原则、依赖对、字典顺序等）。
我只是说这可能会产生误导。为什么会出现这种情况的答案也涉及OP的问题4。
\n\n\n\n\n4）据我所知Isabelle是一种严格的编程语言。如何使用无限对象？比方说，无限列表。伊莎贝尔/HOL 可以吗？
\n
Isabelle/HOL不是一种编程语言，它特别没有任何评估策略（我们也可以说：它有你喜欢的任何评估策略）。
\n\n这就是为什么“终止”这个词会产生误导（鼓声）：如果没有评估策略并且我们终止了一个函数f，人们可能会期望f终止与所使用的策略无关。但这种情况并非如此。terminationa 的证明确保function了它f是明确定义的。即使f是可计算的，证明也P仅仅确保存在一个终止的评估策略f。
（顺便说一句：我在这里所说的“策略”通常受到 Isabelle/HOL 中所谓的cong规则（即一致性规则）的影响。）
\n\n作为一个例子，证明该函数很简单（请参阅函数包文档中的第 10.1 节同余规则和求值顺序）：
\n\nfun f\' :: "nat \xe2\x87\x92 bool"\nwhere\n "f\' n \xe2\x9f\xb7 f\' (n - 1) \xe2\x88\xa8 n = 0"\ntermination添加 cong-rule 后终止（在定义的意义上）：
lemma [fundef_cong]:\n "Q = Q\' \xe2\x9f\xb9 (\xc2\xac Q\' \xe2\x9f\xb9 P = P\') \xe2\x9f\xb9 (P \xe2\x88\xa8 Q) = (P\' \xe2\x88\xa8 Q\')"\nby auto\n这本质上说明逻辑或应该从右到左“评估”。但是，如果您在 OCaml 中编写相同的函数，则会导致堆栈溢出......
\n