简单地说，声明类型是一个定理，返回该类型的程序是相应定理的证明。因此，库里-霍华德将程序与数学证明联系在一起，没有错误。因此，Curry-Howard如何在数学世界中翻译程序错误的概
浏览 28提问于2017-02-25得票数 1
回答已采纳
3回答
如果我正确理解Curry-Howard同构，每个依赖类型都对应一个定理，实现它的程序就是一个证明。这意味着任何数学问题，比如a^n + b^n = c^n，都可以以某种方式表示为一个类型。现在，假设我想设计一个生成随机类型(定理)的游戏，玩家必须尝试实现这些类型(定理)的程序(证明)。有可能控制这些定理的难度吗？也就是说，简单模式会产生琐碎的定理，而困难模式会产生更难的定理。
浏览 5提问于2016-04-21得票数 6
1回答
为了解决这个问题，我修改了/war/projectName/sc/modules/ISC_Core.js的一部分。下面是我修改的代码：第二行是我添加的，使代码在Chrome中的特定环境下工作。
浏览 3提问于2013-08-09得票数 0
2回答
(f (Stream f m r)) | Return r Stream数据类型等同于，可以表示任何有效的连续步骤，其中步骤或“命令”的形式由第一个(函数器)参数指定。我想知道Stream类型如何等同于FreeTdata FreeF f a b = Pure a | Free (f b)
newtype FreeT f m a = FreeT{ runFreeT
浏览 41提问于2018-05-29得票数 7
回答已采纳
1回答
我已经设法获得了对基本原则的理解，但当我试图定义这一点时，我一无所获，因为它一直在告诉我：
"Error: The我已经尝试了我之前在脚本中使用的常用策略，我确信必须使用相同的方法(有趣)来解决这个问题，但是我似乎尝试的一切都以该错误消息结束。有什么建议吗？
浏览 4提问于2014-11-15得票数 0
根据
若要指定同构类型的可变长度元组，请使用文字省略号，例如Tupleint、.普通元组等价于TupleAny，.，然后依次等同于元组。因此，注释Tuple[int]指定一个包含单个整数的元组；然而，List[int]意味着可变长度。为什么...必须与Tuple[int, ...]一起使用，而不是与List[int]一起使用，如果两者都可以是同源的/异己的？
浏览 3提问于2020-06-02得票数 3
回答已采纳
2回答
我正在浏览球拍指南，刚刚完成了这一页：
(provide [argmax (dominates-all f@r flov))]))))]))
我敢打赌，这个契约已经达到了比所需的实际实现更高的复杂性更让我困惑的是，契约甚至不是一个编译时组件，就像Curry-How
浏览 0提问于2017-06-27得票数 0
我的问题很简单。我用networkx从蛋白质结构构建图表。我使用subgraph_is_isomorphic()函数，但是我只需要允许一些氨基酸被认为是相等的。例如，低浓缩铀应被视为等于ILE，但不等同于跨国激进党。我如何定义一个自定义的node_match函数来完成这个任务？在下面的代码中，我需要一个node_match函数，如果使用它，G1和G2就会变成同构的，而不是同构的。
浏览 8提问于2022-07-09得票数 2
回答已采纳
2回答
我有一个函数，它接受不同长度的元组作为参数：
# Do nasty tuplestuff
process_tuple(("a", "b"))当我像上面提到的那样注释函数时has incompatible
浏览 1提问于2019-02-18得票数 64
回答已采纳
2回答
这是一个基本的问题。Coq有一种Gallina形式的规范语言。据我所知，Coq本身是用OCaml编写的。
我的问题是，Gallina什么时候开始发挥作用？它是用来做什么的，为什么？我想我误解了规范语言和编程语言的使用。
浏览 39提问于2019-08-14得票数 1
这不同于list类型的提示： # do something
func([1,2]) # would also be fine在某种程度上，这是必然的，因为元组的类型。所以我的问题是，有没有办法让元组类型提示中的项数变得灵活呢？我试过这样的方法，但不起作用：
def func(var:
浏览 0提问于2017-11-28得票数 63
回答已采纳
b -> b ) -> (a -> b )
问题：为什么(b -> b) -> (a -> b)等同于(a -> b)
浏览 2提问于2017-05-19得票数 2
回答已采纳
我是一个全新的Coq新手，正在学习Mike Nahas的教程：。那么对于(forall x, ~(P x))，我的猜测是x被Coq推断为Set类型，并且它被解读为“每一个集合都会产生一个不可证明的/错误的命题”。这些似乎在逻辑上是等价的。我只是在语言上苦苦挣扎。可以将P解释为从集合空间映射到命题空间的函数吗？我用了“产生”和“暗示存在”这两个短语，对吗？有没有更正确的方式来说明这一点？
感谢您的帮助！编辑:对于任何有类似问题
浏览 14提问于2019-11-21得票数 2
回答已采纳
它们之间的区别是什么和我分析了这两个语句，发现前一个语句中多个模式的边缘不允许重复。我曾经认为路径模式只约束了一条路径，多个路径模式之间应该没有这样的限制，但这与我目前的测试结果不一致。
这怎么说得通呢？
浏览 3提问于2021-11-18得票数 0
= { r: string };type B = { b: string };因为Main等同于{r: string, a: string} | {r: string, b: string}，所以这是可行的： r: 'r',这没什么好惊讶的。exist on type 'Root &a
浏览 36提问于2018-12-12得票数 3
回答已采纳
1回答
所以我想，通过定义数据类型AllDifferent、函数allDiff以及派生的someEq和someDiff，我就可以获得Foldable结构的。如果我的工作结果是正确的，那么如何恰当地描述这组数据类型和函数呢？
浏览 0提问于2019-04-24得票数 2
回答已采纳
1回答
在的第12页，它写道：“容器的一个突出的例子是列表数据类型。列表可以用列表的长度和列表中的函数映射位置来表示”。那么，上述容器上的免费单片是什么？同构的是什么</em
浏览 5提问于2022-02-22得票数 9
回答已采纳
4回答
在使用C++编程时，我经常混淆"+=“和"=+"，前者实际上是我指的运算符。Visual似乎两者都接受，但它们的行为不同，是我的许多bug的来源。我知道+= b在语义上等同于a= a+b，但是"=+“做什么呢？
浏览 3提问于2013-10-17得票数 15
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
云直播活动推荐
腾讯云开发者
