গণিত প্রমাণ এবং কম্পিউটার প্রোগ্রাম সমতুল্য গভীর লিঙ্ক | কোয়ান্টা ম্যাগাজিন

কিছু বৈজ্ঞানিক আবিষ্কার গুরুত্বপূর্ণ কারণ তারা নতুন কিছু প্রকাশ করে — ডিএনএর ডাবল হেলিকাল গঠন, উদাহরণস্বরূপ, বা ব্ল্যাক হোলের অস্তিত্ব। যাইহোক, কিছু উদ্ঘাটন গভীর কারণ তারা দেখায় যে দুটি পুরানো ধারণা, যা একবার আলাদা বলে মনে করা হয়েছিল, বাস্তবে একই। জেমস ক্লার্ক ম্যাক্সওয়েলের সমীকরণগুলি ধরুন যা দেখায় যে বিদ্যুৎ এবং চুম্বকত্ব একটি একক ঘটনার দুটি দিক, বা সাধারণ আপেক্ষিকতা একটি বাঁকা স্থান-কালের সাথে মহাকর্ষের সংযোগ।

কারি-হাওয়ার্ডের চিঠিপত্র একই কাজ করে কিন্তু একটি বৃহত্তর স্কেলে, শুধুমাত্র একটি ক্ষেত্রের মধ্যে পৃথক ধারণাগুলি নয়, বরং সমগ্র শৃঙ্খলাগুলিকে সংযুক্ত করে: কম্পিউটার বিজ্ঞান এবং গাণিতিক যুক্তি. কারি-হাওয়ার্ড আইসোমরফিজম নামেও পরিচিত (একটি শব্দ যার অর্থ দুটি জিনিসের মধ্যে এক-এক রকমের চিঠিপত্র বিদ্যমান), এটি গাণিতিক প্রমাণ এবং কম্পিউটার প্রোগ্রামের মধ্যে একটি সংযোগ স্থাপন করে।

সহজভাবে বলা যায়, কারি-হাওয়ার্ডের চিঠিপত্রে ধারণা করা হয়েছে যে কম্পিউটার বিজ্ঞানের দুটি ধারণা (প্রকার এবং প্রোগ্রাম) যথাক্রমে প্রস্তাবনা এবং প্রমাণের সমতুল্য - যুক্তি থেকে ধারণা।

এই চিঠিপত্রের একটি সংমিশ্রণ হল যে প্রোগ্রামিং - প্রায়শই একটি ব্যক্তিগত নৈপুণ্য হিসাবে দেখা হয় - গণিতের আদর্শ স্তরে উন্নীত হয়। একটি প্রোগ্রাম লেখা শুধু "কোডিং" নয়, এটি একটি উপপাদ্য প্রমাণ করার একটি কাজ হয়ে ওঠে। এটি প্রোগ্রামিংয়ের কাজকে আনুষ্ঠানিক করে এবং প্রোগ্রামগুলির সঠিকতা সম্পর্কে গাণিতিকভাবে যুক্তি দেওয়ার উপায় সরবরাহ করে।

চিঠিপত্রের নামকরণ করা হয়েছে দুই গবেষকের জন্য যারা স্বাধীনভাবে এটি আবিষ্কার করেছেন। 1934 সালে, গণিতবিদ এবং যুক্তিবিদ হাসকেল কারি গণিতের ফাংশন এবং যুক্তিবিদ্যার অন্তর্নিহিত সম্পর্কের মধ্যে একটি মিল লক্ষ্য করেছিলেন, যা দুটি প্রস্তাবের মধ্যে "যদি-তাহলে" বিবৃতির আকার নেয়।

কারির পর্যবেক্ষণ দ্বারা অনুপ্রাণিত হয়ে, গাণিতিক যুক্তিবিদ উইলিয়াম অ্যালভিন হাওয়ার্ড 1969 সালে গণনা এবং যুক্তিবিদ্যার মধ্যে একটি গভীর যোগসূত্র আবিষ্কার করেন, যা দেখায় যে একটি কম্পিউটার প্রোগ্রাম চালানো অনেকটা যৌক্তিক প্রমাণকে সরল করার মতো। যখন একটি কম্পিউটার প্রোগ্রাম চলে, প্রতিটি লাইন একটি একক আউটপুট প্রদানের জন্য "মূল্যায়ন" করা হয়। একইভাবে, একটি প্রমাণে, আপনি জটিল বিবৃতি দিয়ে শুরু করেন যা আপনি সহজ করতে পারেন (অপ্রয়োজনীয় পদক্ষেপগুলি দূর করে, বা সহজতর দিয়ে জটিল অভিব্যক্তি প্রতিস্থাপন করে) যতক্ষণ না আপনি একটি সিদ্ধান্তে পৌঁছান — অনেক অন্তর্বর্তী বিবৃতি থেকে প্রাপ্ত একটি আরও ঘনীভূত এবং সংক্ষিপ্ত বিবৃতি। .

যদিও এই বর্ণনাটি চিঠিপত্রের একটি সাধারণ ধারণা প্রকাশ করে, এটি সম্পূর্ণরূপে বোঝার জন্য কম্পিউটার বিজ্ঞানীরা যাকে "টাইপ থিওরি" বলে তা সম্পর্কে আমাদের আরও কিছু শিখতে হবে।

একটি বিখ্যাত প্যারাডক্স দিয়ে শুরু করা যাক: একটি গ্রামে একজন নাপিত থাকেন যিনি সমস্ত পুরুষদের শেভ করেন যারা নিজেদের শেভ করেন না, এবং শুধুমাত্র তাদের। নাপিত কি নিজেকে শেভ করে? যদি উত্তর হ্যাঁ হয়, তাহলে তাকে অবশ্যই নিজেকে শেভ করা উচিত নয় (কারণ তিনি শুধুমাত্র সেই পুরুষদেরই শেভ করেন যারা নিজেদের শেভ করেন না)। যদি উত্তর না হয়, তবে তাকে অবশ্যই নিজেকে শেভ করতে হবে (কারণ সে সমস্ত পুরুষদের শেভ করে যারা নিজেরা শেভ করে না)। এটি সেট নামে একটি ধারণা ব্যবহার করে গণিতের ভিত্তি স্থাপন করার চেষ্টা করার সময় আবিষ্কৃত একটি প্যারাডক্স বার্ট্রান্ড রাসেলের একটি অনানুষ্ঠানিক সংস্করণ। অর্থাৎ, দ্বন্দ্বের সম্মুখীন না হয়ে এমন সমস্ত সেটকে সংজ্ঞায়িত করা অসম্ভব যা নিজেদেরকে ধারণ করে না।

এই প্যারাডক্স এড়াতে, রাসেল দেখিয়েছেন, আমরা "টাইপ" ব্যবহার করতে পারি। মোটামুটিভাবে বলতে গেলে, এগুলি এমন বিভাগ যার নির্দিষ্ট মানগুলিকে অবজেক্ট বলা হয়। উদাহরণস্বরূপ, যদি "Nat" নামে একটি প্রকার থাকে যার অর্থ প্রাকৃতিক সংখ্যা, এর বস্তুগুলি হল 1, 2, 3 এবং আরও অনেক কিছু। গবেষকরা সাধারণত একটি বস্তুর ধরন বোঝাতে একটি কোলন ব্যবহার করেন। পূর্ণসংখ্যার প্রকারের 7 নম্বরটিকে "7: পূর্ণসংখ্যা" হিসাবে লেখা যেতে পারে। আপনার এমন একটি ফাংশন থাকতে পারে যা A টাইপের একটি অবজেক্ট নেয় এবং B টাইপের একটি অবজেক্ট বের করে দেয়, অথবা যেটি A টাইপ এবং B টাইপ করা এক জোড়া বস্তুকে একত্রিত করে একটি নতুন টাইপে, যাকে বলা হয় "A × B"।

প্যারাডক্স সমাধান করার একটি উপায়, তাই, এই প্রকারগুলিকে একটি অনুক্রমের মধ্যে রাখা, যাতে তারা শুধুমাত্র নিজেদের থেকে "নিম্ন স্তরের" উপাদানগুলি ধারণ করতে পারে। তারপরে একটি টাইপ নিজেকে ধারণ করতে পারে না, যা স্ব-উল্লেখযোগ্যতা এড়িয়ে যায় যা প্যারাডক্স তৈরি করে।

টাইপ তত্ত্বের জগতে, প্রমাণ করা যে একটি বিবৃতি সত্য তা আমরা যা করতে অভ্যস্ত তার থেকে আলাদা দেখতে পারে। যদি আমরা প্রমাণ করতে চাই যে পূর্ণসংখ্যা 8 জোড়, তাহলে দেখাতে হবে যে 8 প্রকৃতপক্ষে "জোড়" নামক একটি নির্দিষ্ট ধরণের একটি বস্তু যেখানে সদস্যতার নিয়মটি 2 দ্বারা বিভাজ্য। যাচাই করার পর যে 8 বিভাজ্য। 2 দ্বারা, আমরা উপসংহারে আসতে পারি যে 8 প্রকৃতপক্ষে ইভেন টাইপের একটি "নিবাসী"।

কারি এবং হাওয়ার্ড দেখিয়েছেন যে প্রকারগুলি মৌলিকভাবে যৌক্তিক প্রস্তাবের সমতুল্য। যখন একটি ফাংশন একটি টাইপ "অবাস করে" - অর্থাৎ, যখন আপনি সফলভাবে একটি ফাংশন সংজ্ঞায়িত করতে পারেন যা সেই ধরণের একটি বস্তু - আপনি কার্যকরভাবে দেখান যে সংশ্লিষ্ট প্রস্তাবটি সত্য। সুতরাং যে ফাংশনগুলি টাইপ A-এর একটি ইনপুট নেয় এবং টাইপ B-এর একটি আউটপুট দেয়, টাইপ A → B হিসাবে চিহ্নিত করা হয়, তাদের অবশ্যই একটি অন্তর্নিহিততার সাথে সঙ্গতিপূর্ণ হতে হবে: "যদি A, তাহলে B।" উদাহরণস্বরূপ, প্রস্তাবটি নিন "যদি বৃষ্টি হয়, তাহলে মাটি ভিজে যায়।" টাইপ তত্ত্বে, এই প্রস্তাবটিকে "বৃষ্টি → গ্রাউন্ডআইসওয়েট" টাইপ সহ একটি ফাংশন দ্বারা মডেল করা হবে। ভিন্ন চেহারার ফর্মুলেশনগুলি আসলে গাণিতিকভাবে একই।

এই সংযোগটি যতটা বিমূর্ত মনে হতে পারে, এটি গণিত এবং কম্পিউটার বিজ্ঞানের অনুশীলনকারীরা তাদের কাজ সম্পর্কে কীভাবে চিন্তা করে তা কেবল পরিবর্তন করেনি, তবে উভয় ক্ষেত্রেই বেশ কয়েকটি ব্যবহারিক প্রয়োগের দিকে পরিচালিত করেছে। কম্পিউটার বিজ্ঞানের জন্য, এটি সফ্টওয়্যার যাচাইকরণের জন্য একটি তাত্ত্বিক ভিত্তি প্রদান করে, সফ্টওয়্যারের সঠিকতা নিশ্চিত করার প্রক্রিয়া। যৌক্তিক প্রস্তাবের পরিপ্রেক্ষিতে পছন্দসই আচরণ গঠন করে, প্রোগ্রামাররা গাণিতিকভাবে প্রমাণ করতে পারে যে একটি প্রোগ্রাম প্রত্যাশিত আচরণ করে। এটি আরও শক্তিশালী কার্যকরী প্রোগ্রামিং ভাষা ডিজাইন করার জন্য একটি শক্তিশালী তাত্ত্বিক ভিত্তি প্রদান করে।

আর গণিতের জন্য চিঠিপত্রের জন্ম হয়েছে প্রমাণ সহকারী, এছাড়াও ইন্টারেক্টিভ উপপাদ্য provers বলা হয়. এগুলি এমন সফ্টওয়্যার সরঞ্জাম যা আনুষ্ঠানিক প্রমাণ তৈরিতে সহায়তা করে, যেমন Coq এবং Lean৷ Coq-এ, প্রমাণের প্রতিটি ধাপ মূলত একটি প্রোগ্রাম, এবং প্রমাণের বৈধতা টাইপ-চেকিং অ্যালগরিদম দিয়ে পরীক্ষা করা হয়। গণিতবিদরাও প্রমাণ সহকারী ব্যবহার করছেন - উল্লেখযোগ্যভাবে, লীন উপপাদ্য prover — গণিতকে আনুষ্ঠানিক করতে, যার মধ্যে গাণিতিক ধারণা, উপপাদ্য এবং প্রমাণগুলিকে একটি কঠোর, কম্পিউটার-যাচাইযোগ্য বিন্যাসে উপস্থাপন করা জড়িত। এটি কম্পিউটার দ্বারা গণিতের কখনও কখনও অনানুষ্ঠানিক ভাষা পরীক্ষা করার অনুমতি দেয়।

গবেষকরা এখনও গণিত এবং প্রোগ্রামিংয়ের মধ্যে এই লিঙ্কের ফলাফলগুলি অন্বেষণ করছেন। মূল কারি-হাওয়ার্ড চিঠিপত্র প্রোগ্রামিংকে এক ধরনের যুক্তির সাথে ফিউজ করে যাকে ইনটুইশনিস্টিক লজিক বলা হয়, কিন্তু দেখা যাচ্ছে যে আরও ধরনের যুক্তিও এই ধরনের একীকরণের জন্য উপযুক্ত হতে পারে।

"কারির অন্তর্দৃষ্টির পর থেকে শতাব্দীতে যা ঘটেছে তা হল যে আমরা আরও বেশি সংখ্যক দৃষ্টান্ত আবিষ্কার করতে থাকি যেখানে 'লজিক্যাল সিস্টেম এক্স কম্পিউটেশনাল সিস্টেম ওয়াই'-এর সাথে মিলে যায়," বলেছেন মাইকেল ক্লার্কসন, কর্নেল বিশ্ববিদ্যালয়ের একজন কম্পিউটার বিজ্ঞানী। গবেষকরা ইতিমধ্যেই প্রোগ্রামিংকে অন্যান্য ধরনের লজিকের সাথে সংযুক্ত করেছেন যেমন লিনিয়ার লজিক, যার মধ্যে রয়েছে "সম্পদ" এবং মডেল লজিক, যা সম্ভাবনা এবং প্রয়োজনীয়তার ধারণা নিয়ে কাজ করে।

এবং যখন এই চিঠিপত্রটি কারি এবং হাওয়ার্ডের নাম বহন করে, তারা কোনভাবেই এটি আবিষ্কার করেনি। এটি চিঠিপত্রের মৌলিক প্রকৃতির প্রমাণ দেয়: লোকেরা এটি বারবার লক্ষ্য করে। ক্লার্কসন বলেন, "এটি কোনো দুর্ঘটনা বলে মনে হচ্ছে না যে গণনা এবং যুক্তিবিদ্যার মধ্যে একটি গভীর সম্পর্ক রয়েছে।"