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

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

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

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

تمت دراسة أنواع مختلفة من حسابات لامدا المكتوبة. يحتوي حساب لامدا المكتوب ببساطة على مُنشئ نوع واحد فقط ، وهو السهم.${\displaystyle \to }$وأنواعها الوحيدة هي الأنواع الأساسية وأنواع الدوال${\displaystyle \sigma \to \tau }$يُوسّع النظام T حساب لامدا البسيط ليشمل نوع الأعداد الطبيعية والاستدعاء الذاتي الأولي من الرتبة العليا ؛ في هذا النظام، يمكن تعريف جميع الدوال القابلة للحساب بشكل قاطع في حساب بيانو. يسمح النظام F بتعدد الأشكال باستخدام التكميم الشامل على جميع الأنواع؛ من منظور منطقي، يمكنه وصف جميع الدوال الكلية بشكل قاطع في منطق الرتبة الثانية . تُشكّل حسابات لامدا ذات الأنواع التابعة أساس نظرية الأنواع الحدسية ، وحساب الإنشاءات ، والإطار المنطقي (LF)، وهو حساب لامدا خالص ذو أنواع تابعة. استنادًا إلى عمل بيراردي على أنظمة الأنواع الخالصة ، اقترح هينك باريندريخت مكعب لامدا لتنظيم علاقات حسابات لامدا الخالصة (بما في ذلك حساب لامدا البسيط، والنظام F، والإطار المنطقي، وحساب الإنشاءات). ^{[ 3 ]}

تُدخل بعض حسابات لامدا المكتوبة مفهومًا للتصنيف الفرعي ، أي إذا${\displaystyle A}$هو نوع فرعي من${\displaystyle B}$ثم جميع المصطلحات من النوع${\displaystyle A}$يوجد أيضًا نوع${\displaystyle B}$. حسابات لامدا المكتوبة مع التنميط الفرعي هي حسابات لامدا المكتوبة ببساطة مع أنواع اقترانية ونظام F _<: .

جميع الأنظمة المذكورة حتى الآن، باستثناء حساب لامدا غير المُنمذج، تُعتبر أنظمة مُنمذجة بقوة : أي أن جميع العمليات الحسابية تنتهي. لذلك، لا يمكنها وصف جميع الدوال القابلة للحساب بواسطة آلة تورينج . ^{[ 4 ]} ونتيجةً لذلك، فهي متسقة كمنطق، أي أن هناك أنواعًا غير مُشغولة. مع ذلك، توجد حسابات لامدا مُنمذجة ليست مُنمذجة بقوة. على سبيل المثال، حساب لامدا المُنمذج التابع بنوع من جميع الأنواع (Type  : Type) ليس مُنمذجًا بسبب مفارقة جيرارد . هذا النظام هو أيضًا أبسط نظام نوع بحت، وهو شكلية تُعمم مكعب لامدا. الأنظمة ذات مُركبات الاستدعاء الذاتي الصريحة، مثل " لغة برمجة الدوال القابلة للحساب " (PCF) لبلوتكين ، ليست مُنمذجة، ولكنها ليست مُصممة ليتم تفسيرها كمنطق. في الواقع، PCF هي لغة برمجة وظيفية نموذجية مُنمذجة، حيث تُستخدم الأنواع لضمان حسن سلوك البرامج ولكن ليس بالضرورة لضمان انتهائها.

في برمجة الحاسوب ، تتطابق إجراءات (الدوال، والإجراءات، والأساليب) لغات البرمجة ذات الأنواع القوية بشكل وثيق مع تعبيرات لامدا ذات الأنواع. ^{[ 5 ]}

• حساب كابا - وهو نظير لحساب لامدا المكتوب الذي يستبعد الدوال ذات الرتبة الأعلى

• باريندريخت، هينك (1992). "حسابات لامدا مع الأنواع" . في أبرامسكي، س. (محرر). الخلفية: الهياكل الحسابية . دليل المنطق في علوم الحاسوب. المجلد  2. مطبعة جامعة أكسفورد. الصفحات 117-309 . ISBN  9780198537618.
• براندل، هيلموت (2022). حساب التفاضل والتكامل للإنشاءات / حساب التفاضل والتكامل لامدا المكتوب