حساب لامبدا
کلیات

حساب لامبدا شامل زبانی از عناصر لامبدا است که با عناصر نحوی مشخص بیان می‌شود و هم چنین قانون‌های انتقال که به عناصر لامبدا اجازه دستکاری می‌دهد؛ که این قانون‌های انتقال در قضیه معدله‌ای و بیان عملیاتی استفاده می‌شود.
برای توضیح بالا تمام توابع در حساب لامبدا توابع ناشناس هستند؛ که فقط یک ورودی متغیر را می‌پذیرند؛ که با تابع کارینگ می‌توان چندین متغیر را به عنوان ورودی در نظر گرفت
عناصر لامبدا
نحو حساب لامبدا برای بیان متغیرهای معتبر و نامعتبر است برای رشته‌ای از کاراکترهای معتبر زبان و برنامه سی و نامعتبر آن. به حساب لامبدا معتبر عناصر لامبدا می‌گویند.
سه قانون زیر یک معنای القایی به ما می‌دهد که می‌تواند تمام نحو معتبر حساب لامبدا را شمال شود
متغیر xخود به تنهایی یک عناصر معتبر لامبدا است.
اگر t یک عنصر لامبدا و xیک متغیر باشد آنگاه. (λx.t) یک عنصر لامبدا است.
اگر tوsعناصر لامبدا باشند آنگاه (ts)عناصر لامبدا اسنت
هیچ عبارت دیگری عناصر لامبدا نیست؛ بنابراین عناصر لامبدا معتبر هستند اگر شامل تکرار قوانین بالا باشند. اگرچه بعضی از پرانتزگذاری‌ها با استفاده از این قوانین حذف شده‌است. به عنوان مثال پرانتز خارج از محدوده به صورت معمول نوشته نمی‌شودبه نشانه‌گذاری پایین دقت کنید
مفهوم یا برداشت لامبداx.tتوضیحی از توابع ناشناخته که این توانایی را دارد که ورودی xرا بگیرد و با tجایگزین کند بنابراین یک تابع ناشناخته را بیان می‌کند که xرا می‌گیرد و t را برمی‌گرداند. به عنوان مثال x.x2+2یک مفهوم از تابع f(x)=x2+2که از عناصر x2+2استفاده می‌کند تعریف تابع به همراه مفهوم لامبدا صرفاً تولید و تشکیل تابع است انا نه فراخوانی کردن آن. در کل پیوند متغیر xدر عنصر t.
برنامه ts بیان گر برنامه‌ای از تابع tبا ورودی sاست. باعث صدا زدن تابع tبا ورودی sبرای تولید t(s) می‌شود.
هیچ نظر و جنبه‌ای در حساب لامبدا برای اعلام متغیر نیست. با این تعریف مانند x.x+y(i.e. f(x)=x+y)می توان عنوان کرد. حساب لامبدا yرا متغیری عنوان می‌کند که هنوز مشخص و قابل تعریف نیست. مفهوم لامبدا x.x+yبه صورت نخوی معتبر است و هم چنین تابعی را تولید می‌کند که ورودی را با yکه هنوز ناشناخته هست جمع می‌کند.
Bracketingهم استفاده می‌شود و هم برای عناصر غیرضروری مورد نیاز است. به عنوان مثالλx.((λx.x)x) و(λx.(λx.x)) دو عنصر مختلف را بیان می‌کنند (اگرچه که هر دو اگر گاهش داده شوند به یک آرش و مقدار می‌رسند). اینجا اولین مثال برای معرفی تابع است که این معرفی تابع و برگرداندن نتیجه برای درخواست xاز تابع فرزندان به حساب می‌آید (درخواست تابع و بعد بازگشت) مثال دوم معرفی و تعیین تابع که تابعی را برمی‌گرداند که با هر ورودی کار می‌کند و در آخر برنامهxرا برمی‌گرداند (بازگشت تابع و بعد از درخواست)
توابعی روی توابع دیگر کار می‌کنند
در حساب لامبدا توابع در واقع همان کلاس اول با ارزش بالا هستند پس ممکن است توابع به عنوان ورودی گرفته شوند یا به عنوان خروجی از بقیه توابع.
به عنوان مثال λx.x نماینده‌ای برای معرفی تابع x=xو (λx.x)yنماینده تابعی کهyرا درخواست می‌کند. اگرچه(λx.y)تابع ثابت x=yرا بیان می‌کند تابعی که همیشه yرا برگرداند برای ورودی مشکلی ندارد. در حساب لامبدا برنامه توابع به نوان وابسته چپ در نظر گرفته شده‌است پس stxبه معنای (st)xمی‌باشد.
ایده‌های متفاوتی برای همبستگی و کاهش وجود دارد که عناصر لامبدا به عناصر وابسته لامبدا کاهش پیدا کنند.
همبستگی آلفا
اساس همبستگی که روی عناصر لامبدا قابل تعریف است را همبستگی آلفا گویند. بینشی برای انتخاب مشخص در محدوده متغیر را می‌گیرد که در مفهوم لامبدا مشکلی با این تعریف نیست. به عنوان مثال mx.xوmy.yدو همبستگ=ی آلفا از عناصر لامبدا هستند و هر دو نماینده یک تابع می‌باشند (تابع مشخص شده). دو عنصر xوyهمبستگی آلفا ندارند زیرا در محدوده مفهوم لامبدا قرار نگرفته‌اند. در بسیاری از بیانات پیدا کردن همبستگی آلفا با عناصر لامبدا کاری معمول و رایج است.
پیدا کردن بسیار مهم‌تر از پیدا کردن کاهش بتا است.
متغیرهای آزاد
متغیرهای آزاد برای یک عنصر متغیرهایی است که در محدوده مفهوم لامبدا نباشند. متغیرهای آزاد این‌گونه معرفی می‌شوند
متغیر آزاد xهمان x است.
متغیر آزاد λx.tهمان متغیر آزاد t است اما زمانی که xحذف شود.
متغیر آزاد tsدر واقع همان متغیر آزاد tو متغیر آزاد s است.
به عنوان مثال نماینده عناصر لامبدا که به این هویت و نشانه استλx.xمتغیر آزادی ندارد اما تابع λx.yxیک متغیر آزاد به نام yدارد.
جلوگیری از جایگزینی کردن
فرض کنید tوsوrعناصر لامبدا باشند و xوyمتغیر باشند. این نشانه‌گذاری t[x:=r]بان جایگزینی rبرایxدر tبا شیوه جلوگیری از گرفتن است؛ که به این شرح است.
X[x:=r]=r
Y[x:=r]=y if x≠y
(ts)[x:=r]=(t[x:=r])(s[x:=r])
(mx.t)[x:=r]=mx.t
(my.t)[x:=r]=my.(t[x:=r]) if x≠y و هم چنین yجز متغیر آزاد rبه حساب نمی‌آید.. متغیر yبه r درخواست نو شدن می‌دهد.
به عنوان مثال (mx.x)[y:=y]=mx.(x[y:=y])=mx.x و((mx.y)[x:=y])=((mx.y)(x[x:=y])=(mx.y)y.
نو شدن شرایط (به اینکه y از متغیرهای آزاد r نباشد احتیاج دارد) حیاتی تر از اطمینان یافتن است زیرا جایگزینی نباید معنی تابع را تغییر دهد. به عنوان مثال جایگزینی از شرایط نو چشم پوشی می‌کند(λx.y)
[y:=x]= λx.(y[y:=x])= λx.xکه این جایگزینی تابع ثابت λx.yبه λx.xاست.
در کل دیدن شرایط نو که به وسیله تغییر نام آلفا همراه با متغیرهای تازه تصفیه شده باشد با شکست رو به رو می‌شود به عنوان مثال رفتن به عقب برای جایگزینی صحیح در (λx.y)[y:=x]مفهوم لامبدا با متغیر تازه zتغییر نام داده‌است که شامل(λz.y)[y:=x]= λz.(y(y:=x])= λz.xکه یعنی تابع با جایگزینی حفظ شده‌است.
کاهش بتا
قانون کاهش بتا برنامه‌ای است برای فرم (λx.t)sکه به t[x:=s]کاهش پیدا کرده‌است. نشانه‌گذاری (λx.t)s=t[x:=s]که استفاده می‌شود تا نشان دهد (λx.t)sکاهش بتا در t[x:=s]به عنوان مثال برای تمام s(λx.x)s=x[x:=s]=sکه این عبارت نشان می‌دهد که λx.xشناخته شده‌است. هم چنین (λx.y)sy[x:=s]=y نشان می‌دهد که λx.yیک تابع ثابت است.
حساب لامبدا در واقع یک ورژن ایدئال از یک زبان برنامه‌نویسی تابعی است به مانند Haskellیاstandard ML. علاوه بر این کاهش بتا با محاسبات تطابق دارد. این گام می‌تواند به وسیله تبدیل بتا اضافی تکرار شود تا زمانی که برنامه‌ای برای کاهش وجود نداشته باشد. در حساب لامبدا نانوشته که در این‌جا وجود دارد که این کار کاهش را خاتمه نمی‌دهد. برای مثال فرض کنید عنصرλx.xx)(λx.xx))=Ωکه در اینجا(λx.xx)(λx.xx)=(xx)[x:= λ x.xx]=(x[x:= λx.xx])(x[x:= λx.xx])=(λx.xx)(λx.xx)در اینجا نصر به خودش کاهش پیدا می‌کند با استفاده از کاهش بتا و هم چنین عمل کاهش هیچ وقت خاتمه پیدا نمی‌کند.
جنبه دیگر حساب لامبدا نانوشته تشخیص داده‌های مختلف را نمی‌دهد. به عنوان مثال مطلوب است که که تابعی که فقط با اعداد کار دارد نوشته شود. اگرچه حساب لامبدا نانوشته راهی برای جلوگیری از بیان ارزش درست و رشته هاو شی‌های بدون اعداد ندارد
تعریف رسمی
تعریف
عبارات لامبدا عبارتند از:
متغیرهای v1، v2، …، vn، ...
نمادهای انتزاعی lambda ،' λ 'و نقطه '.' است.
پرانتز ()
مجموعه‌ای از عبارات لامبدا، Λ، می‌تواند به صورت القایی تعریف شود:
اگر x یک متغیر باشد، پس x ∈ Λ
اگر x یک متغیر و M ∈ Λ باشد، (λx.M) ∈ Λ
اگر M, N ∈ Λ، و سپس (M N) ∈ Λ
نمونه‌هایی از قانون ۲ به عنوان انتزاع و نمونه‌هایی از قانون ۳ به عنوان برنامه‌های کاربردی شناخته می‌شوند
نشانه گذاری
برای حفظ نشانه‌ای از عبارات لامبدا بدون سر و صدا، معمولاً قراردادهای زیر اعمال می‌شود:
پرانتز خارج از محدوده کاهش می‌یابد: M N به جای (M N)
فرض می‌شود که برنامه‌های کاربردی باقی می‌مانند: M N P ممکن است به جای ((M N) P)
بدن انتزاع به همان اندازه که ممکن است به سمت راست گسترش می‌یابد: λx.M N معنی λx.(M N) و نه (λx.M) N
یک دنباله از انتزاع قرارداد: λx. λy. λz.N به اختصار λxyz.N می‌باشد
متغیرهای آزاد و محدود
گفته می‌شود که اپراتور انتزاعی، λ، متغیر آن را هر جا که در انتهای انتزاع رخ می‌دهد، مرتبط کند. گفته می‌شود متغیرهایی که در محدوده یک انتزاع قرار می‌گیرند محدود می‌شوند. همه متغیرهای دیگر نامیده می‌شوند. به عنوان مثال، در عبارت زیر، یک متغیر محدود و x آزاد است: λy.x x y. همچنین توجه داشته باشید که یک متغیر با انتزاع «نزدیکترین» آن محدود شده‌است. در مثال زیر، وقفه تک x در بیان توسط لامبدا دوم محدود می‌شود: λx.y (λx.z x)
مجموعه‌ای از متغیرهای آزاد بیان Lambda, M، به عنوان FV (M) تعریف شده‌است و توسط بازگشتی بر ساختار اصطلاحات تعریف شده‌است، به شرح زیر است:
FV(x) = {x}, where x is a variable
FV(λx.M) = FV(M) \ {x}
3. FV(M N) = FV(M) ∪ FV(N)
گفته می‌شود که عبارت ای که حاوی هیچ متغیر آزاد نیست بسته می‌شود. عبارت lambda بسته نیز به عنوان ترکیبی شناخته می‌شود و معادل آن‌ها در منطق ترکیبی است.
کاهش
معنای عبارات لامبدا به این معناست که چگونه عبارات را می‌توان کاهش داد.
سه نوع کاهش وجود دارد:
α تبدیل: تغییر متغیرهای متناوب (آلفا).
β-reduction: اعمال توابع به استدلال‌های آن‌ها (بتا).
η-conversion: که مفهوم گسترش (eta) را ترسیم می‌کند.
ما همچنین از معادلات حاصل می‌گوییم: دو عبارات β-معادل هستند، اگر آن‌ها می‌توانند β-تبدیل به یک عبارت مشابه باشند، و α / η-هم‌ارزی به‌طور مشابه تعریف می‌شوند.
اصطلاح redex، کوتاهی برای عبارت reducible refers to subterms که می‌تواند توسط یکی از قوانین کاهش کاهش یابد. به عنوان مثال (λx.M) N یک بتا-redex در بیان جایگزینی N برای x در M است؛ اگر x در M آزاد نباشد، λx.M x نیز eta-redex است. بیان که بازده کاهش می‌یابد، کاهش آن نامیده می‌شود؛ با استفاده از مثال قبلی، کاهش این عبارات به ترتیب M [x: = N] و M.
α تبدیل
تبدیل آلفا، که گاهی اوقات به عنوان تغییر نام آلفا شناخته می‌شود، نام نام متغیر را تغییر می‌دهد. به عنوان مثال، تبدیل آلفا λx.x ممکن است λy.y. شرایطی که فقط با تبدیل آلفا متفاوت هستند، معادل α نامیده می‌شوند. اغلب، در استفاده از محاسبات لامبدا، معادلات معادل α معادل است.
قوانین دقیق برای تبدیل آلفا کاملاً بی‌اهمیت نیستند. اول، هنگامی که تبدیل آلفا یک انتزاع، تنها رخ داده‌های متغیر که تغییر نام داده‌اند، کسانی هستند که به یک انتزاع متعهد هستند. به عنوان مثال، تبدیل آلفا λx. λx.x می‌تواند به λy. λx.x منجر شود، اما نمی‌تواند نتیجه λy. λx.y. این دومین معنای متفاوت از اصل دارد.
دوم، تبدیل آلفا امکان‌پذیر نیست اگر یک متغیر با یک انتزاع متفاوت گرفته شود. برای مثال، اگر x را با y در λx. λy.x جایگزین کنیم، می‌توانیم λy. λy.y را به دست آوریم که کاملاً متفاوت نیست.
در زبان‌های برنامه‌نویسی با محدوده استاتیک، تبدیل آلفا می‌تواند برای ایجاد وضوح نام ساده‌تر با اطمینان از اینکه نام متغیر یک نام را در دامنه حاوی مخفی می‌کند (نگاه کنید به تغییر نام آلفا برای ایجاد وضوح نام نامطلوب).
در نماد شاخص De Bruijn، هر دو اصطلاح معادل آلفای معادل به صورت همگانی یکسان هستند.
جایگزینی
تعویض، نوشته شده E [V: = R]، فرایند جایگزینی تمام رخدادهای آزاد متغیر V در عبارت E با بیان R است. تعویض در شرایط λ-calculus توسط بازگشتی بر ساختار اصطلاحات تعریف شده‌است، همان‌طور که به این ترتیب (توجه داشته باشید: x و y فقط متغیر هستند در حالی که M و N هر عبارت λ هستند).
x[x := N]       ≡ N
y[x := N]       ≡ y, if x ≠ y
(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])
(λx.M)[x := N]  ≡ λx.M
(λy.M)[x := N]  ≡ λy.(M[x := N]), if x ≠ y, provided y ∉ FV(N)
برای جایگزینی به یک انتزاع لامبدا، گاهی لازم است که بیان α تبدیل شود. به عنوان مثال، برای (λx.y) [y: = x] درست نیست (به خاطر آوردن (λx.x)، زیرا x جایگزین به صورت آزاد بود اما به پایان رسید. جایگزینی صحیح در این مورد (λz.x)، تا α-هم‌ارزی است. توجه داشته باشید که تعویض به صورت منحصر به فرد به α-هم‌ارزی تعریف شده‌است.
β-کاهش
کاهش بتا ایده برنامه کاربردی را ضبط می‌کند. بتا-کاهش از نظر جایگزینی تعریف می‌شود: کاهش بتا
((λV.E) E ') E [V: E] است.
به عنوان مثال، با فرض برخی از کدگذاری ۲، ۷، ×، ما کاهش زیر را داریم: ((λn.n × ۲) ۷) → ۷ × ۲.
η-تبدیل
Eta-conversion بیان عقلی را بیان می‌کند که در این چارچوب این است که دو توابع یکسان هستند اگر و فقط اگر آن‌ها نتایج مشابهی را برای تمام استدلال‌ها ارائه دهند. Eta-conversion بین λx (fx) و f تبدیل می‌کند هر زمان که x در فضای آزاد ظاهر نشود.
اشکال طبیعی و همپوشانی
برای محاسبه لامبدا ty، β-reduction به عنوان یک قانون بازنویسی نه به شدت نرمال و نه ضعیف نرمال کردن است.
با این حال، می‌توان نشان داد که β-reduction با هم مخلوط است. (البته، ما به آلفا تبدیل می‌پردازیم، یعنی ما دو عددی معمول را در نظر می‌گیریم، اگر ممکن است به α-تبدیل یک به دیگری تبدیل شود)
بنابراین، هر دو اصطلاح به شدت نرمال و شرایط ضعیف عادی، یک فرم طبیعی منحصر به فرد دارند. برای اصطلاحات به شدت نرمال، هر استراتژی کاهش تضمین می‌شود که فرم طبیعی را تولید کند، در حالی که برای اصطلاحات ضعیف نرمال، برخی از استراتژی‌های کاهش می‌توانند آن را پیدا نکنند.
انواع داده‌ها کدگذاری
مقالات اصلی: رمزگذاریchurch و کدگذاری مگنسن اسکات
محاسبات پایه لامبدا ممکن است برای مدل‌سازی بولی‌ها، ریاضیات، ساختار داده‌ها و رکود استفاده شود، که در زیر بخش‌های زیر نشان داده شده‌است.
ریاضی در محاسبات لامبدا
چندین روش ممکن برای تعریف اعداد طبیعی در محاسبات لامبدا وجود دارد، اما اکثر عبارات church هستند که می‌توانند به صورت زیر تعریف شوند:
۰ := λf. λx.x
۱ := λf. λx.f x
۲ := λf. λx.f (f x)
۳ := λf. λx.f (f (f x))
و غیره یا با استفاده از نحوه جایگزین ارائه شده در بالا در نماد:
۰ := λfx.x
۱ := λfx.f x
۲ := λfx.f (f x)
۳ := λfx.f (f (f x))
یک عدد church یک تابع مرتبه بالاتر است - یک تابع یک پارامتر تابع f را می‌گیرد و یک تابع تک استدلالی را بازمی‌گرداند. عدد n عنصر کلیسا یک تابع است که یک تابع f را به عنوان علامت می‌گیرد و ترکیب n-th f را به دست می‌دهد، یعنی تابع f با خود برابر n برابر است. این نشان دهنده f (n) است و در واقع n-th power f است (در نظر گرفته شده به عنوان یک اپراتور)؛ f (0) به عنوان تابع هویت تعریف می‌شود. چنین ترکیبات تکراری (از یک تابع f) به قوانین مادیات احترام می‌گذارند، به همین دلیل این عددها را می‌توان برای محاسبات استفاده کرد. (در محاسبات لامبدا اصلی کلیسای، پارامتر رسمی بیان لامبدا حداقل یکبار در بدن تابع اتفاق افتاد که تعریف فوق از ۰ غیرممکن بود).
ما می‌توانیم یک تابع جانشین را تعریف کنیم که یک عدد n را می‌گیرد و n + 1 را با اضافه کردن یک برنامه دیگر از f تعریف می‌کند، where '(mf) x' به معنی تابع 'f' است 'm' بار در 'x' اعمال می‌شود:
SUCC: = λn. λf. λx.f (n f x)
از آنجا که ترکیب m-th f با ترکیب n-th f به ترکیب m + n-th f می‌دهد، افزودن می‌تواند به صورت زیر تعریف شود:
PLUS: = λm. λn. λf. λx.m f (n f x)
PLUS را می‌توان به عنوان یک تابع در نظر گرفت که دو عدد طبیعی را به عنوان استدلال و بازگشت یک عدد طبیعی؛ می‌توان آن را تأیید کرد
PLUS 2 3
و
۵
عبارات لامبدا β معادل هستند. از آنجا که اضافه کردن m به عدد n می‌توان با اضافه کردن 1 m بار، تعریف معادل آن است: PLUS: = λm. λn.m SUCC n
به‌طور مشابه، ضرب می‌تواند به صورت زیر تعریف شود
MULT: = λm. λn. λf.m (n f)
متناوباً
MULT: = λm. λn.m (PLUS n) 0
از آنجا که ضرب m و n همانند تکرار تابع add n تابع m است و سپس آن را به صفر اعمال می‌کند. انحراف در عبارات church نسبتاً پیچیده‌است.
POW: = λb. λe.e b
عملکرد پیشینی تعریف شده توسط PRED n = n-1 برای یک عدد صحیح مثبت n و PRED 0 = ۰ به مراتب سخت‌تر است. فرمول
PRED: = λn. λf. λx.n (λg. λh.h (g f)) (λu.x) (λu.u)
می‌توان با نشان دادن الگویی که اگر T نامیده می‌شود (λg. λh.h (gf)), T (n) (λu.x) = (λh.h (f (n-1) (x))) برای n> 0. دو تعریف دیگر از PRED در زیر آمده‌است، یکی با استفاده از شرط و دیگری با استفاده از جفت. با عملکرد پیشین، تفریق ساده است. تعریف کردن
SUB: = λm. λn.n PRED m،
SUB m n بازده m - n زمانی که m> n و ۰ در غیر این صورت.
منطق و پیش فرض‌ها
به‌طور مشترک، دو تعریف زیر (به نام کلیسای booleans) برای مقادیر بولین TRUE و FALSE استفاده می‌شود:
TRUE: = λx. λy.x
FALSE: = λx. λy.y
(توجه داشته باشید که FALSE برابر با عدد صفر کلیسا است که در بالا تعریف شده‌است)
سپس با استفاده از این دو λ-term، می‌توانیم برخی از اپراتورهای منطقی را تعریف کنیم (این فقط فرمول‌های ممکن است؛ عبارات دیگر به همان اندازه صحیح هستند):
AND := λp. λq.p q p
OR := λp. λq.p p q
NOT := λp.p FALSE TRUE
IFTHENELSE := λp. λa. λb.p a b
اکنون می‌توانیم برخی از توابع منطقی را محاسبه کنیم، مثلاً:
و
TRUE FALSE
≡ (λp. λq.p q p) TRUE FALSE →β TRUE FALSE TRUE
≡ (λx. λy.x) FALSE TRUE →β FALSE
و ما می‌بینیم که عدد درست عدد برابر با FALSE است.
یک پیش‌فرض یک تابع است که مقدار boolean را بازمی‌گرداند. اساسی‌ترین اساسی ISZERO است، که اگر علامت آن عدد کلیسای عدد ۰ باشد، عدد را درست می‌کند، و علامت FALSE اگر علامت دیگری باشد، عدد کلیسای دیگری است:
ISZERO: = λn.n (λx.FALSE) درست است.
پیش فرض زیر تست می‌کند که آیا آرگومان اول کمتر از نسبت یا برابر با دوم است:
LEQ: = λm. λn.ISZERO (SUB m n)،
و از آنجا که m = n، اگر LEQ m n و LEQ n m باشد، ساختن پیش‌فرض برای برابری عددی ساده است.
در دسترس بودن پیش فرض‌ها و تعریف بالا از TRUE و FALSE، آن را مناسب برای بیان عبارات "if-then-else" در محاسبات لامبدا ایجاد کنید. برای مثال، تابع پیشینی را می‌توان به صورت زیر تعریف کرد:
PRED: = λn.n (λg. λk.ISZERO (g 1) k (PLUS (g k) 1)) (λv 0) 0
که می‌تواند با نشان دادن القاء الگویی که n (λg. λk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) تابع افزودن n - 1 برای n> 0 است.
جفت
یک جفت (2-tuple) را می‌توان از نظر TRUE و FALSE تعریف کرد، با استفاده از کلیسای رمزگذاری برای جفت‌ها. به عنوان مثال، PAIR جفت (x, y) را محاسبه می‌کند، FIRST اولین عنصر جفت را باز می‌کند و SECOND دوم را بازمی‌گرداند.
PAIR := λx. λy. λf.f x y
FIRST := λp.p TRUE
SECOND := λp.p FALSE
NIL := λx.TRUE
NULL := λp.p (λx. λy.FALSE)
یک لیست مرتبط را می‌توان به عنوان NIL برای لیست خالی یا PAIR یک عنصر و یک لیست کوچکتر تعریف کرد. آزمون NULL پیش‌فرض برای مقدار NIL. (به جای آن، با NIL: = FALSE، ساختار l (λh. λt. λz.deal_with_head_h_and_tail_t) (deal_with_nil) نیاز به یک آزمون NULL صریح را از بین می‌برد).
به عنوان مثال استفاده از جفت، تابع shift و increment کهm,n))به(n,n+1) می‌توان تعریف کرد به عنوان
Φ: = λx.PAIR (SECOND x) (SUCC (SECOND x))
که به ما اجازه می‌دهد تا شاید نسخه شفاف تابع سلف:
PRED: = λn.FIRST (n Φ (PAIR 0)).
ر کوردها و نقاط ثابت
همچنین نگاه کنید به: SKI حساب کاربری ترکیبی § خود برنامه‌ریزی و بازپخش
Recursion تعریف یک تابع با استفاده از تابع خود است. محاسبات لامبدا نمی‌تواند این را به‌طور مستقیم به عنوان برخی از نشانه‌های دیگر بیان کند: تمام توابع در محاسبات لامبدا ناشناس هستند، بنابراین ما نمی‌توانیم به یک مقدار که هنوز تعریف شده‌است، در داخل عبارت لامبدا تعریف کنیم که همان مقدار است. با این وجود، می‌توان از طریق برگزاری یک عبارت لامبدا برای بازگشت خود به عنوان ارزش استدلال خود، به عنوان مثال در (λx.xx) E. دریافت کرد.
تابع فاکتوریل F (n) را به صورت بازگشتی به وسیلهٔ تعریف می‌کنیم
F(n) = 1, if n = 0; else n × F(n − ۱)
در بیان لامبدا که برای نشان دادن این تابع است، پارامتر (به‌طور پیش‌فرض اول) فرض می‌شود که خودش را به عنوان مقدار خود دریافت می‌کند، به‌طوری‌که فراخوانی آن - استفاده از آن به یک استدلال - به مقدار بازگشتی تبدیل می‌شود؛ بنابراین برای رسیدن به بازگشت، استدلال در نظر گرفته شده به عنوان خود ارجاع (به نام r اینجا) همیشه باید در داخل بدن تابع در یک نقطه تماس منتقل شود:
G := λr. λn.(1, if n = 0; else n × (r r (n−۱)))
with r r x = F x = G r x to hold, so r = G and
F := G G = (λx.x x) G
خود نرم‌افزار در اینجا تکرار می‌کند، بیانگر لامبدا تابع را به فراخوانی بعدی به عنوان یک مقدار استدلال انتقال می‌دهد، و آن را در دسترس برای ارجاع و فراخوانی در آنجا قرار می‌دهد.
این را حل می‌کند اما نیاز به نوشتن هر تماس مجدد را به عنوان خود برنامه کاربردی دارد. ما می‌خواهیم یک راه حل عمومی بدون نیاز به نوشتن مجدد داشته باشیم:
G := λr. λn.(1, if n = 0; else n × (r (n−۱)))
with r x = F x = G r x to hold, so r = G r =: FIX G and
F := FIX G where FIX g := (r where r = g r) = g (FIX g)
so that FIX G = G (FIX G) = (λn.(1, if n = 0; else n × ((FIX G) (n−۱))))
با توجه به یک اصطلاح لامبدا با اولین آرگومان که نشانگر فراخوانی بازگشتی است (به عنوان مثال G در اینجا)، ترکیبی FIX نقطه ثابت یک بیان لامبدا خود تکراری را نشان می‌دهد که نشانگر تابع بازگشتی (در اینجا، F) است. این تابع به هیچ وجه نباید صریحاً به خود منتقل شود، زیرا خود تکرار به صورت پیشفرض تنظیم می‌شود، زمانی که آن ایجاد می‌شود، هر بار که آن را فراخوانی می‌شود؛ بنابراین بیان اصلی لامبدا (FIX G) در داخل خود، در نقطه تماس، دستیابی به خود ارجاع ایجاد می‌شود.
در حقیقت، بسیاری از تعاریف ممکن برای این اپراتور FIX، ساده‌ترین آن‌ها وجود دارد:
Y: = λg. (λx.g (xx)) (λx.g (xx))
در محاسبات لامبدا، Yg یک نقطه ثابت از g است، به عنوان گسترش به:
Y g
(λh.(λx.h (x x)) (λx.h (x x))) g
(λx.g (x x)) (λx.g (x x))
g ((λx.g (x x)) (λx.g (x x)))
g (Y g)
حالا، برای فراخوانی بازگشتی ما به تابع فاکتوریل، ما به سادگی می‌توانیم (Y G) n, where n تعدادی است که فاکتوریل را محاسبه می‌کنیم. به عنوان مثال، با توجه به n = ۴، این می‌دهد:
(Y G) 4
G (Y G) 4
(λr. λn.(1, if n = 0; else n × (r (n−1)))) (Y G) ۴
(λn.(1, if n = 0; else n × ((Y G) (n−۱)))) ۴
1, if ۴ = 0; else ۴ × ((Y G) (4−۱))
۴ × (G (Y G) (4−۱))
۴ × ((λn.(1, if n = 0; else n × ((Y G) (n−۱)))) (۴−۱))
۴ × (1, if ۳ = 0; else ۳ × ((Y G) (3−۱)))
۴ × (۳ × (G (Y G) (3−۱)))
۴ × (۳ × ((λn.(1, if n = 0; else n × ((Y G) (n−۱)))) (۳−۱)))
۴ × (۳ × (1, if ۲ = 0; else ۲ × ((Y G) (2−۱))))
۴ × (۳ × (۲ × (G (Y G) (2−۱))))
۴ × (۳ × (۲ × ((λn.(1, if n = 0; else n × ((Y G) (n−۱)))) (۲−۱))))
۴ × (۳ × (۲ × (1, if ۱ = 0; else ۱ × ((Y G) (1−۱)))))
۴ × (۳ × (۲ × (۱ × (G (Y G) (1−۱)))))
۴ × (۳ × (۲ × (۱ × ((λn.(1, if n = 0; else n × ((Y G) (n−۱)))) (۱−۱)))))
۴ × (۳ × (۲ × (۱ × (1, if ۰ = 0; else ۰ × ((Y G) (0−۱))))))
۴ × (۳ × (۲ × (۱ × (۱))))
۲۴
هر تابع تعریف بازگشتی را می‌توان به عنوان یک نقطه ثابت از برخی از تابع تعریف شده مناسب تعریف شده در تماس فراخوان با یک استدلال اضافی دیده می‌شود و بنابراین، با استفاده از Y، هر تابع تعریف بازگشتی را می‌توان به عنوان بیان لامبدا بیان کرد. به‌طور خاص، اکنون می‌توانیم تفکیک، ضرب و محاسبه مقادیر عدد طبیعی را به صورت مجزا تعریف کنیم.
شرایط استاندارد
اصطلاحات خاصی نام‌های رایج دارند:
I: = λx.x
K: = λx. λy.x
S: = λx. λy. λz.x z (y z)
B: = λx. λy. λz.x (y z)
C: = λx. λy. λz.x z y
W: = λx. λy.x y y
U: = λx. λy.y (x x y)
ω: = λx.x x
Ω: = ω ω
Y: = λg. (λx.g (xx)) (λx.g (xx))
محاسبات لامبدا تایپ شده
یک محاسبات لامبدا تایپ شده یک فرمالیسم تایپی است که از نماد لامبدا ({\ displaystyle \ lambda} \ lambda) برای انتساب تابع ناشناس استفاده می‌کند. در این زمینه، انواع معمولاً اشیاء طبیعت نحوی هستند که به شرایط لامبدا اختصاص دارند؛ نوع دقیق یک نوع بستگی به محاسبات دارد (نگاه کنید به انواع زیر). از دیدگاه خاص، محاسبات لامبدا تایپ شده را می‌توان به عنوان اصلاحاتی از محاسبات لامبدا غیرتصویر مشاهده کرد، اما از دیدگاه دیگر، آن‌ها همچنین می‌توانند تئوری بنیادی تر و محاسبات لامبدا با استفاده از یک مورد خاص با تنها یک نوع در نظر گرفته شوند.
زبان‌های تایپ شده لامبدا زبان‌های برنامه‌نویسی پایه هستند و پایه زبان‌های برنامه‌نویسی کارکردی مانند ML و Haskell و غیرمستقیم زبان‌های برنامه‌نویسی ضروری را تایپ می‌کنند. Calibles lambda تایپ شده نقش مهمی در طراحی سیستم‌های نوع زبان‌های برنامه‌نویسی بازی می‌کند. در اینجا typability معمولاً ویژگی‌های مطلوب برنامه را ضبط می‌کند، برای مثال برنامه باعث نقض دسترسی به حافظه نمی‌شود.
محاسبات لامبدا تایپ شده با منطق ریاضی و تئوری اثبات شده از طریق Isomorphism کاری-هوارد مرتبط هستند و می‌توان آن‌ها را به عنوان زبان داخلی کلاس‌های دسته‌بندی، به عنوان مثال محاسبات لامبدا به سادگی تایپ شده‌است زبان رده بسته دکارتی (CCCs).
توابع قابل محاسبه و محاسبات لامبدا
یک تابع F: N → N از اعداد طبیعی یک تابع قابل محاسبه است اگر و فقط اگر یک عبارت lambda f وجود دارد به‌طوری‌که برای هر جفت x, y در N, F (x) = y اگر و فقط اگر fx = β y، جایی که x و y عددهای church مربوط به x و y هستند و به ترتیب β = β معادل بودن با کاهش بتا است. این یکی از روش‌های بسیاری برای تعریف محاسبات است. دیدگاه کلیسون تورینگ را برای بحث در مورد رویکردهای دیگر و همسانیشان ببینید.
عدم قطعیت برابر بودن
هیچ الگوریتمی وجود ندارد که به عنوان ورودی دو علامت لامبدا و خروجی TRUE یا FALSE را در نظر بگیرد که آیا دو عبارت برابر هستند یا نه. این مسئله از لحاظ تاریخی اولین مشکل بود که قابل اثبات نیست. همان‌طور که برای اثبات غیرقابل انکار بودن معمول است، اثبات نشان می‌دهد که هیچ تابع قابل محاسبه نمی‌تواند همسان‌سازی را تعیین کند. سپس پایان‌نامه کلیسا به نشان می‌دهد که هیچ الگوریتمی نمی‌تواند این کار را انجام دهد.
اثبات کلیسا برای اولین بار مشکل را برای تعیین اینکه آیا یک لامبدا داده شده به شکل نرمال است، کاهش می‌دهد. یک فرم عادی بیان معادل است که نمی‌تواند تحت قوانینی که توسط فرم اعمال می‌شود کاهش یابد. سپس فرض می‌کند که این پیش‌فرض قابل محاسبه است و بنابراین می‌تواند در محاسبات لامبدا بیان شود. بر اساس کار قبلی Kleene و ساخت شماره Gödel برای عبارات لامبدا، او یک عبارت لامبدا را ایجاد می‌کند که دقیقاً به اثبات اولین قضیه ناقص گودل می‌رسد. اگر e به شماره Gödel خود اعمال شود، یک تضاد حاصل می‌شود.
محاسبات لامبدا و زبان‌های برنامه‌نویسی
همان‌طور که توسط مقاله پیتر لندن در سال ۱۹۶۵ ذکر شده‌است A Correspondence between ALGOL 60 and Lambda-notation کلیسا، زبان برنامه‌نویسی رویه‌های متوالی را می‌توان از طریق محاسبات لامبدا، که مکانیسم اولیه برای انتزاع رویه و برنامه (زیر برنامه) کاربرد را فراهم می‌کند.
توابع ناشناس
به عنوان مثال، در Lisp تابع 'مربع' می‌تواند به صورت بیان lambda به صورت زیر بیان شود:
(لامبدا (x) (* x x))
مثال فوق یک عبارت است که به یک تابع کلاس اول ارزیابی می‌شود. نماد lambda تابع ناشناس ایجاد می‌کند، با توجه به لیستی از نام‌های پارامتر، (x) - فقط یک آرگومان در این مورد و یک عبارت است که به عنوان بدن تابع (* x x) ارزیابی می‌شود. توابع ناشناس گاهی اوقات عبارات لامبدا نامیده می‌شود.
به عنوان مثال، پاسکال و بسیاری از زبان‌های ضروری دیگر، از طریق مکانیزم اشاره گرهای عملکرد، مدت زمان پشتیبانی از زیر برنامه‌ها را به عنوان استدلال برای دیگر برنامه‌های زیر پشتیبانی می‌کنند. با این حال، دستورالعمل‌های تابع شرایط کافی برای توابع به عنوان نوع داده‌های کلاس اول نیستند، زیرا یک تابع نوع داده کلاس اول است اگر و تنها اگر نمونه‌های جدیدی از تابع در زمان اجرا ایجاد شود؛ و این ایجاد زمان اجرای توابع در Smalltalk، جاوا اسکریپت، و اخیراً در Scala, Eiffel ("عوامل")، C # ("نمایندگان") و C ++ 11 در میان دیگر پشتیبانی می‌شود.
استراتژی کاهش
برای جزئیات بیشتر در مورد این موضوع، به استراتژی ارزیابی مراجعه کنید.
این که آیا یک اصطلاح عادی است یا خیر، و چه مقدار کار باید انجام شود در عادی‌سازی آن، در صورت وجود، به شدت به استراتژی کاهش استفاده بستگی دارد. تمایز بین استراتژی‌های کاهش شامل تمایز در زبان‌های برنامه‌نویسی کاربردی بین ارزیابی مشتاق و ارزیابی تنبل است.
کاهش بتا کامل
هر گونه بازدهی می‌تواند در هر زمان کاهش یابد. این بدان معنی است که اساساً فقدان استراتژی کاهش خاص، با توجه به کاهش پذیری، «تمام شرط‌ها خاموش است».
سفارش کاربردی
راست‌ترین، بازخورد بیرونی همیشه اولین بار کاهش می‌یابد. به‌طور مستقیم این به این معنی است که استدلال‌های تابع همیشه قبل از تابع خود کاهش می‌یابد. دستور Applicatory همیشه تلاش می‌کند تا توابع را به فرم‌های معمول اعمال کند، حتی اگر این امکان‌پذیر نباشد.