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

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

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

प्रयोग

चर्च एन्कोडिंग का एक सीधा कार्यान्वयन कुछ एक्सेस ऑपरेशंस को धीमा कर देता है $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$ बीटा रिडक्शन या .CE.B2-रिडक्शन|β-समतुल्य है $(\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 के चारों ओर एक कंटेनर बनाकर हासिल किया जाता है, जिसे इस तरह से प्रारंभ किया जाता है कि फ़ंक्शन के आवेदन को पहली बार छोड़ दिया जाता है। अधिक विस्तृत विवरण के लिए पूर्ववर्ती कार्य की या Derivation देखें।

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

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

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

Function	Algebra	Identity	Function definition	Lambda expressions
Successor	$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)$	...
Addition	$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$
Multiplication	$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)$
Exponentiation	$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$
Predecessor	$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)$
Subtraction (Monus)	$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}$