Curry-Howard同构引发的最有趣的等价性是什么？

Question

Curry-Howard同构引发的最有趣的等价性是什么？

functional-programmingformal-methodscurry-howard

104

我在我的编程生涯中相对较晚才了解到 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

- Tom Crockett

闭包 ~= 公理集 - Apocalisp

1

+1 这个问题和所有高质量的答案和评论让我学到了比我在互联网上能学到的更多关于计算机科学的知识。 - Alexandre C.

30

@Paul Nathan：goto | 草率下结论 - Joey Adams

1

我认为所有有效程序的集合将是一个“模型”。 - Daniil

1

fst/snd | conjunction elimiation， Left/Right | disjunction introduction - Tony Morris

外部库或接口 | 公理？ - GClaramunt

10个回答

28

您在非终止方面有些混淆。假性由不可居住类型表示，根据定义，这种类型本身无法进行非终止计算，因为首先没有该类型的任何内容可以进行评估。

非终止代表矛盾——一种不一致的逻辑。不一致的逻辑当然会允许你证明任何事情，包括虚假。

忽略不一致性，类型系统通常对应于直觉主义逻辑，并且必须是构造主义的，这意味着某些古典逻辑的部分不能直接（如果有的话）表示。另一方面，这很有用，因为如果一个类型是有效的构造证明，则该类型的术语是构建您已经证明存在的任何内容的手段。

构造主义风格的一个重要特点是双重否定并不等同于非否定。实际上，否定在类型系统中很少是基元，因此我们可以将其表示为暗示虚假，例如，not P变成P -> Falsity。因此，双重否定将是一个带有类型(P -> Falsity) -> Falsity的函数，显然不等同于仅具有类型P的内容。

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

但是，这有什么意义？为什么要编写这样的类型？从编程角度来看，它是否有意义？嗯，您可以将其视为已经在某处具有P类型的函数，并需要您提供一个以P作为参数的函数，整个过程在最终结果类型中是多态的。在某种意义上，它代表了一个挂起的计算，等待其他部分的提供。在这种意义上，这些挂起的计算可以组合在一起，传递，调用等等。这应该开始听起来熟悉了，对于一些语言的粉丝，例如Scheme或Ruby，因为它意味着双重否定对应于延续传递样式，实际上我上面给出的类型正是Haskell中的延续单子。

- C. A. McCann

感谢您的纠正，我已将“虚假性”作为非终止的同义词删除。双重否定<=> CPS加1！ - Tom Crockett

1

@Antal S-Z：直觉是直觉逻辑，当然！但是，实际编写这样的函数很困难。我在您的个人资料中看到您了解Haskell，所以您可能正在考虑代数数据类型和模式匹配？请考虑一个无人居住的类型必须没有构造函数，因此没有东西可以与之进行模式匹配。你必须编写一个没有主体的“函数”，这在Haskell中是不合法的。实际上，据我所知，没有办法在Haskell中编写否定类型的术语，而不使用运行时异常或非终止。 - C. A. McCann

1

另一方面，如果等价逻辑是一致的，所有函数必须是完全的，例如，所有模式匹配必须是穷尽的。因此，为了编写一个没有模式的函数，参数类型必须没有构造函数，例如，是不可居住的。因此，这样的函数将是合法的——因此它自己的类型是有人居住的——仅当它的参数是不可居住的时候。因此，函数 P -> Falsity 等价于 P 为假。 - C. A. McCann

啊哈，我想我明白了。我一直在考虑的版本是类似于 f x = x 的东西，只有当 P = ⊥ 时才能实例化，但这显然不够通用。所以这个想法是，要返回一个无值类型，你不需要函数体；但为了使函数可定义和总体的，你不需要情况，所以如果 P 是不可居住的，一切都能解决？这有点奇怪，但我想我明白了。这似乎与我的 Xor 类型的定义相互作用得非常奇怪...我得好好想想。谢谢！ - Antal Spector-Zabusky

Antal S-Z：当且仅当P不成立时，P -> ⊥应该被占用。是的！有一个函数恰好可以占用P -> ⊥，它就是多态恒等函数应用于 ⊥，例如 ((forall A. A->A) ⊥) = ⊥ -> ⊥。 - Tom Crockett

显示剩余7条评论

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 -> *。

- Frank Atanassow

[1] - 是的，我应该更具体一些。我指的是“结构递归”，而不是无限制递归，我猜这与“折叠”相同。[3] - 它确实存在于依赖类型语言中。 - Tom Crockett

事实是，如果递归函数调用（演绎法）不会导致程序非终止，则调用所给定的参数（假设）或环境在这些调用之间必须是不同的。因此，递归只是多次应用相同的定理。如果有任何特殊情况，那就是通常增加/减少数字（归纳步骤）并检查现有情况（基本情况），这对应于逻辑中的数学归纳法。 - Earth Engine

我真的很喜欢这个图表，但我不会说“n/a”，因为一致的逻辑并不是唯一的逻辑，就像终止程序并不是唯一的程序类型一样。一个非终止函数将对应于“循环论证”，并且是Curry-Howard同构的一个很好的例子：“跟随”循环论证会让你陷入无尽的循环中。 - Joey Adams

14

function composition      | syllogism

- Apocalisp

我会说“Modus ponens”。 - undefined

13

我真的很喜欢这个问题。虽然我不是很了解，但我有一些东西（辅助维基百科文章，它本身就有一些不错的表格等）：

我认为和类型/联合类型（如 data Either a b = Left a | Right b）等价于包容性析取。虽然我对Curry-Howard不是很熟悉，但我认为这证明了它。考虑以下函数：

andImpliesOr :: (a,b) -> Either a b
andImpliesOr (a,_) = Left a

如果我理解正确，这个类型说明(a ∧ b) → (a ★ b)，并且定义说这是正确的，其中★表示包含或排除或，无论哪种Either代表。您使用Either代表排他或， ⊕; 但是，(a ∧ b) ↛ (a ⊕ b)。例如， ⊤ ∧ ⊤ ≡ ⊤，但 ⊤ ⊕ ⊥ ≡ ⊥，而 ⊤ ↛ ⊥。换句话说，如果a和b都为真，则假设为真，但结论为假，因此此蕴涵式必须为假。但是，显然，(a ∧ b) → (a ∨ b)，因为如果a和b都为真，则至少有一个为真。因此，如果区分联合是某种形式的分离，则它们必须是包含的类型。我认为这是一个证明，但请随意纠正我。

类似地，你关于tautology和absurdity的定义作为恒等函数和非终止函数有些错误。真正的公式由unit type表示，它是只有一个元素的类型(data ⊤ = ⊤;通常在函数式编程语言中拼写为()和/或Unit)。这是有道理的：因为该类型保证被占据，并且因为只有一种可能的居住者，它必须为真。恒等函数仅表示特定的重言式a → a。

根据您的意思，关于无限循环函数的评论有些牵强附会。Curry-Howard functions是类型系统中的一种，但非终止性并未编码其中。根据维基百科，处理非终止性是一个问题，因为添加它会产生不一致的逻辑（例如，我可以通过wrong x = wrong x定义wrong :: a -> b，从而“证明”对于任何a 和 b，a → b）。如果这就是你所说的“荒谬”，那么你完全正确。如果你指的是错误陈述，那么你想要的是任何 uninhabited type，例如由data ⊥定义的数据类型——即没有任何构造方式的数据类型。这确保它根本没有值，因此必须是 uninhabited，等效于 false。我认为您可能还可以使用 a -> b，因为如果禁止非终止函数，则该函数也是 uninhabited，但我不确定。

维基百科表示，公理是以两种不同的方式编码的，具体取决于您如何解释 Curry-Howard：要么在组合器中，要么在变量中。我认为 combinator 视图意味着我们默认情况下给定的原始函数编码为我们可以说的东西（类似于 modus ponens 是一个公理，因为函数应用是原始的）。我认为 variable 视图实际上也可能意味着同样的事情——毕竟，组合器只是特定函数的全局变量。至于原始类型：如果我对此的想法正确，那么我认为原始类型是实体——我们试图证明其内容的原始对象。

根据我的逻辑和语义课程，(a ∧ b) → c ≡ a → (b → c)（以及 b → (a → c））被称为输出等价性法则，至少在自然推演证明中是这样。我当时没有注意到它就是柯里化——我希望我注意到了，因为那很酷！

虽然我们现在有一种表示包容性的析取的方法，但我们没有一种表示排除性析取的方法。我们应该能够使用排除性析取的定义来表示它：a ⊕ b ≡ (a ∨ b) ∧nbsp;¬(a ∧ b)。我不知道如何写否定，但我知道 ¬p ≡ p → ⊥，而且蕴含和假语都很容易。因此，我们可以通过以下方式表示排除性析取：

data ⊥
data Xor a b = Xor (Either a b) ((a,b) -> ⊥)

这里定义了一个空类型⊥，它没有任何值，对应于假；然后定义Xor包含(并且)Either一个a或者b(或者)和一个从(a,b)(并且)到底部类型(false)的函数(蕴含)。虽然我一开始不知道这意味着什么(编辑1：现在我知道了，请看下一段!)，但是因为类型(a,b) -> ⊥没有任何值(有吗？)，所以我无法想象它在程序中的含义。是否有人知道另外一种更好的方式来思考这个定义或其他定义？(编辑1：是的，camccann。)

编辑1： 感谢camccann的回答（特别是他在评论中给我的帮助），我想我明白了这里发生了什么。要构造类型为Xor a b 的值，您需要提供两件事情。首先，作为第一个参数，证明存在a或b元素的见证；也就是说，是Left a或Right b。其次，证明既不适用于类型a又不适用于类型b的元素——换句话说，证明（a，b）是不可居住的——作为第二个参数。由于只有在（a，b）是不可居住的情况下，您才能编写从（a，b） -> ⊥的函数；那么如果它是这种情况，这意味着什么？那将意味着（a，b）的某些部分无法构建；换句话说，至少有一个，可能还有两个，即a和b也是不可居住的！在这种情况下，如果我们考虑模式匹配，您不可能对这样的元组进行模式匹配：假设b是不可居住的，则我们应该编写什么才能匹配该元组的第二部分？因此，我们不能根据它进行模式匹配，这可能会帮助您了解为什么会使其不可居住。现在，唯一的方法是拥有一个不需要参数的总函数（因为这个函数必须如此，既然（a，b）是不可居住的），就是将结果设置为一个无人居住的类型——如果我们从模式匹配的角度来看待这个问题，这意味着即使函数没有任何情况，它也没有可能有任何的体，所以一切都好。

很多时候我是在自言自语/即兴证明事情，但我希望它有用。我真的建议参考维基百科文章；我并没有详细阅读它，但它的表格是一个非常好的摘要，而且非常全面。

- Antal Spector-Zabusky

1

+1 指出 Either 是包含或的。请注意，(Either a a) 是一个定理（对于所有的 a）。 - Apocalisp

3

“Bottoms are not proofs.” 翻译为中文是“底部不等于证明。”“底部不等于证明。”这句话是指，在计算机科学和数理逻辑中，程序的正确性不能完全依赖于测试用例。需要对程序进行形式化证明，证明其在所有情况下都能产生正确的结果。“Aristoteles”是亚里士多德的拉丁名。他曾说过：“认为无法知晓和不确定的事物可以包含和决定其他事物，这是荒谬和不可能的。” - Apocalisp

2

@Tom：只是为了强调非终止的观点，如果逻辑一致，所有程序都会终止。非终止仅发生在表示不一致逻辑的类型系统中，或者等效地说，在支持图灵完备语言的类型系统中。 - C. A. McCann

1

Apocalisp: Either a a 不应该是一个定理: Either ⊥ ⊥ 仍然是无人居住的。Tom: 正如camccann所说，一致性意味着终止。因此，一致的类型系统不会允许您表达 f :: a -> b，因此该类型将是无人居住的；不一致的类型系统将有一个该类型的居民，但不会终止。camccann: 是否有一些介于不完备和图灵完备之间的不一致类型系统？或者最后一步（添加通用递归或其他东西）恰好等效于不一致性？ - Antal Spector-Zabusky

导出就是指数乘法法则！ - user76284

显示剩余2条评论

13

以下是一个相对比较晦涩的话题，我很惊讶为什么之前没有提到：“古典”函数响应式编程对应于时间逻辑。

当然，除非您是哲学家、数学家或过度追求函数编程的人，否则这可能会引起更多问题。

首先，什么是函数响应式编程？它是一种处理时变值的声明式方式。这对于编写用户界面非常有用，因为用户输入是随时间变化的值。 "古典" FRP 有两种基本数据类型：事件和行为。

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

行为是始终存在但可以不断更改的值。鼠标位置是一个很好的例子：它只是 x、y 坐标的行为。毕竟，鼠标始终有一个位置，并且概念上，随着您移动鼠标，该位置不断地变化。毕竟，移动鼠标是一个持续的单个动作，而不是一堆离散的步骤。

那么什么是时间逻辑呢？恰当的是，它是一组用于处理随时间量化的命题的逻辑规则。本质上，它扩展了具有两个量词的普通一阶逻辑：□ 和 ◇。第一个意思是"始终"：将 □φ 读作 "φ 总是成立"。第二个是"最终"：◇φ 意味着" φ 最终会成立"。这是一种特定类型的模态逻辑。以下两个法则涉及量词：

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

所以，□和◇在同样的方式上是相互对偶的，就像∀和∃一样。

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

- Tikhon Jelvis

8

与连续性和双重否定的关系有关，call/cc 的类型是 Peirce 定律http://en.wikipedia.org/wiki/Call-with-current-continuation

C-H 通常被陈述为直觉主义逻辑和程序之间的对应关系。然而，如果我们添加 call-with-current-continuation (callCC) 运算符（其类型对应于 Peirce 定律），则我们得到了经典逻辑和具有 callCC 的程序之间的对应关系。

- James Iry

6

2-continuation           | Sheffer stoke
n-continuation language  | Existential graph
Recursion                | Mathematical Induction

重要的一点是，尚未研究的是2-continuation（接受2个参数的continuation）与Sheffer stroke之间的关系。在经典逻辑中，Sheffer stroke本身可以形成完整的逻辑系统（加上一些非运算符概念）。这意味着熟悉的and，or，not只能使用Sheffer stoke或nand来实现。

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

2-continuation的类型签名是(a,b) -> Void。通过这种实现，我们可以将1-continuation（普通continuation）定义为(a,a) -> Void，乘积类型为((a,b)->Void,(a,b)->Void)->Void，求和类型为((a,a)->Void,(b,b)->Void)->Void。这给我们留下了令人印象深刻的表达能力。

如果我们深入挖掘，就会发现Piece的存在图等价于一种只有n-连续性数据类型的语言，但我没有看到任何现有的语言是以这种形式存在的。因此，我认为创造一种这样的语言可能会很有趣。

- Earth Engine

5

虽然这不是一个简单的同构，但关于构造性LEM的讨论是一个非常有趣的结果。特别是在结论部分，Oleg Kiselyov讨论了如何使用单子得到构造逻辑中的双重否定消除，类比于区分计算上可判定命题（在构造性设置中LEM有效）和所有命题。单子捕获计算效应的概念是一个老概念，但是此处的Curry-Howard同构有助于将其放入透视，并帮助理解双重否定的真正含义。

- wren romano

4

一流的Continuations支持允许您表达$P \lor \neg P$。这个技巧基于一个事实，即不调用continuation并使用某些表达式退出等效于使用同样的表达式调用continuation。

更详细的信息请参见：http://www.cs.cmu.edu/~rwh/courses/logic/www-old/handouts/callcc.pdf

- Daniil

谢谢你的见解！ - paulotorrens

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- RD1 · Accepted Answer

既然你明确要求最有趣和难以理解的内容：

你可以将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 - 这是一个很好的起点，因为它从基本原理开始，并且大部分内容都旨在让非逻辑学家/语言理论家易于理解。（虽然我是第二作者，但我有偏见。）