ریاضی کے ثبوتوں اور کمپیوٹر پروگراموں کو برابر کرنے والا گہرا لنک | کوانٹا میگزین

کچھ سائنسی دریافتیں اہمیت رکھتی ہیں کیونکہ وہ کچھ نیا ظاہر کرتی ہیں — مثال کے طور پر ڈی این اے کی دوہری ہیلیکل ساخت، یا بلیک ہولز کا وجود۔ تاہم، کچھ انکشافات گہرے ہیں کیونکہ وہ یہ ظاہر کرتے ہیں کہ دو پرانے تصورات، جو ایک بار الگ الگ تصور کیے جاتے تھے، درحقیقت ایک جیسے ہیں۔ جیمز کلرک میکسویل کی مساوات کو لیں جو یہ ظاہر کرتے ہیں کہ بجلی اور مقناطیسیت ایک ہی رجحان کے دو پہلو ہیں، یا عمومی اضافیت کا کشش ثقل کو خمیدہ خلائی وقت کے ساتھ جوڑنا۔

کری-ہاورڈ خط و کتابت ایسا ہی کرتی ہے لیکن بڑے پیمانے پر، نہ صرف ایک فیلڈ کے اندر الگ الگ تصورات کو جوڑتی ہے، بلکہ پورے ڈسپلن: کمپیوٹر سائنس اور ریاضیاتی منطق. Curry-Howard isomorphism کے نام سے بھی جانا جاتا ہے (ایک اصطلاح جس کا مطلب ہے کہ دو چیزوں کے درمیان کسی قسم کی ایک سے ایک خط و کتابت موجود ہے)، یہ ریاضی کے ثبوتوں اور کمپیوٹر پروگراموں کے درمیان ایک ربط قائم کرتا ہے۔

سیدھے الفاظ میں، کری ہاورڈ کی خط و کتابت یہ پیش کرتی ہے کہ کمپیوٹر سائنس کے دو تصورات (قسم اور پروگرام) بالترتیب تجویزات اور ثبوتوں کے مساوی ہیں - منطق کے تصورات۔

اس خط و کتابت کا ایک نتیجہ یہ ہے کہ پروگرامنگ - جسے اکثر ذاتی دستکاری کے طور پر دیکھا جاتا ہے - کو ریاضی کی مثالی سطح تک بڑھا دیا جاتا ہے۔ پروگرام لکھنا صرف "کوڈنگ" نہیں ہے، یہ ایک تھیوریم کو ثابت کرنے کا عمل بن جاتا ہے۔ یہ پروگرامنگ کے عمل کو باقاعدہ بناتا ہے اور پروگراموں کی درستگی کے بارے میں ریاضی سے استدلال کرنے کے طریقے فراہم کرتا ہے۔

خط و کتابت کا نام ان دو محققین کے لیے رکھا گیا ہے جنہوں نے اسے آزادانہ طور پر دریافت کیا۔ 1934 میں، ریاضی دان اور منطق دان ہاسکل کری نے ریاضی میں افعال اور منطق میں مضمر تعلق کے درمیان مماثلت کو دیکھا، جو دو تجاویز کے درمیان "اگر-تو" بیانات کی شکل اختیار کرتا ہے۔

کری کے مشاہدے سے متاثر ہو کر، ریاضی کے منطق دان ولیم ایلون ہاورڈ نے 1969 میں حساب اور منطق کے درمیان ایک گہرا ربط دریافت کیا، جس سے ظاہر ہوتا ہے کہ کمپیوٹر پروگرام چلانا ایک منطقی ثبوت کو آسان بنانے جیسا ہے۔ جب ایک کمپیوٹر پروگرام چلتا ہے، تو ہر سطر کا "تجزیہ" کیا جاتا ہے تاکہ ایک ہی پیداوار حاصل ہو سکے۔ اسی طرح، ایک ثبوت میں، آپ پیچیدہ بیانات کے ساتھ شروع کرتے ہیں جنہیں آپ آسان بنا سکتے ہیں (مثال کے طور پر فالتو اقدامات کو ختم کرکے، یا پیچیدہ تاثرات کو آسان کے ساتھ بدل کر) جب تک کہ آپ کسی نتیجے پر نہ پہنچ جائیں — ایک بہت سے عبوری بیانات سے اخذ کردہ ایک زیادہ گاڑھا اور مختصر بیان۔ .

اگرچہ یہ تفصیل خط و کتابت کے عمومی احساس کو ظاہر کرتی ہے، لیکن اسے مکمل طور پر سمجھنے کے لیے ہمیں اس بارے میں تھوڑا سا مزید جاننے کی ضرورت ہے جسے کمپیوٹر سائنس دان "ٹائپ تھیوری" کہتے ہیں۔

آئیے ایک مشہور تضاد سے شروع کرتے ہیں: ایک گاؤں میں ایک حجام رہتا ہے جو ان تمام مردوں کی مونڈ دیتا ہے جو خود شیو نہیں کرتے، اور صرف ان کو۔ کیا حجام اپنا شیو کرتا ہے؟ اگر جواب ہاں میں ہے، تو اسے اپنے آپ کو منڈوانا نہیں چاہیے (کیونکہ وہ صرف ان مردوں کو مونڈتا ہے جو خود نہیں منڈواتے ہیں)۔ اگر جواب نفی میں ہے، تو اسے اپنے آپ کو منڈوانا چاہیے (کیونکہ وہ ان تمام مردوں کو مونڈتا ہے جو اپنے آپ کو شیو نہیں کرتے)۔ یہ اس تضاد کا ایک غیر رسمی ورژن ہے جسے برٹرینڈ رسل نے سیٹس نامی تصور کا استعمال کرتے ہوئے ریاضی کی بنیادیں قائم کرنے کی کوشش کرتے ہوئے دریافت کیا۔ یعنی، ایسے سیٹ کی وضاحت کرنا ناممکن ہے جس میں وہ تمام سیٹ ہوں جو تضادات کا سامنا کیے بغیر خود پر مشتمل نہ ہوں۔

اس تضاد سے بچنے کے لیے، رسل نے دکھایا، ہم "قسم" استعمال کر سکتے ہیں۔ موٹے طور پر، یہ وہ زمرے ہیں جن کی مخصوص اقدار کو آبجیکٹ کہا جاتا ہے۔ مثال کے طور پر، اگر "Nat" نام کی ایک قسم ہے، جس کا مطلب ہے قدرتی اعداد، تو اس کی اشیاء 1، 2، 3، وغیرہ ہیں۔ محققین عام طور پر کسی چیز کی قسم کو ظاہر کرنے کے لیے بڑی آنت کا استعمال کرتے ہیں۔ عدد 7، عددی قسم کے، کو "7: Integer" کے طور پر لکھا جا سکتا ہے۔ آپ کے پاس ایک ایسا فنکشن ہو سکتا ہے جو قسم A کا ایک شے لیتا ہے اور B قسم کی کسی چیز کو باہر نکالتا ہے، یا ایک ایسی چیز جو A اور ٹائپ B کو ایک نئی قسم میں جوڑتا ہے، جسے "A × B" کہا جاتا ہے۔

تضادات کو حل کرنے کا ایک طریقہ، لہذا، ان اقسام کو ایک درجہ بندی میں ڈالنا ہے، لہذا وہ صرف اپنے سے "نچلی سطح" کے عناصر پر مشتمل ہوسکتے ہیں۔ پھر ایک قسم اپنے آپ پر مشتمل نہیں ہوسکتی ہے، جو خود حوالہ جات سے گریز کرتی ہے جو تضاد پیدا کرتی ہے۔

قسم کے نظریہ کی دنیا میں، یہ ثابت کرنا کہ کوئی بیان درست ہے اس سے مختلف نظر آسکتا ہے جس کے ہم عادی ہیں۔ اگر ہم یہ ثابت کرنا چاہتے ہیں کہ عدد 8 برابر ہے، تو یہ ظاہر کرنے کی بات ہے کہ 8 درحقیقت ایک مخصوص قسم کی چیز ہے جسے "Even" کہا جاتا ہے، جہاں رکنیت کے اصول کو 2 سے تقسیم کیا جا رہا ہے۔ یہ تصدیق کرنے کے بعد کہ 8 قابل تقسیم ہے۔ 2 سے، ہم یہ نتیجہ اخذ کر سکتے ہیں کہ 8 درحقیقت ایون قسم کا "باقی" ہے۔

کری اور ہاورڈ نے دکھایا کہ اقسام بنیادی طور پر منطقی تجاویز کے برابر ہیں۔ جب کوئی فنکشن کسی قسم کو "آباد" کرتا ہے — یعنی جب آپ کامیابی کے ساتھ کسی فنکشن کی وضاحت کر سکتے ہیں جو اس قسم کا ایک شے ہے — تو آپ مؤثر طریقے سے دکھا رہے ہیں کہ متعلقہ تجویز درست ہے۔ اس لیے وہ فنکشنز جو ٹائپ A کا ان پٹ لیتے ہیں اور قسم B کا آؤٹ پٹ دیتے ہیں، جسے ٹائپ A → B کے طور پر ظاہر کیا جاتا ہے، ان کو ایک مفہوم کے مطابق ہونا چاہیے: "اگر A، تو B۔" مثال کے طور پر، "اگر بارش ہو رہی ہے، تو زمین گیلی ہے۔" ٹائپ تھیوری میں، اس تجویز کو "بارش → GroundIsWet" کی قسم کے ساتھ ایک فنکشن کے ذریعے ماڈل بنایا جائے گا۔ مختلف نظر آنے والے فارمولیشن درحقیقت ریاضی کے لحاظ سے ایک جیسے ہیں۔

جتنا خلاصہ یہ تعلق لگ سکتا ہے، اس نے نہ صرف یہ بدلا ہے کہ ریاضی اور کمپیوٹر سائنس کے ماہرین اپنے کام کے بارے میں کس طرح سوچتے ہیں، بلکہ دونوں شعبوں میں کئی عملی اطلاقات کا باعث بھی بنے۔ کمپیوٹر سائنس کے لیے، یہ سافٹ ویئر کی تصدیق کے لیے ایک نظریاتی بنیاد فراہم کرتا ہے، سافٹ ویئر کی درستگی کو یقینی بنانے کا عمل۔ منطقی تجاویز کے لحاظ سے مطلوبہ طرز عمل کو ترتیب دے کر، پروگرامرز ریاضیاتی طور پر ثابت کر سکتے ہیں کہ پروگرام توقع کے مطابق برتاؤ کرتا ہے۔ یہ زیادہ طاقتور فنکشنل پروگرامنگ زبانوں کو ڈیزائن کرنے کے لیے ایک مضبوط نظریاتی بنیاد بھی فراہم کرتا ہے۔

اور ریاضی کے لیے خط و کتابت نے جنم لیا۔ ثبوت معاونینجسے انٹرایکٹو تھیوریم پرورز بھی کہا جاتا ہے۔ یہ سافٹ ویئر ٹولز ہیں جو باضابطہ ثبوت بنانے میں مدد کرتے ہیں، جیسے Coq اور Lean۔ Coq میں، ثبوت کا ہر مرحلہ بنیادی طور پر ایک پروگرام ہے، اور ثبوت کی درستگی کو ٹائپ چیکنگ الگورتھم کے ساتھ چیک کیا جاتا ہے۔ ریاضی دان پروف اسسٹنٹ بھی استعمال کرتے رہے ہیں - خاص طور پر، دبلی پتلی تھیوری کہنے والا - ریاضی کو باضابطہ بنانے کے لیے، جس میں ریاضی کے تصورات، نظریات اور ثبوتوں کو ایک سخت، کمپیوٹر سے قابل تصدیق فارمیٹ میں پیش کرنا شامل ہے۔ یہ کمپیوٹر کے ذریعہ ریاضی کی بعض اوقات غیر رسمی زبان کو جانچنے کی اجازت دیتا ہے۔

محققین اب بھی ریاضی اور پروگرامنگ کے درمیان اس لنک کے نتائج کی تلاش کر رہے ہیں۔ اصل Curry-Howard خط و کتابت پروگرامنگ کو ایک قسم کی منطق کے ساتھ فیوز کرتی ہے جسے intuitionistic logic کہا جاتا ہے، لیکن یہ پتہ چلتا ہے کہ منطق کی مزید اقسام بھی اس طرح کے اتحاد کے لیے موزوں ہو سکتی ہیں۔

"کری کی بصیرت کے بعد سے اس صدی میں جو کچھ ہوا ہے وہ یہ ہے کہ ہم زیادہ سے زیادہ ایسی مثالیں دریافت کرتے رہتے ہیں جہاں 'لاجیکل سسٹم X کمپیوٹیشنل سسٹم Y سے مطابقت رکھتا ہے،'" کہا۔ مائیکل کلارکسنکارنیل یونیورسٹی میں کمپیوٹر سائنسدان۔ محققین نے پہلے ہی پروگرامنگ کو منطق کی دوسری قسموں سے جوڑ دیا ہے جیسے لکیری منطق، جس میں "وسائل" کا تصور اور موڈل منطق شامل ہے، جو امکان اور ضرورت کے تصورات سے متعلق ہے۔

اور جب کہ اس خط و کتابت میں کری اور ہاورڈ کے نام ہیں، لیکن وہ کسی بھی طرح سے صرف وہی نہیں ہیں جنہوں نے اسے دریافت کیا ہے۔ یہ خط و کتابت کی بنیادی نوعیت کی تصدیق کرتا ہے: لوگ اسے بار بار دیکھتے رہتے ہیں۔ "یہ کوئی حادثہ نہیں لگتا ہے کہ حساب اور منطق کے درمیان گہرا تعلق ہے،" کلارکسن نے کہا۔