Church encoding
ગણિતમાં, ચર્ચ એન્કોડિંગ એ લેમ્બડા કલનમાં માહિતી અને સંચાલકોનું પ્રતિનિધિત્વ કરવાનું એક સાધન છે. ચર્ચના અંકો લેમ્બડા નોટેશનનો ઉપયોગ કરીને કુદરતી સંખ્યાઓનું પ્રતિનિધિત્વ કરે છે. આ પદ્ધતિને અલોન્ઝો ચર્ચ માટે નામ આપવામાં આવ્યું છે, જેમણે આ રીતે લેમ્બડા કલનમાં માહિતીને સૌપ્રથમ એન્કોડ કરી હતી. જે શબ્દોને સામાન્ય રીતે અન્ય સંકેતોમાં આદિમ માનવામાં આવે છે (જેમ કે પૂર્ણાંકો, બુલિયન, જોડીઓ, યાદીઓ અને ટેગ કરેલા યુનિયનો) તેને ચર્ચ એન્કોડિંગ હેઠળ ઉચ્ચ ક્રમના કાર્યોમાં મેપ કરવામાં આવે છે. ચર્ચ-ટ્યુરિંગ થીસીસ ભારપૂર્વક જણાવે છે કે કોઈપણ ગણતરીપાત્ર સંચાલક (અને તેના ઓપરેન્ડ્સ) ને ચર્ચ એન્કોડિંગ હેઠળ રજૂ કરી શકાય છે. અનટાઈપ્ડ લેમ્બડા કેલ્ક્યુલસમાં એકમાત્ર પ્રિમિટિવ ડેટા પ્રકાર ફંક્શન છે. ચર્ચ એન્કોડિંગનું સીધું અમલીકરણ કેટલીક ઍક્સેસ કામગીરીને ધીમું કરે છે, જ્યાં ડેટા સ્ટ્રક્ચરનું કદ છે, જે ચર્ચ એન્કોડિંગને અવ્યવહારુ બનાવે છે. સંશોધનોએ દર્શાવ્યું છે કે આને લક્ષિત ઓપ્ટિમાઇઝેશન દ્વારા સંબોધિત કરી શકાય છે, પરંતુ મોટાભાગની કાર્યાત્મક પ્રોગ્રામિંગ ભાષાઓ તેના બદલે બીજગણિત ડેટા પ્રકારોને સમાવવા માટે તેમની મધ્યવર્તી રજૂઆતને વિસ્તૃત કરે છે. તેમ છતાં ચર્ચ એન્કોડિંગનો ઉપયોગ ઘણીવાર સૈદ્ધાંતિક દલીલોમાં થાય છે, કારણ કે તે આંશિક મૂલ્યાંકન અને પ્રમેય સાબિત કરવા માટે કુદરતી રજૂઆત છે. ઓપરેશન્સને ઉચ્ચ ક્રમાંકિત પ્રકારોનો ઉપયોગ કરીને લખી શકાય છે, અને આદિમ પુનરાવર્તન સરળતાથી સુલભ છે. એવી ધારણા કે કાર્યો એકમાત્ર આદિમ ડેટા પ્રકારો છે જે ઘણા પુરાવાઓને સુવ્યવસ્થિત કરે છે. ચર્ચ એન્કોડિંગ સંપૂર્ણ છે પરંતુ માત્ર પ્રતિનિધિત્વાત્મક છે. પ્રતિનિધિત્વને સામાન્ય ડેટા પ્રકારોમાં અનુવાદિત કરવા માટે, લોકોને પ્રદર્શિત કરવા માટે વધારાના કાર્યોની જરૂર છે. ચર્ચના પ્રમેયમાંથી સમાનતાની અનિશ્ચિતતાને કારણે બે કાર્યો વિસ્તૃત રીતે સમાન છે કે નહીં તે નક્કી કરવું સામાન્ય રીતે શક્ય નથી. અનુવાદ કાર્યને તે રજૂ કરે છે તે મૂલ્યને પુનઃપ્રાપ્ત કરવા માટે કોઈ રીતે લાગુ કરી શકે છે, અથવા તેના મૂલ્યને શાબ્દિક લેમ્બડા શબ્દ તરીકે જોઈ શકે છે. લામ્બડા કલનને સામાન્ય રીતે સઘન સમાનતાનો ઉપયોગ તરીકે અર્થઘટન કરવામાં આવે છે. સમાનતાની સઘન અને વિસ્તૃત વ્યાખ્યા વચ્ચેના તફાવતને કારણે પરિણામોના અર્થઘટનમાં સંભવિત સમસ્યાઓ છે. ચર્ચ અંકો એ ચર્ચ એન્કોડિંગ હેઠળ કુદરતી સંખ્યાઓની રજૂઆત છે. ઉચ્ચ ક્રમનું વિધેય કે જે કુદરતી સંખ્યા n નું પ્રતિનિધિત્વ કરે છે તે એક એવું વિધેય છે જે કોઈપણ વિધેયને તેની n-ગણો રચના સાથે મેળવે છે. સરળ શબ્દોમાં કહીએ તો, આંકડાનું "મૂલ્ય" એ કાર્ય તેની દલીલને કેટલી વાર સમાવી લે છે તેની સમકક્ષ છે. બધા ચર્ચ અંકો એવા કાર્યો છે જે બે પરિમાણો લે છે. ચર્ચના અંકો 0,1,2, ને લેમ્બડા કલનમાં નીચે પ્રમાણે વ્યાખ્યાયિત કરવામાં આવ્યા છે. 0 થી શરૂ કરીને કાર્યને બિલકુલ લાગુ ન કરો, 1 કાર્યને એકવાર લાગુ કરો, 2 કાર્યને બે વાર લાગુ કરો, 3 કાર્યને ત્રણ વખત લાગુ કરો, વગેરે સાથે આગળ વધો. : ચર્ચ અંક 3 કોઈ પણ કાર્યને મૂલ્ય પર ત્રણ વખત લાગુ કરવાની ક્રિયાને રજૂ કરે છે. પૂરી પાડવામાં આવેલ કાર્ય પહેલા પૂરી પાડવામાં આવેલ પરિમાણ પર લાગુ કરવામાં આવે છે અને પછી ક્રમિક રીતે તેના પોતાના પરિણામ પર લાગુ કરવામાં આવે છે. અંતિમ પરિણામ અંક 3 નથી (જ્યાં સુધી પૂરું પાડવામાં આવેલ પરિમાણ 0 ન હોય અને કાર્ય અનુગામી કાર્ય ન હોય). કાર્ય પોતે જ, અને તેનું અંતિમ પરિણામ નહીં, તે ચર્ચ અંક 3 છે. ચર્ચ નંબર 3 નો અર્થ ફક્ત ત્રણ વખત કંઈપણ કરવું. તે "ત્રણ વખત" નો અર્થ શું છે તેનું એક દેખીતું પ્રદર્શન છે. ચર્ચ અંકો સાથેની ગણતરી સંખ્યાઓ પરની અંકગણિત કામગીરીને ચર્ચ અંકો પરના કાર્યો દ્વારા રજૂ કરી શકાય છે. આ કાર્યોને લેમ્બડા કલનમાં વ્યાખ્યાયિત કરી શકાય છે, અથવા મોટાભાગની કાર્યાત્મક પ્રોગ્રામિંગ ભાષાઓમાં લાગુ કરી શકાય છે (લેમ્બડા અભિવ્યક્તિઓને કાર્યોમાં રૂપાંતરિત કરતા જુઓ). એડિશન ફંક્શન ઓળખનો ઉપયોગ કરે છે. અનુગામી કાર્ય β-સમાન છે. ગુણાકાર કાર્ય ઓળખનો ઉપયોગ કરે છે. ઘાતાંક કાર્ય ચર્ચ અંકોની વ્યાખ્યા દ્વારા આપવામાં આવે છે. વ્યાખ્યામાં મેળવવાનો વિકલ્પ અને, જે લેમ્બડા અભિવ્યક્તિ આપે છે, કાર્યને સમજવું વધુ મુશ્કેલ છે. ચર્ચ અંક એ કાર્યને n વખત લાગુ કરે છે. પુરોગામી વિધેયે તેના પરિમાણ n-1 વખત લાગુ કરતું વિધેય પાછું આપવું આવશ્યક છે. આ f અને x ની આસપાસ કન્ટેનર બનાવીને પ્રાપ્ત થાય છે, જે એવી રીતે શરૂ કરવામાં આવે છે કે જે પ્રથમ વખત કાર્યના ઉપયોગને અવગણે છે. વધુ વિગતવાર સમજૂતી માટે પુરોગામી જુઓ. બાદબાકી કાર્ય પૂર્વવર્તી કાર્યના આધારે લખી શકાય છે. ચર્ચ અંકો પરના કાર્યોનું કોષ્ટક પૂર્વવર્તી કાર્યની વ્યુત્પત્તિ ચર્ચ એન્કોડિંગમાં વપરાતું પૂર્વવર્તી કાર્ય છે,. પુરોગામી બનાવવા માટે આપણે ફંક્શન 1 ઓછા સમયમાં લાગુ કરવાની રીતની જરૂર છે. આંકડાનો ઉપયોગ કાર્યના સમયને લાગુ પડે છે. પૂર્વવર્તી વિધેયે વિધેય સમય લાગુ કરવા માટે આંકડાનો ઉપયોગ કરવો આવશ્યક છે. પૂર્વવર્તી કાર્યને અમલમાં મૂકતા પહેલા, અહીં એક યોજના છે જે મૂલ્યને કન્ટેનર કાર્યમાં લપેટી લે છે. આપણે 'અને' ની જગ્યાએ 'અને' તરીકે ઓળખાતા નવા કાર્યોને વ્યાખ્યાયિત કરીશું. કન્ટેનર કાર્ય કહેવાય છે. કોષ્ટકની ડાબી બાજુ અને પર લાગુ કરાયેલ અંક દર્શાવે છે. સામાન્ય પુનરાવૃત્તિનો નિયમ છે, જો કન્ટેનર (કહેવાય છે) માંથી મૂલ્ય પુનઃપ્રાપ્ત કરવા માટે પણ કોઈ કાર્ય હોય, તો પછી કાર્યને વ્યાખ્યાયિત કરવા માટે તેનો ઉપયોગ કરી શકાય છે, કાર્ય આંતરિક રીતે ઉપયોગી નથી. જો કે, પ્રતિનિધિઓ તેની કન્ટેનર દલીલને બોલાવતા હોવાથી, આપણે વ્યવસ્થા કરી શકીએ છીએ કે પ્રથમ અરજી પર એક વિશેષ કન્ટેનર પ્રાપ્ત થાય છે જે તેની દલીલની અવગણના કરે છે જે તેની પ્રથમ અરજીને અવગણવાની મંજૂરી આપે છે. આ નવા પ્રારંભિક કન્ટેનરને કૉલ કરો. ઉપરના કોષ્ટકની જમણી બાજુ તેના વિસ્તરણ દર્શાવે છે. પછી કાર્ય માટે અભિવ્યક્તિમાં બદલીને આપણે પુરોગામી કાર્ય મેળવીએ છીએ, જેમ કે કાર્યોની નીચે સમજાવાયેલ છે,,,, અને તેને આ રીતે વ્યાખ્યાયિત કરી શકાય છે, જે લેમ્બડા અભિવ્યક્તિ આપે છે, પ્રિડ પ્રિડને વ્યાખ્યાયિત કરવાની બીજી રીત પણ જોડીનો ઉપયોગ કરીને વ્યાખ્યાયિત કરી શકાય છેઃ આ એક સરળ વ્યાખ્યા છે, પરંતુ પ્રિડ માટે વધુ જટિલ અભિવ્યક્તિ તરફ દોરી જાય છે. આના માટે વિસ્તરણઃ કુદરતી સંખ્યાઓનો વિભાજન વિભાગ આના દ્વારા અમલમાં મૂકી શકાય છે, ગણતરી ઘણા બીટા ઘટાડા લે છે. જ્યાં સુધી હાથથી ઘટાડો કરવામાં ન આવે ત્યાં સુધી, તેનાથી બહુ ફરક પડતો નથી, પરંતુ આ ગણતરી બે વાર ન કરવી તે વધુ સારું છે. પરીક્ષણ સંખ્યાઓ માટે સૌથી સરળ આગાહી IsZero છે તેથી શરતને ધ્યાનમાં લો. પરંતુ આ શરત સમકક્ષ છે, નહીં. જો આ અભિવ્યક્તિનો ઉપયોગ કરવામાં આવે તો ઉપર આપેલી વિભાજનની ગાણિતિક વ્યાખ્યાને ચર્ચ અંકો પરના કાર્યમાં અનુવાદિત કરવામાં આવે છે, જેમ કે ઇચ્છા મુજબ, આ વ્યાખ્યામાં એક જ કૉલ છે. જો કે પરિણામ એ છે કે આ સૂત્ર નું મૂલ્ય આપે છે. આ સમસ્યાને વિભાજીત કરતા પહેલા 1 થી n ઉમેરીને સુધારી શકાય છે. વિભાજનની વ્યાખ્યા એ છે કે, વિભાજન 1 એ પુનરાવર્તિત વ્યાખ્યા છે. વાય સંયોજકનો ઉપયોગ પુનરાવર્તનને અમલમાં મૂકવા માટે થઈ શકે છે. જમણી બાજુએ મેળવવા માટે, પછી, જ્યાં, આપે છે, અથવા લખાણ તરીકે,\for નો ઉપયોગ કરીને, ભાગ = (\n. ((\f. (\x. xx) (\x. f (xx))) (\c. \n. \m. \f. \x. (\d. (\n. n (\x. (\a. \b. b)) (\a. \b. a)) d (((\f. \x. x) fx) (f (cdm. \n. n (\n. \f. \x. n (\g. \h. h (gf)) (\u. x) (\u. x) m) nm) ((\n. \f. \x. \x.)) ((\n. f (n f x)) n)) ઉદાહરણ તરીકે, 9/3 ને ભાગાકાર (\f. \x. f (f (f (f (f (f (f (f x))))))) (\f. \x. f (f (f (f x)))) દ્વારા રજૂ કરવામાં આવે છે. \f. \x. f (f (f (x))) સહી કરેલી સંખ્યાઓ ચર્ચની સંખ્યાઓને સહી કરેલી સંખ્યાઓ સુધી લંબાવવાનો એક સરળ અભિગમ ચર્ચ જોડીનો ઉપયોગ કરવાનો છે, જેમાં ચર્ચની સંખ્યાઓ હકારાત્મક અને નકારાત્મક મૂલ્યનું પ્રતિનિધિત્વ કરે છે. પૂર્ણાંક મૂલ્ય એ બે ચર્ચ અંકો વચ્ચેનો તફાવત છે. કુદરતી સંખ્યાને હસ્તાક્ષરિત સંખ્યામાં રૂપાંતરિત કરવામાં આવે છે, નકારાત્મક મૂલ્યોની અદલાબદલી કરીને કરવામાં આવે છે. જો જોડીમાંથી એક શૂન્ય હોય તો પૂર્ણાંક મૂલ્ય વધુ કુદરતી રીતે રજૂ થાય છે. વન ઝીરો ફંક્શન આ શરત હાંસલ કરે છે, પુનરાવર્તન વાય સંયોજકનો ઉપયોગ કરીને અમલમાં મૂકી શકાય છે, પ્લસ અને માઇનસ એડિશનને જોડી પર ગાણિતિક રીતે વ્યાખ્યાયિત કરવામાં આવે છે, છેલ્લી અભિવ્યક્તિને લેમ્બડા કેલ્ક્યુલસમાં આ રીતે અનુવાદિત કરવામાં આવે છે, તેવી જ રીતે બાદબાકીને વ્યાખ્યાયિત કરવામાં આવે છે, આપીને, ગુણાકાર કરો અને ગુણાકારને વિભાજીત કરો દ્વારા વ્યાખ્યાયિત કરી શકાય છે, છેલ્લી અભિવ્યક્તિને લેમ્બડા કેલ્ક્યુલસમાં અનુવાદિત કરવામાં આવે છે, વિભાજન માટે અહીં સમાન વ્યાખ્યા આપવામાં આવી છે, આ વ્યાખ્યા સિવાય, દરેક જોડીમાં એક મૂલ્ય શૂન્ય હોવું જોઈએ (ઉપર વનઝીરો જુઓ). ડિવઝેડ ફંક્શન આપણને શૂન્ય ઘટક ધરાવતા મૂલ્યને અવગણવાની મંજૂરી આપે છે. પછી ડિવીઝેડનો ઉપયોગ નીચેના સૂત્રમાં થાય છે, જે ગુણાકાર માટે સમાન છે, પરંતુ મલ્ટીને ડિવીઝેડ દ્વારા બદલવામાં આવે છે. તર્કસંગત અને વાસ્તવિક સંખ્યાઓ તર્કસંગત અને ગણતરીપાત્ર વાસ્તવિક સંખ્યાઓને પણ લેમ્બડા કલનમાં એન્કોડ કરી શકાય છે. તર્કસંગત સંખ્યાઓને હસ્તાક્ષરિત સંખ્યાઓની જોડી તરીકે એન્કોડ કરી શકાય છે. કોમ્પ્યુટેબલ વાસ્તવિક સંખ્યાઓને મર્યાદિત પ્રક્રિયા દ્વારા એન્કોડ કરી શકાય છે જે બાંયધરી આપે છે કે વાસ્તવિક મૂલ્યથી તફાવત એક સંખ્યા દ્વારા અલગ પડે છે જે આપણને જરૂર હોય તેટલી નાની બનાવી શકાય છે. આપવામાં આવેલા સંદર્ભો એવા સોફ્ટવેરનું વર્ણન કરે છે જે સિદ્ધાંતમાં લેમ્બડા કલનમાં અનુવાદિત થઈ શકે છે. એકવાર વાસ્તવિક સંખ્યાઓ વ્યાખ્યાયિત થઈ જાય પછી, જટિલ સંખ્યાઓ કુદરતી રીતે વાસ્તવિક સંખ્યાઓની જોડી તરીકે એન્કોડ કરવામાં આવે છે. ઉપર વર્ણવેલ ડેટા પ્રકારો અને કાર્યો દર્શાવે છે કે કોઈપણ ડેટા પ્રકાર અથવા ગણતરીને લેમ્બડા કલનમાં એન્કોડ કરી શકાય છે. આ ચર્ચ-ટ્યુરિંગ થીસીસ છે. અન્ય રજૂઆતો સાથે અનુવાદ મોટાભાગની વાસ્તવિક-વિશ્વની ભાષાઓ મશીન-મૂળ પૂર્ણાંકો માટે આધાર ધરાવે છે; ચર્ચ અને અનચર્ચ કાર્યો બિન-નકારાત્મક પૂર્ણાંકો અને તેમના અનુરૂપ ચર્ચ અંકો વચ્ચે રૂપાંતરિત થાય છે. વિધેયો અહીં હાસ્કેલમાં આપવામાં આવ્યા છે, જ્યાં λ લંબડા કલનની λ ને અનુરૂપ છે. અન્ય ભાષાઓમાં અમલીકરણ સમાન છે. પ્રકાર ચર્ચ a = (a-> a)-> a-> એક ચર્ચઃઃ પૂર્ણાંક-> ચર્ચ પૂર્ણાંક ચર્ચ 0 = \f-> \x-> x ચર્ચ n = \f-> \x-> f (ચર્ચ (n-1) f x) અનચર્ચઃઃ ચર્ચ પૂર્ણાંક-> પૂર્ણાંક અનચર્ચ cn = cn (+ 1) 0 ચર્ચ બુલિયન્સ ચર્ચ બુલિયન્સ એ બૂલિયન મૂલ્યોના સાચા અને ખોટા ચર્ચ એન્કોડિંગ છે. કેટલીક પ્રોગ્રામિંગ ભાષાઓ બુલિયન અંકગણિત માટે અમલીકરણ નમૂના તરીકે આનો ઉપયોગ કરે છે; ઉદાહરણ તરીકે સ્મોલટૉક અને પિકો છે. બુલિયન તર્કને પસંદગી તરીકે ગણી શકાય. સાચું અને ખોટું ચર્ચ એન્કોડિંગ બે પરિમાણોના કાર્યો છેઃ સાચું પ્રથમ પરિમાણ પસંદ કરે છે. ફોલ્સ બીજા પરિમાણને પસંદ કરે છે. બે વ્યાખ્યાઓ ચર્ચ બુલિયન્સ તરીકે ઓળખાય છેઃ આ વ્યાખ્યા આગાહીઓને મંજૂરી આપે છે (એટલે કે. લોજિકલ મૂલ્યો પરત કરતા કાર્યો) સીધા આઇએફ-ક્લોઝ તરીકે કાર્ય કરે છે. બૂલિયન પરત કરતું વિધેય, જે પછી બે પરિમાણો પર લાગુ થાય છે, તે પ્રથમ અથવા બીજા પરિમાણને પરત કરે છેઃ જો વિધેય-x સાચું હોવાનું મૂલ્યાંકન કરે તો પછી-કલમનું મૂલ્યાંકન કરે છે, અને જો વિધેય-x ખોટું હોવાનું મૂલ્યાંકન કરે તો અન્ય-કલમનું મૂલ્યાંકન કરે છે. કારણ કે સાચું અને ખોટું પ્રથમ કે બીજું પરિમાણ પસંદ કરે છે, તેઓ તર્ક ઓપરેટરો પ્રદાન કરવા માટે જોડાઈ શકે છે. નોંધ લો કે 'ના' ના બહુવિધ સંભવિત અમલીકરણ છે. કેટલાક ઉદાહરણોઃ પ્રિડિકેટ એ એક વિધેય છે જે બુલિયન મૂલ્ય આપે છે. સૌથી મૂળભૂત આગાહી એ છે કે, જો તેની દલીલ ચર્ચની સંખ્યા હોય અને જો તેની દલીલ કોઈ અન્ય ચર્ચની સંખ્યા હોય તો તે પરત કરે છેઃ નીચેની આગાહી પરીક્ષણ કરે છે કે શું પ્રથમ દલીલ બીજા કરતા ઓછી અથવા સમાન છેઃ, ઓળખને કારણે, સમાનતા માટેની કસોટીને અમલમાં મૂકી શકાય છે કારણ કે, ચર્ચ જોડી ચર્ચ જોડી એ જોડી (બે-ટુપલ) પ્રકારનું ચર્ચ એન્કોડિંગ છે. જોડી એક કાર્ય તરીકે રજૂ થાય છે જે કાર્ય દલીલ લે છે. જ્યારે તેની દલીલ આપવામાં આવે ત્યારે તે દલીલને જોડીના બે ઘટકો પર લાગુ કરશે. લેમ્બડા કલનની વ્યાખ્યા છે, ઉદાહરણ તરીકે, સૂચિ સંકેતલિપી સૂચિ ગાંઠોમાંથી એક (અપરિવર્તનીય) સૂચિ બનાવવામાં આવે છે. સૂચિ પરની મૂળભૂત કામગીરીઓ છે; અમે નીચે સૂચિની ચાર જુદી જુદી રજૂઆતો આપીએ છીએઃ બે જોડીમાંથી દરેક સૂચિ નોડ બનાવો (ખાલી સૂચિને મંજૂરી આપવા માટે). એક જોડીમાંથી દરેક સૂચિ નોડ બનાવો. જમણા ફોલ્ડ ફંક્શનનો ઉપયોગ કરીને સૂચિનું પ્રતિનિધિત્વ કરો. સ્કોટના એન્કોડિંગનો ઉપયોગ કરીને સૂચિનું પ્રતિનિધિત્વ કરો જે મેળના અભિવ્યક્તિના કિસ્સાઓને દલીલો તરીકે લે છે સૂચિ નોડ તરીકે બે જોડી ચર્ચ જોડી દ્વારા બિન-ખાલી સૂચિ અમલમાં મૂકી શકાય છે; પ્રથમ વડા ધરાવે છે. બીજામાં પૂંછડી હોય છે. જો કે આ ખાલી સૂચિનું પ્રતિનિધિત્વ આપતું નથી, કારણ કે ત્યાં કોઈ "નલ" નિર્દેશક નથી. નલને રજૂ કરવા માટે, જોડી અન્ય જોડીમાં લપેટી શકાય છે, જે ત્રણ મૂલ્યો આપે છેઃ પ્રથમ-નલ પોઇન્ટર (ખાલી સૂચિ). Second.First હેડ ધરાવે છે. Second.Second એ પૂંછડી ધરાવે છે. આ વિચારનો ઉપયોગ કરીને મૂળભૂત સૂચિ કામગીરીઓને આ રીતે વ્યાખ્યાયિત કરી શકાય છેઃ શૂન્ય નોડમાં સેકન્ડનો ક્યારેય ઉપયોગ થતો નથી, જો કે હેડ અને પૂંછડી માત્ર ખાલી ન હોય તેવી સૂચિ પર જ લાગુ થાય છે. સૂચિ નોડ તરીકે એક જોડી વૈકલ્પિક રીતે, વ્યાખ્યાયિત કરો કે છેલ્લી વ્યાખ્યા સામાન્યનો એક વિશેષ કેસ ક્યાં છે જમણી બાજુનો ઉપયોગ કરીને સૂચિનું પ્રતિનિધિત્વ કરો ચર્ચ જોડીનો ઉપયોગ કરીને એન્કોડિંગના વિકલ્પ તરીકે, સૂચિને તેના જમણી બાજુના કાર્ય સાથે ઓળખીને એન્કોડ કરી શકાય છે. ઉદાહરણ તરીકે, ત્રણ ઘટકો x, y અને z ની સૂચિને ઉચ્ચ ક્રમના કાર્ય દ્વારા એન્કોડ કરી શકાય છે જે જ્યારે સંયોજક c પર લાગુ થાય છે અને n મૂલ્ય c x (c y (c z n)) આપે છે. આ સૂચિ રજૂઆતને સિસ્ટમ એફમાં પ્રકાર આપી શકાય છે. સ્કોટ એન્કોડિંગનો ઉપયોગ કરીને સૂચિનું પ્રતિનિધિત્વ કરો વૈકલ્પિક રજૂઆત સ્કોટ એન્કોડિંગ છે, જે સાતત્યના વિચારનો ઉપયોગ કરે છે અને સરળ કોડ તરફ દોરી શકે છે. (મોગેનસન-સ્કોટ એન્કોડિંગ પણ જુઓ). આ અભિગમમાં, આપણે એ હકીકતનો ઉપયોગ કરીએ છીએ કે પેટર્ન મેચિંગ એક્સપ્રેશનનો ઉપયોગ કરીને સૂચિઓનું નિરીક્ષણ કરી શકાય છે. ઉદાહરણ તરીકે, સ્કેલા નોટેશનનો ઉપયોગ કરીને, જો સૂચિ ખાલી સૂચિ નીલ અને કન્સ્ટ્રક્ટર વિપક્ષ (એચ, ટી) સાથે પ્રકાર સૂચિનું મૂલ્ય સૂચવે છે, તો આપણે સૂચિનું નિરીક્ષણ કરી શકીએ છીએ અને જો સૂચિ ખાલી હોય અને જ્યારે સૂચિ ખાલી ન હોય ત્યારે નિલકોડની ગણતરી કરી શકીએ છીએઃ સૂચિ મેળ ખાય છે {કેસ નિલ => નિલકોડ કેસ વિપક્ષ (એચ, ટી) => કોન્સકોડ (એચ, ટી)} તે કેવી રીતે કાર્ય કરે છે અને તેના દ્વારા આપવામાં આવે છે. તેથી આપણે સૂચિને એવા કાર્ય તરીકે વ્યાખ્યાયિત કરીએ છીએ જે આવા અને દલીલોને સ્વીકારે છે, જેથી ઉપરની પેટર્ન મેળને બદલે આપણે ફક્ત લખી શકીએઃ ચાલો આપણે અનુરૂપ પરિમાણ દ્વારા અને અનુરૂપ પરિમાણ દ્વારા સૂચવીએ. ખાલી સૂચિ તે છે જે શૂન્ય દલીલ આપે છેઃ માથા અને પૂંછડી સાથેની બિન-ખાલી સૂચિ દ્વારા આપવામાં આવે છે વધુ સામાન્ય રીતે, વિકલ્પો સાથેનો બીજગણિત ડેટા પ્રકાર પરિમાણો સાથેનું કાર્ય બની જાય છે. જ્યારે th કન્સ્ટ્રક્ટર પાસે દલીલો હોય, ત્યારે એન્કોડિંગનું અનુરૂપ પરિમાણ દલીલો પણ લે છે. સ્કોટ એન્કોડિંગ અનટાઈપ્ડ લેમ્બડા કેલ્ક્યુલસમાં કરી શકાય છે, જ્યારે પ્રકારો સાથે તેના ઉપયોગ માટે પુનરાવર્તન અને પ્રકાર બહુરૂપતા સાથે ટાઇપ સિસ્ટમની જરૂર પડે છે. આ રજૂઆતમાં તત્વ પ્રકાર E સાથેની સૂચિ કે જેનો ઉપયોગ પ્રકાર C ના મૂલ્યોની ગણતરી કરવા માટે થાય છે તેમાં નીચેની પુનરાવર્તિત પ્રકારની વ્યાખ્યા હશે, જ્યાં '=>' કાર્ય પ્રકારને સૂચવે છેઃ પ્રકાર સૂચિ = C =>// શૂન્ય દલીલ (E => સૂચિ => C) =>// વિપક્ષ દલીલ C// પેટર્ન સાથે મેળ ખાતું પરિણામ એ સૂચિ કે જેનો ઉપયોગ મનસ્વી પ્રકારોની ગણતરી કરવા માટે થઈ શકે છે તેમાં એક પ્રકાર હશે જે C પર પરિમાણ આપે છે. E માં સામાન્ય સૂચિ પણ E ને પ્રકાર દલીલ તરીકે લેશે. ટાઇપ કરેલ કલનમાં ચર્ચ અંકો માટે લામ્બડા કેલ્ક્યુલસ સિસ્ટમ એફ પણ જુઓ મોગેનસેન-સ્કોટ એન્કોડિંગ વોન ન્યુમેન ઓર્ડિનલ્સની વ્યાખ્યા-કુદરતી સંખ્યાઓને એન્કોડ કરવાની બીજી રીતઃ સેટ તરીકે સંદર્ભો ચર્ચ અને અન્ય સમાન એન્કોડિંગ વિશે બધા, જેમાં તેમને કેવી રીતે મેળવવું અને તેમના પરની કામગીરી, પ્રથમ સિદ્ધાંતોમાંથી ચર્ચ અંકોના કેટલાક ઇન્ટરેક્ટિવ ઉદાહરણો લામ્બડા કેલ્ક્યુલસ લાઇવ ટ્યુટોરિયલઃ બુલિયન બીજગણિત લામ્બડા કેલ્ક્યુલસ