Prologue : différence entre var, nonvar et sol

Aug 18 2020

En Prolog, en particulier dans ses aspects de métaprogrammation, les gens parlent souvent de variables sol et non sol . En plus d'utiliser des prédicats tels que var/1 , nonvar/1 et ground/1 . Mais quelle est exactement la distinction entre eux?

Ma compréhension actuelle est la suivante :

  • Un var est complètement non instancié (par exemple, X)
  • Un nonvar est instancié, mais peut contenir des variables plus bas (par exemple, term(1,2,Y)). Ceci est similaire à une forme normale de tête faible de Haskell.
  • Une variable de base est complètement instanciée, jusqu'au bout (par exemple, term(1,2,3)).

Est-ce correct?

Réponses

DavidTonhofer Aug 18 2020 at 01:22

Presque.

  • Si var(X)alors la variable Xdésigne quelque chose qui n'est pas instancié, un "trou". Xest une "variable fraîche". Remarque : Ce prédicat devrait vraiment être nommé fresh(...). Si Xest une variable est en fait une question sur le texte du programme. Mais ce que nous voulons savoir, c'est si ce qui se trouve entre les parenthèses est une nouvelle variable (au moment où cet appel est effectué, car, de manière tout à fait non logique, cela peut changer.)

  • nonvar(X)est juste le complément de var(X), identique à \+ var(X). Tout ce qui est entre parenthèses désigne quelque chose (s'il s'agit d'une variable) ou est quelque chose (s'il s'agit d'un terme non variable, comme dans nonvar(foo)) qui n'est pas un "trou".

  • ground(X)signifie que tout ce qui est entre parenthèses désigne quelque chose ou est quelque chose qui n'a pas de trous dans sa structure (en effet, pas de trous aux feuilles du terme).

Un code de test. Je m'attendais à ce que le compilateur émette plus d'avertissements qu'il ne l'a fait.

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