Prolog: diferença entre var, nonvar e ground

Question

No Prolog, especialmente em seus aspectos de metaprogramação, as pessoas costumam falar sobre variáveis ​​de solo e não-terra . Além de usar predicados como var/1 , nonvar/1 e ground/1 . Mas qual é exatamente a distinção entre eles?

Meu entendimento atual é o seguinte:

• Uma var é completamente não instanciada (por exemplo, X)
• Um nonvar é instanciado, mas pode conter algumas variáveis ​​mais profundas (por exemplo, term(1,2,Y)). Isso é semelhante a uma forma normal de cabeça fraca de Haskell.
• Um ground var é completamente instanciado, todo o caminho (ex. term(1,2,3)).

Isso está correto?

Answer 1

Por pouco.

• Se var(X)então variável Xdesigna algo que não é instanciado, um "buraco". Xé uma "variável nova". Nota: Esse predicado deve realmente ser nomeado fresh(...). Se Xé uma variável é, na verdade, uma questão sobre o texto do programa. Mas o que queremos saber é se o que está entre os parênteses é uma nova variável (no momento em que a chamada é feita, porque, de forma não lógica, isso pode mudar).

• nonvar(X)é apenas o complemento de var(X), o mesmo que \+ var(X). O que estiver entre parênteses designa algo (se for uma variável) ou é algo (se for um termo não variável, como em nonvar(foo)) que não é um "buraco".

• ground(X)significa que o que quer que esteja entre os parênteses designa algo ou é algo que não tem buracos em sua estrutura (na verdade, nenhum buraco nas folhas do termo).

Algum código de teste. Eu esperava que o compilador emitisse mais avisos do que emitiu.

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