Prolog: difference between var, nonvar and ground

Question

In Prolog, especially in it's metaprogramming aspects, people often talk about ground and non-ground variables. As well as using predicates such as var/1, nonvar/1 and ground/1. But what exactly is the distincion between them?

My current understanding is the following:

A var is completely uninstantiated (eg. X)
A nonvar is instantiated, but might contain some variables deeper down (eg. term(1,2,Y)). This is similar to a weak head normal form from Haskell.
A ground var is completely instantiated, all the way down (eg. term(1,2,3)).

Is this correct?

Yes, your intuition is correct. Just be aware that e.g. X = a, ground(X) succeeds but ground(X), X = a fails. In other words, the metalogical predicates give you information about the instantiation status of the term in the current derivation (under the current answer substitution), not the syntactic structure of its argument. — lambda.xy.x

David Tonhofer David Tonhofer · Accepted Answer · 2020-08-17T18:22:41

Nearly.

If var(X) then variable X designates something that is uninstantiated, a "hole". X is a "fresh variable". Note: That predicate should really be named fresh(...). Whether X is a variable is actually a question about the program text. But what we want to know is whether what is in between the parentheses is a fresh variable (at the moment that call is made, because, quite non-logically, that can change.)
nonvar(X) is just the complement of var(X), same as \+ var(X). Whatever is between the parentheses designates something (if it is a variable) or is something (if it is a non-variable term, as in nonvar(foo)) that is not a "hole".
ground(X) means that whatever is between the parenthese designates something or is something that has no holes in its structure (in effect, no holes at the term's leaves).

Some test code. I expected the compiler to issue more warnings than it did.

:- begin_tests(var_nonvar).

% Amazingly, the compiler does not warn about the code below.

test("var(duh) is always false", fail) :-
  var(duh). 

% Amazingly, the compiler does not warn about the code below.

test("var(X) is true if X is a fresh variable (X designates a 'hole')") :-
   var(_). 

% Compiler warning: " Singleton variable, Test is always true: var(X)"

test("var(X) is true if X is a fresh variable (X designates a 'hole')") :-
   var(X). 
   
% The hole designated by X is filled with f(_), which has its own hole.
% the result is nonvar (and also nonground)

test("var(X) maybe true but become false as computation progresses") :-
   var(X),X=f(_),nonvar(X).
   
test("var(X) is false otherwise") :-
   var(_).   

% The hole is designated by an anonymous variable

test("a fresh variable is not ground, it designates a 'hole'", fail) :-
   ground(_). 
   
% Both hhe holes are designated by anonymous variables

test("a structure with 'holes' at the leaves is non-ground", fail) :-
   ground(f(_,_)). 
   
test("a structure with no 'holes' is ground") :-
   ground(f(x,y)).

test("a structure with no 'holes' is ground, take 2") :-
   X=f(x,y), ground(X).
   
% var/1 or ground/1 are questions about the state of computation,
% not about any problem in logic that one models. For example:

test("a structure that is non-ground can be filled as computation progresses") :-
   K=f(X,Y), \+ ground(f(X,Y)), X=x, Y=y, ground(f(X,Y)).
   
:- end_tests(var_nonvar).

Prolog: difference between var, nonvar and ground

1 Answers