Đầu tiên là một vấn đề nhỏ: định nghĩa chung của plus/3 có đối số đầu tiên và thứ hai trao đổi cho phép khai thác lập chỉ mục đối số đầu tiên. Xem Chương trình 3.3 của Nghệ thuật Prolog. Điều đó cũng sẽ được thay đổi trong số previous post của bạn. Tôi sẽ gọi định nghĩa được trao đổi của bạn plusp/3 và định nghĩa được tối ưu hóa của bạn pluspo/3. Như vậy, do
plusp(X, 0, X) :- natural_number(X).
plusp(X, s(Y), s(Z)) :- plusp(X, Y, Z).
Phát hiện cắt giảm đỏ (câu hỏi một)
Làm thế nào để chứng minh hoặc bác bỏ/cắt xanh đỏ? Trước hết, hãy xem cho "viết" -unifications trong bảo vệ. Đó là, cho bất kỳ sự thống nhất như vậy trước khi cắt. Trong chương trình tối ưu hóa của bạn:
pluspo(X, Y, X) :- (Y == 0 -> ! ; Y = 0), (X == 0 -> ! ; true), ...
Tôi nhận ra điều sau đây:
pluspo(X, Y, X) :- (...... ->! ; ...), ...
Vì vậy, chúng ta hãy xây dựng một phản ví dụ : Để thực hiện việc cắt giảm này theo cách thức màu đỏ, "viết thống nhất" phải thực hiện bảo vệ thực tế của nó Y == 0 đúng sự thật. Điều đó có nghĩa là mục tiêu xây dựng phải chứa hằng số 0 bằng cách nào đó. Chỉ có hai khả năng để xem xét. Đối số đầu tiên hoặc thứ ba. Một số không trong đối số cuối cùng có nghĩa là chúng ta có tối đa một giải pháp, do đó không có khả năng cắt bỏ các giải pháp tiếp theo. Vì vậy, số 0 phải nằm trong đối số đầu tiên! (Đối số thứ hai không được là 0 ngay từ đầu hoặc "viết hợp nhất sẽ không có ảnh hưởng bất lợi.).Dưới đây là một phản ví dụ như:
?- pluspo(0, Y, Y).
mang đến cho một giải pháp đúng Y = 0, nhưng giấu tất cả những người khác! Vì vậy, ở đây chúng tôi có một cắt đỏ ác! Và ngược lại nó vào chương trình được tối ưu hóa trong đó đã vô cùng nhiều giải pháp:
Y = 0 ;
Y = s(0) ;
Y = s(s(0)) ;
Y = s(s(s(0))) ;
...
Vì vậy, chương trình của bạn không đầy đủ, và thắc mắc về tiếp tục tối ưu hóa nó là như vậy, không có liên quan. Nhưng chúng ta có thể làm tốt hơn, hãy để tôi trình bày lại các định nghĩa thực tế chúng tôi muốn tối ưu hóa:
plus(0, X, X) :- natural_number(X).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).
Trong thực tế tất cả các hệ thống Prolog, có đầu tiên đối số chỉ mục, mà làm cho quyết tâm truy vấn sau đây:
?- plus(s(0),0,X).
X = s(0).
Nhưng nhiều hệ thống không hỗ trợ (đầy đủ) lập chỉ mục đối số thứ ba. Vì vậy chúng tôi có được trong SWI, YAP, SICStus:
?- plus(X, Y, 0).
X = Y, Y = 0 ;
false.
Những gì bạn có thể muốn viết là:
pluso(X, Y, Z) :-
% Part one: green cuts
( X == 0 -> ! % first-argument indexing
; Z == 0 -> ! % 3rd-argument indexing, e.g. Jekejeke, ECLiPSe
; true
),
% Part two: the original unifications
X = 0,
Y = Z,
natural_number(Z).
pluso(s(X), Y, s(Z)) :- pluso(X, Y, Z).
Lưu ý sự khác biệt để pluspo/3: Hiện nay chỉ kiểm tra trước khi cắt! Tất cả các hợp nhất là sau đó.
?- pluso(X, Y, 0).
X = Y, Y = 0.
Tối ưu hóa cho đến nay chỉ dựa vào việc điều tra thủ trưởng của hai điều khoản. Họ không tính đến quy tắc đệ quy. Như vậy, chúng có thể được tích hợp vào trình biên dịch Prolog mà không cần phân tích toàn cầu. Trong thuật ngữ của O'Keefe, những vết cắt màu xanh lá cây này có thể được coi là vết cắt màu xanh. Để trích dẫn The Craft of Prolog, 3.12:
xanh cắt giảm đang có để cảnh báo cho hệ thống Prolog để một determinacy nó nên đã nhận thấy nhưng sẽ không được. Cắt màu xanh không làm thay đổi hành vi hiển thị của chương trình: tất cả những gì họ làm là làm cho nó khả thi.
Màu xanh lá cây cắt giảm để tránh những bằng chứng cố gắng thành công hoặc không liên quan hoặc bị ràng buộc thất bại, nhưng bạn sẽ không mong đợi hệ thống Prolog có thể nói điều đó.
Tuy nhiên, điểm chính là các vết cắt này cần một số nhân viên bảo vệ để hoạt động bình thường.
Bây giờ, bạn coi một truy vấn:
?- pluso(X, s(s(0)), s(s(s(0)))).
X = s(0) ;
false.
hoặc để đặt một trường hợp đơn giản:
?- pluso(X, s(0), s(0)).
X = 0 ;
false.
Ở đây, cả hai người đứng đầu áp dụng, do đó hệ thống là không thể xác định định mệnh. Tuy nhiên, chúng tôi biết rằng không có giải pháp cho mục tiêu plus(X, s^n, s^m) với n>m. Vì vậy, bằng cách xem xét mô hình của plus/3, chúng tôi có thể tránh xa các điểm lựa chọn.Tôi sẽ quay lại ngay sau giờ nghỉ này:
Sử dụng tốt hơn call_semidet/1!
Ngày càng phức tạp và rất có thể là việc tối ưu hóa có thể dễ dàng giới thiệu các lỗi mới trong chương trình. Các chương trình tối ưu hóa cũng là một cơn ác mộng để duy trì. Đối với mục đích lập trình thực tế sử dụng thay vì call_semidet/1. Nó là an toàn, và sẽ tạo ra một lỗi sạch sẽ giả định của bạn hóa ra là sai.
Quay lại doanh nghiệp: Đây là một tối ưu hóa khác. Nếu Y và Z là giống hệt nhau, mệnh đề thứ hai không thể áp dụng:
pluso2(X, Y, Z) :-
% Part one: green cuts
( X == 0 -> ! % first-argument indexing
; Z == 0 -> ! % 3rd-argument indexing, e.g. Jekejeke, ECLiPSe
; Y == Z, ground(Z) -> !
; true
),
% Part two: the original unifications
X = 0,
Y = Z,
natural_number(Z).
pluso2(s(X), Y, s(Z)) :- pluso2(X, Y, Z).
tôi (hiện tại) tin rằng pluso2/3 là việc sử dụng tối ưu các vết cắt màu xanh lá cây/xanh w.r.t. điểm còn dư. Bạn đã yêu cầu một bằng chứng. Vâng, tôi nghĩ rằng đó là vượt quá một câu trả lời SO ...
Mục tiêu ground(Z) là cần thiết để đảm bảo các thuộc tính không chấm dứt. Mục tiêu plus(s(_), Z, Z) không chấm dứt, thuộc tính đó được giữ nguyên bởi ground(Z). Có lẽ bạn nghĩ rằng nó là một ý tưởng tốt để loại bỏ các chi nhánh thất bại vô hạn quá? Theo kinh nghiệm của tôi, điều này khá là vấn đề. Đặc biệt, nếu những nhánh đó được xóa tự động. Trong khi ở cái nhìn đầu tiên nó có vẻ là một ý tưởng tốt, nó làm cho chương trình phát triển giòn hơn nhiều: Một sự thay đổi chương trình lành tính khác bây giờ có thể vô hiệu hóa tối ưu hóa và do đó "gây ra" không chấm dứt. Nhưng dù sao, ở đây chúng tôi đi:
Ngoài cắt giảm xanh đơn giản
pluso3(X, Y, Z) :-
% Part one: green cuts
( X == 0 -> ! % first-argument indexing
; Z == 0 -> ! % 3rd-argument indexing, e.g. Jekejeke, ECLiPSe
; Y == Z -> !
; var(Z), nonvar(Y), \+ unify_with_occurs_check(Z, Y) -> !, fail
; var(Z), nonvar(X), \+ unify_with_occurs_check(Z, X) -> !, fail
; true
),
% Part two: the original unifications
X = 0,
Y = Z,
natural_number(Z).
pluso3(s(X), Y, s(Z)) :- pluso3(X, Y, Z).
Bạn có thể tìm thấy một trường hợp pluso3/3 không chấm dứt trong khi có nhiều câu trả lời hữu hạn?
mệnh đề đầu tiên của 'plus/3' lần đọc' (Y == 0 ->!; Y = 0) 'mà không có ý nghĩa nhiều, vì' Y' là một biến mới. – gusbro
@gusbro: cảm ơn bạn đã báo cáo lỗi. –