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