프롤로그 : var, nonvar 및 ground의 차이

Question

Prolog에서, 특히 메타 프로그래밍 측면에서 사람들은 종종 지상 및 비 지상 변수에 대해 이야기 합니다. 또한 var / 1 , nonvar / 1 및 ground / 1 과 같은 술어를 사용 합니다. 그러나 그들 사이의 차이점은 정확히 무엇입니까?

내 현재 이해는 다음과 같습니다.

• var에 완전히는 uninstantiated (예. X)
• nonvar는 인스턴스화하지만, 더 깊은까지 변수를 포함 할 수 있습니다 (예. 용어 (1, 2, Y)). 이것은 Haskell의 약한 머리 정상 형태와 유사합니다.
• 지상 var에 완전히 인스턴스화, 모든 방법을 아래로 (예. 용어 (1,2,3)).

이 올바른지?

Answer 1

거의.

• 경우 var(X)다음 변수 X는 uninstantiated되는 무언가에 "구멍"을 지정합니다. 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).