۱ - ۵ساده‌سازی بتا
وقتی تابعی رو به یک آرگومان اعمال می‌کنیم، همه‌ی متغیرهای مقیّد در بدنه‌ی تجرید رو با بیانیه‌ی ورودی جایگزین می‌کنیم. سرِ تجرید رو هم حذف می‌کنیم، چراکه نقشش فقط انقیاد ِ یک متغیر بود. به این کار ساده‌سازی بتا گفته میشه.
همون تابعی که بالاتر داشتیم رو فرض کنیم:
λx.xاولین ساده‌سازی بتا رو با یه عدد انجام میدیم*. اول تابع رو به ۲ اعمال می‌کنیم، بعد بجای همه متغیرهای مقیّد در بدنه‌ی تابع ۲ میذاریم، و نهایتاً سر رو هم حذف می‌کنیم:
(λx.x) ۲۲تنها متغیر مقیّد اینجا x ِه، پس اعمال این تابع به ۲، خود ۲ رو برمی‌گردونه. این تابع به اسم تابع همانی معرفی میشه†. تنها کاری که می‌کنه یه آرگومان x می‌گیره و همون آرگومان رو برمی‌گردونه. خود x ذاتاً هیچ معنایی اینجا نداره، ولی چون در سر این تابع قید شده، وقتی تابع به یه آرگومان اعمال میشه، همه‌ی x های داخل بدنه‌ی تابع باید همون مقدار رو بگیرن.
در جبر لاندا، میشه اعداد رو با تجریدهای لاندا به تنهایی (به جای استفاده از اعدادی که می‌شناسیم) هم بدست آورد، ولی نوشتار خیلی زود سنگین میشه و خوندنش خیلی سخت (م. منظور استفاده از اعدادِ چرچ ِه، که بطور خلاصه، عدد مورد نظر توسط تعداد دفعاتی که تابع با خودش ترکیب میشه نشون داده میشه).
دقت کنید که این همون تابع همانی در ریاضیات، با معادله‌ی f(x)=x هست. یک فرق بین این دو اینه که f(x)=x تعریفِ یک تابع به اسمِ f ِه، ولی اون تجرید لاندا، خودش تابع‌ه.
یه مثال دیگه میزنیم که یه کم حساب هم داشته باشه. اینجا از پرانتز استفاده کردیم تا واضحتر بشه که x + ۱، بدنه‌ی بیانیه‌ست. یا به عبارت دیگه، مشخص باشه که تابع رو به ۱ اعمال نکردیم:
(λx.x + ۱)به نظرتون جوابِ این تجرید بعد از اعمال به ۲ چی میشه؟ به ۱۰ چطور؟
ساده‌سازیِ بتا همین فرایندِ اعمال یک جمله‌ی لاندا به یه آرگومان، جایگزینی متغیرهای مقیّد با مقدارِ اون آرگومان، و حذفِ سر از جمله است. حذف سر نشون از اینه که تابع اعمال شده.
می‌تونیم به جای یه مقدار معین، تابع‌مون رو به یه تابع همانی دیگه اعمال کنیم:
(λx.x)(λy.y)در این مورد، به جای x، کل تجرید ِ λy.y رو میذاریم. در زیر برای جایگذاری از علامتِ ≔ استفاده کردیم:
(λx.x)(λy.y)[x ≔ (λy.y)]λy.yجواب نهایی‌مون یه تابعِ همانی ِدیگه‌ست. بیشتر از این ساده نمیشه، چرا که آرگومان دیگه‌ای باقی نمونده که تابع رو بهش اعمال کنیم.
همین مثال رو با یه آرگومانِ اضافه ببینیم:
(λx.x)(λy.y)zدر جبر لاندا، اعمال تجریدها، شرکت‌پذیری از چپ داره. یعنی از چپ همبند، یا دسته‌بندی، میشن (مگر با پرانتز همبندیِ دیگه‌ای تعیین شده باشه). پس، این جمله رو:
(λx.x)(λy.y)zمیشه اینطوری بازنویسی کرد:
((λx.x)(λy.y))zبه ساده‌سازی که ادامه بدیم:
((λx.x)(λy.y))z[x ≔ (λy.y)](λy.y)z[y ≔ z]zدیگه چیزی برای اعمال نمونده، در موردِ z هم هیچ چیز نمی‌دونیم. پس از این ساده‌تر نمیشه.
در بخش بعد، تابع‌هایی رو می‌بینیم که چند سر دارن. تابع‌هایی هم می‌بینیم که متغیر آزاد دارن (متغیرهایی که در بدنه وجود دارن ولی در سر قید نشدن). در هر صورت فرایندِ اصلی تغییری نمی‌کنه. ساده‌سازی بتا وقتی متوقف میشه که یا هیچ سر (یا لاندایی) نمونده باشه، یا هیچ آرگومانی که توابع بهش اعمال بشن نمونده باشه. بنابراین یه محاسبه با یک بیانیه‌ی لاندا شروع میشه (یا دو بیانه، اگه بخوایم تابع و ورودیش رو جدا در نظر بگیریم)، و از تعدادِ محدودی جملاتِ لاندا به دنبال هم، که هر کدوم از یکبار ساده‌سازیِ بتا ِ جمله‌ی قبلش بدست میاد تشکیل میشه. ما این فرایند رو در اعمالِ توابع به آرگومان‌ها اونقدر ادامه میدیم تا دیگه سر یا لاندایی باقی نمونه که حساب کنیم، یا آرگومان‌ها تموم بشن.
متغیرهای آزاد
نقشِ سرِ یک تابع اینه که متغیرهایی که باید بعد از اعمالِ تابع جایگزین بشن رو مشخص کنه، یا به طور خلاصه، وظیفه‌ی انقیاد ِ متغیرها رو داره. یک متغیرِ مقیّد باید در کلِ بیانیه فقط یک مقدار داشته باشه.
ولی گاهی پیش میاد که متغیرهایی در بدنه‌ی بیانیه باشند که در سرِ تابع نامگذاری نشدن. اینجور متغیرها رو میگیم free یا آزاد. در بیانیه‌ی زیر:
λx.xyx متغیر مقیّد ِه، چون در سر تابع قید شده، ولی y که قید نشده، یه متغیر آزاد به حساب میاد. وقتی این تابع رو به یه آرگومان اعمال می‌کنیم، هیچ کاری نمیشه با y کرد؛ ساده نشده باقی می‌مونه.
این بیانه میتونه به یه آرگومان مثل z اعمال بشه، اینطوری: (λx.xy)z. اینجا یک مرحله‌ی اضافه با ≔ که قبلاً معرفی کردیم نشون میدیم (اکثر کتابهای جبر لاندا این مرحله رو نمی‌نویسن):
آ.
(λx․xy)z
لاندا رو به آرگومان z اعمال می‌کنیم.
ب.
(λ[x ≔ z]․xy)
از اونجا که x یه متغیر مقیّد ِه، همه‌ی x ها در بدنه‌ی تابع با z جایگزین میشن. سر تابع هم حذف میشه.
پ.
zy
تابع اعمال شده و دیگه سر یا متغیر مقیّدی باقی نمونده. چیزی هم از z یا y نمی‌دونیم، پس از این ساده‌تر نمیشه.
دقت کنید که تعادل آلفا به متغیرهای آزاد اعمال نمیشه. یعنی λx․xz و λx․xy معادل هم نیستن، چون z و y ممکنه یکی نباشن. ولی بیانیه‌های λxy․yx و λab․ba به خاطر تعادل آلفا معادلِ همدیگن؛ λx․xz و λy․yz هم همینطور، چون متغیرهای آزادشون دست نخوردن.