Tag: curry howard

咖喱霍华德同构

我已经在互联网上search了一遍，我也找不到任何关于“气”的解释，这些解释并没有迅速退化成一个逻辑理论的演讲，而这个逻辑理论在我的脑海中已经大打折扣了。 （这些人认为“直觉主义演算”是一个实际上对于正常人来说意味着什么的短语！） 粗略地说，CHI说types是定理，程序是这些定理的certificate。 但是这到底意味着什么呢？ 到目前为止，我已经明白了这一点： 考虑一下id :: x -> x 。 其types表示“鉴于X是真实的，我们可以得出结论X是真实的”。 对我来说似乎是一个合理的定理。 现在考虑foo :: x -> y 。 正如任何Haskell程序员会告诉你的，这是不可能的。 你不能写这个函数。 （好吧，无论如何都不要作弊。）读作为一个定理，它说“假设任何X是真的，我们可以得出结论，任何Y是真的”。 这显然是无稽之谈。 而且，果然，你不能写这个function。 更一般地说，函数的论点可以被认为是“被假定为真的”，结果types可以被认为是“假设所有其他事物都是真的”。 如果有一个函数论证，比如说x -> y ，那么我们可以把这个假设看作X是真的，这意味着Y必须是真的。 例如， (.) :: (y -> z) -> (x -> y) -> x -> z可以被认为是“假设Y意味着Z，X意味着Y，并且X是真实的，我们可以得出结论Z是真的“。 这对我来说似乎是合情合理的。 现在，究竟是什么Int -> Int意思是？ O_O 我可以想到的唯一明智的答案是：如果你有一个函数X – > Y – > Z，那么types签名表示“假设可以构造一个Xtypes的值，另一个types为Y，那么有可能构造一个Z型的值“。 […]

Curry-Howard同构是什么引起了最有意思的等价？

在我的编程生涯中，我遇到了库里 – 霍华德同构（Curry-Howard Isomorphism）的相对较晚的时期，也许这有助于我完全着迷于它。 这意味着对于每个编程概念，在forms逻辑中都存在精确的模拟，反之亦然。 这是一个类似的“基本”清单，从我的头顶开始： program/definition | proof type/declaration | proposition inhabited type | theorem/lemma function | implication function argument | hypothesis/antecedent function result | conclusion/consequent function application | modus ponens recursion | induction identity function | tautology non-terminating function | absurdity/contradiction tuple | conjunction (and) disjoint union | disjunction (or) — corrected by […]