۱ - ۴ساختار جملات لاندا

جبر لاندا سه‌تا مؤلفه‌ی اصلی، یا جمله‌ی لاندا داره: بیانیه‌ها یا expressions، متغیرها یا variables، و تجریدها یا abstractions. بیانیه در واقع یه ابَرمجموعه از همه‌ی اونهاست: یک بیانیه می‌تونه اسمِ یه متغیر باشه، یه تجرید باشه، یا ترکیبی از اونها باشه. یه متغیرِ مجرد ساده‌ترین نوعِ بیانیه‌ست. متغیرها اینجا هیچ معنی یا مقداری ندارن؛ فقط یه اسم برای ورودی‌های ممکن به تابع‌اند.

یه تجرید در واقع یه تابع ِه: جمله‌ی لاندایی که یک سر (یه لاندا) و یک بدنه ای داره که به یک آرگومان اعمال میشه. آرگومان یا argument، همون مقدارِ ورودی‌ه.

تجریدها شاملِ دو بخش اصلی‌اند: head یا سر و body یا بدنه. سرِ تابع، یک لاندا (‏‎λ‎‏) ست که بعدش اسم یه متغیر میاد. بدنه‌ی تابع هم یه بیانیه‌ی دیگه‌ست. بنابراین، یک تابعِ ساده چیزی شبیهِ این میشه:

متغیری که اسمش در سرِ جمله اومده، parameter یا پارامتر ِه و همه‌ی نمونه‌های همون متغیر در بدنه‌ی تابع رو انقیاد میده. یعنی وقتی این تابع رو به یک آرگومان اعمال می‌کنیم، هر ‏‎x‎‏ در بدنه‌ی تابع، مقدارِ اون آرگومان رو می‌گیره. این رو در بخشِ بعد بیشتر می‌بینیم.

در بخش قبل، تابع‌هامون به اسم ‏‎f‎‏ بودن. ولی تجرید ِلاندای
 ‏‎λx.x‎‏ هیچ اسمی نداره. به عبارت دیگه، یک تابع بی‌نام ِه. تابعی که اسم داره رو میشه توسط یه تابع دیگه صدا زد؛ ولی تابع بی‌نام اینطور نیست.

در زیر، ساختارِ این جمله‌ی لاندا رو جز به جز بررسی می‌کنیم:

λ x . x
^─┬─^
  └───── بازه‌ی سر جمله‌ی لاندا.

λ x . x
  ^───── تنـها پارامتر تابع؛ هر متـغـیر با
          ایـن نام در بـدنه‌ی تابـع، به ایـن
          پارامتر مقیّد میشه.

λ x . x
      ^─ بدنـه، بیانیـه‌ای که لاندا بعـد از
          اعـمال شـدن بـرمـی‌گـردونه. این یک
          متغیر مقیّده.

اون نقطه (.) پارامترهای لاندا رو از بدنه‌ی تابع جدا می‌کنه.

تجرید به طور کلی هیچ اسمی نداره، ولی به این خاطر بهش میگیم تجرید که در واقع یک جامع‌کننده، یا تجریدِ^* نمونه‌ی معینی از یک مسئله‌ست، و این تجرید رو از طریق نامگذاری انجام میده. این نام‌ها که جایگزین مقادیر معین هستن و به متغیرها نسبت داده میشن، این اجازه رو میدن که تابعِ کلی به مقادیرِ مختلفی (یا حتی تایپ‌های مختلفی از مقادیر، که بعداً می‌بینیم) اعمال بشه. وقتی تجرید رو به آرگومان‌ها اعمال می‌کنیم، اون نام‌ها رو با مقادیر جایگزین می‌کنیم، و از تجرید به یه بیانیه‌ی معین می‌رسیم.

تعادل آلفا

اکثراً وقتی این تابع رو در جبر لاندا بیان می‌کنن، چیزی شبیه این رو می‌بینید:

متغیر ‏‎x‎‏ اینجا مفهوم خاصی نداره، جز اینکه نقش یه متغیر رو، فقط در همون بیانه ایفا می‌کنه. به همین خاطر، یک نوع تعادل بین جملات لاندا وجود داره به اسم تعادل آلفا، که میگه بیانیه‌های زیر:

همه یک معنا دارن. همشون یک تابع‌اند.

حالا به حاصلِ اعمال این تجرید به یک مقدار معین نگاه میندازیم.