柯里-霍华德同构

柯里-霍華德对应是在计算机程序和数学证明之间的紧密联系;这种对应也叫做柯里-霍華德同构公式为类型对应命题为类型对应。这是对形式逻辑系统和公式计算(computational calculus)之间符号的相似性的推广。它被认为是由美国数学家 哈斯凯尔·加里和逻辑学家 William Alvin Howard独立发现的。

對應的起源、范圍和結論

对应可以在两个层面上看到,首先是 类比层次,它声称對一个函数计算出的值的类型的断言可类比于一个逻辑定理,计算这个值的程序可类比于这个定理的证明。在理论 计算机科学中,这是连接 λ演算类型论的毗邻领域的一个重要的底层原理。它被经常以下列形式陈述为“证明是程序”。一个可选择的形式化为“命题为类型”。其次,更加正式的,它指定了在两个数学领域之间的同构,就是以一种特定方式形式化的 自然演绎简单类型λ演算之间是 双射,首先是证明和项,其次是证明归约步骤和beta归约。

有多种方式考虑柯里-霍華德对应。在一个方向上,它工作于“把证明编译为程序”级别上。这裡的“证明”最初被限定为在 构造性逻辑中—典型的是 直觉逻辑系统中的证明。而“程序”是在常规的 函数式编程的意义上的;从 语法的观点上看,这种程序是用某种 λ演算表达的。所以柯里-霍華德同构的具体实现是详细研究如何把来自直觉逻辑的证明写成λ项。(这是霍華德的贡献;柯里贡献了 组合子,它是相对于是高级语言的λ演算是能写所有东西的机器语言)。最近,同样处理 经典逻辑的柯里-霍華德对应的扩展可被公式化了,通过对经典有效规则比如 双重否定除去皮尔士定律关联上明确的用续体比如 call/cc处理的一类项。

还有一个相反的方向,对一个程序的 正确性关联上“证明提取”的可能性。这在非常丰富的 类型论环境中是可行的。实际上理论家对推进非常丰富类型的函数式编程语言的开发的动机,已经部分地混合了希望带给柯里-霍華德对应更加显著的地位的因素。