logic - 关于逻辑和Curry-Howard对应的问题

Question

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

Answer 1

Curry-Howard的对应关系与逻辑编程无关，而与函数编程有关。证明理论中，约翰·罗宾逊的resolution technique证明了Prolog的基本原理是正确的，这表明了如何检查表达为Horn子句的逻辑公式是否为satisfiable，即，是否可以找到替代它们的逻辑变量的术语。真的。

因此，逻辑编程就是将程序指定为逻辑公式，而程序的计算是Prolog解决方案中某种形式的证明推论，正如我所说的。与此相反，Curry-Howard对应关系表明，在称为natural deduction的特殊逻辑公式中的证明如何与lambda微积分中的程序相对应，并且程序的类型与证明所证明的公式相对应。 Lambda演算中的计算与证明理论中的一个重要现象相称，即归一化，该现象将证明转化为新的，更直接的证明。因此，逻辑编程和功能编程在这些逻辑中对应不同的层次:逻辑程序匹配逻辑公式，而功能程序匹配公式证明。

还有另一个区别:所使用的逻辑通常是不同的。逻辑编程通常使用更简单的逻辑-正如我所说，Prolog建立在Horn子句的基础上，Horn子句是一类严格限制的公式，其中的含义可能不会嵌套，也没有析取，尽管Prolog使用削减规则。相反，诸如Haskell之类的函数式编程语言大量使用了类型具有嵌套含义的程序，并以各种形式的多态性为装饰。它们还基于直觉逻辑，这是一类逻辑，禁止使用罗宾逊的计算机制所基于的排除中间原理。

其他一些要点:

可以将逻辑编程基于比Horn子句更复杂的逻辑。例如，Lambda-prolog基于直觉逻辑，其计算机制与分辨率不同。

Dale Miller称逻辑证明后的证明理论范式为证明搜索作为编程隐喻，以与证明作为程序隐喻进行对比，后者是用于Curry-Howard对应的另一个术语。