بخشی از پاورپوینت
--- پاورپوینت شامل تصاویر میباشد ----
اسلاید 1 :
محاسبات لامبدا
¨سیستمی با سه جزء:
نشانه گذاری برای تعریف توابع
سیستمی برای اثبات تساوی گزاره ها
مجموعه ای از قوانین که کاهش (reduction) نام دارد
اسلاید 2 :
تاریخچه
¨هدف اصلی:
¡تئوری اصلی جانشینی
¨برای توابع قابل محاسبه موفق تر بود
¡جانشینی ß محاسبه سمبلیک
¡تز Church
¨طراحی لیسپ، ML و زبانهای دیگر را تحت تأثیر قرار داده است.
اسلاید 3 :
دلایل مطالعه
¨نشانه گذاری های نحوی پایه
متغیر های آزاد(free) و مقید(free)
توابع
اعلانها
¨قانون محاسبات
ارزیابی سمبولیک مناسب برای توصیف برنامه
در بهینه سازی و توسعه ی ماکرو کاربرد دارد
ایده هایی در مورد حوزه ی مقید سازی(binding) را ارائه می دهد.
اسلاید 4 :
عبارتها و توابع
¨عبارتها:
x + y x + 2*y + z
¨توابع:
- l (x+y) lz. (x + 2*y + z)
¨کاربرد:
(lx. (x+y)) 3 = 3 + y
(lz. (x + 2*y + z)) 5 = x + 2*y + 5
اسلاید 5 :
توابع مرتبه ی بالاتر
¨با داشتن تابع f، تابع fof را برمی گرداند:
- l lx. f (f x)
¨طریقه ی عمل کردن:
(lf. lx. f (f x)) (ly. y+1)
= lx. (ly. y+1) ((ly. y+1) x)
= lx. (ly. y+1) (x+1)
= lx. (x+1)+1
اسلاید 6 :
روندی مشابه، با استفاده از نحو لیسپ
¨با داشتن تابع 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))
اسلاید 7 :
متغیرهای آزاد و مقید
¨متغیر آزاد: متغیری که در یک عبارت تعریف نشده باشد:
¡متغیر y در lx. (x+y) آزاد است
¡تابع lx. (x+y) با lx. (x+z) تفاوت دارد
¨متغیر مقید: متغیری که آزاد نیست
¡متغیر x در lx. (x+y) مقید است
¡تابع lx. (x+y) با lz. (z+y) یکسان است (تغییر نام)
¨مقایسه
ò x+y dx = ò z+y dz
¨مثال :
¡y در lx. ((ly. y+2) x) + y هم آزاد و هم مقید است
اسلاید 8 :
تقلیل
¨قانون محاسبات برپایه ی تقلیل b قرار دارد
(lx. e1) e2 ® [e2/x]e1
که جانشین سازی شامل تغییر نام در صورت نیاز است
¨تقلیل:
¡اعمال قوانین محاسباتی پایه به هر عبارت
¡تکرار
¨اتصال:
¡نتیجه ی نهایی (در صورت وجود) مستقل از ترتیب ارزیابی ، همیشه یکتا است
اسلاید 9 :
تغییر نام متغیر های مقید
¨مثال:
(lf. lx. f (f x)) (ly. y+x)
¨
¨جانشینی ” کورکورانه“
- l [(ly. y+x) ((ly. y+x) x)] = lx. x+x+x
¨تغییر نام متغیرهای مقید:
(lf. lz. f (f z)) (ly. y+x)
= lz. [(ly. y+x) ((ly. y+x) z))] = lz. z+x+x
قانون ساده: همیشه متغیرهایی را تغییر نام می دهیم که مجزا می شوند.
