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

Question

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?

Tiphany

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. – Cowart

Answer 1

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))

Constringe

Answer 2

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.

Cowart

The biggest annoyance here is that SWI adds extra quotes when writing this operator, so your traces will be just as unreadable as '|-'. An ISO conforming Prolog using Unicode would avoid such quotes. – Constringe

@Constringe Hmm, this hasn't even occurred to me, I guess I don't use the tracer often enough. To me the biggest annoyance is still finding a decent way to type in more than one symbol multiple times. My solution before has been to use a descriptive name; at the end, it is the least hustle. (You can always go wild with the presentation of the source code later, for example pretty-printing like WEB. I still haven't made up my mind whether pretty-printing is ever a good idea.) – Cowart

By traces I did not mean the tracer. But just the traces that proof systems produce. – Constringe

I have opened a new SWI-Prolog issue: github.com/SWI-Prolog/swipl-devel/issues/172 – Alkalize

@Constringe It seems this was an actual bug that has been fixed in the latest development release (7.3.29) – Cowart

@j4nbur53 Thank you very much for reporting it; it has been already fixed! I didn't even realize it is a legitimate error. – Cowart

@Boris: Well, that's the problem with SWI: Since its declaration of non-conformance it has become pointless to report errors. – Constringe

@Constringe That's a bit unnecessarily harsh. Obviously, this was, indeed, an error, and reporting it was not pointless. – Cowart

The issue got fixed, see here github.com/SWI-Prolog/swipl-devel/issues/… – Alkalize

Answer 3

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.

Cashbox

Answer 4

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.

Alkalize