Curry-Howard 同构产生的最有趣的等价是啥？

Posted 2023-05-08

【中文标题】Curry-Howard 同构产生的最有趣的等价是啥？

【英文标题】：What are the most interesting equivalences arising from the Curry-Howard Isomorphism?Curry-Howard 同构产生的最有趣的等价是什么？

【发布时间】：2011-02-27 11:43:42

【问题描述】：

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

【问题讨论】：

闭包 ~= 公理集

+1 这个问题以及所有高质量的答案和 cmets 在 CHI 方面教会了我比我在互联网上学到的更多。

@Paul Nathan: goto | jumping to conclusions

我认为所有有效程序的集合都是一个模型

fst/snd |连词消除，左/右 |析取介绍

【参考方案1】：

既然你明确要求最有趣和最晦涩的：

您可以将 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 - 这是一个很好的起点，因为它从第一原理开始，其中大部分旨在为非逻辑学家/语言理论家所用。 （虽然我是第二作者，所以我有偏见。）

【讨论】：

感谢您提供一些不那么琐碎的示例（这确实是原始问题的精神），尽管我承认其中有几个在我的脑海中......是术语“必要性”和“可能性”在逻辑上精确定义？它们如何转化为计算等价物？

我可以指出其中每一篇的已发表论文，因此它们是精确定义的。模态逻辑被大量研究（自亚里士多德以来）并且涉及不同的真理模式 - “A 必然为真”意味着“在每个可能的世界中 A 都是真的”，而“A 可能是真的”意味着“A 在一个可能的世界中是真的” .您可以证明诸如“（必然（A -> B）和可能的A） -> 可能的B”之类的东西。模态推理规则直接产生表达式构造、类型和归约规则，就像在 C-H 中一样。请参阅：en.wikipedia.org/wiki/Modal_logic 和 cs.cmu.edu/~fp/papers/mscs00.pdf

@pelotom：您可能想了解一下other kinds of logic。简单的经典逻辑在这种情况下通常没有用——我在回答中提到了直觉逻辑，但 modal 和 linear 逻辑甚至“更奇怪”，但也非常棒。

感谢您的指点，听起来我有一些阅读要做！

@RD1：你认为这很糟糕，我在 Haskell 中花了很多时间思考，以至于我必须在头脑中将谓词逻辑公式转换为类型签名，然后它们才有意义。 :( 更不用说排中律等开始看起来真的很混乱甚至可疑。

【参考方案2】：

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

不终止代表矛盾——一种不一致的逻辑。不一致的逻辑当然会allow you to proveanything，但是包括错误。

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

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

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

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

【讨论】：

感谢您的更正，我已将“虚假”作为非终止的同义词删除。 +1 双重否定 CPS!

我不太明白将 ¬p 表示为 P -> Falsity 背后的直觉。我理解它为什么起作用（¬p ≡ p → ⊥），但我没有得到代码版本。 P -> ⊥ 应该在P 不在的时候有人居住，对吧？但是这个功能不应该一直有人居住吗？或者可能永远不会，实际上，因为您不能返回⊥ 的实例？我不太明白它的条件。这里的直觉是什么？

@Antal S-Z：直觉当然是直觉逻辑！但是，是的，实际上编写这样一个函数是很困难的。我在您的个人资料中看到您知道 Haskell，所以也许您正在考虑代数数据类型和模式匹配？考虑一个无人居住的类型必须有没有构造函数，因此没有什么可以匹配的。您必须编写一个没有主体的“函数”，这不是合法的 Haskell。事实上，据我所知，如果不使用运行时异常或非终止，就无法在 Haskell 中编写否定类型的术语。

@Antal S-Z：另一方面，如果等价逻辑是一致的，那么所有的函数必须是全部的，例如，所有的模式匹配必须是穷举的。因此，为了编写一个没有模式的函数，参数类型必须没有构造函数，例如，是无人居住的。因此，这样的函数是合法的——因此它自己的类型被占用——准确地说，只有当它的参数是无人居住的时候。因此，函数P -> Falsity 等价于P 为假。

啊哈，我想我明白了。我一直在娱乐的版本类似于f x = x，如果P = ⊥ 可以实例化，但这显然不够通用。所以想法是返回一个无价值的类型，你不需要身体；但是要使函数可定义且完整，您不需要 cases，因此如果 P 无人居住，一切都会好起来吗？这有点奇怪，但我想我明白了。这似乎与我对Xor 类型的定义产生了相当奇怪的相互作用……我必须考虑一下。谢谢！

【参考方案3】：

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

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

【讨论】：

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

[1] 事实是，如果递归函数调用 (modus ponens) 不会导致程序不终止，则给予调用或环境的参数（假设）必须在那些电话。因此，递归只是多次应用相同的定理。如果有什么特别之处，通常是增加/减少数字（归纳步骤）并检查现有案例（基本案例），这对应于 - 逻辑中的数学归纳。

我真的很喜欢这张图表，但我不会说“n/a”，因为一致的逻辑不是唯一的逻辑，就像终止程序不是唯一的程序一样.非终止函数对应于“循环参数”，是 Curry-Howard 同构的一个很好的说明：“跟随”循环参数会使您陷入无限循环。

【参考方案4】：

function composition      | syllogism

【参考方案5】：

我真的很喜欢这个问题。我不知道很多，但我确实有一些东西（由the Wikipedia article 提供帮助，它有一些整洁的桌子等等）：

我认为 sum 类型/联合类型（例如 data Either a b = Left a | Right b）等同于inclusive析取。而且，虽然我对库里-霍华德不是很熟悉，但我认为这证明了这一点。考虑以下函数：

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 为真，则至少有一个为真。因此，如果有区别的联合是某种形式的析取，那么它们必须是包容的变体。我认为这可以作为一个证据，但请随意驳斥我的这个想法。

同样，您将重言式和荒谬分别定义为恒等函数和非终止函数有点偏离。真正的公式由 unit type 表示，它是只有一个元素的类型（data ⊤ = ⊤；在函数式编程语言中通常拼写为() 和/或Unit）。这是有道理的：因为这种类型是保证有人居住的，而且因为只有一个可能的居住者，所以它一定是真的。恒等函数只是表示 a → a 的特定重言式。

您对非终止函数的评论是，根据您的确切意思，更多。 Curry-Howard 在类型系统上起作用，但不在那里编码非终止。根据Wikipedia，处理非终止是一个问题，因为添加它会产生不一致的逻辑（例如，我可以通过wrong x = wrong x 定义wrong :: a -> b，从而“证明”a → b 对于任何 a 和 b）。如果这就是你所说的“荒谬”，那么你是完全正确的。如果你的意思是错误的陈述，那么你想要的是任何无人居住的类型，例如由data ⊥定义的东西——也就是说，没有任何方法来构造它的数据类型。这保证了它根本没有值，所以它一定是无人居住的，相当于false。我想你可能也可以使用a -> b，因为如果我们禁止非终止函数，那么这也是无人居住的，但我不是 100% 确定。

Wikipedia 表示公理以两种不同的方式编码，具体取决于您如何解释 Curry-Howard：组合器或变量。我认为组合子视图意味着我们得到的原始函数编码了我们默认可以说的东西（类似于 modus ponens 是公理的方式，因为函数应用程序是原始的）。而且我认为变量视图实际上可能意味着相同的东西——组合器毕竟只是作为特定函数的全局变量。至于原始类型：如果我的想法正确，那么我认为原始类型是实体——我们试图证明的原始对象。

根据我的逻辑和语义课，事实是 (a ∧ b) → c ≡ a  → (b → c)（还有那个b → (a →  c)) 被称为出口等价法，至少在自然演绎证明中如此。当时我没有注意到它只是在咖喱——我希望我有，因为那很酷！

虽然我们现在有一种方法来表示 inclusive 析取，但我们没有一种方法来表示独家品种。我们应该可以用排他析取的定义来表示：a ⊕ b ≡ (a ∨ b) ∧ ¬(a ∧ b)。我不知道如何写否定，但我知道 ¬p ≡ p → ⊥，暗示和错误都很容易。因此，我们应该能够通过以下方式表示排他性析取：

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

这将⊥定义为没有值的空类型，对应于虚假；然后将Xor 定义为包含（和）Either一个a或一个b（或 ) 和一个函数 (implication) 从 (a,b) (and) 到底部类型 (false ）。 但是，我不知道这是什么意思。（编辑1：现在我知道了，请看下一段！）从那里没有(a,b) -> ⊥ 类型的值（有吗？），我无法理解这在程序中意味着什么。有谁知道更好的方式来考虑这个定义或另一个定义？（编辑 1： 是的，camccann。）

编辑 1： 感谢camccann's answer（更具体地说，是他留下来帮助我的 cmets），我想我明白这里发生了什么。要构造Xor a b 类型的值，您需要提供两件事。首先，证明存在a 或b 的元素作为第一个参数；即Left a 或Right b。其次，证明不存在a 和b 这两种类型的元素——换句话说，证明(a,b) 是无人居住的——作为第二个论点。如果(a,b) 无人居住，您只能从(a,b) -> ⊥ 编写函数，那么这种情况意味着什么？这意味着无法构造 (a,b) 类型的对象的某些部分；换句话说，a 和b 中的至少一个，也可能两个都是无人居住的！在这种情况下，如果我们正在考虑模式匹配，你不可能在这样的元组上进行模式匹配：假设 b 是无人居住的，我们会写什么来匹配该元组的第二部分？因此，我们无法对其进行模式匹配，这可能会帮助您了解为什么这会使其无人居住。现在，拥有一个不带参数的总函数的唯一方法（这是必须的，因为(a,b) 是无人居住的）是结果也是无人居住的类型 - 如果我们从模式考虑这个 -匹配透视图，这意味着即使函数没有 case，也不可能有 body，所以一切正常。

其中很多是我在飞行中大声思考/证明（希望）的事情，但我希望它有用。我真的推荐the Wikipedia article；我没有详细阅读它，但它的表格是一个非常好的总结，而且非常彻底。

【讨论】：

+1 用于指出 Either 是包容或。注意 (Either a a) 是一个定理（对于所有 a）。

问题重新。 2（b）：唯一居民是非终止的函数类型和无人居住的函数类型有什么区别？例如，如果我声明了一个没有构造函数的类型 B，然后定义了一个函数 A->B，如下所示： fun (a:A):B := f(a) 这将在很多语言中进行类型检查，即使它是永远不可能返回 B。所以从某种意义上说，这个函数是“有人居住的”，但它的“居住者”是荒谬的……所以它根本没有真正有人居住。希望这有某种意义:)

底部不是证明。 “假设不可知和不确定的东西应该包含和确定是荒谬和不可能的。” ——亚里士多德

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

Apocalisp: Either a a 不应该是一个定理：Either ⊥ ⊥ 仍然无人居住。 Tom： 正如 camccann 所说，一致性意味着终止。因此，一致的类型系统不允许您表达f :: a -> b，因此该类型将是无人居住的；一个不一致的类型系统将有一个该类型的居民，但一个不会终止的居民。 camccann: 是否存在不一致的类型系统，它们不是图灵完备的，占用了层次结构的一些中间点？或者最后一步（添加一般递归或其他）是否完全等同于不一致？

【参考方案6】：

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

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

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

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

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

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

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

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

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

【参考方案7】：

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

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

【参考方案8】：

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（正常延续）定义为 (a,a) -> Void，产品类型为 ((a,b)->Void,(a,b)->Void)->Void，sum 类型为 ((a,a)->Void,(b,b)->Void)->Void。这让我们对它的表现力印象深刻。

如果我们进一步挖掘，我们会发现 Piece 的 existential graph 相当于一种语言，唯一的数据类型是 n-continuation，但我没有看到任何现有的语言是这种形式的。所以发明一个可能会很有趣，我认为。

【参考方案9】：

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

【参考方案10】：

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

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

【讨论】：

感谢您的洞察力！