۱ - ۶آرگومان‌های متعدد
هر لاندا فقط یک پارامتر رو قید می‌کنه، و فقط یک آرگومان می‌گیره. توابعی که چند آرگومان می‌گیرن، در واقع سرهای متعدد و تودرتو دارن. بعد از اولین اعمالِ این توابع به یک آرگومان، چپ‌ترین سر حذف میشه، و همینطور اعمالِ آرگومان‌های بیشتر سرها رو حذف می‌کنه. اینطور فرمول‌بندیِ توابع اولین بار توسط موسی شینفینکل در دهه‌ی ۱۹۲۰ کشف شده بود، ولی بعداً هسکل کاری دوباره به اون دست پیدا کرد، و حالا به currying شناخته میشه.
فرض کنید این لانداها رو به مقادیر مشخص اعمال کنیم. از یه مثال ساده با تابع همانی شروع می‌کنیم:
۱.
λx․x
۲.
(λx․x) ۱
۳.
[x ≔ ۱]
۴.
۱
حالا یه مثال با تابعی که "چند آرگومان" می‌گیره:
۱.
λxy․xy
۲.
(λxy․xy)(λz․a) ۱
۳.
(λx․(λy․xy))(λz․a) ۱
۴.
[x ≔ (λz․a)]
۵.
(λy․(λz․a)y) ۱
۶.
[y ≔ ۱]
۷.
(λz․a) ۱
یک مرحله دیگه ساده‌تر میشه.
۸.
[z ≔ ۱]
ولی z اصلاً در بدنه‌ی تابع وجود نداره، پس جایی نیست که ۱ رو بذاریم. بعد از حذف سر، داریم:
۹.
a
در مطالب و مباحثِ آکادمیکِ جبر لاندا، بیشتر از متغیرهای انتزاعی استفاده میشه تا مقادیر معین؛ با این حال تاثیری در فرایند ساده‌سازیِ بتا نداره. جبر لاندا یه فرایند یا رَوِش‌ه، مثل یه بازی با چندتا قاعده‌ی ساده برای تبدیل و اعمالِ لانداها. توی مثال‌ها، ما مقادیر معین رو فقط برای تداعیِ بهترِ ساده‌سازی آوردیم.
در مثال بعدی فقط از متغیرهای انتزاعی استفاده می‌کنیم. توی کتابهای جبرِ لاندا، به خاطر تعادل آلفا، گاهی ممکنه بیانیه‌ای مثل بیانیه‌ی زیر ببینید:
(λxy․xxy)(λx․xy)(λx․xz)ساده‌سازیِ چنین بیانیه‌ای، به خاطرِ x هایی که بعضیاشون با سرهای متفاوتی قید شدن، خیلی زود گیج‌کننده میشه. برای دوری از چنین گِره‌ای، می‌تونیم از متغیرهای مختلف برای هر تجرید استفاده کنیم. باز هم جای تاکید داره که اسم متغیرها (حرف انگلیسیِ استفاده شده) به خودیِ‌خود مفهوم خاصی ندارن:
۱.
(λxyz․xz(yz))(λmn․m)(λp․p)
۲.
(λx․λy․λz․xz(yz))(λm․λn․m)(λp․p)
اینجا نه ساده‌سازی کردیم نه تابعی رو اعمال کردیم. فقط لانداها رو باز کردیم تا currying واضحتر بشه.
۳.
(λy․λz․(λm․λn․m)z(yz))(λp․p)
اولین قدم در ساده‌سازی، اعمالِ لاندای بیرونی (که x رو قید می‌کرد) به اولین آرگومان، یعنی (λm․λn․m) بود.
۴.
λz․(λm․λn․m)z((λp․p)z)
با اعمالِ y، تنها y موجود رو با آرگومان بعدی، یعنی جمله‌ی λp․p جایگزین کردیم. در این مرحله، لاندای بیرونی (یعنی لاندای z) رو نمیشه ساده کرد، چون آرگومانی نداره. برای ساده‌سازیِ بیشتر باید لایه‌لایه بریم داخلِ جملات تا چیزی برای ساده کردن پیدا کنیم.
۵.
λz․(λn․z)((λp․p)z)
اینجا لاندایی که m رو قید کرده بود به آرگومان z اعمال کردیم. اگه باز هم بگردیم، می‌بینیم که با اعمال لاندای n به جمله‌ی ((λp․p)z) بیانیه ساده‌تر میشه.
۶.
λz․z
این مرحله‌ی آخر ممکنه یه کم عجیب به نظر برسه. اینجا بیرونی‌ترین (یا چپ‌ترین) جمله‌ای که ساده‌تر میشد، λn․z بود که به کل ((λp․p)z) اعمال شده بود. همونطوری که توی یکی از مثال‌های قبلی دیدیم، وقتی متغیری که سر قید کرده توی بدنه‌ی تابع نیست، یعنی اون تابع ورودی‌ش رو کنار میذاره و بدنه‌ش رو به عنوانِ خروجی برمی‌گردونه. اینجا هم مهم نبود که n به چه چیزی قید شده بود، λn․z بدون قید و شرط فقط z رو برگردوند. نهایتاً هم به یه بیانیه‌ای رسیدیم که ساده‌تر نمیشه.
آنتراکت: تمرین تعادل
۱.
λxy․xz
a)
λxz․xz
b)
λmn․mz
c)
λz․(λx․xz)
۲.
λxy․xxy
a)
λmn․mnp
b)
λx․(λy․xy)
c)
λa․(λb․aab)
۳.
λxyz․zx
a)
λx․(λy․(λz․z))
b)
λtos․st
c)
λmnp․mn