प्रोलॉग भविष्यवाणी - अनंत लूप

Question

मुझे प्राकृतिक संख्याओं के साथ 2 की शक्ति के लिए प्रोलॉग अनुमान बनाने की आवश्यकता है। प्राकृतिक संख्या रहे हैं: 0, एस (0), एस (रों (0)) इतने पर ans ..

उदाहरण के लिए:

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

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

:

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

यह मेरा कोड है और यह पहले उदाहरण के साथ पूरी तरह से काम करता है, लेकिन दूसरे में एक अनंत लूप में प्रवेश करता है ..
मैं इसे कैसे ठीक कर सकता हूं?

Answer 1

यह खुशी करता है क्योंकि pow2 के मूल्यांकन आदेश का। यदि आप पाउ 2 के ऑर्डर को स्विच करते हैं, तो आपके पास अनंत लूप में फंस गया पहला उदाहरण होगा .. तो यदि आप var या nonvar हैं तो आप पहले जांच सकते हैं।

तो जैसा

:

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

यहाँ एक संस्करण है कि पहली या दूसरी बहस के लिए समाप्त हो जाता है बाध्य किया जा रहा है: CTI साथ

determine its termination conditions

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

आप कर सकते हैं।

तो, मैं उस समाधान के साथ कैसे आया? विचार यह था कि दूसरा तर्क कैसे पहला तर्क के आकार को निर्धारित कर सकता है। कुंजी विचार किया जा रहा है कि सभी के लिए मैं ∈ एन: 2 ^मैं > मैं।

इसलिए मैंने इस संबंध को व्यक्त करने के लिए एक और तर्क जोड़ा। शायद आप इसे थोड़ा और मजबूत कर सकते हैं?

---

और यही कारण है कि मूल प्रोग्राम समाप्त नहीं होता है। मैं failure-slice के कारण बताता हूं। अधिक जानकारी और अन्य उदाहरणों के लिए टैग देखें।

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

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

यह छोटा टुकड़ा है जो गैर-समाप्ति के लिए स्रोत है! Z देखें जो एक नया नया चर है! समस्या को ठीक करने के लिए, इस खंड को किसी भी तरह में संशोधित किया जाना है।

---

और यहाँ कारण है कि @ कीपर के समाधान 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).