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

Question

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

Answer 1

Curry-Howard的对应关系不是逻辑编程,而是功能编程.Prolog的基本机制在证明理论中得到了John Robinson的解析技术的证明,该技术展示了如何检查表达为Horn子句的逻辑公式是否可以满足,也就是说,是否可以找到替代它们的逻辑变量的术语他们是真的.

因此,正如我所说的,逻辑编程是关于将程序指定为逻辑公式,并且程序的计算是Prolog解决方案中的某种形式的证明推理.相比之下,Curry-Howard的对应显示了一种特殊的逻辑公式(称为自然演绎)中的证明如何与lambda演算中的程序相对应,程序的类型对应于证明证明的公式; lambda演算中的计算对应于称为归一化的证明理论中的一个重要现象,它将证明转化为新的更直接的证明.因此,逻辑编程和函数编程对应于这些逻辑中的不同级别:逻辑程序匹配逻辑的公式,而功能程序匹配公式的证明.

还有另一个不同之处:使用的逻辑通常是不同的.逻辑编程通常使用更简单的逻辑 - 正如我所说,Prolog建立在Horn子句上,这是一个高度限制的公式,其中的含义可能不是嵌套的,并且没有析取,尽管Prolog使用了它来恢复经典逻辑的全部优势.削减规则.相比之下,像Haskell这样的函数式编程语言大量使用类型具有嵌套含义的程序,并且由各种形式的多态性进行修饰.它们也是基于直觉逻辑,这是一类逻辑,禁止使用罗宾逊的计算机制所基于的被排除中间原理.

其他一些观点:

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