Hacker"Propositions as Types" by Philip Wadler
Strange Loop ConferenceYouTube ↗
延伸阅读 1
字幕解读
Philip Wadler 从可计算性和 lambda calculus 讲到自然演绎与简单类型 lambda 演算：逻辑命题对应类型，证明对应程序，证明规范化对应程序求值；简单类型系统还保证程序终止。Curry–Howard 对应由逻辑学家与计算机科学家分别发现，促使讲者主张某些结构是被发现而非任意发明。问答延伸到依赖类型、线性逻辑及并发类型的研究。
自动字幕 · 引文按字幕原文展示，可点时间戳回看片段。
内容要点
- 逻辑中的命题、证明和证明化简，分别对应程序类型、程序项和求值。
- 简单类型 lambda 演算可保证终止；加入一般递归后，停机问题又无法普遍判定。
- 逻辑与类型间的深层对应支持“结构被发现”的看法，但演讲也指出编程语言仍含约定成分。
视频章节 6
- 算法与可计算性问题
- Hilbert 问题与不可判定性
- Church、Gödel 与 Turing
- 自然演绎与证明规范化
- 简单类型 lambda 演算
- 命题即类型与 Curry–Howard
具体观点与证据 4
要证明某个问题不存在算法解，必须先精确定义算法可表达的范围。
讲者用判定问题的历史说明形式化的动机。
need a formal definition of algorithm so you can show that no algorithm is going to work命题、证明和证明化简分别对应类型、程序和程序求值，Curry–Howard对应涉及结构与运行过程。
演示使用蕴涵、合取与简单类型lambda演算，不是任何语言程序都自动构成可靠证明。
proofs in the logic correspond to terms programs in the programming language简单类型lambda演算的终止保证依赖排除无限制的一般递归；加入不动点算子会改变这一边界。
这是受限语言的保证，并未解决任意程序的停机问题。
if you've typed it and you're not using What's called the fixo operator that is unlimited General recursion线性逻辑与会话类型的对应为并发通信协议提供形式化研究方向。
讲者明确称其为进行中的研究，不能当作已解决所有分布式问题。
linear Logic on the left seems to correspond to things called session Types补充字幕原文 2
演讲以“由计算机执行的一系列指令”作为算法的直观起点。
an algorithm is a sequence of instructions followed by a computer命题与程序类型相对应，是演讲对 Curry–Howard 关系的核心概括。
propositions in logic correspond to types in a programming language解读边界
演讲是对 Curry–Howard 关系的教学性阐释，并以历史和哲学观点延伸；“发现而非发明”是论证立场，不是由数学对应本身唯一推出的结论。字幕含较多专名 ASR 错误。