تناظر کوری-هاوارد چیست؟
تناظر کوری- هاوارد نتیجه ایست در حوزه منطق و علوم کامپیوتر که ارتباط عمیقی میان برهان ها و برنامه های کامپیوتری برقرار می کند. در این نوشتار ترویجی، ایده های کلیدی پشت این تناظر، پیامدهای آن برای هر دو حوزه منطق و علوم کامپیوتر، و تاثیر آن بر توسعه زبان های برنامه نویسی (تابعی) و اثبات یارها بررسی می شود. تناظر کوری- هاوارد، در ساده ترین شکلش، یک تناظر میان نوع ها و ترم ها از حساب لامبدای نوع دار (ساده ترین زبان برنامه نویسی تابعی) و فرمول ها و برهان ها در دستگاه استنتاج طبیعی منطق شهودی گزاره ای برقرار می کند. این تناظر نه تنها یک نتیجه مهم در نظریه برهان است؛ بلکه زیربنایی برای گسترش و توسعه دستگاه های نوع دار برای زبان های برنامه نویسی تابعی است. این نوشتار این تناظر را به گونه ای معرفی می کند که درک آن برای افراد غیرمتخصص (با دانش پایه در مبانی منطق) ممکن باشد.
- حق عضویت دریافتی صرف حمایت از نشریات عضو و نگهداری، تکمیل و توسعه مگیران میشود.
- پرداخت حق اشتراک و دانلود مقالات اجازه بازنشر آن در سایر رسانههای چاپی و دیجیتال را به کاربر نمیدهد.