حساب لامبدا یک سیستم رسمی در منطق ریاضی برای بیان محاسبات مبتنی بر انتزاع و اعمال توابع با استفاده از اتصال و جایگزینی متغیر است. این یک مدل جهانی است که می تواند در طراحی هر ماشین تورینگ اعمال شود. حساب لامبدا برای اولین بار توسط چرچ، ریاضیدان مشهور، در دهه 1930 معرفی شد.
سیستم از ساخت اعضای لامبدا و انجام عملیات کاهش بر روی آنها تشکیل شده است.
توضیحات و کاربردها
حرف یونانی lambda (λ) در عبارات لامبدا و اصطلاحات لامبدا برای نشان دادن اتصال یک متغیر در یک تابع استفاده می شود.
حساب لامبدا را می توان غیر تایپ یا تایپ کرد. در نوع اول، توابع تنها در صورتی قابل استفاده هستند که بتوانند داده هایی از این نوع را دریافت کنند. محاسبات لامبدا تایپ شده ضعیف تر هستند، می توانند مقدار کمتری را بیان کنند. اما، از سوی دیگر، آنها به شما اجازه می دهند چیزهای بیشتری را ثابت کنید.
یکی از دلایل وجود انواع مختلف این است که میل دانشمندان به انجام کارهای بیشتر بدون از دست دادن فرصت اثبات قضایای محاسباتی قوی لامبدا است.
این سیستم در بسیاری از زمینه های مختلف ریاضیات، فلسفه، زبان شناسی و علوم کامپیوتر کاربرد دارد. اول از همه، حساب لامبدا، حسابی است که نقش مهمی در توسعه تئوری زبان های برنامه نویسی داشته است. این سبک های ایجاد عملکردی است که سیستم ها اجرا می کنند. آنها همچنین موضوع داغ تحقیق در تئوری این دسته بندی ها هستند.
برای آدمک ها
حساب لامبدا توسط ریاضیدان آلونزو چرچ در دهه 1930 به عنوان بخشی از تحقیقات او در زمینه مبانی علم معرفی شد. سیستم اصلی در سال 1935 زمانی که استفن کلین و جی بی راسر پارادوکس کلین-روسر را توسعه دادند از نظر منطقی ناسازگار بود.
بعداً، در سال 1936، چرچ تنها بخشی را که مربوط به محاسبات است، که امروزه حساب لامبدای تایپ نشده نامیده می شود، جدا و منتشر کرد. در سال 1940 او همچنین یک نظریه ضعیف‌تر اما از نظر منطقی سازگار به نام سیستم نوع اول را معرفی کرد. او در کار خود کل نظریه را به زبان ساده توضیح می دهد، بنابراین می توان گفت که چرچ حساب لامبدا را برای آدمک ها منتشر کرد.
تا دهه 1960، زمانی که رابطه آن با زبان های برنامه نویسی مشخص شد، λ فقط یک فرمالیسم بود. به لطف کاربردهای ریچارد مونتاگو و دیگر زبان شناسان در معناشناسی زبان طبیعی، حساب دیفرانسیل و انتگرال جایگاه خود را هم در زبان شناسی و هم در علوم کامپیوتر به خود اختصاص داده است.
منشا نماد
لامبدا مخفف یک کلمه یا مخفف نیست، بلکه از یک مرجع در ریاضیات اصلی راسل و به دنبال آن دو تغییر تایپی آمده است. مثال علامت گذاری: برای یک تابع f با f (y)=2y + 1 برابر است با 2ŷ + 1. و در اینجا از یک caret ("hat") روی y برای برچسب گذاری متغیر ورودی استفاده می کنیم.
کلیسا در ابتدا قصد داشت از نمادهای مشابه استفاده کند، اما حروفچین ها نتوانستند نماد "کلاه" را بالای حروف قرار دهند. بنابراین در عوض آنها آن را در اصل به صورت "/\y.2y+1" چاپ کردند. در قسمت بعدی ویرایش، تایپیست‌ها "/ \" را با یک کاراکتر شبیه بصری جایگزین کردند.
مقدمه ای بر حساب لامبدا
سیستم متشکل از زبانی از اصطلاحات است که توسط یک نحو رسمی خاص انتخاب می شوند و مجموعه ای از قوانین تبدیل که امکان دستکاری آنها را فراهم می کند. آخرین نکته را می توان به عنوان یک نظریه معادله یا به عنوان یک تعریف عملیاتی در نظر گرفت.
همه توابع در حساب لامبدا ناشناس هستند، به این معنی که نام ندارند. آنها فقط یک متغیر ورودی را می گیرند، و Currying برای پیاده سازی نمودارهایی با چندین متغیر استفاده می شود.
شرایط لامبدا
نحو حساب دیفرانسیل و انتگرال برخی از عبارات را معتبر و برخی دیگر را نامعتبر تعریف می کند. درست مانند رشته‌های مختلف کاراکترها، برنامه‌های C معتبر هستند و برخی معتبر نیستند. بیان واقعی حساب لامبدا را اصطلاح لامبدا می نامند.
سه قانون زیر یک تعریف استقرایی ارائه می دهد که می تواند باشدبرای ساخت همه مفاهیم صحیح نحوی اعمال شود:
متغیر x خود یک اصطلاح لامبدا معتبر است:
- اگر T LT باشد و x غیر ثابت باشد، آنگاه (lambda xt) یک انتزاع نامیده می شود.
- اگر T و همچنین s مفاهیم باشند، آنگاه (TS) یک برنامه کاربردی نامیده می شود.
هیچ چیز دیگری اصطلاح لامبدا نیست. بنابراین، یک مفهوم در صورتی معتبر است که بتوان آن را با اعمال مکرر این سه قاعده به دست آورد. با این حال، برخی از براکت ها ممکن است بر اساس معیارهای دیگر حذف شوند.
تعریف
عبارات لامبدا عبارتند از:
- متغیرهای v 1, v 2, …, v n, …
- نمادهای انتزاع 'λ' و نقطه '.'
- پرانتز ().
مجموعه Λ را می توان به صورت استقرایی تعریف کرد:
- اگر x یک متغیر است، x ∈ Λ;
- x ثابت نیست و M ∈ Λ، سپس (λx. M) ∈ Λ;
- M، N ∈ Λ، سپس (MN) ∈ Λ.
تعیین
برای بی نظم نگه داشتن نماد عبارات لامبدا، معمولاً از قراردادهای زیر استفاده می شود:
- براکت های بیرونی حذف شده است: MN به جای (MN).
- فرض بر این است که برنامه‌ها به صورت ارتباطی باقی می‌مانند: می‌توان به جای ((MN) P MNP را نوشت.
- بدنه انتزاع بیشتر به سمت راست گسترش می یابد: λx. MN به معنای λx است. (MN)، نه (λx. M) N.
- توالی انتزاعات کاهش می یابد: λx.λy.λz. N می تواند λxyz. N. باشد.
متغیرهای آزاد و محدود
عملگر λ ناثابت خود را به هر کجای بدنه انتزاع متصل می کند. متغیرهایی که در محدوده قرار می گیرند محدود نامیده می شوند. در عبارت λ x. M، قسمت λ x اغلب به عنوان یک اتصال دهنده نامیده می شود. گویی اشاره می کند که متغیرها با اضافه کردن X x به M تبدیل به یک گروه می شوند. همه متغیرهای ناپایدار دیگر آزاد نامیده می شوند.
مثلاً در عبارت λ y. x x y، y - محدود غیر دائمی، و x - رایگان. و همچنین شایان ذکر است که متغیر بر اساس "نزدیکترین" انتزاع خود گروه بندی می شود. در مثال زیر، راه حل حساب لامبدا با یک رخداد واحد x نشان داده شده است که مربوط به جمله دوم است:
λ x. y (λ x. z x)
مجموعه متغیرهای آزاد M با FV (M) نشان داده می شود و با بازگشت بر ساختار اصطلاحات به صورت زیر تعریف می شود:
- FV (x)={x}، که در آن x یک متغیر است.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
فرمولی که حاوی متغیرهای آزاد نباشد بسته نامیده می شود. عبارات بسته لامبدا نیز به عنوان ترکیب‌کننده شناخته می‌شوند و معادل اصطلاحات در منطق ترکیبی هستند.
مخفف
معنای عبارات لامبدا با نحوه کوتاه کردن آنها تعیین می شود.
سه نوع برش وجود دارد:
- a-transform: تغییر متغیرهای کران (آلفا).
- β-reduction: اعمال توابع به آرگومان های آنها (بتا).
- η-transform: مفهوم گسترش پذیری را پوشش می دهد.
اینجا هم هستما در مورد معادل‌های حاصل صحبت می‌کنیم: اگر بتوان آنها را بتا به یک جزء تبدیل کرد، دو عبارت β-معادل هستند، و α/η-معادل به طور مشابه تعریف می‌شود.
اصطلاح redex که مخفف چرخش قابل کاهش است، به موضوعات فرعی اطلاق می شود که می توان آنها را با یکی از قوانین کاهش داد. حساب لامبدا برای آدمک‌ها، مثال‌ها:
(λ x. M) N یک بتا ریدکس در بیان جایگزینی N با x در M است. مؤلفه ای که یک ریدکس به آن کاهش می یابد، کاهش آن نامیده می شود. کاهش (λ x. M) N M است [x:=N].
اگر x در M آزاد نیست، λ x. M x همچنین em-REDEX با تنظیم کننده M.
آ-تغییر
تغییر نام آلفا به شما امکان می دهد نام متغیرهای محدود را تغییر دهید. به عنوان مثال، x. x می تواند λ y را بدهد. y اصطلاحاتی که فقط در تبدیل آلفا با هم تفاوت دارند، معادل α هستند. اغلب، هنگام استفاده از حساب لامبدا، معادل‌های α متقابل در نظر گرفته می‌شوند.
قوانین دقیق برای تبدیل آلفا کاملاً بی اهمیت نیستند. ابتدا با این انتزاع، تنها متغیرهایی که با یک سیستم مرتبط هستند تغییر نام می‌دهند. به عنوان مثال، تبدیل آلفا λ x.λ x. x می تواند منجر به λ y.λ x شود. x، اما این ممکن است به λy.λx.y منجر نشود. دومی معنای متفاوتی با اصلی دارد. این شبیه به مفهوم برنامه نویسی سایه متغیر است.
ثانیاً، تبدیل آلفا در صورتی امکان‌پذیر نیست که توسط یک انتزاع غیردائمی دیگر گرفته شود. برای مثال، اگر x را با y در λ x.λ y جایگزین کنید. x، سپس می توانید دریافت کنیدλy.λy. u، که اصلاً یکسان نیست.
در زبان های برنامه نویسی با دامنه ایستا، از تبدیل آلفا می توان برای ساده کردن وضوح نام استفاده کرد. در عین حال، مراقب باشید که مفهوم متغیر، نام را در ناحیه حاوی پنهان نکند.
در نماد نمایه De Bruyne، هر دو عبارت معادل آلفا از نظر نحوی یکسان هستند.
تعویض
تغییرات نوشته شده توسط E [V:=R] فرآیند جایگزینی تمام رخدادهای آزاد متغیر V در عبارت E با گردش مالی R است. جایگزینی بر حسب λ با لامبدا بازگشت تعریف می شود. محاسبه ساختار مفهومی به صورت زیر
x [x:=N] ≡ N
y [x:=N] ≡ y اگر x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] ≡ λ x. M
(λ y. M) [x:=N] y λ y. (M [x:=N]) اگر x ≠ y، به شرطی که y ∉ FV (N).
برای جایگزینی به یک انتزاع لامبدا، گاهی اوقات لازم است یک عبارت α-تبدیل شود. برای مثال، این درست نیست که (λ x. Y) [y:=x] منجر به (λ x. X) می شود زیرا x جایگزین باید آزاد می بود، اما در نهایت محدود می شد. جایگزینی صحیح در این مورد (λ z. X) تا α-هم ارز است. توجه داشته باشید که جایگزینی تا لامبدا منحصراً تعریف شده است.
β-کاهش
کاهش بتا منعکس کننده ایده اعمال یک تابع است. بتا-کاهشی در اصطلاح تعریف می شودجایگزینی: ((X V. E) E ') E [V:=E'] است.
مثلاً، با فرض کدگذاری 2، 7، ×، کاهش β زیر وجود دارد: ((λ n. N × 2) 7) → 7 × 2.
کاهش بتا را می توان همانند مفهوم تقلیل پذیری محلی تحت کسر طبیعی از طریق ایزومورفیسم Curry-Howard مشاهده کرد.
η-transform
این تبدیل ایده توسعه پذیری را بیان می کند، که در این زمینه این است که دو تابع زمانی که نتیجه یکسانی برای همه آرگومان ها به دست می دهند برابر هستند. این تبدیل بین λ x مبادله می شود. (F x) و f هر زمان که x در f آزاد به نظر نمی رسد.
این عمل را می توان همان مفهوم کامل بودن محلی در استنتاج طبیعی از طریق ایزومورفیسم کری-هاوارد در نظر گرفت.
اشکال عادی و همجوشی
برای حساب لامبدای نامشخص، قانون کاهش β معمولاً نه نرمال‌کننده قوی است و نه ضعیف.
با این وجود، می توان نشان داد که کاهش β هنگام اجرا قبل از تبدیل α با هم ادغام می شود (به عنوان مثال، اگر تبدیل α از یکی به دیگری امکان پذیر باشد، دو شکل عادی را می توان برابر در نظر گرفت).
بنابراین، هم اصطلاحات به شدت عادی و هم اصطلاحات با تنظیم ضعیف، یک شکل عادی دارند. برای اولین شرایط، هر استراتژی کاهش تضمین شده است که به یک پیکربندی معمولی منجر شود. در حالی که برای شرایط ضعیف نرمال کردن، برخی از استراتژی های کاهش ممکن است آن را پیدا نکنند.
روش های برنامه نویسی اضافی
اصطلاحات خلقت زیادی برای حساب لامبدا وجود دارد. بسیاری از آنها در اصل در زمینه استفاده از سیستم ها به عنوان مبنایی برای معناشناسی یک زبان برنامه نویسی توسعه یافته اند و به طور موثر آنها را به عنوان یک ساختار سطح پایین به کار می برند. از آنجایی که برخی از سبک ها شامل حساب لامبدا (یا چیزی بسیار مشابه) به عنوان یک قطعه هستند، این تکنیک ها در ایجاد عملی نیز کاربرد دارند، اما ممکن است به عنوان مبهم یا خارجی تلقی شوند.
ثابت نامگذاری شده
در حساب لامبدا، یک کتابخانه به شکل مجموعه ای از توابع تعریف شده قبلی است، که در آن عبارت ها فقط ثابت های مشخص هستند. حساب دیفرانسیل و انتگرال خالص مفهومی از تغییرناپذیرهای نامگذاری شده ندارد زیرا همه اصطلاحات لامبدای اتمی متغیر هستند. اما می‌توان آنها را با در نظر گرفتن متغیر تغییرپذیر به‌عنوان نام ثابت، استفاده از انتزاع لامبدا برای اتصال آن فرار در بدن، و اعمال آن انتزاع در تعریف مورد نظر تقلید کرد. بنابراین اگر از f برای نشان دادن M در N استفاده می کنید، می توانید بگویید
(λ f. N) M.
نویسندگان اغلب یک مفهوم نحوی را معرفی می کنند، مانند let to اجازه می دهد چیزها به روشی بصری نوشته شوند.
f=M تا N
با زنجیر کردن چنین تعاریفی، می توان یک "برنامه" حساب لامبدا را به صورت تعاریف صفر یا چند تابع و به دنبال آن یک عضو لامبدا، با استفاده از تعاریفی که بخش عمده ای از برنامه را تشکیل می دهند، نوشت.
یک محدودیت قابل توجه در این اجازه این است که نام f در M تعریف نشده است.از آنجایی که M خارج از محدوده الزام آور انتزاع لامبدا f است. این بدان معنی است که یک ویژگی تابع بازگشتی را نمی توان به عنوان M با let استفاده کرد. نحو پیشرفته‌تر letrec، که به شما امکان می‌دهد تعاریف تابع بازگشتی را در این سبک بنویسید، علاوه بر این از ترکیب‌کننده‌های نقطه ثابت به جای آن استفاده می‌کند.
آنالوگ های چاپ شده
این نوع یک فرمالیسم تایپ شده است که از یک نماد برای نمایش یک انتزاع تابع ناشناس استفاده می کند. در این زمینه، انواع معمولاً اشیایی با ماهیت نحوی هستند که به اصطلاحات لامبدا نسبت داده می شوند. ماهیت دقیق به حساب مورد نظر بستگی دارد. از یک دیدگاه خاص، LI تایپ شده را می توان به عنوان اصلاحات LI بدون تایپ در نظر گرفت. اما از سوی دیگر، آنها را می‌توان نظریه‌ای بنیادی‌تر نیز در نظر گرفت، و حساب لامبدا تایپ نشده یک مورد خاص با تنها یک نوع است.
Typed LI پایه و اساس زبان های برنامه نویسی و ستون فقرات زبان های کاربردی مانند ML و Haskell هستند. و به طور غیرمستقیم تر، سبک های ضروری خلقت. محاسبات لامبدا تایپ شده نقش مهمی در توسعه سیستم های نوع برای زبان های برنامه نویسی دارند. در اینجا، تایپ‌پذیری معمولاً ویژگی‌های مورد نظر برنامه را ثبت می‌کند، به عنوان مثال، باعث نقض دسترسی به حافظه نمی‌شود.
محاسبات لامبدا تایپ شده از طریق ایزومورفیسم کری-هاوارد ارتباط نزدیکی با منطق ریاضی و نظریه برهان دارند و می‌توان آن را به‌عنوان زبان داخلی کلاس‌های دسته‌بندی در نظر گرفت.به سادگی سبک بسته شدن دکارتی است.
