• سیستمی با سه جزء
 نشانه گذاری برای تعریف توابع
 سیستمی برای اثبات تساوی گزاره ها
 مجموعه ای از قوانین که کاهش (reduction) نام دارد

• نشانه گذاری های نحوی پایه
 متغیر های آزاد(free) و مقید(free)
 توابع
 اعلانها
• قانون محاسبات
 ارزیابی سمبولیک مناسب برای توصیف برنامه
 در بهینه سازی و توسعه ی ماکرو کاربرد دارد
 ایده هایی در مورد حوزه ی مقید سازی(binding) را ارائه می دهد.

• متغیر آزاد متغیری که در یک عبارت تعریف نشده باشد
 متغیر y در x. (x+y) آزاد است
 تابع x. (x+y) با x. (x+z) تفاوت دارد
• متغیر مقید متغیری که آزاد نیست
 متغیر x در x. (x+y) مقید است
 تابع x. (x+y) با z. (z+y) یکسان است (تغییر نام)
• مقایسه
 x+y dx =  z+y dz
• مثال
 y در x. ((y. y+2) x) + y هم آزاد و هم مقید است

---

برچسب ها: پاورپوینت محاسبات لامبدا بررسی ساختار محاسبات لامبدا تئوری اصلی جانشینی