Die*_*ias 5 recursion theorem-proving isabelle
问题
我想知道在 Isabelle 中是否有一种自然的编码方式是这样的语法：
type_synonym Var = string
datatype Value = VInt int | ...
datatype Cmd = Skip | NonDeterministicChoice "Cmd set" | ...
动机是根据非确定性选择定义一些规范命令，例如：
Magic == NonDeterministicChoice {}
Rely c r z = Defined using set compreehension and NonDeterministicChoice
Isabelle 抱怨“Cmd set”中类型“Cmd”的递归出现，即：
不支持通过类型表达式“Cmd set”中的类型构造函数“Set.set”递归出现类型“Cmd”。使用“bnf”命令将“Set.set”注册为有界自然函子以允许嵌套（共）递归通过它
在我使用 set 时查看 Isabelle 错误消息，我无法弄清楚如何在这种情况下为“set”类型注册有界自然函子，因此我决定尝试一种推测性解决方案。
投机解决方案
相反，如果我使用归纳定义的数据类型，例如列表，伊莎贝尔不会抱怨，例如
datatype Cmd = Skip | NonDeterministicChoice "Cmd list" | ...
列表在这里不是正确的抽象，但我试一试看看它是否有效。使用列表的直接效果是，我需要使用序列过滤而不是使用集合理解，然后问题就变成了假设存在两个列表：一个包含Cmd 的所有元素，另一个包含Value 的所有元素。
我声明了两个未解释的常量：
consts Values :: "Value list"
consts Programs :: "Cmd list"
因为列表是有限的，所以将常量解释为“Cmd 的所有元素（感兴趣的）”和“所有值（感兴趣的）”更有意义。比如说，所有感兴趣的元素都是可以在计算机内存中表示的元素。
同理，我可以声明一个常量 NonDeterministicChoiceSet
consts NonDeterministicChoiceSet :: "Cmd set ? Cmd"
and explain it (informally) as a function that receives a set of Cmd, and returns the correspondent NonDeterministicChoice fed with the list containing all the elements of the set given as argument, ordered by some criteria, say lexicographic order. Then, rather than use "NonDeterministicChoice" when giving a semantics, I would give a semantics for "NonDeterministicChoiceSet" and only use "NonDeterministicChoiceSet" in the theory.
Questions
Thanks! :-)
首先，允许从任意命令集中进行非确定性选择的命令数据类型的概念存在很大问题。我会解释原因。
\n\n假设你有一个数据类型
\n\ndatatype Cmd = Skip | NonDeterministicChoice "Cmd set"\n就像你想要的那样。让A := (UNIV :: Cmd)，即所有有效命令的集合。那么，当然，函数
f: P(A) \xe2\x86\x92 A, X \xe2\x86\xa6 NonDeterministicChoice X\nA是 的幂集的单射函数A。根据康托尔对角化定理，这是不可能的。这意味着什么？这意味着对于您定义的编程语言，不可能存在所有命令\xe2\x80\x99 的\xe2\x80\x98 集。这使得你的语言很难使用。我对 Z/EVES 一无所知，但如果它允许这样的数据类型定义，我对其一致性非常怀疑。
这就是为什么你想做的事情有问题的理论原因。正如错误消息所示，数据类型定义失败的确切技术原因是，它set不是有界自然函子 (BNF)。我不是 BNF 专家，但据我所知，这里的问题是，如上所述，允许嵌套数据类型递归set可能会使数据类型 \xe2\x80\x98 太大\xe2\x80\x99。
您已经注意到，列表可以工作，但并不理想。您可以fset使用有限集 ( ) 或可数集 ( )来代替列表cset。这些是有界自然函子。我自己没有使用过它们中的任何一个，但快速浏览一下表明这fset可能更好用，因此如果您只想从一组有限的命令中进行非确定性选择，fset那么这是可行的方法。如果您需要countable多种替代方案，请使用cset. 它们都可以在 中找到~~/src/HOL/Library/，理论分别称为FSet和Countable_Set_Type。
fset有很多语法使其看起来很像普通集合（{||}而不是{},|\xe2\x88\x88|而不是\xe2\x88\x88）；cset支持几乎相同的操作，但没有漂亮的语法。当然，如果集合是有限/可数的，您可以将fset/转换cset为setand ，反之亦然。这意味着您可以使用涵盖所有有效命令的集合推导式，过滤掉您不需要的命令，但结果集必须是有限/可数的。
请注意，开头提到的问题仍然存在。\n当您使用 时，您可以从有限的命令集中进行非确定性选择，但所有命令fset的集合将不是有限的。如果使用，则可以从任何有限或可数无限命令集中进行选择，但所有命令的集合将不可数。这是一个根深蒂固的逻辑问题，我认为你无法回避。（尽管逻辑学家在处理这些事情时可能具有令人惊讶的创造力）cset
我不明白你NonDeterministicChoiceSet做了什么或应该做什么。\xe2\x80\x98all 感兴趣的程序/值\xe2\x80\x99 的构造让我觉得有些奇怪和人为。我所看到的非确定性正式建模的方式始终是，您要么在两个程序（而不是整个集合）之间非确定性地选择，要么根本不在程序之间进行选择，而是从一组程序中非确定性地选择一个值。值，然后取决于该值。这两种变体显然都不会导致我上面提到的问题。
如果不知道您到底想要做什么，很难说哪种方法最适合您的问题，但我之前用fset/概述的方法cset可能是最接近您最初意图的方法。
由于在下面的评论中被问到，我现在将尝试展示 \xe2\x80\x98big\xe2\x80\x99 命令集如何根据非确定性中的集合大小施加的界限来表示选择运算符。免责声明：我对红衣主教知之甚少，所以我不能绝对确定我在这里的所有推理都是完全正确的。
\n\n设 A 为所有命令的集合，并让 [A]^\xce\xba 表示 A 的所有子集的集合，基数最多为 \xce\xba （例如，在您的情况下， \xce\xba = \xe2\x84\ xb5\xe2\x82\x80，其中 \xe2\x84\xb5\xe2\x82\x80 是自然数的基数）。通过你的非确定性选择运算符，你有一个注入 [A]^\xce\xba \xe2\x86\x92 A，即 |A| \xe2\x89\xa5 |[A]^\xce\xba|。
\n\n如果 \xce\xba \xe2\x89\xa5 |A|，则 [A]^\xce\xba 只是 2^A（A 的幂集），因此 |A| \xe2\x89\xa5 |2^A|，这与康托尔定理相矛盾。因此我们知道 \xce\xba < |A|。（实际上，这就是我之前所说的：您必须将非确定性选择限制为某些有界基数 \xce\xba 的命令集，该基数小于所有命令的基数）
\n\n现在，自从 |A| \xe2\x89\xa5 \xce\xba，我们可以用 |K| 选择一个集合 K = \xce\xba 并将 K 的任何子集单射映射到 [A]^\xce\xba 中的集合，即我们有一个注入 2^K \xe2\x86\x92 [A]^\xce\xba ，因此 |一个| \xe2\x89\xa5 |[A]^\xce\xba| \xe2\x89\xa5 |2^K| = 2^\xce\xba。
\n\n总之，如果允许对基数最多为 \xce\xba 的一组命令进行非确定性选择，则该命令集的基数至少为 2^\xce\xba，严格大于 \xce\xba康托尔定理。特别是，如果您让 \xce\xba = \xe2\x84\xb5\xe2\x82\x80，这意味着如果您允许从任何可数命令集中进行选择，则您的命令集将是不可数的。
\n