معرفی حساب لامبدا

[arashtabaie]

چکيده:
در منطق رياضي و علوم کامپيوتر، حساب لامبدا سامانه ي رسمي براي تعريف توابع، استفاده از توابع و بازگشت است. اين مفهوم توسط آلونزو چرچ در سال 1932 به عنوان قسمتي از تحقيقي روي اصول رياضي معرفي شد. اين روش اصول نحوي براي ارائه ي موارد نام برده شده ارائه مي دهد.

در این تاپیک به معرفی حساب لامبدا که مبنای طراحی بسیاری از زبان های برنامه سازی است می پردازم که در بخش های زیر خدمت شما ارائه خواهد شد:
1.مقدمه و تعاریف
2.توابع و نمایش توابع
3.نحو عبارات
4.variable binding
5.تساوی و جابجایی
6.تغییر نام متغیرهای وابسته
7.برنامه سازی با استفاده از حساب لامبدا

[arashtabaie]

مقدمه و تعاریف:
حساب لامبدا سامانه ي رياضي است که برخي مفاهيم زبان هاي برنامه سازي را به شکل ساده و خالص بيان مي کند. حساب لامبداي ابتدايي سه قسمت اصلي دارد: يک نشان گذاري براي تعريف توابع، يک روش اثبات براي محاسبه ي تساوي دو عبارت و مجموعه اي از قواعد محاسباتي که تقليل ناميده مي شود. علت وجود لغت لامبدا در نام حساب لامبدا، استفاده از حرف يوناني لامبدا(λ) براي تعريف توابع است. لغت "حساب" هم به علت استفاده از تقليل براي محاسبه ي مقدار يک تابع با توجه به مقادير ورودي استفاده شده است. اين محاسبه عبارت است از مقدار يابي نمادين يک عبارت. حساب لامبدا نشان گذاري مناسبي را براي توصيف کردن يک زبان برنامه سازي محيا مي کند و مي توان به آن به عنوان پايه ي ساخت بسياري از زبان هاي برنامه سازي نگريست. در حقيقت، حساب لامبدا فرم هاي پايه اي و ابتدايي براي پارامتري کردن (با استفاده از تعريف توابع) و پيوند دادن(با استفاده از اظهار توابع) را در اختيار قرار مي دهد. اينها مفاهيم پايه اي هستند که نقطه ي مشترک تقريبا تمام زبان هاي برنامه سازي امروزي مي باشند. در نتيجه آشنايي با حساب لامبدا براي کار با زبان برنامه نويسي مورد علاقه ي شما بسيار مهم است. در اين رساله سعي بر آن است که به علت پيچيدگي کمتر حساب لامبداي بدون گونه به علت سادگي بيشتر مورد بررسي قرار گيرند. از انواع ديگر اين حساب، حساب لامبداي با بررسي گونه است که البته در همه ي اين گونه ها محاسبات و نمايش پايه اي همانگونه که در اين مقاله توضيح داده مي شود انجام مي گيرد.

[arashtabaie]

توابع و نمايش توابع:

يک تابع نمايشي از يک قاعده براي مشخص کردن يک مقدار از يک مقدار ورودي است. اين نوع نگاه به توابع به صورت غير رسمي در قسمت اعظم رياضيات استفاده مي شود. در ساده ترين و خالص ترين نوع حساب لامبدا، هيج عملگر وابسته به دامنه اي، مانند جمع و تفريق يا توان، استفاده نمي شود. تنها استفاده از تعريف توابع مجاز است. با توجه به اين موضوع مي توان تابعي به شکل زير نوشت:
Please Login or Register to see this code
دليل امکان همچون نمايشي اين است که H تنها به کمک استفاده از توابع تعريف شده و فرض مي کنيم توابع مورد استفاده در تعريف قبلا تعريف شده اند. امکان اضافه کردن عملگرهايي مانند جمع يا توان به حساب لامبداي خالص نيز وجود دارد.
ساختارهاي اصلي حساب لامبدا، تجريد لامبدا و کاربرد لامبدا هستند. از تجريد لامبدا براي نوشتن توابع استفاده مي شود: اگر M يک عبارت باشد، در نتيجه λx.M تابعي است که در صورت استفاده از M به عنوان تابعي که متغير x را مي گيرد به دست مي آوريم. براي مثال λx.x يک تجريد لامبدا است که تابع يکه را تعريف مي کند.تابع يکه تابعي است که مقدارش در نقطه ي X برابر x است.نمونه ي آشنا تر براي تعريف تابع يکه به شکل زير است:
I(x) = x
به هر حال، اين روش تعريف توابع ما را مجبور مي سازد که براي هر تابعي که تعريف مي کنيم اسمي در نظر بگيريم. حساب لامبدا اين امکان را ايجاد مي کند تا توابع بي نام ايجاد کنيم و از آنها در عبارات بزرگتر بهره ببريم. در نشان گذاري لامبدا مرسوم است که کاربرد لامبدا تنها با قرار دادن يک عبارت تابع در مقابل يک يا چند متغير انجام شود. استفاده از پرانتز دلخواه است. براي مثال، مي توانيم از تابع يکه براي عبارت M به شکل زير استفاده کنيم:
Please Login or Register to see this code
مقدار اين عبارت تابع يکه است که تابع M به عنوان ورودي به آن داده شده است، مشخصا نتيجه آن M خواهد بود. در نتيجه:
Please Login or Register to see this code
قسمتي از حساب لامبدا مجموعه اي از قوانين براي کاهش تساوي ها مانند مثال بالاست. نمونه اي ديگر از عبارت لامبدا به اين صورت است:
Please Login or Register to see this code
براي توابع f و g اين تابع ترکيب λx.f(g(x)) از توابع f و g را مي سازد. مي توانيم حساب لامبداي خالص را با اضافه کردن مجموعه اي از ساختارها گسترش دهيم. اين گسترش هاي حساب لامبداي خالص با عملکردهاي اضافي حساب لامبداي کاربردي ناميده مي شود. يک ايده ي پايه اي ارتباط بين حساب لامبدا و علوم کامپيوتر عبارت زير است:
زبان برنامه سازي = حساب لامبداي کاربردي = حساب لامبداي خالص + انواع داده ي اضافي.

[arashtabaie]

نحو عبارات:

نحو عبارات لامبداي بدون گونه مي تواند با يک گرامر BNF تعريف شود. فرض مي کنيم که مجموعه اي نامتناهي به نام V از متغييرها داريم و از x,y,z,… براي نمايش متغير هاي استفاده مي کنيم. گرامر براي عبارات لامبدا به شرح زير است:
M::= x|MM|λx.M
در صورتي که x ميتواند هر متغيري باشد(عضوي از V). يک عبارت با فرم M1M2 يک application ناميده مي شود و يک عبارت با فرم λx.M انتزاع لامبدا ناميده مي شود.متغير x اشاره به تابعي دارد که توسط زمينه مشخص شده است.M1M2 استفاده از تابع M1 با متغير M2 است.و λx.M تابعي است که با مقدار اوليه ي x مقدار M را باز مي گرداند. در ادبيات حساب لامبدا مرسوم است که به عبارات حساب لامبدا، عبارات لامبدا اتلاق شود.
بعضي عبارات لامبدا وجود دارند که براي متخصصان زبان کاملا جا افتاده اند ولي براي عموم بعضا گيج کننده است و يادگيري آن دشوار است.


Variable binding:

اتفاق يک متغير در يک عبارت مي تواند آزاد يا وابسته باشد.اگر يک متغير در يک عبارت آزاد باشد، اين به اين معنا است که متغير در اين عبارت تعريف نشده است. براي مثال، متغير x در در عبارت x+3 آزاد است . مقدار x+3 را به طو ر مستقل نمي توان بدون قرار دادن اين عبارت در عبارتي بزرگ تر که مقداري به x بدهد محاسبه کرد.
سمبل λ يک سمبل وابسته کننده است و يک متغير را وابسته به يک قسمت از يک عبارت مي کند. متغير X در λx.M يک متغير وابسته است.اين بدان معني است که x تنها يک جانگهدار است. مي توان x را با متغيري مثل y بدون تغيير معني عبارت جايگزين کرد. يعني λx.x همان تابعي را تعريف مي کند که λy.y. عباراتي که تنها در نام متغيرهاي وابسته با هم تفاوت دارند هم تراز آلفا خوانده مي شوند.
در λx.M عبارت M حوزه ي وابستگي λx ناميده ميشود. متغير x که در يک عبارت ظاهر مي شود، وابسته است اگر و فقط اگر در حوزه ي يک λx قرار بگيرد و در غير اين صورت آزاد است. براي اينکه دقيق تر باشيم، مي توانيم مجموعه ي FV(M) را به صورت مجموعه ي عناصر آزاد M تعريف کنيم.


تساوي و جابجايي:

قبل از اين به تساوي آلفا اشاره شده است که يکي از اصول حساب لامبداست. سامانه ي اثبات تساوي حساب لامبدا به قاعده ي زير است:
λx.M = λy.[y/x]M
که y نبايد قبلا در M به کار رفته باشده و [x/y] به معني تعويض تمام اتفاق افتادن هاي آزاد x با y در M است. سه قاعده تساوي ديگر و چهار قانون استنتاجي براي اثبات تساوي دو عبارت وجود دارد. در اينجا تنها به يک قاعده ي تساوي ديگر اشاره مي شود.
قاعده ي مرکزي تساوي در حساب لامبدا براي محاسبه ي مقدار استفاده ي يک تابع روي متغير ها با جابجايي صورت مي گيرد. به اين علت که λx.M تابعي است که از فرض اينکه M تابعي از X است به دست مي آوريم، مي توان مقدار تابع M را بر اساس N با جابجا کردن X با N به دست آورد. داريم:
(λx.M)N = [N/x]M
که قاعده ي تساوي بتا ناميده مي شود.


تغيير نام متغيرهاي وابسته:

به اين علت که وابستگي هاي λ در M ممکن است با متغير هاي وابسته در N ناهماهنگي ايجاد کند، جابجايي [N/x]M از چيزي که در ابتدا به نظر مي رسد پيچيده تر است. به هر حال، مي توانيم از اين ناهماهنگي ها با استفاده از قراردادهاي استفاده از متغيرها پيشگيري کنيم: تغيير نام ومتغيرهاي وابسته درx.M)N (λ به صورتي که نام تمام متغيرهاي وابسته و آزاد با هم متفاوت باشد.

[arashtabaie]

برنامه سازي با استفاده از حساب لامبدا:

مي توان به حساب لامبدا به عنوان يک زبان ساده ي برنامه سازي تابعي نگاه کرد. در عين حال که اين زبان بسيار ساده است، در صورت استفاده از برخي اختصارات مي توان به راحتي با لامبدا برنامه سازي کرد. در ادامه به مسئله ي توابع با چندين ورودي اشاره مي شود.


توابع با چند ورودي
تجريد لامبدا اين امکان را به ما مي دهد که با هر عبارت M مانند با شکل نحوي λx.M به عنوان يک تابع برخورد کنيم. در صورت احتياج به استفاده از چند متغير براي تابع هيچ احتياجي به اضافه کردن عملگر λ اضافي وجود ندارد.
تابعي مانند f با دو متغير به شکل تابعي تک متغيره با شکل λx.(λy.M) تعريف مي¬شود و به اين صورت است که در ابتدا تابع تک متغيره با متغير اول مقدار بر مي گرداند و اين مقدار، يک تابع است که متغير دوم را مي گيرد.
اين ايده ي ساده توسط شونفينکل در سال 1920 ابداع شد. اين تکنيک به نام هاسکل کاري، از اولين دانشمنداني که روي حساب لامبدا کار کرد، کارينگ ناميده مي شود.

تعريف توابع
براي عبارات لامبدا اختصار زير را به کار مي بريم:
Let x = M in N = (λx.N)M
ساختار let ممکن است در تعريف توابع ترکيبي استفاده شود. مانند:
Let compose = λf.λg.λx.f(gx) in compose h h
با استفاده از تساوي بتا مي توان عبارت فوق را به شکل λx.h(hx) خلاصه کرد.

بازگشت و نقاط ثابت
حقيقتي جالب راجع به حساب لامبداي خالص اين است که مي توان با استفاده از يک حقه، توابع بازگشتي در اين زبان نوشت.
بسياري از زبان هاي برنامه سازي اجازه ي تعريف توابع بازگشتي را به برنامه ساز مي دهند. خصوصيت يک تعريف بازگشتي از يک تابع اين است که بدنه ي تابع تعدادي (يک يا بيشتر از يک) فراخواني خود تابع f دارد. براي انتخاب يک نمونه فرض مي کنيم تعريف تابع فاکتوريل را در يک زبان دلخواه به صورت زير نوشته ايم:
Function f(n) {if n=0 then 1 else n*f(n-1)}
که در آن بدنه ي تابع عبارت درون آکولاد است. اين تعريف، تفسير بسيار ساده اي از اين تابع به دست مي دهد: وقتي f با متغير a فراخواني مي شود، پارامتر n تابع با a جايگزين مي شود و مقدار تابع با آن محاسبه مي شود. اگر محاسبه ي مقدار تابع به فراخواني بازگشتي تابع مي رسد، اين پروسه تکرار مي شود. براي رسيدن به يک تعريف بازگشتي در حساب لامبدا بايد مرابطه ي يک تساوي با بازگشت را به دست بياوريم. براي مثال مي توانيم تساوي زير را با تعريف بازگشتي قبلي عوض کنيم:
F(n) = if n = 0 then 1 else n*f(n-1)
اين تساوي يک خاصيت فاکتوريل را نمايش مي دهد. مقدار عبارت f(n) مساوي مقدار عبارت بالاست وقتي که f يک تابع فاکتوريل باشد. حساب لامبدا روشي براي يافتن راه حل براي تساوي هايي است که در آنها يک مشخص کننده )در اينجا نام تابع بازگشتي) در دوطرف تساوي به چشم مي خورد.
مي توانيم به سادگي تساوي فوق را با تجرد لامبدا براي حذف n از سمت چپ تساوي نمايش دهيم.
F=λn. If n=0 then 1 else n*f(n-1)
حال تابع G را در نظر بگيريد که با حرکت دادن F به سمت راست تساوي به دست آمده است.
G=λf.λn. if n=0 then 1 else n*f(n-1)





منبع : concepts in programming languages by : john c. Mitchell , Stanford university

استفاده از این مطلب بدون ذکر نام مرکز انجمن های تخصصی مخالف اخلاقیات است.

[atousamehr]

سلام
میشه روند ارسال با نام به کمک حساب لامبدا رو توضیح بدید
متشکرم