functional-programming - Curry-Howard同构引起的最有趣的等价是什么？

我在编程生活中才来到Curry-Howard Isomorphism的较晚时期，也许这让我对它非常着迷。这意味着对于每个编程概念，形式逻辑中都存在一个精确的类似物，反之亦然。这是此类比喻的“基本” list ，让我无所适从:

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

那么，对我的问题:这种同构有哪些更有趣/晦涩的含义？ 我不是逻辑学家，所以我敢肯定，我只是从表面上摸索了这份 list 。

例如，以下是一些编程概念，我不知道它们的逻辑名称:

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

最佳答案

由于您明确要求最有趣和晦涩的内容:

您可以将C-H扩展到许多有趣的逻辑和逻辑公式，以获得种类繁多的对应关系。在这里，我尝试着眼于一些更有趣的主题，而不是晦涩难懂的主题，再加上一些尚未出现的基本主题。

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

编辑:我将向有兴趣了解C-H扩展的更多人推荐引用:

“模态逻辑的判断性重构” http://www.cs.cmu.edu/~fp/papers/mscs00.pdf-这是一个很好的起点，因为它是从第一原理开始的，并且其大部分目标是非逻辑学家/语言理论家可以使用的。 (尽管我是第二作者，所以我有偏见。)

关于functional-programming - Curry-Howard同构引起的最有趣的等价是什么？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/2969140/