个人中心
文章发布
退出
作者热门文章
- html - 出于某种原因，IE8 对我的 Sass 文件中继承的 html5 CSS 不友好？
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景？
25
4
这些程序中的每一个是为什么而设计的，每个程序彼此提供什么？此外，这两个系统是否一致，而且，它们是否基于一些基础数学理论？
我关心的两件事:
最佳答案
Coq 的设计考虑了定理证明，而 Agda 的设计考虑了依赖类型编程。
它们在理论方面有些等价(尽管它们有差异，Coq 在其公理上稍微保守一些，并且默认更接近 CIC 的数学基础)，但在这一点上我几乎同等地信任它们。例如，他们都被发现在对共归纳的处理上不一致，但对常规归纳部分中的错误非常有效。
根据我的经验，它们都很容易安装在 Linux 系统上。当 Cabal 工作时，Agda 可能会稍微容易一些，但当它不工作时会更糟糕。 Coq 可以捆绑在一起，也可以从源代码构建它，根据我的经验，这没问题，但有时会很痛苦，因为您必须关心 OCaml 和 camlp5 的版本。
在学习方面，我认为 Coq 可能更容易学习，因为它有一些现有的书籍，它们相当冗长且节奏缓慢(软件基础、Coq'Art 等)和一些高级书籍(CPDT)。对于 Agda 来说，根据我的经验，它有点苛刻，基本上是 Norell 的 PDF 和 wiki ......
另一方面，Agda 需要较少的学习，因为您主要需要了解依赖类型、语法和标准库。而在 Coq 中，您还必须学习策略，这是另一回事!
我的观点是:
- 如果您打算使用大证明进行重大开发，Coq 可能是您的安全选择
- 如果你只是对一些依赖类型的编程感兴趣，Agda 可能是更受欢迎的选择
无论如何，学习任何一个都会对学习另一个有很大帮助，那么为什么不尝试两者呢？ :)
关于coq - Coq 和 Agda 之间的差异，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/24416252/
25
4
0
所以我试图理解为什么这段代码在 () data sometype : List ℕ → Set where constr : (l1 l2 : List ℕ)(n : ℕ) → sometype
我最近问了这个问题: An agda proposition used in the type -- what does it mean? 并获得了关于如何使类型隐式和获得真正的编译时错误的深思熟虑的
背景:我正在研究 Prabakhar Ragde 的 "Logic and Computation Intertwined" ，对计算直觉逻辑的绝妙介绍。在他的最后一章中，他介绍了使用 Agda 的一
我正在尝试了解 Categories 库，但我对 Agda 还很陌生，所以我正在寻找某种文档来解释在该库的实现中所做的选择。在自述文件中有一个链接到这样的东西，但它坏了。 最佳答案 对于将来登陆这里的
我目前正在 Agda 中实现常规数据结构的衍生物， 如 Conor McBride [5] 的 One-Hole Context 论文中所述。 Löh & Magalhães [3,4] 也在 OHC
阅读 this answer促使我尝试构造并证明多态容器函数的规范形式。构造很简单，但证明让我很困惑。以下是我尝试编写证明的简化版本。 简化版本证明了足够多态的函数，由于参数性，不能仅根据参数的选择来
我正在尝试遵循 McBride 的 How to Keep Your Neighbours in Order 的代码，并且无法理解为什么 Agda(我使用的是 Agda 2.4.2.2)给出以下错误信
在 Agda 中玩证明验证时，我意识到我对某些类型明确使用了归纳原则，而在其他情况下则使用模式匹配。 我终于在维基百科上找到了一些关于模式匹配和归纳原则的文字:“在 Agda 中，依赖类型模式匹配是该
我看到的所有否定，即 A -> Bottom in agda 形式的结论都来自荒谬的模式匹配。还有其他情况可以在agda中获得否定吗？依赖类型理论中是否还有其他可能的情况？ 最佳答案 类型理论通常没有
我是 agda 的新手，正在阅读 http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf .我的浅薄知识以某种方式发现点阵图案不是很有必要
我有这样一个函数: open import Data.Char open import Data.Nat open import Data.Bool open import Relation.Bina
我是 Agda 的新手，我认为我在那个范式中仍然有问题需要思考。这是我的问题..我有一个类型 monoid 和一个类型 Group 实现如下: record Monoid : Set₁ where
我对类型理论和依赖类型编程还很陌生，最近正在试验 Agda 的各种功能。以下是我编写的记录类型 C 的一个非常简化的示例，它包含多个组件记录和一些我们可以用来证明事物的约束。 open import
我在 Cubical agda 工作，并试图为以后的证明建立一些通用的实用程序。其中之一是，对于任何类型 A，它与 Σ A (\_ -> Top) 类型“相同”，其中 Top是具有一个元素的类型。问题
我在学习 Agda by tutorial ，现在我正在阅读有关依赖对的信息。 所以，这是代码片段: data Σ (A : Set) (B : A → Set) : Set where _,_
我有以下几点: open import Agda.Builtin.Equality open import Agda.Builtin.Nat renaming (Nat to ℕ) open impo
我是 Agda 的新手，对此感到困惑。 open import Data.Vec open import Data.Nat open import Data.Nat.DivMod open impor
为什么函数组合 (∘) 和应用程序 ($) 有可用的实现 https://github.com/agda/agda-stdlib/blob/master/src/Function.agda#L74-L
我是第一次尝试 Agda，我已经定义了 Bool 数据类型及其基本函数，就像所有教程所说的那样: data Bool : Set where true : Bool false : Bool not
在下面的 Agda 程序中，我收到关于 one 定义中缺少大小写的警告，尽管 myList 仅适合 cons 案例。 open import Data.Nat data List (A : Set)
我是一名优秀的程序员,十分优秀！