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 Antal SZ parametric polymorphism | universal quantification 所以，对于我的问题： 这种同构的一些更有趣/晦涩的含义是什么？ 我不是一个逻辑学家，所以我确信我只是用这个列表划痕。
例如，下面是一些编程概念，我不知道逻辑中的精明名字：
currying | "((a & b) => c) iff (a => (b => c))" scope | "known theory + hypotheses"
这里有一些逻辑上的概念，我没有把它们编入程序。
primitive type? | axiom set of valid programs? | theory
编辑：
以下是从回答中收集的更多等价物：
function composition | syllogism -- from Apocalisp continuation-passing | double negation -- from camccann
既然你明确地询问了最有趣和最晦涩的问题：
您可以将CH扩展到许多有趣的逻辑和逻辑expression式，以获得各种各样的对应关系。 在这里，我试图把重点放在一些比较有意思的部分，而不是晦涩难懂的部分，再加上一些还没有出现的基本部分。
evaluation | proof normalisation/cut-elimination variable | assumption SK combinators | axiomatic formulation of logic pattern matching | left-sequent rules subtyping | implicit entailment (not reflected in expressions) intersection types | implicit conjunction union types | implicit disjunction open code | temporal next closed code | necessity effects | possibility reachable state | possible world monadic metalanguage | lax logic non-termination | truth in an unobservable possible world distributed programs | modal logic S5/Hybrid logic meta variables | modal assumptions explicit substitutions | contextual modal necessity pi-calculus | linear logic
编辑：我会推荐给任何有兴趣学习更多关于CH的扩展的参考：
“模态逻辑的判断性重构” ~fp/papers/mscs00.pdf – 这是一个很好的开始，因为它从最初的原则开始，其中的大部分目标是非逻辑学家/语言理论家可以访问。 （虽然我是第二作者，所以我有点偏袒。）
关于非终止你有点混淆。 虚假是由无人居住的types来表示的，根据定义，虚拟types不是无止境的，因为没有任何types的东西需要首先评估。
不终止代表了矛盾 – 不一致的逻辑。 然而，不一致的逻辑当然会让你certificate 任何东西 ，包括错误。
忽略不一致性，types系统通常与直觉主义逻辑相对应，并且是必要的build构主义者 ，这意味着某些经典逻辑不能直接expression。 另一方面，这是有用的，因为如果一个types是一个有效的build设性certificate，那么这个types的术语就是一种构造你所certificate的存在的一种手段 。
build构主义风格的一个主要特征是双重否定不等于非否定。 事实上，否定在一个types体系中很less是一个原始的，所以相反，我们可以把它表示为隐含的虚假性，例如， not P变成P -> Falsity 。 双重否定因此是一个types(P -> Falsity) -> Falsity的函数，这显然不等于typesP东西。
然而，这有一个有趣的转折！ 在具有参数多态的语言中，typesvariables的范围覆盖了所有可能的types，包括无人居住的types，因此是完全多态的types，例如∀a. a ∀a. a某种意义上说，a几乎是错误的。 那么，如果我们使用多态性来写双重否定呢？ 我们得到一个如下所示的types： ∀a. (P -> a) -> a ∀a. (P -> a) -> a 。 这相当于P型的东西吗？ 事实上 ，仅仅是将其应用于身份function。
但是有什么意义呢？ 为什么要写这样的types？ 这是否意味着编程方面的任何事情？ 那么，你可以把它看作一个函数，它已经在某个地方已经有了typesP ，并且需要给它一个函数，把P作为一个参数，整个事物在最终结果types中是多态的。 从某种意义上说，它代表了一个暂停计算 ，等待剩下的提供。 从这个意义上说，这些暂停计算可以组合在一起，传递，调用，无论如何。 对于一些语言的爱好者来说，比如Scheme或者Ruby，听起来应该是很熟悉的，因为这意味着双重否定对应于延续传递风格 ，事实上我给出的types正是Haskell中的延续单子。
你的图表不太对， 在许多情况下，您会将术语与types混淆。
function type implication function proof of implication function argument proof of hypothesis function result proof of conclusion function application RULE modus ponens recursion n/a [1] structural induction fold (foldr for lists) mathematical induction fold for naturals (data N = Z | SN) identity function proof of A -> A, for all A non-terminating function n/a [2] tuple normal proof of conjunction sum disjunction n/a [3] first-order universal quantification parametric polymorphism second-order universal quantification currying (A,B) -> C -||- A -> (B -> C), for all A,B,C primitive type axiom types of typeable terms theory function composition syllogism substitution cut rule value normal proof
[1]图灵完备function语言的逻辑是不一致的。 recursion在一致的理论中没有对应关系。 在一个不一致的逻辑/不合理的certificate理论中，你可以把它称为一个导致不一致/不稳定的规则。
[2]这也是完整性的结果。 如果逻辑是一致的，那么这将是一个反定理的certificate – 因此它不可能存在。
[3]在函数式语言中不存在，因为它们消除了一阶逻辑特征：所有的量化和参数化都是通过公式完成的。 如果你有一阶function，那么除了* ， * -> *等之外， 话语领域的这种元素。 例如，在Father(X,Y) :- Parent(X,Y), Male(X) ， X和Y在话语范围（称为Dom ）和Male :: Dom -> * 。
我真的很喜欢这个问题。 我不是很了解，但是我确实有一些东西（由维基百科的文章提供 ，这个文章有一些整洁的表格等等）：
-
我认为总和types/联合types（ 例如
data Either ab = Left a | Right b）相当于包容性分离。 而且，虽然我不太了解库里 – 霍华德，但我认为这也certificate了这一点。 考虑以下function：andImpliesOr :: (a,b) -> Either ab andImpliesOr (a,_) = Left a如果我理解正确，那么types表示（a∧b）→（ a ★ b ）并且定义说这是真的，其中★是包含性的或排他性的，或者无论哪
Either表示。 你有Either代表独家或者，⊕; 然而，（a∧b）↛（a⊕b）。 例如⊤∧⊤≡⊤，但是⊕⊥⊥和⊤↛⊥。 换句话说，如果a和b都是真的，那么这个假设是正确的，但结论是错误的，所以这个含义必须是假的。 然而，显然，（a∧b）→（a∨b），因为如果a和b都是真的，那么至less有一个是真的。 因此，如果被歧视的工会是某种forms的分离，他们必须是包容性的多样性。 我认为这是一个certificate，但是更多的是自由地解除这个观念。 -
同样，你对重言式和荒谬性的定义分别作为身份函数和非终结函数，也是有点偏离的。 真正的公式由单元types来表示，它是只有一个元素的types（
data ⊤ = ⊤;在函数式编程语言中经常被拼写()和/或Unit）。 这是有道理的，因为这种types是有保障的 ，因为只有一个可能的居民，所以一定是真的。 身份函数仅仅代表了a → a的特定重言式。你对非终结函数的评论，取决于你的意思，更多closures。 types系统上的Curry-Howardfunction，但是非终止不在那里编码。 根据维基百科 ，处理非终止是一个问题，因为添加它会产生不一致的逻辑（ 例如 ，我可以通过
wrong x = wrong x来定义wrong :: a -> b，从而“certificate” a → b a和b ）。 如果这就是“荒谬”的意思，那么你完全正确。 如果你的意思是虚假陈述，那么你想要的就是任何无人居住的types， 比如由data ⊥定义的东西 – 也就是说，一个没有任何方法来构造它的数据types。 这确保它没有任何价值，所以它必须是无人居住的，这相当于假的。 我想你可能也可以使用a -> b，因为如果我们禁止非终止函数，那么这也是无人居住，但我不是100％确定。 -
维基百科说，公理是以两种不同的方式编码的，取决于你如何解释库里 – 霍华德：无论是在组合或variables。 我认为combinator视图意味着我们给出的基本函数默认编码我们可以说的东西（类似于modus ponens是一个公理，因为函数应用是原始的）。 而且我认为variables视图实际上可能意味着同样的事情 – 组合器毕竟只是作为特定函数的全局variables。 至于原始types：如果我正确地思考这个问题，那么我认为原始types是实体 – 我们试图certificate的东西的原始对象。
-
根据我的逻辑和语义学的类别，（ a ^ b ）→c≡a→（ b → c ）（也称为b →（ a → c ））这个事实被称为输出等价定律，至less在自然演绎certificate。 当时我没有注意到它只是咖啡，我希望我有，因为这很酷！
-
虽然我们现在有一种方法来表示包容性分离，但是我们没有办法来表示这个独有的变体。 我们应该能够使用排他析取的定义来表示：a⊕b≡（a∨b）∧¬（a∧b）。 我不知道怎么写否定，但我知道¬p≡p→⊥，而且蕴涵和谬误都很容易。 因此，我们应该能够通过以下方式performance出独占性的不合
data ⊥ data Xor ab = Xor (Either ab) ((a,b) -> ⊥)这将
⊥定义为没有值的空types，这对应于错误; 然后将Xor定义为包含（ 和 ） a或b （ 或 ）和（a，b） （ 和 ）到底部types（ false ）的函数（ 蕴含 ）。不过，我不知道这是什么意思 。（ 编辑1：现在我看，下一个段落！）由于没有types(a,b) -> ⊥（在那里）的值，所以我无法理解这在程序中意味着什么。有没有人知道更好的方式来思考这个定义或另一个？（ 编辑1：是， camccann 。）编辑1：感谢camccann的回答 （更具体地说，他留下的意见，以帮助我），我想我看看这里发生了什么。 要构造一个
Xor abtypes的值，你需要提供两件事情。 首先，certificatea或b的一个元素是第一个参数的存在; 即Left a或Right b。 其次，certificate不存在a和btypesa元素 – 换句话说，certificate(a,b)是无人的 – 作为第二个参数。 如果(a,b)无人居住，你只能从(a,b) -> ⊥写一个函数，那么这意味着什么呢？ 那就意味着(a,b)types的某个对象的某个部分不能被构造; 换句话说，a和b中至less有一个，也可能两个都是无人居住的！ 在这种情况下，如果我们考虑模式匹配，那么就不可能在这样一个元组上进行模式匹配：假设b是无人的，我们会写什么来匹配这个元组的第二部分？ 因此，我们不能模式匹配它，这可能会帮助你明白为什么这使得它无人居住。 现在，拥有一个没有任何争论的总function（因为(a,b)无人居住的这个必须的唯一方法）是结果也是一个无人居住的types – 如果我们从模式匹配的angular度来看，这意味着即使函数没有案例，也没有可能的实体，所以一切正常。
其中很多是我大声思考/希望能够在飞行中certificate一些事情，但我希望这是有用的。 我真的推荐维基百科的文章 ; 我没有详细阅读过，但是它的表格是一个很好的总结，而且非常全面。
function composition | syllogism
这是一个稍微模糊的，我很惊讶，没有提出更早：“经典”function反应编程对应于时态逻辑。
当然，除非你是哲学家，math家或执着的function程序员，否则这可能会带来更多的问题。
所以，首先：什么是function性反应式编程？ 这是一个声明性的方式来处理随时间变化的值 。 这对编写诸如用户界面之类的东西很有用，因为来自用户的input是随时间变化的值。 “古典”玻璃钢有两种基本的数据types：事件和行为。
事件表示只存在于离散时间的值。 击键是一个很好的例子：您可以将键盘的input视为一个给定时间的字符。 每个按键与键的字符和按下的时间只是一对。
行为是不断存在的价值，但可以不断变化。 鼠标位置就是一个很好的例子：它只是x，y坐标的行为。 毕竟，鼠标总是有一个位置，从概念上讲，当你移动鼠标时，这个位置会不断变化。 毕竟，移动鼠标是一个单一的长期行动，而不是一堆离散的步骤。
什么是时态逻辑？ 恰当地说，这是处理随时间量化的命题的一套逻辑规则。 本质上，它用两个量词扩展正常的一阶逻辑：□和◇。 第一种意思是“总是”：将□φ读为“φ总是成立”。 第二个是“最终”：◇φ表示“φ最终会成立”。 这是一种特殊的模态逻辑 。 以下两个法则涉及量词：
□φ ⇔ ¬◇¬φ ◇φ ⇔ ¬□¬φ
所以□和◇与∀和∃相同。
这两个量词对应于FRP中的两种types。 特别是，□对应于行为，◇对应于事件。 如果我们考虑这些types如何居住，这应该是有道理的：一个行为在每个可能的时间居住，而一个事件只发生一次。
与延续和双重否定之间的关系有关，call / cc的types是Peirce定律http://en.wikipedia.org/wiki/Call-with-current-continuation
CH通常被认为是直觉逻辑和程序之间的对应关系。 但是，如果我们添加call-with-current-continuation（callCC）操作符（其types符合Peirce定律），我们就可以通过callCC获得经典逻辑和程序之间的对应关系。
虽然这不是一个简单的同构，但是这种对build设性LEM的讨论是一个非常有趣的结果。 特别是在结论部分，Oleg Kiselyov讨论了如何在build构性逻辑中使用单子获得双重否定消除，类似于在所有命题中区分计算上可判断的命题（LEM在build设性环境中是有效的）。 单子捕捉计算效应的观念是一个古老的概念，但是这个库里 – 霍华德同构的例子有助于理解它，并帮助理解双重否定的真正“意义”。
一stream的延续支持可以让你expression$ P \ lor \ neg P $。 诀窍是基于这样一个事实，即不用调用继续和退出某个expression式相当于用相同的expression式来调用继续。
有关更详细的视图，请参阅： http : //www.cs.cmu.edu/~rwh/courses/logic/www-old/handouts/callcc.pdf
2-continuation | Sheffer stoke n-continuation language | Existential graph Recursion | Mathematical Induction
有一件很重要的事情，但尚未被调查的是2连续（带2个参数的连续）和Sheffer笔画的关系 。 在经典逻辑中，Sheffer stroke是实际需要的单个逻辑运算符。 这意味着熟悉的， or not只用Sheffer stoke或nand来实现。
这是编程types对应的一个重要事实，因为它提示可以使用单一types来形成所有其他types。
2连续的types签名是(a,b) -> Void 。 通过这个实现，我们可以把(a,a) – > Void， ((a,b)->Void,(a,b)->Void)->Void产品types定义为1-延拓键入为((a,a)->Void,(b,b)->Void)->Void 。 这给了我们一个performance力的印象深刻。
如果我们进一步挖掘，我们会发现Piece的存在图相当于一种只有数据types的语言是n连续的，但是我没有看到任何现有的语言是以这种forms存在的。 所以发明一个可能是有趣的，我想。
