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?

Answer 1

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