Prolog: var, nonvar ve zemin arasındaki fark

Question

Prolog'da, özellikle metaprogramlama yönlerinde, insanlar genellikle temel ve temel olmayan değişkenlerden bahseder . Var / 1 , nonvar / 1 ve zemin / 1 gibi yüklemleri kullanmanın yanı sıra . Ama aralarındaki fark tam olarak nedir?

Şu anki anlayışım şu:

• Bir var tamamen doğrulanmamış (ör. X)
• Bir nonvar somutlaştırılır, ancak daha derinlerde bazı değişkenler içerebilir (ör. Terim (1,2, Y)). Bu, Haskell'den gelen zayıf kafa normal şekline benzer.
• Bir zemin varyantı tamamen somutlaştırılır (ör. Terim (1,2,3)).

Bu doğru mu?

Answer 1

Neredeyse.

• Eğer var(X)o zaman değişken Xuninstantiated bir şeyi, bir "delik" belirtir. X"taze bir değişken" dir. Not: Bu yüklem gerçekten adlandırılmalıdır fresh(...). XDeğişken olup olmadığı aslında program metni ile ilgili bir sorudur. Ancak bilmek istediğimiz şey, parantezler arasında bulunan şeyin yeni bir değişken olup olmadığıdır (arama yapıldığı anda, çünkü mantıksız bir şekilde bu değişebilir.)

• nonvar(X)sadece tamamlayıcısıdır var(X), aynı \+ var(X). (Bu değişken ise) veya parantez atar şey arasında ne olursa olsun olduğu (o olduğu gibi, olmayan bir değişken vadeli ise bir şey nonvar(foo)) bir "delik" olmadığını söyledi.

• ground(X) parantezler arasında ne varsa, bir şeyi belirtir veya yapısında delik olmayan bir şeydir (aslında, terimin yapraklarında delik yoktur).

Bazı test kodları. Derleyicinin ondan daha fazla uyarı vermesini bekliyordum.

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