Prolog: ความแตกต่างระหว่าง var, nonvar และ ground

Question

ใน Prolog โดยเฉพาะอย่างยิ่งในด้าน metaprogramming ผู้คนมักพูดถึงตัวแปรกราวด์และไม่ใช่กราวด์ รวมทั้งการใช้ภาคเช่นvar / 1 , nonvar / 1และพื้นดิน / 1 แต่อะไรคือความแตกต่างระหว่างพวกเขา?

ความเข้าใจปัจจุบันของฉันมีดังต่อไปนี้:

• varเป็น uninstantiated สมบูรณ์ (เช่น. X)
• nonvarถูกสร้าง แต่อาจจะมีตัวแปรบางลึกลง (เช่นระยะ. (1,2, Y)) คล้ายกับหัวที่อ่อนแอจาก Haskell
• var พื้นดินถูกสร้างอย่างสมบูรณ์ทุกทางลง (เช่น. ระยะ (1,2,3))

ถูกต้องหรือไม่?

Answer 1

เกือบ

• หากvar(X)ตัวแปรนั้น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).