Prólogo: diferencia entre var, nonvar y suelo
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
Por poco.
Si
var(X)
entonces la variableX
designa algo que no está instanciado, un "agujero".X
es una "variable fresca". Nota: ese predicado realmente debería llamarsefresh(...)
. SiX
es 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 devar(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 ennonvar(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).