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

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

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

प्रयोग

चर्च एन्कोडिंग का सीधा कार्यान्वयन $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 फलन प्रयुक्त करने के लिए n-1 बार।

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

${\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. इस नए प्रारंभिक कंटेनर को कॉल करें const. उपरोक्त तालिका के दाहिने हाथ की ओर के विस्तार को दर्शाता है n inc const. फिर रिप्लेस करके init साथ const के लिए अभिव्यक्ति में same  फलन  हमें पूर्ववर्ती  फलन  मिलता है,

$\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=\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$ कई बीटा कटौती लेता है। जब तक हाथ से कटौती नहीं कर रहा है, इससे कोई फर्क नहीं पड़ता, किन्तु यह उत्तम है कि इस गणना को दो बार न करना पड़े। परीक्षण संख्याओं के लिए सबसे सरल विधेय IsZero है इसलिए स्थिति पर विचार करें।

$\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 पुनरावर्ती परिभाषा है। रिकर्सन को प्रयुक्त करने के लिए फिक्स्ड-पॉइंट कॉम्बिनेटर का उपयोग किया जा सकता है। Div by नामक नया फलन बनाएँ;

• वाम भाग में $\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)))$

विभाजन के लिए यहाँ समान परिभाषा दी गई है, इस परिभाषा को छोड़कर, प्रत्येक जोड़ी में मान शून्य होना चाहिए (ऊपर OneZero देखें)। 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}$