Definition of operators, including vertical bars (|) in the SWI prolog

Question

I am trying to code the basic logic in Prolog, and I want to define some user-defined operators for ordering notation. It would be convenient if I could type |- for ⊢. So I tried

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

but when I try to execute the gamma |- or(a,X) request, I get an error

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

instead of true I expect.

The problem is that a certain operator contains a vertical bar symbol. If I change 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 responding to a gamma imp or(a,X) request. Is a vertical bar a reserved character that I am not allowed to use in definitions? Or is there some way around this?

Answer 1

You cannot do this. Neither in ISO Prolog, nor in SWI. While the vertical bar serves as the operator; if an appropriate operator declaration is present, it cannot be used without quotation marks as part of an operator with two or more characters. The best you can get in your situation is to declare the |- operator and use it in quotation marks. In both cases below, quotes are strictly necessary.

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

Doesn't look too attractive. One, like one character, bar serves as an infix operator.

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

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

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

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

Answer 2

SWI-Prolog supports Unicode

Maybe, maybe you can use the character itself? Using u22A2, I can enter the following source file:

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

And I can download it without a problem and request it:

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

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

Answer 3

Trumpet '|' the symbol represents the special role of “syntactic sugar” for representing lists. To use [a | [b, c]] instead. (a ,. (b ,. (c, []). The prolog parser treats it differently before it resolves other parts of the expression.

You can still define the predicate '|-' and then declare it as an operator, but you will have to use it in quotation marks, such as a '|-' b , which cannot defeat the target.

Answer 4

In the Prolog ISO prolog, the vertical bar refers to the category of solo characters. In particular, ISO clause 6.5.3, the main standard defines solo characters. Among the solo characters, we find the so-called tail tail separator char:

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

The Prolog scanner examines solo characters, so they are considered presumptuous tokens.

means that they do not join other characters. So if someone writes | -, this is the same as the two characters were separated, and someone writes | - in the text of the Prologue.

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

Another thing is the so-called quoted atoms, of course you can use '| - ', enclose the characters in quotation marks and the Prolog Scanner then recognizes them as one solid atom.