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

7
votes

I am trying to encode basic logical inferences in Prolog, and I want to define some custom operators to streamline the notation. It would be handy if I can type |- for ⊢. So I tried

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

but when I try the query gamma |- or(a,X), I get the error message

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

instead of the true I expect.

The problem seems to be that the defined operator includes a vertical bar character. If I modify the knowledge base to

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

Then Prolog has no problems answering the query gamma imp or(a,X). Is the vertical bar a reserved character that I'm not allowed to use in definitions? Or is there some way around this?

4
prologoperatorsswi-prolog
This has nothing to do with the question, however: trying to emulate the look of a mathematical operator like this is a lost battle. You either have all the symbols, APL style, or just use the names. I would almost suggest using the TeX math mode symbols and the amsmath names; at least you have a precedent for almost any operator you can come up with. – user1812457

4 Answers

7
votes

SWI-Prolog supports Unicode

Maybe, just maybe, you can use the symbol itself? Using u22A2, I can type in the following source file:

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

And I can, without any problem, load it and query it:

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

I realize this is not what you are asking, and I also realize that this is only useful if you can find an easy way to enter these characters in your text editor and the top level.

3
votes

You cannot do this. Neither in ISO Prolog nor in SWI. While the vertical bar serves as an operator — provided a corresponding operator declaration is present, it cannot be used unquoted as part of an operator with a length of two or more characters. The best you can get in your situation is to declare an operator |- and use it in quoted form. In both cases below, quotes are strictly needed.

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

a '|-' b.

Doesn't look too attractive. Alone, as a single character, the bar serves as an infix operator.

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

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

There is another use of | as a head-tail separator in lists. Due to the restrictions to the priority the infix bar can take, there is no ambiguity between [A|As] and above use.

Note that [a|-]. is valid Prolog text. Even gamma |- a. is valid in SWI and even valid Prolog text in ISO, provided there is an operator declaration!

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

The pipe '|' symbol has a special role as "syntactic sugar" to represent lists. In order to use [a | [b, c]] instead of .(a, .(b, .(c, []). The prolog parser treats it differently before it resolves other parts of the expression.

You can still define a predicate '|-' and then declare it as an operator, but you would have to use it in quotes like a '|-' b which kinda defeats the purpose.

1
votes

In ISO core Prolog the vertical bar belongs to the category of solo characters. In particular section 6.5.3 of the ISO core standard defines the solo characters. Among the list of solo characters we find the so called head tail separator char:

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

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

The scanner of Prolog treats solo characters such that they are considered selfstanding tokens.

Means they don't join with other characters. So if somebody writes |-, its the same as if the two characters were separated and somebody writes | - in a Prolog text.

As a result the | cannot be combined with other characters and then defined as an operator. The Prolog system will just not be able to see it as the combined symbol, for example |-.

Another matter are so called quoted atoms, one can of course use '|-', i.e enclose the characters in quotes, and the Prolog scanner will then recognize them as a one whole atom.