حساب التفاضل والتكامل لامدا

📅 آخر تحديث: ٢٤ يوليو ٢٠٢٦
✍️ نُشر في: ٢٤ يوليو ٢٠٢٦
📷 يحتوي على 79 صور
الموسوعة الحرة
تفكك مفهوم التجريد اللامدا.λ{\displaystyle \lambda }يشير إلى بداية وظيفة.x{\displaystyle x}هو مُدخل المعامل.م{\displaystyle M}هو الجسم، مفصول بنقطة فاصلة ".{\displaystyle .}"من معلمات الإدخال."

في المنطق الرياضي ، يُعد حساب لامدا (أو حساب λ ) نظامًا رسميًا للتعبير عن العمليات الحسابية، قائمًا على تجريد الدوال وتطبيقها باستخدام ربط المتغيرات واستبدالها . ويُعتبر حساب لامدا غير المُنمّط، موضوع هذه المقالة، آلةً شاملة ، أي نموذجًا حسابيًا يُمكن استخدامه لمحاكاة أي آلة تورينج (والعكس صحيح). وقد قدّمه عالم الرياضيات ألونسو تشيرش في ثلاثينيات القرن العشرين كجزء من بحثه في أسس الرياضيات . وفي عام ١٩٣٦، وجد تشيرش صيغةً متسقةً منطقيًا ، ووثّقها في عام ١٩٤٠.

تعريف

يتألف حساب لامدا من لغة مصطلحات لامدا ، والتي تُعرَّف بواسطة صيغة رسمية، ومجموعة من قواعد التحويل لمعالجة تلك المصطلحات. في BNF ، تكون الصيغة هيهـ::=x|λx.هـ|هـهـ،{\displaystyle e::=x\mid \lambda x{\text{.}}e\mid e\,e,}حيث المتغيراتx،y،z{\displaystyle x,y,z}نطاق واسع يشمل مجموعة لا نهائية من الأسماء. المصطلحاتم،شمال،ت،s،هـ،و{\displaystyle M,N,t,s,e,f}يشمل هذا النطاق جميع حدود لامدا. ويتوافق هذا مع التعريف الاستقرائي التالي :

  • متغير​x{\displaystyle x}هو مصطلح لامدا صالح.
  • التجريد هو مصطلح لامدا(λx.ت){\displaystyle (\lambda x{\text{.}}t)}أينت{\displaystyle t}هو مصطلح لامدا، ويُشار إليه باسم جسم التجريد ، وx{\displaystyle x}هو متغير المعامل الخاص بالتجريد ،
  • التطبيق هو مصطلح لامدا(تs){\displaystyle (t\,s)}أينت{\displaystyle t}وs{\displaystyle s}هي مصطلحات لامدا.

يكون مصطلح لامدا صحيحًا نحويًا إذا أمكن الحصول عليه بتطبيق هذه القواعد الثلاث بشكل متكرر. ولتسهيل الأمر، يمكن غالبًا حذف الأقواس عند كتابة مصطلح لامدا - انظر تعريف حساب لامدا §  الترميز لمزيد من التفاصيل.

في مصطلحات لامدا، أي ظهور لمتغير ليس مُعاملاً لبعض المُحيطاتλ{\displaystyle \lambda }يُقال إنه مجاني . أي حدوث مجاني لـx{\displaystyle x}في مصطلحم{\displaystyle M}مُجلّد في​λx.م{\displaystyle \lambda x{\text{.}}M}أي ظهور حر لأي متغير آخر ضمنم{\displaystyle M}يبقى حراً فيλx.م{\displaystyle \lambda x{\text{.}}M}.

على سبيل المثال، في المصطلحxy{\displaystyle x\,y}، كلاهماx{\displaystyle x}وy{\displaystyle y}يحدث مجاناً. في(λx.xy){\displaystyle (\lambda x{\text{.}}x\,y)}،y{\displaystyle y}مجاني، ولكنx{\displaystyle x}لا يكون العنصر الموجود في جسم النص (أي بعد النقطة) حراً، ويُقال إنه مرتبط (بالمعامل). بينماy{\displaystyle y}مجاني في(λx.xy){\displaystyle (\lambda x{\text{.}}x\,y)}، وهو مُجلّد في(λy.λx.xy){\displaystyle (\lambda y{\text{.}}\lambda x{\text{.}}x\,y)}هناك حالتان منx{\displaystyle x}في(λy.(λx.xy)x){\displaystyle (\lambda y{\text{.}}(\lambda x{\text{.}}x\,y)\,x)}أحدهما مقيد، والآخر حر.

FV⁡(م){\displaystyle \operatorname {FV} (M)}هي مجموعة المتغيرات الحرة لـم{\displaystyle M}أي المتغيرات التي تظهر بشكل حر فيم{\displaystyle M}مرة واحدة على الأقل. ويمكن تعريفها استقرائياً على النحو التالي:

  • FV⁡(x)={x}{\displaystyle \operatorname {FV} (x)=\{x\}}
  • FV⁡(م1م2)=FV⁡(م1)∪FV⁡(م2){\displaystyle \operatorname {FV} (M_{1}M_{2})=\operatorname {FV} (M_{1})\cup \operatorname {FV} (M_{2})}
  • FV⁡(λx.م)=FV⁡(م)∖{x}{\displaystyle \operatorname {FV} (\lambda x{\text{.}}M)=\operatorname {FV} (M)\backslash \{x\}}

الترميزم[x:=شمال]{\displaystyle M[x:=N]}يشير إلى الاستبدال الذي يتجنب الاستحواذ : الاستبدالشمال{\displaystyle N}لكل حدث مجاني منx{\displaystyle x}فيم{\displaystyle M}مع تجنب التقاط المتغيرات. [ أ ] تُعرَّف هذه العملية استقرائيًا على النحو التالي:

  • x[x:=شمال]=شمال{\displaystyle x[x:=N]=N}؛y[x:=شمال]=y{\displaystyle y[x:=N]=y}لوy≠x{\displaystyle y\neq x}.
  • (م1م2)[x:=شمال]=(م1[x:=شمال])(م2[x:=شمال]){\displaystyle (M_{1}M_{2})[x:=N]=(M_{1}[x:=N])(M_{2}[x:=N])}.
  • (λy.م)[x:=شمال]{\displaystyle (\lambda y{\text{.}}M)[x:=N]}يوجد ثلاث حالات:
    • لوy=x{\displaystyle y=x}، يصبحλx.م{\displaystyle \lambda x{\text{.}}M}(x{\displaystyle x}مُلزم؛ لا تغيير).
    • لوy∉FV⁡(شمال){\displaystyle y\notin \operatorname {FV} (N)}، يصبحλy.(م[x:=شمال]){\displaystyle \lambda y{\text{.}}(M[x:=N])}.
    • لوy∈FV⁡(شمال){\displaystyle y\in \operatorname {FV} (N)}، أول إعادة تسمية ألفاλy.م{\displaystyle \lambda y{\text{.}}M}لλy′.م[y:=y′]{\displaystyle \lambda y'{\text{.}}M[y:=y']}معy′{\displaystyle y'}قم بتحديثه لتجنب تضارب الأسماء ، ثم تابع كما هو موضح أعلاه. يصبحλy′.م[y:=y′][x:=شمال]{\displaystyle \lambda y'{\text{.}}M[y:=y'][x:=N]}معy′∉FV⁡(م)∪FV⁡(شمال){\displaystyle y'\notin \operatorname {FV} (M)\cup \operatorname {FV} (N)}.

توجد عدة مفاهيم لـ "التكافؤ" و "الاختزال" التي تجعل من الممكن اختزال حدود لامدا إلى حدود لامدا مكافئة. [ 3 ]

  • يجسد التحويل ألفا الحدس القائل بأن الاختيار المحدد لمتغير مقيد، في التجريد، لا يهم (عادةً). إذاy∉FV⁡(م){\displaystyle y\notin \operatorname {FV} (M)}ثم المصطلحاتλx.م{\displaystyle \lambda x{\text{.}}M}وλy.م[x:=y]{\displaystyle \lambda y{\text{.}}M[x:=y]}تُعتبر متكافئة ألفا ، مكتوبةλx.م≡αλy.م[x:=y]{\displaystyle \lambda x{\text{.}}M\equiv _{\alpha }\lambda y{\text{.}}M[x:=y]}تُعرَّف علاقة التكافؤ بأنها أصغر علاقة تطابق على حدود لامدا الناتجة عن هذه القاعدة. على سبيل المثال،λx.x{\displaystyle \lambda x{\text{.}}x}وλy.y{\displaystyle \lambda y{\text{.}}y}هي مصطلحات لامدا مكافئة لـ ألفا.
  • تنص قاعدة اختزال بيتا على أن اختزال بيتا هو تطبيق للشكل(λx.ت)s{\displaystyle (\lambda x{\text{.}}t)s}، يختزل إلى المصطلحت[x:=s]{\displaystyle t[x:=s]}[ ب ] على سبيل المثال، لكلs{\displaystyle s}،(λx.x)s→x[x:=s]=s{\displaystyle (\lambda x{\text{.}}x)s\to x[x:=s]=s}وهذا يدل على أنλx.x{\displaystyle \lambda x{\text{.}}x}إنها الهوية الحقيقية. وبالمثل،(λx.y)s→y[x:=s]=y{\displaystyle (\lambda x{\text{.}}y)s\to y[x:=s]=y}مما يدل على أنλx.y{\displaystyle \lambda x{\text{.}}y}هي دالة ثابتة.
  • يُعبّر التحويل η عن الامتدادية ويُحوّل بينλx.وx{\displaystyle \lambda x{\text{.}}fx}وو{\displaystyle f}حينماx{\displaystyle x}لا يظهر مجاناً فيو{\displaystyle f}. غالباً ما يتم حذفه في العديد من علاجات حساب التفاضل والتكامل لامدا.

يشير مصطلح redex ، وهو اختصار لعبارة reducible expression (التعبير القابل للاختزال )، إلى المصطلحات الفرعية التي يمكن اختزالها باستخدام إحدى قواعد الاختزال. على سبيل المثال،(λx.م)شمال{\displaystyle (\lambda x{\text{.}}M)\,N}هو β-redex في التعبير عن استبدالشمال{\displaystyle N}لx{\displaystyle x}فيم{\displaystyle M}يُطلق على التعبير الذي يُختزل إليه التعبير المختزل اسم اختزاله ؛ اختزالλx.مشمال{\displaystyle \lambda x{\text{.}}M\,N}يكونم[x:=شمال]{\displaystyle M[x:=N]}.

الشرح والتطبيقات

حساب لامدا هو حساب كامل تورينج ، أي أنه نموذج حسابي عالمي يمكن استخدامه لمحاكاة أي آلة تورينج . [ 4 ] ويُستخدم الحرف اليوناني لامدا (λ)، الذي سُمّيَ به، في تعابير لامدا ومصطلحات لامدا للدلالة على ربط متغير في دالة .

قد يكون حساب لامدا غير مُحدد النوع أو مُحدد النوع . في حساب لامدا المُحدد النوع، لا يمكن تطبيق الدوال إلا إذا كانت قادرة على قبول "نوع" البيانات المُدخلة. يُعد حساب لامدا المُحدد النوع أضعف من حساب لامدا غير المُحدد النوع، وهو الموضوع الرئيسي لهذه المقالة، بمعنى أن حساب لامدا المُحدد النوع يُمكنه التعبير عن معلومات أقل مما يُمكنه حساب لامدا غير المُحدد النوع. من ناحية أخرى، يُمكن إثبات المزيد من الأمور باستخدام حساب لامدا المُحدد النوع. على سبيل المثال، في حساب لامدا المُحدد النوع ببساطة ، تنص إحدى النظريات على أن كل استراتيجية تقييم تنتهي لكل حد لامدا مُحدد النوع ببساطة، [ 5 ] بينما لا يلزم أن ينتهي تقييم حدود لامدا غير المُحددة النوع (انظر أدناه ). أحد أسباب وجود العديد من حسابات لامدا المُحددة النوع هو الرغبة في القيام بالمزيد (مما يُمكن لحساب لامدا غير المُحدد النوع القيام به) دون التخلي عن القدرة على إثبات نظريات قوية حول هذا الحساب.

تُستخدم حسابات لامدا في العديد من المجالات المختلفة في الرياضيات والفلسفة [ 6 ] واللغويات [ 7 ] [ 8 ] وعلوم الحاسوب [ 9 ] [ 10 ] . وقد لعبت حسابات لامدا دورًا هامًا في تطوير نظرية لغات البرمجة . وتُطبّق لغات البرمجة الوظيفية حسابات لامدا. كما تُعدّ حسابات لامدا موضوعًا بحثيًا راهنًا في نظرية الفئات [ 11 ] .

تاريخ

قدّم عالم الرياضيات ألونسو تشيرش حساب لامدا في ثلاثينيات القرن العشرين كجزء من بحثه في أسس الرياضيات . [ 12 ] [ ج ] وقد تبيّن أن النظام الأصلي غير متسق منطقيًا في عام 1935 عندما طوّر ستيفن كلين وجي بي روسر مفارقة كلين-روسر . [ 13 ] [ 14 ]

لاحقًا، في عام 1936، قام تشرش بعزل ونشر الجزء المتعلق بالحساب فقط، وهو ما يُعرف الآن بحساب لامدا غير المُنمّط. [ 15 ] وفي عام 1940، قدّم أيضًا نظامًا أضعف حسابيًا، ولكنه متسق منطقيًا، يُعرف بحساب لامدا المُنمّط ببساطة . [ 16 ]

حتى ستينيات القرن العشرين، حين اتضحت علاقته بلغات البرمجة، كان حساب لامدا مجرد شكلية. وبفضل تطبيقات ريتشارد مونتاغيو وغيره من اللغويين في دلالات اللغة الطبيعية، بدأ حساب لامدا يتبوأ مكانة مرموقة في كل من اللغويات [ 17 ] وعلوم الحاسوب [ 18 ] .

أصل رمز λ

ثمة بعض الغموض حول سبب استخدام تشيرش للحرف اليوناني لامدا (λ{\displaystyle \lambda }) كرمز لتجريد الدوال في حساب لامدا، ربما يعود ذلك جزئيًا إلى التفسيرات المتضاربة التي قدمها تشيرش نفسه. وفقًا لكاردون وهيندلي (2006):

بالمناسبة، لماذا اختارت تشيرش هذه الصيغة؟λ{\displaystyle \lambda }«؟ في [رسالة غير منشورة عام 1964 إلى هارالد ديكسون] ذكر بوضوح أنها جاءت من التدوين "x^{\displaystyle {\hat {x}}}"استُخدمت في تجريد الفئات بواسطة وايتهيد وراسل ، عن طريق تعديل "x^{\displaystyle {\hat {x}}}" ل "∧x{\displaystyle \land x}"لتمييز تجريد الدوال عن تجريد الأصناف، ثم تغيير"∧{\displaystyle \land }" ل "λ{\displaystyle \lambda }"لتسهيل الطباعة".

وقد ورد هذا الأصل أيضًا في [روسر، 1984، ص 338]. من ناحية أخرى، أخبر تشيرش في سنواته الأخيرة اثنين من الباحثين أن الاختيار كان أكثر عرضية: فقد كانت هناك حاجة إلى رمز وλ{\displaystyle \lambda }لقد تم اختياري بالصدفة.

وقد تناول دانا سكوت هذا السؤال أيضاً في العديد من المحاضرات العامة. [ 19 ] يروي سكوت أنه طرح ذات مرة سؤالاً حول أصل رمز لامدا على جون دبليو أديسون الابن، الطالب السابق لتشرش وصهره، والذي كتب بعد ذلك بطاقة بريدية إلى حماه:

عزيزي البروفيسور تشيرش،

كان لدى راسل عامل إيوتا ، وكان لدى هيلبرت عامل إبسيلون . لماذا اخترتَ لامدا كعامل؟

بحسب سكوت، فإن رد تشيرش بالكامل كان عبارة عن إعادة البطاقة البريدية مع التعليق التالي: " إيني، ميني، مايني، مو ".

تحفيز

تُعدّ الدوال القابلة للحساب مفهومًا أساسيًا في علوم الحاسوب والرياضيات. يوفر حساب لامدا دلالات بسيطة للحساب، مما يُسهّل دراسة خصائص الحساب بشكل رسمي. يتضمن حساب لامدا تبسيطين يُبسّطان دلالاته. التبسيط الأول هو أن حساب لامدا يتعامل مع الدوال "بشكل مجهول"؛ فهو لا يعطيها أسماءً صريحة. على سبيل المثال، الدالة

squأرهـ_suم⁡(x،y)=x2+y2{\displaystyle \operatorname {square\_sum} (x,y)=x^{2}+y^{2}}

يمكن إعادة كتابتها بشكل مجهول على النحو التالي:

(x،y)↦x2+y2{\displaystyle (x,y)\mapsto x^{2}+y^{2}}

(والتي تُقرأ على أنها " مجموعة منx{\displaystyle x}وy{\displaystyle y}يتم تعيينها إلىx2+y2{\textstyle x^{2}+y^{2}}"). [ د ] وبالمثل، الدالة

بطاقة تعريف⁡(x)=x{\displaystyle \operatorname {id} (x)=x}

يمكن إعادة كتابتها بشكل مجهول على النحو التالي:

x↦x{\displaystyle x\mapsto x}

حيث يتم ببساطة تعيين المدخلات إلى نفسها. [ د ]

التبسيط الثاني هو أن حساب لامدا لا يستخدم إلا الدوال ذات المدخل الواحد. أما الدالة العادية التي تتطلب مدخلين، على سبيل المثال...squأرهـ_suم{\textstyle \operatorname {square\_sum} }يمكن إعادة صياغة الدالة إلى دالة مكافئة تقبل مُدخلًا واحدًا، وتُخرج دالة أخرى تقبل بدورها مُدخلًا واحدًا. على سبيل المثال،

(x،y)↦x2+y2{\displaystyle (x,y)\mapsto x^{2}+y^{2}}

يمكن إعادة صياغتها إلى

x↦(y↦(x2+y2)){\displaystyle x\mapsto (y\mapsto (x^{2}+y^{2}))}

هذه الطريقة، المعروفة باسم "التقسيم الجزئي "، تحول الدالة التي تأخذ وسائط متعددة إلى سلسلة من الدوال، كل منها بوسيط واحد.

تطبيق الوظيفة لـsquأرهـ_suم{\textstyle \operatorname {square\_sum} }الدالة على الوسائط (5، 2)، تُنتج على الفور

((x،y)↦x2+y2)(5،2){\textstyle ((x,y)\mapsto x^{2}+y^{2})(5,2)}
=52+22{\textstyle =5^{2}+2^{2}}
=29{\textstyle =29}،

بينما يتطلب تقييم النسخة بالكاري خطوة إضافية

((x↦(y↦x2+y2))(5))(2){\textstyle {\Bigl (}{\bigl (}x\mapsto (y\mapsto x^{2}+y^{2}){\bigr )}(5){\Bigr )}(2)}
=(y↦52+y2)(2){\textstyle =(y\mapsto 5^{2}+y^{2})(2)}// تعريفx{\displaystyle x}تم استخدامه مع5{\displaystyle 5}في التعبير الداخلي. هذا يشبه اختزال بيتا.
=52+22{\textstyle =5^{2}+2^{2}}// تعريفy{\displaystyle y}تم استخدامه مع2{\displaystyle 2}مرة أخرى، يشبه ذلك اختزال بيتا.
=29{\textstyle =29}

للوصول إلى نفس النتيجة.

في حساب التفاضل والتكامل اللامدا، تُعتبر الدوال " قيمًا من الدرجة الأولى "، لذا يمكن استخدامها كمدخلات، أو إرجاعها كمخرجات من دوال أخرى. على سبيل المثال، مصطلح لامداλx.x{\displaystyle \lambda x.x}يمثل دالة التطابق ،x↦x{\displaystyle x\mapsto x}. إضافي،λx.y{\displaystyle \lambda x.y}يمثل الدالة الثابتةx↦y{\displaystyle x\mapsto y}، الدالة التي تُرجع دائمًاy{\displaystyle y}بغض النظر عن المدخلات. كمثال على دالة تعمل على دوال أخرى، يمكن تعريف تركيب الدوال على النحو التالي:λو.λز.λx.(و(زx)){\displaystyle \lambda f.\lambda g.\lambda x.(f(gx))}.

الأشكال الطبيعية والالتقاء

يمكن إثبات أن اختزال بيتا متلاقٍ حتى تحويل ألفا (أي عندما يُعتبر شكلان طبيعيان متساويين إذا كان من الممكن تحويل أحدهما إلى الآخر باستخدام تحويل ألفا). وبحسب نظرية تشرش-روسر ، فإن أي تسلسل معين من خطوات الاختزال يبدأ من حد لامدا معين وينتهي في النهاية سينتج عنه نفس الشكل الطبيعي بيتا . ومع ذلك، فإن حساب لامدا غير المصنف في ظل اختزال بيتا كقاعدة لإعادة الكتابة ليس معياريًا قويًا ولا معياريًا ضعيفًا ؛ فهناك حدود ليس لها شكل طبيعي مثل Ω .

بالنظر إلى الحدود الفردية، فإن لكل من الحدود ذات التطبيع القوي والحدود ذات التطبيع الضعيف شكلاً طبيعياً فريداً. بالنسبة للحدود ذات التطبيع القوي، تضمن أي استراتيجية اختزال الحصول على الشكل الطبيعي، بينما بالنسبة للحدود ذات التطبيع الضعيف، قد تفشل بعض استراتيجيات الاختزال في إيجاده.

ترميز أنواع البيانات

يمكن استخدام حساب لامدا الأساسي لنمذجة العمليات الحسابية ، والقيم المنطقية، وهياكل البيانات، والتكرار، كما هو موضح في الأقسام الفرعية التالية i و ii و iii و § iv .

الحساب في حساب التفاضل والتكامل لامدا

توجد عدة طرق ممكنة لتعريف الأعداد الطبيعية في حساب التفاضل والتكامل لامدا، ولكن الأكثر شيوعًا هي أرقام الكنيسة ، والتي يمكن تعريفها على النحو التالي:

0  := λ f .λ x . x
1  := λ f .λ x . f x
2  := λ f .λ x . f ( f x )
3  := λ f .λ x . f ( f ( f x ))

وهكذا دواليك. أو باستخدام صيغة بديلة تسمح بتمرير وسائط متعددة غير مُجزأة إلى دالة:

0  := λ fx . x
1  := λ fx . f x
2  := λ fx . f ( f x )
3  := λ fx . f ( f ( f x ))

عدد تشرش هو دالة من الرتبة العليا ، تأخذ دالة ذات وسيط واحد f ، وتعيد دالة أخرى ذات وسيط واحد. عدد تشرش n هو دالة تأخذ الدالة f كوسيط، وتعيد التركيب النوني للدالة f ، أي الدالة f مركبة مع نفسها n مرة. يُرمز لهذا التركيب بـ f ( n ) ، وهو في الواقع القوة النونية للدالة f (باعتبارها مؤثرًا). تُعرَّف f (0) بأنها دالة التطابق. التركيب الدوالي تجميعي ، ولذلك، فإن هذه التركيبات المتكررة لدالة واحدة f تخضع لقانونين من قوانين الأسس : f ( m ) ∘ f ( n ) = f ( m+n ) و ( f ( n ) ) ( m ) = f ( m*n ) ، ولهذا السبب يمكن استخدام هذه الأعداد في العمليات الحسابية. (في حساب لامدا الأصلي لتشرش، كان من الضروري أن يظهر المعامل الرسمي لتعبير لامدا مرة واحدة على الأقل في جسم الدالة، مما جعل تعريف الصفر المذكور أعلاه مستحيلاً ).

إحدى طرق فهم رمز الكنيسة n ، المفيد غالبًا عند تحليل البرامج، هي اعتباره تعليمة "كرر n مرة". على سبيل المثال، باستخدام الدالتين PAIR و NIL الموضحتين أدناه، يمكن تعريف دالة تُنشئ قائمة ( مرتبطة ) من n عنصرًا، جميعها تساوي x، وذلك بتكرار عبارة "أضف عنصر x آخر" n مرة، بدءًا من قائمة فارغة. يُستخدم مصطلح لامدا (lambda) في هذا السياق.

λ n .λ x . n (زوج x ) لا شيء

يُنشئ، بمعلومية رقم تشرش n وبعض x ، سلسلة من n تطبيقًا

زوج × (زوج × ...(زوج × لا شيء)...)

من خلال تغيير ما يتم تكراره، وما هي الوسائط التي يتم تطبيق تلك الوظيفة المتكررة عليها، يمكن تحقيق العديد من التأثيرات المختلفة.

يمكننا تعريف دالة لاحقة، تأخذ رقمًا تشرشيًا n وتعيد رقمه اللاحق n + 1 عن طريق إجراء تطبيق إضافي واحد للدالة f التي تم تزويدها بها، حيث ( nfx ) تعني " n تطبيقًا لـ f بدءًا من x ":

SUCC  := λ n .λ f .λ x . f ( n f x )

لأن التركيب m للدالة f مع التركيب n للدالة f يعطي التركيب m + n للدالة f ، فإن f ( m ) ∘ f ( n ) = f ( m + n ) ، وبالتالي يمكن تعريف الجمع على النحو التالي:

PLUS  := χ م .ω n .χ f .ω x . م و ( ن و س )

يمكن اعتبار دالة الجمع (PLUS) دالة تأخذ عددين طبيعيين كمعاملات وتعيد عددًا طبيعيًا؛ ويمكن التحقق من ذلك.

بالإضافة إلى 2 3

و

5

هي تعابير لامدا مكافئة لـ بيتا. بما أن إضافة m إلى عدد ما يمكن إنجازها بتكرار العملية اللاحقة m مرة، فإن التعريف البديل هو:

PLUS′  := lect m .lect n . م SUCC ن [ 20 ]

وبالمثل، وفقًا لـ ( f ( n ) ) ( m ) = f ( m*n ) ، يمكن تعريف الضرب على النحو التالي:

MULT  := λ m .λ n .λ f . m ( n f ) [ 21 ]

وبالتالي فإن ضرب الأرقام الكنسية هو ببساطة تركيبها كدوال. أو بدلاً من ذلك

MULT′  := lect m .lect n . م (زائد ن ) 0

لأن ضرب m و n هو نفسه جمع n بشكل متكرر، m مرة، بدءًا من الصفر.

الأسس، كونها ضرب عدد في نفسه بشكل متكرر، تُترجم إلى تركيب متكرر لرقم كنسي مع نفسه، كدالة. والتركيب المتكرر هو ما تمثله الأرقام الكنسية .

POW  := λ b .λ n . n b [ 1 ]

أو هنا أيضاً،

أسير'  := ẫ b .ạn . ن (متعدد ب ) 1

وباختصار، يصبح

أسرى الحرب''  := ẫ b .ạn .ạf f . ن ب و

لكن هذه مجرد نسخة موسعة من لعبة POW التي لدينا بالفعل، أعلاه.

إن دالة السلف ، المحددة بمعادلتين PRED (SUCC n ) = n و PRED 0 = 0 ، أكثر تعقيدًا بكثير. الصيغة

PRED  := χ n .χ f .ω x . n (π g .ẫ h . h ( g f )) (π u . x ) (π u . u )

يمكن التحقق من ذلك بإثبات استقرائيًا أنه إذا رمزت T إلى (λ g .λ h . h ( g f )) ، فإن T ( n ) (λ u . x ) = (λ h . h ( f ( n −1) ( x ))) لـ n > 0. يرد أدناه تعريفان آخران لـ PRED ، أحدهما باستخدام العبارات الشرطية والآخر باستخدام الأزواج . باستخدام دالة السلف، يكون الطرح مباشرًا. تعريف

SUB  := α m .lect n . ن بريد م ،

SUB m n ينتج m − n عندما يكون m > n و 0 خلاف ذلك.

المنطق والمسندات

بحسب الاصطلاح، يتم استخدام التعريفين التاليين (المعروفين باسم القيم المنطقية الكنسية) للقيم المنطقية TRUE و FALSE :

صحيح  := λ س .λ ص . س
خطأ  := λ x .λ y . y

ثم، باستخدام هذين المصطلحين لامدا، يمكننا تعريف بعض عوامل المنطق (هذه مجرد صيغ ممكنة؛ يمكن أن تكون التعبيرات الأخرى صحيحة بنفس القدر): [ 22 ]

و  := λ p .λ q . p q p
أو  := λ p .λ q . p p q
ليس  := λ p . p خطأ صحيح
IFTHENELSE  := α p .ο a .lect b . ص أ ب

أصبحنا الآن قادرين على حساب بعض الدوال المنطقية، على سبيل المثال:

صحيح خطأ
≡ ( p . q . p q p ) TRUE FALSE → β TRUE FALSE TRUE
≡ (× x .lect y . x ) FALSE TRUE → β FALSE

ونرى أن AND TRUE FALSE تعادل FALSE .

الدالة الشرطية هي دالة تُرجع قيمة منطقية (Boolean). أبسط دالة شرطية هي ISZERO ، التي تُرجع القيمة TRUE إذا كان مُدخلها هو الرقم الكنسي 0 ، ولكنها تُرجع القيمة FALSE إذا كان مُدخلها أي رقم كنسي آخر.

إيزيرو  := lectn . ن (× × .FALSE) صحيح

يختبر الشرط التالي ما إذا كانت الوسيطة الأولى أصغر من أو تساوي الوسيطة الثانية:

LEQ  := lect m .lect n .ISZERO (SUB m n ) ,

وبما أن m = n إذا كان LEQ m n و LEQ n m ، فمن السهل بناء مسند للمساواة العددية.

إن توفر المسندات والتعريف المذكور أعلاه للقيمتين TRUE و FALSE يجعلان كتابة تعابير "إذا-ثم-وإلا" في حساب لامدا أمرًا سهلاً. على سبيل المثال، يمكن تعريف دالة السلف على النحو التالي:

بريد  := lect n . n (π g .lect 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.

أزواج

يُمثل الزوج (الزوج الثنائي) قيمتين، ويتم تمثيله بواسطة تجريد يتوقع معالجًا يُمرر إليه القيمتين. تُعيد الدالة FIRST العنصر الأول من الزوج، بينما تُعيد الدالة SECOND العنصر الثاني.

الزوج  := λ x .λ y .λ f . f x y
أولا  := φp . ص (× س . × ص . س )
الثاني  := φp . ص (× س . × ذ . ذ )

يمكن أن تكون القائمة المتصلة إما فارغة (NIL)، أو عبارة عن زوج من عنصر (يُسمى الرأس ) وقائمة أصغر ( الذيل ). تُرجع الدالة NULL القيمة TRUE للقيمة NIL ، والقيمة FALSE للقائمة غير الفارغة.

NIL  := λ f .TRUE
NULL  := χ ص . ص (× س . × ص .FALSE)

بدلاً من ذلك، مع NIL := FALSE ، فإن البنية ( l (λ h .λ t .λ z . ... h ... t ...) _on_nil_) تغني عن الحاجة إلى اختبار NULL صريح: 

NIL  := λ x .λ y . y
NULL  := lect l . l (π h .ạt .ạz .FALSE ) TRUE

كمثال على استخدام الأزواج، يمكن تعريف دالة الإزاحة والزيادة التي تربط ( m , n ) بـ ( n , n + 1) على النحو التالي:

Φ  := λ p .PAIR (SECOND p ) (SUCC (SECOND p ))
Ψ  := λ fp .PAIR (SECOND p ) (f (SECOND p ))

مما يسمح لنا بتقديم ربما النسخة الأكثر شفافية من وظيفة السلف:

PRED  := λ n .FIRST ( n (Ψ SUCC) (PAIR 0 0))
 = λ nfx .FIRST ( n (Ψ f ) (PAIR xx ))

يؤدي استبدال التعريفات وتبسيط التعبير الناتج إلى تعريفات أكثر وضوحًا.

 = φ نفكس . n ( rab . rb ( fb )) ( ab . a ) xx
 = φ نفكس . n (α rij . j ( rjf )) (λ ij . x ) II
 = φ نفكس . n (π rij . i ( rjj )) (π ij . x ) I f
 = φ نفكس . n (π ri . i ( rf )) (π i . x ) I

(حيث I := λ x . x )، مما يؤدي بوضوح إلى الأصل.  

تقنيات برمجة إضافية

توجد مجموعة كبيرة من المصطلحات البرمجية لحساب لامدا. وقد طُوِّر العديد منها في الأصل لاستخدام حساب لامدا كأساس لدلالات لغات البرمجة ، ما يعني فعليًا استخدام حساب لامدا كلغة برمجة منخفضة المستوى . ولأن العديد من لغات البرمجة تتضمن حساب لامدا (أو ما يشابهه) كجزء منها، فإن هذه التقنيات تُستخدم أيضًا في البرمجة العملية، ولكن قد يُنظر إليها حينها على أنها غامضة أو غير مألوفة.

الثوابت المسماة

في حساب لامدا، تتخذ المكتبة شكل مجموعة من الدوال المُعرَّفة مسبقًا، والتي تُمثل، كمصطلحات لامدا، ثوابت مُحددة. لا يوجد في حساب لامدا البحت مفهوم الثوابت المُسماة لأن جميع مصطلحات لامدا الذرية هي متغيرات، ولكن يُمكن محاكاة وجود ثوابت مُسماة عن طريق تخصيص متغير كاسم للثابت، واستخدام التجريد لربط هذا المتغير في الجزء الرئيسي من البرنامج، وتطبيق هذا التجريد على التعريف المقصود. وبالتالي، لاستخدام f لتمثيل N (مصطلح لامدا صريح) في M (مصطلح لامدا آخر، وهو "البرنامج الرئيسي")، يُمكن القول

(λ f . M ) N

كثيراً ما يستخدم المؤلفون اختصارات نحوية ، مثل let ، [ e ]، للسماح بكتابة ما سبق بترتيب أكثر سهولة.

ليكن f = N في M

من خلال ربط هذه التعريفات، يمكن للمرء كتابة "برنامج" حساب التفاضل والتكامل لامدا على شكل صفر أو أكثر من تعريفات الدوال، متبوعة بمصطلح لامدا واحد يستخدم تلك الدوال التي تشكل الجزء الرئيسي من البرنامج.

من القيود البارزة لهذا النوع من الدوال `let` أنه لا يمكن الإشارة إلى الاسم ` f` في `N` ، لأن `N` خارج نطاق الربط التجريدي `f` ، وهو `M` ؛ وهذا يعني أنه لا يمكن كتابة تعريف دالة تكرارية باستخدام `let` . يسمح بناء `letrec [ f ]` بكتابة تعريفات دوال تكرارية، حيث يشمل نطاق الربط التجريدي ` f` كلاً من `N` و` M` . أو يمكن استخدام تطبيق ذاتي على غرار ما يؤدي إلى مُركِّب `Y` .

التكرار والنقاط الثابتة

الاستدعاء الذاتي هو عندما تستدعي دالة نفسها. ما هي القيمة التي تُمثل هذه الدالة؟ يجب أن تُشير إلى نفسها بطريقة ما داخل نفسها، تمامًا كما يُشير تعريفها إلى نفسه داخل نفسه. إذا احتوت هذه القيمة على نفسها كقيمة، فسيكون حجمها لانهائيًا، وهو أمر مستحيل. تتغلب بعض الرموز الأخرى، التي تدعم الاستدعاء الذاتي بشكل أصيل، على هذه المشكلة بالإشارة إلى الدالة باسمها داخل تعريفها. لا يُمكن لحساب لامدا التعبير عن هذا، لأنه لا توجد فيه أسماء للمصطلحات في الأساس، بل أسماء الوسائط فقط، أي المعاملات في التجريدات. وبالتالي، يُمكن لتعبير لامدا أن يستقبل نفسه كوسيط له ويُشير إلى (نسخة من) نفسه عبر اسم المعامل المُقابل. سيعمل هذا بشكل صحيح إذا تم استدعاؤه بالفعل مع نفسه كوسيط. على سبيل المثال، (λ x . x x ) E = ( EE ) يُعبر عن الاستدعاء الذاتي عندما يكون E تجريدًا يُطبق معامله على نفسه داخل جسمه للتعبير عن استدعاء ذاتي. بما أن هذه المعلمة تتلقى E كقيمة لها، فإن تطبيقها الذاتي سيكون هو نفسه ( EE ) مرة أخرى.

كمثال ملموس، لنأخذ دالة المضروب F( n ) المعرفة بشكل تكراري كما يلي:

F( n ) = 1 إذا كان n = 0؛ وإلا n × F( n − 1) .

في تعبير لامدا الذي يُمثل هذه الدالة، يُفترض أن أحد المعاملات (عادةً المعامل الأول) يستقبل تعبير لامدا نفسه كقيمة له، بحيث أن استدعاء الدالة مع نفسها كمعامل أول يُعد استدعاءً تكراريًا. وبالتالي، لتحقيق التكرار، يجب دائمًا تمرير المعامل المُراد استخدامه كمرجع ذاتي (يُسمى هنا s ، وهو اختصار لـ "self" أو "self-applying") إلى نفسه داخل جسم الدالة عند نقطة الاستدعاء التكراري.

E  := λ s . λ n .(1, إذا كان n = 0; else n × ( s s ( n −1)))
بما أن ssn = F n = EE n لكي يتحقق الشرط، فإن s = E و
F  := (λ x . x x ) E = EE

ولدينا

F = EE = λ n .(1، إذا كان n = 0؛ وإلا n × (EE ( n −1)))

هنا، يصبح ss هو نفسه (EE) داخل نتيجة التطبيق (EE) ، واستخدام نفس الدالة للاستدعاء هو تعريف التكرار. يحقق التطبيق الذاتي التكرار هنا، حيث يمرر تعبير لامدا الخاص بالدالة إلى الاستدعاء التالي كقيمة وسيطة، مما يجعله متاحًا للإشارة إليه هناك بواسطة اسم المعامل s ليتم استدعاؤه عبر التطبيق الذاتي s s ، مرارًا وتكرارًا حسب الحاجة، وفي كل مرة يتم إعادة إنشاء مصطلح لامدا F = EE .

يُعدّ هذا التطبيق خطوة إضافية تمامًا كما هو الحال مع البحث عن الاسم. وله نفس تأثير التأخير. فبدلًا من احتواء F داخله ككلٍّ مُسبقًا ، فإن تأخير إعادة إنشائه حتى الاستدعاء التالي يُتيح وجوده من خلال وجود حدّين لامدا محدودين E داخله، واللذين يُعيدان إنشائه لاحقًا عند الحاجة.

يحلّ هذا النهج التطبيقي الذاتي المشكلة، ولكنه يتطلب إعادة كتابة كل استدعاء تكراري كتطبيق ذاتي. نرغب في الحصول على حل عام، دون الحاجة إلى أي إعادة كتابة.

G  := λ r . λ n .(1, إذا كان n = 0; else n × ( r ( n −1)))
مع r x = F x = G r x للتحقق، إذن r = G r =: ثبت G و
F  := FIX G حيث FIX g = ( r حيث r = g r ) = g (FIX g )
بحيث يكون FIX G = G (FIX G) = (λ n .(1, إذا كان n = 0؛ وإلا n × ((FIX G) ( n −1))))

عند إعطاء تعبير لامدا ذي وسيط أول يُمثل استدعاءً تكراريًا (مثل G هنا)، فإن مُركِّب النقطة الثابتة FIX يُعيد تعبير لامدا ذاتي التكرار يُمثل الدالة التكرارية (هنا، F ). لا يلزم تمرير الدالة إلى نفسها صراحةً في أي مرحلة، لأن التكرار الذاتي مُرتب مُسبقًا عند إنشائها، ليتم تنفيذه في كل مرة تُستدعى فيها. وبالتالي، يُعاد إنشاء تعبير لامدا الأصلي (FIX G) داخل نفسه عند نقطة الاستدعاء، مُحققًا بذلك مرجعية ذاتية .

في الواقع، هناك العديد من التعريفات المحتملة لعامل FIX هذا ، وأبسطها ما يلي:

Y  := lect g .( x . g ( x x )) ( x . g ( x x ))

في حساب التفاضل والتكامل لامدا، Y g هي نقطة ثابتة لـ g ، حيث تتوسع إلى:

Yg​
~> (λ 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 )

الآن، لإجراء الاستدعاء التكراري لدالة المضروب لمتغير n ، نستدعي ببساطة ( Y G) n . على سبيل المثال، إذا كان n = 4، فإن هذا يعطينا:

( Y G) 4
~> G ( Y G) 4
~> (λ r .λ n .(1, if n = 0; else n × ( r ( n −1)))) ( Y G) 4
~> (λ n .(1, if n = 0; else n × (( Y G) ( n −1)))) 4
~> 1، إذا كان 4 = 0؛ وإلا 4 × (( Y G) (4−1))
~> 4 × (G ( Y G) (4−1))
~> 4 × ((λ n .(1, إذا كان n = 0; else n × (( Y G) ( n −1)))) (4−1))
~> 4 × (1، إذا كان 3 = 0؛ وإلا 3 × (( Y G) (3−1)))
~> 4 × (3 × (G ( Y G) (3−1)))
~> 4 × (3 × ((λ n .(1, إذا كان n = 0؛ وإلا n × (( Y G) ( n −1)))) (3−1)))
~> 4 × (3 × (1، إذا كان 2 = 0؛ وإلا 2 × (( Y G) (2−1))))
~> 4 × (3 × (2 × (G ( Y G) (2−1))))
~> 4 × (3 × (2 × ((λ n .(1, إذا كان n = 0؛ وإلا n × (( Y G) ( n −1)))) (2−1))))
~> 4 × (3 × (2 × (1، إذا كان 1 = 0؛ وإلا 1 × (( Y G) (1−1))))))
~> 4 × (3 × (2 × (1 × (G ( Y G) (1−1))))))
~> 4 × (3 × (2 × (1 × ((λ n .(1, إذا كان n = 0؛ وإلا n × (( Y G) ( n −1)))) (1−1)))))
~> 4 × (3 × (2 × (1 × (1، إذا كان 0 = 0؛ وإلا 0 × (( Y G) (0−1))))))
~> 4 × (3 × (2 × (1 × (1))))
24

يمكن اعتبار كل دالة مُعرَّفة بشكل تكراري نقطة ثابتة لدالة من الرتبة العليا (تُعرف أيضًا بالدالة الوظيفية) مُعرَّفة بشكل مناسب، تُغلق الاستدعاء التكراري مع وسيط إضافي. لذلك، باستخدام Y ، يمكن التعبير عن كل دالة تكرارية بتعبير لامدا. على وجه الخصوص، يمكننا الآن تعريف دوال الطرح والضرب والمقارنة للأعداد الطبيعية بشكل واضح باستخدام التكرار.

عندما تتم برمجة مُركِّب Y مباشرةً بلغة برمجة صارمة ، فإن ترتيب التقييم التطبيقي المستخدم في مثل هذه اللغات سيؤدي إلى محاولة توسيع التطبيق الذاتي الداخلي بشكل كامل(xx){\displaystyle (xx)}قبل الأوان، مما يتسبب في تجاوز سعة المكدس أو، في حالة تحسين استدعاء الذيل ، في حلقة لا نهائية. [ 24 ] يمكن استخدام متغير مؤجل من Y، وهو مُركِّب Z ، في مثل هذه اللغات. يحتوي على تطبيق ذاتي داخلي مخفي خلف تجريد إضافي من خلال توسيع إيتا ، كما(λv.xxv){\displaystyle (\lambda v.xxv)}وبالتالي منع توسعها المبكر: [ 25 ]

Z=λو.(λx.و(λv.xxv)) (λx.و(λv.xxv)) .{\displaystyle Z=\lambda f.(\lambda x.f(\lambda v.xxv))\ (\lambda x.f(\lambda v.xxv))\ .}

الشروط القياسية

توجد أسماء شائعة ومقبولة لبعض المصطلحات: [ 26 ] [ 27 ] [ 28 ]

I  := λ x . x
S  := ο x .lect y .lect z . س ض ( ذ ض )
K  := λ x .λ y . x
ب  := ο x .lect y .lect z . س ( ص ض )
ج  := λ س .λ ص .λ ع . س ع ص
W  := λ x .λ y . x y y
ω أو Δ أو U  := λ x . x x
Ω  := ω ω

I هي دالة التطابق. يشكل كل من SK و BCKW نظامي حساب توافيق كاملينقادرين على التعبير عن أي حد لامدا - انظر القسم التالي . Ω هو UU ، وهو أصغر حد ليس له شكل معياري. YI هو حد آخر من هذا النوع. Y هو حد معياري ومُعرَّف أعلاه ، ويمكن تعريفه أيضًا على أنه Y = BU(CBU) ، بحيث يكون Y g = g( Y g) .يُشار عادةً إلى TRUE و FALSE المُعرَّفين أعلاه بالاختصارين T و F.

إزالة التجريد

إذا كان N مصطلحًا لامدا بدون تجريد، ولكنه قد يحتوي على ثوابت مُسماة ( مجموعات ) ، فإنه يوجد مصطلح لامدا T ( x , N ) يُكافئ λx.N ولكنه يفتقر إلى التجريد ( باستثناء كونه جزءًا من الثوابت المُسماة، إذا اعتُبرت هذه الثوابت غير ذرية). يمكن أيضًا اعتبار هذا بمثابة إخفاء هوية المتغيرات، حيث أن T ( x , N ) يُزيل جميع حالات x من N ، مع السماح في الوقت نفسه باستبدال قيم الوسائط في المواضع التي تحتوي فيها N على x . يمكن تعريف دالة التحويل T كما يلي:

T ( x , x ) := I 
T ( x , N ) := K N إذا لم يكن x حراً في N . 
T ( x , M N ) := S T ( x , M ) T ( x , N ) 

في كلتا الحالتين، يتم اختزال الحد من الشكل T(x, N)P عن طريق قيام المُركِّب الأولي I أو K أو S باستلام الوسيط P ، تمامًا كما يفعل اختزال بيتا لـ ( λx.N)P. يُعيد I هذا الوسيط . يتجاهل KN الوسيط، تمامًا كما يفعل ( λx.N) عندما لا يكون لـ x ظهور حر في N. يمرر S الوسيط إلى كلا الحدين الفرعيين للتطبيق، ثم يُطبق نتيجة الأول على نتيجة الثاني ، تمامًا كما أن ( λx.MN ) P هو نفسه ( ( λx.M ) P ) ( ( λx.N ) P ) .

تتشابه المُركِّبات B و C مع S ، لكنها تُمرِّر الوسيط إلى حدٍّ فرعيٍّ واحدٍ فقط من التطبيق ( B إلى الحدّ الفرعي "الوسيط" و C إلى الحدّ الفرعي "الدالة")، مما يُجنِّب استخدام K لاحقًا في حال عدم وجود x في أيٍّ من الحدود الفرعية. بالمقارنة مع B و C ، فإن المُركِّب S يجمع في الواقع بين وظيفتين: إعادة ترتيب الوسائط، وتكرار الوسيط بحيث يُمكن استخدامه في موضعين. أما المُركِّب W فيقوم بالوظيفة الأخيرة فقط، مما يُنتج نظام B، C، K، W كبديلٍ لحساب المُركِّبات SKI .

حساب التفاضل والتكامل لامدا المكتوب

حساب التفاضل والتكامل اللامدا المكتوب هو شكل رسمي مكتوب يستخدم رمز لامدا (λ{\displaystyle \lambda }يُستخدم هذا المصطلح للدلالة على تجريد الدوال المجهولة. في هذا السياق، تُعتبر الأنواع عادةً كائنات ذات طبيعة تركيبية تُسند إلى مصطلحات لامدا؛ وتعتمد طبيعة النوع تحديدًا على الحساب المُستخدم (انظر: أنواع حسابات لامدا المُنمّطة ). من وجهة نظر معينة، يُمكن اعتبار حسابات لامدا المُنمّطة تحسينات لحسابات لامدا غير المُنمّطة، ولكن من وجهة نظر أخرى، يُمكن اعتبارها النظرية الأساسية، وحسابات لامدا غير المُنمّطة حالة خاصة بنوع واحد فقط. [ 29 ]

تُعدّ حسابات لامدا المُصنّفة من أساسيات لغات البرمجة، وهي أساس لغات البرمجة الوظيفية المُصنّفة مثل ML و Haskell، وبشكل غير مباشر، لغات البرمجة الإجرائية المُصنّفة . تلعب حسابات لامدا المُصنّفة دورًا هامًا في تصميم أنظمة الأنواع للغات البرمجة؛ حيث تُجسّد قابلية التصنيف عادةً الخصائص المرغوبة للبرنامج، مثل عدم تسبب البرنامج في انتهاك الوصول إلى الذاكرة.

ترتبط حسابات لامدا المكتوبة ارتباطًا وثيقًا بالمنطق الرياضي ونظرية البرهان عبر تماثل كاري-هوارد ، ويمكن اعتبارها اللغة الداخلية لفئات التصنيفات ، على سبيل المثال، حساب لامدا المكتوب ببساطة هو لغة فئة ديكارتية مغلقة (CCC). [ 30 ]

استراتيجيات الحد من

يعتمد تحديد ما إذا كان المصطلح قابلاً للتطبيع أم لا، ومقدار العمل المطلوب لتطبيعه إن كان كذلك، إلى حد كبير على استراتيجية الاختزال المستخدمة. تشمل استراتيجيات الاختزال الشائعة في حساب لامدا ما يلي: [ 31 ] [ 32 ] [ 33 ]

ترتيب طبيعي
يُختزل أولًا العنصر الخارجي الأيسر في تعريف الاختزال. أي أنه كلما أمكن، تُستبدل الوسائط في متن التجريد قبل اختزالها. إذا كان للمصطلح شكل بيتا-طبيعي، فإن اختزال الترتيب الطبيعي سيصل دائمًا إلى ذلك الشكل الطبيعي.
أمر تطبيقي
يتم اختزال أول تعبير داخلي من اليسار أولاً. ونتيجة لذلك، يتم دائمًا اختزال وسائط الدالة قبل استبدالها فيها. على عكس اختزال الترتيب العادي، قد يفشل اختزال الترتيب التطبيقي في إيجاد الصيغة الطبيعية بيتا للتعبير، حتى لو كانت هذه الصيغة موجودة. على سبيل المثال، المصطلح(λx.y(λz.(zz)λz.(zz))){\displaystyle (\;\lambda x.y\;\;(\lambda z.(zz)\;\lambda z.(zz))\;)}يُختزل إلى نفسه بواسطة الترتيب التطبيقي، بينما يُختزل إلى شكله الطبيعي بيتا.y{\displaystyle y}.
اختزالات بيتا الكاملة
يمكن تقليص أي فهرس مُعاد في أي وقت. وهذا يعني أساسًا عدم وجود استراتيجية تقليص محددة - فيما يتعلق بإمكانية التقليص، "كل الاحتمالات واردة".

لا تؤدي استراتيجيات الاختزال الضعيفة إلى الاختزال في ظل تجريدات لامدا:

الاتصال بالقيمة
يشبه هذا الترتيب التطبيقي، لكن لا تُجرى أي عمليات اختزال داخل التجريدات. وهذا مشابه لترتيب التقييم في اللغات الصارمة مثل لغة C: حيث تُقيّم وسائط الدالة قبل استدعائها، ولا تُقيّم أجسام الدوال جزئيًا إلا بعد استبدال الوسائط.
الاتصال بالاسم
يشبه الترتيب العادي، ولكن لا تُجرى أي اختزالات داخل التجريدات. على سبيل المثال، λ x .(λ y . y ) x يكون في شكله العادي وفقًا لهذه الاستراتيجية، على الرغم من أنه يحتوي على الاختزال (λ y . y ) x .

تقلل استراتيجيات المشاركة من العمليات الحسابية "المتشابهة" عند تنفيذها بالتوازي:

التخفيض الأمثل
كما هو الحال في الترتيب العادي، ولكن يتم تقليل العمليات الحسابية التي تحمل نفس التصنيف في وقت واحد.
اتصل عند الحاجة
يُستخدم هذا الأسلوب، الذي يعتمد على استدعاء الدالة بالاسم (وهو أسلوب ضعيف)، في تطبيقات الدوال التي قد تُكرر المصطلحات، حيث يتم تسمية الوسيط بدلاً من ذلك. يمكن تقييم الوسيط "عند الحاجة"، وعندها يتم تحديث ربط الاسم بالقيمة المُختزلة. وهذا يوفر الوقت مقارنةً بالتقييم الترتيبي العادي.

قابلية الحوسبة

لا توجد خوارزمية تأخذ تعبيرين لامدا كمدخلات وتُخرج قيمة صحيحة أو خاطئة بناءً على ما إذا كان أحدهما يُختزل إلى الآخر. [ 15 ] بتعبير أدق، لا توجد دالة قابلة للحساب قادرة على حسم المسألة. تاريخيًا، كانت هذه أول مشكلة يُمكن إثبات عدم قابليتها للحسم. وكما هو معتاد في مثل هذا البرهان، فإن قابلية الحساب تعني قابلية الحساب بواسطة أي نموذج حسابي كامل تورينج . في الواقع، يُمكن تعريف قابلية الحساب نفسها عبر حساب لامدا: الدالة F : N → N من الأعداد الطبيعية هي دالة قابلة للحساب إذا وفقط إذا وُجد تعبير لامدا f بحيث يكون لكل زوج x و y في N ، F ( x ) = y إذا وفقط إذا كان f( x) = βy ، حيث x و y هما عددا تشرش المُقابلان لـ x و y على التوالي، و = β تعني التكافؤ مع اختزال β. انظر أطروحة تشرش-تورينج للاطلاع على مناهج أخرى لتعريف قابلية الحساب وتكافؤها.  

يبدأ برهان تشرش على عدم قابلية الحساب باختزال المشكلة إلى تحديد ما إذا كان لتعبير لامدا معين شكل طبيعي . ثم يفترض أن هذا المسند قابل للحساب، وبالتالي يمكن التعبير عنه في حساب لامدا. بالاستناد إلى عمل سابق لكلين، وبناءً على ترقيم غودل لتعبيرات لامدا، يبني تشرش تعبير لامدا e يتبع بدقة برهان نظرية عدم الاكتمال الأولى لغودل . إذا طُبِّق e على عدد غودل الخاص به، ينتج تناقض.

تعقيد

يُعدّ مفهوم التعقيد الحسابي لحساب لامدا معقدًا بعض الشيء، لأن تكلفة اختزال بيتا قد تختلف باختلاف طريقة تنفيذه. [ 34 ] وللدقة، يجب إيجاد مواقع جميع حالات المتغير المقيد V في التعبير E ، مما يستلزم تكلفة زمنية، أو تتبع مواقع المتغيرات الحرة بطريقة ما، مما يستلزم تكلفة مكانية. يُعدّ البحث البسيط عن مواقع V في E من رتبة O ( n ) في طول E البالغ n . كانت سلاسل التوجيه نهجًا مبكرًا استبدل هذه التكلفة الزمنية باستخدام مساحة تربيعية. [ 35 ] وبشكل أعم، أدى ذلك إلى دراسة الأنظمة التي تستخدم الاستبدال الصريح .

في عام ٢٠١٤، تبيّن أن عدد خطوات اختزال بيتا اللازمة لاختزال حدٍّ ما باستخدام الاختزال ذي الترتيب العادي يُمثّل نموذجًا معقولًا لتكلفة الوقت، أي أنه يُمكن محاكاة الاختزال على آلة تورينج في وقت يتناسب طرديًا مع عدد الخطوات. [ ٣٦ ] كانت هذه مشكلة مفتوحة لفترة طويلة، نظرًا لتضخم حجم الحدود ، أي وجود حدود لامدا التي يزداد حجمها أُسّيًا مع كل عملية اختزال بيتا. يتجاوز هذا الحل هذه المشكلة بالعمل مع تمثيل مشترك مُدمج. يُوضّح هذا الحل أن مقدار المساحة اللازمة لتقييم حد لامدا لا يتناسب طرديًا مع حجم الحد أثناء الاختزال. ولا يُعرف حاليًا ما هو المقياس الأمثل لتعقيد المساحة. [ ٣٧ ]

لا يعني النموذج غير المنطقي بالضرورة عدم الكفاءة. يُقلل الاختزال الأمثل جميع العمليات الحسابية التي تحمل نفس التصنيف في خطوة واحدة، متجنبًا العمل المكرر، ولكن عدد خطوات اختزال بيتا المتوازية اللازمة لاختزال حد معين إلى شكله الطبيعي يتناسب خطيًا تقريبًا مع حجم الحد. هذا العدد ضئيل جدًا ليكون مقياسًا معقولًا للتكلفة، إذ يمكن ترميز أي آلة تورينج في حساب لامدا بحجم يتناسب خطيًا مع حجم آلة تورينج. لا تكمن التكلفة الحقيقية لاختزال حدود لامدا في اختزال بيتا بحد ذاته، بل في معالجة تكرار عمليات الاختزال أثناء اختزال بيتا. [ 38 ] من غير المعروف ما إذا كانت تطبيقات الاختزال الأمثل معقولة عند قياسها بنموذج تكلفة معقول، مثل عدد خطوات الاختزال من اليسار إلى الخارج للوصول إلى الشكل الطبيعي، ولكن ثبت بالنسبة لأجزاء من حساب لامدا أن خوارزمية الاختزال الأمثل فعالة، وأن تكلفتها الإضافية لا تتجاوز الدرجة الثانية مقارنةً بخطوات الاختزال من اليسار إلى الخارج. [ 37 ] بالإضافة إلى ذلك، تفوقت النسخة الأولية من تطبيق BOHM للاختزال الأمثل على كل من Caml Light و Haskell في حدود لامدا البحتة. [ 38 ]

حساب التفاضل والتكامل لامدا ولغات البرمجة

كما أشار بيتر لاندين في ورقته البحثية لعام 1965 بعنوان " مراسلة بين ALGOL 60 ورمز لامدا لتشرش "، [ 39 ] يمكن فهم لغات البرمجة الإجرائية المتسلسلة من حيث حساب لامدا، الذي يوفر الآليات الأساسية للتجريد الإجرائي وتطبيق الإجراءات (البرامج الفرعية).

الوظائف المجهولة

على سبيل المثال، في لغة بايثون، يمكن التعبير عن دالة "square" كتعبير لامدا كما يلي:

( lambda x : x ** 2 )

المثال أعلاه هو تعبير يُقيّم إلى دالة من الدرجة الأولى. يُنشئ الرمز lambdaدالة مجهولة، مع إعطاء قائمة بأسماء المعاملات - الوسيط الوحيد xفي هذه الحالة - وتعبير يُقيّم كجسم للدالة x**2. تُسمى الدوال المجهولة أحيانًا بتعبيرات لامدا.

لطالما دعمت لغة باسكال والعديد من اللغات الإجرائية الأخرى تمرير البرامج الفرعية كوسائط لبرامج فرعية أخرى عبر آلية مؤشرات الدوال . مع ذلك، لا تُعد مؤشرات الدوال شرطًا كافيًا لاعتبار الدوال أنواع بيانات من الدرجة الأولى ، لأن الدالة تُعتبر نوع بيانات من الدرجة الأولى إذا وفقط إذا أمكن إنشاء نسخ جديدة منها أثناء التشغيل . يدعم كل من سمول توك ، وجافا سكريبت ، ولغة وولفرام ، ومؤخرًا سكالا ، وإيفل (كوكلاء)، وسي شارب (كمفوضين) ، وسي++11 ، وغيرها، إنشاء الدوال أثناء التشغيل.

التوازي والتزامن

تُتيح خاصية تشرش -روسر لحساب لامدا إمكانية إجراء التقييم (اختزال بيتا) بأي ترتيب ، حتى بالتوازي. وهذا يعني أن استراتيجيات التقييم غير الحتمية المختلفة ذات صلة. مع ذلك، لا يُقدّم حساب لامدا أي بنى صريحة للتوازي . يُمكن إضافة بنى مثل المستقبلات إلى حساب لامدا. وقد طُوّرت حسابات عمليات أخرى لوصف الاتصال والتزامن.

علم الدلالة

إن حقيقة أن مصطلحات حساب لامدا تعمل كدوال على مصطلحات أخرى في حساب لامدا، وحتى على نفسها، أثارت تساؤلات حول دلالات حساب لامدا. هل يمكن إسناد معنى منطقي لمصطلحات حساب لامدا؟ الدلالة الطبيعية هي إيجاد مجموعة D متماثلة مع فضاء الدوال D → D ، أي مجموعة الدوال على نفسها. مع ذلك، لا يمكن أن توجد مجموعة D غير تافهة، وذلك بسبب قيود العدد، لأن مجموعة جميع الدوال من D إلى D لها عدد أكبر من D ، إلا إذا كانت D مجموعة أحادية .

في سبعينيات القرن العشرين، أظهر دانا سكوت أنه إذا تم النظر فقط في الدوال المتصلة ، فإنه يمكن إيجاد مجموعة أو مجال D بالخاصية المطلوبة، مما يوفر نموذجًا لحساب لامدا. [ 40 ]

وقد شكل هذا العمل أيضاً الأساس للدلالات الدلالية للغات البرمجة.

التباينات والتوسعات

هذه الإضافات موجودة في مكعب لامدا :

هذه الأنظمة الرسمية هي امتدادات لحساب التفاضل والتكامل لامدا التي لا تنتمي إلى مكعب لامدا:

هذه الأنظمة الرسمية هي اختلافات في حساب التفاضل والتكامل لامدا:

ترتبط هذه الأنظمة الرسمية بحساب التفاضل والتكامل لامدا:

  • المنطق التوافقي – تدوين للمنطق الرياضي بدون متغيرات
  • حساب التوافيق SKI – نظام حسابي يعتمد على مُوَافِقات S و K و I ، وهو مُكافئ لحساب لامدا، ولكنه قابل للاختزال دون استبدال المتغيرات.

انظر أيضاً

ملحوظات

  1. ↑ "أينم[x:=شمال]{\displaystyle M[x:=N]}يشير إلى استبدالشمال{\displaystyle N}لكل حالة من حالاتx{\displaystyle x}فيم{\displaystyle M}[ 1 ] : 7 ويُشار إليه أيضًا بـم[شمال/x]{\displaystyle M[N/x]}، "استبدالشمال{\displaystyle N}لx{\displaystyle x}فيم{\displaystyle M}[ 2 ]​
  2. ↑ Barendregt, Barendsen (2000) يسمي هذه القاعدة بديهية β
  3. ↑ للاطلاع على التاريخ الكامل، انظر كتاب كاردون وهيندلي "تاريخ حساب لامدا والمنطق التوافقي" (2006).
  4. 1 2↦{\displaystyle \mapsto }تُنطق " maps to ".
  5. ↑ يمكن نطق (λ f . M ) N على النحو التالي "دع f يكون N في M".
  6. يستخدم أريولا وبلوم [ 23 ] ما يلي: 1) بديهيات لحساب تمثيلي باستخدام رسوم بيانية لامدا دورية جيدة التكوين مُوسّعة باستخدام letrec ، للكشف عن الأشجار غير المحدودة المحتملة؛ 2) يشكل الحساب التمثيلي مع اختزال بيتا لرسوم بيانية لامدا ذات نطاق محدد امتداد أريولا/بلوم الدوري لحساب لامدا؛ 3) يستدل أريولا/بلوم على اللغات الصارمة باستخدام الاستدعاء بالقيمة ، ويقارنها بحساب موجي وحساب هاسيغاوا. الاستنتاجات في الصفحة 111. [ 23 ]

مراجع

تستند بعض أجزاء هذه المقالة إلى مواد من موقع FOLDOC ، وقد تم استخدامها بإذن .

  1. 1 2 باريندريغت, هنك ; باريندسن، إريك (مارس 2000)، مقدمة في حساب التفاضل والتكامل لامدا (PDF)
  2. ↑ استبدال صريح في مختبر n
  3. ↑ دي كيروز، روي جيه جي بي (1988). "تفسير نظري للبرمجة ودور قواعد الاختزال". ديالكتيكا . 42 (4): 265-282 . doi : 10.1111/j.1746-8361.1988.tb00919.x .
  4. ↑ تورينج، آلان م. (ديسمبر 1937). " قابلية الحوسبة وقابلية تعريف لامدا". مجلة المنطق الرمزي . 2 (4): 153-163 . doi : 10.2307/2268280 . JSTOR 2268280. S2CID 2317046 .  
  5. ↑ تايت، دبليو دبليو (أغسطس 1967). " التفسيرات القصدية للدوال من النوع الأول المحدود" . مجلة المنطق الرمزي . 32 (2): 198-212 . doi : 10.2307/2271658 . ISSN 0022-4812 . JSTOR 2271658. S2CID 9569863 .   
  6. ↑ كوكاند، تييري (8 فبراير 2006). زالتا، إدوارد ن. (محرر). "نظرية الأنواع" . موسوعة ستانفورد للفلسفة ( طبعة صيف 2013) . تم الاطلاع عليه بتاريخ 17 نوفمبر 2020 . 
  7. ↑ مورتغات، مايكل (1988). دراسات تصنيفية: الجوانب المنطقية واللغوية لحساب لامبيك . منشورات فوريس. ISBN 9789067653879.
  8. ^ بونت ، هاري. موسكينز، رينهارد، محرران. (2008). معنى الحوسبة . سبرينغر. رقم ISBN 978-1-4020-5957-5.
  9. ↑ ميتشل، جون سي. (2003). مفاهيم في لغات البرمجة . مطبعة جامعة كامبريدج. ص 57. ISBN  978-0-521-78098-8..
  10. ↑ تشاكون سارتوري، كاميلو (5 ديسمبر 2023). مقدمة في حساب لامدا باستخدام راكيت (تقرير فني). مؤرشف من الأصل في 7 ديسمبر 2023.
  11. ↑ بيرس، بنجامين سي. نظرية الفئات الأساسية لعلماء الحاسوب . ص 53. 
  12. ↑ تشرش، ألونسو (1932). "مجموعة من المسلمات لتأسيس المنطق". حوليات الرياضيات . السلسلة 2. 33 (2): 346-366 . doi : 10.2307/1968337 . JSTOR 1968337 . 
  13. ↑ كلين، ستيفن سي .؛ روسر، جيه بي (يوليو 1935). "عدم اتساق بعض المنطق الصوري". حوليات الرياضيات . 36 (3): 630. doi : 10.2307/1968646 . JSTOR 1968646 . 
  14. ↑ تشيرش، ألونسو (ديسمبر 1942). "مراجعة لكتاب هاسكل ب. كاري، عدم اتساق بعض المنطق الصوري ". مجلة المنطق الرمزي . 7 (4): 170-171 . doi : 10.2307/2268117 . JSTOR 2268117 . 
  15. 1 2 تشيرش، ألونسو (1936). "مسألة غير قابلة للحل في نظرية الأعداد الأولية". المجلة الأمريكية للرياضيات . 58 (2): 345-363 . doi : 10.2307/2371045 . JSTOR 2371045 . 
  16. ↑ تشرش، ألونسو (1940). " صياغة النظرية البسيطة للأنواع". مجلة المنطق الرمزي . 5 (2): 56-68 . doi : 10.2307/2266170 . JSTOR 2266170. S2CID 15889861 .  
  17. ↑ بارتي، بي بي إتش؛ تير مولين، أ .؛ وول، آر إي (1990). الأساليب الرياضية في اللغويات . سبرينغر. ISBN 9789027722454تم الاطلاع عليه بتاريخ 29 ديسمبر 2016 .
  18. ↑ ألاما، جيسي. زالتا، إدوارد ن. (محرران). "حساب لامدا" . موسوعة ستانفورد للفلسفة ( طبعة صيف 2013) . تم الاطلاع عليه بتاريخ 17 نوفمبر 2020 . 
  19. ↑ دانا سكوت، " نظرة إلى الماضي؛ نظرة إلى المستقبل "، محاضرة مدعوة في ورشة عمل تكريمًا لذكرى ميلاد دانا سكوت الخامسة والثمانين ومرور خمسين عامًا على نظرية المجال، 7-8 يوليو، مؤتمر FLoC 2018 (المحاضرة بتاريخ 7 يوليو 2018). يبدأ المقطع ذو الصلة عند الدقيقة 32:50 . (انظر أيضًا هذا المقتطف من محاضرة ألقيت في مايو 2016 في جامعة برمنغهام، المملكة المتحدة).
  20. ↑ فيليسين، ماتياس؛ فلات، ماثيو (2006)، لغات البرمجة وحسابات لامدا (ملف PDF) ، ص 26، مؤرشف من الأصل (ملف PDF) بتاريخ 2009-02-05 تشير ملاحظة (تم الاطلاع عليها في عام 2017) في الموقع الأصلي إلى أن المؤلفين يعتبرون العمل المشار إليه أصلاً قد تم استبداله بكتاب.
  21. ↑ سيلينجر، بيتر (2008)، محاضرات في حساب لامدا (ملف PDF) ، المجلد 0804، قسم الرياضيات والإحصاء، جامعة أوتاوا، ص 9، arXiv : 0804.3434 ، Bibcode : 2008arXiv0804.3434S  
  22. ↑ بروس، كيم ب. (2002). أسس لغات البرمجة الكائنية: الأنواع والدلالات . مطبعة معهد ماساتشوستس للتكنولوجيا. ص 151. ISBN  978-0-262-02523-2.
  23. 1 2 زينا م. أريولا وستيفان بلوم، وقائع مؤتمر TACS '94 سينداي، اليابان 1997 (1997) حسابات لامدا الدورية 114 صفحة.
  24. ↑ بيني، آدم (17 أغسطس 2017). "المُركِّبات ذات النقطة الثابتة في جافا سكريبت" . بيني ستوديو . ميديوم . تم الاطلاع عليه في 2 أغسطس 2020 .
  25. ↑ "محاضرة CS 6110 S17 رقم 5. التكرار والمُركِّبات ذات النقطة الثابتة" (ملف PDF) . جامعة كورنيل . 4.1 مُرَكِّب ذو نقطة ثابتة من نوع CBV.
  26. ↑ كير، أندرو د. "حساب لامدا وأنواعه" (ملف PDF) . ص 6. تم الاطلاع عليه بتاريخ 14 يناير 2022 . 
  27. ↑ ديزاني-سيانكاغليني، ماريانجيولا؛ غيلزان، سيلفيا (2014). "دقة التنميط الفرعي على أنواع التقاطع والاتحاد" (ملف PDF) . إعادة الكتابة وحسابات لامدا المكتوبة . سلسلة محاضرات في علوم الحاسوب. المجلد 8560. ص 196. doi : 10.1007/978-3-319-08918-8_14 . hdl : 2318/149874 . ISBN   978-3-319-08917-1تم الاطلاع عليه بتاريخ 14 يناير 2022 .
  28. ↑ فورستر، يانيك؛ سمولكا، جيرت (أغسطس 2019). "حساب لامدا بالقيمة كنموذج للحساب في Coq" (ملف PDF) . مجلة الاستدلال الآلي . 63 (2): 393-413 . doi : 10.1007/s10817-018-9484-2 . S2CID 53087112. تاريخ الاسترجاع: 14 يناير 2022 . 
  29. ↑ أنواع لغات البرمجة، صفحة 273، بنجامين سي. بيرس
  30. ↑ "نظرية تمثيل سكوت ومغلف كاروبي أحادي القيمة" (ملف PDF) . دار نشر داغشتول . تم الاطلاع عليه بتاريخ 19-05-2026 .
  31. ↑ بيرس، بنجامين سي. (2002). أنواع ولغات البرمجة . مطبعة معهد ماساتشوستس للتكنولوجيا . ص 56. ISBN  0-262-16209-1.
  32. ↑ سيستوفت، بيتر (2002). "إثبات اختزال حساب لامدا" (ملف PDF) . جوهر الحوسبة . سلسلة محاضرات في علوم الحاسوب. المجلد 2566. الصفحات 420-435 . doi : 10.1007/3-540-36377-7_19 . ISBN   978-3-540-00326-7تم الاطلاع عليه بتاريخ 22 أغسطس 2022 .
  33. ^ بيرناكا، مالغورزاتا؛ تشاراتونيك، فيتولد؛ دراب ، توماسز (2022). أندرونيك، يونيو؛ دي مورا، ليوناردو (محرران). حديقة الحيوان لاستراتيجيات الحد من حساب التفاضل والتكامل لامدا، وCoq (PDF) . إجراءات لايبنيز الدولية في مجال المعلوماتية (LIPIcs). المجلد. 237. شلوس داغستوهل – مركز لايبنتز للمعلوماتية. ص 7: 1-7: 19. دوى : 10.4230/LIPIcs.ITP.2022.7 . رقم ISBN   978-3-95977-252-5تم الاطلاع عليه بتاريخ 22 أغسطس 2022 .
  34. ↑ فراندسن، جودموند سكوفبيرج؛ ستورتيفانت، كارل (26 أغسطس 1991). "ما هو التنفيذ الفعال لحساب لامدا؟" . لغات البرمجة الوظيفية وهندسة الحاسوب: المؤتمر الخامس لجمعية آلات الحوسبة. كامبريدج، ماساتشوستس، الولايات المتحدة الأمريكية، 26-30 أغسطس 1991. وقائع المؤتمر . سلسلة محاضرات في علوم الحاسوب. المجلد 523. سبرينغر-فيرلاغ. الصفحات 289-312 . CiteSeerX 10.1.1.139.6913 . doi : 10.1007/3540543961_14 . ISBN    9783540543961.
  35. ↑ سينوت، ف. ر. (2005). "إعادة النظر في سلاسل الموجه: منهج عام للتمثيل الفعال للمتغيرات الحرة في إعادة الكتابة من الرتبة العليا" (ملف PDF) . مجلة المنطق والحوسبة . 15 (2): 201-218 . doi : 10.1093/logcom/exi010 .
  36. ↑ أكاتولي، بنيامينو؛ دال لاغو، أوغو (14 يوليو 2014). "اختزال بيتا ثابت بالفعل". وقائع الاجتماع المشترك للمؤتمر السنوي الثالث والعشرين لجمعية EACSL حول منطق علوم الحاسوب (CSL) والندوة السنوية التاسعة والعشرين لجمعية ACM/IEEE حول المنطق في علوم الحاسوب (LICS) . الصفحات 1-10 . arXiv : 1601.01233 . doi : 10.1145/2603088.2603105 . ISBN  9781450328869. S2CID 11485010 . 
  37. 1 2 أكاتولي، بنيامينو (أكتوبر 2018). "(عدم) الكفاءة ونماذج التكلفة المعقولة" . ملاحظات إلكترونية في علوم الحاسوب النظرية . 338 : 23-43 . doi : 10.1016/j.entcs.2018.10.003 .
  38. 1 2 أسبرتي، أندريا (16 يناير 2017). "حول الاختزال الفعال لمصطلحات لامدا". arXiv : 1701.04240v1 [ cs.LO ].
  39. ↑ لاندين، بي جيه (1965). "مراسلة بين لغة ALGOL 60 ورمز لامدا لتشرش" . اتصالات ACM . 8 (2): 89-101 . doi : 10.1145/363744.363749 . S2CID 6505810 . 
  40. ↑ سكوت، دانا (1993). "بديل نظري للأنواع لـ ISWIM وCUCH وOWHY" (ملف PDF) . علوم الحاسوب النظرية . 121 ( 1-2 ): 411-440 . doi : 10.1016/0304-3975(93)90095-B . تاريخ الاسترجاع: 1 ديسمبر 2022 .كُتبت عام 1969، وتم تداولها على نطاق واسع كمخطوطة غير منشورة.

للمزيد من القراءة

كتب/دراسات متخصصة لطلاب الدراسات العليا
  • سورنسن، مورتن هاين وأورزيتشين، باويل (2006)، محاضرات حول تماثل كاري-هوارد ، إلسيفير، ISBN 0-444-52077-5هذا كتاب حديث يتناول المواضيع الرئيسية لحساب لامدا، بدءًا من النوع غير المعتمد على النوع، وصولًا إلى معظم حسابات لامدا المعتمدة على النوع ، بما في ذلك التطورات الحديثة مثل أنظمة الأنواع النقية ومكعب لامدا . ولا يتناول الكتاب امتدادات الأنواع الفرعية .
  • بيرس، بنيامين (2002)، أنواع ولغات البرمجة ، مطبعة معهد ماساتشوستس للتكنولوجيا، رقم ISBN 0-262-16209-1يغطي هذا الكتاب حسابات لامدا من منظور نظام النوع العملي؛ بعض المواضيع مثل الأنواع التابعة يتم ذكرها فقط، لكن التفرع النوعي موضوع مهم.
وثائق
  1. ↑ "الصفحة الرئيسية لغريغ مايكلسون" . العلوم الرياضية والحاسوبية . ريكارتون، إدنبرة: جامعة هيريوت وات . تم الاطلاع عليه بتاريخ 6 نوفمبر 2022 .