تناظر کوری - هاوارد چیست؟
|
|
|
|
|
|
|
|
نویسنده
|
علی زاده مجید
|
|
منبع
|
علوم رايانشي - 1402 - دوره : 8 - شماره : 4 - صفحه:78 -86
|
|
چکیده
|
تناظر کوری- هاوارد نتیجه ایست در حوزه منطق و علوم کامپیوتر که ارتباط عمیقی میان برهان‌ها و برنامه‌های کامپیوتری برقرار می‌کند. در این نوشتارِ ترویجی، ایده‌های کلیدی پشت این تناظر، پیامدهای آن برای هر دو حوزه منطق و علوم کامپیوتر، و تاثیر آن بر توسعه زبان‌های برنامه‌نویسی(تابعی) و اثبات‌یارها بررسی می‌شود. تناظر کوری- هاوارد، در ساده‌ترین شکلش، یک تناظر میان نوع‌ها و ترم‌ها از حساب لامبدای نوع‌دار (ساده‌ترین زبان برنامه‌نویسی تابعی) و فرمول‌ها و برهان‌ها در دستگاه استنتاج طبیعی منطق شهودی گزاره‌ای برقرار می‌کند. این تناظر نه تنها یک نتیجه مهم در نظریه برهان است؛ بلکه زیربنایی برای گسترش و توسعة دستگاه‌های نوع‌دار برای زبان‌های برنامه‌نویسی تابعی است. این نوشتار این تناظر را به گونه‌ای معرفی می‌کند که درک آن برای افراد غیرمتخصص (با دانش پایه در مبانی منطق) ممکن باشد.
|
|
کلیدواژه
|
تناظر کوری - هاروارد، منطق، زبان های برنامه‌نویسی تابعی
|
|
آدرس
|
دانشگاه تهران، دانشکدگان علوم, دانشکده ریاضی، آمار و علوم کامپیوتر, گروه علوم کامپیوتر, ایران
|
|
پست الکترونیکی
|
majidalizadeh@ut.ac.ir
|
|
|
|
|
|
|