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

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

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

प्रयोग

चर्च एन्कोडिंग का सीधा कार्यान्वयन $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}}$

देता है,

$\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)$

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

डिवाइड = (\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}}$

कुछ उदाहरण:

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

विधेय

एक विधेय एक ऐसा कार्य है जो एक बूलियन मान लौटाता है। सबसे मौलिक विधेय $\operatorname {IsZero}$ है, जो $\operatorname {true}$ लौटाता है यदि इसका तर्क चर्च अंक $0$ है, और $\operatorname {false}$ यदि इसका तर्क कोई अन्य चर्च अंक है:

$\operatorname {IsZero} =\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true}$

निम्नलिखित विधेय परीक्षण करता है कि क्या पहला तर्क दूसरे से कम-से-या-समान है:

$\operatorname {LEQ} =\lambda m.\lambda n.\operatorname {IsZero} \ (\operatorname {minus} \ m\ n)$,

पहचान के कारण,

$x=y\equiv (x\leq y\land y\leq x)$

समानता के लिए परीक्षण के रूप में प्रयुक्त किया जा सकता है,

$\operatorname {EQ} =\lambda m.\lambda n.\operatorname {and} \ (\operatorname {LEQ} \ m\ n)\ (\operatorname {LEQ} \ n\ m)$

चर्च जोड़े

See also: दोष

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

${\begin{aligned}\operatorname {pair} &\equiv \lambda x.\lambda y.\lambda z.z\ x\ y\\\operatorname {first} &\equiv \lambda p.p\ (\lambda x.\lambda y.x)\\\operatorname {second} &\equiv \lambda p.p\ (\lambda x.\lambda y.y)\end{aligned}}$

उदाहरण के लिए,

${\begin{aligned}&\operatorname {first} \ (\operatorname {pair} \ a\ b)\\=&(\lambda p.p\ (\lambda x.\lambda y.x))\ ((\lambda x.\lambda y.\lambda z.z\ x\ y)\ a\ b)\\=&(\lambda p.p\ (\lambda x.\lambda y.x))\ (\lambda z.z\ a\ b)\\=&(\lambda z.z\ a\ b)\ (\lambda x.\lambda y.x)\\=&(\lambda x.\lambda y.x)\ a\ b=a\end{aligned}}$

सूची एन्कोडिंग

सूची नोड्स से (अपरिवर्तनीय वस्तु) सूची (कंप्यूटिंग) का निर्माण किया जाता है। सूची पर मूल संचालन हैं;

कार्य	विवरण
शून्य	एक खाली सूची बनाएँ।
इस्निल	सूची खाली होने पर परीक्षण करें।
दोष	किसी दिए गए मान को (संभवतः खाली) सूची में जोड़ें।
शीर्ष	सूची का पहला तत्व प्राप्त करें।
अंतिम भाग	बाकी सूची प्राप्त करें।

हम नीचे सूचियों के चार अलग-अलग प्रतिनिधित्व देते हैं:

• प्रत्येक सूची नोड को दो जोड़े से बनाएं (खाली सूचियों की अनुमति देने के लिए)।
• प्रत्येक सूची नोड को जोड़ी से बनाएँ।
• फोल्ड (उच्च-क्रम फलन ) का उपयोग करके सूची का प्रतिनिधित्व करें।
• स्कॉट के एन्कोडिंग का उपयोग करके सूची का प्रतिनिधित्व करें जो मिलान अभिव्यक्ति के स्थितियों को तर्क के रूप में लेता है

सूची नोड के रूप में दो जोड़े

एक चर्च जोड़ी द्वारा गैर-खाली सूची को प्रयुक्त किया जा सकता है;

• सबसे पहले सिर होता है।
• दूसरे में पूंछ होती है।

चूँकि यह खाली सूची का प्रतिनिधित्व नहीं देता है क्योंकि कोई अशक्त सूचक नहीं है। शून्य का प्रतिनिधित्व करने के लिए, जोड़ी को दूसरी जोड़ी में लपेटा जा सकता है, जिससे तीन मान मिलते हैं:

• सबसे पहले - अशक्त सूचक (खाली सूची)।
• दूसरा। पहले में सिर होता है।
• दूसरा। दूसरे में पूंछ होती है।

इस विचार का उपयोग करते हुए मूल सूची संचालन को इस प्रकार परिभाषित किया जा सकता है:

अभिव्यक्ति	विवरण
$\operatorname {nil} \equiv \operatorname {pair} \ \operatorname {true} \ \operatorname {true}$	जोड़ी का पहला तत्व सत्य है जिसका अर्थ है कि सूची शून्य है।
$\operatorname {isnil} \equiv \operatorname {first}$	अशक्त (या खाली सूची) सूचक को पुनः प्राप्त करें।
$\operatorname {cons} \equiv \lambda h.\lambda t.\operatorname {pair} \operatorname {false} \ (\operatorname {pair} h\ t)$	एक सूची नोड बनाएँ, जो शून्य नहीं है, और इसे हेड एच और टेल टी दें।
$\operatorname {head} \equiv \lambda z.\operatorname {first} \ (\operatorname {second} z)$	दूसरा.पहला शीर्ष है।
$\operatorname {tail} \equiv \lambda z.\operatorname {second} \ (\operatorname {second} z)$	दूसरा.दूसराअंतिम भाग है।

एक शून्य नोड में दूसरा कभी भी एक्सेस नहीं किया जाता है, परंतु कि 'सिर' और 'पूंछ' केवल गैर-खाली सूचियों पर प्रयुक्त हों।

सूची नोड के रूप में एक जोड़ी

वैकल्पिक रूप से परिभाषित करें

${\begin{aligned}\operatorname {cons} &\equiv \operatorname {pair} \\\operatorname {head} &\equiv \operatorname {first} \\\operatorname {tail} &\equiv \operatorname {second} \\\operatorname {nil} &\equiv \operatorname {false} \\\operatorname {isnil} &\equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\operatorname {false} )\operatorname {true} \end{aligned}}$

जहां अंतिम परिभाषा सामान्य का विशेष स्थति है

$\operatorname {process-list} \equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\operatorname {head-and-tail-clause} )\operatorname {nil-clause}$

राइट फोल्ड का उपयोग करके सूची का प्रतिनिधित्व करें

चर्च जोड़े का उपयोग करके एन्कोडिंग के विकल्प के रूप में, सूची को इसके फोल्ड (उच्च-क्रम फलन ) के साथ पहचान कर एन्कोड किया जा सकता है। उदाहरण के लिए, तीन तत्वों x, y और z की सूची को उच्च-क्रम फलन द्वारा एन्कोड किया जा सकता है जब कॉम्बिनेटर c पर प्रयुक्त किया जाता है और मान n रिटर्न c x (c y (c z n)) देता है।

${\begin{aligned}\operatorname {nil} &\equiv \lambda c.\lambda n.n\\\operatorname {isnil} &\equiv \lambda l.l\ (\lambda h.\lambda t.\operatorname {false} )\ \operatorname {true} \\\operatorname {cons} &\equiv \lambda h.\lambda t.\lambda c.\lambda n.c\ h\ (t\ c\ n)\\\operatorname {head} &\equiv \lambda l.l\ (\lambda h.\lambda t.h)\ \operatorname {false} \\\operatorname {tail} &\equiv \lambda l.\lambda c.\lambda n.l\ (\lambda h.\lambda t.\lambda g.g\ h\ (t\ c))\ (\lambda t.n)\ (\lambda h.\lambda t.t)\end{aligned}}$

इस सूची प्रतिनिधित्व को प्रणाली एफ में टाइप किया जा सकता है।

स्कॉट एन्कोडिंग का उपयोग करके सूची का प्रतिनिधित्व करें

एक वैकल्पिक प्रतिनिधित्व स्कॉट एन्कोडिंग है जो निरंतरता के विचार का उपयोग करता है और सरल कोड को जन्म दे सकता है। (मोजेन्सन-स्कॉट एन्कोडिंग भी देखें)।

इस दृष्टिकोण में, हम इस तथ्य का उपयोग करते हैं कि प्रतिरूप मिलान अभिव्यक्ति का उपयोग करके सूचियों को देखा जा सकता है। उदाहरण के लिए, स्काला (प्रोग्रामिंग भाषा) नोटेशन का उपयोग करते हुए, यदि List खाली सूची Nil और कंस्ट्रक्टर Cons(h, t) के साथ प्रकार list के मान को दर्शाती है, तो हम सूची का निरीक्षण कर सकते हैं और सूची के खाली होने की स्थिति में nilCode और consCode(h, t) की गणना कर सकते हैं। सूची खाली नहीं है:

list match {
  case Nil        => nilCode
  case Cons(h, t) => consCode(h,t)
}

यह list}st दी गई है कि यह nilCode और consCodeपर कैसे कार्य करता है। इसलिए हम एक सूची को एक फलन के रूप में परिभाषित करते हैं जो ऐसे nilCodeऔर consCodeको तर्कों के रूप में स्वीकार करता है, जिससे उपरोक्त प्रतिरूप मिलान के अतिरिक्त हम बस लिख सकें:

$\operatorname {list} \ \operatorname {nilCode} \ \operatorname {consCode}$

आइए nilCode के अनुरूप पैरामीटर n द्वारा और consCodeके अनुरूप पैरामीटर c द्वारा निरूपित करें। खाली सूची वह है जो शून्य तर्क लौटाती है:

$\operatorname {nil} \equiv \lambda n.\lambda c.\ n$

सिर के साथ गैर-खाली सूची h और पूंछ t द्वारा दिया गया है

$\operatorname {cons} \ h\ t\ \ \equiv \ \ \lambda n.\lambda c.\ c\ h\ t$

अधिक सामान्यतः $m$ विकल्पों के साथ बीजगणितीय डेटा प्रकार $m$ पैरामीटर के साथ एक फलन बन जाता है। जब iवें कंस्ट्रक्टर में $n_{i}$ तर्क होते हैं, तो एन्कोडिंग के संबंधित पैरामीटर $n_{i}$ तर्क भी लेते हैं।

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

type List = 
  C =>                    // nil argument
  (E => List => C) =>     // cons argument
  C                       // result of pattern matching

एक सूची जिसका उपयोग मनमानी प्रकारों की गणना करने के लिए किया जा सकता है, में एक प्रकार होगा जो Cसे अधिक मात्रा में होता है। E में एक सामान्य सूची भी E को प्रकार तर्क के रूप में ले जाएगा।

यह भी देखें

• लैम्ब्डा कैलकुलस
• टाइप किए गए कलन में चर्च अंकों के लिए प्रणाली एफ
• मोगेनसेन-स्कॉट एन्कोडिंग
• क्रमसूचक संख्या या वॉन न्यूमैन क्रमसूचकों की परिभाषा - प्राकृतिक संख्याओं को सांकेतिक शब्दों में बदलने का दूसरा विधि: समुच्चय के रूप में

संदर्भ

• Stump, A. (2009). "Directly reflective meta-programming" (PDF). Higher-Order Symb Comput. 22 (2): 115–144. CiteSeerX 10.1.1.489.5018. doi:10.1007/s10990-007-9022-0. S2CID 16124152.
• Cartwright, Robert. "Church numerals and booleans explained" (PDF). Comp 311 — Review 2. Rice University.
• Kemp, Colin (2007). "§2.4.1 Church Naturals, §2.4.2 Church Booleans, Ch. 5 Derivation techniques for TFP". Theoretical Foundations for Practical 'Totally Functional Programming' (PhD). School of Information Technology and Electrical Engineering, The University of Queensland. pp. 14–17, 93–145. CiteSeerX 10.1.1.149.3505. All about Church and other similar encodings, including how to derive them and operations on them, from first principles
• Some interactive examples of Church numerals
• Lambda Calculus Live Tutorial: Boolean Algebra