haskell - समानता के लिए दो कार्यों की तुलना कैसे करें, जैसे(λx.2*x)==(λx.x+x)?




clojure lambda (4)

2 साल बीत चुके हैं, लेकिन मैं इस सवाल पर एक छोटी टिप्पणी जोड़ना चाहता हूं। मूल रूप से, मैंने पूछा कि क्या यह बताने का कोई तरीका है कि (λx.2*x) बराबर है (λx.x+x) । Λ-calculusus पर अतिरिक्त और गुणा को परिभाषित किया जा सकता है:

add = (a b c -> (a b (a b c)))
mul = (a b c -> (a (b c)))

अब, यदि आप निम्नलिखित शर्तों को सामान्यीकृत करते हैं:

add_x_x = (λx . (add x x))
mul_x_2 = (mul (λf x . (f (f x)))

आपको मिला:

result = (a b c -> (a b (a b c)))

दोनों कार्यक्रमों के लिए। चूंकि उनके सामान्य रूप बराबर हैं, दोनों कार्यक्रम स्पष्ट रूप से बराबर हैं। हालांकि यह सामान्य रूप से काम नहीं करता है, यह अभ्यास में कई शर्तों के लिए काम करता है। (λx.(mul 2 (mul 3 x)) और (λx.(mul 6 x)) उदाहरण के लिए दोनों समान सामान्य रूप हैं।

समानता के लिए दो कार्यों की तुलना करने का कोई तरीका है? उदाहरण के लिए, (λx.2*x) == (λx.x+x) सत्य वापस आना चाहिए, क्योंकि वे स्पष्ट रूप से समकक्ष हैं।


गणित की तरह प्रतीकात्मक गणना के साथ एक भाषा में:

या सी # कंप्यूटर बीजगणित पुस्तकालय के साथ :

MathObject f(MathObject x) => x + x;
MathObject g(MathObject x) => 2 * x;

{
    var x = new Symbol("x");

    Console.WriteLine(f(x) == g(x));
}

उपरोक्त कंसोल पर 'ट्रू' प्रदर्शित करता है।


यह बहुत अच्छी तरह से ज्ञात है कि सामान्य कार्य समानता सामान्य रूप से अपरिहार्य है, इसलिए आपको उस समस्या का एक सबसेट चुनना होगा जिसमें आप रुचि रखते हैं। आप इनमें से कुछ आंशिक समाधानों पर विचार कर सकते हैं:

  • प्रेस्बर्गर अंकगणित प्रथम क्रम तर्क + अंकगणित का एक निर्णायक खंड है।
  • universe पैकेज परिमित डोमेन के साथ कुल कार्यों के लिए फ़ंक्शन समानता परीक्षण प्रदान करता है।
  • आप जांच सकते हैं कि आपके कार्य इनपुट के पूरे समूह के बराबर हैं और अवांछित इनपुट पर समानता के सबूत के रूप में व्यवहार करते हैं; QuickCheck चेक देखें।
  • एसएमटी सॉल्वर एक बेहतरीन प्रयास करते हैं, कभी-कभी "बराबर" या "बराबर नहीं" के बजाय "पता नहीं" का जवाब देते हैं। हैकेज पर एसएमटी सॉल्वर के लिए कई बाइंडिंग हैं; मेरे पास सबसे अच्छा सुझाव देने के लिए पर्याप्त अनुभव नहीं है, लेकिन थॉमस एम। डुबुइसन एसबीवी का सुझाव sbv
  • कॉम्पैक्ट कार्यों पर फ़ंक्शन समानता और अन्य चीजों का निर्णय लेने पर शोध की एक मजेदार रेखा है; ब्लॉग शोध में इस शोध की मूल बातें वर्णित असंभव कार्यात्मक कार्यक्रमों में वर्णित हैं । (ध्यान दें कि कॉम्पैक्टनेस एक बहुत ही मजबूत और बहुत सूक्ष्म स्थिति है! यह ऐसा नहीं है जो अधिकांश हास्केल कार्य संतुष्ट करता है।)
  • यदि आप जानते हैं कि आपके कार्य रैखिक हैं, तो आप स्रोत स्थान के लिए आधार पा सकते हैं; तो प्रत्येक समारोह में एक अद्वितीय मैट्रिक्स प्रतिनिधित्व होता है।
  • आप अपनी अभिव्यक्ति भाषा को परिभाषित करने का प्रयास कर सकते हैं, साबित कर सकते हैं कि इस भाषा के लिए समानता निर्णायक है, और उसके बाद उस भाषा को हास्केल में एम्बेड करें। यह सबसे लचीला लेकिन प्रगति करने का सबसे कठिन तरीका भी है।

यह सामान्य रूप से अपरिहार्य है, लेकिन एक उपयुक्त सबसेट के लिए, आप आज इसे प्रभावी रूप से एसएमटी सॉल्वर का उपयोग कर प्रभावी ढंग से कर सकते हैं:

$ ghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
Prelude> :m Data.SBV
Prelude Data.SBV> (\x ->  2 * x) === (\x -> x + x :: SInteger)
Q.E.D.
Prelude Data.SBV> (\x ->  2 * x) === (\x -> 1 + x + x :: SInteger)
Falsifiable. Counter-example:
  s0 = 0 :: Integer

विवरण के लिए, देखें: https://hackage.haskell.org/package/sbv





lisp