تناظر کوری-هاوارد چیست؟
نویسندگان
1 دانشگاه ارومیه
doi
10.22034/csj.2024.192416چکیده
تناظر کوری- هاوارد نتیجهایست در حوزه منطق و علوم کامپیوتر که ارتباط عمیقی میان برهانها و برنامههای کامپیوتری برقرار میکند. در این نوشتارِ ترویجی، ایدههای کلیدی پشت این تناظر، پیامدهای آن برای هر دو حوزة منطق و علوم کامپیوتر، و تأثیر آن بر توسعه زبانهای برنامهنویسی(تابعی) و اثباتیارها بررسی میشود. تناظر کوری- هاوارد، در سادهترین شکلش، یک تناظر میان نوعها و ترمها از حساب لامبدای نوعدار (سادهترین زبان برنامهنویسی تابعی) و فرمولها و برهانها در دستگاه استنتاج طبیعی منطق شهودی گزارهای برقرار میکند. این تناظر نه تنها یک نتیجه مهم در نظریه برهان است؛ بلکه زیربنایی برای گسترش و توسعة دستگاههای نوعدار برای زبانهای برنامهنویسی تابعی است. این نوشتار این تناظر را به گونهای معرفی میکند که درک آن برای افراد غیرمتخصص (با دانش پایه در مبانی منطق) ممکن باشد.
