Prólogo: diferencia entre var, nonvar y suelo

Aug 18 2020

En Prolog, especialmente en sus aspectos de metaprogramación, la gente suele hablar de variables terrestres y no terrestres . Además de usar predicados como var/1 , nonvar/1 y ground/1 . Pero, ¿cuál es exactamente la distinción entre ellos?

Mi comprensión actual es la siguiente:

  • Una var está completamente sin instanciar (por ejemplo, X)
  • Se crea una instancia de nonvar , pero puede contener algunas variables más abajo (p. ej., term(1,2,Y)). Esto es similar a una forma normal de cabeza débil de Haskell.
  • Una var de tierra está completamente instanciada, hasta el final (por ejemplo, término (1,2,3)).

¿Es esto correcto?

Respuestas

DavidTonhofer Aug 18 2020 at 01:22

Por poco.

  • Si var(X)entonces la variable Xdesigna algo que no está instanciado, un "agujero". Xes una "variable fresca". Nota: ese predicado realmente debería llamarse fresh(...). Si Xes una variable es en realidad una pregunta sobre el texto del programa. Pero lo que queremos saber es si lo que está entre paréntesis es una variable nueva (en el momento en que se realiza la llamada, porque, lógicamente, eso puede cambiar).

  • nonvar(X)es simplemente el complemento de var(X), igual que \+ var(X). Lo que esté entre paréntesis designa algo (si es una variable) o es algo (si es un término no variable, como en nonvar(foo)) que no es un "agujero".

  • ground(X)significa que lo que está entre paréntesis designa algo o es algo que no tiene agujeros en su estructura (en efecto, no hay agujeros en las hojas del término).

Algo de código de prueba. Esperaba que el compilador emitiera más advertencias de las que emitió.

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