在 SWI-prolog 中定义包括竖线 (|) 的运算符

Defining operators including vertical bars(|) in SWI-prolog

我正在尝试在 Prolog 中对基本逻辑推理进行编码,我想定义一些自定义运算符来简化符号。如果我可以为 ⊢ 输入 |- 会很方便。所以我尝试了

:- op(1150, xfy, [ '|-' ]).
gamma |- a.
Gamma |- or(A,_) :- Gamma |- A.
Gamma |- or(_,A) :- Gamma |- A.

但是当我尝试查询 gamma |- or(a,X) 时,我收到错误消息

ERROR: '<meta-call>'/1: Undefined procedure: gamma/0

而不是我期望的 true

问题似乎是定义的运算符包含竖线字符。如果我修改知识库为

:- op(1150, xfy, [ imp ]).
gamma imp a.
Gamma imp or(A,_) :- Gamma imp A.
Gamma imp or(_,A) :- Gamma imp A.

然后 Prolog 可以毫无问题地回答查询 gamma imp or(a,X)。竖线是我不允许在定义中使用的保留字符吗?或者有什么办法可以解决这个问题?

管道'|' symbol 具有特殊的作用,如 "syntactic sugar" 来表示列表。 为了使用 [a | [b, c]] 而不是 .(a, .(b, .(c, [])。prolog 解析器在解析表达式的其他部分之前对其进行不同的处理。

您仍然可以定义一个谓词 '|-',然后将其声明为运算符,但您必须在像 a '|-' b 这样的引号中使用它,这有点违背了目的。

你不能这样做。既不在 ISO Prolog 中也不在 SWI 中。虽然竖线用作运算符 - 如果存在相应的运算符声明,则不能将其用作长度为两个或更多字符的运算符的一部分。在你的情况下你能得到的最好的方法是声明一个运算符 |- 并以引用的形式使用它。在以下两种情况下,引号都是必需的。

:- op(1200, xfx, '|-').  

a '|-' b.

看起来不太吸引人。作为一个单独的字符,竖线用作中缀运算符。

?- ( a | b ) = '|'(a, b).
true.

?- current_op(Pri,Fix,'|').
Pri = 1105,
Fix = xfy.

| 还有另一种用法作为列表中的头尾分隔符。由于中缀栏可以采用的优先级的限制,[A|As] 和以上用法之间没有歧义。

请注意 [a|-]. 是有效的 Prolog 文本。如果有运算符声明,甚至 gamma |- a. 在 SWI 中也是有效的,甚至在 ISO 中也是有效的 Prolog 文本!

?- write_canonical((gamma|-a)).
'|'(gamma,-(a))

SWI-Prolog 支持 Unicode

也许,只是也许,你可以使用符号本身?使用 u22A2,我可以输入以下源文件:

:-op(1150, xfy, ⊢).
gamma ⊢ a.
Gamma ⊢ or(A,_) :- Gamma ⊢ A.
Gamma ⊢ or(_,A) :- Gamma ⊢ A.

而且我可以毫无问题地加载和查询它:

?- gamma ⊢ or(a,X).
true ;
X = a ;
X = or(a, _2484) . % and so on

我知道这不是你要问的,我也知道这只有在你能找到一种简单的方法在你的文本编辑器和顶层输入这些字符时才有用。

在ISO core Prolog中竖线属于类别 独奏角色。特别是 ISO 的第 6.5.3 节 核心标准定义了独奏角色。名单之中 独奏字符我们找到所谓的头尾分隔符 char:

solo char (* 6.5.3 *)
    = cut char
    ...
    | head tail separator char
    ... ;

cut char = "!" ;
...
head tail separator char = "|"
...

Prolog 的扫描器处理单独的字符,这样 它们被认为是独立的代币。

表示他们不加入其他角色。因此,如果 有人写|-,就好像这两个字符一样 分开,有人写道 | - 在 Prolog 文本中。

因此|不能与其他字符组合 然后定义为运算符。 Prolog系统只会 无法将其视为组合符号,例如 |-.

另一件事是所谓的引用原子,当然可以 使用'|-',即将字符括在引号中,并且 然后 Prolog 扫描器会将它们识别为一个完整的原子。