类型化SLD-Resolution：逻辑编程的动态类型化
摘要：逻辑编程的语义基础通常分为两种不同的方法。操作语义使用SLD-resolution，这是一种计算逻辑编程中的答案的证明方法，而声明性语义将逻辑程序视为公式，它的语义为模型。在这里，我们定义了一种新的操作语义，称为TSLD-resolution，其中包括一个值“wrong”，它对应于在运行时检测到类型错误。为此，我们定义了一种新的类型一致性算法。最后，我们证明了TSLD-resolution相对于一个有类型声明的语义的正确性。
作者：Jo~ao Barbosa, M''ario Florido, V''itor Santos Costa
论文ID：2208.00192
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-08-02