Does Prolog have an "if and only if" operator?

Question

I would normally write such a statement as two clauses, like this:

x :- y.
y :- x.

In Prolog, is there any concise way to write a statement like "if x then y, and vice-versa"?

In other words, is it possible to write "x if and only if y" as a single statement?

Answer 1

You said you would normally write "p if and only if q" (I will write q <=> q in the following) as

p :- q.
q :- p.

but that is only correct if

1. there are no other clauses for p and q
2. there are no variables involved

And under those circumstances, the code doesn't really say anything interesting, only that p and q are equivalent, but whether they are true or false is not stated.

If variables are involved, say

p(X) :- q(X).
q(X) :- p(X).

then the meaning is

forall X: p(X) <= q(X)  and  forall X': q(X') <= p(X')

which is the same as

forall X,X':  p(X) <= q(X)  and  q(X') <= p(X')

when what you actually wanted to say was

forall X:  p(X) <= q(X)  and  q(X) <= p(X)

---

On the other hand, as long as you have only a single clause for a predicate, then that clause alone can be read as an "if and only if". For example

p(X,Y) :- q(X,Z).

means

forall X,Y  exists Z:  p(X,Y) <=> q(X,Z)

and if q/2 is defined elsewhere, then this is a sensible thing to write. That way you can define aliases, projections, etc.

---

You haven't given any background to your question, but once you consider variables, it makes sense to ask "under which circumstances is p <=> q ?", where p and q defined arbitrarily. Then you would like to write something like

p_iff_q(X) :- p(X) <=> q(X).

which, in plain Prolog, you'd have to rewrite into something like

p_iff_q(X) :- p(X),q(X) ; \+p(X),\+q(X).

Answer 2

As far as I know not in swi-prolog.

On the other hand, you can write a small rewrite-predicate to automatically rewrite your program theory using the following small program:

:- dynamic([system:term_expansion/2]).

:- op(900, xfx, user:(:::)).

system:term_expansion(:::(H,T),[H :- T, T :- H]) :-
    callable(H),
    callable(T).

Then you can simply use

x ::: y.

Of course you can assign another operator than :::, you simply replace the operator definition (op/3) and term_expansion/2 accordingly.

---

On the other hand, only when the the head and body are resolved before you call this, this won't yield to an infinite loop. Otherwise, the transformed program will loop infinitely. Prolog is not a real logic engine, it's merely logic programming: specifying a program in a logical syntax, not expressing a logical theory.