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

Question

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

Answer 1

Curry-Howard 对应的不是逻辑编程，而是函数式编程。Prolog 的基本机制通过 John Robinson 的解析技术在证明理论中得到了证明，这表明如何检查表示为 Horn 子句的逻辑公式是否可满足，也就是说，您是否可以找到替换它们的逻辑变量的项，使得他们是真的。

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

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

其他几点：

1. 可以将逻辑编程基于比 Horn 子句更复杂的逻辑；例如，Lambda-prolog 基于直觉逻辑，具有与分辨率不同的计算机制。
2. 戴尔·米勒（Dale Miller）将逻辑编程背后的证明理论范式称为编程隐喻的证明搜索，以与作为程序隐喻的证明形成对比，后者是用于 Curry-Howard 对应关系的另一个术语。

Answer 2

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

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

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