关于逻辑和库里-霍华德对应关系的问题

Posted 2023-05-08

【中文标题】关于逻辑和库里-霍华德对应关系的问题

【英文标题】：A question about logic and the Curry-Howard correspondence

【发布时间】：2011-02-19 05:41:18

【问题描述】：

您能否解释一下逻辑编程的基础与类型系统和常规逻辑之间的句法相似现象之间的基本联系是什么？

【问题讨论】：

你能不能说的更具体一些，或者提供一些例子？

【参考方案1】：

Curry-Howard 对应的不是逻辑编程，而是函数式编程。 Prolog 的基本机制由 John Robinson 的resolution technique 在证明论中得到证明，它显示了如何检查表示为 Horn 子句的逻辑公式是否为satisfiable，也就是说，您是否可以找到替换它们的逻辑的术语使它们成为真的变量。

因此，逻辑编程是关于将程序指定为逻辑公式，而程序的计算是某种形式的证明推理，在 Prolog 中，正如我所说的那样。相比之下，Curry-Howard 对应显示了特殊逻辑公式中的证明，称为natural deduction，如何对应于 lambda 演算中的程序，程序的类型对应于证明证明的公式； lambda 演算中的计算对应于证明理论中的一个重要现象，称为规范化，它将证明转换为新的、更直接的证明。所以逻辑编程和函数式编程对应于这些逻辑的不同层次：逻辑程序匹配逻辑的公式，而函数式程序匹配公式的证明。

还有另一个区别：使用的逻辑通常不同。逻辑编程通常使用更简单的逻辑——正如我所说，Prolog 是建立在 Horn 子句上的，这是一个高度受限的公式类，其中蕴涵可能不会嵌套，并且没有析取，尽管 Prolog 使用削减规则。相比之下，像 Haskell 这样的函数式编程语言大量使用了类型具有嵌套含义的程序，并被各种形式的多态性修饰。它们还基于直觉逻辑，这是一类禁止使用排中原理的逻辑，罗宾逊的计算机制就是基于该原理的。

其他几点：

可以将逻辑编程基于比 Horn 子句更复杂的逻辑；例如，Lambda-prolog 基于直觉逻辑，其计算机制与解析不同。 Dale Miller 将逻辑编程背后的证明理论范式称为 proof search as programming 隐喻，与 proofs as program 隐喻形成对比，后者是另一个用于库里-霍华德的对应关系。

【讨论】：

多么美妙的解释！你比我读过的 wiki 和书籍做得更好，非常感谢！

还有一个想问（可能有点傻）的问题：一般来说，lambda演算中的一等函数对应于WRT到自然演绎..这些高阶谓词是什么？

糟糕，如果用谓词扩展，我的意思是“自然演绎”:)

对不起，另一个评论：只是为了清楚我最后一个问题的要点-请您帮我破译functional programming languages such as Haskell make heavy use of programs whose types have nested implications这个短语吗？

@Bubba：一阶谓词演算中的量化对应于 lambda 演算中的依赖类型：有几种方法可以做到这一点。你不能用 Horn 子句表达像 m​​ap 这样的组合子：类型是 (a -> b) -> [a] -> [b]，其中第一个 "->" 是嵌套的，因为它出现在括号的左侧final "->"，使其成为 2 阶函数。 Horn 子句只能表达 1 阶函数。

【参考方案2】：

逻辑编程本质上是关于目标导向的证明搜索。类型语言和逻辑之间的结构关系通常涉及函数式语言，尽管有时是命令式和其他语言 - 但不是直接的逻辑编程语言。这种关系将证明与程序相关联。

因此，逻辑编程证明搜索可用于查找证明，然后将其解释为功能程序。这似乎是两者之间最直接的关系（正如您所要求的）。

以这种方式构建整个程序并不实用，但它对于在程序中填充繁琐的细节很有用，并且在实践中有一些重要的例子。这方面的一个基本示例是结构子类型 - 它对应于通过简单的蕴涵证明填写几个证明步骤。一个更复杂的例子是 Haskell 的类型类系统，它涉及一种特定类型的目标导向搜索——在极端情况下，这涉及编译时的图灵完备形式的逻辑编程。