क्या यह साबित हो सकता है कि कॉल-बाय-आवश्यकता में सभी कमी रणनीतियों के बीच न्यूनतम असीमित समय जटिलता है?

Question

जब मैं चर्च Rosser द्वितीय प्रमेय here

प्रमेय (चर्च Rosser द्वितीय)

पढ़ अगर वहाँ एक समाप्त कमी है, तो सबसे बाहरी कमी को समाप्त कर देगा, भी।

मैं सोच रहा हूँ: वहाँ कुछ प्रमेय जो चर्च Rosser द्वितीय प्रमेय को मजबूत इतना है कि यह asymptotic समय के बजाय जटिलता समाप्ति के बारे में बताता है है?

या, क्या यह साबित हो सकता है कि कॉल-दर-आवश्यकता रणनीति में सभी कमी रणनीतियों के बीच न्यूनतम असीमित समय जटिलता है?

Answer 1

मुझे लगता है कि आपका प्रश्न थोड़ा उलझन में है। कृपया, मुझे कुछ बिंदुओं को स्पष्ट करने दें।

सभी प्रमेय

सबसे पहले आप का उल्लेख पारंपरिक रूप से मानकीकरण प्रमेय के रूप में जाना जाता है, और करी की वजह से है और Feys (combinatory तर्क मैं, 1958), Hindley से ईटा कमी का सामान्यीकरण (Standard and normal reductions), और फिर कई अन्य लेखकों द्वारा संशोधित (उदाहरण के लिए यह question देखें)।

दूसरा, बाहरीतम कमी आवश्यकता से कॉल से अलग है (आवश्यकता के अनुसार कॉल शब्द की पारंपरिक समझ में कमी रणनीति भी नहीं है)।

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

       n 2 I I 

जहां एन और 2 चर्च पूर्णांक हैं, और मैं एक पहचान है। मैं अंत में दो I जोड़ता हूं, अन्यथा कमजोर-कमी वाली भाषाएं गणना को बहुत जल्दी रोक देंगे।

गौर करें कि अवधि

      2 (2 (... (2 I))..) I 

और करने के लिए कम कर देता है (2 मैं), तो मैं करने के लिए कम कर देता है अंतरतम कमी के साथ आप रैखिक समय w.r.t n में अवधि को कम करने में सक्षम होगा।

दूसरी तरफ, मैं आपको हास्केल में पिछली गणना करने के लिए आमंत्रित करता हूं, और आपको पता चलेगा कि कमी का समय एन में तेजी से बढ़ता है।मैं इस घटना के कारणों को समझने के लिए आपको छोड़ देता हूं।

इसी तरह की एक चर्चा इस thread में की गई है।

Answer 2

निश्चित रूप से नहीं। पर विचार करें

f x y = sum [1..x] + y 
g x = sum (map (f x) [1..x]) 

कॉल-दर-जरूरत g x की कमी हे (एक्स^2) अतिरिक्त प्रदर्शन करेंगे, लेकिन वास्तव में केवल हे (एक्स) जरूरी हैं। उदाहरण के लिए, आलसी एचएनएफ हमें यह जटिलता प्राप्त करेगा।

-- The definition f3 will get lazily refined. 
let f3 y = f 3 y = sum [1,2,3] + y 

g 3 = sum (map f3 [1,2,3]) 
    = sum [f3 1, f3 2, f3 3] 

-- Now let's refine f3 to HNF *before* applying it 
f3 y = sum [1,2,3] + y 
    = 6 + y 

-- And continue g 3 
g 3 = sum [f3 1, f3 2, f3 3] 
    -- no need to compute sum [1..x] three times 
    = sum [6 + 1, 6 + 2, 6 + 3] 
    = ... 

मैंने मूल्यांकन आदेश को यहां थोड़ा सा सौंप दिया, लेकिन उम्मीद है कि आपको यह विचार मिल जाएगा। हम इसे लागू करने से पहले एचएनएफ को फ़ंक्शन बॉडी को कम करते हैं, इस प्रकार किसी भी गणना को साझा करते हैं जो तर्क पर निर्भर नहीं होता है।

इसके बारे में बहुत कुछ के लिए, माइकल जोनाथन थियर के Lazy Specialization देखें।