ये सभी प्रमेय राज्य यह है कि एक अभिव्यक्ति जिसे कई पथों के माध्यम से कम किया जा सकता है, एक सामान्य उत्पाद के लिए आवश्यक रूप से कम हो जाएगा।
उदाहरण के लिए, हास्केल कोड के इस टुकड़े ले:
vecLenSq :: Float -> Float -> Float
vecLenSq x y =
xsq + ysq
where
xsq = x * x
ysq = y * y
लैम्ब्डा पथरी में, इस समारोह मोटे तौर पर के बराबर है (कोष्ठक स्पष्टता के लिए कहा, ऑपरेटरों आदिम ग्रहण):
λ x . (λ y . (λ xsq . (λ ysq . (xsq + ysq)) (y * y)) (x * x))
पहली बार xsq पर β कमी को लागू करने या ysq पर β कमी लागू करने के द्वारा अभिव्यक्ति को कम किया जा सकता है, यानी "मूल्यांकन का क्रम" मनमाना है। एक निम्न क्रम में अभिव्यक्ति को कम कर सकते हैं:
λ x . (λ y . (λ xsq . (xsq + (y * y))) (x * x))
λ x . (λ y . ((x * x) + (y * y)))
... या निम्न क्रम में:
λ x . (λ y . (λ ysq . ((x * x) + ysq)) (y * y))
λ x . (λ y . ((x * x) + (y * y)))
परिणाम जाहिर है एक ही है।
इसका मतलब है कि xsq और ysq शब्द स्वतंत्र रूप से कमजोर हैं, और उनकी कटौती समानांतर हो सकती है। और वास्तव में, एक हास्केल में तो जैसे कटौती parallelize सकता है:
vecLenSq :: Float -> Float -> Float
vecLenSq x y =
(xsq `par` ysq) `pseq` xsq + ysq
where
xsq = x * x
ysq = y * y
यह बनता है वास्तव में इस विशेष स्थिति में एक लाभ की पेशकश नहीं होगा, के बाद से दो साधारण नाव गुणा अनुक्रम में मार डाला दो paralellized गुणा क्योंकि से अधिक प्रभावी हैं शेड्यूलिंग ओवरहेड का, लेकिन यह अधिक जटिल संचालन के लिए सार्थक हो सकता है।
मैं उस प्रमेय से परिचित नहीं हूं, लेकिन पहली बार यह वास्तव में कोड लिखने के बजाय सैद्धांतिक दृष्टिकोण से अधिक उपयोगी लगता है। संगम सुनिश्चित करने के लिए यह "अच्छी" संपत्तियों में से एक है जो एक पुनर्लेखन प्रणाली हो सकती है। एक बेवकूफ उदाहरण हो सकता है (मुझे यकीन नहीं है) अभिव्यक्ति '(5-1) * (1 + 1) ': आप या तो' 5-1' या '1 + 1' को सरल बनाकर शुरू कर सकते हैं, लेकिन आप समाप्त हो सकते हैं एक ही परिणाम के लिए। –
यह समांतर कमी की धारणा बताता है: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.5081 धारा 4, पृष्ठ 12 –