1

λProlog是 Prolog 的高阶方言。另一方面，据说 HiLog使用具有一阶模型理论的高阶语法。换句话说，它们都具有高阶语法，但只有 λProlog 具有高阶语义。

高阶语义在 λProlog 中给了你什么（除了你已经通过高阶语法得到的）？λProlog 中有什么简单的例子可以说明这些收益？

4

2 回答 2

4

λProlog 最有可能实现的不仅仅是 HiLog。在我看来，HiLog 似乎是我们现在或多或少在每个 Prolog 系统中看到的，一些调用/n 和一些库（lambda）。

call/n 和 library(lambda) 可以做一种 beta-reduction。但是在 λProlog 中有一个规则 AUGMENT 和一个规则 GENERIC，没有被 beta-reduction 覆盖。这增强了底层逻辑：

G, A |- B
------------ (AUGMENT)
G |- A -: B

G |- B(c)
------------- (GENERIC) c ∉ G
G |- ∀xB(x)

AUGMENT 规则的一个典型例子是假设推理。这回答了“假设”问题。一些演绎数据库，甚至在普通 Prolog 之上实现也可以做到这一点。这里有一个简单的例子：

grade(S) :-
   take(S, german),
   take(S, french).
grade(S) :-
   take(S, german),
   take(S, italian).

take(hans, french).

上述规则表示何时有人可以评分。我们也有一些关于“汉斯”的信息。我们现在可以直接在顶层提出假设性问题，而无需修改事实数据库。

?- take(hans, german) -: grade(hans).
Yes
?- take(hans, italian) -: grade(hans).
No

我想人们也可以提出更高阶统一的理由。λProlog book 包含一些更高阶的统一示例，这些示例可能在 HiLog 中也不起作用。

也可以看看：

λProlog
Miller & Nadathur 概述 - 1988
https://www.researchgate.net/publication/220986335

假设推理的逻辑
Bonner - 1988
http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.1451

于 2020-12-04T16:24:11.010 回答
2

这是一个硬坚果。

HiLog 和 Lambda-Prolog 采用的让 Prolog “做更多”的两种想法非常不同，因此一个程序在另一个中不一定有意义。

也不是说 Lambda-Prolog 不是真正的“方言”，它是一个不同的“Prolog”，就像 ASP 是一个不同的“Prolog”一样。

现在，找到语义不同的程序意味着首先要找到具有可比性的程序，因此从程序员的角度来看“意图做同样的事情”（除了“不重要的句法细节”），因此必须将自己限制在一个共同的子集上两种语言。

另一方面，即使 Lamba Prolog 的证明过程不是（或者更好的是，不映射到）“解析反驳”，整个想法是捕捉逻辑演绎的直觉。在 HiLog 中也应该如此。

因此，“根本不同”意味着“从根本上打破程序员直觉的期望”在一种情况下，可能在两种情况下。

我想这是重新阅读论文的好时机。

于 2020-12-01T09:43:34.570 回答