λProlog 中的高阶语义给了你什么? [英] What does higher-order semantics give you in λProlog?

问题描述

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

λProlog is a higher-order dialect of Prolog. On the other hand, HiLog is said to use higher-order syntax with first-order model theory. In other words, they both have higher-order syntax, but only λProlog has higher-order semantics.

高阶语义在 λProlog 中为您提供了什么(超出您仅使用高阶语法已经获得的)?λProlog 中说明这些收益的简单示例是什么?

What does higher-order semantics give you in λProlog (beyond what you already get with higher-order syntax alone)? What would be a simple example in λProlog that illustrates these gains?

推荐答案

最有可能的是，λProlog 比 HiLog 实现的更多.在我看来，HiLog 似乎是我们现在或多或少在每个 Prolog 系统中看到的，一些调用/n 和一些库(lambda).

Most likely, λProlog implements more than HiLog. HiLog seems to me what we nowadays more or less see in every Prolog system, some call/n and some library(lambda).

call/n 和 library(lambda) 可以做一种 beta-reduce.但是在 λProlog 中有一个规则 AUGMENT 和一个规则 GENERIC，不包括在 beta-reduction 中.这增强了底层逻辑:

The call/n and library(lambda) can do a kind of beta-reduction. But in λProlog there is a rule AUGMENT and a rule GENERIC, not covered by beta-reduction. This enhances the underlying logic:

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

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

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

A typical example for the AUGMENT rule is hypothetical reasoning. This answers "what-if" questions. Some deductive databases, even implemented on top of ordinary Prolog can do that as well. Here a simple example:

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

take(hans, french).

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

The above rules express when somebody can grade. And we have also some information about "hans". We can now ask hypothetical questions directly in the top-level, without modifying the fact database.

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

我想人们也可以为更高阶的统一提出理由.λProlog 书中包含了一些更高层次的统一示例，这些示例可能也不适用于 HiLog.

I guess one could also make a case for higher order unification. The λProlog book contains some higher oder unification examples, that probably also don't work in HiLog.

另见:

λProlog 概述
米勒&纳达瑟 - 1988
https://www.researchgate.net/publication/220986335

假设推理的逻辑
邦纳 - 1988
http://citeseer.ist.psu.edu/viewdoc/摘要?doi=10.1.1.56.1451

这篇关于λProlog 中的高阶语义给了你什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！