বিংশ শতাব্দী জুড়ে গণিত যুক্তিবিজ্ঞান, কম্পিউটার বিজ্ঞান এবং ক্যাটাগরি থিওরি তিনটি বিচ্ছিন্ন দ্বীপের মতো আলাদাভাবে বিকশিত হচ্ছিল। যুক্তিবিজ্ঞান বিশ্লেষণ করছিল উক্তি ও প্রমাণের কাঠামো; কম্পিউটার বিজ্ঞান তৈরি করছিল অ্যালগরিদম ও ডেটা টাইপ; আর ক্যাটাগরি থিওরি খুঁজছিল মহাজাগতিক রূপান্তর ও তীরচিত্র। হঠাৎ এক অভাবনীয় আবিষ্কার এই তিন মহাসমুদ্রকে এক মোহনায় মিলিয়ে দিল: কারি-হাওয়ার্ড-ল্যামবেক সাদৃশ্য (Curry-Howard-Lambek Correspondence)। একটি গাণিতিক উক্তি হলো মূলত একটি ডেটা টাইপ; সেই উক্তির আনুষ্ঠানিক প্রমাণ হলো একটি কম্পিউটার প্রোগ্রাম; আর প্রমাণ সরলীকরণ হলো সরাসরি সেই প্রোগ্রামের কার্যকর সম্পাদন।
১. প্রপোজিশন-অ্যাজ-টাইপস নীতি (The Curry-Howard Isomorphism)
১৯৩৪ সালে হাস্কেল কারি এবং ১৯৬৯ সালে উইলিয়াম আলভিন হাওয়ার্ড আবিষ্কার করেন যে ইনটুইশনিস্টিক যুক্তিবিজ্ঞান এবং টাইপযুক্ত ল্যাম্বডা ক্যালকুলাসের ($lambda^to$) মধ্যে একটি নিখুঁত দ্বিমুখী আইসোমরফিজম বিদ্যমান:
কারি-হাওয়ার্ড-ল্যামবেক সমন্বয় অভিধান
| ইনটুইশনিস্টিক যুক্তি | টাইপ থিওরি / কম্পিউটার বিজ্ঞান | ক্যাটাগরি থিওরি (CCC) |
|---|---|---|
| উক্তি $A$ (Proposition) | ডেটা টাইপ $A$ | অবজেক্ট $A in text{Ob}(mathcal{C})$ |
| $A$-এর প্রমাণ $pi$ | $A$ টাইপের প্রোগ্রাম $t : A$ | মর্ফিজম $f: 1 to A$ |
| যোজক $A land B$ | প্রোডাক্ট টাইপ $A times B$ (Pair) | ক্যাটাগরিক্যাল প্রোডাক্ট $A times B$ |
| বিয়োজক $A lor B$ | সাম বা আইদার টাইপ $A + B$ | কোপণ্য / কোপ্রোডাক্ট $A amalg B$ |
| শর্তায়ন $A to B$ | ফাংশন টাইপ $A to B$ | এক্সপোনেনশিয়াল অবজেক্ট $B^A$ |
| কাট এলিমিনেশন (প্রমাণ সরলীকরণ) | বিটা-রিডাকশন (প্রোগ্রাম এক্সিকিউশন) | তীরচিহ্নের সমতা |
২. শর্তায়ন ও ল্যাম্বডা ফাংশনের অভিন্নতা
ন্যাচারাল ডিডাকশনে যখন বলা হয়: “$A$-কে ধরে নিয়ে যদি $B$ প্রমাণ করা যায়, তবে $A to B$ সত্য”—কম্পিউটার বিজ্ঞানে এর অর্থ কী?
এর অর্থ হলো: ইনপুট হিসেবে $A$ টাইপের আর্গুমেন্ট গ্রহণ করে $B$ টাইপের ফলাফল প্রদানকারী একটি ল্যাম্বডা ফাংশন তৈরি করা $(lambda x: A . e)$। আর মোডাস পনেনস মানে হলো ফাংশনে আর্গুমেন্ট পাস করে তাকে রান করা $(f , a)$!
ফাংশন যখন তার আর্গুমেন্ট গ্রহণ করে মান বের করে ($beta$-reduction):
[
(lambda x . e) , a longrightarrow_beta e[x mapsto a]
]
এটি হুবহু গণিতের সেই কাট এলিমিনেশন প্রক্রিয়া! অর্থাৎ একটি কম্পিউটার প্রোগ্রাম চালানো এবং একটি গাণিতিক প্রমাণকে সরলতম রূপ দেওয়া মূলত একই ঘটনার দুটি ভিন্ন নাম।
৩. জোয়াকিম ল্যামবেক: কার্তেসীয় বদ্ধ ক্যাটাগরি (CCC)
১৯৭২ সালে কানাডিয়ান গণিতবিদ জোয়াকিম ল্যামবেক প্রমাণ করেন যে এই কাঠামোটি হুবহু কার্তেসীয় বদ্ধ ক্যাটাগরি (Cartesian Closed Category)-এর কাঠামোর সাথে সমার্থক। ফাংশনাল স্পেস এবং কার্তেসীয় গুণফলের ক্যাটাগরিক্যাল রূপান্তর ল্যাম্বডা ক্যালকুলাস ও যুক্তিবিজ্ঞানের সমীকরণগুলোকে পরম জ্যামিতিক উচ্চতায় অধিষ্ঠিত করে। যুক্তি, ভাষা ও মহাবিশ্ব একই সুতোয় বাঁধা পড়ল।
৪. ডিপেন্ডেন্ট টাইপ থিওরি: আধুনিক গণিতের ভবিষ্যৎ
১৯৭২ সালে পার মার্টিন-লোফ উদ্ভাবন করেন ডিপেন্ডেন্ট টাইপ থিওরি (Dependent Type Theory):
- সার্বজনীন কোয়ান্টিফায়ার $forall x . P(x)$ পরিণত হলো $Pi$-টাইপে (যেখানে আউটপুট টাইপ ইনপুটের ওপর নির্ভরশীল)।
- অস্তিত্ববাচক কোয়ান্টিফায়ার $exists x . P(x)$ পরিণত হলো $Sigma$-টাইপে (একটি ডিপেন্ডেন্ট জোড় যেখানে উপাদান ও তার প্রমাণের যৌথ বসবাস)।
আজকের দিনে যখন Lean 4 বা Coq-এর মতো সফটওয়্যারে গণিতবিদরা কঠিন উপপাদ্য প্রমাণ করেন, তখন তারা মূলত ডিপেন্ডেন্ট টাইপ থিওরিতে কোড লেখেন। টাইপ চেকার যদি কোডটি সফলভাবে কম্পাইল করতে পারে, তবে উপপাদ্যটি ১০০% প্রমাণিত! ভুল প্রমাণ মানে স্রেফ একটি কম্পাইলার এরর। গণিত ও কোডিং চিরতরে একাকার হয়ে গেল।
