作者热门文章
- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我发现了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
最佳答案
既然您明确询问了最有趣和最晦涩的内容:
您可以将 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 - 库里-霍华德同构产生的最有趣的等价是什么?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/2969140/
我是一名优秀的程序员,十分优秀!