CODEWITHSUNDEEP
prolog
Greg Nisbet
Greg Nisbet

Reputation: 6994

Prolog ... define predicate that checks if both arguments are/point to the same atom

I have a prolog predicate that takes two parameters (both labelled X here since they should be the same) and compares them to see if they evaluate to the same atom. That is the intent. However, the predicate unexpectedly returns false when both arguments are variables.

I'm trying to define a notion of an expression in sentential logic / propositional calculus being in "implication normal form" in Prolog. Implication normal form here meaning that all connectives are replaced with -> and falsum.

As a base case, I want to say that an expression consisting entirely of an atom is already in normal form with itself.

Here's how I'm attempting to express that. I'm repeating a parameter name instead of doing some type of check of sameness between the parameters.

% foo.P
implication_normal(X, X) :- atom(X).

This incomplete-but-still-useful definition is intended to capture the fact that implication_normal(x, x) is true but implication_normal(x, y) is false.

In some ways it seems to work:

$ swipl -s foo.P

?- implication_normal(x, x).
true.

?- implication_normal(x, y).
false.

?- implication_normal(1, 1).
false.

It does the wrong thing with variables (It should be enumerating pairs of "binding contexts" where X and Z happen to point to the same atom).

?- implication_normal(X, Z).
false.

It also just returns false if you give it the same variable twice.

?- implication_normal(X, X).
false.

for some strange reason, the behavior is correct if you give it a variable and a single atom (and you get failure with an integer).

?- implication_normal(X, z).
X = z.

?- implication_normal(X, 1).
false.

and similarly if the variable is second.

?- implication_normal(z, X).
X = z.

?- implication_normal(1, X).
false.

How do I change the definition of implication_normal so that it enumerates in all the cases where variables are supplied?

Upvotes: 1

Views: 1357

Answers (1)

Paulo Moura
Paulo Moura

Reputation: 18663

The standard atom/1 predicate is a type-checking predicate. It doesn't enumerate atoms. It just deterministically checks if its argument is an atom. Moreover, your definition of the implication_normal /2 predicate attempts to unify its two arguments and, if the unification is successful, calls atom/1 with the resulting term. That's why a call such as implication_normal(X, z) succeeds: X is unified with z and atom(z) is true.

Note that some Prolog systems provide a current_atom/1 that does enumerate atoms. On those systems, you could write instead:

implication_normal(X, X) :- current_atom(X).

Some sample calls using SWI-Prolog:

?- implication_normal(X, Z).
X = Z, Z = '' ;
X = Z, Z = abort ;
X = Z, Z = '$aborted'
...

?- implication_normal(X, X).
X = '' ;
X = abort ;
X = '$aborted' ;
...

?- implication_normal(X, z).
X = z.

?- implication_normal(X, 1).
false.

Upvotes: 2

Related Questions