算法与理论计算机2018homepages.inf.ed.ac.uk
线性逻辑初尝（A Taste of Linear Logic）
A Taste of Linear Logic (1993)
进阶 · 约 75 分钟读完前置知识：λ 演算、命题逻辑基础、函数式编程
导读
Philip Wadler 1993 年的经典教程《A Taste of Linear Logic》，以通俗方式介绍线性逻辑：一种资源敏感的逻辑，其中命题如同资源，使用一次后即被消耗，不能随意复制或丢弃。论文将其与 λ 演算和函数式编程联系起来，展示了线性类型如何刻画内存管理、会话通信等计算中的资源问题。
HN 关注点：线性逻辑是 Rust 借用检查器、Haskell 线性类型扩展等现代语言特性的理论基础，HN 读者关注其与编程语言设计的深层联系。
后来怎么样
这篇教程把线性逻辑和线性类型引入了编程语言社区，是线性类型研究的经典入门文献；其思想后续发展为会话类型（Wadler 本人的 Propositions as Sessions）和 Linear Haskell 提案，也被普遍视为 Rust 所有权/借用系统的理论渊源之一。
HN 评论精选
这几条评论里：支持 1 补充 2
补充补充资料：SPJ 关于 Haskell 线性类型的演讲
Simon Peyton Jones 有一个关于将线性类型集成到 Haskell 的精彩演讲：https://www.youtube.com/watch?v=t0mhvd3-60Y
tpush查看英文原文
Here's a great talk by Simon Peyton Jones on integrating linear types into Haskell: https://www.youtube.com/watch?v=t0mhvd3-60Y
补充指出经典线性逻辑的构造性解读及其在数学和编程中的应用
线性逻辑最奇妙的一点是：经典线性逻辑具有直接的构造性解读。这在构造数学（https://arxiv.org/abs/1805.07518）和编程（多方会话协议等，见 Wadler 的 multiparty 论文）中都有有趣的应用。
fmap查看英文原文
One of the most amazing things about linear logic is that "classical" linear logic has a direct constructive reading. This has some interesting applications in constructive mathematics (https://arxiv.org/abs/1805.07518) and programming (http://homepages.inf.ed.ac.uk/wadler/papers/multiparty/multiparty.pdf).
支持热情解读：线性逻辑是资源/状态/引用的逻辑，是 Rust 借用检查器等的理论基础
线性逻辑太棒了，我认为它是 21 世纪的形式体系。它像经典逻辑但有两个玩家，从玩家 1 的视角看玩家 2 的 AND 语义不同。它是状态随时间演化的逻辑：经典逻辑中命题永恒为真，而线性逻辑处理"我有一美元"这类命题——可以花掉买冰淇淋，因此先为假、变真、再变假。它还刻画了引用与值的区别，Unix 的"一切皆文件"其实应改为"一切皆引用"。Rust 借用检查器基于线性逻辑的子集，是编译器的秘密武器，能对动态系统做静态推理。此外概率论也可基于线性逻辑（Vovk 用博弈论即本质上线性逻辑来构建概率），GAN 基于 minimax 也与线性逻辑相关。
adamnemecek查看英文原文
Linear logic is the shit. I've been reading up a lot on linear logic and certain things I have a hunch it closely corresponds to and I'm convinced it's the formalism for 21st century. Basically, it's like classical logic but with two players. From player 1's point of view, player 2's AND has different semantics than his own AND. It's the logic of state developing over time. In classical logic a statement can only be true since negative eternity and it will be true until eternity. On the other hand, linear logic deals with statements like "I have a dollar" which can be spent on an ice cream. Therefore, at some point, "I have a dollar" was false, then it became true, and then it became false again. It's also the logic that captures the difference between a reference and a value which is weirdly important. Unix's "everything is a file" should actually be recast as "everything is a reference". The Rust borrow checker is based on a subset of linear logic and it's the secret sauce of said compiler. It can reason statically about dynamic systems. I'll make some claims that I can support with papers if need to be so ask if you want proof. Currently, probability is based on measure theory however linear logic can also be used (Vovk bases probability on game theory which is essentially linear logic). Generative adversarial networks (which are based on minimax) are based on linear logic as minimax is very linear logical. I would go as far as to say that mathematics, in addition to axiom of choice also needs an axiom of adversarial choice. Axiom of choice assumes that you can always pick the best possible option, however you need to be able to account for your worst possible options as well. All mathematical optimization falls outside of classical logic. The funniest thing is that this idea, the duality of things is very old. Dialectics is very firmly rooted in Western philosophy (Aristotle, Kant, Hegel, you know the usual suspects) however no one ever extended it to a formal logic. Karl Marx (I hate Marx but realize that his ideas might have influenced people so knowing why he was wrong is worth something) also talked about a similar idea (https://en.wikipedia.org/wiki/Dialectical_materialism). In particular Engel's summary is work exploring https://en.wikipedia.org/wiki/Dialectical_materialism#Engels's_dialectics They are essentially talking about linear logic, however the third rule is very much wrong, negation of negation is not a part of a logic of two opposites. It can also be used as the foundation of probability instead of the more traditional measure theory. I can talk about this for hours.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2018Hacker News 讨论帖146 分 · 62 评
同领域还值得读
哲学家为何应关注计算复杂性
Why Philosophers Should Care About Computational Complexity (2011)
Scott Aaronson 的这篇长文论证计算复杂性理论（如 P vs NP、停机问题的复杂度视角）对哲学问题（如知识的本质、中文房间、水槽论证等）具有实质意义，而不仅是技术细…
算法与理论计算机2015 · 552 分 · 120 评进阶 · 约 90 分钟编辑精选通信的数学理论
A Mathematical Theory of Communication
是香农1948年的《通信的数学理论》，为通信建立数学框架：把信息量定义为不确定性或自由度（信息熵），并讨论信源编码、信道容量与可靠传输。
算法与理论计算机2020 · 495 分 · 91 评进阶 · 约 120 分钟编辑精选物理、拓扑、逻辑与计算：罗塞塔石碑
Physics, Topology, Logic and Computation: A Rosetta Stone (2009)
用范畴论充当“罗塞塔石碑”，试图在量子物理、拓扑、逻辑与计算四个领域之间建立统一的结构性类比：物理中的量子过程、拓扑中的配边、逻辑中的证明和计算中的程序，都可被视为某类范畴中的态…
算法与理论计算机2009 · 390 分 · 55 评 · 引用 13专业 · 约 180 分钟编辑精选一种快速、极小内存的一致性哈希算法
A Fast, Minimal Memory, Consistent Hash Algorithm
论文给出一种快速、省内存的一致哈希方案，目标是在桶数量变化时保持较小的键迁移成本，同时降低计算和内存开销。
算法与理论计算机2014 · 327 分 · 57 评 · 引用 4进阶 · 约 25 分钟编辑精选第五个 Busy Beaver 值的确定
Determination of the fifth Busy Beaver value
宣布确定了第五个 Busy Beaver 值 BB(5)：即 5 状态图灵机中停机前运行步数最多的机器（Champion）在 47,176,870 步后停机。
算法与理论计算机2025 · 288 分 · 116 评 · 引用 1专业 · 约 75 分钟编辑精选