Пролог: разница между var, nonvar и ground

Question

В Prolog, особенно в аспектах метапрограммирования, люди часто говорят о наземных и неосновных переменных. А также использование таких предикатов, как var / 1 , nonvar / 1 и ground / 1 . Но в чем именно между ними разница?

Мое текущее понимание таково:

• Вар полностью uninstantiated (например, X)
• Nonvar конкретизируется, но может содержать некоторые переменные глубже (например, член (1,2, Y)). Это похоже на нормальную форму со слабой головой из Haskell.
• Земля вар полностью инстанцирован, весь путь вниз (например, термин (1,2,3)).

Это правильно?

Answer 1

Около.

• Если var(X)тогда переменная Xобозначает что-то необоснованное, то есть «дыру». Xэто «свежая переменная». Примечание: этот предикат действительно должен быть назван fresh(...). Вопрос в том, Xявляется ли переменная переменной, на самом деле, в тексте программы. Но мы хотим знать, является ли то, что находится между круглыми скобками, новой переменной (в момент выполнения этого вызова, потому что, совершенно нелогично, это может измениться).

• nonvar(X)это просто дополнение var(X), то же самое, что и \+ var(X). Что бы ни было между скобками обозначает что - то (если это переменная) или это что - то (если он не является переменной термин, как и в nonvar(foo)) , что не является «дыра».

• ground(X) означает, что все, что находится в круглых скобках, обозначает что-то или является чем-то, что не имеет дыр в своей структуре (фактически, нет дыр в листьях термина).

Какой-то тестовый код. Я ожидал, что компилятор выдаст больше предупреждений, чем он сделал.

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