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

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

يُستخدم مصطلح " النوع البسيط" أيضًا للإشارة إلى امتدادات حساب لامدا ذي النوع البسيط، والتي تتضمن بنيات مثل الضرب ، والضرب المشترك ، والأعداد الطبيعية ( النظام T )، أو حتى الاستدعاء الذاتي الكامل (مثل PCF ). في المقابل، لا تُعتبر الأنظمة التي تُدخل أنواعًا متعددة الأشكال (مثل النظام F ) أو أنواعًا تابعة (مثل الإطار المنطقي ) ذات نوع بسيط . وتظل الأنواع البسيطة، باستثناء الاستدعاء الذاتي الكامل، تُعتبر بسيطة لأن ترميز Church لهذه البنى يُمكن إجراؤه باستخدام فقط${\displaystyle \to }$ومتغيرات النوع المناسبة، بينما لا يمكن ذلك مع تعدد الأشكال والتبعية.

في ثلاثينيات القرن العشرين، سعى ألونسو تشيرش إلى استخدام المنهج اللوجستي : ^{[ أ ]} يتألف حساب لامدا الخاص به ، كلغة رسمية قائمة على التعبيرات الرمزية، من سلسلة لا نهائية قابلة للعد من البديهيات والمتغيرات، ^{[ ب ]} بالإضافة إلى مجموعة محدودة من الرموز الأولية، ^{[ ج ]} التي تدل على التجريد والنطاق، فضلاً عن أربعة ثوابت: النفي، والفصل، والتكميم الشامل، والاختيار على التوالي؛ ^{[ د ] [ هـ ]} وكذلك مجموعة محدودة من القواعد من الأول إلى السادس. تضمنت هذه المجموعة المحدودة من القواعد القاعدة الخامسة ( modus ponens) بالإضافة إلى القاعدتين الرابعة والسادسة للاستبدال والتعميم على التوالي. ^{[ و ]} تُعرف القواعد من الأول إلى الثالث باسم تحويلات ألفا وبيتا وإيتا في حساب لامدا. سعى تشيرش إلى استخدام اللغة الإنجليزية فقط كلغة نحوية (أي لغة ما وراء رياضية) لوصف التعبيرات الرمزية دون أي تفسيرات. ^{[ ز ]}

في عام 1940، استقر تشيرش على استخدام رمز سفلي للدلالة على النوع في التعبير الرمزي. ^{[ ب ]} في عرضه، استخدم تشيرش نوعين أساسيين فقط:${\displaystyle o}$بالنسبة إلى "نوع القضايا" و${\displaystyle \iota }$بالنسبة إلى "نوع الأفراد". النوع${\displaystyle o}$لا يحتوي على ثوابت مصطلحية، بينما${\displaystyle \iota }$يحتوي على حد ثابت واحد. غالبًا ما يكون حساب التفاضل والتكامل بنوع أساسي واحد فقط، عادةً${\displaystyle o}$، يُؤخذ في الاعتبار. الأحرف اليونانية السفلية${\displaystyle \alpha }$،​​${\displaystyle \beta }$تشير الرموز ⁠ ، إلخ. إلى متغيرات النوع؛ والرموز ذات الفهرس السفلي بين قوسين${\displaystyle (\alpha \beta )}$يشير إلى نوع الدالة${\displaystyle \beta \to \alpha }$. استخدمت الكنيسة عام 1940 صفحة 58 كلمة "سهم " أو${\displaystyle \to }$يشير الرمز ' إلى ، أو هو اختصار لـ . ^{[ g ]} بحلول سبعينيات القرن العشرين، كان يُستخدم رمز السهم المستقل؛ على سبيل المثال، في هذه المقالة، الرموز غير المُفهرسة${\displaystyle \sigma }$و${\displaystyle \tau }$يمكن أن تتنوع الأنواع. وقد تبين أن العدد اللانهائي من البديهيات هو نتيجة لتطبيق القواعد من الأول إلى السادس على الأنواع (انظر بديهيات بيانو ). بشكل غير رسمي، نوع الدالة${\displaystyle \sigma \to \tau }$يشير إلى نوع الدوال التي، عند إعطائها مدخلات من النوع ⁠${\displaystyle \sigma }$⁠ , إنتاج مخرج من النوع ⁠${\displaystyle \tau }$بحسب العرف ،${\displaystyle \to }$الزملاء على اليمين:${\displaystyle \sigma \to \tau \to \rho }$تُقرأ على النحو التالي :${\displaystyle \sigma \to (\tau \to \rho )}$⁠ .

لتحديد الأنواع، مجموعة من الأنواع الأساسية ،${\displaystyle B}$يجب تعريفها أولاً. تُسمى هذه الأنواع أحيانًا بالأنواع الذرية أو ثوابت الأنواع . بعد تحديد ذلك، تكون صيغة الأنواع كما يلي:

${\displaystyle \tau \;{{:}{:=}}\;\tau \to \tau \mid T\quad \mathrm {where} \quad T\in B.}$

على سبيل المثال ،${\displaystyle B=\{a,b\}}$، يُنشئ مجموعة لا نهائية من الأنواع تبدأ بـ${\displaystyle a}$،​​${\displaystyle b}$،​​${\displaystyle a\to a}$،​​${\displaystyle a\to b}$،​​${\displaystyle b\to b}$،​​${\displaystyle b\to a}$،​​${\displaystyle a\to (a\to a)}$...​​${\displaystyle (b\to a)\to (a\to b)}$...​

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

إن بنية حساب التفاضل والتكامل اللامدا ذي النوع البسيط هي في الأساس بنية حساب التفاضل والتكامل اللامدا نفسه. المصطلح${\displaystyle x{\mathbin {:}}\tau }$يشير إلى أن المتغير${\displaystyle x}$من النوع ⁠${\displaystyle \tau }$⁠ . مصطلح بناء الجملة، في شكل باكوس-ناور ، هو مرجع متغير ، أو تجريدات ، أو تطبيق ، أو ثابت :

${\displaystyle e\;{{:}{:=}}\;x\mid \lambda x\mathbin {:} \tau .e\mid e\,e\mid c}$

أين${\displaystyle c}$هو ثابت مصطلح. مرجع متغير${\displaystyle x}$يكون مرتبطًا إذا كان داخل ربط تجريدي${\displaystyle x}$. يكون الحد مغلقًا إذا لم تكن هناك متغيرات غير مقيدة.

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

${\displaystyle e\;{{:}{:=}}\;x\mid \lambda xe\mid e\,e}$

بينما في حساب التفاضل والتكامل اللامدا المكتوب، يجب على كل تجريد (أي دالة) تحديد نوع وسيطه.

لتحديد مجموعة مصطلحات لامدا ذات النوع الصحيح لنوع معين، يتم تعريف علاقة كتابة بين المصطلحات والأنواع. أولاً، يتم تقديم سياقات الكتابة ، أو بيئات الكتابة.${\displaystyle \Gamma ,\Delta ,\dots }$وهي عبارة عن مجموعات من افتراضات تحديد النوع. يأخذ افتراض تحديد النوع الشكل التالي :${\displaystyle x{\mathbin {:}}\sigma }$، بمعنى متغير${\displaystyle x}$لديه نوع ⁠${\displaystyle \sigma }$⁠ .

علاقة الكتابة${\displaystyle \Gamma \vdash e{\mathbin {:}}\sigma }$يشير إلى أن${\displaystyle e}$هو مصطلح من نوع${\displaystyle \sigma }$في السياق${\displaystyle \Gamma }$في هذه الحالة${\displaystyle e}$يقال إنه ذو كتابة جيدة (يمتلك نوع ⁠${\displaystyle \sigma }$تُسمى حالات علاقة التصنيف أحكام التصنيف . وتُثبت صحة حكم التصنيف بتقديم استنتاج تصنيفي ، مُنشأ باستخدام قواعد التصنيف (حيث تسمح لنا المقدمات أعلاه باستنتاج النتيجة أدناه). يستخدم حساب لامدا المُصنَّف ببساطة هذه القواعد ^: [ ^{h ]}

${\displaystyle {\frac {x{\mathbin {:}}\sigma \in \Gamma }{\Gamma \vdash x{\mathbin {:}}\sigma }}}$(1)	${\displaystyle {\frac {c{\text{ is a constant of type }}T}{\Gamma \vdash c{\mathbin {:}}T}}}$(2)
${\displaystyle {\frac {\Gamma ,x{\mathbin {:}}\sigma \vdash e{\mathbin {:}}\tau }{\Gamma \vdash (\lambda x{\mathbin {:}}\sigma .~e){\mathbin {:}}(\sigma \to \tau )}}}$(3)	${\displaystyle {\frac {\Gamma \vdash e_{1}{\mathbin {:}}\sigma \to \tau \quad \Gamma \vdash e_{2}{\mathbin {:}}\sigma }{\Gamma \vdash e_{1}~e_{2}{\mathbin {:}}\tau }}}$(4)

بالكلمات،

1. لو${\displaystyle x}$له نوع${\displaystyle \sigma }$في هذا السياق، إذن${\displaystyle x}$لديه نوع ⁠${\displaystyle \sigma }$⁠ .
2. تحتوي الثوابت الحدية على الأنواع الأساسية المناسبة.
3. إذا، في سياق معين مع${\displaystyle x}$النوع​${\displaystyle \sigma }$،​${\displaystyle e}$لديه نوع ⁠${\displaystyle \tau }$ثم ، في السياق نفسه بدون${\displaystyle x}$،​​${\displaystyle \lambda x{\mathbin {:}}\sigma .~e}$لديه نوع​${\displaystyle \sigma \to \tau }$⁠ .
4. إذا، في سياق معين،${\displaystyle e_{1}}$لديه نوع ⁠${\displaystyle \sigma \to \tau }$، و${\displaystyle e_{2}}$لديه نوع ⁠${\displaystyle \sigma }$ثم​${\displaystyle e_{1}~e_{2}}$لديه نوع ⁠${\displaystyle \tau }$⁠ .

أمثلة على المصطلحات المغلقة، أي المصطلحات التي يمكن كتابتها في السياق الفارغ، هي:

• لكل نوع${\displaystyle \tau }$مصطلح​${\displaystyle \lambda x{\mathbin {:}}\tau .x{\mathbin {:}}\tau \to \tau }$( دالة الهوية / مُركِّب الهوية)،
• للأنواع​${\displaystyle \sigma ,\tau }$مصطلح​${\displaystyle \lambda x{\mathbin {:}}\sigma .\lambda y{\mathbin {:}}\tau .x{\mathbin {:}}\sigma \to \tau \to \sigma }$(المُركِّب K)، و
• للأنواع​${\displaystyle \tau ,\tau ',\tau ''}$مصطلح​${\displaystyle \lambda x{\mathbin {:}}\tau \to \tau '\to \tau ''.\lambda y{\mathbin {:}}\tau \to \tau '.\lambda z{\mathbin {:}}\tau .xz(yz):(\tau \to \tau '\to \tau '')\to (\tau \to \tau ')\to \tau \to \tau ''}$(المُركِّب S).

هذه هي تمثيلات حساب التفاضل والتكامل اللامدا المكتوبة للمجموعات الأساسية للمنطق التوافقي .

كل نوع${\displaystyle \tau }$يتم تخصيص أمر ورقم له${\displaystyle o(\tau )}$بالنسبة للأنواع الأساسية ،${\displaystyle o(T)=0}$بالنسبة لأنواع الدوال ،${\displaystyle o(\sigma \to \tau )={\mbox{max}}(o(\sigma )+1,o(\tau ))}$أي أن ترتيب نوع ما يقيس عمق السهم المتداخل الأيسر. ومن ثم:

${\displaystyle o(\iota \to \iota \to \iota )=1}$

${\displaystyle o((\iota \to \iota )\to \iota )=2}$

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

التحقق من النوع ثنائي الاتجاه

ثمة عرض بديل آخر لحساب لامدا ذي الأنواع البسيطة يعتمد على التحقق ثنائي الاتجاه من الأنواع ^{[ 12 ]} ، والذي يتطلب عددًا أكبر من تعليقات الأنواع مقارنةً باستدلال هيندلي-ميلنر ، ولكنه أسهل في الوصف. ينقسم نظام الأنواع إلى حكمين، يمثلان كلاً من التحقق والتركيب ، مكتوبين${\displaystyle \Gamma \vdash e\Leftarrow \tau }$و${\displaystyle \Gamma \vdash e\Rightarrow \tau }$على التوالي. من الناحية التشغيلية، المكونات الثلاثة${\displaystyle \Gamma }$،​​${\displaystyle e}$، و${\displaystyle \tau }$جميعها مدخلات لعملية التحقق من الحكم${\displaystyle \Gamma \vdash e\Leftarrow \tau }$، في حين أن حكم التركيب${\displaystyle \Gamma \vdash e\Rightarrow \tau }$لا يتطلب الأمر سوى${\displaystyle \Gamma }$و${\displaystyle e}$كمدخلات، مما ينتج النوع${\displaystyle \tau }$كمخرجات. تُستخلص هذه الأحكام عبر القواعد التالية:

${\displaystyle {\frac {x{\mathbin {:}}\sigma \in \Gamma }{\Gamma \vdash x\Rightarrow \sigma }}}$[1]	${\displaystyle {\frac {c{\text{ is a constant of type }}T}{\Gamma \vdash c\Rightarrow T}}}$[2]
${\displaystyle {\frac {\Gamma ,x{\mathbin {:}}\sigma \vdash e\Leftarrow \tau }{\Gamma \vdash \lambda x.~e\Leftarrow \sigma \to \tau }}}$[3]	${\displaystyle {\frac {\Gamma \vdash e_{1}\Rightarrow \sigma \to \tau \quad \Gamma \vdash e_{2}\Leftarrow \sigma }{\Gamma \vdash e_{1}~e_{2}\Rightarrow \tau }}}$[4]
${\displaystyle {\frac {\Gamma \vdash e\Rightarrow \tau }{\Gamma \vdash e\Leftarrow \tau }}}$[5]	${\displaystyle {\frac {\Gamma \vdash e\Leftarrow \tau }{\Gamma \vdash (e{\mathbin {:}}\tau )\Rightarrow \tau }}}$[6]

لاحظ أن القواعد من [1] إلى [4] تكاد تكون متطابقة مع القواعد من (1) إلى (4) المذكورة أعلاه ، باستثناء الاختيار الدقيق لأحكام التحقق أو التركيب. ويمكن تفسير هذه الاختيارات على النحو التالي:

1. لو${\displaystyle x{\mathbin {:}}\sigma }$في هذا السياق، يمكننا توليف النوع${\displaystyle \sigma }$لـ​${\displaystyle x}$⁠ .
2. أنواع ثوابت المصطلحات ثابتة ويمكن تركيبها.
3. للتأكد من ذلك${\displaystyle \lambda x.~e}$له نوع${\displaystyle \sigma \to \tau }$في بعض السياقات، نقوم بتوسيع السياق بـ${\displaystyle x{\mathbin {:}}\sigma }$وتأكد من ذلك${\displaystyle e}$لديه نوع ⁠${\displaystyle \tau }$⁠ .
4. لو${\displaystyle e_{1}}$يُركّب النوع${\displaystyle \sigma \to \tau }$(في سياق معين)، و${\displaystyle e_{2}}$التحقق من النوع${\displaystyle \sigma }$(في السياق نفسه)، إذن${\displaystyle e_{1}~e_{2}}$يُركّب النوع${\displaystyle \tau }$⁠ .

لاحظ أن قواعد التركيب تُقرأ من الأعلى إلى الأسفل، بينما تُقرأ قواعد التحقق من الأسفل إلى الأعلى. لاحظ تحديدًا أننا لسنا بحاجة إلى أي شرح إضافي على تجريد لامدا في القاعدة [3]، لأنه يمكن استنتاج نوع المتغير المُقيد من النوع الذي نتحقق عنده من الدالة. أخيرًا، نشرح القاعدتين [5] و[6] كما يلي:

5. للتأكد من ذلك${\displaystyle e}$لديه نوع ⁠${\displaystyle \tau }$يكفي توليف النوع${\displaystyle \tau }$⁠ .
6. لو${\displaystyle e}$التحقق من النوع${\displaystyle \tau }$ثم المصطلح المشروح صراحةً${\displaystyle (e{\mathbin {:}}\tau )}$يُركّب​${\displaystyle \tau }$⁠ .

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

بالنظر إلى الدلالات القياسية، فإن حساب لامدا ذو النوع البسيط هو حساب معياري قوي : كل سلسلة من عمليات الاختزال تنتهي في النهاية. ^{[ 10 ]} هذا لأن قواعد النوع لا تسمح بالاستدعاء الذاتي: من المستحيل إيجاد أنواع للمُركِّبات ذات النقطة الثابتة وحد التكرار .${\displaystyle \Omega =(\lambda x.~x~x)(\lambda x.~x~x)}$يمكن إضافة خاصية الاستدعاء الذاتي إلى اللغة إما عن طريق وجود عامل تشغيل خاص .${\displaystyle {\mathtt {fix}}_{\alpha }}$من النوع${\displaystyle (\alpha \to \alpha )\to \alpha }$أو إضافة أنواع تكرارية عامة ، على الرغم من أن كليهما يلغي التطبيع القوي.

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

• أظهر تيت في عام 1967 أن${\displaystyle \beta }$يُعدّ الاختزال عملية تطبيع قوية . ^{[ 10 ]} وكنتيجة لذلك${\displaystyle \beta \eta }$التكافؤ قابل للتقرير . أثبت ستاتمان في عام 1979 أن مشكلة التطبيع غير أولية ، ^{[ 13 ]} وهو برهان بسّطه مايرسون لاحقًا. ^{[ 14 ]} من المعروف أن المشكلة تنتمي إلى المجموعة${\displaystyle {\mathcal {E}}^{4}}$من التسلسل الهرمي لغريغورتشيك ، ^{[ 15 ]} وبشكل أدق، فهو كامل في فئة التعقيد المسماة TOWER . ^{[ 16 ]} قدم بيرغر وشفيتشتنبرغ برهانًا للتطبيع الدلالي البحت (انظر التطبيع بالتقييم ) في عام 1991. ^{[ 17 ]}
• مشكلة التوحيد لـ${\displaystyle \beta \eta }$التكافؤ غير قابل للتقرير. أثبت هويه في عام 1973 أن التوحيد من الرتبة الثالثة غير قابل للتقرير ^{[ 18 ]} ، وقد حسّن باكستر هذا الإثبات في عام 1978 ^{[ 19 ]} ، ثم غولدفراب في عام 1981 ^{[ 20 ]} بإثبات أن التوحيد من الرتبة الثانية غير قابل للتقرير بالفعل. أعلن كولن ستيرلينغ في عام 2006 عن برهان على أن المطابقة من الرتب العليا (التوحيد الذي يحتوي فيه حد واحد فقط على متغيرات وجودية) قابلة للتقرير، ونُشر برهان كامل في عام 2009. ^{[ 21 ]}
• يمكننا ترميز الأعداد الطبيعية باستخدام مصطلحات من النوع${\displaystyle (o\to o)\to (o\to o)}$( الأرقام الكنسية ). أظهر شفيتشتنبرغ في عام 1975 أنه في${\displaystyle \lambda ^{\to }}$يمكن تمثيل كثيرات الحدود الممتدة بالضبط كدوال على أرقام الكنيسة؛ ^{[ 22 ]} هذه هي تقريبًا كثيرات الحدود المغلقة تحت عامل شرطي.
• نموذج كامل لـ${\displaystyle \lambda ^{\to }}$يُعطى ذلك بتفسير الأنواع الأساسية كمجموعات وأنواع الدوال بواسطة فضاء الدوال النظري للمجموعات . وقد أظهر فريدمان في عام 1975 أن هذا التفسير كامل لـ${\displaystyle \beta \eta }$التكافؤ، إذا تم تفسير الأنواع الأساسية بواسطة مجموعات غير منتهية. ^{[ 23 ]} أظهر ستاتمان في عام 1983 أن${\displaystyle \beta \eta }$التكافؤ هو أقصى تكافؤ يكون عادةً غامضًا ، أي مغلقًا تحت استبدالات النوع ( نظرية ستاتمان للغموض النموذجي ). ^{[ 24 ]} ومن نتائج ذلك أن خاصية النموذج المحدود صحيحة، أي أن المجموعات المحدودة كافية لتمييز المصطلحات التي لا يتم تحديدها بواسطة${\displaystyle \beta \eta }$التكافؤ.
• قدّم بلوتكين العلاقات المنطقية عام 1973 لوصف عناصر النموذج التي يمكن تعريفها باستخدام مصطلحات لامدا. ^{[ 25 ]} وفي عام 1993، بيّن يونغ وتيورين أن شكلاً عاماً من العلاقات المنطقية (علاقات كريپكي المنطقية ذات الرتبة المتغيرة) يصف بدقة قابلية تعريف لامدا. ^{[ 26 ]} افترض بلوتكين وستاتمان أنه من الممكن تحديد ما إذا كان عنصر معين من نموذج مُولّد من مجموعات منتهية قابلاً للتعريف باستخدام مصطلح لامدا ( فرضية بلوتكين-ستاتمان ). وقد أثبت لودر خطأ هذه الفرضية عام 2001. ^{[ 27 ]}

• لودر، رالف (فبراير 1998). "ملاحظات حول حساب التفاضل والتكامل لامدا المكتوب ببساطة" .
• مدخل "نظرية الأنواع عند تشيرش" في موسوعة ستانفورد للفلسفة