پیوند عمیق معادل اثبات ریاضی و برنامه های کامپیوتری | مجله کوانتا

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

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

به بیان ساده، مکاتبات Curry-Howard بیان می کند که دو مفهوم از علوم کامپیوتر (انواع و برنامه ها) به ترتیب معادل گزاره ها و برهان ها هستند - مفاهیمی از منطق.

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

این مکاتبات به نام دو محققی است که به طور مستقل آن را کشف کردند. در سال 1934، هاسکل کوری، ریاضی‌دان و منطق‌دان، متوجه شباهت بین توابع در ریاضیات و رابطه ضمنی در منطق شد، که به شکل گزاره‌های «اگر-آنگاه» بین دو گزاره است.

با الهام از مشاهدات کری، منطق‌دان ریاضی ویلیام آلوین هاوارد در سال 1969 پیوند عمیق‌تری بین محاسبات و منطق کشف کرد و نشان داد که اجرای یک برنامه کامپیوتری بسیار شبیه ساده‌سازی یک اثبات منطقی است. هنگامی که یک برنامه کامپیوتری اجرا می شود، هر خط برای به دست آوردن یک خروجی "ارزیابی" می شود. به طور مشابه، در یک اثبات، شما با جملات پیچیده‌ای شروع می‌کنید که می‌توانید آن‌ها را ساده کنید (مثلاً با حذف مراحل اضافی یا جایگزینی عبارات پیچیده با عبارات ساده‌تر) تا زمانی که به نتیجه برسید - یک گزاره فشرده‌تر و موجزتر که از بسیاری از گزاره‌های میانی مشتق شده است. .

در حالی که این توصیف یک مفهوم کلی از متناظر را بیان می کند، برای درک کامل آن، باید کمی بیشتر در مورد آنچه دانشمندان کامپیوتر "نظریه نوع" می نامند، بیاموزیم.

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

راسل نشان داد برای جلوگیری از این پارادوکس، می‌توانیم از «انواع» استفاده کنیم. به طور کلی، اینها مقوله هایی هستند که مقادیر خاص آنها را اشیا می نامند. به عنوان مثال، اگر نوعی به نام "Nat" به معنای اعداد طبیعی وجود داشته باشد، اشیاء آن 1، 2، 3 و غیره هستند. محققان معمولا از دو نقطه برای نشان دادن نوع یک شی استفاده می کنند. عدد 7 از نوع عدد صحیح را می توان به صورت "7: Integer" نوشت. شما می توانید تابعی داشته باشید که یک شی از نوع A را می گیرد و یک شی از نوع B را بیرون می اندازد، یا تابعی که یک جفت از اشیاء نوع A و نوع B را در یک نوع جدید به نام "A × B" ترکیب می کند.

بنابراین، یکی از راه‌های حل پارادوکس، قرار دادن این انواع در یک سلسله مراتب است، بنابراین آنها فقط می‌توانند حاوی عناصری از «سطح پایین‌تر» از خودشان باشند. سپس یک نوع نمی تواند خود را مهار کند، که از خودارجاعی که پارادوکس را ایجاد می کند اجتناب می کند.

در دنیای تئوری نوع، اثبات درست بودن یک جمله می تواند متفاوت از آنچه ما به آن عادت کرده ایم به نظر برسد. اگر بخواهیم ثابت کنیم که عدد صحیح 8 زوج است، باید نشان دهیم که 8 در واقع یک شی از نوع خاصی به نام زوج است، که در آن قانون عضویت بر 2 بخش پذیر است. پس از تأیید اینکه 8 قابل تقسیم است. با 2، می توانیم نتیجه بگیریم که 8 در واقع یک "ساکن" از نوع Even است.

کری و هوارد نشان دادند که انواع اساساً معادل گزاره های منطقی هستند. هنگامی که یک تابع در یک نوع "ساکن" می شود - یعنی وقتی می توانید با موفقیت یک تابع را تعریف کنید که یک شی از آن نوع است - به طور موثر نشان می دهید که گزاره مربوطه درست است. بنابراین توابعی که یک ورودی از نوع A می گیرند و یک خروجی از نوع B می دهند که با نوع A → B مشخص می شود، باید با یک مفهوم مطابقت داشته باشند: "اگر A، پس B." به عنوان مثال، گزاره "اگر باران می بارد، پس زمین خیس است" را در نظر بگیرید. در تئوری نوع، این گزاره با تابعی با نوع «باران → زمین خیس» مدل‌سازی می‌شود. فرمول‌های ظاهری متفاوت در واقع از نظر ریاضی یکسان هستند.

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

و برای ریاضیات، مکاتبات منجر به تولد شده است دستیاران اثبات، که اثبات کننده قضیه تعاملی نیز نامیده می شود. اینها ابزارهای نرم افزاری هستند که به ساختن اثبات های رسمی کمک می کنند، مانند Coq و Lean. در Coq، هر مرحله از اثبات اساساً یک برنامه است و اعتبار اثبات با الگوریتم‌های بررسی نوع بررسی می‌شود. ریاضیدانان همچنین از دستیارهای اثبات استفاده می کنند - به ویژه، اثبات قضیه ناب - رسمی کردن ریاضیات، که شامل نمایش مفاهیم، ​​قضایا و براهین ریاضی در قالبی دقیق و قابل تأیید توسط رایانه است. این اجازه می دهد تا زبان گاهی اوقات غیررسمی ریاضیات توسط رایانه بررسی شود.

محققان هنوز در حال بررسی عواقب این پیوند بین ریاضی و برنامه نویسی هستند. مکاتبات اصلی Curry-Howard برنامه‌نویسی را با نوعی منطق به نام منطق شهودی ترکیب می‌کند، اما معلوم می‌شود که انواع بیشتری از منطق نیز می‌توانند متمایل به چنین وحدت‌هایی باشند.

"آنچه در یک قرن از زمان بینش کری رخ داده است این است که ما به کشف موارد بیشتر و بیشتری ادامه می دهیم که "سیستم منطقی X با سیستم محاسباتی Y مطابقت دارد." مایکل کلارکسون، دانشمند کامپیوتر در دانشگاه کرنل. محققان قبلاً برنامه نویسی را به انواع دیگر منطق مانند منطق خطی که شامل مفهوم "منابع" و منطق مدال است که با مفاهیم امکان و ضرورت سر و کار دارد، مرتبط کرده اند.

و در حالی که این مکاتبات نام های کری و هاوارد را دارد، آنها به هیچ وجه تنها کسانی نیستند که آن را کشف کرده اند. این امر ماهیت بنیادی مکاتبات را تأیید می کند: مردم بارها و بارها متوجه آن می شوند. کلارکسون گفت: "به نظر می رسد تصادفی نیست که یک پیوند عمیق بین محاسبات و منطق وجود دارد."