تناظر كوري - هاوارد چيست؟

تناظر كوري- هاوارد نتيجه ‌ايست در حوزه منطق و علوم كامپيوتر كه ارتباط عميقي ميان برهان‌ها و برنامه‌هاي كامپيوتري برقرار مي‌كند. در اين نوشتارِ ترويجي، ايده‌هاي كليدي پشت اين تناظر، پيامدهاي آن براي هر دو حوزه منطق و علوم كامپيوتر، و تأثير آن بر توسعه‌ زبان‌هاي برنامه‌نويسي(تابعي) و اثبات‌يارها بررسي مي‌شود. تناظر كوري- هاوارد، در ساده‌ترين شكلش، يك تناظر ميان نوع‌ها و ترم‌ها از حساب لامبداي نوع‌دار (ساده‌ترين زبان برنامه‌نويسي تابعي) و فرمول‌ها و برهان‌ها در دستگاه استنتاج طبيعي منطق شهودي گزاره‌اي برقرار مي‌كند. اين تناظر نه تنها يك نتيجه مهم در نظريه برهان است؛ بلكه زيربنايي براي گسترش و توسعة دستگاه‌هاي نوع‌دار براي زبان‌هاي برنامه‌نويسي تابعي است. اين نوشتار اين تناظر را به گونه‌اي معرفي مي‌كند كه درك آن براي افراد غيرمتخصص (با دانش پايه در مباني منطق) ممكن باشد.