Curry-Howard同构引起的最有趣的等价是什么？ [英] What are the most interesting equivalences arising from the Curry-Howard Isomorphism?
问题描述
在我的相对较晚的时候，我遇到了库里 - 霍华德同构编程生活，也许这有助于我对它完全着迷。这意味着对于每个编程概念，在形式逻辑中都存在精确的模拟，反之亦然。这是一个类似的基本列表，不在我头顶：
程序/定义|证明
类型/声明|命题
居住类型|定理/引理
函数|蕴含
函数的参数|假设/先行
函数结果|结论/结果
函数应用程序| modus ponens
递归|感应
身份函数|重言式
非终止函数|荒谬/矛盾
tuple |连接（和）
不相交union |分离（或） - 由Antal S-Z
参数多态|进行更正通用量化
因此，对于我的问题：什么是一些更有趣/这是同构吗？我不是逻辑学家，所以我确信我只是用这个列表来划分表面。
例如，这里有一些编程概念，我不知道逻辑中的精巧名称：
currying | （（a& b）=> c）iff（a =>（b => c））
scope | 已知理论+假设
这里有一些逻辑概念，我并没有把它放在编程术语：
原始类型？ |公理
一组有效的程序？ |理论
编辑：
从回答中收集到更多等价物：
函数组合|三段论 - 从Apocalisp
continuation-passing |双重否定 - 来自camccann
最有趣和最晦涩的：
您可以将CH扩展到许多有趣的逻辑和逻辑表达式，以获得各种各样的对应关系。在这里，我试着把重点放在一些比较有意思的部分上，而不是在晦涩难懂的部分，再加上一些尚未出现的基本部分。
评估|证明标准化/消除
变量|假设
S K combinators |逻辑公理化表达式
模式匹配|左边的规则
subtyping |隐式蕴含（不反映在表达式中）
交集类型|隐式联合
联合类型|隐式分解
开放代码|暂时的下一个
结束码|必要性
特效|可能性
可达状态|可能的世界
一元元语言|宽松逻辑
非终止|在一个不可观察的可能世界中的真理
分布式程序|模态逻辑S5 /混合逻辑
元变量|模态假设
显式替换|情境模态必然性
pi-calculus |线性逻辑
编辑：我建议有兴趣学习更多关于CH的扩展的参考：
模态逻辑的判断重构 http://www.cs.cmu.edu/~fp/papers/mscs00.pdf - 这是一个很好的开始，因为它从最初的原则开始，其中大部分目标是可以被非逻辑学家/语言理论家使用。 （虽然我是第二作者，所以我有点偏袒。）
I came upon the Curry-Howard Isomorphism relatively late in my programming life, and perhaps this contributes to my being utterly fascinated by it. It implies that for every programming concept there exists a precise analogue in formal logic, and vice versa. Here's a "basic" list of such analogies, off the top of my head:
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 S-Z
parametric polymorphism | universal quantification
So, to my question: what are some of the more interesting/obscure implications of this isomorphism? I'm no logician so I'm sure I've only scratched the surface with this list.
For example, here are some programming notions for which I'm unaware of pithy names in logic:
currying | "((a & b) => c) iff (a => (b => c))"
scope | "known theory + hypotheses"
And here are some logical concepts which I haven't quite pinned down in programming terms:
primitive type? | axiom
set of valid programs? | theory
Edit:
Here are some more equivalences collected from the responses:
function composition | syllogism -- from Apocalisp
continuation-passing | double negation -- from camccann
Since you explicitly asked for the most interesting and obscure ones:
You can extend C-H to many interesting logics and formulations of logics to obtain a really wide variety of correspondences. Here I've tried to focus on some of the more interesting ones rather than on the obscure, plus a couple of fundamental ones that haven't come up yet.
evaluation | proof normalisation/cut-elimination
variable | assumption
S K 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
EDIT: A reference I'd recommend to anyone interested in learning more about extensions of C-H:
"A Judgmental Reconstruction of Modal Logic" http://www.cs.cmu.edu/~fp/papers/mscs00.pdf - this is a great place to start because it starts from first principles and much of it is aimed to be accessible to non-logicians/language theorists. (I'm the second author though, so I'm biased.)
这篇关于Curry-Howard同构引起的最有趣的等价是什么？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
