问题标签 [coinduction]

在使用 Isabelle 的无限流数据类型时，我需要这个显然是真的引理，但我无法弄清楚如何证明它（因为我还不精通共归纳法）。我将如何去证明它？

这是“使用延迟模态从定点算子计算（无限）树”的变体。

那个设定。我们研究一种二叉树语言，增强了通过从根开始的路径引用树中任意其他节点的能力：

路径是在某个根的上下文中定义的，当我们在路径中看到 False/True 时，它​​会识别通过连续跟随左/右子节点找到的子树。例如，路径在树中[False, True]标识。SLeaf 2SNode (SNode (SLeaf 1) (SLeaf 2)) (SLeaf 3)

例如，此类树可用于识别任意流图（包括不可约图，这是使用固定点运算符无法实现的。）

我们可以考虑由这种描述诱导的无限树。

这是一个从一个到另一个的转换函数，利用一个辅助函数follow在树的某个路径上找到子树：

不幸的是，这个函数没有生产力：它在flatten (SPath []).

问题。我们现在考虑这种结构的变体，它增加了延迟模态（如“使用延迟模态从定点算子计算（无限）树”中所述），以及Loop指示自引用循环的构造函数。

不使用非结构递归函数调用（因此，您可以在STreeand上进行结构递归Path），编写一个STree -> Tree展开无限树的函数（或类似函数）。

后记。在许多情况下，我们不想计算无限展开：如果存在，我们想要有限展开，否则会出错。具体来说，给定原始数据类型：

在不使用非结构递归的情况下，我们可能想要编写一个函数STree -> Maybe Tree（或类似函数），如果它存在则将语法展开为有限树，否则失败。这种结构中没有延迟模态保证了它是有限的。

由于此结构中没有延迟模态的实例，因此似乎无法使用fixD: 我们将得到一个我们永远无法使用的延迟结果。看来我们必须将树转换为图，对其进行拓扑排序，然后直接实现高斯消元算法，而不使用fixD.

是否有替代的打字规则允许我们像在原始（错误）代码中一样优雅地实现展开？如果是这样，您可能刚刚（重新）发现了另一种在图中查找循环的算法。

所以我最近一直在阅读关于共归纳法的文章，现在我想知道：Haskell 列表是归纳法还是归纳法？我也听说 Haskell 不区分这两者，但如果是这样，他们是如何正式区分的？

列表是归纳定义的，data [a] = [] | a : [a]，但可以互归纳地使用，ones = a:ones。我们可以创建无限列表。然而，我们可以创建有限列表。那么它们是什么？

相关是在 Idris 中，其中类型List a是严格的归纳类型，因此只是有限列表。它的定义类似于它在 Haskell 中的定义。但是，Stream a是一种互感类型，建模一个无限列表。它被定义为（或者更确切地说，定义等同于）codata Stream a = a :: (Stream a)。创建无限列表或有限流是不可能的。但是，当我写定义

我从 Haskell 列表中得到了我期望的行为，即我可以制作有限和无限的结构。

所以让我把它们归结为几个核心问题：

1. Haskell 不区分归纳类型和共归纳类型吗？如果是这样，那它的形式化是什么？如果不是，那么哪个是[a]？

2. HList 是互感的吗？如果是这样，协约类型如何包含有限值？

3. 如果我们定义了data HList' a = L (List a) | R (Stream a)呢？会考虑什么和/或它会比 just 有用HList吗？

我正在试验 Coq Coinductive 类型。我使用 Coq'Art 书中的惰性列表类型（第 13.1.4 节）：

为了匹配保护条件，我还使用本书中的以下分解函数：

左中性引理LNil很容易证明：

但是我证明这LNil也是正确中性的：

在亚瑟的回答之后，我尝试了新的平等：

我在这里卡住了。Coq 的回答是：

在 Eponier 的回答之后，我想通过引入可扩展性公理来对其进行最后的润色：

有了这个公理，我得到了引理的最终切割：

现在，这是我对该线程的最后一个问题：

• 某些 Coq 库中是否已经存在这样的公理？
• 这个公理与 Coq 一致吗？
• 该公理与 Coq 的哪些标准公理（例如，classic、UIP、fun ext、Streicher K）不一致？

或者只是有时很难证明一个类型是一个共归纳类型？

我说的是一种完全的编程语言，这意味着它不是图灵完备的，递归都是有根据的，核心递归都是有效的。图灵完备是否真的带来了比这种语言更多的东西？

1）我相信可以在没有模式匹配的情况下使用归纳类型。（仅使用 _rec、_rect、_ind）。它是不透明的，复杂的，但可能的。2）是否可以在没有模式匹配的情况下使用共归纳类型？

存在从协归纳类型到协归纳类型构造函数域的并集的函数。Coq 是否显式生成它？如果是，如何重写 'hd' ？

我正在尝试为 IMP 语言编写具有并行抢占式调度的功能语义，如以下论文的第 4 节所述。

我正在使用 Agda 2.5.2 和标准库 0.13。此外，整个代码可在以下gist中找到。

首先，我将相关语言的语法定义为归纳类型。

状态只是自然数的向量，表达语义很简单。

然后，我定义了恢复的类型，这是某种延迟计算。

接下来，在1之后，我定义了语句的顺序和并行执行

到现在为止还挺好。接下来，我需要定义语句评估函数与在恢复中关闭（执行暂停计算）的操作。

当我试图填补构造函数eval方程中的漏洞时，Agda 的整体检查器抱怨说终止检查在函数和函数的几个点上都失败了。atomicδ (♯ close (eval s st))evalclose

我对这个问题的问题是：

1) 为什么 Agda 终止检查抱怨这些定义？在我看来，调用δ (♯ close (eval s st))很好，因为它是在结构上更小的语句上完成的。

2）当前 Agda 的语言文档说这种基于乐谱的联合归纳法是 Agda 中的“旧方式”联合归纳法。它建议使用共归纳记录和 copatterns。我环顾四周，但找不到流和延迟单子之外的共同模式示例。我的问题：是否可以使用共归纳记录和共同模式来表示恢复？

当我写

我明白了

"inftree" 既不与 "inftree" 相互核递归，也不是通过自身嵌套核递归

为什么，我该如何避免呢？