4

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

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

这个困境能解决吗？

4

1 回答 1

0

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

这些是无类型的：

来自 HiOrd 论文：

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

  • Ciao（包括 HiOrd）
于 2020-12-13T23:56:20.503 回答