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

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

هي تعميم للتمثيل الصرفي للتمثيل بين أنظمة المنطق الرسمي وحسابات الحوسبة التي اكتشفها لأول مرة عالم الرياضيات الأمريكي هاسكل كاري والمنطقي ويليام آلفين هوارد. هي الرابط بين المنطق والحوسبة الذي يُنسب عادة إلى كاري وهوارد، على الرغم من أن الفكرة تتعلق بالتفسير التشغيلي للمنطق الحسي الذي قدمه لويتسن براور،  وأندريه كولموغوروف وستيفن كول كلين (انظر ). تم توسيع العلاقة لتشمل نظرية الفئات كـ**مراسلة كاري-هوارد-لامبك**.

## الأصل والنطاق والنتائج
تبدأ **مراسلة كاري-هوارد** من عدة ملاحظات:
# في عام 1934، لاحظ هاسكل كاري أن أنواع المجمّعين يمكن أن تُرى كمخطط-مفردات لمنطق الاستدلال التضميني.
# في عام 1958، لاحظ أن نوعًا معينًا من أنظمة البرهان، والذي يُشار إليه بنظام الاستدلال بأسلوب هيلبرت، يتزامن مع جزء من نموذج حوسبة معروف باسم منطق تجميعي.
# في عام 1969، لاحظ ويليام آلفين هوارد أن نوعًا آخر من أنظمة البرهان، والذي يُشار إليه بالاستدلال الطبيعي، يمكن تفسيره بشكل مباشر في نسخته منطق الاستدلال كنوع مطبوع من نموذج حوسبة يعرف بتكامل لامدا.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

يمكن أيضاً نقل النتائج المتعلقة بكمال بعض مجموعات المنظمات أو المسلمات. على سبيل المثال، حقيقة أن المنظم **X** يشكل  للمنطق التركيبي (الامتدادي) تعني أن مخطط المسلمة الوحيد
: (((*α* → (*β* → *γ*)) → ((*α* → *β*) → (*α* → *γ*))) → ((*δ* → (*ε* → *δ*)) → *ζ*)) → *ζ*,
الذي هو النوع الرئيسي لـ **X**, هو استبدال مناسب للمزيج من مخططات المسلمات
: *α* → (*β* → *α*) و
: (*α* → (*β* → *γ*)) → ((*α* → *β*) → (*α* → *γ*)).

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

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

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

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

* نظام F لجيرارد-رينولد كلغة مشتركة لكل من منطق المقترحات من الدرجة الثانية وتكامل لامدا الموصوف بالأنواع البوليموريك.
* المنطق من الدرجة الأعلى ونظام Fω لجيرارد.
* الأنواع الاستقرائية كالنوع البياني الجبري.
* الضرورة \Box في منطق موجهات وحساب المراحل
* الإمكانية \Diamond في منطق موجهات وأنواع الموناد للتأثيرات
* حساب  (حيث يُقتصر التجريد على *λx*.*E* حيث *x* يحتوي على ظهور واحد على الأقل في *E*) و**CL**I تتوافق مع المنطق ذي الصلة.
* الحقيقة المحلية (∇) في طوبولوجيا غروثنديك أو المعامل المكافئ "المرن" (◯) لـ بينتون، بييرمان، ودي بايفا (1998) تتوافق مع منطق CL الذي يصف "أنواع الحساب".

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

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

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

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

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

### دور دي بروين

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

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

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

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

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

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

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

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

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

الأشياء (المقترحات/الأنواع) تشمل:
* \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

الآن، يوجد  بحيث \alpha_1 \times \ldots \times \alpha_n \vdash t : \beta إذا وفقط إذا كانت \alpha_1, \ldots, \alpha_n \vdash \beta  قابلة للإثبات في المنطق الحدسي الاستنباطي.

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

### المركّب الهوية باعتباره إثباتًا لـ ''α'' → ''α'' في منطق هيلبرت
كمثال، فلننظر إلى إثبات النظرية . في حساب لامدا، هذا هو نوع دالة الهوية ، وفي المنطق التركيبي يتم الحصول على دالة الهوية بتطبيق **S** = *λfgx*.*fx*(*gx*) مرتين على **K** = *λxy*.*x*. أي أن . كتوصيف للإثبات، فإن هذا يعني أن الخطوات التالية يمكن استخدامها لإثبات :

* تطبيق المخطط الثاني للبديهية باستخدام الصيغ ،  و للحصول على إثبات لـ:
  ,
* تطبيق المخطط الأول للبديهية مرة واحدة باستخدام  و للحصول على إثبات لـ:
  ,
* تطبيق المخطط الأول للبديهية مرة ثانية باستخدام  و للحصول على إثبات لـ:
  ,
* تطبيق قاعدة القياس (Modus Ponens) مرتين للحصول على إثبات لـ:
  

بشكل عام، الإجراء هو أنه كلما احتوى البرنامج على تطبيق من الشكل (*P* *Q*), يجب اتباع الخطوات التالية:
# أولاً، إثبات النظريات المقابلة لأنواع *P* و*Q*.
# بما أن *P* يتم تطبيقه على *Q*، يجب أن يكون نوع *P* من الشكل  ونوع *Q* من الشكل  لبعض  و. وبالتالي، يمكن فصل النتيجة  باستخدام قاعدة القياس.

### مركّب التركيب باعتباره إثباتًا لـ (''β'' → ''α'') → (''γ'' → ''β'') → ''γ'' → ''α'' في منطق هيلبرت
كمثال أكثر تعقيدًا، دعنا ننظر إلى النظرية التي تقابل الدالة **B**. نوع **B** هو:
.
**B** تعادل: (**S** (**K** **S**) **K**). هذا هو مخططنا لإثبات النظرية:
.

الخطوة الأولى هي بناء (**K** **S**). لجعل مقدم بديهية **K** يبدو كأنه بديهية **S**، نضبط  ليكون
،
و ليكون  (لتفادي تعارض المتغيرات):

:
:

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

:

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

:,

نضع , , و، لينتج:

:

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

:

هذه هي الصيغة المقابلة لنوع (**S** (**K** **S**)). حالة خاصة من هذه النظرية تكون عندما :

:

### الإثبات العادي لـ (''β'' → ''α'') → (''γ'' → ''β'') → ''γ'' → ''α'' في الاستنتاج الطبيعي كما يُرى كـ ''λ''-تعبير
يعرض المخطط أدناه إثباتًا للصيغة  في نظام الاستنتاج الطبيعي، ويوضح كيف يمكن تفسير هذا الإثبات باعتباره تعبير لامبدا  من النوع .

                                      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) : (β → α) → (γ → β) → γ → α

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

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

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

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

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

## المراجع

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

* 

* 

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

* . 

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

refs= 
* .
* .
* .
* . (الإصدار الكامل من الورقة المعروضة في *منطق كولوكويوم '90'، هلسنكي. الملخص في *JSL* 56(3):1139–1140، 1991.)
* .
* . (الإصدار الكامل من ورقة قدمت في *منطق كولوكويوم '91'، أوبسالا. الملخص في *JSL* 58(2):753–754، 1993.)
* .
* .
* . (الإصدار الكامل من ورقة قدمت في *2nd WoLLIC'95*، ريسيفي. الملخص في *مجلة مجموعة الاهتمام في المنطق البحت والتطبيقي* 4(2):330–332، 1996.)
* , يتعلق بتكييف الإثباتات كبرامج لتوليد البرامج للمشاكل ذات الحبيبات الكبيرة وبرمجة الأمثل المعتمدة على الأوامر، عبر طريقة يسميها المؤلفون بروتوكول كوري-هوارد. يتضمن مناقشة حول تناظر كوري-هوارد من منظور علوم الكمبيوتر.
* . (الإصدار الكامل من ورقة قدمت في *LSFA 2010*، ناتال، البرازيل.)

### التفسيرات الفلسفية
* . (الإصدار المبكر المعروض في *منطق كولوكويوم '88'، بادوفا. الملخص في *JSL* 55:425، 1990.)
* . (الإصدار المبكر المعروض في *الندوة الدولية الرابعة عشرة حول فيتجنشتاين (الاحتفال بمرور المئة عام)'' التي أقيمت في كيرشبرغ/ويشيل، 13–20 أغسطس 1989.)
* .

### الأوراق الاصطناعية
* , مساهمة دي بروين بنفسه.
* , يحتوي على مقدمة تركيبية إلى تناظر كوري–هوارد.
* , يحتوي على مقدمة تركيبية إلى تناظر كوري–هوارد.
* 

### كتب
* , يُعيد نشر الأوراق الرائدة لكوري-فايس وهوارد، وورقة لـ دي بروين وعدد قليل من الأوراق الأخرى.
* , ملاحظات في نظرية الإثبات ونظرية الأنواع، تتضمن عرضًا لتناظر كوري–هوارد، مع تركيز على تناظر الصيغ-كأنواع.
* , ملاحظات في نظرية الإثبات مع عرض لتناظر كوري–هوارد.
* .
* , يتناول تكييف برنامج توليد البرامج من الإثباتات لحل مشكلات تطوير البرامج التقريرية والبرمجة الموجّهة بالأوامر، عبر طريقة يسميها المؤلفون "بروتوكول كوري–هوارد". يتضمن مناقشة لتناظر كوري–هوارد من منظور علوم الحاسوب.
* 
* .

## قراءة إضافية
*  — gives a categorical view of "what happens" in the Curry–Howard correspondence.

## وصلات خارجية
* هوارد عن كوري-هوارد
* تطابق كوري-هوارد في هاسكل
* ذا مونايد ريدر 6: مغامرات في أرض الكلاسيك: كوري-هوارد في هاسكل، قانون بيرس

تصنيف:علم الحاسوب في 1958
تصنيف:علم الحاسوب في 1969
تصنيف:نظرية البرهان
تصنيف:منطق في علم الحاسوب
تصنيف:نظرية النمط
تصنيف:فلسفة علم الحاسوب