शुद्ध लैम्ब्डा कैलकुस - और फ़ंक्शन

Question

मैं वर्तमान में हास्केल सीख रहा हूं और विश्वविद्यालय में कार्यात्मक प्रोग्रामिंग के बारे में एक सैद्धांतिक व्याख्यान में भाग ले रहा हूं।

मुझे पता है कि यह विशुद्ध रूप से सैद्धांतिक/शैक्षणिक सवाल यह है, लेकिन फिर भी मैं कैसे बस शुद्ध लैम्ब्डा पथरी के साथ विभिन्न सरल कार्यों को व्यक्त करने के दिलचस्पी है (अर्थात परिभाषित किसी भी स्थिरांक के बिना)।

मेरा कुछ व्याख्यान सामग्री जैसे बूलियन मूल्यों को परिभाषित:

सच = \ xy.x
झूठी = \ xy.y

(\ दर्शाने लैम्ब्डा प्रतीक)

यदि इन्हें इन चयनकर्ता कार्यों की तरह परिभाषित किया गया है, तो if-con प्रत्यर्पण आसानी से परिभाषित किया जा सकता है:

तो = \ x.x

अब, मैं तार्किक "और" समारोह के लिए कुछ संक्षिप्त रूप के साथ आने की कोशिश कर रहा हूँ। मेरा पहला अनुमान है:।

और = \ xy {( यदि x) [(तो वाई) सचझूठी] झूठी}

तो मूल रूप से यह लैम्ब्डा फ़ंक्शन 2 तर्क प्राप्त करेगा जहां दोनों को सत्य/गलत जैसा टाइप करना होगा। यदि मैं तर्क तालिका के सभी 4 संयोजनों के साथ विभिन्न बीटा-कटौती करता हूं तो मुझे सही परिणाम मिलते हैं।

फिर भी यह फ़ंक्शन थोड़ा बदसूरत दिखता है और मैं इसे और अधिक सुरुचिपूर्ण बनाने के बारे में सोच रहा हूं। यहां कोई प्रस्ताव है?

Answer 1

हम केवल एक पिथियर प्राप्त करने के लिए आपके उत्तर पर कटौती कर सकते हैं।

पहले कुछ गर्म-अप। स्पष्ट रूप से IF x ==> x, और TRUE TRUE FALSE ==> TRUE और FALSE TRUE FALSE ==> FALSE यदि x एक बूलियन है तो x TRUE FALSE ==> x है।

अब हम

\x y . (IF x) ((IF y) TRUE FALSE) FALSE 
\x y .  x ( y TRUE FALSE) FALSE -- using IF x   ==> x 
\x y .  x ( y   ) FALSE -- using y TRUE FALSE ==> y 
\x y . x y FALSE       -- clean up 

को कम करने और इस अभिव्यक्ति अभी भी

AND TRUE TRUE = TRUE TRUE FALSE = TRUE 
AND FALSE TRUE = FALSE TRUE FALSE = FALSE 
AND TRUE FALSE = TRUE FALSE FALSE = FALSE 
AND FALSE FALSE = FALSE FALSE FALSE = FALSE 

Answer 2

अच्छा, and True पहचान फ़ंक्शन है, और and False निरंतर फ़ंक्शन False लौटा रहा है, इसलिए हम इसका उपयोग कर सकते हैं।

and = \x. if x id (const False) 

जो के साथ एक अच्छा समरूपता है

or = \x. if x (const True) id 

(जहां

id = \x. x 
const = \x y. x 

)

eliminators के लिए आम पैटर्न तर्क सूची के अंत में डेटा ले जाता है जो अक्सर पॉइंटफ्री शैली के साथ खूबसूरती से काम करता है, इसलिए यदि आपने परिभाषित किया है:

cond = \t f b. b t f 

तो आप

and = cond id (const False) 
or = cond (const True) id 

व्यक्त कर सकते हैं जो सबसे अच्छा मुझे मिल गया है है। शांत तरीकों से बूल को देखकर शायद अभी तक और अधिक सुरुचिपूर्ण फॉर्मूलेशन हैं।

Answer 3

चर्च के बूलियन्स, सही सच्चाई तालिकाओं के साथ काम करता है? :) मैंने RankNTypes सुविधा का उपयोग कर एक छोटे मॉड्यूल के लिए विकसित किया ताकि उन्हें मूल लैम्ब्डा कैलकुस संस्करण के करीब के रूप में प्रस्तुत किया जा सके।

तो, आप RankNTypes सक्षम करता है, तो:

{-# LANGUAGE RankNTypes #-} 

आप किसी भी प्रकार a के लिए कार्य a -> a -> a रूप में चर्च बूलियन्स के प्रकार का प्रतिनिधित्व कर सकते हैं, इस प्रकार यह सच है और झूठी से मिलता-जुलता के लिए एक कॉम्पैक्ट प्रतिनिधित्व कर रहे हैं। यहां टाइपिंग हमें कार्यों को अधिक स्वतंत्र रूप से लिखने की अनुमति देगी, हालांकि।

type CBool = forall a. a -> a -> a 

ctrue :: CBool 
ctrue t f = t 

cfalse :: CBool 
cfalse t f = f 

अब, इन शर्तों में एक संयोजन कैसे लिखा गया है? आइए मान लें कि आपके पास बाएं ऑपरेंड l और दाएं ऑपरेंड r है जो CBool दोनों हैं, जो a -> a -> a फ़ंक्शन हैं जो या तो आपको ctrue या cfalse पर निर्भर करता है या तो आपको पहला या दूसरा पैरामीटर देता है। आप पहले पैरामीटर और l इनपुट के रूप में इनपुट r इनपुट करके इस फ़ंक्शन का मूल्यांकन कर सकते हैं। यदि lctrue है, तो यह उसके पहले पैरामीटर का मूल्यांकन करेगा, जो r है: यह ctrue फिर से होना चाहिए, तो हमारा संयोजन संतुष्ट है। किसी भी अन्य मामले में, cfalse वापस कर दिया जाएगा।

cand :: CBool -> CBool -> CBool 
cand l r = l r l 

अलगाव सीधे कार्यों इनपुट में दी गई बूलियन्स का प्रतिनिधित्व करने का मूल्यांकन करने का एक ही चाल के साथ एक समान तरीके से दर्शाया जा सकता है।सिवाय इसके कि यहाँ आप l के मूल्यांकन के लिए दो तर्क स्वैप करेंगे: यदि lctrue है, यह वापस आ जाएगी l ही नहीं तो यह है सब r के मूल्य

cor :: CBool -> CBool -> CBool 
cor l r = l l r 

को RankNTypes सक्षम करके, मुझे लगता है कि यह है निकटतम के रूप में आप Lambda कैलकुस में चर्च के बुलियन संख्याओं के संयोजन और संयोजन के मूल परिभाषाओं के लिए प्राप्त कर सकते हैं। मैंने नियमित रूप से बूल और सीबीूल, अस्वीकृति, और उसी शैली के साथ चर्च की प्राकृतिक संख्याओं से आगे और आगे अनुवाद करने के लिए कार्यों को भी लिखा। आप पूरे स्रोत कोड को https://github.com/rtraverso86/haskkit/blob/master/Haskkit/Data/Church.hs पर पा सकते हैं।