在 Haskell 中，列表是归纳的还是余归纳的？
最近我在阅读有关共归的内容，现在我想知道：Haskell中的列表是归纳的还是共归的？我也听说过Haskell不区分这两者，但如果是这样，他们如何在形式上区分呢？ 列表是归纳定义的，data [a] = [] | a : [a]，但可以用于共归，ones = a:ones。我们可以创建无限的列...
递归和归纳证明之间有什么关系？
递归和归纳证明之间的关系是什么？ 假设 fn(n), 递归是 fn(n) 不断调用自身，直到满足 base condition； 归纳是当满足 base condition 时，尝试证明 (base case + 1) 也是正确的。 看起来递归和归纳是不同的方向。一个从 n 到 bas...
展示两个不同的斐波那契函数是等价的。
我正在尝试学习证明程序正确的确切含义。我从零开始，但在第一步/主题介绍上遇到了困难。 在这篇关于完全函数式编程的论文中，给出了斐波那契函数的两个定义。传统的定义如下：fib 0 = 0 fib 1 = 1 fib n = fib (n-1) + fib (n-2) --fib (n+2) =...
如何高效地将归纳类型转换为非递归的余归纳类型？（无需使用递归）
> {-# LANGUAGE DeriveFunctor, Rank2Types, ExistentialQuantification #-} 任何归纳类型的定义如下所示 > newtype Ind f = Ind {flipinduct :: forall r. (f r ...
Agda 中的 Sized 类型是什么？
我可以为您翻译。以下是需要翻译的内容： Agda 中的大小类型是什么？我试图阅读有关MiniAgda的论文，但由于以下原因未能继续： 为什么数据类型通常会涵盖它们的大小？据我所知，大小是归纳树的深度。 为什么数据类型在其大小上是协变的，即 i <= j -> T_i <...
我能否告诉Coq从n归纳到n+2？
我试图从https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html中证明evenb n = true <-> exists k, n = double k，而不涉及奇数。我尝试了以下内容： Theorem eve...
了解Python中的递归
我真的在努力理解递归是如何工作并且理解递归算法。例如，当我输入5时，下面的代码返回120，抱歉我的无知，但我就是看不懂为什么？ def fact(n): if n == 0: return 1 else: return n * fact(n-1...
如何在Coq中使用自定义归纳原理？
我读到类型归纳原理只是一个关于命题P的定理。因此，我基于右（或反向）列表构造器构建了一个List的归纳原理。 Definition rcons {X:Type} (l:list X) (x:X) : list X := l ++ x::nil. 归纳原理本身是： Definiti...
棋盘覆盖递归算法的直觉是什么，如何更好地制定这样的算法？
你可能听说过经典的棋盘覆盖难题。如何使用L形砖块覆盖一个缺少一个角落正方形的棋盘？ 在书籍《Python算法：掌握Python语言的基本算法》中，有一种递归方法来解决这个问题。 其思想是将棋盘分成4个较小的正方形，然后将L形砖块放置在大棋盘的中心，有效地创建了4个缺少1个砖块的小正方形并继...