مقدمه:
محاسبات لامبدا محاسبات لامبدا سیستمی با سه جزء: نشانه گذاری برای
تعریف توابع سیستمی برای اثبات تساوی گزاره ها مجموعه ای از قوانین که کاهش
(reduction) نام دارد تاریخچه هدف اصلی: تئوری اصلی جانشینی برای توابع
قابل محاسبه موفق تر بود جانشینی محاسبه سمبلیک تز Church طراحی لیسپ، ML
و زبانهای دیگر را تحت تأثیر قرار داده است.
دلایل مطالعه نشانه گذاری
های نحوی پایه متغیر های آزاد(free) و مقید(free) توابع اعلانها قانون
محاسبات ارزیابی سمبولیک مناسب برای توصیف برنامه در بهینه سازی و توسعه ی
ماکرو کاربرد دارد ایده هایی در مورد حوزه ی مقید سازی(binding) را ارائه
می دهد.
عبارتها و توابع عبارتها: x + y x + 2*y + z توابع: x.
(x+y) z.
(x + 2*y + z) کاربرد: (x.
(x+y)) 3 = 3 + y (z.
(x + 2*y + z)) 5 = x + 2*y + 5 توابع مرتبه ی بالاتر با داشتن تابع f، تابع fof را برمی گرداند: f.
x.
f (f x) طریقه ی عمل کردن: (f.
x.
f (f x)) (y.
y+1) = x.
(y.
y+1) ((y.
y+1) x) = x.
(y.
y+1) (x+1) = x.
(x+1)+1
روندی مشابه، با استفاده از نحو لیسپ با داشتن تابع f، تابع fof را برمی
گرداند: (lambda (f) (lambda (x) (f (f x)))) طریقه ی عمل کردن: ((lambda
(f) (lambda (x) (f (f x)))) (lambda (y) (+ y 1)) = (lambda (x) ((lambda
(y) (+ y 1)) ((lambda (y) (+ y 1)) x)))) = (lambda (x) ((lambda (y) (+ y
1)) (+ x 1)))) = (lambda (x) (+ (+ x 1) 1)) متغیرهای آزاد و مقید متغیر
آزاد: متغیری که در یک عبارت تعریف نشده باشد: متغیر 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 هم آزاد و هم مقید است تقلیل قانون محاسبات برپایه ی تقلیل قرار دارد (x.
e1)
e2 [e2/x]e1 که جانشین سازی شامل تغییر نام در صورت نیاز است تقلیل:
اعمال قوانین محاسباتی پایه به هر عبارت تکرار اتصال: نتیجه ی نهایی (در
صورت وجود) مستقل از ترتیب ارزیابی ، همیشه یکتا است تغییر نام متغیر های
مقید مثال: (f.
x.
f (f x)) (y.
y+x) جانشینی ” کورکورانه“ x.
[(y.
y+x) ((y.
y+x) x)] = x.
x+x+x تغییر نام متغیرهای مقید: (f.
z.
f (f z)) (y.
y+x) = z.
[(y.
y+x) ((y.
y+x) z))] = z.
z+x+x قانون ساده: همیشه متغیرهایی را تغییر نام می دهیم که مجزا می شوند.
.