prolog - 是否有不需要类型系统的更高阶 Prolog？

Question

我怀疑 λProlog 需要一个类型系统来使它们的
高阶统一听起来不错。否则通过自我应用
可能会出现一些罗素型异常。

是否有不需要 .sig 文件的替代高阶 Prolog？
也许通过一个更简单的类型系统，不需要那么多
声明但仍然有某种形式的高阶统一？

这个困境能解决吗？

标签： prologhigher-order-functionslambda-prolog

Answer 1

是否有不需要类型系统的更高阶 Prolog？

这些是无类型的：

• HiLog

• 历史记录

来自 HiOrd 论文：

提出的框架提出了许多作者希望在未来研究中解决的问题。特别是，为了与其他高阶形式系统（Hilog、Lambda-Prolog）进行比较，必须进行严格的处理。例如，通过擦除类型将 λProlog 的高阶 Horn 片段保守地转换为 Hiord 是相当简单的，因为解析规则本质上是相同的（假设类型安全的高阶统一过程）。

• Ciao（包括 HiOrd）