关于逻辑和Curry-Howard对应关系的一个问题

Question

你能给我解释一下逻辑编程的基本原理和类型系统和传统逻辑之间的语法相似现象之间的基本联系吗？

Answer 1

Curry-Howard对应关系不是逻辑编程，而是函数式编程。Prolog的基本机制由John Robinson的resolution technique在证明理论中得到了证明，该理论展示了如何检查表示为Horn子句的逻辑公式是否为，即您是否可以找到使它们为真的逻辑变量的替代项。

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

还有另一个区别:使用的逻辑通常是不同的。逻辑编程通常使用更简单的逻辑-正如我所说的，Prolog是建立在Horn子句上的，Horn子句是一类高度受限的公式，其中的含义可能不是嵌套的，并且没有析取，尽管Prolog使用截断规则恢复了经典逻辑的全部强度。相比之下，函数式编程语言，如Haskell，大量使用类型具有嵌套含义的程序，并由各种形式的多态性装饰。它们还基于直觉逻辑，这是一类禁止使用排除中间原则的逻辑，而罗宾逊的计算机制正是基于该原则。

其他一些要点：

prolog逻辑编程可以基于比Horn子句更复杂的逻辑；例如，Lambda-

• 是基于直觉逻辑的，具有不同的计算机制，而不是米勒将逻辑编程背后的证明论范式称为证明搜索为编程隐喻，以与另一个用于库里-霍华德correspondence.

的术语证明作为程序隐喻形成对比

Answer 2

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

因此，可以使用逻辑编程证明搜索来查找证明，然后将这些证明解释为函数式程序。这似乎是两者之间最直接的关系(正如您所要求的)。

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