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 ایک تکراری تعریف ہے۔ Y کمبینٹر کو ریکرشن کو لاگو کرنے کے لیے استعمال کیا جا سکتا ہے۔ ایک نیا فنکشن بنائیں جسے ڈیوی بائی کہا جاتا ہے ؛ بائیں ہاتھ کی طرف دائیں ہاتھ کی طرف حاصل کرنے کے لیے، پھر، جہاں، دیتا ہے، یا بطور متن، استعمال کرتے ہوئے\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 (\m. \n. n (\n. \f. \x. n (\g. \h. h (gf)) (\u. x) (\u. x) m) nm) (((\n. \f. \x) nx۔ f (n f x)) n)) مثال کے طور پر، 9/3 کی نمائندگی تقسیم (\f. \x. f (f (f (f (f (f (f (f (f x))))))) (\f. \x. f (f (f (f x)))) کے ذریعے کی جاتی ہے۔ \f. \x. f (f (f (x))) دستخط شدہ اعداد چرچ کے اعداد کو دستخط شدہ اعداد تک بڑھانے کا ایک آسان طریقہ چرچ کے جوڑے کا استعمال کرنا ہے، جس میں چرچ کے اعداد ہوتے ہیں جو مثبت اور منفی قدر کی نمائندگی کرتے ہیں۔ انٹیجر ویلیو دو چرچ کے اعداد کے درمیان فرق ہے۔ ایک قدرتی نمبر کو دستخط شدہ نمبر میں تبدیل کیا جاتا ہے، منفی اقدار کو تبدیل کرکے انجام دیا جاتا ہے۔ اگر جوڑی میں سے کوئی ایک صفر ہو تو انٹیجر ویلیو زیادہ قدرتی طور پر ظاہر ہوتی ہے۔ ون زیرو فنکشن اس شرط کو حاصل کرتا ہے، ریکرشن کو Y کمبینٹر کا استعمال کرتے ہوئے لاگو کیا جاسکتا ہے، پلس اور مائنس ایڈیشن کو جوڑی پر ریاضیاتی طور پر اس طرح بیان کیا جاتا ہے، آخری اظہار کا ترجمہ لیمبڈا کیلکولس میں اس طرح کیا جاتا ہے، اسی طرح گھٹاؤ کی تعریف کی جاتی ہے، دینا، ضرب اور تقسیم ضرب کی تعریف اس طرح کی جا سکتی ہے، آخری اظہار کا ترجمہ لیمبڈا کیلکولس میں اس طرح کیا جاتا ہے، تقسیم کے لیے یہاں اسی طرح کی تعریف دی گئی ہے، سوائے اس تعریف کے، ہر جوڑے میں ایک قدر صفر ہونی چاہیے (اوپر ون زیرو دیکھیں)۔ ڈیو زیڈ فنکشن ہمیں اس قدر کو نظر انداز کرنے کی اجازت دیتا ہے جس میں صفر جزو ہوتا ہے۔ اس کے بعد ڈیوی زیڈ کو مندرجہ ذیل فارمولے میں استعمال کیا جاتا ہے، جو ضرب کے لیے یکساں ہے، لیکن ملٹی کے ساتھ ڈیوی زیڈ سے تبدیل ہوتا ہے۔ عقلی اور حقیقی اعداد عقلی اور کمپیوٹیبل حقیقی اعداد کو بھی لیمبڈا کیلکولس میں انکوڈ کیا جا سکتا ہے۔ عقلی اعداد کو دستخط شدہ اعداد کے جوڑے کے طور پر انکوڈ کیا جا سکتا ہے۔ کمپیوٹیبل حقیقی اعداد کو ایک محدود عمل کے ذریعے انکوڈ کیا جا سکتا ہے جو اس بات کی ضمانت دیتا ہے کہ حقیقی قدر سے فرق ایک ایسے نمبر سے مختلف ہوتا ہے جسے ہماری ضرورت کے مطابق چھوٹا بنایا جا سکتا ہے۔ دیئے گئے حوالہ جات ایسے سافٹ ویئر کی وضاحت کرتے ہیں جو نظریہ طور پر لیمبڈا کیلکولس میں ترجمہ کیا جا سکتا ہے۔ ایک بار جب حقیقی اعداد کی وضاحت ہو جاتی ہے، تو پیچیدہ اعداد کو قدرتی طور پر حقیقی اعداد کے جوڑے کے طور پر انکوڈ کیا جاتا ہے۔ اوپر بیان کردہ ڈیٹا کی اقسام اور افعال یہ ظاہر کرتے ہیں کہ کسی بھی ڈیٹا کی قسم یا حساب کو لیمبڈا کیلکولس میں انکوڈ کیا جا سکتا ہے۔ یہ چرچ ٹورنگ کا مقالہ ہے۔ دیگر نمائندوں کے ساتھ ترجمہ زیادہ تر حقیقی دنیا کی زبانوں میں مشین کے مقامی انٹیجرز کی حمایت ہوتی ہے۔ چرچ اور ان چرچ کے افعال غیر منفی انٹیجرز اور ان کے متعلقہ چرچ کے اعداد کے درمیان تبدیل ہوتے ہیں۔ افعال یہاں ہاسکل میں دیے گئے ہیں، جہاں λ لیمبڈا کیلکولس کے λ سے مطابقت رکھتا ہے۔ دیگر زبانوں میں نفاذ اسی طرح کے ہیں۔ ٹائپ کریں چرچ 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 کو بھی قسم کی دلیل کے طور پر لے گی۔ ٹائپ شدہ کیلکولس موگینسن سکاٹ انکوڈنگ وان نیومن میں چرچ کے اعداد کے لیے لیمبڈا کیلکولس سسٹم ایف بھی دیکھیں۔ آرڈینلز کی تعریف-قدرتی اعداد کو انکوڈ کرنے کا ایک اور طریقہ: سیٹ کے طور پر حوالہ جات چرچ اور دیگر اسی طرح کے انکوڈنگ کے بارے میں، بشمول انہیں حاصل کرنے کا طریقہ اور ان پر عمل، پہلے اصولوں سے چرچ کے اعداد کی کچھ انٹرایکٹو مثالیں لیمبڈا کیلکولس لائیو ٹیوٹوریل: بولین الجبرا لیمبڈا کیلکولس