2016-06-27 5 views
7

dif/2 बाधा के आसपास बहुत प्रचार है, विशेष रूप से कुछ गैर-घोषणा (\ =)/2 और (\ ==)/2 के लिए एक बचाव के रूप में। इस गैर-घोषणात्मकता को अक्सर गैर-monotonicity के रूप में चिह्नित किया जाता है और गैर-सांप्रदायिकता के उदाहरण दिए जाते हैं।dif/2 बाधा शामिल कम्यूटेटिविटी को कैसे सत्यापित करें?

लेकिन यह जांचने का साधन क्या होगा कि अलग-अलग परीक्षण मामलों में अंतर/2 शामिल हैं या नहीं। यहाँ एक मेटा विवरण है कि मैं क्या करना चाहते हैं:

मैं एक commutativity परीक्षण करना, और मैं जांच करने के लिए दोनों एक ही परिणाम दे वेरिएंट कि चाहते हैं: तो आम तौर पर आप कर सकते हैं

?- A, B. 
-- versus -- 
?- B, A. 

monotonicity की जांच करें, अगर यह कम्यूटेटिविटी की जांच करने के लिए उबलता है, (==)/2 अंतर्निर्मित भविष्यवाणी के साथ। चूंकि यह अनुमान तत्काल चर का पालन करता है।

लेकिन यदि आप बाधा उत्पन्न करने वाले मामलों का परीक्षण कर रहे हैं, तो call_with_residue/2 पर्याप्त नहीं है, आपको बाधाओं की समानता भी प्राप्त करने की आवश्यकता है। कौन सा मुश्किल हो सकता है, जैसा कि निम्न उदाहरण दिखाता है:

Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.23) 
Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam 

?- dif(f(X,X),f(a(U,g(T)),a(g(Z),U))), X=a(g(Z),U). 
X = a(g(Z), U), 
dif(f(a(g(Z), U), U, Z, U, T), f(a(U, g(T)), g(Z), T, g(Z), Z)). 

?- X=a(g(Z),U), dif(f(X,X),f(a(U,g(T)),a(g(Z),U))). 
X = a(g(Z), U), 
dif(f(U, T), f(g(Z), Z)). 

कोई भी विचार कैसे आगे बढ़ना है?

अस्वीकरण, इसकी एक जाल:
मैं एक अच्छा परीक्षण विधि है, जहां आप एक विनिर्देश बनाम अच्छे और बुरे विधेय अलग कर सकते हैं के रूप में commutativity परीक्षण का समर्थन नहीं करते। चूंकि आम तौर पर दोनों अच्छे और बुरे भविष्यवाणियों में कम्यूटिटी के साथ कोई समस्या नहीं हो सकती है।

मैं अलग-अलग/2 बाधाओं की समानता के तरीकों के बारे में जानने के लिए वाहन के रूप में कम्यूटिटीविटी परीक्षण का उपयोग कर रहा हूं। इस समानता का उपयोग अधिक पारंपरिक परीक्षण मामलों में सत्यापन बिंदु के रूप में किया जा सकता है।

उत्तर

4

कई तरीके हैं। शायद इस मामले में सबसे आसान संग्रहित अवशिष्ट बाधाओं को फिर से पोस्ट करना है।

इस उदाहरण में, हम पाते हैं:

 
?- X = a(g(Z), U), 
    dif(f(a(g(Z), U), U, Z, U, T), f(a(U, g(T)), g(Z), T, g(Z), Z)). 
X = a(g(Z), U), 
dif(f(U, T), f(g(Z), Z)). 

लक्ष्य अब बहुत सरल है!

आप अवशिष्ट लक्ष्यों को copy_term/3 और call_residue_vars/2 के साथ एकत्र कर सकते हैं।

+0

लेकिन क्या मैं call_residue_vars/2 के साथ एक रिपोस्ट स्वचालित भी कर सकता हूं। मैंने कोशिश नहीं की और यह शायद बिल का केवल आधा है। यदि वे सरल हैं, तो क्या आप किसी भी तरह की बाधाओं की तुलना कर सकते हैं? (सरल लोगों को बराबर दिखने की आवश्यकता नहीं है) –

संबंधित मुद्दे