1回答
Coq可以做什么，而Agda/Idris不能做？
coq、agda、idris
Coq是一个证明助手，而Agda/Idris是编程语言(尽管它们可以被称为证明助手)。
我正在探索这些语言，我想知道Agda/Idris是否足以做Coq所能做的一切。那么，有没有一些证据/管理代码/IDE (Emacs)函数的方法/其他Coq可以做而Agda/Idris不能做</
浏览 21提问于2017-12-16得票数 9
回答已采纳
2回答
Agda和Idris的区别
agda、type-theory、idris
我开始深入研究依赖类型编程，并发现Agda和Idris语言最接近Haskell，所以我从那里开始。Idris有类似于Haskell的类型类，而Agda使用实例argumentsIdris包括一元和应用符号，它们似乎都有某种可重新绑定的语法，尽管不能真正确定它们是否相同。
浏览 75提问于2012-02-28得票数 181
回答已采纳
2回答
从哪里开始依赖类型编程？
scala、haskell、agda、dependent-type、idris
有一个Idris教程，一个Agda教程和许多其他教程风格的论文和介绍性材料，没有结束的参考资料，但仍有待学习。我在这些过程中爬来爬去，大多数时候，我被数学符号和新术语困住了，没有任何解释。就像当您想学习Haskell时，您先从"Teach yourself“开始，当您想学习Scala时，您可以从Odersky的书开始，对于Ruby来说，您读过带有变异bug的奇怪教程。但我不能从他们的书开始Agda或Idris。它们远远高于我的脑袋。我试过Coq，被困在它的全面气象证明风格。<e
浏览 7提问于2012-11-21得票数 44
1回答
Idris中第一类类型的概念
language-design、idris、dependent-type、first-class
当我用Edwin的type Development Idris学习Idris时，我读到了Idris的独特特性，与其他编程语言相比，Idris类型是一个一流的构造，尤其是那些具有依赖类型系统的人。为什么其他系统/语言中的类型不是第一类(例如Agda或Coq )？我假设这个特性对程序在编译时可以检查什么引入了一些理论上的限制，但是我不知道它是什么。或者更具体地说：我希望看到一些积极的例子(好处)和一些负
浏览 9提问于2022-04-30得票数 1
回答已采纳
1回答
如果使用“安全语言”验证了SSL/TLS实现，那么它是否仍然容易受到心脏出血的攻击？
haskell、ssl、coq、agda、idris
您的实现可能容易受到侧通道攻击(特别是定时攻击)的攻击，而逻辑上仍然正确。我的问题是：在一种“安全语言”(即Haskell，Idris)中有一个经过验证的SSL/TLS实现，或者用定理验证器(Coq，Agda)检查它是否仍然容易受到心脏出血攻击？
浏览 1提问于2014-04-15得票数 3
回答已采纳
1回答
为什么我们不能在Coq/Agda/Idris中的Set/Type上进行模式匹配？
coq、idris、agda
ByteLength a where byteLength = 1
以更一般的方式，也许我们可以在我认为使用Interface和使用forall是非常不同的，因为Interface意味着“某些类型”，而forall意味着“用于所有类型”。
浏览 0提问于2018-09-08得票数 6
1回答
把Coq定义翻译给agda？
compilation、coq、translate、agda
我想知道是否有一种系统的方法来解释Coq定义为agda程序。我正在翻译部分编程基础，无法让tUpdate函数在下面工作。为什么这个失败。对coq代码进行注释。编辑：
我意识到更新应该返回一张地图，但我很困惑，因为它似乎可以推断出这一点，而agda不能？对于后一个问题，我仍然欢迎一个更笼统的答案。
浏览 2提问于2020-04-10得票数 1
回答已采纳
1回答
什么是累积宇宙和‘*：*’？
functional-programming、type-systems、agda、dependent-type、idris
在Agda中，有Set n。据我所知，Set n将Haskell样式的值类型类型层次结构扩展到无限级别。相反，Idris有所谓的“宇宙的累积层次”。看来，对于a < b、Type a: Type b和宇宙水平是推断出来的。但在现实世界中，这意味着什么呢？我们不能定义一些只在更高而不是更低的宇宙上运作的东西吗？
顺便说一句，我知道这在逻辑上是不一致的，但是与上述一致的解决方案相比，* : *是什么呢？
浏览 1提问于2015-11-13得票数 10
回答已采纳
1回答
可证明正确性和运行时复杂性的编程语言/工具
programming、real-time
我正在寻找一种编程语言/工具，它可以完成以下两件事：证明一个程序将在小于N秒和/或执行少于N个简单的操作，对一个有界的输入大小。
浏览 0提问于2018-05-06得票数 1
3回答
用补码操作形式化正则表达式
regex、coq、agda、idris
我正在处理Idris中一个经过认证的正则表达式匹配器的形式化(我相信在任何基于理论的证明助手(如Agda和Coq)中都存在同样的问题)，而且我一直在讨论如何定义补码操作的语义。我想以Idris终止检查器接受的方式来定义这种语义。
我是否可以用某种方式来表示补语操作的语义而不出现InRegExp的负数。
浏览 3提问于2016-02-05得票数 4
回答已采纳
1回答
Coq与Agda的差异
coq、agda
这些程序中的每一个都是为什么而设计的，它们各自提供给对方什么？另外，这两个系统是否都是一致的，而且它们是否基于一些基本的数学理论？
浏览 7提问于2014-06-25得票数 31
3回答
我试图使用Coq对正则表达式(REs)上的一些属性进行形式化化。stuck heres' : string============================至少在我看来，使用归纳似乎可以完成证明，因为我可以在归纳假设中使用H4来完成证明，但是当我开始使用而不是我有一些(至少对我来说)毫无意义的目标。在Idris</e
浏览 3提问于2016-11-25得票数 4
回答已采纳
1回答
Idris是否与Agda的↔相当
list、equality、agda、idris
Agda使用以下操作符显示集合之间的逆：在Idris中也有类似的吗？List a -> List a -> Type这样，当l1 ~~ l2和l1和l2按任何顺序都有相同的元素时，我们就可以构造似乎非常复杂，我不确定Idris标准库中是否有类似的东西。
浏览 2提问于2014-12-03得票数 6
回答已采纳
如果需要的话，必须在Coq中以公理方式添加UIP (以及类似于公理K的等价物)：这是令人惊讶的，因为从等式的定义来看，这是显而易见的(当然，这取决于对Coq中归纳定义包含其类型的所有元素的解释)。
浏览 5提问于2021-12-22得票数 3
回答已采纳
3回答
依赖类型(例如Coq或Agda)启用的编程风格的名称是什么？
coq、specifications、dependent-type、formal-methods、curry-howard
在Coq中，您有一种元编程语言(Ltac)，它允许您在幕后构建实际程序的同时“细化”规范，而在Agda中，通过填充“漏洞”(我不确定它在Agda中是如何进行的，因为我主要习惯于Coq)来编写程序。至少在Coq中，我发现它相当容易上瘾！
...but，我怎么才能在证据助手之外寻找方法呢？这就引出了一个问题:我正在为这种编程风格寻找一个名字，这样我就可以尝试查找一些工具，让我可以用其他编程语言那样编程。而且要明确的是，我并不完全希望我能找到很多东西；这些都是学术上的消遣，<
浏览 8提问于2020-12-24得票数 1
据我所知，Coq策略是在幕后编译成一些函数式程序的，但我真的不确定这是怎么回事。我非常确定这不是我想要做的。 我想要做的是类似下面的Idris程序。在Coq中，两个证明卡在一个lambda中，我不确定这是怎么发生的。我看到Coq的induction策略并没有做我认为它应该做的事情。除了上面的解释之外，让我问一下，有没有比软件基础更多的Coq入门材料，以防我在某些策略上再次陷入这样的困境？请注意，我知道如何在Coq中解决这个问题，因为我已经在网上找到了解决方案。早在2016年，我就尝试过将
浏览 15提问于2019-04-09得票数 1
回答已采纳
4回答
在依赖类型的函数式编程语言中，扁平列表更容易吗？
haskell、functional-programming、coq、agda、idris
但是，这些家族和类似乎也是由于haskell中缺少/替代依赖类型而引入的(例如，状态“类型族.非常类似于依赖类型”)。(例如Idris、Agda、Coq、.)我对这些语言没有经验，这就是我为什么要问的原因。例如，在Idris网站上，有人说“类型可以作为参数传递给函数”，因此，我认为，在列表扁平化的情况下，可以简单地将列表类型作为参数传递，并以简单的方式实现所需的函数。这个是可能的吗？
浏览 8提问于2021-08-22得票数 2
回答已采纳
1回答
无法匹配haskell中的多态类型
haskell、polymorphism
= case x of (K') -> K''
k3 x = k2 ( k1 x)
k4 = k2 . k1
除了不写点自由的风格
浏览 1提问于2017-08-30得票数 2
回答已采纳
2回答
所以，举例来说，自动满足那么，我是否可以获得以下类型的Agda术语： → f (map g xs) ≡ map g (f xs)
或者如果是这样/如果不是，我可以做一些更通用我知道的存在，但我不认为它能做我想做的事情(或者即使它做了，我对它的理解也不够好，无法做到这一点)。
浏览 0提问于2014-07-13得票数 13
1回答
证明了如果n=m和m= o，那么n+m=m+o在Idris？
proof、idris
我正在努力提高我的Idris技能，通过查看一些练习 (最初是为Coq，但我希望翻译到Idris不太坏)。我在上遇到了麻烦，它写着：
plusIdExercise : (n : Nat) -> (o : Nat我能做些什么来解决这个问题吗？我来的对吗？我有点困惑。
浏览 3提问于2018-05-26得票数 2
回答已采纳
云服务器
对象存储
ICP备案
云点播
语音识别
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号