102

我在编程生涯中比较晚才接触到Curry-Howard 同构，也许这有助于我对它完全着迷。这意味着对于每个编程概念，在形式逻辑中都存在一个精确的类比，反之亦然。这是我想不到的此类类比的“基本”列表：

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
4

10 回答 10

36

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

您可以将 CH 扩展到许多有趣的逻辑和逻辑公式，以获得非常广泛的对应关系。在这里，我试图专注于一些更有趣的而不是晦涩的，以及一些尚未出现的基本问题。

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

编辑：我推荐给任何有兴趣了解更多关于 CH 扩展的人的参考：

“模态逻辑的判断性重构” http://www.cs.cmu.edu/~fp/papers/mscs00.pdf - 这是一个很好的起点，因为它从第一原则开始，其中大部分旨在成为非逻辑学家/语言理论家可以访问。（虽然我是第二作者，所以我有偏见。）

于 2010-07-30T09:22:57.580 回答
27

关于非终止，你有点混淆了。虚假由无人居住的类型表示，根据定义，它不能是非终止的，因为首先没有要评估的那种类型。

不终止代表矛盾——一种不一致的逻辑。但是，不一致的逻辑当然可以让您证明 任何事情，包括错误。

忽略不一致性，类型系统通常对应于直觉逻辑，并且必然是建构主义的，这意味着某些经典逻辑不能直接表达，如果有的话。另一方面，这很有用，因为如果一个类型是一个有效的建设性证明，那么该类型的一个术语就是一种构建任何你已经证明存在的东西的方法。

建构主义风格的一个主要特征是双重否定不等于非否定。事实上，否定在类型系统中很少是原语，因此我们可以将其表示为暗示错误，例如，not P变为P -> Falsity。因此，双重否定将是一个带有 type 的函数(P -> Falsity) -> Falsity，这显然不等同于只是 type 的东西P。

然而，这有一个有趣的转折！在具有参数多态性的语言中，类型变量涵盖所有可能的类型，包括无人居住的类型，因此∀a. a在某种意义上，完全多态的类型几乎是假的。那么如果我们使用多态性来写双重几乎否定呢？我们得到一个看起来像这样的类型：∀a. (P -> a) -> a. 那是否等同于某种类型的东西P？确实如此，只需将其应用于恒等函数即可。

但有什么意义呢？为什么要写这样的类型？它在编程方面有什么意义吗？好吧，您可以将其视为一个函数，该函数在某处已经具有某种类型P，并且需要您给它一个以P作为参数的函数，整个事物在最终结果类型中是多态的。从某种意义上说，它代表了一个暂停的计算，等待其余的提供。从这个意义上说，这些暂停的计算可以组合在一起，传递，调用，等等。对于某些语言的爱好者来说，这应该开始听起来很熟悉，比如 Scheme 或 Ruby——因为这意味着双重否定对应于延续传递风格，实际上我上面给出的类型正是 Haskell 中的 continuation monad。

于 2010-06-03T21:08:01.657 回答
15

你的图表不太对；在许多情况下，您将类型与术语混淆了。

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 | S N)
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] 图灵完备的函数式语言的逻辑是不一致的。递归在一致的理论中没有对应关系。在不一致的逻辑/不健全的证明理论中，您可以将其称为导致不一致/不健全的规则。

[2] 同样，这是完整性的结果。如果逻辑是一致的，这将是一个反定理的证明——因此，它不存在。

[3] 在函数式语言中不存在，因为它们省略了一阶逻辑特征：所有量化和参数化都是通过公式完成的。如果你有一阶特征，就会有除*,* -> *等以外的一种；话语领域的元素的种类。例如，在Father(X,Y) :- Parent(X,Y), Male(X)和X范围Y内的话语域（称为Dom），和Male :: Dom -> *。

于 2010-06-17T09:32:25.253 回答
14 
function composition      | syllogism
于 2010-06-03T20:26:36.887 回答
13
于 2010-06-03T20:36:46.473 回答
13

这是一个有点晦涩的问题，我很惊讶没有早点提出：“经典”函数式反应式编程对应于时间逻辑。

当然，除非你是哲学家、数学家或痴迷的函数式程序员，否则这可能会带来更多问题。

那么，首先：什么是函数式反应式编程？这是一种处理随时间变化的值的声明方式。这对于编写用户界面之类的东西很有用，因为来自用户的输入是随时间变化的值。“经典”FRP 有两种基本数据类型：事件和行为。

事件表示仅在离散时间存在的值。击键就是一个很好的例子：您可以将键盘的输入视为给定时间的一个字符。然后，每个按键都只是键的字符和按下时间的一对。

行为是不断存在但可以不断变化的价值观。鼠标位置就是一个很好的例子：它只是 x、y 坐标的行为。毕竟，鼠标总是有一个位置，从概念上讲，这个位置会随着你移动鼠标而不断变化。毕竟，移动鼠标是一个持久的动作，而不是一堆离散的步骤。

什么是时间逻辑？恰当地说，它是一组处理随时间量化的命题的逻辑规则。本质上，它用两个量词扩展了正常的一阶逻辑：□和◇。第一个意思是“总是”：把□φ读作“φ总是成立”。第二个是“最终”：◇φ表示“φ最终会成立”。这是一种特殊的模态逻辑。以下两条定律与量词有关：

□φ ⇔ ¬◇¬φ
◇φ ⇔ ¬□¬φ

所以□和◇与∀和∃一样是对偶的。

这两个量词对应FRP中的两种类型。特别是，□对应行为，◇对应事件。如果我们考虑这些类型是如何存在的，这应该是有道理的：一种行为在每个可能的时间都存在，而一个事件只发生一次。

于 2013-05-11T04:32:53.203 回答
8

关于延续和双重否定的关系，call/cc的类型是皮尔斯定律http://en.wikipedia.org/wiki/Call-with-current-continuation

CH 通常表示为直觉逻辑和程序之间的对应关系。但是，如果我们添加 call-with-current-continuation (callCC) 运算符（其类型对应于皮尔士定律），我们会得到经典逻辑和带有 callCC 的程序之间的对应关系。

于 2012-09-07T20:23:15.293 回答
6 
2-continuation           | Sheffer stoke
n-continuation language  | Existential graph
Recursion                | Mathematical Induction

重要但尚未研究的一件事是 2-continuation（采用 2 个参数的延续）和Sheffer stroke的关系。在经典逻辑中，Sheffer stroke 可以自己形成一个完整的逻辑系统（加上一些非算子的概念）。这意味着熟悉and的or,not可以仅使用 Sheffer stoke 或 来实现nand。

这是其编程类型对应的一个重要事实，因为它提示可以使用单个类型组合器来形成所有其他类型。

2-continuation 的类型签名是(a,b) -> Void. 通过这种实现，我们可以将 1-continuation（正常的延续）定义为(a,a)-> Void，乘积类型为((a,b)->Void,(a,b)->Void)->Void，总和类型为((a,a)->Void,(b,b)->Void)->Void。这让我们对它的表现力印象深刻。

如果我们进一步挖掘，我们会发现 Piece 的存在图等价于一种语言，唯一的数据类型是 n-continuation，但我没有看到任何现有的语言是这种形式的。所以发明一个可能会很有趣，我想。

于 2012-12-22T14:07:35.787 回答
5

虽然这不是一个简单的同构，但这个关于建设性 LEM的讨论是一个非常有趣的结果。特别是，在结论部分，Oleg Kiselyov 讨论了如何在构造逻辑中使用单子来消除双重否定，这类似于将计算可判定命题（LEM 在构造设置中有效）与所有命题区分开来。monads 捕获计算效果的概念是一个古老的概念，但是 Curry-Howard 同构的这个例子有助于理解它，并有助于理解双重否定的真正“含义”。

于 2010-06-04T02:42:11.403 回答
4

一流的延续支持允许您表达 $P \lor \neg P$。诀窍是基于这样一个事实，即不调用延续并使用某个表达式退出等同于使用相同的表达式调用延续。

更详细的视图请看：http ://www.cs.cmu.edu/~rwh/courses/logic/www-old/handouts/callcc.pdf

于 2012-09-27T08:46:32.327 回答