柯里—霍华德对应

柯里—霍华德对应是逻辑学与计算之间的一种结构性关系：命题对应于类型，数学证明对应于属于这些类型的项，而证明简化对应于程序求值。其典型例子将直觉主义逻辑与有类型λ演算联系起来。它并不是说任意软件都构成证明，而是在特定的逻辑系统与计算系统中找出彼此对应的规则。它为证明论、类型论和计算机科学之间的联系提供了基础。(homepages.inf.ed.ac.uk)

历史发展

1934年，哈斯凯尔·柯里发现，赋予某些组合子的类型可以被解读为蕴涵逻辑中的可证公式。威廉·霍华德在一份于1969年传阅的手稿中，阐述了自然演绎与有类型λ演算之间更深层的关系。这份手稿于1980年以《公式即类型的构造观念》为题发表。霍华德还指出了证明简化与程序求值之间的对应关系。(homepages.inf.ed.ac.uk)

这一对应与布劳威尔—海廷—柯尔莫哥洛夫解释密切相关；后者通过确立逻辑联结词所表达命题的构造来解释这些联结词。后续的发展，包括德布鲁因的Automath系统和马丁-洛夫类型论，将“命题即类型”的思想扩展到了用于表达和检查数学的系统中。因此，这一名称指的是一族相互关联的对应关系，而不是一个涵盖所有逻辑和编程语言的定理。(homepages.inf.ed.ac.uk)

命题、类型与判断

这里的基本区分是命题与确立该命题的证据之间的区分。类型表示命题；具有该类型的项表示一个具体的证明。判断

\Gamma\vdash t:A

从计算角度看，表示在上下文 $\Gamma$ 的变量声明下，项 $t$ 具有类型 $A$ 。从逻辑角度看，则表示 $t$ 编码了一个推导：从该上下文所表示的假设出发，推导出命题 $A$ 。假设成为带类型的变量，推理规则则成为构造带类型项的规则。(arxiv.org)

在所选定的系统中，一个命题可证，当且仅当其对应类型中存在项。这比比较真值更强：不同的项可以记录同一命题的不同证明。将这一关系称为同构，强调的是结构的保持，不过其精确表述取决于所采用的演算，以及对证明和项所规定的等价关系。(arxiv.org)

逻辑联结词与类型构造器

对于直觉主义命题逻辑，主要的对应关系如下：

逻辑构造	类型论中的对应形式	所表示的证据
蕴涵 $A\to B$	函数类型 $A\to B$	将 $A$ 的证据转化为 $B$ 的证据的函数
合取 $A\land B$	[[product-type	积类型]] $A\times B$
析取 $A\lor B$	[[sum-type	和类型]] $A+B$
真 $\top$	单元类型	一个典范的平凡证明
假 $\bot$	空类型	在一致的系统中不存在该类型的闭项

引入规则和消去规则决定了如何构造和使用这些证据。合取引入构造一个序对；合取消去选取其中一个分量。析取消去对应于分情况分析，各个分支分别处理一种可能的标记。否定 $\neg A$ 则由 $A\to\bot$ 表示。(cs.cmu.edu)

蕴涵尤其清楚地展示了这一对应。假设 $x:A$ ，并构造出 $t:B$ ，便得到λ抽象 $\lambda x.t:A\to B$ 。将 $f:A\to B$ 应用于 $a:A$ ，便得到 $f\,a:B$ ，对应于肯定前件式。因此，恒等项 $\lambda x.x:A\to A$ 编码了 $A$ 蕴涵自身的证明。(docs.lean-lang.org)

证明简化与计算

这一对应也描述了动态过程。假设通过引入一个假设证明了某个蕴涵，随后立即通过蕴涵消去使用它。由此产生的迂回步骤，可以通过用所提供的证明替换该假设来消除。从计算角度看，这就是β归约：

(\lambda x.t)\,u\longrightarrow t[u/x],

其中，替换操作须避免捕获自由变量。同样，从一个刚构造出的序对中投影出第一个分量，会直接归约为该分量。(cs.cmu.edu)

在简单类型λ演算中，类型正确的项具有强规范化性质：每一条归约序列都会终止。相应的证明规范化结果则消除了证明中不必要的迂回步骤。不能在保留这一逻辑解释的同时，直接加入不受限制的递归：一个不终止的项可能被赋予某个类型，却无法产生其对应命题的证据。因此，将程序视为证明时，对终止性的限制至关重要。(cs.cmu.edu)

量词与更丰富的系统

依赖类型的结构可以依赖于值，从而将这一解释扩展到量化命题。类型为 $\prod_{x:D}P(x)$ 的依赖函数为每个 $x$ 提供 $P(x)$ 的证据，对应于全称量化。依赖序对 $(x,p)$ ，其中 $p:P(x)$ ，则为存在量化提供见证及相应证据。(cs.cmu.edu)

这种直接解释是构造性的。经典逻辑需要额外处理：排中律无法由基本的直觉主义规则推导出来。经典原则可以通过额外公理引入，也可以使用适当的计算机制来解释。因此，它们的计算含义不同于基本的函数与序对解释。(docs.lean-lang.org)

证明助手与验证

在基于类型论的证明助手中，证明一个定理，就是构造一个以所需命题为类型的项。自动化策略可以生成这样的项，而对其类型的检查则验证了由此得到的形式证明。这种架构是相关形式验证应用的基础。(lean-lang.org)

具体实现会进一步细化这一一般对应。例如，Lean证明助手将 Prop 中的命题与计算用的数据类型区分开来，并将同一命题的所有证明视为定义相等。其存在性证明包含见证，但一般不能通过消去该证明，将这些见证提取为可执行的数据。这些限制说明，“命题即类型”并不意味着每个证明都是一个能够生成见证的可执行程序。(docs.lean-lang.org)