プロローグ:var、nonvar、groundの違い

Aug 18 2020

プロローグでは、特にそれのメタプログラミングの面では、人々はしばしばについて話地面非地面変数。var / 1nonvar / 1ground / 1などの述語を使用するだけでなく。しかし、それらの間の違いは正確には何ですか?

私の現在の理解は次のとおりです。

  • varが完全にインスタンス生成される(例えばX)
  • nonvarがインスタンス化されていますが、より深いダウン、いくつかの変数が含まれている場合があります(例:用語(1,2、Y))。これは、Haskellの弱い頭の通常のフォームに似ています。
  • グランドvarが完全にインスタンス化され、すべての方法ダウン(例えば用語(1,2,3))。

これは正しいです?

回答

DavidTonhofer Aug 18 2020 at 01:22

ほぼ。

  • var(X)then変数がインスタンス化Xされていないもの、つまり「穴」を指定している場合。X「新鮮な変数」です。注:その述語は実際にはfresh(...)。という名前にする必要があります。X変数であるかどうかは、実際にはプログラムテキストに関する質問です。しかし、私たちが知りたいのは、括弧の間にあるものが新しい変数であるかどうかです(呼び出しが行われた時点で、それは非常に非論理的に変更される可能性があるためです)。

  • nonvar(X)の補数でありvar(X)、と同じ\+ var(X)です。括弧の間にあるものは何でも何かを指示する(それが変数の場合)、またはある何か(それはのように、非可変用語である場合にはnonvar(foo)「穴」ではありません)。

  • ground(X) 括弧の間にあるものは何かを示しているか、その構造に穴がない(事実上、用語の葉に穴がない)ことを意味します。

いくつかのテストコード。コンパイラーがそれよりも多くの警告を出すことを期待していました。

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