جبر لامبدا ۰۳

جبر لامبدا

قاعدتا داشتن تصویرهای بهتر به فهم موضوع بهتر کمک می کرد ولی متاسفانه امکانش رو ندارم فعلا بعدا همه مطالب رو یکجا مناسب می نویسم

می رسیم به عبارات منطقی

طبق یک قرارداد می گیم که درست یا True تابعی هستش که دو تا ورودی می گیره و اولی رو بر می گردونه و غلط منطقی False هم تابعی هست که دو تا ورودی می گیره و دومی رو بر می گردونه

T ≡ (λxy.x)

F ≡ (λxy.y)

و برای عملگرهای منطقی هم می دونیم که ٬و٬ منطقی عبارتی هست که فقط در صورتی که هر دو عبارت درست باشند درست بر می گردونه و ٬یا٬ منطقی در صورتی که هر دو غلط باشند فقط غلط بر می گردونه

(and)≡ (λxy.xyF)

تحلیل: دو تا ورودی در جای x و y رو می گیره و توی بدنه تابع توضیع می کنه؛ انتظار ما اینه که فقط در حالی که هر دو T هستند به ما T بده و در غیر این صورت F. چیزی که می مونه این شکلیه xyF اولی دو تا حالت داره یا Tیا F اگر Fباشه طبق تعریف بالاتر دومی رو بر می گردونه یعنی جواب نهایی F می شه و اگر اولی T باشه باز طبق تعریف میاد و از دو تای بعدی انتخاب می کنه و اولین ورودی که همون y باشه می شه جواب ما که اگر T باشه هر دو T بودند و جواب درسته و اگر F باشه باز هم جواب درسته.

برای OR منطقی هم اینطور باید باشه که اگر اولی درست بود درست برگردون فارغ از اینکه دومی چیه ولی اگر غلط بود دومی تعیین کننده جواب نهاییه

(OR)≡ (λxy.xTy)

و تعریف not هم اینه که اگر درست بود غلط بده و اگر غلط بود درست بده.

(Not)≡ (λx.xFT)

این تابع هم اگر T بگیره می شه TFT که طق قانون همیشگی از چپ شروع می کنیم به خوندن و گذاره اولی که درست هست ورودی اولیش رو انتخاب می کنه و جواب نهایی F می شه و اگر به این تابع F بدیم FFT می شه که جوابش باز اینه که F اولی میاد دو تای بعدی رو به عنوان ورودی می گیره و T رو بر می گردونه

قطعا توی برنامه نویسی نیازه که یه جاهایی تصمیم گرفته بشه که به کدوم شاخه قراره بریم و برنامه دو تا مسیر بشه

خیلی برنامه ها می بینیم که 0 رو معادل F و باقی اعداد رو معادل T می گیرند ولی چطوری؟

میایم یه تابع تعریف می کنیم که این کار رو بکنه

لازمه یادمون بیاد تابع 0 دو تا ورودی می گیره و اولی رو نابود می کنه.

0fa≡(λsz.z)fa≡a

تابع F هم گفتیم دو تا ورودی می گیره دومی رو بر می گردونه و اگر روی یک عضو اعمال بشه تابع یک به یک یا واحد باقی می مونه

(λxy.y)a ≡ (λy.y) ≡ ID

یعنی یه جورایی تابع F و 0 یکی هستند. به این اتفاق توی برنامه نویسی Overloading می گیم.

تابع Zرو تعریف می کنیم .

Z0 = (λx.xF¬F)0

این رو محاسبه کنیم T در میاد ولی برای اعداد دیگه محاسبه کنیم F میاد بیرون تایپ و اثباتش خیلی طول ممکنه بکشه

در مطلب بعدی توابعی برای پیدا کردن عدد قبل و بعد می نویسیم