جبر لامبدا 02

قسمت دوم؛ تعاریف بیشتر در لامبدا و پیش به سوی تعریف اعداد برای برنامه نویسی تابعی functional programming و کلی حرف های قلمبه که یعنی ما خفنیم ؛)

ممکنه اول بحث به نظر کند باشه که حتی اعداد هم نداریم ولی یهویی چنان شتابی می گیره که از هر برنامه ای سریع تر و جالب تره (فقط با دو تا کلیدواژه و دو تا کمک کلید واژه یه برنامه می خوایم بنویسیم با حلقه و همه چیز اونم با اطلاعات سال ۱۹۳۶ که کامپیوتر اختراع نشده هنوز)

خب برای اینکه سریع تر جلو بریم یه سری قسمت ها رو خلاصه می کنم و از جزییات کمی پرهیز می کنیم که ایده کلی مشخص بشه

چیزی که می دونیم اینه که می خوایم تمام توابع رو یا برنامه های کامپیوتری رو با یه زبان برنامه نویسی که تنها از دو تا عامل اصلی کلمه لاندا (لامبدا) λ و نقطه . ارائه بکنیم ولی این چطور عمل می کنه؟

چند تا قرارداد می گذاریم با هم؛ قرار۱ : وقتی حرف λ رو می بینیم یعنی یه تابع شروع شده و حروف یا علامت هایی که بین λ و نقطه میان ورودی های تابع ما هستن. قرار دوم اینه که از نقطه به بعد بدنه تابع هستش قرار ۳سوم اینه که با فاصله گذاری و پرانتز گذاری می تونیم تابع و ورودی ها و بدنه اش رو خوانا تر کنیم قرار چهارم: هر چیزی که می بینیم جز پرانتز و λ و نقطه علامت های قراردادی هستند که نشون می دن ما منظورمون اون نقطه هستش. مثلا منظورمون ورودی دوم تابع هستش حالا ممکنه هر چیزی اونجا بنویسیم یا معمولا ورودی رو با آرگومان ها یک اسم می گیریم به معنی یکی بودن نیست. حالا با چند تا مثال معلوم می شه منظور چیه

(λa.a)

خب این می شه تابع یک به یک که هر ورودی ای رو بگیره همون رو می ده بیرون اینجا داره ورودی رو به نام a می گیره که توی بدنه تابع به شکل همون a تحویل می ده

حالا می خوایم یه ورودی بدیم به این تابع

(λa.a)x---> x

می بینیم که ورودی x رو λ می گیره می گه خب این معادل a و بعد میگذاره جای a توی بدنه

دقیقا مثل توابع و آرگومان هایی که توی محیط های برنامه نویسی تعریف می کنیم که می گیم توی برنامه مثلا یه متغیر داشتیم و یه جای دیگه تابع رو که تعریف کنیم توی سیگنچر تابع میایم ورودی اول و دوم تعریف می کنیم و هر بار کال کردن تابع می تونیم ورودی های مختلف بدیم به اون تابع.

نکته خیلی خفن این ماجرا اینه که این موضوع رو سال ۱۹۳۶ اختراع٫کشف کرده موقعی که کامپیوتر اصلا نبوده.

یه تابع زیر در جاوا رو ببینیم

public class Main {
public static void main(String[] args){
int a=0,b=0,sum;
sum = sum(a,b);}
private static int sum(int x, int y){return x+y;}}

تابع sum دو تا آرگومان ورودی داره و یه خروجی داره حالا به عنوان ورودی ما بهش توی خط چهارم دو تا عدد a و b رو پاس دادیم. کاری به خروجی نداشته باشید و این فرمول رو ببینید.

(λxy.xy)ab

در واقع اون جمله ای که بالا گفتیم در مورد ورودی گرفتن و قرار دادن جای آرگومان ها توی این تابع اتفاق افتاده. (در مورد خروجی عجله نکنید چون الان تابع ما دو تا خروجی داره ولی خروجی توی اون تابعی که بالا نوشتیم یک عدد و حاصل جمع x و y بود)

می بینیم که λ یه جور نقش توضیع کننده رو داره. متغیرها رو از بیرون می گیره و می زاره جای x y همون کاری که سیگنچر توابع توی برنامه نویسی انجام می دن

خب حالا برای شروع کار نیاز به یه سری تعریف داریم که بتونیم اعداد رو تعریف کنیم.

میایم اول می گیم یه تابع داریم به اسم صفر

(λsz.z)ab ≡ b لامبدا آ و ب را می گیرد و در تابع توضیع می کند جای اس و زد که ب باقی می ماند

کارش چیه؟ دو تا ورودی بگیره اولی رو نابود کنه دومی رو تحویل بده (از اینجا به بعد من یه جاهایی مساوی می نویسم ولی توی جبر لامبدا مساوی نداریم یه علامت مساوی با سه تا خط داریم که به معنی معادل به کار می ره توی هر مرحله انجام کارها یا با فلش نشون می دن ولی من مساوی می نویسم)
یه چیزی هم معرفی می کنیم که به اسم ساکسسور یعنی چیزی که دقیقا دنبال این عضو ما اومده

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

1 ≡ λsz.s(z)

2 ≡ λsz.s(s(z))

3 ≡ λsz.s(s(s(z)))

باز هم توجه که توی جبر لامبدا ۱ و ۳ و این چیزا نداریم. ما فقط از این علامت ها استفاده می کنیم که خودمون راحت بفهمیم. اینجوری اعداد رو تعریف کردیم. نکته دیگه اینه که تا ۹ رو می تونیم اینجوری بنویسیم به ۱۰ که برسیم نمی تونیم از علامت ۱۰ استفاده کنیم چون این معنی یه دونه یک و یه دونه صفر کنار هم می ده نه ساکسسور ۹ پس باید یا یه علامت دیگه استفاده کنیم یا توی باکس بنویسیم یا هرچیزی که بشه یک علامت نه مجموع دو تا علامت.

حالا خود این تابع ساکسسور چجوری تعریف می شه؟

S ≡ λwyx.y(wyx)

حالا با چیزایی که یادگرفتیم محاسبه کنیم که ببینیم ساکسسور صفر یک می شه یا نه

S0 ≡ (λwyx.y(wyx))(λsz.z) ≡ λyx.y((λsz.z)yx) = λyx.y((λz.z)x) = λyx.y(x) ≡ 1

بله خوشبختانه روسفید شدیم و بعد از صفر یک اومد معادل اونی که بالاتر گفتیم و بعد از یک ببینیم آیا دو می شه یا نه

S1 ≡ (λwyx.y(wyx))(λsz.s(z)) = λyx.y((λsz.s(z))yx) = λyx.y(y(x)) ≡ 2

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

حالا که اعداد رو داریم بیایم تابع جمع رو هم تعریف کنیم

اون چیزی که توی بدنه عدد یک با اس کوچیک نوشتیم برای این بود که به ذهن اینجوری بیاد که این ساکسسور زیرو هستش ولی اون تعریف عدد داره می گه که عدد یک یعنی یک بار ما تابع ساکسسور رو روی صفر اعمال کردیم و عدد دو یعنی دو بار اعمال کردیم. پس می تونیم بفهمیم که جمع دو عدد مثل دو و سه یعنی اینکه به خاطر ۲ دوبار و به خاطر ۳ سه بار تابع ساکسسور رو به صفر اعمال کنیم و در مجموع ۵ بار ساکسسور صفر که می شه ۵ و درست هم هست

پس دو بار ساکسسور رو روی ۳ اعمال می کنیم

2S3 ≡ (λsz.s(sz))(λwyx.y(wyx))(λuv.u(u(uv))) ≡ (λwyx.y((wy)x))((λwyx.y((wy)x))(λuv.u(u(uv)))) ≡ SS3

که ساکسسور ساکسسور ۳ می شه پنج

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

بریم سراغ ضرب کردن که تابع ضرب کردن اینطور تعریف می شه

(λxyz.x(yz))

بیایم اینو روی ۲ و ۲ اعمال کنیم

(λxyz.x(yz))22 ≡ (λz.2(2z))

که بسته به حال خواننده با جاگذاری عدد دو با تعاریفی که بالا داشتیم می بینیم می شه ۴

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

پ.ن ۱ . واقعا باحال نیست که با یه لامبدا و یه نقطه بشه همه چیز رو از صفر تعریف کرد اونم پیش از عصر کامپیوتر؟

پ.ن ۲ . منبع من جزوه و کلاس های Raul Rojas هستش به علاوه مطالبی که توی یوتیوب یا کلاس ها از دانشجوها یاد می گیرم (از روخاس نپرسیدم اجازه دارم ترجمه کنم کارش رو یا نه در اولین فرصت می پرسم)

پ.ن ۳ . توی این لینک // لینک منبع می تونید لینک به تمامی قسمت ها رو پیدا کنید