चर्च एन्कोडिंग

गणित में, चर्च एन्कोडिंग लैम्ब्डा कैलकुलस में डेटा और ऑपरेटरों का प्रतिनिधित्व करने का साधन है। चर्च अंक लैम्ब्डा संकेतन का उपयोग करते हुए प्राकृतिक संख्याओं का प्रतिनिधित्व करते हैं। विधि का नाम अलोंजो चर्च के नाम पर रखा गया है, जिसने सबसे पहले लैम्ब्डा कैलकुलस में डेटा को इस तरह से एनकोड किया था।

सामान्यतः अन्य संकेतन (जैसे पूर्णांक, बूलियन, जोड़े, सूचियाँ और टैग किए गए संघ) में आदिम माने जाने वाले शब्दों को चर्च एन्कोडिंग के अनुसार उच्च-क्रम के कार्यों में मैप किया जाता है। चर्च-ट्यूरिंग थीसिस का प्रमाणित है कि किसी भी संगणनीय ऑपरेटर (और उसके संचालन) को चर्च एन्कोडिंग के अनुसार प्रदर्शित किया जा सकता है। लैम्ब्डा कैलकुलस में एकमात्र आदिम डेटा प्रकार फलन है।

प्रयोग

चर्च एन्कोडिंग का सीधा कार्यान्वयन $O(1)$ को $O(n)$ तक कुछ पहुंच संचालन को धीमा कर देता है , जहां $n$ डेटा संरचना का आकार है, जो चर्च एन्कोडिंग को अव्यावहारिक हो जाती है। शोध से पता चला है कि इसे लक्षित अनुकूलन द्वारा संबोधित किया जा सकता है, किन्तु अधिकांश कार्यात्मक प्रोग्रामिंग भाषाएं इसके अतिरिक्त बीजगणितीय डेटा प्रकारों को सम्मिलित करने के लिए अपने मध्यवर्ती प्रतिनिधित्वों का विस्तार करती हैं। वैसे भी, चर्च एन्कोडिंग अधिकांशतः सैद्धांतिक तर्कों में प्रयोग किया जाता है, क्योंकि यह आंशिक मूल्यांकन और प्रमेय सिद्ध करने के लिए प्राकृतिक प्रतिनिधित्व है। संचालन को उच्च-सीमा वाले प्रकारों का उपयोग करके टाइप किया जा सकता है, और आदिम पुनरावर्तन आसानी से सुलभ है। यह धारणा कि फलन केवल आदिम डेटा प्रकार हैं, कई प्रमाणों को सुव्यवस्थित करते हैं।

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

चर्च अंक

चर्च अंक चर्च एन्कोडिंग के अनुसार प्राकृतिक संख्याओं का प्रतिनिधित्व करते हैं। प्राकृतिक संख्या n का प्रतिनिधित्व करने वाला उच्च-क्रम फलन ऐसा फलन है जो किसी फलन $f$ इसकी एन-गुना फलन संरचना के लिए मैप करता है। सरल शब्दों में, अंक का मान उस संख्या के समान होता है जितनी बार फलन अपने तर्क को समाहित करता है।

$f^{\circ n}=\underbrace {f\circ f\circ \cdots \circ f} _{n{\text{ times}}}.\,$

सभी चर्च अंक ऐसे फलन हैं जो दो पैरामीटर लेते हैं। चर्च अंक 0, 1, 2, ..., को लैम्ब्डा कैलकुस में निम्नानुसार परिभाषित किया गया है।

प्रारंभिक 0 फलन को बिल्कुल भी प्रयुक्त नहीं करना 1 फलन को एक बार प्रयुक्त करना, 2 फलन को दो बार प्रयुक्त करना, 3 फलन को तीन बार प्रयुक्त करना आदि:

${\begin{array}{r|l|l}{\text{Number}}&{\text{Function definition}}&{\text{Lambda expression}}\\\hline 0&0\ f\ x=x&0=\lambda f.\lambda x.x\\1&1\ f\ x=f\ x&1=\lambda f.\lambda x.f\ x\\2&2\ f\ x=f\ (f\ x)&2=\lambda f.\lambda x.f\ (f\ x)\\3&3\ f\ x=f\ (f\ (f\ x))&3=\lambda f.\lambda x.f\ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\ f\ x=f^{n}\ x&n=\lambda f.\lambda x.f^{\circ n}\ x\end{array}}$

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

चर्च अंकों के साथ गणना

संख्याओं पर अंकगणितीय संक्रियाओं को चर्च अंकों पर कार्यों द्वारा दर्शाया जा सकता है। इन कार्यों को लैम्ब्डा कैलकुस में परिभाषित किया जा सकता है, या अधिकांश कार्यात्मक प्रोग्रामिंग भाषाओं में कार्यान्वित किया जा सकता है (लैम्ब्डा अभिव्यक्ति को फलन में परिवर्तित करना देखें))।

अतिरिक्त फलन $\operatorname {plus} (m,n)=m+n$ पहचान का उपयोग करता है $f^{\circ (m+n)}(x)=f^{\circ m}(f^{\circ n}(x))$.

$\operatorname {plus} \equiv \lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)$

उत्तराधिकारी फलन $\operatorname {succ} (n)=n+1$ बीटा रिडक्शन या सीई.बी2-रिडक्शन β-समतुल्य है $(\operatorname {plus} \ 1)$.

$\operatorname {succ} \equiv \lambda n.\lambda f.\lambda x.f\ (n\ f\ x)$

गुणन फलन $\operatorname {mult} (m,n)=m*n$ पहचान का उपयोग करता है $f^{\circ (m*n)}(x)=(f^{\circ n})^{\circ m}(x)$.

$\operatorname {mult} \equiv \lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f)\ x$

घातांक फलन $\operatorname {exp} (m,n)=m^{n}$ चर्च अंकों की परिभाषा द्वारा दिया गया है, $n\ h\ x=h^{n}\ x$. परिभाषा में स्थानापन्न $h\to m,x\to f$ पाने के $n\ m\ f=m^{n}\ f$ और,

$\operatorname {exp} \ m\ n=m^{n}=n\ m$

जो लैम्ब्डा अभिव्यक्ति देता है,

$\operatorname {exp} \equiv \lambda m.\lambda n.n\ m$

$\operatorname {pred} (n)$ h> फलन को समझना अधिक कठिन है।

$\operatorname {pred} \equiv \lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)$

एक चर्च अंक n बार फलन प्रयुक्त करता है। पूर्ववर्ती फलन को फलन वापस करना चाहिए जो इसके पैरामीटर n - 1 बार प्रयुक्त करता है। यह f और x के चारों ओर कंटेनर बनाकर प्राप्त किया जाता है, जिसे इस तरह से प्रारंभ किया जाता है कि फलन के आवेदन को पहली बार छोड़ दिया जाता है। अधिक विस्तृत विवरण के लिए पूर्ववर्ती फलन की या व्युत्पत्ति देखें।

घटाव फलन पूर्ववर्ती फलन के आधार पर लिखा जा सकता है।

$\operatorname {minus} \equiv \lambda m.\lambda n.(n\operatorname {pred} )\ m$

चर्च अंकों पर कार्यों की तालिका

फलन	बीजगणित	पहचान	फलन परिभाषा	लैम्ब्डा भाव
उत्तराधिकारी	$n+1$	$f^{n+1}\ x=f(f^{n}x)$	$\operatorname {succ} \ n\ f\ x=f\ (n\ f\ x)$	$\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)$	...
जोड़ना	$m+n$	$f^{m+n}\ x=f^{m}(f^{n}x)$	$\operatorname {plus} \ m\ n\ f\ x=m\ f\ (n\ f\ x)$	$\lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)$	$\lambda m.\lambda n.n\operatorname {succ} m$
गुणन	$m*n$	$f^{m*n}\ x=(f^{m})^{n}\ x$	$\operatorname {multiply} \ m\ n\ f\ x=m\ (n\ f)\ x$	$\lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f)\ x$	$\lambda m.\lambda n.\lambda f.m\ (n\ f)$
घातांक	$m^{n}$	$n\ m\ f=m^{n}\ f$	$\operatorname {exp} \ m\ n\ f\ x=(n\ m)\ f\ x$	$\lambda m.\lambda n.\lambda f.\lambda x.(n\ m)\ f\ x$	$\lambda m.\lambda n.n\ m$
पूर्वाधिकारी	$n-1$	$\operatorname {inc} ^{n}\operatorname {con} =\operatorname {val} (f^{n-1}x)$	$if(n==0)\ 0\ else\ (n-1)$	$\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)$
घटाव (मोनस)	$m-n$	$f^{m-n}\ x=(f^{-1})^{n}(f^{m}x)$	$\operatorname {minus} \ m\ n=(n\operatorname {pred} )\ m$	...	$\lambda m.\lambda n.n\operatorname {pred} m$

 Note:

पूर्ववर्ती फलन की व्युत्पत्ति

चर्च एन्कोडिंग में प्रयुक्त पूर्ववर्ती फलन है,

$\operatorname {pred} (n)={\begin{cases}0&{\mbox{if }}n=0,\\n-1&{\mbox{otherwise}}\end{cases}}$.

पूर्ववर्ती बनाने के लिए हमें फलन को 1 कम समय में प्रयुक्त करने का एक विधि चाहिए। एक अंक n फलन f n बार x पर प्रयुक्त होता है। फलन n-1 बार प्रयुक्त करने के लिए पूर्ववर्ती फलन को अंक n का उपयोग करना चाहिए।

पूर्ववर्ती फलन को प्रयुक्त करने से पहले, यहां एक योजना है जो मान को कंटेनर फलन में लपेटती है। हम f और x के स्थान पर उपयोग करने के लिए नए कार्यों को परिभाषित करेंगे, जिन्हें inc और init कहा जाता है। कंटेनर फलन को + कहा जाता है। तालिका के बाईं ओर inc और init पर प्रयुक्त अंक n दिखाता है।

${\begin{array}{r|r|r}{\text{Number}}&{\text{Using init}}&{\text{Using const}}\\\hline 0&\operatorname {init} =\operatorname {value} \ x&\\1&\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f\ x)&\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x\\2&\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} )=\operatorname {value} \ (f\ (f\ x))&\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} )=\operatorname {value} \ (f\ x)\\3&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} ))=\operatorname {value} \ (f\ (f\ (f\ x)))&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} ))=\operatorname {value} \ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f^{n}\ x)=\operatorname {value} \ (n\ f\ x)&n\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ (f^{n-1}\ x)=\operatorname {value} \ ((n-1)\ f\ x)\\\end{array}}$

सामान्य पुनरावृत्ति नियम है

$\operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)$

यदि कंटेनर से मान प्राप्त करने के लिए कोई फलन भी है ( extract कहा जाता है),

$\operatorname {extract} \ (\operatorname {value} \ v)=v$

तब extract का उपयोग samenum कार्य को परिभाषित करने के लिए किया जा सकता है,

$\operatorname {samenum} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {init} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ (n\ f\ x))=\lambda n.\lambda f.\lambda x.n\ f\ x=\lambda n.n$

samenum}um कार्य आंतरिक रूप से उपयोगी नहीं है। चूँकि, जैसा कि inc प्रतिनिधियों ने अपने कंटेनर तर्क के लिए f को कॉल किया है, हम यह व्यवस्थित कर सकते हैं कि पहले एप्लिकेशन inc पर एक विशेष कंटेनर प्राप्त होता है जो f के पहले एप्लिकेशन को छोड़ने की अनुमति देने वाले इसके तर्क को अनदेखा करता है। इस नए प्रारंभिक कंटेनर को कॉल करें। उपरोक्त तालिका का दाहिना भाग n inc const के विस्तार को दर्शाता है। फिर same फलन के व्यंजक में init को const से प्रतिस्थापित करने पर हमें पूर्ववर्ती फलन प्राप्त होता है,

$\operatorname {pred} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {const} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ ((n-1)\ f\ x))=\lambda n.\lambda f.\lambda x.(n-1)\ f\ x=\lambda n.(n-1)$

जैसा कि कार्यों के नीचे समझाया गया है inc, init, const, value और extract के रूप में परिभाषित किया जा सकता है,

${\begin{aligned}\operatorname {value} &=\lambda v.(\lambda h.h\ v)\\\operatorname {extract} k&=k\ \lambda u.u\\\operatorname {inc} &=\lambda g.\lambda h.h\ (g\ f)\\\operatorname {init} &=\lambda h.h\ x\\\operatorname {const} &=\lambda u.x\end{aligned}}$

जो pred के रूप में लैम्ब्डा अभिव्यक्ति देता है जैसा,

$\operatorname {pred} =\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)$

वैल्यू कंटेनर मान कंटेनर फलन को उसके मान पर प्रयुक्त करता है। इसके द्वारा परिभाषित किया गया है, $\operatorname {value} \ v\ h=h\ v$ इसलिए, $\operatorname {value} =\lambda v.(\lambda h.h\ v)$ इंक inc}nc फलन को v युक्त मान लेना चाहिए, और f v युक्त एक नया मान वापस करना चाहिए। $\operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)$ g को मान कंटेनर होने दें, $g=\operatorname {value} \ v$ तब, $g\ f=\operatorname {value} \ v\ f=f\ v$ इसलिए, $\operatorname {inc} \ g=\operatorname {value} \ (g\ f)$ $\operatorname {inc} =\lambda g.\lambda h.h\ (g\ f)$

निकालें पहचान फलन प्रयुक्त करके मान निकाला जा सकता है, $I=\lambda u.u$ I का उपयोग करते हुए , $\operatorname {value} \ v\ I=v$ इसलिए, $\operatorname {extract} \ k=k\ I$ स्थिरांक pred को प्रयुक्त करने के लिए init फलन को उस const से बदल दिया जाता है जो f प्रयुक्त नहीं होता है। हमें संतुष्ट करने के लिए const की आवश्यकता है, $\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x$ $\lambda h.h\ (\operatorname {const} \ f)=\lambda h.h\ x$ जो संतुष्ट है यदि , $\operatorname {const} \ f=x$ या लैम्ब्डा अभिव्यक्ति के रूप में, $\operatorname {const} =\lambda u.x$

पूर्व को परिभाषित करने का अन्य विधि

जोड़े का उपयोग करके पूर्व को भी परिभाषित किया जा सकता है:

${\begin{aligned}\operatorname {f} =&\ \lambda p.\ \operatorname {pair} \ (\operatorname {second} \ p)\ (\operatorname {succ} \ (\operatorname {second} \ p))\\\operatorname {zero} =&\ (\lambda f.\lambda x.\ x)\\\operatorname {pc0} =&\ \operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} \\\operatorname {pred} =&\ \lambda n.\ \operatorname {first} \ (n\ \operatorname {f} \ \operatorname {pc0} )\\\end{aligned}}$

यह सरल परिभाषा है, किन्तु पूर्व के लिए अधिक जटिल अभिव्यक्ति की ओर ले जाती है।

के लिए विस्तार $\operatorname {pred} \operatorname {three}$:

${\begin{aligned}\operatorname {pred} \operatorname {three} =&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} ))))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {zero} \ \operatorname {one} )))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {one} \ \operatorname {two} ))\\=&\ \operatorname {first} \ (\operatorname {pair} \ \operatorname {two} \ \operatorname {three} )\\=&\ \operatorname {two} \end{aligned}}$

विभाग

प्राकृतिक संख्याओं का विभाजन (गणित) किसके द्वारा कार्यान्वित किया जा सकता है,

$n/m=\operatorname {if} \ n\geq m\ \operatorname {then} \ 1+(n-m)/m\ \operatorname {else} \ 0$

$n-m$ की गणना करने में कई बीटा कटौती होती है। जब तक हाथ से कटौती नहीं कर रहा है, इससे कोई फर्क नहीं पड़ता, किन्तु यह उत्तम है कि इस गणना को दो बार न करना पड़े। परीक्षण संख्याओं के लिए सबसे सरल विधेय इस्ज़ेरो है इसलिए स्थिति पर विचार करें।

$\operatorname {IsZero} \ (\operatorname {minus} \ n\ m)$

किन्तु यह स्थिति $n\leq m$ के समतुल्य है, न कि $n<m$ यदि इस अभिव्यक्ति का उपयोग किया जाता है तो ऊपर दी गई विभाजन की गणितीय परिभाषा को चर्च के अंकों पर कार्य में अनुवादित किया जाता है,

$\operatorname {divide1} \ n\ m\ f\ x=(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (\operatorname {divide1} \ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)$

वांछित के रूप में, इस परिभाषा में $\operatorname {minus} \ n\ m$ के लिए एक ही कॉल है। चूँकि परिणाम यह है कि यह सूत्र $(n-1)/m$ का मान देता है।

विभाजित करने से पहले n में 1 जोड़कर इस समस्या को ठीक किया जा सकता है। विभाजन की परिभाषा तब है,

$\operatorname {divide} \ n=\operatorname {divide1} \ (\operatorname {succ} \ n)$

विभाजित 1 पुनरावर्ती परिभाषा है। पुनरावर्तन को प्रयुक्त करने के लिए फिक्स्ड-पॉइंट कॉम्बिनेटर का उपयोग किया जा सकता है। डिव बाय; नामक नया फलन बनाएँ;

• वाम भाग में $\operatorname {divide1} \rightarrow \operatorname {div} \ c$
• दाहिने हाथ में $\operatorname {divide1} \rightarrow c$

पाने के लिए और,

$\operatorname {div} =\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)$

तब,

$\operatorname {divide} =\lambda n.\operatorname {divide1} \ (\operatorname {succ} \ n)$

जहां ,

${\begin{aligned}\operatorname {divide1} &=Y\ \operatorname {div} \\\operatorname {succ} &=\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)\\Y&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\0&=\lambda f.\lambda x.x\\\operatorname {IsZero} &=\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} \end{aligned}}$

${\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}$

${\begin{aligned}\operatorname {minus} &=\lambda m.\lambda n.n\operatorname {pred} m\\\operatorname {pred} &=\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)\end{aligned}}$

देता है,

${\displaystyle \scriptstyle \operatorname {divide} =\lambda n.((\lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x)))\ (\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.(\lambda n.n\ (\lambda x.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a))\ d\ ((\lambda f.\lambda x.x)\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ ((\lambda m.\lambda n.n(\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u))m)\ n\ m)))\ ((\lambda n.\lambda f.\lambda x.f\ (n\ f\ x))\$

या λ के लिए \ का उपयोग कर पाठ के रूप में

डिवाइड = (\n.((\f.(\x.x x) (\x.f (x x))) (\c.\n.\m.\f.\x.(\d.(\n.n (\x) .(\a.\b.b)) (\a.\b.a)) d ((\f.\x.x) f x) (f (c d m f x))) ((\m.\n.n (\n.\f.\) x.n (\g.\h.h (g f)) (\u.x) (\u.u)) m) n m))) ((\n.\f.\x. f (n f x)) n))

उदाहरण के लिए, 9/3 द्वारा दर्शाया गया है

डिवाइड (\f.\x.f (f (f (f (f (f (f (f (f x)))))))) (\f.\x.f (f (f x)))

लैम्ब्डा कैलकुलस कैलकुलेटर का उपयोग करते हुए, सामान्य क्रम का उपयोग करते हुए, उपरोक्त अभिव्यक्ति 3 तक कम हो जाती है।

\f.\x.f (f (f (x)))

हस्ताक्षरित संख्या

चर्च अंकों को पूर्णांक तक विस्तारित करने के लिए सरल दृष्टिकोण चर्च जोड़ी का उपयोग करना है, जिसमें चर्च अंक सकारात्मक और ऋणात्मक मान का प्रतिनिधित्व करते हैं। पूर्णांक मान दो चर्च अंकों के बीच का अंतर है।

एक प्राकृतिक संख्या को हस्ताक्षरित संख्या में परिवर्तित किया जाता है,

$\operatorname {convert} _{s}=\lambda x.\operatorname {pair} \ x\ 0$

मानो की अदला-बदली करके ऋणात्मकता का प्रदर्शन किया जाता है।

$\operatorname {neg} _{s}=\lambda x.\operatorname {pair} \ (\operatorname {second} \ x)\ (\operatorname {first} \ x)$

यदि जोड़ी में से शून्य है तो पूर्णांक मान अधिक स्वाभाविक रूप से प्रदर्शित होता है। OneZero फलन इस स्थिति को प्राप्त करता है,

$\operatorname {OneZero} =\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (\operatorname {OneZero} \ \operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x))))$

रिकर्सन को वाई कॉम्बिनेटर का उपयोग करके कार्यान्वित किया जा सकता है,

$\operatorname {OneZ} =\lambda c.\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (c\ \operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x))))$

$\operatorname {OneZero} =Y\operatorname {OneZ}$

प्लस और माइनस

जोड़ी पर जोड़ को गणितीय रूप से परिभाषित किया गया है,

$x+y=[x_{p},x_{n}]+[y_{p},y_{n}]=x_{p}-x_{n}+y_{p}-y_{n}=(x_{p}+y_{p})-(x_{n}+y_{n})=[x_{p}+y_{p},x_{n}+y_{n}]$

अंतिम अभिव्यक्ति का लैम्ब्डा कैलकुलस में अनुवाद किया गया है,

$\operatorname {plus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))$

इसी प्रकार घटाव परिभाषित किया गया है,

$x-y=[x_{p},x_{n}]-[y_{p},y_{n}]=x_{p}-x_{n}-y_{p}+y_{n}=(x_{p}+y_{n})-(x_{n}+y_{p})=[x_{p}+y_{n},x_{n}+y_{p}]$

देना,

$\operatorname {minus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))$

गुणा और भाग

गुणन द्वारा परिभाषित किया जा सकता है,

$x*y=[x_{p},x_{n}]*[y_{p},y_{n}]=(x_{p}-x_{n})*(y_{p}-y_{n})=(x_{p}*y_{p}+x_{n}*y_{n})-(x_{p}*y_{n}+x_{n}*y_{p})=[x_{p}*y_{p}+x_{n}*y_{n},x_{p}*y_{n}+x_{n}*y_{p}]$

अंतिम अभिव्यक्ति का लैम्ब्डा कैलकुलस में अनुवाद किया गया है,

$\operatorname {mult} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))$

विभाजन के लिए यहाँ समान परिभाषा दी गई है, इस परिभाषा को छोड़कर, प्रत्येक जोड़ी में मान शून्य होना चाहिए (ऊपर वनजीरो देखें)। DivZ फलन हमें शून्य घटक वाले मान को अनदेखा करने की अनुमति देता है।

$\operatorname {divZ} =\lambda x.\lambda y.\operatorname {IsZero} \ y\ 0\ (\operatorname {divide} \ x\ y)$

divZ का उपयोग तब निम्न सूत्र में किया जाता है, जो गुणन के समान है, किन्तु divZ द्वारा प्रतिस्थापित बहु के साथ है ।

$\operatorname {divide} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))$

परिमेय और वास्तविक संख्याएं

लैम्ब्डा कैलकुस में तर्कसंगत और गणना योग्य संख्या भी एन्कोड की जा सकती है। तर्कसंगत संख्याओं को हस्ताक्षरित संख्याओं की जोड़ी के रूप में एन्कोड किया जा सकता है। संगणनीय वास्तविक संख्याओं को सीमित प्रक्रिया द्वारा एन्कोड किया जा सकता है जो गारंटी देता है कि वास्तविक मान से अंतर संख्या से भिन्न होता है जो कि हमारी आवश्यकता के अनुसार छोटा हो सकता है।

दिए गए संदर्भ सॉफ्टवेयर का वर्णन करते हैं जो सैद्धांतिक रूप से लैम्ब्डा कैलकुलस में अनुवादित हो सकते हैं। बार वास्तविक संख्या परिभाषित हो जाने के बाद जटिल संख्याएं स्वाभाविक रूप से वास्तविक संख्याओं की जोड़ी के रूप में एन्कोडेड होती हैं।

ऊपर वर्णित डेटा प्रकार और फलन प्रदर्शित करते हैं कि लैम्ब्डा कैलकुलस में किसी भी डेटा प्रकार या गणना को एन्कोड किया जा सकता है। यह चर्च-ट्यूरिंग थीसिस है।

अन्य अभ्यावेदन के साथ अनुवाद

अधिकांश वास्तविक विश्व की भाषाओं में मशीन-देशी पूर्णांकों का समर्थन है; चर्च और अनचर्च फलन गैर-ऋणात्मक पूर्णांक और उनके संबंधित चर्च अंकों के बीच परिवर्तित होते हैं। फलन यहां हास्केल (प्रोग्रामिंग भाषा) में दिए गए हैं, जहां \ लैम्ब्डा कैलकुस के λ के अनुरूप है। अन्य भाषाओं में कार्यान्वयन समान हैं।

type Church a = (a -> a) -> a -> a

church :: Integer -> Church Integer
church 0 = \f -> \x -> x
church n = \f -> \x -> f (church (n-1) f x)

unchurch :: Church Integer -> Integer
unchurch cn = cn (+ 1) 0

चर्च बूलियन्स

चर्च बूलियन सच्चे और झूठे बूलियन मानो के चर्च एन्कोडिंग हैं। कुछ प्रोग्रामिंग भाषाएं इन्हें बूलियन अंकगणित के कार्यान्वयन मॉडल के रूप में उपयोग करती हैं; उदाहरण स्मालटाक और पिको (प्रोग्रामिंग भाषा) हैं।

बूलियन तर्क को विकल्प के रूप में माना जा सकता है। सच और झूठ का चर्च एन्कोडिंग दो मापदंडों के फलन हैं:

• सच पहला पैरामीटर चुनता है।
• झूठा दूसरा पैरामीटर चुनता है।

दो परिभाषाओं को चर्च बूलियंस के रूप में जाना जाता है:

${\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}$

यह परिभाषा विधेय (अर्थात सत्य मान लौटाने वाले कार्य) को सीधे-सीधे क्रिया-खंड के रूप में फलन करने की अनुमति देती है। बूलियन लौटाने वाला फलन जिसे दो पैरामीटर पर प्रयुक्त किया जाता है, या तो पहला या दूसरा पैरामीटर देता है:

$\operatorname {predicate-} x\ \operatorname {then-clause} \ \operatorname {else-clause}$

तत्कालीन खंड का मूल्यांकन करता है यदि विधेय-एक्स सत्य का मूल्यांकन करता है और अन्य-खंड का मूल्यांकन करता है यदि विधेय-एक्स गलत का मूल्यांकन करता है।

क्योंकि सत्य और असत्य पहले या दूसरे पैरामीटर का चयन करते हैं, उन्हें लॉजिक ऑपरेटर प्रदान करने के लिए संयोजित किया जा सकता है। ध्यान दें कि नहीं के कई संभावित कार्यान्वयन हैं।

${\begin{aligned}\operatorname {and} &=\lambda p.\lambda q.p\ q\ p\\\operatorname {or} &=\lambda p.\lambda q.p\ p\ q\\\operatorname {not} _{1}&=\lambda p.\lambda a.\lambda b.p\ b\ a\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}$

कुछ उदाहरण:

$\operatorname {IsZero}$