Блог

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

Мое текущее понимание заключается в следующем:

• Var полностью деинсталлируется (например. X)
• Создается экземпляр nonvar, но он может содержать некоторые переменные глубже (например, term(1,2,Y)). Это похоже на слабую головную нормальную форму из Haskell.
• Экземпляр основного var создается полностью, вплоть до самого низа (например, term(1,2,3)).

Правильно ли это?

Почти.

• Если 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).