4

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

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

这个困境能解决吗?

4

1 回答 1

0

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

这些是无类型的:

来自 HiOrd 论文:

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

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