चर्च एन्कोडिंग: Difference between revisions

Revision as of 22:24, 19 May 2023

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

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

प्रयोग

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

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

चर्च अंक

चर्च अंक चर्च एन्कोडिंग के तहत प्राकृतिक संख्याओं का प्रतिनिधित्व करते हैं। प्राकृतिक संख्या 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$ ^{[lower-alpha 1]}	$\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$
पूर्वाधिकारी^{[lower-alpha 2]}	$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)$
घटाव^{[lower-alpha 2]} (मोनस)	$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:

↑ This formula is the definition of a Church numeral $n$ with $f\to m,x\to f$ .
↑ ^2.0 ^2.1
In the Church encoding,
- $\operatorname {pred} (0)=0$
- $m\leq n\to m-n=0$

पूर्ववर्ती समारोह की व्युत्पत्ति

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

\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}}

विभाग

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

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

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

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

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

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

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

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

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

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

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

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} and true false & = (λ p . λ q . p q p) true false = true false true = (λ a . λ b . a) false true = false \\ or true false & = (λ p . λ q . p p q) (λ a . λ b . a) (λ a . λ b . b) = (λ a . λ b . a) (λ a . λ b . a) (λ a . λ b . b) = (λ a . λ b . a) = true \\ {not}_{1} true & = (λ p . λ a . λ b . p b a) (λ a . λ b . a) = λ a . λ b . (λ a . λ b . a) b a = λ a . λ b . (λ c . b) a = λ a . λ \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)

चर्च जोड़े

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

{\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}}

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

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

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

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

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

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

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

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

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

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

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

अभिव्यक्ति	विवरण
$\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)$	दूसरा.दूसराअंतिम भाग है।

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

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

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

{\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}}

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

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

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

इस दृष्टिकोण में, हम इस तथ्य का उपयोग करते हैं कि पैटर्न मिलान अभिव्यक्ति का उपयोग करके सूचियों को देखा जा सकता है। उदाहरण के लिए, स्काला (प्रोग्रामिंग भाषा) नोटेशन का उपयोग करना, यदि list प्रकार के मान को दर्शाता है List खाली सूची के साथ Nil और कंस्ट्रक्टर Cons(h, t) हम सूची का निरीक्षण कर सकते हैं और गणना कर सकते हैं 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}

आइए हम द्वारा निरूपित करें n के अनुरूप पैरामीटर nilCode और तक c के अनुरूप पैरामीटर consCode.

खाली सूची वह है जो शून्य तर्क लौटाती है:

\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}$ तर्क भी।

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

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

एक सूची जिसका उपयोग मनमानी प्रकारों की गणना करने के लिए किया जा सकता है, में एक प्रकार होगा जो मात्रा निर्धारित करता है C. एक सूची सामान्य^{[clarification needed]} में E भी ले जाएगा E प्रकार तर्क के रूप में।

यह भी देखें

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

संदर्भ

↑ ^1.0 ^1.1 ^1.2 Trancón y Widemann, Baltasar; Parnas, David Lorge (2008). "सारणीबद्ध भाव और कुल कार्यात्मक प्रोग्रामिंग". Implementation and Application of Functional Languages. Lecture Notes in Computer Science. 5083: 228–229. doi:10.1007/978-3-540-85373-2_13. ISBN 978-3-540-85372-5.
↑ Jansen, Jan Martin; Koopman, Pieter W. M.; Plasmeijer, Marinus J. (2006). "Efficient interpretation by transforming data types and patterns to functions". In Nilsson, Henrik (ed.). Trends in functional programming. Volume 7. Bristol: Intellect. pp. 73–90. CiteSeerX 10.1.1.73.9841. ISBN 978-1-84150-188-8.
↑ "Predecessor and lists are not representable in simply typed lambda calculus". Lambda Calculus and Lambda Calculators. okmij.org.
↑ Allison, Lloyd. "Lambda Calculus Integers".
↑ Bauer, Andrej. "Andrej's answer to a question; "Representing negative and complex numbers using lambda calculus"".
↑ "Exact real arithmetic". Haskell. Archived from the original on 2015-03-26.
↑ Bauer, Andrej (26 September 2022). "Real number computational software". GitHub.
↑ Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press. p. 500. ISBN 978-0-262-16209-8.
↑ Tromp, John (2007). "14. Binary Lambda Calculus and Combinatory Logic". In Calude, Cristian S (ed.). यादृच्छिकता और जटिलता, लीबनिज से चैतिन तक. World Scientific. pp. 237–262. ISBN 978-981-4474-39-9.
As PDF: Tromp, John (14 May 2014). "Binary Lambda Calculus and Combinatory Logic" (PDF). Retrieved 2017-11-24.
↑ Jansen, Jan Martin (2013). "Programming in the λ-Calculus: From Church to Scott and Back". In Achten, Peter; Koopman, Pieter W. M. (eds.). The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday. Lecture Notes in Computer Science. Vol. 8106. Springer. pp. 168–180. doi:10.1007/978-3-642-40355-2_12.

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

[Church_numeral_definition-4] This formula is the definition of a Church numeral $n$ with $f\to m,x\to f$ .

[ce-5] 2.0 ^2.1 In the Church encoding,
$\operatorname {pred} (0)=0$

$m\leq n\to m-n=0$

[3] $\operatorname {pred} (0)=0$

[4] $m\leq n\to m-n=0$

[Widemann-1] 1.0 ^1.1 ^1.2 Trancón y Widemann, Baltasar; Parnas, David Lorge (2008). "सारणीबद्ध भाव और कुल कार्यात्मक प्रोग्रामिंग". Implementation and Application of Functional Languages. Lecture Notes in Computer Science. 5083: 228–229. doi:10.1007/978-3-540-85373-2_13. ISBN 978-3-540-85372-5.

[2] Jansen, Jan Martin; Koopman, Pieter W. M.; Plasmeijer, Marinus J. (2006). "Efficient interpretation by transforming data types and patterns to functions". In Nilsson, Henrik (ed.). Trends in functional programming. Volume 7. Bristol: Intellect. pp. 73–90. CiteSeerX 10.1.1.73.9841. ISBN 978-1-84150-188-8.

[3] "Predecessor and lists are not representable in simply typed lambda calculus". Lambda Calculus and Lambda Calculators. okmij.org.

[6] Allison, Lloyd. "Lambda Calculus Integers".

[7] Bauer, Andrej. "Andrej's answer to a question; "Representing negative and complex numbers using lambda calculus"".

[8] "Exact real arithmetic". Haskell. Archived from the original on 2015-03-26.

[9] Bauer, Andrej (26 September 2022). "Real number computational software". GitHub.

[10] Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press. p. 500. ISBN 978-0-262-16209-8.

[11] Tromp, John (2007). "14. Binary Lambda Calculus and Combinatory Logic". In Calude, Cristian S (ed.). यादृच्छिकता और जटिलता, लीबनिज से चैतिन तक. World Scientific. pp. 237–262. ISBN 978-981-4474-39-9.
As PDF: Tromp, John (14 May 2014). "Binary Lambda Calculus and Combinatory Logic" (PDF). Retrieved 2017-11-24.

[12] Jansen, Jan Martin (2013). "Programming in the λ-Calculus: From Church to Scott and Back". In Achten, Peter; Koopman, Pieter W. M. (eds.). The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday. Lecture Notes in Computer Science. Vol. 8106. Springer. pp. 168–180. doi:10.1007/978-3-642-40355-2_12.

[1]

[2]

[3]

[lower-alpha 1]

[lower-alpha 2]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

@@ Line 45: / Line 45: @@
 : <math>\operatorname{plus} \equiv \lambda m.\lambda n.\lambda f.\lambda x. m\ f\ (n\ f\ x)</math>
-उत्तराधिकारी समारोह <math>\operatorname{succ}(n)=n+1</math> बीटा रिडक्शन या  .CE.B2-रिडक्शन|β-समतुल्य है <math>(\operatorname{plus}\ 1)</math>.
+उत्तराधिकारी समारोह <math>\operatorname{succ}(n)=n+1</math> बीटा रिडक्शन या  .सीई.बी2-रिडक्शन|β-समतुल्य है <math>(\operatorname{plus}\ 1)</math>.
 : <math>\operatorname{succ} \equiv \lambda n.\lambda f.\lambda x. f\ (n\ f\ x)</math>
@@ Line 59: / Line 59: @@
 : <math>\operatorname{pred} \equiv \lambda n.\lambda f.\lambda x. n\ (\lambda g.\lambda h. h\ (g\ f))\ (\lambda u. x)\ (\lambda u. u)</math>
-एक चर्च अंक n बार फ़ंक्शन लागू करता है। पूर्ववर्ती फ़ंक्शन को एक फ़ंक्शन वापस करना चाहिए जो इसके पैरामीटर n - 1 बार लागू करता है। यह f और x के चारों ओर एक कंटेनर बनाकर हासिल किया जाता है, जिसे इस तरह से प्रारंभ किया जाता है कि फ़ंक्शन के आवेदन को पहली बार छोड़ दिया जाता है। अधिक विस्तृत विवरण के लिए पूर्ववर्ती कार्य की  या  Derivation देखें।
+एक चर्च अंक n बार फ़ंक्शन लागू करता है। पूर्ववर्ती फ़ंक्शन को एक फ़ंक्शन वापस करना चाहिए जो इसके पैरामीटर n - 1 बार लागू करता है। यह f और x के चारों ओर एक कंटेनर बनाकर हासिल किया जाता है, जिसे इस तरह से प्रारंभ किया जाता है कि फ़ंक्शन के आवेदन को पहली बार छोड़ दिया जाता है। अधिक विस्तृत विवरण के लिए पूर्ववर्ती कार्य की  या  व्युत्पत्ति देखें।
 घटाव समारोह पूर्ववर्ती समारोह के आधार पर लिखा जा सकता है।
@@ Line 70: / Line 70: @@
 {| class="wikitable"
 |-
-! Function !! Algebra !! Identity !! Function definition
+! कार्य !! बीजगणित !! पहचान !! समारोह परिभाषा
-! colspan="2" | Lambda expressions
+! colspan="2" | लैम्ब्डा भाव
 |-
-| [[Successor function|Successor]] || <math>n + 1</math> || <math>f^{n+1}\ x = f (f^n x) </math> ||  <math>\operatorname{succ}\ n\ f\ x = f\ (n\ f\ x) </math> || <math>\lambda n.\lambda f.\lambda x.f\ (n\ f\ x) </math> || ...
+| [[Successor function|उत्तराधिकारी]] || <math>n + 1</math> || <math>f^{n+1}\ x = f (f^n x) </math> ||  <math>\operatorname{succ}\ n\ f\ x = f\ (n\ f\ x) </math> || <math>\lambda n.\lambda f.\lambda x.f\ (n\ f\ x) </math> || ...
 |-
-| [[Addition]] || <math>m + n</math> || <math>f^{m+n}\ x = f^m (f^n x) </math> || <math>\operatorname{plus}\ m\ n\ f\ x = m\ f\ (n\ f\ x) </math> || <math> \lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x) </math> || <math>\lambda m.\lambda n.n \operatorname{succ} m</math>
+| [[Addition|जोड़ना]] || <math>m + n</math> || <math>f^{m+n}\ x = f^m (f^n x) </math> || <math>\operatorname{plus}\ m\ n\ f\ x = m\ f\ (n\ f\ x) </math> || <math> \lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x) </math> || <math>\lambda m.\lambda n.n \operatorname{succ} m</math>
 |-
-| [[Multiplication]] || <math>m * n </math> || <math> f^{m*n}\ x = (f^m)^n\ x </math> ||<math>\operatorname{multiply}\ m\ n\ f\ x = m\ (n\ f) \ x </math> || <math>\lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f) \ x </math> || <math>\lambda m.\lambda n.\lambda f.m\ (n\ f) </math>
+| [[Multiplication|गुणन]] || <math>m * n </math> || <math> f^{m*n}\ x = (f^m)^n\ x </math> ||<math>\operatorname{multiply}\ m\ n\ f\ x = m\ (n\ f) \ x </math> || <math>\lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f) \ x </math> || <math>\lambda m.\lambda n.\lambda f.m\ (n\ f) </math>
 |-
-| [[Exponentiation]] || <math>m^n </math> || <math> n\ m\ f = m^n\ f </math>{{efn|name=Church numeral definition|This formula is the definition of a Church numeral {{mvar|n}} with <math>f \to m, x \to f</math>.}} ||<math>\operatorname{exp} \ m\ n\ f\ x = (n\ m)\ f\ x </math> || <math> \lambda m.\lambda n.\lambda f.\lambda x.(n\ m)\ f\ x </math> || <math> \lambda m.\lambda n.n\ m </math>
+| [[Exponentiation|घातांक]] || <math>m^n </math> || <math> n\ m\ f = m^n\ f </math>{{efn|name=Church numeral definition|This formula is the definition of a Church numeral {{mvar|n}} with <math>f \to m, x \to f</math>.}} ||<math>\operatorname{exp} \ m\ n\ f\ x = (n\ m)\ f\ x </math> || <math> \lambda m.\lambda n.\lambda f.\lambda x.(n\ m)\ f\ x </math> || <math> \lambda m.\lambda n.n\ m </math>
 |-
-| [[#Derivation of predecessor function|Predecessor]]{{efn|name=ce}} || <math>n - 1</math> || <math>\operatorname{inc}^n \operatorname{con} = \operatorname{val} (f^{n-1} x) </math> || <math>if (n == 0)\ 0\ else\ (n-1)</math>
+| [[Index.php?title=चर्च एन्कोडिंग#Derivation of पूर्वाधिकारी function|पूर्वाधिकारी]]{{efn|name=ce}} || <math>n - 1</math> || <math>\operatorname{inc}^n \operatorname{con} = \operatorname{val} (f^{n-1} x) </math> || <math>if (n == 0)\ 0\ else\ (n-1)</math>
 | colspan="2" |
 <math>\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u) </math>
 |-
-| [[Subtraction]]{{efn|name=ce}} ([[Monus]]) || <math> m - n </math> || <math>f^{m-n}\ x = (f^{-1})^n (f^{m} x)</math> || <math>\operatorname{minus}\ m\ n = (n \operatorname{pred})\ m</math>  || ... ||  <math>\lambda m.\lambda n.n \operatorname{pred} m</math>
+| [[Subtraction|घटाव]]{{efn|name=ce}} [[Subtraction|(मोनस)]]  || <math> m - n </math> || <math>f^{m-n}\ x = (f^{-1})^n (f^{m} x)</math> || <math>\operatorname{minus}\ m\ n = (n \operatorname{pred})\ m</math>  || ... ||  <math>\lambda m.\lambda n.n \operatorname{pred} m</math>
 |}
@@ Line 415: / Line 415: @@
 == चर्च जोड़े ==
-{{see also|Cons}}
+{{see also|दोष}}
 चर्च जोड़े विपक्ष (दो-टुपल) प्रकार के चर्च एन्कोडिंग हैं। जोड़ी को एक फ़ंक्शन के रूप में दर्शाया गया है जो फ़ंक्शन तर्क लेता है। जब इसका तर्क दिया जाता है तो यह तर्क जोड़ी के दो घटकों पर लागू होगा। लैम्ब्डा कैलकुस में परिभाषा है,
@@ Line 441: / Line 441: @@
 {| class="wikitable"
 |-
-! Function !! Description
+! कार्य !! विवरण
 |-
-| ''nil'' || Construct an empty list.
+| ''शून्य'' || एक खाली सूची बनाएँ।
 |-
-| ''isnil'' || Test if list is empty.
+| ''इस्निल'' || सूची खाली होने पर परीक्षण करें।
 |-
-| ''cons'' || Prepend a given value to a (possibly empty) list.
+| ''दोष'' || किसी दिए गए मान को (संभवतः खाली) सूची में जोड़ें।
 |-
-| ''head'' || Get the first element of the list.
+| ''शीर्ष'' || सूची का पहला तत्व प्राप्त करें।
 |-
-| ''tail'' || Get the rest of the list.
+| ''अंतिम भाग'' || बाकी सूची प्राप्त करें।
 |}
 हम नीचे सूचियों के चार अलग-अलग प्रतिनिधित्व देते हैं:
@@ Line 482: / Line 482: @@
 {| class="wikitable"
 |-
-! Expression !! Description
+! अभिव्यक्ति !! विवरण
 |-
 | <math> \operatorname{nil} \equiv \operatorname{pair}\ \operatorname{true}\ \operatorname{true} </math>
-| The first element of the pair is ''true'' meaning the list is null.
+| जोड़ी का पहला तत्व सत्य है जिसका अर्थ है कि सूची शून्य है।
 |-
 | <math> \operatorname{isnil} \equiv \operatorname{first} </math>
-| Retrieve the null (or empty list) indicator.
+| अशक्त (या खाली सूची) सूचक को पुनः प्राप्त करें।
 |-
 | <math> \operatorname{cons}  \equiv \lambda h.\lambda t.\operatorname{pair} \operatorname{false}\  (\operatorname{pair} h\ t) </math>
-| Create a list node, which is not null, and give it a head ''h'' and a tail ''t''.
+| एक सूची नोड बनाएँ, जो शून्य नहीं है, और इसे एक हेड एच और एक टेल टी दें।
 |-
 |<math> \operatorname{head}  \equiv \lambda z.\operatorname{first}\ (\operatorname{second} z) </math>
-| ''second.first'' is the head.
+| दूसरा.पहला ''शीर्ष'' है।
 |-
 | <math> \operatorname{tail}  \equiv \lambda z.\operatorname{second}\ (\operatorname{second} z) </math>
-| ''second.second'' is the tail.
+| दूसरा.दूसरा''अंतिम भाग''  है।
 |}
 एक शून्य नोड में दूसरा कभी भी एक्सेस नहीं किया जाता है, बशर्ते कि 'सिर' और 'पूंछ' केवल गैर-खाली सूचियों पर लागू हों।
@@ Line 557: / Line 557: @@
 </math>
 आइए हम द्वारा निरूपित करें {{code|n}} के अनुरूप पैरामीटर {{code|nilCode}} और तक {{code|c}} के अनुरूप पैरामीटर {{code|consCode}}.
 खाली सूची वह है जो शून्य तर्क लौटाती है:
 : <math>

v t e Alonzo Church
Notable ideas	Lambda calculus Simply typed lambda calculus Church–Turing thesis Church encoding Frege–Church ontology Church–Rosser theorem
Students	Alan Turing C. Anthony Anderson Peter Andrews George Alfred Barnard William Boone Martin Davis William Easton Alfred Foster Leon Henkin John George Kemeny Stephen Cole Kleene Simon B. Kochen Maurice L'Abbé Isaac Malitz Gary R. Mar Michael O. Rabin Nicholas Rescher Hartley Rogers, Jr J. Barkley Rosser Dana Scott Norman Shapiro Raymond Smullyan
Institutions	Princeton University University of California, Los Angeles
Family	Alonzo Church (college president) A. C. Croom

Anonymous

Search

चर्च एन्कोडिंग: Difference between revisions

Namespaces

More

Page actions

Revision as of 22:24, 19 May 2023

Contents

प्रयोग

चर्च अंक

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

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

पूर्ववर्ती समारोह की व्युत्पत्ति

वैल्यू कंटेनर

निकालें

स्थिरांक

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

विभाग

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

प्लस और माइनस

गुणा और भाग

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

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

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

विधेय

चर्च जोड़े

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

यह भी देखें

संदर्भ

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

चर्च एन्कोडिंग: Difference between revisions

Revision as of 22:24, 19 May 2023

प्रयोग

चर्च अंक

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

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

पूर्ववर्ती समारोह की व्युत्पत्ति

वैल्यू कंटेनर

निकालें

स्थिरांक

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

विभाग

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

प्लस और माइनस

गुणा और भाग

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

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

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

विधेय

चर्च जोड़े

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

यह भी देखें

संदर्भ

Navigation

Wiki tools

Page tools

Other projects

Categories