Prolog predicate - vòng lặp vô hạn

Question

Tôi cần tạo một vị từ Prolog cho lũy thừa của 2, với các số tự nhiên. số tự nhiên là: 0, s (0), s (s (0)) ans vv ..

Ví dụ:

?- pow2(s(0),P). 
P = s(s(0)); 
false. 
?- pow2(P,s(s(0))). 
P = s(0); 
false. 

Đây là mã của tôi:

times2(X,Y) :- 
    add(X,X,Y). 

pow2(0,s(0)). 
pow2(s(N),Y) :- 
    pow2(N,Z), 
    times2(Z,Y). 

Và nó hoạt động hoàn hảo với ví dụ đầu tiên, nhưng đi vào một vòng lặp vô hạn trong lần thứ hai ..
Làm thế nào tôi có thể sửa lỗi này?

Answer 1

Điều này vui vẻ vì thứ tự đánh giá của pow2. Nếu bạn chuyển đổi thứ tự của pow2, bạn sẽ có ví dụ đầu tiên bị mắc kẹt trong vòng lặp vô hạn .. Vì vậy, bạn có thể kiểm tra trước nếu Y là var hoặc nonvar.

Giống như vậy:

times2(X,Y) :- 
    add(X,X,Y). 

pow2(0,s(0)). 
pow2(s(N),Y) :- 
    var(Y), 
    pow2(N,Z), 
    times2(Z,Y). 
pow2(s(N),Y) :- 
    nonvar(Y), 
    times2(Z,Y), 
    pow2(N,Z). 

Answer 2

Đây là một phiên bản đó chấm dứt cho số đầu tiên hoặc thứ hai bị ràng buộc:

 
pow2(E,X) :- 
    pow2(E,X,X). 

pow2(0,s(0),s(_)). 
pow2(s(N),Y,s(B)) :- 
    pow2(N,Z,B), 
    add(Z,Z,Y). 

Bạn có thể determine its termination conditions với CTI.

Vì vậy, làm cách nào tôi tìm ra giải pháp đó? Ý tưởng là tìm ra cách thức đối số thứ hai có thể xác định kích thước của đối số đầu tiên. Ý tưởng chủ chốt được rằng đối với tất cả i ∈ N: 2 ⁱ > i.

Vì vậy, tôi đã thêm một đối số nữa để thể hiện quan hệ này. Có lẽ bạn có thể tăng cường thêm một chút?

---

Và đây là lý do tại sao chương trình gốc không chấm dứt. Tôi đưa ra lý do là failure-slice. Xem thẻ để biết thêm chi tiết và các ví dụ khác.

 
?- pow2(P,s(s(0))), false. 

pow2(0,s(0)) :- false. 
pow2(s(N),Y) :- 
    pow2(N,Z), false, 
    times2(Z,Y). 

Đây là mảnh nhỏ bé này là nguồn không chấm dứt! Nhìn vào Z là một biến mới tươi! Để khắc phục sự cố, đoạn này phải được sửa đổi bằng cách nào đó.

---

Và đây là lý do giải pháp @ Keeper không chấm dứt cho pow2(s(0),s(N)).

 
?- pow2(s(0),s(N)), false. 

add(0,Z,Z) :- false. 
add(s(X),Y,s(Z)) :- 
    add(X,Y,Z), false. 

times2(X,Y) :- 
    add(X,X,Y), false. 

pow2(0,s(0)) :- false. 
pow2(s(N),Y) :- false, 
    var(Y), 
    pow2(N,Z), 
    times2(Z,Y). 
pow2(s(N),Y) :- 
    nonvar(Y), 
    times2(Z,Y), false, 
    pow2(N,Z).