我在我的编程生涯中相对较晚才了解到 Curry-Howard Isomorphism ,或许这也是我对它感到着迷的原因。它意味着每个编程概念都存在于形式逻辑中的一个精确的类比,反之亦然。以下是我能够想到的一些基本类比列表:
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
所以,我要问的是:这个同构有哪些更有趣/更隐晦的含义?我不是逻辑学家,所以我肯定只是浅尝辄止了这个列表。例如,这里有一些编程概念,其中我不知道在逻辑中应该使用什么简洁的名称:
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
goto | 草率下结论
- Joey Adams