تناظر کوری-هاوارد چیست؟
Publish place: Computing Science Journal، Vol: 8، Issue: 4
Publish Year: 1402
نوع سند: مقاله ژورنالی
زبان: Persian
View: 30
This Paper With 9 Page And PDF Format Ready To Download
- Certificate
- من نویسنده این مقاله هستم
استخراج به نرم افزارهای پژوهشی:
شناسه ملی سند علمی:
JR_CSJI-8-4_006
تاریخ نمایه سازی: 28 اسفند 1402
Abstract:
تناظر کوری- هاوارد نتیجه ایست در حوزه منطق و علوم کامپیوتر که ارتباط عمیقی میان برهان ها و برنامه های کامپیوتری برقرار می کند. در این نوشتار ترویجی، ایده های کلیدی پشت این تناظر، پیامدهای آن برای هر دو حوزه منطق و علوم کامپیوتر، و تاثیر آن بر توسعه زبان های برنامه نویسی(تابعی) و اثبات یارها بررسی می شود. تناظر کوری- هاوارد، در ساده ترین شکلش، یک تناظر میان نوع ها و ترم ها از حساب لامبدای نوع دار (ساده ترین زبان برنامه نویسی تابعی) و فرمول ها و برهان ها در دستگاه استنتاج طبیعی منطق شهودی گزاره ای برقرار می کند. این تناظر نه تنها یک نتیجه مهم در نظریه برهان است؛ بلکه زیربنایی برای گسترش و توسعه دستگاه های نوع دار برای زبان های برنامه نویسی تابعی است. این نوشتار این تناظر را به گونه ای معرفی می کند که درک آن برای افراد غیرمتخصص (با دانش پایه در مبانی منطق) ممکن باشد.
Keywords:
Authors
مجید علیزاده
دانشیار دانشکدگان علوم دانشکده ریاضی، آمار و علوم کامپیوتر- گروه علوم کامپیوتر- دانشگاه تهران- تهران- ایران
مراجع و منابع این Paper:
لیست زیر مراجع و منابع استفاده شده در این Paper را نمایش می دهد. این مراجع به صورت کاملا ماشینی و بر اساس هوش مصنوعی استخراج شده اند و لذا ممکن است دارای اشکالاتی باشند که به مرور زمان دقت استخراج این محتوا افزایش می یابد. مراجعی که مقالات مربوط به آنها در سیویلیکا نمایه شده و پیدا شده اند، به خود Paper لینک شده اند :