Prolog: differenza tra var, nonvar e ground
In Prolog, specialmente nei suoi aspetti di metaprogrammazione, le persone parlano spesso di variabili ground e non ground . Oltre a utilizzare predicati come var/1 , nonvar/1 e ground/1 . Ma qual è esattamente la distinzione tra loro?
La mia comprensione attuale è la seguente:
- Una var è completamente non istanziata (es. X)
- Un nonvar viene istanziato, ma potrebbe contenere alcune variabili più in basso (ad es. term(1,2,Y)). Questo è simile a una forma normale con testa debole di Haskell.
- Un ground var è completamente istanziato, fino in fondo (es. term(1,2,3)).
È corretto?
Risposte
Quasi.
If
var(X)
allora variabileX
designa qualcosa che non è istanziato, un "buco".X
è una "variabile fresca". Nota: quel predicato dovrebbe davvero essere chiamatofresh(...)
. SeX
è una variabile è in realtà una domanda sul testo del programma. Ma quello che vogliamo sapere è se ciò che è tra le parentesi è una nuova variabile (nel momento in cui viene effettuata la chiamata, perché, in modo del tutto non logico, può cambiare).nonvar(X)
è solo il complemento divar(X)
, uguale a\+ var(X)
. Qualunque cosa sia tra le parentesi designa qualcosa (se è una variabile) o è qualcosa (se è un termine non variabile, come innonvar(foo)
) che non è un "buco".ground(X)
significa che qualunque cosa sia tra parentesi designa qualcosa o è qualcosa che non ha buchi nella sua struttura (in effetti, nessun buco alle foglie del termine).
Qualche codice di prova. Mi aspettavo che il compilatore emettesse più avvisi di quanti ne avesse.
:- 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).