تطابق كاري-هوارد

في نظرية لغات البرمجة ونظرية البرهان، تطابق كاري-هوارد هي العلاقة المباشرة بين البرامج والبراهين الراضية. تُعرف أيضًا باسم تماثل كاري-هوارد أو المعادلة, أو البرهانات كبرامج والمقترحات- أو الصيغ كأنواع تفسير.

هي تعميم للتمثيل الصرفي للتمثيل بين أنظمة المنطق الرسمي وحسابات الحوسبة التي اكتشفها لأول مرة عالم الرياضيات الأمريكي هاسكل كاري والمنطقي ويليام آلفين هوارد.^[1] هي الرابط بين المنطق والحوسبة الذي يُنسب عادة إلى كاري وهوارد، على الرغم من أن الفكرة تتعلق بالتفسير التشغيلي للمنطق الحسي الذي قدمه لويتسن براور، أريند هيتينغ ^{[الإنجليزية]} وأندريه كولموغوروف^[2] وستيفن كول كلين (انظر قابلية التحقيق ^{[الإنجليزية]}). تم توسيع العلاقة لتشمل نظرية الفئات كـمراسلة كاري-هوارد-لامبك.^[3]^[4]^[5]

الأصل والنطاق والنتائج

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

في عام 1934، لاحظ هاسكل كاري أن أنواع المجمّعين يمكن أن تُرى كمخطط-مفردات لمنطق الاستدلال التضميني.^[6]
في عام 1958، لاحظ أن نوعًا معينًا من أنظمة البرهان، والذي يُشار إليه بنظام الاستدلال بأسلوب هيلبرت، يتزامن مع جزء من نموذج حوسبة معروف باسم منطق تجميعي.^[7]
في عام 1969، لاحظ ويليام آلفين هوارد أن نوعًا آخر من أنظمة البرهان، والذي يُشار إليه بالاستدلال الطبيعي، يمكن تفسيره بشكل مباشر في نسخته منطق الاستدلال كنوع مطبوع من نموذج حوسبة يعرف بتكامل لامدا.^[8]

مطابقة كاري-هوارد هي الملاحظة التي تشير إلى وجود تماثل بين أنظمة البرهان، ونماذج الحوسبة. إنها بيان بأن هاتين العائلتين من الأشكال يمكن اعتباره متماثلين.

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

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

أنظمة حساب لامدا المطبوع المشتقة من نموذج كاري-هوارد أدت إلى برامج مثل "Rocq"، حيث يمكن تمثيل البرهانات كبرامج والتحقق منها وتشغيلها. الاتجاه العكسي هو استخدام برنامج لاستخراج برهان، بالنظر إلى صحته—وهو مجال بحث مرتبط بشكل وثيق بالرمز الحامل للبرهان. هذا غير ممكن إلا إذا كانت لغة برمجة التي كُتب فيها البرنامج غنية جدًا بالأنواع: لقد تم تحفيز تطوير مثل هذه الأنظمة لأنواع البيانات جزئيًا بالرغبة في جعل مراسلة كاري-هوارد ذات صلة عملية.

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

نظرًا لاحتمالية كتابة برامج غير منتهية، يجب تفسير نماذج الحساب كمال تورنغ (مثل اللغات التي تحتوي على العودية) بعناية، حيث يؤدي التطبيق الساذج للمراسلة إلى منطق غير متسق. أفضل طريقة للتعامل مع الحسابات غير المحدودة من وجهة نظر منطقية ما زالت موضوعًا نشطًا للبحث، لكن أحد الأساليب الشائعة يعتمد على استخدام المونادات لفصل الأكواد التي يمكن إثبات إنهائها عن الأكواد التي قد تكون غير منتهية (وهو أسلوب يعمم أيضًا على نماذج حسابية أكثر غنى،^[9] وهو نفسه مرتبط بالمنطق المودالي من خلال تمديد طبيعي لتماثل كاري-هوارد^{[ext 1]}). أحد الأساليب الأكثر راديكالية، التي يدافع عنها البرمجة الوظيفية الكاملة، هو القضاء على العودية غير المحدودة (والتنازل عن كمال تورنغ، مع الاحتفاظ بالتعقيد الحسابي العالي)، باستخدام المزيد من التحقق التكراري حيثما يكون السلوك غير المنتهي مرغوبًا فيه.

الصياغة العامة

في صياغتها الأكثر عمومية، تعد مراسلة كاري-هوارد مراسلة بين أنظمة البرهان الرسمية ونظام الأنواع لـنموذج حوسبة. على وجه الخصوص، تنقسم إلى مراسلتين. واحدة على مستوى صيغة جيدة التكوين ونوع بيانات الذي لا يعتمد على أي نظام برهان أو نموذج حوسبة معين يتم اعتباره، وأخرى على مستوى البراهين الرياضية والبرامج التي تكون هذه المرة محددة بالاختيار الخاص لنظام البرهان ونموذج الحوسبة المعتمد.

على مستوى الصيغ والأنواع، تقول المراسلة أن التضمين يتصرف مثل نوع دالة، والتقاطع مثل نوع "المنتج" (يمكن تسمية هذا بالـtuple أو الـstruct أو الـlist أو مصطلح آخر حسب اللغة)، والتفاضل مثل نوع المجموع (يمكن تسمية هذا النوع بالاتحاد)، والصيغة الكاذبة مثل النوع الفارغ والصيغة الصحيحة مثل نوع الوحدة (الذي يتضمن العضو الوحيد هو الكائن الفارغ). تتوافق الكميات مع المساحة الوظيفية المعتمدة أو المنتجات (حسب المناسب).

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

الجانب المنطقي	الجانب البرمجي
الصيغة	النوع
البرهان	المصطلح
الصيغة صحيحة	النوع يحتوي على عنصر
الصيغة خاطئة	النوع لا يحتوي على عنصر
الثابت المنطقي ⊤ (الصدق)	نوع الوحدة
الثابت المنطقي ⊥ (الكذب)	النوع الفارغ
التضمين المنطقي	نوع الدالة
العطف المنطقي	نوع المنتج
التفاضل المنطقي	نوع المجموع
التكميل الكوني	نوع المنتج المعتمد
التكميل الوجودي	نوع المجموع المعتمد

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

الجانب المنطقي	الجانب البرمجي
نظام الاستدلال على الطراز هيلبرت	نظام النوع لللمنطق التركيبي
الاستدلال الطبيعي	نظام النوع لتكامل لامدا

بين نظام الاستدلال الطبيعي وحساب لامدا، توجد المطابقات التالية:

الجانب المنطقي	الجانب البرمجي
فرضية	المتغيرات الحرة
قياس استثنائي (modus ponens)	التطبيق
إدخال التضمين	التجريد

الأنظمة المتوافقة

أنظمة الاستدلال على الطراز هيلبرت الحدسية والمنطق التركيبي الموصوف بالأنواع

كان ذلك في البداية ملاحظة بسيطة في كتاب كوري وفيس عام 1958 حول المنطق التركيبي: الأنواع الأبسط للمنظمات الأساسية K و S في المنطق التركيبي كانت تطابق بشكل مفاجئ مخططات المسلمة α → (β → α) و (α → (β → γ)) → ((α → β) → (α → γ)) المستخدمة في أنظمة الاستدلال على الطراز هيلبرت. لهذا السبب، تُسمى هذه المخططات الآن غالباً بالمسلمات K و S. يتم إعطاء أمثلة على البرامج التي يُنظر إليها كدلائل في منطق على طراز هيلبرت أدناه.

إذا تم التقيد بالجزء الحدسي المتعلق بالاستدلالات، فإن الطريقة البسيطة لتشكيل المنطق على طراز هيلبرت هي كما يلي. لنفترض أن Γ هي مجموعة من الصيغ المحدودة، ويُنظر إليها على أنها فرضيات. عندها δ تعتبر "مستنتجة" من Γ، ويرمز لها بـ Γ ⊢ δ في الحالات التالية:

δ هي فرضية، أي هي صيغة من Γ،
δ هي حالة من مخطط المسلمة؛ أي، ضمن أكثر أنظمة المسلمات شيوعاً:
- δ تأخذ الشكل α → (β → α)، أو
- δ تأخذ الشكل (α → (β → γ)) → ((α → β) → (α → γ)),
δ تتبع بالاستدلال، أي، لوجود α، كل من α → δ و α مستنتجان بالفعل من Γ (هذه هي قاعدة قياس استثنائي)

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

يمكن صياغة المنطق التركيبي الموصوف بالأنواع باستخدام بنية مشابهة: لنفترض أن Γ هي مجموعة من المتغيرات المحدودة، مع توضيح أنواعها. سيكون للعبارة T (أيضاً مع توضيح نوعها) اعتماد على هذه المتغيرات [Γ ⊢ T:δ] عندما:

T هو أحد المتغيرات في Γ،
T هو منظم أساسي؛ أي، ضمن أساس المنظمات الشائع:
- T هو K:α → (β → α) [حيث α و β يرمزان إلى أنواع وسائطه]، أو
- T هو S:(α → (β → γ)) → ((α → β) → (α → γ)),
T هو تركيب لمصطلحين فرعيين يعتمدان على المتغيرات في Γ.

يتم إعطاء قواعد التوليد هنا في العمود الأيمن أدناه. ملاحظة كوري ببساطة تفيد أن كلا العمودين يتطابقان بشكل واحد إلى واحد. يقتصر تطابق المنطق الحدسي على المنطق الحدسي مما يعني أن بعض النتائج المبدئية، مثل قانون بيرس ((α → β) → α) → α، مستبعدة من التطابق.

منطق الاستدلال الحدسي على طراز هيلبرت	المنطق التركيبي الموصوف بالأنواع
${\frac {\alpha \in \Gamma }{\Gamma \vdash \alpha }}\qquad \qquad {\text{Assum}}$	${\frac {x:\alpha \in \Gamma }{\Gamma \vdash x:\alpha }}$
${\frac {}{\Gamma \vdash \alpha \rightarrow (\beta \rightarrow \alpha )}}\qquad {\text{Ax}}_{K}$	${\frac {}{\Gamma \vdash K:\alpha \rightarrow (\beta \rightarrow \alpha )}}$
${\frac {}{\Gamma \vdash (\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}\;{\text{Ax}}_{S}$	${\frac {}{\Gamma \vdash S:(\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}$
${\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}\quad {\text{Modus Ponens}}$	${\frac {\Gamma \vdash E_{1}:\alpha \rightarrow \beta \qquad \Gamma \vdash E_{2}:\alpha }{\Gamma \vdash E_{1}\;E_{2}:\beta }}$

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

جانب المنطق	جانب البرمجة
الافتراض	المتغير
مخططات المسلمات	المنظمات
قياس استثنائي	التطبيق
نظرية الاستدلال	إزالة التجريد

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

بالمقابل، فإن عدم القابلية للإثبات في المنطق الحدسي لـ قانون بيرس يمكن نقله مرة أخرى إلى المنطق التركيبي: لا يوجد مصطلح مبرمج في المنطق التركيبي يمكن أن يُخصص له النوع

((α → β) → α) → α.

يمكن أيضاً نقل النتائج المتعلقة بكمال بعض مجموعات المنظمات أو المسلمات. على سبيل المثال، حقيقة أن المنظم X يشكل أساس نقطة واحدة ^{[لغات أخرى]}‏ للمنطق التركيبي (الامتدادي) تعني أن مخطط المسلمة الوحيد

(((α → (β → γ)) → ((α → β) → (α → γ))) → ((δ → (ε → δ)) → ζ)) → ζ,

الذي هو النوع الرئيسي لـ X, هو استبدال مناسب للمزيج من مخططات المسلمات

α → (β → α) و

(α → (β → γ)) → ((α → β) → (α → γ)).

الاستدلال الطبيعي الحدسي و تكامل لامدا الموصوف بالأنواع

بعد أن أشار هاسكل كاري إلى المطابقة الصرفية بين الاستدلال الحدسي على طراز هيلبرت والمنطق التركيبي الموصوف بالأنواع، أوضح ويليام آلفين هوارد في عام 1969 تشابهًا صرفيًا بين البرامج في تكامل لامدا الموصوف بالأنواع والأدلة في الاستدلال الطبيعي. أدناه، يُعرض الجانب الأيسر بشكل رسمي للاستدلال الطبيعي الحدسي للفرضيات كحساب للسلسلات (يعد استخدام السلسلات أمرًا شائعًا في مناقشات التناظر بين كاري وهوارد حيث يسمح لقاعدة الاستدلال أن تُصرح بشكل أنظف)، والجانب الأيمن يُظهر قواعد التخصيص في تكامل لامدا. في الجانب الأيسر، تشير Γ، Γ₁ وΓ₂ إلى تسلسلات مرتبة من الصيغ بينما في الجانب الأيمن، تشير إلى تسلسلات من الصيغ المسماة (أي المخصصة بالأنواع) مع جميع الأسماء مختلفة.

الاستدلال الطبيعي الحدسي	قواعد تخصيص النوع في تكامل لامدا
${\frac {}{\Gamma _{1},\alpha ,\Gamma _{2}\vdash \alpha }}{\text{Ax}}$	${\frac {}{\Gamma _{1},x:\alpha ,\Gamma _{2}\vdash x:\alpha }}$
${\frac {\Gamma ,\alpha \vdash \beta }{\Gamma \vdash \alpha \rightarrow \beta }}\rightarrow I$	${\frac {\Gamma ,x:\alpha \vdash t:\beta }{\Gamma \vdash (\lambda x\!:\!\alpha .~t):\alpha \rightarrow \beta }}$
${\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}\rightarrow E$	${\frac {\Gamma \vdash t:\alpha \rightarrow \beta \qquad \Gamma \vdash u:\alpha }{\Gamma \vdash t\;u:\beta }}$

لإعادة صياغة المطابقة، فإن إثبات Γ ⊢ α يعني امتلاك برنامج يقوم، عند إعطائه قيمًا بالأنواع المدرجة في Γ، بإنشاء كائن من النوع α. يتوافق الافتراض/الفرضية مع إدخال متغير جديد بنوع جديد غير مقيد، وقاعدة $\to I$ تتوافق مع تجريد الدالة وقاعدة $\to E$ تتوافق مع تطبيق الدالة. لاحظ أن المطابقة ليست دقيقة إذا تم أخذ السياق Γ كمجموعة من الصيغ، حيث على سبيل المثال، لن يتم التمييز بين مصطلحات λ-التي هي λx.λy.x و λx.λy.y من النوع $α \to α \to α$ في المطابقة. يتم إعطاء الأمثلة أدناه.

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

جانب المنطق	جانب البرمجة
الافتراض/الفرضية	المتغير
قاعدة الإدخال	المنشئ
قاعدة الاستبعاد	المحلل
الاستدلال العادي	الشكل العادي
تطبيع الاستدلالات	التطبيع الضعيف
القابلية للإثبات	نوع الإقامة
التوافق الحدسي	النوع المسكون عالميًا

تتمدد مطابقة هوارد بشكل طبيعي إلى امتدادات أخرى للاستدلال الطبيعي وتكامل لامدا الموصوف بالأنواع. فيما يلي قائمة غير شاملة:

نظام F لجيرارد-رينولد كلغة مشتركة لكل من منطق المقترحات من الدرجة الثانية وتكامل لامدا الموصوف بالأنواع البوليموريك.
المنطق من الدرجة الأعلى ونظام F_ω لجيرارد.
الأنواع الاستقرائية كالنوع البياني الجبري.
الضرورة $\Box$ في منطق موجهات وحساب المراحل^{[ext 2]}
الإمكانية $\Diamond$ في منطق موجهات وأنواع الموناد للتأثيرات^{[ext 1]}
حساب $λ I$ (حيث يُقتصر التجريد على λx.E حيث x يحتوي على ظهور واحد على الأقل في E) وCL_I تتوافق مع المنطق ذي الصلة.^[10]
الحقيقة المحلية (∇) في طوبولوجيا غروثنديك أو المعامل المكافئ "المرن" (◯) لـ بينتون، بييرمان، ودي بايفا (1998) تتوافق مع منطق CL الذي يصف "أنواع الحساب".^[11]

المنطق الكلاسيكي وموصلات التحكم

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

جانب المنطق	جانب البرمجة
قانون بيرس: ((α → β) → α) → α	الاستدعاء مع الاستمرارية الجارية
ترجمة النفي المزدوج	الاستمرارية

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

حساب المتتاليات

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

يتميز حساب المتتاليات بوجود قواعد إدخال لليسار، وقاعدة إدخال لليمين، وقاعدة القطع التي يمكن إلغاؤها. هيكل حساب المتتاليات يتعلق بحساب يكون هيكله قريبًا من هيكل بعض الآلات المجردة. المطابقة غير الرسمية هي كما يلي:

جانب المنطق	جانب البرمجة
إلغاء القطع	التبسيط في شكل آلة مجردة
قواعد الإدخال لليمين	منشئو الكود
قواعد الإدخال لليسار	منشئو أكوام التقييم
الأولوية للجانب الأيمن في إلغاء القطع	استراتيجية التقييم التبسيط
الأولوية للجانب الأيسر في إلغاء القطع	استراتيجية التقييم التبسيط

المطابقات المتعلقة بالأدلة-البرامج

دور دي بروين

استخدم [[نيكولاس غوفيرت دي بروين] تدوين اللامدا لتمثيل أدلة نظام التحقق من النظريات أوتومات، ويمثل المقترحات كـ "فئات" من أدلتها. في أواخر الستينات، في نفس الفترة التي كتب فيها هاوارد مخطوطته؛ كان دي بروين على الأرجح غير مدرك لأعمال هاوارد، وذكر المطابقة بشكل مستقل (سورنسن وأورزيشين [1998] 2006، الصفحات 98–99). يميل بعض الباحثين إلى استخدام مصطلح "مطابقة كاري-هاوارد-دي بروين" بدلاً من "مطابقة كاري-هاوارد".

تفسير بروير-هايتينغ-كولموغوروف

يفسر تفسير بروير-هايتينغ-كولموغوروف الأدلة الحدسية كدوال، لكنه لا يحدد فئة الدوال المناسبة للتفسير. إذا تم أخذ حساب اللامدا كفئة لهذه الدوال، فإن تفسير BHK يحدد نفس الشيء مثل مطابقة هاوارد بين الاستدلال الطبيعي وحساب اللامدا.

التحقيق القابل للتنفيذ

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

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

تفسير كورت غودل تفسير ديالكتيكا يحقق (تمديدًا) الحساب الحدسي باستخدام الدوال القابلة للحساب. العلاقة مع حساب اللامدا غير واضحة، حتى في حالة الاستدلال الطبيعي.

مطابقة كاري-هاوارد-لامبك

أظهر جواكيم لامبك في أوائل السبعينات أن أدلة المنطق القيمي الحدسي والمنظمات اللامدية لأنواع اللامدا ذات الأنواع المجمعة في المنطق التجميعي تشترك في نظرية معادلات مشتركة، وهي نظرية الفئات المغلقة الكارتيسية. يتم استخدام تعبير "مطابقة كاري-هاوارد-لامبك" الآن من قبل بعض الأشخاص للإشارة إلى العلاقات بين المنطق الحدسي، حساب اللامدا ذي الأنواع، والفئات المغلقة الكارتيسية. في ظل هذه المطابقة، يمكن تفسير كائنات الفئة المغلقة كارتيسياً على أنها مقترحات (أنواع)، والمورفismes على أنها استدلالات تربط مجموعة من الافتراضات (سياق الأنواع) إلى نتيجة صحيحة (مصطلح مُصنف بشكل صحيح).^[12] مطابقة لامبك هي مطابقة لنظريات المعادلات، حيث يتم تجريد الديناميكيات الخاصة بالحساب مثل تقليص بيتا وتطبيع المصطلحات، ولا تمثل تعبيرًا عن هوية تركيبية للهياكل كما هو الحال بالنسبة لمطابقات كاري وهاوارد: أي أن هيكل المورفزم المحدد في فئة مغلقة كارتيسيا لا يمكن مقارنته بهيكل دليل الحكم المقابل في منطق هيلبرت أو الاستدلال الطبيعي. على سبيل المثال، من غير الممكن أن نصرح أو نثبت أن المورفزم يُطَبِّع، أو نثبت نظرية من نوع "تشارش-روسر"، أو نتحدث عن فئة مغلقة كارتيسيا "تطبيعًا قويًا". لتوضيح هذا التمييز، يعاد صياغة الهيكل التركيبي الأساسي للفئات المغلقة كارتيسيا أدناه.

الأشياء (المقترحات/الأنواع) تشمل:

$\top$ ككائن
إذا كانت $\alpha$ و $\beta$ كائنات، فإن $\alpha \times \beta$ و $\alpha \rightarrow \beta$ كائنات.

المورفزمات (الاستدلالات/المصطلحات) تشمل:

الهويات: ${\text{id}}_{\alpha }:\alpha \to \alpha$
التكوين: إذا كان $t:\alpha \to \beta$ و $u:\beta \to \gamma$ مورفزمات، فإن $u\circ t:\alpha \to \gamma$ هو مورفزم
المورفزمات النهائية: $\star _{\alpha }:\alpha \to \top$
المنتجات: إذا كان $t:\alpha \to \beta$ و $u:\alpha \to \gamma$ مورفزمات، فإن $(t,u):\alpha \to \beta \times \gamma$ هو مورفزم
الإسقاطات: $\pi _{\alpha ,\beta ,1}:\alpha \times \beta \to \alpha$ و $\pi _{\alpha ,\beta ,2}:\alpha \times \beta \to \beta$
التقييم: ${\text{eval}}_{\alpha ,\beta }:(\alpha \to \beta )\times \alpha \to \beta$
التكرير: إذا كان $t:\alpha \times \beta \to \gamma$ مورفزم، فإن $\lambda t:\alpha \to \beta \to \gamma$ هو مورفزم.

بما يعادل التعليقات أعلاه، يمكن بناء المورفزمات المحددة بشكل جيد (المصطلحات المصنفة) في أي فئة مغلقة كارتيسيا وفقًا للقواعد قواعد الأنواع التالية. تم استبدال تدوين المورفزم الفئوي المعتاد $f:\alpha \to \beta$ بتدوين سياق الأنواع $\alpha \vdash f:\beta$ .

الهوية:

{\frac {}{\alpha \vdash {\text{id}}:\alpha }}

التكوين:

{\frac {\alpha \vdash t:\beta \qquad \beta \vdash u:\gamma }{\alpha \vdash u\circ t:\gamma }}

النوع الوحيد (الكائن النهائي):

{\frac {}{\alpha \vdash \star :\top }}

المنتج الكارتيسي:

{\frac {\alpha \vdash t:\beta \qquad \alpha \vdash u:\gamma }{\alpha \vdash (t,u):\beta \times \gamma }}

الإسقاطات اليسرى واليمنى:

{\frac {}{\alpha \times \beta ~\vdash ~\pi _{1}:\alpha }}\qquad {\frac {}{\alpha \times \beta ~\vdash ~\pi _{2}:\beta }}

التكرير (تقنية في البرمجة الوظيفية):

{\frac {\alpha \times \beta ~\vdash ~t:\gamma }{\alpha \vdash \lambda t:\beta \to \gamma }}

التطبيق:

{\frac {}{(\alpha \rightarrow \beta )\times \alpha \vdash {\text{eval}}:\beta }}

أخيرًا، المعادلات في الفئة هي:

${\text{id}}\circ t=t$
$t\circ {\text{id}}=t$
$(v\circ u)\circ t=v\circ (u\circ t)$
$\star ={\text{id}}$ (إذا كانت المصطلحات مصنفة بشكل جيد)
$\star \circ u=\star$
$\pi _{1}\circ (t,u)=t$
$\pi _{2}\circ (t,u)=u$
$(\pi _{1},\pi _{2})=id$
$(t_{1},t_{2})\circ u=(t_{1}\circ u,t_{2}\circ u)$
${\text{eval}}\circ (\lambda t\circ \pi _{1},\pi _{2})=t$
$\lambda {\text{eval}}={\text{id}}$
$\lambda t\circ u=\lambda (t\circ (u\circ \pi _{1},\pi _{2}))$

تستنتج هذه المعادلات القوانين $\eta$ التالية:

$(\pi _{1}\circ t,\pi _{2}\circ t)=t$
$\lambda ({\text{eval}}\circ (t\circ \pi _{1},\pi _{2}))=t$

الآن، يوجد $t$ بحيث $\alpha _{1}\times \ldots \times \alpha _{n}\vdash t:\beta$ إذا وفقط إذا كانت $\alpha _{1},\ldots ,\alpha _{n}\vdash \beta$ قابلة للإثبات في المنطق الحدسي الاستنباطي.

أمثلة

بفضل مطابقة كوري–هوارد، فإن التعبير النمطي الذي يتوافق نوعه مع صيغة منطقية يكون موازياً لإثبات تلك الصيغة. فيما يلي بعض الأمثلة.

المركّب الهوية باعتباره إثباتًا لـ α → α في منطق هيلبرت

كمثال، فلننظر إلى إثبات النظرية $α \to α$ . في حساب لامدا، هذا هو نوع دالة الهوية I = λx.x، وفي المنطق التركيبي يتم الحصول على دالة الهوية بتطبيق S = λfgx.fx(gx) مرتين على K = λxy.x. أي أن I = ((S K) K). كتوصيف للإثبات، فإن هذا يعني أن الخطوات التالية يمكن استخدامها لإثبات $α \to α$ :

تطبيق المخطط الثاني للبديهية باستخدام الصيغ $α$ ، $β \to α$ و $α$ للحصول على إثبات لـ:

  $(α \to ((β \to α) \to α)) \to ((α \to (β \to α)) \to (α \to α))$ ,

تطبيق المخطط الأول للبديهية مرة واحدة باستخدام $α$ و $β \to α$ للحصول على إثبات لـ:

  $α \to ((β \to α) \to α)$ ,

تطبيق المخطط الأول للبديهية مرة ثانية باستخدام $α$ و $β$ للحصول على إثبات لـ:

  $α \to (β \to α)$ ,

تطبيق قاعدة القياس (Modus Ponens) مرتين للحصول على إثبات لـ:

  $α \to α$

بشكل عام، الإجراء هو أنه كلما احتوى البرنامج على تطبيق من الشكل (P Q), يجب اتباع الخطوات التالية:

أولاً، إثبات النظريات المقابلة لأنواع P وQ.
بما أن P يتم تطبيقه على Q، يجب أن يكون نوع P من الشكل $α \to β$ ونوع Q من الشكل $α$ لبعض $α$ و $β$ . وبالتالي، يمكن فصل النتيجة $β$ باستخدام قاعدة القياس.

مركّب التركيب باعتباره إثباتًا لـ (β → α) → (γ → β) → γ → α في منطق هيلبرت

كمثال أكثر تعقيدًا، دعنا ننظر إلى النظرية التي تقابل الدالة B. نوع B هو: $(β \to α) \to (γ \to β) \to γ \to α$ . B تعادل: (S (K S) K). هذا هو مخططنا لإثبات النظرية: $(β \to α) \to (γ \to β) \to γ \to α$ .

الخطوة الأولى هي بناء (K S). لجعل مقدم بديهية K يبدو كأنه بديهية S، نضبط $α$ ليكون $(α \to β \to γ) \to (α \to β) \to α \to γ$ ، و $β$ ليكون $δ$ (لتفادي تعارض المتغيرات):

K : α → β → α

K[α = (α → β → γ) → (α → β) → α → γ, β = δ] : ((α → β → γ) → (α → β) → α → γ) → δ → (α → β → γ) → (α → β) → α → γ

بما أن المقدم هنا هو فقط S، يمكن فصل النتيجة باستخدام قاعدة القياس:

K S : δ → (α → β → γ) → (α → β) → α → γ

هذه هي النظرية التي تتوافق مع نوع (K S). الآن نطبق S على هذا التعبير. نأخذ S على النحو التالي:

S : (α → β → γ) → (α → β) → α → γ,

نضع $α = δ$ , $β = α \to β \to γ$ , و $γ = (α \to β) \to α \to γ$ ، لينتج:

S[α = δ, β = α → β → γ, γ = (α → β) → α → γ] : (δ → (α → β → γ) → (α → β) → α → γ) → (δ → (α → β → γ)) → δ → (α → β) → α → γ

ثم نفصل النتيجة:

S (K S) : (δ → α → β → γ) → δ → (α → β) → α → γ

هذه هي الصيغة المقابلة لنوع (S (K S)). حالة خاصة من هذه النظرية تكون عندما $δ = (β \to γ)$ :

S (K S)[δ = β → γ] : ((β → γ) → α → β → γ) → (β → γ) → (α → β) → α → γ

الإثبات العادي لـ (β → α) → (γ → β) → γ → α في الاستنتاج الطبيعي كما يُرى كـ λ-تعبير

يعرض المخطط أدناه إثباتًا للصيغة $(β \to α) \to (γ \to β) \to γ \to α$ في نظام الاستنتاج الطبيعي، ويوضح كيف يمكن تفسير هذا الإثبات باعتباره تعبير لامبدا $λ a .λ b .λ g .(a (b g))$ من النوع $(β \to α) \to (γ \to β) \to γ \to α$ .

                                     a:β → α, b:γ → β, g:γ ⊢ b : γ → β    
                                     a:β → α, b:γ → β, g:γ ⊢ g : γ  
———————————————————————————————————  ————————————————————————————————————————————————————————————————————  
         a:β → α, b:γ → β, g:γ ⊢ a : β → α      
         a:β → α, b:γ → β, g:γ ⊢ b g : β  
————————————————————————————————————————————————————————————————————————  
               a:β → α, b:γ → β, g:γ ⊢ a (b g) : α  
               ————————————————————————————————————  
               a:β → α, b:γ → β ⊢ λ g. a (b g) : γ → α  
               ————————————————————————————————————————  
                        a:β → α ⊢ λ b. λ g. a (b g) : (γ → β) → γ → α  
                        ————————————————————————————————————  
                                ⊢ λ a. λ b. λ g. a (b g) : (β → α) → (γ → β) → γ → α

تطبيقات أخرى

مؤخرًا، اقتُرح استخدام هذا التناظر كطريقة لتعريف تقسيم فضاء البحث في برمجة وراثية.^[13] تعتمد هذه الطريقة على فهرسة مجموعات الأنماط الجينية (وهي أشجار البرامج التي يُنتجها نظام البرمجة الوراثية) وفقًا لإثباتها المماثل في تناظر كوري–هوارد (والذي يُشار إليه هنا بـ «النوع» أو «النوع التطوري»).

كما أشار مدير الأبحاث في المعهد الفرنسي للأبحاث في علوم الحاسب الآلي والأتمتة برنار لانغ،^[14] فإن تناظر كوري–هوارد يشكّل حجة ضد قابلية براءات الاختراع في البرمجيات: بما أن الخوارزميات ما هي إلا إثباتات رياضية، فإن إتاحة تسجيل براءة اختراع على الخوارزميات يعني ضمنًا إتاحة تسجيل براءة اختراع على الإثباتات الرياضية. وهذا يعني أن النظرية قد تُصبح ملكية خاصة؛ وسيضطر الرياضي إلى الدفع لاستخدامها، والاعتماد على الشركة التي تبيعها دون الكشف عن الإثبات، بينما تُخلي مسؤوليتها عن أي أخطاء.

تعميمات

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

علاوة على ذلك، يمكن إظهار أن هذه الفئات تقابل الحدود الشعاعية،^[15] والتي تلعب دورًا محوريًا في نظرية الأوتار.

كما تُستكشف مجموعة موسّعة من التكافؤات ضمن تحاول، حيث تُوسّع نظرية النمط عبر مسلمة التوحيد ("التكافؤ يكافئ المساواة")، ما يتيح استخدام نظرية النمط المُمَثلة طوبولوجيًا كأساس شامل للرياضيات كلها (بما في ذلك نظرية المجموعات والمنطق الكلاسيكي، مع تقديم طرق جديدة لمناقشة بديهية الاختيار والعديد من المفاهيم الأخرى). وبذلك، فإن تناظر كوري–هوارد الذي يفيد بأن الإثباتات هي عناصر في أنواع مأهولة، يتوسع ليشمل مفهوم تحاول الإثباتات (بوصفها مسارات في الفضاء، إذ يتم تفسير نوع الهوية أو نوع المساواة في نظرية الأنواع كمسار).^[16]

المراجع

^ تم توضيح المراسلة لأول مرة في Howard 1980. انظر، على سبيل المثال، القسم 4.6، ص. 53 Gert Smolka and Jan Schwinghammer (2007-8), Lecture Notes in Semantics
^ تفسير بروير-هيتينغ-كولموغوروف يُسمى أيضًا "تفسير البرهان": ص. 161 من كتاب جوليت كينيدي، رومان كوساك، محرران. 2011. Set Theory, Arithmetic, and Foundations of Mathematics: Theorems, Philosophies (ردمك 978-1-107-00804-5) نسخة محفوظة 2025-02-23 على موقع واي باك مشين.
^ Casadio، Claudia؛ Scott، Philip J. (2021). Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics. Springer. ص. 184. ISBN:978-3-030-66545-6. مؤرشف من الأصل في 2024-01-17.
^ Coecke، Bob؛ Kissinger، Aleks (2017). Picturing Quantum Processes. Cambridge University Press. ص. 82. ISBN:978-1-107-10422-8. مؤرشف من الأصل في 2024-01-17.
^ "Computational trilogy". nLab. مؤرشف من الأصل في 2025-05-23. اطلع عليه بتاريخ 2023-10-29.
^ Curry 1934.
^ Curry & Feys 1958.
^ Howard 1980.
^ Moggi، Eugenio (1991)، "Notions of Computation and Monads" (PDF)، Information and Computation، ج. 93، ص. 55–92، DOI:10.1016/0890-5401(91)90052-4، مؤرشف من الأصل (PDF) في 2018-10-11
^ Sørenson، Morten؛ Urzyczyn، Paweł (1998)، Lectures on the Curry-Howard Isomorphism، CiteSeerX:10.1.1.17.7385
^ Goldblatt، "7.6 Grothendieck Topology as Intuitionistic Modality" (PDF)، Mathematical Modal Logic: A Model of its Evolution، ص. 76–81. المعامل "المرن" المشار إليه هو من Benton؛ Bierman؛ de Paiva (1998)، "Computational types from a logical perspective"، Journal of Functional Programming، ج. 8، ص. 177–193، CiteSeerX:10.1.1.258.6004، DOI:10.1017/s0956796898002998، S2CID:6149614
^ لامبك، جواكيم؛ سكوت، P. J. (1989). مقدمة إلى منطق الفئات الأعلى. كامبريدج نيويورك بورت شستر [إلخ]: دار نشر كامبريدج. ISBN:0521356539.
^ F. Binard and A. Felty, "Genetic programming with polymorphic types and higher-order functions." In Proceedings of the 10th annual conference on Genetic and evolutionary computation, pages 1187–1194, 2008. [1] نسخة محفوظة 2025-04-05 على موقع واي باك مشين.
^ "Article". bat8.inria.fr. مؤرشف من الأصل في 2013-11-17. اطلع عليه بتاريخ 2020-01-31.
^ John C. Baez and Mike Stay, "Physics, Topology, Logic and Computation: A Rosetta Stone", (2009) ArXiv 0903.0340 في New Structures for Physics، تحرير Bob Coecke، Lecture Notes in Physics، المجلد 813، Springer، برلين، 2011، الصفحات 95–174. نسخة محفوظة 2024-12-20 على موقع واي باك مشين.
^ Homotopy Type Theory: Univalent Foundations of Mathematics. (2013) برنامج الأسس الموحدة. معهد الدراسات المتقدمة. نسخة محفوظة 2025-06-01 على موقع واي باك مشين.

المراجع الأساسية

كوري، ه. ب. (20 سبتمبر 1934). "الوظائفية في المنطق التركيبي". وقائع الأكاديمية الوطنية للعلوم في الولايات المتحدة الأمريكية. ج. 20 ع. 11: 584–90. Bibcode:1934PNAS...20..584C. DOI:10.1073/pnas.20.11.584. ISSN:0027-8424. PMC:1076489. PMID:16577644. {{استشهاد بدورية محكمة}}: تجاهل المحلل الوسيط |وصول-doi= لأنه غير معروف (مساعدة)

كوري، هاسكل ب.؛ فايس، روبرت (1958). كريغ، ويليام (المحرر). المنطق التركيبي. دراسات في المنطق وأسس الرياضيات. شركة نورث-هولاند للنشر. ج. 1. LCCN:a59001593. {{استشهاد بكتاب}}: تجاهل المحلل الوسيط |لاحقة= لأنه غير معروف (مساعدة)

دي بروين، نيكولاس (1968)، أوتومات، لغة للرياضيات، قسم الرياضيات، جامعة آيندهوفن للتكنولوجيا، تقرير TH-68-WSK-05. أعيد نشره بصيغة منقحة، مع تعليق من صفحتين، في: الأتمتة والاستدلال، المجلد 2، أوراق كلاسيكية في المنطق الحسابي 1967–1970، سبرنغر فيرلاج، 1983، الصفحات 159–200.

هوارد، ويليام أ. (سبتمبر 1980)، "فكرة الصيغ-كأنواع في البناء"، في سيلدين، جوناثان ب.؛ هيندلي، ج. روجر (المحررون)، إلى ه. ب. كوري: مقالات حول المنطق التركيبي، حساب λ، والشكليات، أكاديميك برس، ص. 479–490، ISBN:978-0-12-349050-6 {{استشهاد}}: تجاهل المحلل الوسيط |رابط-الفصل= لأنه غير معروف (مساعدة)، تجاهل المحلل الوسيط |سنة-الأصل= لأنه غير معروف (مساعدة)، تجاهل المحلل الوسيط |محرر1-رابط= لأنه غير معروف (مساعدة)، وتجاهل المحلل الوسيط |محرر2-رابط= لأنه غير معروف (مساعدة).

امتدادات المراسلات

^ ^ا ^ب Pfenning، Frank؛ Davies، Rowan (2001)، "A Judgmental Reconstruction of Modal Logic" (PDF)، Mathematical Structures in Computer Science، ج. 11، ص. 511–540، CiteSeerX:10.1.1.43.1611، DOI:10.1017/S0960129501003322 (غير نشط 5 فبراير 2025)، S2CID:16467268، مؤرشف من الأصل (PDF) في 2025-05-26{{استشهاد}}: صيانة الاستشهاد: وصلة دوي غير نشطة منذ 2025 (link)
^ Davies، Rowan؛ Pfenning، Frank (2001)، "A Modal Analysis of Staged Computation" (PDF)، Journal of the ACM، ج. 48، ص. 555–604، CiteSeerX:10.1.1.3.5442، DOI:10.1145/382780.382785، S2CID:52148006، مؤرشف من الأصل (PDF) في 2025-03-13

غريفين، تيموثي جي. (1990)، "مفهوم الصيغ كأنواع للتحكم"، سجل المؤتمر السابع عشر للمؤتمر السنوي لجمعية الكمبيوتر الأمريكية في مبادئ لغات البرمجة، POPL '90، سان فرانسيسكو، كاليفورنيا، الولايات المتحدة الأمريكية، 17–19 يناير 1990، ص. 47–57، DOI:10.1145/96709.96714، ISBN:978-0-89791-343-0، S2CID:3005134.
باريجو، ميشيل (1992)، "حساب لامبدا-مي: تفسير خوارزمي لاستنتاج الطبيعة الكلاسيكية"، مؤتمر دولي عن البرمجة المنطقية والتبرير الآلي: LPAR '92 وقائع، سانت بطرسبرغ، روسيا، محاضرات في ملاحظات علوم الكمبيوتر، شبرينغر، ج. 624، ص. 190–201، ISBN:978-3-540-55727-2 {{استشهاد}}: تجاهل المحلل الوسيط |العنوان-الرابط= لأنه غير معروف (مساعدة).
هيربلين، هوغو (1995)، "هيكل لامبدا-حساب متساوي هيكل حساب الجمل في أسلوب جنتزن"، في باتشولسكي، ليزك؛ تيرين، جيرزي (المحررون)، منطق علوم الكمبيوتر، ورشة العمل الدولية الثامنة، CSL '94، كازيميرز، بولندا، 25–30 سبتمبر 1994، الأوراق المختارة، محاضرات في ملاحظات علوم الكمبيوتر، شبرينغر، ج. 933، ص. 61–75، ISBN:978-3-540-60017-6.
جاباي، دوف؛ دي كويروز، روي (1992). "توسيع تفسير كوري–هوارد لعلم المنطق الخطي، ذو الصلة ومنطق الموارد الأخرى". مجلة المنطق الرمزي. جمعية المنطق الرمزي. ج. 57. ص. 1319–1365. DOI:10.2307/2275370. JSTOR:2275370. S2CID:7159005. {{استشهاد بكتاب}}: تجاهل المحلل الوسيط |رابط2-المؤلف= لأنه غير معروف (مساعدة). (الإصدار الكامل من الورقة المعروضة في منطق كولوكويوم '90'، هلسنكي. الملخص في JSL 56(3):1139–1140، 1991.)
دي كويروز، روي؛ جاباي، دوف (1994)، "المساواة في الأنظمة الاستنتاجية المسمى وتفسير الوظائف للمساواة الاقتراحية"، في ديكر، بول؛ ستوخو، مارتن (المحررون)، وقائع الكولوكويوم التاسع في أمستردام، ILLC/قسم الفلسفة، جامعة أمستردام، ص. 547–565، ISBN:978-90-74795-07-4.
دي كويروز، روي؛ جاباي، دوف (1995)، "التفسير الوظيفي للكمية الوجودية"، نشرة مجموعة الاهتمام في المنطق البحت والتطبيقي، ج. 3، ص. 243–290 {{استشهاد}}: تجاهل المحلل الوسيط |رابط-الفصل= لأنه غير معروف (مساعدة). (الإصدار الكامل من ورقة قدمت في منطق كولوكويوم '91'، أوبسالا. الملخص في JSL 58(2):753–754، 1993.)
دي كويروز، روي؛ جاباي، دوف (1997)، "التفسير الوظيفي للحاجة النمطية"، في دي رايكي، ماارتن (المحرر)، التطورات في المنطق الحسي، سلسلة المنطق التطبيقي، شبرينغر، ج. 7، ص. 61–91، ISBN:978-0-7923-4711-8.
دي كويروز، روي؛ جاباي، دوف (1999)، "الاستدلال الطبيعي المسمى"، في أوهلباخ، هانس-يورجن؛ رايلي، أوي (المحررون)، المنطق، اللغة والاستدلال. مقالات تكريمية لدوف جاباي، اتجاهات في المنطق، كلوور، ج. 7، ص. 173–250، ISBN:978-0-7923-5687-5 {{استشهاد}}: تجاهل المحلل الوسيط |رابط-الفصل= لأنه غير معروف (مساعدة).
دي أوليفيرا، أنجولينا؛ دي كويروز، روي (1999)، "إجراء التطبيع لجزء المعادلات من الاستدلال الطبيعي المسمى"، مجلة المنطق لمجموعة الاهتمام في المنطق البحت والتطبيقي، دار نشر جامعة أكسفورد، ج. 7، ص. 173–215. (الإصدار الكامل من ورقة قدمت في 2nd WoLLIC'95، ريسيفي. الملخص في مجلة مجموعة الاهتمام في المنطق البحت والتطبيقي 4(2):330–332، 1996.)
بورنومو، إيمان؛ كروسلي، جون؛ ويرسينغ، مارتن (2005)، تكييف الإثباتات كبرامج: بروتوكول كوري-هوارد، أحجام في علوم الكمبيوتر، شبرينغر، ISBN:978-0-387-23759-6, يتعلق بتكييف الإثباتات كبرامج لتوليد البرامج للمشاكل ذات الحبيبات الكبيرة وبرمجة الأمثل المعتمدة على الأوامر، عبر طريقة يسميها المؤلفون بروتوكول كوري-هوارد. يتضمن مناقشة حول تناظر كوري-هوارد من منظور علوم الكمبيوتر.
دي كويروز، روي ج. جي. ب.؛ دي أوليفيرا، أنجولينا (2011)، التفسير الوظيفي للحسابات المباشرة، إلزيفير، ج. 269، ص. 19–40، DOI:10.1016/j.entcs.2011.03.003 {{استشهاد}}: تجاهل المحلل الوسيط |الدورية= لأنه غير معروف (مساعدة). (الإصدار الكامل من ورقة قدمت في LSFA 2010، ناتال، البرازيل.)

التفسيرات الفلسفية

دي كويروز، روي ج. جي. ب. (1994)، التطبيع وألعاب اللغة، ج. 48، ص. 83–123، DOI:10.1111/j.1746-8361.1994.tb00107.x، JSTOR:42968904 {{استشهاد}}: تجاهل المحلل الوسيط |الدورية= لأنه غير معروف (مساعدة). (الإصدار المبكر المعروض في منطق كولوكويوم '88'، بادوفا. الملخص في JSL 55:425، 1990.)
دي كويروز، روي ج. جي. ب. (2001)، "المعنى، الوظيفة، الهدف، الفائدة، العواقب – مفاهيم مترابطة"، مجلة المنطق لمجموعة الاهتمام في المنطق البحت والتطبيقي، ج. 9، ص. 693–734 {{استشهاد}}: تجاهل المحلل الوسيط |رابط-الفصل= لأنه غير معروف (مساعدة). (الإصدار المبكر المعروض في الندوة الدولية الرابعة عشرة حول فيتجنشتاين (الاحتفال بمرور المئة عام) التي أقيمت في كيرشبرغ/ويشيل، 13–20 أغسطس 1989.)
دي كويروز، روي ج. جي. ب. (2008)، حول قواعد الاختزال، المعنى كاستخدام، والمنطق النمطي البرهاني، ج. 90، ص. 211–247، DOI:10.1007/s11225-008-9150-5، S2CID:11321602 {{استشهاد}}: تجاهل المحلل الوسيط |الدورية= لأنه غير معروف (مساعدة).

الأوراق الاصطناعية

دي بروين، نيكولاس هوفرت (1995)، "عن أدوار الأنواع في الرياضيات"، في دي غروت، فيليب دي (المحرر)، De Groote 1995، صفحات 27–54 {{استشهاد}}: تجاهل المحلل الوسيط |رابط-الفصل= لأنه غير معروف (مساعدة), مساهمة دي بروين بنفسه.
خوفيرز، هيرمان (1995)، "حساب التركيبات والمنطق من الرتبة العليا"، De Groote 1995، صفحات 139–191, يحتوي على مقدمة تركيبية إلى تناظر كوري–هوارد.
غالييه، جان هـ. (1995)، "عن التناظر بين الإثباتات وتعبيرات لامبدا"، De Groote 1995، صفحات 55–138 {{استشهاد}}: |archive-date= requires |archive-url= (مساعدة)، تجاهل المحلل الوسيط |رابط-الأرشيف= لأنه غير معروف (مساعدة)، تجاهل المحلل الوسيط |رابط-الفصل= لأنه غير معروف (مساعدة)، وتجاهل المحلل الوسيط |رابط-المؤلف= لأنه غير معروف (مساعدة), يحتوي على مقدمة تركيبية إلى تناظر كوري–هوارد.
وادلر، فيليب (2014)، القضايا كأنواع (PDF)، ج. 58، ص. 75–84، DOI:10.1145/2699407، S2CID:11957500، مؤرشف من الأصل (PDF) في 2025-05-30 {{استشهاد}}: تجاهل المحلل الوسيط |الدورية= لأنه غير معروف (مساعدة) وتجاهل المحلل الوسيط |رابط-المؤلف= لأنه غير معروف (مساعدة)

كتب

دي غروت، فيليب، المحرر (1995)، تناظر كوري–هوارد، دفاتر مركز المنطق (جامعة لوفان الكاثوليكية)، أكاديميا-برويولان، ج. 8، ISBN:978-2-87209-363-2, يُعيد نشر الأوراق الرائدة لكوري-فايس وهوارد، وورقة لـ دي بروين وعدد قليل من الأوراق الأخرى.
سورنسن، مورتن هاينه؛ أورزيزين، بافل (2006)، محاضرات عن تناظر كوري–هوارد، دراسات في المنطق وأسس الرياضيات، إلزيفير، ج. 149، CiteSeerX:10.1.1.17.7385، ISBN:978-0-444-52077-7 {{استشهاد}}: تجاهل المحلل الوسيط |سنة-الأصل= لأنه غير معروف (مساعدة), ملاحظات في نظرية الإثبات ونظرية الأنواع، تتضمن عرضًا لتناظر كوري–هوارد، مع تركيز على تناظر الصيغ-كأنواع.
جيرار، جان-إيف (1987–1990)، الإثباتات والأنواع، رسائل كامبريدج في علوم الحاسوب النظرية، مطبعة جامعة كامبريدج، ج. 7، ISBN:0-521-37181-3، مؤرشف من الأصل في 2008-04-18 {{استشهاد}}: تجاهل المحلل الوسيط |الآخرون= لأنه غير معروف (مساعدة), ملاحظات في نظرية الإثبات مع عرض لتناظر كوري–هوارد.
تومبسون، سيمون (1991)، نظرية الأنواع والبرمجة الدالية، أديسون-ويسلي، ISBN:0-201-41667-0، مؤرشف من الأصل في 2025-05-15.
بورنومو، إيمان؛ كروسلي، جون؛ ويرزينغ، مارتن (2005)، تكييف الإثباتات-كبرامج: بروتوكول كوري–هوارد، دراسات أحادية في علوم الحاسوب، شبرينغر، ISBN:978-0-387-23759-6, يتناول تكييف برنامج توليد البرامج من الإثباتات لحل مشكلات تطوير البرامج التقريرية والبرمجة الموجّهة بالأوامر، عبر طريقة يسميها المؤلفون "بروتوكول كوري–هوارد". يتضمن مناقشة لتناظر كوري–هوارد من منظور علوم الحاسوب.
بينار، ف.؛ فيلتي، أ. (2008)، "البرمجة الوراثية بأنواع متعددة الأشكال ودوال من الدرجة العليا"، وقائع المؤتمر السنوي العاشر حول البرمجة الوراثية والتطور الحسابي، رابطة آلات الحوسبة، ص. 1187–94، DOI:10.1145/1389095.1389330، ISBN:9781605581309، S2CID:3669630 {{استشهاد}}: تجاهل المحلل الوسيط |رابط-الفصل= لأنه غير معروف (مساعدة)
دي كيروز، روي ج. ج. ب.؛ دي أوليفيرا، أنجولينا ج.؛ جاباي، دوف م. (2011)، التفسير الوظيفي للاستنتاج المنطقي، تطورات في المنطق، إمبيريال كولدج برس / وورلد ساينتفك، ج. 5، ISBN:978-981-4360-95-1، مؤرشف من الأصل في 2023-10-13.

قراءة إضافية

Johnstone، P.T. (2002)، "D4.2 λ-Calculus and cartesian closed categories"، Sketches of an Elephant، A Topos Theory Compendium، Clarendon Press، ج. 2، ص. 951–962، ISBN:978-0-19-851598-2، مؤرشف من الأصل في 2023-10-13 — gives a categorical view of "what happens" in the Curry–Howard correspondence.

وصلات خارجية

[1] تم توضيح المراسلة لأول مرة في Howard 1980. انظر، على سبيل المثال، القسم 4.6، ص. 53 Gert Smolka and Jan Schwinghammer (2007-8), Lecture Notes in Semantics

[2] تفسير بروير-هيتينغ-كولموغوروف يُسمى أيضًا "تفسير البرهان": ص. 161 من كتاب جوليت كينيدي، رومان كوساك، محرران. 2011. Set Theory, Arithmetic, and Foundations of Mathematics: Theorems, Philosophies (ردمك 978-1-107-00804-5) نسخة محفوظة 2025-02-23 على موقع واي باك مشين.

[3] Casadio، Claudia؛ Scott، Philip J. (2021). Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics. Springer. ص. 184. ISBN:978-3-030-66545-6. مؤرشف من الأصل في 2024-01-17.

[Coecke_Kissinger_2017_p._82-4] Coecke، Bob؛ Kissinger، Aleks (2017). Picturing Quantum Processes. Cambridge University Press. ص. 82. ISBN:978-1-107-10422-8. مؤرشف من الأصل في 2024-01-17.

[5] "Computational trilogy". nLab. مؤرشف من الأصل في 2025-05-23. اطلع عليه بتاريخ 2023-10-29.

[FOOTNOTECurry1934-6] Curry 1934.

[FOOTNOTECurryFeys1958-7] Curry & Feys 1958.

[FOOTNOTEHoward1980-8] Howard 1980.

[9] Moggi، Eugenio (1991)، "Notions of Computation and Monads" (PDF)، Information and Computation، ج. 93، ص. 55–92، DOI:10.1016/0890-5401(91)90052-4، مؤرشف من الأصل (PDF) في 2018-10-11

[12] Sørenson، Morten؛ Urzyczyn، Paweł (1998)، Lectures on the Curry-Howard Isomorphism، CiteSeerX:10.1.1.17.7385

[13] Goldblatt، "7.6 Grothendieck Topology as Intuitionistic Modality" (PDF)، Mathematical Modal Logic: A Model of its Evolution، ص. 76–81. المعامل "المرن" المشار إليه هو من Benton؛ Bierman؛ de Paiva (1998)، "Computational types from a logical perspective"، Journal of Functional Programming، ج. 8، ص. 177–193، CiteSeerX:10.1.1.258.6004، DOI:10.1017/s0956796898002998، S2CID:6149614

[14] لامبك، جواكيم؛ سكوت، P. J. (1989). مقدمة إلى منطق الفئات الأعلى. كامبريدج نيويورك بورت شستر [إلخ]: دار نشر كامبريدج. ISBN:0521356539.

[15] F. Binard and A. Felty, "Genetic programming with polymorphic types and higher-order functions." In Proceedings of the 10th annual conference on Genetic and evolutionary computation, pages 1187–1194, 2008. [1] نسخة محفوظة 2025-04-05 على موقع واي باك مشين.

[16] "Article". bat8.inria.fr. مؤرشف من الأصل في 2013-11-17. اطلع عليه بتاريخ 2020-01-31.

[17] John C. Baez and Mike Stay, "Physics, Topology, Logic and Computation: A Rosetta Stone", (2009) ArXiv 0903.0340 في New Structures for Physics، تحرير Bob Coecke، Lecture Notes in Physics، المجلد 813، Springer، برلين، 2011، الصفحات 95–174. نسخة محفوظة 2024-12-20 على موقع واي باك مشين.

[18] Homotopy Type Theory: Univalent Foundations of Mathematics. (2013) برنامج الأسس الموحدة. معهد الدراسات المتقدمة. نسخة محفوظة 2025-06-01 على موقع واي باك مشين.

[PfenningDaviesJudgmental-10] ا ^ب Pfenning، Frank؛ Davies، Rowan (2001)، "A Judgmental Reconstruction of Modal Logic" (PDF)، Mathematical Structures in Computer Science، ج. 11، ص. 511–540، CiteSeerX:10.1.1.43.1611، DOI:10.1017/S0960129501003322 (غير نشط 5 فبراير 2025)، S2CID:16467268، مؤرشف من الأصل (PDF) في 2025-05-26{{استشهاد}}: صيانة الاستشهاد: وصلة دوي غير نشطة منذ 2025 (link)

[DaviesPfenningStaged-11] Davies، Rowan؛ Pfenning، Frank (2001)، "A Modal Analysis of Staged Computation" (PDF)، Journal of the ACM، ج. 48، ص. 555–604، CiteSeerX:10.1.1.3.5442، DOI:10.1145/382780.382785، S2CID:52148006، مؤرشف من الأصل (PDF) في 2025-03-13

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[ext 1]

[ext 2]

[10]

[11]

[12]

[13]

[14]

[15]

[16]