Isabelle：不支持通过类型构造函数递归出现数据类型 "Set.set"
Isabelle: Unsupported recursive occurrence of a datatype via type constructor "Set.set"
问题
我想知道在伊莎贝尔语法中是否有一种自然的编码方式
像这样：
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" 类型在 "Cmd set" 中递归出现，即：
Unsupported recursive occurrence of type "Cmd" via type
constructor "Set.set" in type expression "Cmd set". Use the "bnf"
command to register "Set.set" as a bounded natural functor to allow
nested (co)recursion through it
当我使用 set 时查看 Isabelle 错误消息，我无法弄清楚如何在这种情况下为类型 'set' 注册有界自然函子，所以我决定尝试一个推测性的解决方案。
推测解
相反，如果我使用归纳定义的数据类型，例如列表，Isabelle 不会
抱怨例如
datatype Cmd = Skip | NonDeterministicChoice "Cmd list" | ...
列表在这里不是正确的抽象，但我试试看它是否会
工作与否。使用列表的直接效果是，我需要使用序列过滤而不是使用集合理解，然后问题变成假设存在两个列表：一个包含 Cmd 的所有元素, 和其他包含 Value 的所有元素。
我声明了两个未解释的常量：
consts Values :: "Value list"
consts Programs :: "Cmd list"
因为列表是有限的，所以将常量解释为 "all elements (of interest) of Cmd" 和 "all values (of interest)" 更有意义。也就是说，所有感兴趣的元素都是那些可以在计算机内存中表示的元素。
根据相同的论点，我可以声明一个常量 NonDeterministicChoiceSet
consts NonDeterministicChoiceSet :: "Cmd set ⇒ Cmd"
并将其（非正式地）解释为接收一组 Cmd 的函数，并且 returns 对应的 NonDeterministicChoice 提供包含作为参数给定的集合的所有元素的列表，按某些标准排序，说字典顺序。然后，我不会在给出语义时使用 "NonDeterministicChoice"，而是给出 "NonDeterministicChoiceSet" 的语义并且在理论上只使用 "NonDeterministicChoiceSet"。
问题
- 这个建模有意义吗？
- 有没有更好的方法来表示这个语法？
- 如果我想表示这个文法，Isabelle 是合适的定理证明者吗？例如，我尝试在 Z/Eves 中定义这个语法，并且没有引起任何抱怨。
谢谢！ :-)
理论解释
首先，允许从任意一组命令中进行非确定性选择的命令数据类型的概念存在严重问题。我会解释为什么。
假设您有一个数据类型
datatype Cmd = Skip | NonDeterministicChoice "Cmd set"
如你所愿。让A := (UNIV :: Cmd)，即所有有效命令的集合。那么，当然，函数
f: P(A) → A, X ↦ NonDeterministicChoice X
是从A的幂集到A的单射函数。根据 Cantor 的对角化定理，这是不可能的。那是什么意思？这意味着对于您定义的编程语言，不可能存在诸如“所有命令集”之类的东西。这使您的语言很难使用。我对Z/EVES一无所知，但如果它允许这样的数据类型定义，我很怀疑它的一致性。
技术说明
这就是为什么你想做的事情有问题的理论上的原因。正如错误消息所暗示的那样，您的数据类型定义失败的确切技术原因是 set 不是有界自然函子 (BNF)。我几乎不是 BNF 的专家，但据我所知，这里的问题是，如上所述，允许使用 set 的嵌套数据类型递归会使数据类型“太大”。
如何绕过它
您已经注意到列表有效但并不理想。您 可以 使用有限集 (fset) 或可数集 (cset) 而不是列表。这些 是 有界自然函子。我自己没有与他们中的任何一个合作过，但快速浏览表明 fset 可能更好用，所以如果你只想 select 非确定性地从 finite 组命令，fset 是要走的路。如果您需要 countable 个备选方案，请使用 cset。它们都可以在~~/src/HOL/Library/中找到，分别称为FSet和Countable_Set_Type。
fset 有很多语法，使它看起来很像普通集（{||} 而不是 {}，|∈| 而不是 ∈ ); cset 支持几乎相同的操作，但没有很好的语法。当然，您可以将 fset/cset 转换为 set，如果集合是 finite/countable，反之亦然。这意味着您 可以 使用涵盖所有有效命令的集合推导，过滤掉您不想要的那些，但是结果集合 必须 finite/countable.
注意，开头提到的问题依然存在
当您使用 fset 时，您可以从一组有限的命令中进行非确定性选择，但是 all 命令集将 not是有限的。如果您使用 cset，您可以从任何有限或可数无限的命令集中进行选择，但是 所有 命令集将 而不是 可数。这是一个根深蒂固的逻辑问题，我认为您无法回避。 （虽然逻辑学家在这些事情上可以出奇地有创造力）
其他建模方法
我不明白你的 NonDeterministicChoiceSet 做什么或应该做什么。 “all programs/values of interest”的结构让我觉得有些奇怪和做作。我看到非确定性正式建模的方式总是你要么在 两个 程序之间非确定性地选择，而不是整个集合，或者你根本不在程序之间选择，但是从一组值中非确定性地选择一个 值 ，然后依赖于该值。这两种变体显然不会导致我上面提到的问题。
在不了解你到底想做什么的情况下，很难说哪种方法最适合你的问题，但我之前用 fset/cset 概述的方法可能是最接近你初衷的那个。
分析命令集的基数
既然有人在下面的评论中提出了这个问题，我现在将尝试根据非确定性选择运算符中对集合大小施加的界限来展示命令集有多大。免责声明：我对红衣主教知之甚少，所以我不确定我在这里的所有推理是否完全正确。
令 A 为所有命令的集合，令 [A]^κ 表示 A 的所有子集的集合，基数最多为 κ（例如，在您的情况下，κ = ℵ₀，其中 ℵ₀ 是命令的基数自然数）。通过你的非确定性选择运算符，你有一个注入 [A]^κ → A，即 |A| ≥ |[A]^κ|。
如果 κ ≥ |A|，那么 [A]^κ 就是 2^A（A 的幂集），因此 |A| ≥ |2^A|，这与康托定理相矛盾。因此我们知道 κ < |A|。 （实际上，这就是我之前所说的：你必须将你的非确定性选择限制在一些有界基数 κ 小于所有命令基数的命令集）
现在，因为|A| ≥ κ，我们可以用 |K| 选择一个集合 K = κ 并将 K 的任何子集单射映射到 [A]^κ 的集合，即我们有一个注入 2^K → [A]^κ 因此 |A| ≥ |[A]^κ| ≥ |2^K| = 2^κ.
总而言之，如果您允许对基数最多为 κ 的一组命令进行非确定性选择，则该组命令的基数至少为 2^κ，根据康托尔定理，该基数严格大于 κ。特别是，如果你让 κ = ℵ₀，这意味着如果你允许从任何可数的命令集中进行选择，你的命令集将是不可数的。
问题
我想知道在伊莎贝尔语法中是否有一种自然的编码方式 像这样：
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" 类型在 "Cmd set" 中递归出现，即：
Unsupported recursive occurrence of type "Cmd" via type constructor "Set.set" in type expression "Cmd set". Use the "bnf" command to register "Set.set" as a bounded natural functor to allow nested (co)recursion through it
当我使用 set 时查看 Isabelle 错误消息，我无法弄清楚如何在这种情况下为类型 'set' 注册有界自然函子，所以我决定尝试一个推测性的解决方案。
推测解
相反，如果我使用归纳定义的数据类型，例如列表，Isabelle 不会 抱怨例如
datatype Cmd = Skip | NonDeterministicChoice "Cmd list" | ...
列表在这里不是正确的抽象，但我试试看它是否会 工作与否。使用列表的直接效果是，我需要使用序列过滤而不是使用集合理解，然后问题变成假设存在两个列表：一个包含 Cmd 的所有元素, 和其他包含 Value 的所有元素。
我声明了两个未解释的常量：
consts Values :: "Value list"
consts Programs :: "Cmd list"
因为列表是有限的，所以将常量解释为 "all elements (of interest) of Cmd" 和 "all values (of interest)" 更有意义。也就是说，所有感兴趣的元素都是那些可以在计算机内存中表示的元素。
根据相同的论点，我可以声明一个常量 NonDeterministicChoiceSet
consts NonDeterministicChoiceSet :: "Cmd set ⇒ Cmd"
并将其（非正式地）解释为接收一组 Cmd 的函数，并且 returns 对应的 NonDeterministicChoice 提供包含作为参数给定的集合的所有元素的列表，按某些标准排序，说字典顺序。然后，我不会在给出语义时使用 "NonDeterministicChoice"，而是给出 "NonDeterministicChoiceSet" 的语义并且在理论上只使用 "NonDeterministicChoiceSet"。
问题
- 这个建模有意义吗？
- 有没有更好的方法来表示这个语法？
- 如果我想表示这个文法，Isabelle 是合适的定理证明者吗？例如，我尝试在 Z/Eves 中定义这个语法，并且没有引起任何抱怨。
谢谢！ :-)
理论解释
首先，允许从任意一组命令中进行非确定性选择的命令数据类型的概念存在严重问题。我会解释为什么。
假设您有一个数据类型
datatype Cmd = Skip | NonDeterministicChoice "Cmd set"
如你所愿。让A := (UNIV :: Cmd)，即所有有效命令的集合。那么，当然，函数
f: P(A) → A, X ↦ NonDeterministicChoice X
是从A的幂集到A的单射函数。根据 Cantor 的对角化定理，这是不可能的。那是什么意思？这意味着对于您定义的编程语言，不可能存在诸如“所有命令集”之类的东西。这使您的语言很难使用。我对Z/EVES一无所知，但如果它允许这样的数据类型定义，我很怀疑它的一致性。
技术说明
这就是为什么你想做的事情有问题的理论上的原因。正如错误消息所暗示的那样，您的数据类型定义失败的确切技术原因是 set 不是有界自然函子 (BNF)。我几乎不是 BNF 的专家，但据我所知，这里的问题是，如上所述，允许使用 set 的嵌套数据类型递归会使数据类型“太大”。
如何绕过它
您已经注意到列表有效但并不理想。您 可以 使用有限集 (fset) 或可数集 (cset) 而不是列表。这些 是 有界自然函子。我自己没有与他们中的任何一个合作过，但快速浏览表明 fset 可能更好用，所以如果你只想 select 非确定性地从 finite 组命令，fset 是要走的路。如果您需要 countable 个备选方案，请使用 cset。它们都可以在~~/src/HOL/Library/中找到，分别称为FSet和Countable_Set_Type。
fset 有很多语法，使它看起来很像普通集（{||} 而不是 {}，|∈| 而不是 ∈ ); cset 支持几乎相同的操作，但没有很好的语法。当然，您可以将 fset/cset 转换为 set，如果集合是 finite/countable，反之亦然。这意味着您 可以 使用涵盖所有有效命令的集合推导，过滤掉您不想要的那些，但是结果集合 必须 finite/countable.
注意，开头提到的问题依然存在
当您使用 fset 时，您可以从一组有限的命令中进行非确定性选择，但是 all 命令集将 not是有限的。如果您使用 cset，您可以从任何有限或可数无限的命令集中进行选择，但是 所有 命令集将 而不是 可数。这是一个根深蒂固的逻辑问题，我认为您无法回避。 （虽然逻辑学家在这些事情上可以出奇地有创造力）
其他建模方法
我不明白你的 NonDeterministicChoiceSet 做什么或应该做什么。 “all programs/values of interest”的结构让我觉得有些奇怪和做作。我看到非确定性正式建模的方式总是你要么在 两个 程序之间非确定性地选择，而不是整个集合，或者你根本不在程序之间选择，但是从一组值中非确定性地选择一个 值 ，然后依赖于该值。这两种变体显然不会导致我上面提到的问题。
在不了解你到底想做什么的情况下，很难说哪种方法最适合你的问题，但我之前用 fset/cset 概述的方法可能是最接近你初衷的那个。
分析命令集的基数
既然有人在下面的评论中提出了这个问题，我现在将尝试根据非确定性选择运算符中对集合大小施加的界限来展示命令集有多大。免责声明：我对红衣主教知之甚少，所以我不确定我在这里的所有推理是否完全正确。
令 A 为所有命令的集合，令 [A]^κ 表示 A 的所有子集的集合，基数最多为 κ（例如，在您的情况下，κ = ℵ₀，其中 ℵ₀ 是命令的基数自然数）。通过你的非确定性选择运算符，你有一个注入 [A]^κ → A，即 |A| ≥ |[A]^κ|。
如果 κ ≥ |A|，那么 [A]^κ 就是 2^A（A 的幂集），因此 |A| ≥ |2^A|，这与康托定理相矛盾。因此我们知道 κ < |A|。 （实际上，这就是我之前所说的：你必须将你的非确定性选择限制在一些有界基数 κ 小于所有命令基数的命令集）
现在，因为|A| ≥ κ，我们可以用 |K| 选择一个集合 K = κ 并将 K 的任何子集单射映射到 [A]^κ 的集合，即我们有一个注入 2^K → [A]^κ 因此 |A| ≥ |[A]^κ| ≥ |2^K| = 2^κ.
总而言之，如果您允许对基数最多为 κ 的一组命令进行非确定性选择，则该组命令的基数至少为 2^κ，根据康托尔定理，该基数严格大于 κ。特别是，如果你让 κ = ℵ₀，这意味着如果你允许从任何可数的命令集中进行选择，你的命令集将是不可数的。