Hindley–Milner type system
ہینڈلی ملنر (ایچ ایم) قسم کا نظام لیمبڈا کیلکولس کے لیے ایک کلاسیکی قسم کا نظام ہے جس میں پیرامیٹرک پولیمرفزم ہوتا ہے۔ اسے داماس ملنر یا داماس ہنڈلے ملنر کے نام سے بھی جانا جاتا ہے۔ اسے سب سے پہلے جے راجر ہینڈلی نے بیان کیا تھا اور بعد میں رابن ملنر نے اسے دوبارہ دریافت کیا۔ لوئس ڈیماس نے اپنے پی ایچ ڈی مقالے میں اس طریقہ کار کے قریبی رسمی تجزیے اور ثبوت کا تعاون کیا۔ ایچ ایم کی زیادہ قابل ذکر خصوصیات میں اس کی تکمیل اور پروگرامر کے فراہم کردہ قسم کی تشریحات یا دیگر اشارے کے بغیر کسی دیئے گئے پروگرام کی سب سے عام قسم کا اندازہ لگانے کی صلاحیت ہے۔ الگورتھم ڈبلیو عملی طور پر ایک موثر قسم کا تخمینہ طریقہ ہے اور اسے بڑے کوڈ اڈوں پر کامیابی کے ساتھ لاگو کیا گیا ہے، حالانکہ اس میں اعلی نظریاتی پیچیدگی ہے۔ ایچ ایم ترجیحی طور پر فنکشنل زبانوں کے لیے استعمال ہوتا ہے۔ اسے سب سے پہلے پروگرامنگ زبان ایم ایل کے ٹائپ سسٹم کے حصے کے طور پر نافذ کیا گیا تھا۔ اس کے بعد سے، ایچ ایم کو مختلف طریقوں سے بڑھایا گیا ہے، خاص طور پر ٹائپ کلاس کی رکاوٹوں کے ساتھ جیسے کہ ہاسکل میں۔ ایک قسم کے تخمینہ کے طریقہ کار کے طور پر، ہینڈلی ملنر مکمل طور پر غیر ٹائپ شدہ انداز میں لکھے گئے پروگراموں سے متغیرات، تاثرات اور افعال کی اقسام کا اندازہ لگانے کے قابل ہے۔ دائرہ کار کے حوالے سے حساس ہونے کی وجہ سے، یہ صرف سورس کوڈ کے ایک چھوٹے سے حصے سے ہی اقسام حاصل کرنے تک محدود نہیں ہے، بلکہ مکمل پروگراموں یا ماڈیولز سے حاصل کرنے تک محدود ہے۔ پیرامیٹرک اقسام سے نمٹنے کے قابل ہونے کی وجہ سے، یہ بہت سی فنکشنل پروگرامنگ زبانوں کے ٹائپ سسٹمز کا بنیادی حصہ ہے۔ اسے سب سے پہلے ایم ایل پروگرامنگ زبان میں اس طریقے سے لاگو کیا گیا تھا۔ اصل صرف ٹائپ شدہ لیمبڈا کیلکولس کے لیے ٹائپ انفریشن الگورتھم ہے جسے ہاسکل کری اور رابرٹ فیز نے 1958 میں وضع کیا تھا۔ 1969 میں، جے راجر ہینڈلی نے اس کام کو بڑھایا اور ثابت کیا کہ ان کے الگورتھم نے ہمیشہ سب سے عام قسم کا اندازہ لگایا۔ 1978 میں، رابن ملنر نے آزادانہ طور پر ہنڈلے کے کام سے، ایک مساوی الگورتھم، الگورتھم ڈبلیو فراہم کیا۔ 1982 میں، لوئس ڈیماس نے آخر کار ثابت کیا کہ ملنر کا الگورتھم مکمل ہے اور اسے پولیمرفک حوالہ جات والے سسٹمز کی حمایت کرنے کے لیے بڑھایا۔ مونومورفزم بمقابلہ پولیمورفزم سادہ ٹائپ شدہ لیمبڈا کیلکولس میں، اقسام یا تو جوہری قسم کے مستقل یا فنکشن کی اقسام ہیں۔ اس طرح کی اقسام مونومورفک ہوتی ہیں۔ عام مثالیں ریاضی کی اقدار میں استعمال ہونے والی اقسام ہیں: 3: نمبر ایڈ 3 4: نمبر ایڈ: نمبر-> نمبر-> نمبر اس کے برعکس، غیر ٹائپ شدہ لیمبڈا کیلکولس ٹائپنگ کے لیے بالکل غیر جانبدار ہے، اور اس کے بہت سے افعال کو معنی خیز طور پر ہر قسم کے دلائل پر لاگو کیا جا سکتا ہے۔ معمولی مثال شناخت فنکشن آئی ڈی ष्ण λx ہے۔ x جو صرف اس قدر کو واپس کرتا ہے جس پر اس کا اطلاق ہوتا ہے۔ کم معمولی مثالوں میں پیرامیٹرک اقسام جیسے فہرستیں شامل ہیں۔ اگرچہ عام طور پر پولیمرفزم کا مطلب یہ ہے کہ آپریشن ایک سے زیادہ قسم کی اقدار کو قبول کرتے ہیں، لیکن یہاں استعمال ہونے والا پولیمرفزم پیرامیٹرک ہے۔ ادب میں ٹائپ اسکیموں کے اشارے بھی ملتے ہیں، جو پولیمرفزم کی پیرامیٹرک نوعیت پر زور دیتے ہیں۔ مزید برآں، مستقلات کو (مقداری) قسم کے متغیرات کے ساتھ ٹائپ کیا جا سکتا ہے۔ ای۔ جی۔ : نقصانات: فارال اے۔ a-> فہرست a-> فہرست a صفر: عام طور پر a۔ ایک آئی ڈی درج کریں: فارال اے۔ a-> ایک پولیمورفک اقسام اپنے متغیرات کے مستقل متبادل کے ذریعے مونومورفک بن سکتی ہیں۔ مونومورفک مثالوں کی مثالیں یہ ہیں: آئی ڈی ': سٹرنگ-> سٹرنگ نیل': لسٹ نمبر زیادہ عام طور پر، اقسام پولیمورفک ہوتی ہیں جب ان میں ٹائپ متغیر ہوتے ہیں، جبکہ ان کے بغیر اقسام مونومورفک ہوتی ہیں۔ مثال کے طور پر پاسکل (1970) یا سی (1972) میں استعمال ہونے والے ٹائپ سسٹمز کے برعکس، جو صرف مونومورفک اقسام کی حمایت کرتے ہیں، ایچ ایم کو پیرامیٹرک پولیمرفزم پر زور دینے کے ساتھ ڈیزائن کیا گیا ہے۔ سی + + (1985) جیسی مذکور زبانوں کے جانشینوں نے مختلف قسم کے پولیمرفزم پر توجہ مرکوز کی، یعنی آبجیکٹ پر مبنی پروگرامنگ اور اوور لوڈنگ کے سلسلے میں ذیلی ٹائپنگ۔ اگرچہ سب ٹائپنگ ایچ ایم کے ساتھ مطابقت نہیں رکھتی ہے، لیکن ہاسکل کے ایچ ایم پر مبنی قسم کے نظام میں منظم اوور لوڈنگ کا ایک قسم دستیاب ہے۔ جب آسانی سے ٹائپ شدہ لیمبڈا کیلکولس کے لیے قسم کے تخمینے کو پولیمرفزم کی طرف بڑھایا جاتا ہے، تو کسی کو اس بات کی وضاحت کرنی ہوتی ہے کہ قدر کی مثال کب حاصل کرنا قابل قبول ہے۔ مثالی طور پر، باؤنڈ متغیر کے کسی بھی استعمال کے ساتھ اس کی اجازت ہوگی، جیسا کہ: (λ آئی ڈی۔ . (آئی ڈی 3). (آئی ڈی "ٹیکسٹ").) (λx۔ x) بدقسمتی سے، پولیمرفک لیمبڈا کیلکولس میں قسم کا تخمینہ فیصلہ کن نہیں ہے۔ اس کے بجائے، ایچ ایم آئی ڈی = λx کی شکل کا لیٹ پولیمرفزم فراہم کرتا ہے۔ x in. (آئی ڈی 3). (آئی ڈی "ٹیکسٹ"). اظہار نحو کی توسیع میں بائنڈنگ میکانزم کو محدود کرنا۔ صرف لیٹ کنسٹرکٹ میں پابند اقدار فوری ہونے کے تابع ہیں، یعنی۔ پولیمرفک ہوتے ہیں، جبکہ لیمبڈا-تجریدوں میں پیرامیٹرز کو مونومورفک سمجھا جاتا ہے۔ جائزہ اس مضمون کا بقیہ حصہ مندرجہ ذیل ہے: ایچ ایم قسم کے نظام کی وضاحت کی گئی ہے۔ یہ ایک کٹوتی کے نظام کو بیان کرکے کیا جاتا ہے جو واضح کرتا ہے کہ کس قسم کے تاثرات ہیں، اگر کوئی ہیں۔ وہاں سے، یہ ٹائپ انفریشن طریقہ کار کے نفاذ کی طرف کام کرتا ہے۔ مذکورہ بالا کٹوتی کے نظام کا نحو پر مبنی ورژن متعارف کرانے کے بعد، یہ ایک موثر نفاذ (الگورتھم جے) کا خاکہ بناتا ہے، جو زیادہ تر قارئین کے دھاتی وجدان کو اپیل کرتا ہے۔ کیونکہ یہ کھلا رہتا ہے کہ آیا الگورتھم جے واقعی ابتدائی کٹوتی کے نظام کا ادراک کرتا ہے، ایک کم موثر نفاذ (الگورتھم ڈبلیو) متعارف کرایا جاتا ہے اور ثبوت میں اس کے استعمال کا اشارہ دیا جاتا ہے۔ آخر میں، الگورتھم سے متعلق مزید موضوعات پر تبادلہ خیال کیا جاتا ہے۔ کٹوتی کے نظام کی ایک ہی تفصیل پوری طرح استعمال کی جاتی ہے، یہاں تک کہ دو الگورتھم کے لیے بھی، مختلف شکلوں کو بنانے کے لیے جس میں ایچ ایم طریقہ براہ راست موازنہ کیا جاتا ہے۔ ہندلے ملنر قسم کا نظام قسم کے نظام کو رسمی طور پر نحو کے اصولوں کے ذریعے بیان کیا جا سکتا ہے جو تاثرات، اقسام وغیرہ کے لیے زبان طے کرتے ہیں۔ اس طرح کے نحو کی یہاں پیش کش زیادہ رسمی نہیں ہے، اس میں یہ سطحی گرائمر کا مطالعہ کرنے کے لیے نہیں، بلکہ گہرائی کے گرائمر کا مطالعہ کرنے کے لیے لکھی گئی ہے، اور کچھ نحو تفصیلات کو کھلا چھوڑ دیتی ہے۔ پیشکش کی یہ شکل معمول کی بات ہے۔ اس کی بنیاد پر، ٹائپنگ کے قوانین کا استعمال اس بات کی وضاحت کے لیے کیا جاتا ہے کہ تاثرات اور اقسام کا تعلق کیسے ہے۔ پہلے کی طرح، استعمال شدہ شکل قدرے آزادانہ ہے۔ نحو ٹائپ کیے جانے والے تاثرات بالکل لیمبڈا کیلکولس کے ہیں جو لیٹ ایکسپریشن کے ساتھ بڑھائے گئے ہیں جیسا کہ ملحقہ ٹیبل میں دکھایا گیا ہے۔ قوسین کو اظہار کو غیر واضح کرنے کے لیے استعمال کیا جا سکتا ہے۔ ایپلیکیشن لیفٹ بائنڈنگ ہے اور تجریدی یا لیٹ ان کنسٹرکٹ سے زیادہ مضبوط بناتی ہے۔ اقسام کو نحو طور پر دو گروپوں، مونوٹائپز اور پولی ٹائپز میں تقسیم کیا گیا ہے۔ مونوٹائپ ہمیشہ ایک مخصوص قسم کو نامزد کرتے ہیں۔ مونوٹائپز کو نحو طور پر اصطلاحات کے طور پر پیش کیا جاتا ہے۔ مونوٹائپ کی مثالوں میں قسم کے مستقل جیسے یا، اور پیرامیٹرک اقسام جیسے شامل ہیں۔ مؤخر الذکر اقسام قسم کے افعال کی ایپلی کیشنز کی مثالیں ہیں، مثال کے طور پر، سیٹ سے، جہاں سپر اسکرپٹ قسم کے پیرامیٹرز کی تعداد کی نشاندہی کرتا ہے۔ ٹائپ فنکشنز کا مکمل سیٹ ایچ ایم میں من مانی ہے، سوائے اس کے کہ اس میں کم از کم فنکشنز کی قسم ہونی چاہیے۔ یہ اکثر سہولت کے لیے انفیکس نوٹیشن میں لکھا جاتا ہے۔ مثال کے طور پر، سٹرنگ کے لیے انٹیجرز کی نقشہ سازی کرنے والے فنکشن کی قسم ہوتی ہے۔ ایک بار پھر، قوسین کو کسی قسم کے اظہار کو غیر واضح کرنے کے لیے استعمال کیا جا سکتا ہے۔ ایپلی کیشن انفیکس تیر سے زیادہ مضبوط باندھتی ہے، جو دائیں طرف سے جڑا ہوا ہے۔ ٹائپ متغیرات کو مونوٹائپ کے طور پر قبول کیا جاتا ہے۔ مونوٹائپز کو مونومورفک اقسام کے ساتھ الجھن میں نہیں ڈالنا چاہیے، جو متغیرات کو خارج کرتے ہیں اور صرف زمینی اصطلاحات کی اجازت دیتے ہیں۔ دو مونوٹائپ برابر ہوتے ہیں اگر ان کی اصطلاحات ایک جیسی ہوں۔ پولی ٹائپز پولی ٹائپز (یا ٹائپ اسکیمیں) ایسی اقسام ہیں جن میں تمام کوانٹیفایئرز کے لیے صفر یا اس سے زیادہ کے پابند متغیر ہوتے ہیں، مثال کے طور پر۔ ۔ پولی ٹائپ والا فنکشن ایک ہی قسم کی کسی بھی قدر کو اپنے ساتھ نقشہ بنا سکتا ہے، اور شناختی فنکشن اس قسم کے لیے ایک قدر ہے۔ ایک اور مثال کے طور پر، فنکشن کی قسم ہے جو تمام محدود سیٹوں کو انٹیجرز پر نقش کرتی ہے۔ ایک فنکشن جو کسی سیٹ کی بنیادی حیثیت کو واپس کرتا ہے اس قسم کی قیمت ہوگی۔ کوانٹیفائرز صرف اعلی سطح پر ظاہر ہو سکتے ہیں۔ مثال کے طور پر، ایک قسم کو اقسام کے نحو سے خارج کر دیا جاتا ہے۔ نیز مونوٹائپز کو پولی ٹائپز میں شامل کیا جاتا ہے، اس طرح ایک قسم کی عمومی شکل ہوتی ہے، جہاں ایک مونوٹائپ ہوتا ہے۔ کثیر اقسام کی مساوات مقدار کو دوبارہ ترتیب دینے اور مقداری متغیرات (-تبدیلی) کا نام تبدیل کرنے پر منحصر ہے۔ مزید برآں، مونوٹائپ میں نہ پائے جانے والے مقداری متغیرات کو گرایا جا سکتا ہے۔ سیاق و سباق اور ٹائپنگ معنی خیز طور پر اب بھی جداگانہ حصوں (نحو کے تاثرات اور اقسام) کو اکٹھا کرنے کے لیے ایک تیسرے حصے کی ضرورت ہے: سیاق و سباق۔ لفظی طور پر، سیاق و سباق جوڑوں کی ایک فہرست ہے، جسے اسائنمنٹس، مفروضے یا بائنڈنگ کہا جاتا ہے، ہر جوڑا یہ بتاتا ہے کہ ویلیو متغیر کی قسم ہے۔ تینوں حصے مل کر فارم کا ٹائپنگ فیصلہ دیتے ہیں، یہ کہتے ہوئے کہ مفروضوں کے تحت، اظہار کی قسم ہوتی ہے۔ آزاد قسم کے متغیرات ایک قسم میں، علامت مونوٹائپ میں قسم کے متغیرات کو پابند کرنے والا مقداری ہوتا ہے۔ متغیرات کو مقداری کہا جاتا ہے اور کسی مقداری قسم کے متغیر کی کسی بھی موجودگی کو باؤنڈ کہا جاتا ہے اور تمام غیر باؤنڈ قسم کے متغیرات کو فری کہا جاتا ہے۔ پولی ٹائپز میں مقدار کے علاوہ، ٹائپ متغیرات کو سیاق و سباق میں واقع ہونے سے بھی پابند کیا جا سکتا ہے، لیکن اس کے دائیں ہاتھ کی طرف الٹا اثر ہوتا ہے۔ اس طرح کے متغیرات پھر وہاں ٹائپ مستقلات کی طرح برتاؤ کرتے ہیں۔ آخر میں، ایک ٹائپ متغیر قانونی طور پر ٹائپنگ میں غیر پابند ہو سکتا ہے، ایسی صورت میں وہ مضمر طور پر تمام مقدار میں ہوتے ہیں۔ پروگرامنگ زبانوں میں باؤنڈ اور ان باؤنڈ دونوں قسم کے متغیرات کی موجودگی قدرے غیر معمولی ہے۔ اکثر، تمام قسم کے متغیرات کو مضمر طور پر تمام مقدار میں علاج کیا جاتا ہے۔ مثال کے طور پر، پرولاگ میں مفت متغیرات کے ساتھ کلاز نہیں ہیں۔ اسی طرح ہاسکل میں، جہاں تمام قسم کے متغیرات مضمر طور پر مقداری ہوتے ہیں، یعنی۔ ایک ہاسکل ٹائپ کریں a-> a کا مطلب یہاں ہے۔ تفویض کے دائیں ہاتھ کی طرف کا بائنڈنگ اثر متعلقہ اور بہت غیر معمولی بھی ہے۔ عام طور پر، باؤنڈ اور ان باؤنڈ دونوں قسم کے متغیرات کا مرکب ایک اظہار میں فری متغیرات کے استعمال سے پیدا ہوتا ہے۔ مستقل فعل K = ایک مثال فراہم کرتا ہے۔ اس میں مونوٹائپ ہے۔ اس کے ذریعے پولیمرفزم کو مجبور کیا جا سکتا ہے۔ یہاں ٹائپ ہے۔ آزاد مونوٹائپ متغیر ارد گرد کے دائرہ کار میں پابند متغیر کی قسم سے نکلتا ہے۔ قسم ہے۔ کوئی بھی اس قسم کے آزاد قسم کے متغیر کا تصور کر سکتا ہے جس کی قسم میں سے پابند ہو۔ لیکن اس طرح کے دائرہ کار کا اظہار ایچ ایم میں نہیں کیا جا سکتا۔ بلکہ، بائنڈنگ کا احساس سیاق و سباق سے ہوتا ہے۔ ٹائپ آرڈر پولیمرفزم کا مطلب ہے کہ ایک اور ایک ہی اظہار کی (شاید لامحدود) کئی قسمیں ہو سکتی ہیں۔ لیکن اس قسم کے نظام میں، یہ اقسام مکمل طور پر غیر متعلقہ نہیں ہیں، بلکہ پیرامیٹرک پولیمرفزم کے ذریعے ترتیب دی گئی ہیں۔ مثال کے طور پر، شناخت کی اپنی قسم کے ساتھ ساتھ یا اور بہت سے دوسرے بھی ہو سکتے ہیں، لیکن نہیں۔ اس فنکشن کی سب سے عام قسم ہے، جبکہ دیگر زیادہ مخصوص ہیں اور ٹائپ پیرامیٹر کے لیے دوسری قسم کو مستقل طور پر تبدیل کر کے عام سے اخذ کیا جا سکتا ہے، یعنی۔ مقداری متغیر۔ جوابی مثال ناکام ہو جاتی ہے کیونکہ متبادل مستقل نہیں ہوتا ہے۔ مستقل تبدیلی کو تحریری طور پر کسی قسم کی اصطلاح کے متبادل کا اطلاق کرکے رسمی بنایا جا سکتا ہے۔ جیسا کہ مثال سے پتہ چلتا ہے، متبادل کا نہ صرف کسی آرڈر سے گہرا تعلق ہوتا ہے، جو اس بات کا اظہار کرتا ہے کہ ایک قسم کم و بیش خاص ہے، بلکہ تمام مقدار کے ساتھ بھی جو متبادل کو لاگو کرنے کی اجازت دیتا ہے۔ رسمی طور پر، ایچ ایم میں، ایک قسم اس سے زیادہ عام ہوتی ہے، رسمی طور پر، اگر کچھ مقداری متغیر کو مستقل طور پر اس طرح تبدیل کیا جاتا ہے کہ ایک فائدہ ہوتا ہے جیسا کہ سائیڈ بار میں دکھایا گیا ہے۔ یہ ترتیب ٹائپ سسٹم کی قسم کی تعریف کا حصہ ہے۔ ہماری پچھلی مثال میں، متبادل کو لاگو کرنے کا نتیجہ ہوگا۔ جبکہ ایک مقداری متغیر کے لیے مونومورفک (گراؤنڈ) قسم کو تبدیل کرنا سیدھا آگے ہے، پولی ٹائپ کو تبدیل کرنے میں آزاد متغیرات کی موجودگی کی وجہ سے کچھ نقصانات ہوتے ہیں۔ خاص طور پر، غیر پابند متغیرات کو تبدیل نہیں کیا جانا چاہیے۔ انہیں یہاں مستقل سمجھا جاتا ہے۔ مزید برآں، مقدار صرف اعلی سطح پر ہو سکتی ہے۔ پیرامیٹرک قسم کو تبدیل کرتے ہوئے، کسی کو اس کے کوانٹیفایئرز کو اٹھانا پڑتا ہے۔ دائیں طرف کی میز اصول کو درست بناتی ہے۔ متبادل طور پر، کوانٹیفائرز کے بغیر پولی ٹائپز کے لیے ایک مساوی نوٹیشن پر غور کریں جس میں کوانٹیفائیڈ متغیرات کی نمائندگی علامتوں کے ایک مختلف سیٹ کے ذریعے کی جاتی ہے۔ اس طرح کے اشارے میں، تخصص اس طرح کے متغیرات کے سادہ مستقل متبادل تک کم ہو جاتی ہے۔ رشتہ ایک جزوی ترتیب ہے اور اس کا سب سے چھوٹا عنصر ہے۔ پرنسپل ٹائپ جبکہ ٹائپ اسکیم کی تخصص آرڈر کا ایک استعمال ہے، یہ ٹائپ سسٹم میں ایک اہم دوسرا کردار ادا کرتا ہے۔ پولیمرفزم کے ساتھ ٹائپ انفریشن کو تمام ممکنہ اقسام کا خلاصہ کرنے کے چیلنج کا سامنا کرنا پڑتا ہے جو ایک اظہار ہو سکتا ہے۔ آرڈر اس بات کی ضمانت دیتا ہے کہ اس طرح کا خلاصہ اظہار کی سب سے عام قسم کے طور پر موجود ہے۔ ٹائپنگ میں متبادل اوپر بیان کردہ ٹائپ آرڈر کو ٹائپنگ تک بڑھایا جا سکتا ہے کیونکہ ٹائپنگ کی مضمر تمام مقدار مستقل تبدیلی کے قابل بناتی ہے: تخصص کے اصول کے برعکس، یہ تعریف کا حصہ نہیں ہے، بلکہ مضمر تمام مقدار کی طرح ہے بلکہ اگلے بیان کردہ قسم کے اصولوں کا نتیجہ ہے۔ ٹائپنگ میں فری ٹائپ متغیرات ممکنہ اصلاح کے لیے پلیس ہولڈرز کے طور پر کام کرتے ہیں۔ اس کے دائیں جانب فری ٹائپ متغیرات کے لیے ماحول کا بائنڈنگ اثر تخصص کے اصول میں ان کے متبادل کو روکتا ہے کہ ایک متبادل مستقل ہونا چاہیے اور اس میں پوری ٹائپنگ شامل کرنے کی ضرورت ہوگی۔ یہ مضمون چار مختلف قاعدے کے سیٹوں پر تبادلہ خیال کرے گا: ڈیکلیریٹو سسٹم سنٹیکٹیکل سسٹم الگورتھم جے الگورتھم ڈبلیو ڈڈکٹو سسٹم ایچ ایم کے نحو کو تشخیصی اصولوں کے نحو کی طرف آگے بڑھایا جاتا ہے جو رسمی نظام کا بنیادی حصہ بناتے ہیں، ٹائپنگ کو فیصلے کے طور پر استعمال کرتے ہوئے۔ ہر ایک اصول اس بات کی وضاحت کرتا ہے کہ کس احاطے سے کیا نتیجہ اخذ کیا جا سکتا ہے۔ فیصلوں کے علاوہ، اوپر پیش کی گئی کچھ اضافی شرائط کو بھی احاطے کے طور پر استعمال کیا جا سکتا ہے۔ قواعد کا استعمال کرتے ہوئے ثبوت فیصلوں کا ایک سلسلہ ہے جس میں کسی نتیجے سے پہلے تمام احاطے درج کیے جاتے ہیں۔ نیچے دی گئی مثالیں ثبوت کی ممکنہ شکل کو ظاہر کرتی ہیں۔ بائیں سے دائیں، ہر لائن نتیجہ، لاگو کردہ اصول اور احاطے کو ظاہر کرتی ہے، یا تو سابقہ لائن (نمبر) کا حوالہ دے کر اگر بنیاد فیصلہ ہے یا پیش گوئی کو واضح کر کے۔ ٹائپنگ کے قواعد بھی دیکھیں ٹائپنگ کے قواعد سائیڈ باکس ایچ ایم ٹائپ سسٹم کے کٹوتی کے قواعد کو ظاہر کرتا ہے۔ کوئی بھی قواعد کو تقریبا دو گروپوں میں تقسیم کر سکتا ہے: پہلے چار اصول (متغیر یا فنکشن تک رسائی)، (درخواست، یعنی۔ فنکشن کال ایک پیرامیٹر کے ساتھ)، (تجریدی، یعنی۔ فنکشن ڈیکلریشن) اور (متغیر ڈیکلریشن) نحو کے ارد گرد مرکوز ہیں، ہر ایک اظہار فارم کے لیے ایک اصول پیش کرتے ہیں۔ ان کے معنی پہلی نظر میں واضح ہوتے ہیں، کیونکہ وہ ہر اظہار کو تحلیل کرتے ہیں، اپنے ذیلی تاثرات کو ثابت کرتے ہیں اور آخر میں احاطے میں پائے جانے والے انفرادی اقسام کو نتیجہ میں موجود قسم سے جوڑتے ہیں۔ دوسرا گروپ بقیہ دو اصولوں اور قواعد سے تشکیل پاتا ہے۔ وہ اقسام کی تخصص اور عمومی کاری کو سنبھالتے ہیں۔ اگرچہ مذکورہ بالا تخصص کے سیکشن سے قاعدہ واضح ہونا چاہیے، لیکن مخالف سمت میں کام کرتے ہوئے سابقہ کی تکمیل کرتا ہے۔ یہ عام کرنے کی اجازت دیتا ہے، یعنی۔ سیاق و سباق میں پابند نہ ہونے والے مونوٹائپ متغیرات کی مقدار طے کرنا۔ مندرجہ ذیل دو مثالیں قاعدے کے نظام کو عملی جامہ پہناتی ہیں۔ چونکہ اظہار اور قسم دونوں دیئے گئے ہیں، اس لیے وہ قواعد کا ٹائپ چیکنگ استعمال ہیں۔ مثال: کہاں، لکھا جا سکتا ہے اس کا ثبوت مثال: عمومی کاری کو ظاہر کرنے کے لیے، ذیل میں دکھایا گیا ہے: چلو پولیمرفزم فوری طور پر نظر نہیں آتا، قاعدہ سیٹ ایک ضابطے کو انکوڈ کرتا ہے جس کے تحت کسی قسم کو عام کیا جا سکتا ہے یا قواعد میں مونو-اور پولی ٹائپز کے قدرے مختلف استعمال سے نہیں۔ اسے یاد رکھیں اور بالترتیب پولی اور مونوٹائپ کی نشاندہی کریں۔ اصول میں، فنکشن کے پیرامیٹر کی ویلیو متغیر کو بنیاد کے ذریعے مونومورفک قسم کے ساتھ سیاق و سباق میں شامل کیا جاتا ہے، جبکہ اصول میں، متغیر ماحول میں پولیمرفک شکل میں داخل ہوتا ہے۔ اگرچہ دونوں صورتوں میں سیاق و سباق میں کی موجودگی تفویض میں کسی بھی آزاد متغیر کے لیے عمومی اصول کے استعمال کو روکتی ہے، یہ ضابطہ ایک-اظہار میں پیرامیٹر کی قسم کو مونومورفک رہنے پر مجبور کرتا ہے، جبکہ لیٹ-اظہار میں، متغیر کو متعارف کرایا جا سکتا ہے۔ پولیمورفک، تخصصات کو ممکن بناتے ہوئے۔ اس ضابطے کے نتیجے میں، ٹائپ نہیں کیا جا سکتا، کیونکہ پیرامیٹر مونومورفک پوزیشن میں ہے، جبکہ ٹائپ ہے، کیونکہ اسے لیٹ ایکسپریشن میں متعارف کرایا گیا ہے اور اس لیے اسے پولیمرفک سمجھا جاتا ہے۔ عمومی اصول عمومی اصول بھی قریب سے دیکھنے کے قابل ہے۔ یہاں، بنیاد میں مضمر تمام مقدار کو محض نتیجہ میں دائیں ہاتھ کی طرف منتقل کیا جاتا ہے۔ یہ ممکن ہے، کیونکہ یہ سیاق و سباق میں آزادانہ طور پر نہیں ہوتا ہے۔ ایک بار پھر، اگرچہ یہ عمومی اصول کو قابل فہم بناتا ہے، لیکن یہ واقعی کوئی نتیجہ نہیں ہے۔ اس کے برعکس، عام کرنے کا قاعدہ ایچ ایم کے ٹائپ سسٹم کی تعریف کا حصہ ہے اور اس کے نتیجے میں تمام مقدار کا مضمر ہے۔ ایک انفریشن الگورتھم اب جب کہ ایچ ایم کا کٹوتی کا نظام ہاتھ میں ہے، کوئی بھی الگورتھم پیش کر سکتا ہے اور قواعد کے حوالے سے اس کی توثیق کر سکتا ہے۔ متبادل طور پر، اس پر گہری نظر ڈال کر اسے حاصل کرنا ممکن ہو سکتا ہے کہ قواعد کس طرح تعامل کرتے ہیں اور ثبوت تشکیل پاتے ہیں۔ یہ اس مضمون کے بقیہ حصے میں کیا گیا ہے جس میں ٹائپنگ کو ثابت کرتے ہوئے ممکنہ فیصلوں پر توجہ دی گئی ہے۔ ڈگری آف فریڈم قواعد کا انتخاب ایک ثبوت میں نکات کو الگ کرنا، جہاں کوئی فیصلہ بالکل ممکن نہیں ہے، نحو کے ارد گرد مرکوز قواعد کا پہلا گروپ کوئی چارہ نہیں چھوڑتا ہے کیونکہ ہر نحو اصول ٹائپنگ کے ایک منفرد اصول سے مطابقت رکھتا ہے، جو ثبوت کے ایک حصے کا تعین کرتا ہے، جبکہ ان فکسڈ پارٹس کی زنجیروں کے اختتام اور احاطے کے درمیان اور ہو سکتا ہے۔ اس طرح کا سلسلہ ثبوت کے اختتام اور اعلی ترین اظہار کے اصول کے درمیان بھی موجود ہو سکتا ہے۔ تمام ثبوتوں کی اس طرح کی خاکہ شدہ شکل ہونی چاہیے۔ چونکہ قاعدے کے انتخاب کے حوالے سے ثبوت میں واحد انتخاب اور زنجیر ہے، اس لیے ثبوت کی شکل اس سوال کو ظاہر کرتی ہے کہ کیا اسے مزید درست بنایا جا سکتا ہے، جہاں ان زنجیروں کی ضرورت نہیں ہو سکتی۔ یہ حقیقت میں ممکن ہے اور اس طرح کے قواعد کے بغیر قواعد کے نظام کی ایک قسم کی طرف جاتا ہے۔ نحو ہدایت والا قاعدہ نظام ایچ ایم کا ایک عصری علاج کلیمنٹ کی وجہ سے ایک درمیانی مرحلے کے طور پر خالصتا نحو ہدایت والا قاعدہ نظام استعمال کرتا ہے۔ اس نظام میں، تخصص براہ راست اصل اصول کے بعد واقع ہوتی ہے اور اس میں ضم ہو جاتی ہے، جبکہ عمومی اصول کا حصہ بن جاتا ہے۔ وہاں عمومی کاری کا تعین بھی فنکشن کو متعارف کروا کر ہمیشہ سب سے عام قسم پیدا کرنے کے لیے کیا جاتا ہے، جو پابند نہ ہونے والے تمام مونوٹائپ متغیرات کی مقدار طے کرتا ہے۔ رسمی طور پر، اس بات کی توثیق کرنے کے لیے کہ یہ نیا قاعدہ نظام اصل کے مساوی ہے، کسی کو یہ دکھانا پڑتا ہے، جو دو ذیلی ثبوتوں میں تحلیل ہو جاتا ہے: (مستقل مزاجی) (تکمیل) اگرچہ مستقل مزاجی کو اصولوں کو تحلیل کرکے اور ثبوتوں میں دیکھا جا سکتا ہے، یہ ممکنہ طور پر نظر آتا ہے جو نامکمل ہے، جیسا کہ کوئی مثال کے طور پر نہیں دکھا سکتا، لیکن صرف۔ مکملتا کا صرف تھوڑا سا کمزور ورژن قابل ثبوت ہے، حالانکہ اس کا مطلب یہ ہے کہ آخر میں ثبوت کو عام کرنے کی اجازت دینے میں ایک اظہار کے لیے بنیادی قسم حاصل کی جا سکتی ہے۔ موازنہ کرنا اور، اب تمام اصولوں کے فیصلوں میں صرف مونوٹائپ ظاہر ہوتے ہیں۔ مزید برآں، کٹوتی کے نظام کے ساتھ کسی بھی ممکنہ ثبوت کی شکل اب اظہار کی شکل سے ملتی جلتی ہے (دونوں کو درختوں کے طور پر دیکھا جاتا ہے)۔ اس طرح اظہار ثبوت کی شکل کا مکمل طور پر تعین کرتا ہے۔ شکل میں ممکنہ طور پر اور کے علاوہ تمام اصولوں کے حوالے سے طے کیا جائے گا، جو دوسرے نوڈس کے درمیان من مانی طور پر لمبی شاخیں (زنجیروں) بنانے کی اجازت دیتے ہیں۔ اصولوں کو فوری طور پر تسلیم کرنے والی ڈگریاں اب جب کہ ثبوت کی شکل معلوم ہو چکی ہے، کوئی بھی پہلے سے ہی ایک قسم کے تخمینہ الگورتھم کی تشکیل کے قریب ہے۔ چونکہ کسی دیئے گئے اظہار کے لیے کسی بھی ثبوت کی شکل ایک جیسی ہونی چاہیے، اس لیے کوئی بھی ثبوت کے فیصلوں میں مونوٹائپ کو غیر متعین قرار دے سکتا ہے اور ان کا تعین کرنے کے طریقے پر غور کر سکتا ہے۔ یہاں، متبادل (تخصص) آرڈر عمل میں آتا ہے۔ اگرچہ پہلی نظر میں کوئی مقامی طور پر اقسام کا تعین نہیں کر سکتا، لیکن امید یہ ہے کہ پروف ٹری کو عبور کرتے ہوئے آرڈر کی مدد سے ان کو بہتر بنانا ممکن ہے، اس کے علاوہ یہ فرض کرتے ہوئے کہ نتیجے میں الگورتھم ایک تخمینہ طریقہ بننے والا ہے، کہ کسی بھی بنیاد میں قسم کا تعین بہترین ممکنہ طور پر کیا جائے گا۔ اور درحقیقت، جیسا کہ اصولوں کو دیکھتے ہوئے کہا جا سکتا ہے:: اہم انتخاب ہے۔ اس وقت، اس کے بارے میں کچھ بھی معلوم نہیں ہے، لہذا کوئی صرف سب سے عام قسم کو فرض کر سکتا ہے، جو کہ ہے۔ منصوبہ یہ ہے کہ اگر ضروری ہو تو اس قسم کو مہارت دی جائے۔ بدقسمتی سے، اس جگہ پر پولی ٹائپ کی اجازت نہیں ہے، لہذا کچھ کو فی الحال کرنا پڑتا ہے۔ ناپسندیدہ گرفتاریوں سے بچنے کے لیے، ایک قسم کا متغیر جو ابھی تک ثبوت میں نہیں ہے ایک محفوظ انتخاب ہے۔ مزید برآں، یہ بات ذہن میں رکھنی ہوگی کہ یہ مونوٹائپ ابھی طے نہیں ہوا ہے، لیکن اسے مزید بہتر بنایا جا سکتا ہے۔ : انتخاب یہ ہے کہ کس طرح بہتر بنایا جائے۔ کیونکہ یہاں کسی بھی قسم کا انتخاب متغیر کے استعمال پر منحصر ہے، جو مقامی طور پر معلوم نہیں ہے، سب سے محفوظ شرط سب سے عام ہے۔ اوپر کی طرح ایک ہی طریقہ استعمال کرتے ہوئے تمام مقداری متغیرات کو تازہ مونوٹائپ متغیرات کے ساتھ فوری طور پر ظاہر کیا جا سکتا ہے، اور انہیں مزید اصلاح کے لیے کھلا رکھا جا سکتا ہے۔ : قاعدہ کوئی چارہ نہیں چھوڑتا۔ ہو گیا۔ : صرف درخواست کا قاعدہ اب تک "کھلے" متغیرات کو بہتر بنانے پر مجبور کر سکتا ہے، جیسا کہ دونوں احاطوں کی ضرورت ہے۔ پہلی بنیاد نتیجے کے نتیجے کو شکل کا ہونے پر مجبور کرتی ہے۔ اگر ایسا ہے تو ٹھیک ہے۔ بعد میں نتیجہ کے لیے اس کا انتخاب کیا جا سکتا ہے۔ اگر نہیں، تو یہ ایک کھلا متغیر ہو سکتا ہے۔ پھر اسے پہلے کی طرح دو نئے متغیرات کے ساتھ مطلوبہ شکل میں بہتر بنایا جا سکتا ہے۔ بصورت دیگر، ٹائپ چیکنگ ناکام ہوجاتی ہے کیونکہ پہلی بنیاد نے ایک ایسی قسم کا اندازہ لگایا جو فنکشن ٹائپ میں نہیں ہے اور نہ ہی بنایا جا سکتا ہے۔ دوسری بنیاد کے لیے ضروری ہے کہ قیاس شدہ قسم پہلی بنیاد کے برابر ہو۔ اب دو ممکنہ طور پر مختلف اقسام ہیں، شاید کھلی قسم کے متغیرات کے ساتھ، موازنہ کرنے اور اگر ممکن ہو تو مساوی بنانے کے لیے۔ اگر ایسا ہے تو، ایک اصلاح پائی جاتی ہے، اور اگر نہیں، تو ایک قسم کی غلطی کا دوبارہ پتہ چلا ہے۔ ایک موثر طریقہ متبادل کے ذریعے "دو اصطلاحات کو برابر بنانے" کے لیے جانا جاتا ہے، رابنسن کا اتحاد نام نہاد یونین فائنڈ الگورتھم کے ساتھ مل کر۔ یونین فائنڈ الگورتھم کا مختصر خلاصہ پیش کرنے کے لیے، ثبوت میں تمام اقسام کے سیٹ کو دیکھتے ہوئے، یہ کسی کو ایک طریقہ کار کے ذریعے مساوات کی کلاسوں میں اکٹھا کرنے اور طریقہ کار کا استعمال کرتے ہوئے ایسی ہر کلاس کے لیے ایک نمائندہ منتخب کرنے کی اجازت دیتا ہے۔ ضمنی اثر کے معنی میں لفظ کے طریقہ کار پر زور دیتے ہوئے، ہم واضح طور پر ایک موثر الگورتھم تیار کرنے کے لیے منطق کے دائرے کو چھوڑ رہے ہیں۔ a کے نمائندے کا تعین اس طرح کیا جاتا ہے کہ، اگر دونوں اور قسم کے متغیر ہیں تو نمائندہ من مانی طور پر ان میں سے ایک ہے، لیکن متغیر اور اصطلاح کو متحد کرتے ہوئے، اصطلاح نمائندہ بن جاتی ہے۔ ہاتھ میں یونین فائنڈ کے نفاذ کو فرض کرتے ہوئے، کوئی بھی دو مونوٹائپز کے اتحاد کو مندرجہ ذیل طریقے سے تشکیل دے سکتا ہے: متحد کریں (ta, tb): ta = تلاش کریں (ta) tb = تلاش کریں (tb) اگر دونوں ta، tb یکساں D، n کے ساتھ فارم D p1.pn کی اصطلاحات ہیں تو پھر ہر متعلقہ ith پیرامیٹر کے لیے متحد کریں (ta [i]، tb [i]) بصورت دیگر اگر ta، tb میں سے کم از کم ایک ٹائپ متغیر ہے تو یونین (ta, tb) بصورت دیگر غلطی کی اقسام میل نہیں کھاتی ہیں 'اب ہاتھ میں ایک انفریشن الگورتھم کا خاکہ ہونے کی وجہ سے، اگلے حصے میں زیادہ رسمی پیشکش دی گئی ہے۔ اسے ملنر پی۔ 370 ایف ایف میں بیان کیا گیا ہے۔ الگورتھم جے۔ الگورتھم جے کی پیشکش منطقی اصولوں کے اشارے کا غلط استعمال ہے، کیونکہ اس میں مضر اثرات شامل ہیں لیکن ایک ہی وقت میں موثر نفاذ کا اظہار کرتے ہوئے اس کے ساتھ براہ راست موازنہ کرنے کی اجازت دیتا ہے۔ قواعد اب ایک طریقہ کار کی وضاحت کرتے ہیں جس کے پیرامیٹرز اس نتیجے پر پہنچتے ہیں جہاں احاطے کا نفاذ بائیں سے دائیں طرف ہوتا ہے۔ یہ طریقہ کار اصطلاح کو نقل کرکے اور باؤنڈ ٹائپ متغیرات کو مستقل طور پر نئے مونوٹائپ متغیرات سے تبدیل کرکے پولی ٹائپ کی مہارت رکھتا ہے۔ ایک نیا مونوٹائپ متغیر پیدا کرتا ہے۔ ممکنہ طور پر، ناپسندیدہ گرفتاریوں سے بچنے کے لیے مقدار کے لیے نئے متغیرات متعارف کرانے کی قسم کو کاپی کرنا پڑتا ہے۔ مجموعی طور پر، الگورتھم اب ہمیشہ سب سے عام انتخاب کرتے ہوئے آگے بڑھتا ہے جس میں تخصص کو اتحاد پر چھوڑ دیا جاتا ہے، جو خود ہی سب سے عام نتیجہ پیدا کرتا ہے۔ جیسا کہ اوپر بیان کیا گیا ہے، کسی دیے گئے اظہار کے لیے سب سے عام قسم حاصل کرنے کے لیے حتمی نتیجہ کو آخر میں عام کرنا پڑتا ہے۔ چونکہ الگورتھم میں استعمال ہونے والے طریقہ کار کی لاگت تقریبا O (1) ہوتی ہے، اس لیے الگورتھم کی مجموعی لاگت اظہار کے سائز میں لکیری کے قریب ہوتی ہے جس کے لیے ایک قسم کا اندازہ لگایا جانا ہے۔ یہ ٹائپ انفریشن الگورتھم حاصل کرنے کی بہت سی دوسری کوششوں کے بالکل برعکس ہے، جو اکثر این پی-ہارڈ ثابت ہوتے ہیں، اگر ختم کرنے کے حوالے سے ناقابل فیصلہ نہیں ہوتے ہیں۔ اس طرح ایچ ایم بہترین کارکردگی کے ساتھ ساتھ مکمل طور پر باخبر ٹائپ چیکنگ الگورتھم انجام دے سکتا ہے۔ یہاں ٹائپ چیک کرنے کا مطلب یہ ہے کہ الگورتھم کو ثبوت تلاش کرنے کی ضرورت نہیں ہے، بلکہ صرف کسی دیے گئے کی توثیق کرنے کی ضرورت ہے۔ کارکردگی کو قدرے کم کیا جاتا ہے کیونکہ سیاق و سباق میں ٹائپ متغیرات کی بائنڈنگ کو برقرار رکھنا پڑتا ہے تاکہ حساب کی اجازت دی جا سکے اور اس دوران تکراری اقسام کی تعمیر کو روکنے کے لیے ایک واقع چیک کو فعال کیا جا سکے۔ اس طرح کے معاملے کی ایک مثال ہے، جس کے لیے ایچ ایم کا استعمال کرتے ہوئے کوئی قسم حاصل نہیں کی جا سکتی۔ عملی طور پر، اقسام صرف چھوٹی اصطلاحات ہیں اور توسیع پذیر ڈھانچے کی تعمیر نہیں کرتی ہیں۔ اس طرح، پیچیدگی کے تجزیے میں، کوئی بھی ان کا موازنہ مستقل، O (1) لاگت کو برقرار رکھنے کے طور پر کر سکتا ہے۔ الگورتھم کو ثابت کرنا پچھلے حصے میں، الگورتھم کو خاکہ بناتے وقت اس کے ثبوت کو دھاتی استدلال کے ساتھ اشارہ کیا گیا تھا۔ اگرچہ یہ ایک موثر الگورتھم J کی طرف لے جاتا ہے، لیکن یہ واضح نہیں ہے کہ آیا الگورتھم کٹوتی کے نظام D یا S کی مناسب عکاسی کرتا ہے جو سیمنٹک بیس لائن کے طور پر کام کرتا ہے۔ مندرجہ بالا دلیل میں سب سے اہم نقطہ سیاق و سباق سے منسلک مونوٹائپ متغیرات کی اصلاح ہے۔ مثال کے طور پر، الگورتھم دلیری سے سیاق و سباق کو تبدیل کرتا ہے جبکہ مثال کے طور پر۔ ، کیونکہ پیرامیٹر کے سیاق و سباق میں شامل کیے گئے مونوٹائپ متغیر کو بعد میں ایپلی کیشن کو سنبھالتے وقت بہتر بنانے کی ضرورت ہے۔ مسئلہ یہ ہے کہ کٹوتی کے قوانین اس طرح کی اصلاح کی اجازت نہیں دیتے ہیں۔ یہ استدلال کرنا کہ بہتر قسم کو مونوٹائپ متغیر کے بجائے پہلے شامل کیا جا سکتا تھا، سب سے بہتر ہے۔ رسمی طور پر تسلی بخش دلیل تک پہنچنے کی کلید یہ ہے کہ سیاق و سباق کو اصلاح کے اندر مناسب طریقے سے شامل کیا جائے۔ رسمی طور پر ٹائپنگ فری ٹائپ متغیرات کے متبادل کے ساتھ مطابقت رکھتی ہے۔ اس طرح آزاد متغیرات کو بہتر بنانے کا مطلب پوری ٹائپنگ کو بہتر بنانا ہے۔ الگورتھم ڈبلیو وہاں سے، الگورتھم جے کا ثبوت الگورتھم ڈبلیو کی طرف جاتا ہے، جو صرف اس کے سیریل کمپوزیشن کو متبادلات کے ذریعے ظاہر کرکے طریقہ کار کے ذریعہ عائد کردہ ضمنی اثرات کو واضح کرتا ہے۔ سائڈ بار میں الگورتھم ڈبلیو کی پیشکش اب بھی اٹالک میں سیٹ کی گئی کارروائیوں میں ضمنی اثرات کا استعمال کرتی ہے، لیکن یہ اب تازہ علامتیں پیدا کرنے تک محدود ہیں۔ فیصلے کی شکل یہ ہے کہ کسی فنکشن کو سیاق و سباق اور اظہار کے ساتھ پیرامیٹر کے طور پر ظاہر کیا جاتا ہے جو متبادل کے ساتھ مل کر ایک مونوٹائپ تیار کرتا ہے۔ متبادل تیار کرنے کا ایک ضمنی اثر سے پاک ورژن ہے جو سب سے عام یونیفائر ہے۔ اگرچہ الگورتھم ڈبلیو کو عام طور پر ایچ ایم الگورتھم سمجھا جاتا ہے اور اسے اکثر ادب میں قاعدے کے نظام کے بعد براہ راست پیش کیا جاتا ہے، اس کا مقصد ملنر نے پی 369 پر اس طرح بیان کیا ہے: جیسا کہ یہ کھڑا ہے، ڈبلیو شاید ہی ایک موثر الگورتھم ہے۔ متبادل کا اطلاق اکثر ہوتا ہے۔ اسے مضبوطی کے ثبوت میں مدد کے لیے وضع کیا گیا تھا۔ اب ہم ایک آسان الگورتھم J پیش کرتے ہیں جو درست معنوں میں W کی تقلید کرتا ہے۔ اگرچہ وہ ڈبلیو کو زیادہ پیچیدہ اور کم موثر سمجھتے تھے، لیکن انہوں نے اسے جے کے سامنے اپنی اشاعت میں پیش کیا۔ جب ضمنی اثرات دستیاب نہیں ہوتے یا ناپسندیدہ ہوتے ہیں تو اس کی خوبیاں ہوتی ہیں۔ مکمل ہونے کو ثابت کرنے کے لیے بھی W کی ضرورت ہوتی ہے، جسے اس نے ساؤنڈنیس پروف میں شامل کیا ہے۔ ثبوت کی ذمہ داریوں کو مرتب کرنے سے پہلے، ڈی اور ایس کے قواعد کے نظام اور پیش کردہ الگورتھم کے درمیان انحراف پر زور دینے کی ضرورت ہے۔ اگرچہ اوپر کی ترقی نے مونوٹائپز کو "اوپن" پروف متغیرات کے طور پر غلط استعمال کیا، لیکن اس امکان کو کہ مناسب مونوٹائپ متغیرات کو نقصان پہنچا سکتا ہے، تازہ متغیرات کو متعارف کروا کر اور بہترین کی امید کر کے اس سے گریز کیا گیا۔ لیکن ایک پکڑ ہے: کیے گئے وعدوں میں سے ایک یہ تھا کہ ان تازہ متغیرات کو "ذہن میں رکھا جائے گا"۔ یہ وعدہ الگورتھم کے ذریعے پورا نہیں ہوتا ہے۔ سیاق و سباق ہونے کی وجہ سے، اظہار کو یا تو ٹائپ نہیں کیا جا سکتا، لیکن الگورتھم اس قسم کے ساتھ آتا ہے، جہاں W اضافی طور پر متبادل فراہم کرتا ہے، جس کا مطلب ہے کہ الگورتھم تمام قسم کی غلطیوں کا پتہ لگانے میں ناکام رہتا ہے۔ اس کمی کو زیادہ احتیاط سے ثبوت متغیرات اور مونوٹائپ متغیرات میں فرق کرکے آسانی سے طے کیا جا سکتا ہے۔ مصنفین اس مسئلے سے بخوبی واقف تھے لیکن انہوں نے اسے حل نہ کرنے کا فیصلہ کیا۔ اس کے پیچھے کوئی عملی وجہ فرض کی جا سکتی ہے۔ اگرچہ ٹائپ انفریشن کو زیادہ مناسب طریقے سے لاگو کرنے سے الگورتھم تجریدی مونوٹائپز سے نمٹنے کے قابل ہوتا، لیکن ان کی مطلوبہ ایپلی کیشن کے لیے ضرورت نہیں تھی جہاں پہلے سے موجود سیاق و سباق میں کسی بھی آئٹم میں فری متغیر نہ ہوں۔ اس روشنی میں، غیر ضروری پیچیدگی کو ایک آسان الگورتھم کے حق میں چھوڑ دیا گیا۔ باقی منفی پہلو یہ ہے کہ قاعدہ نظام کے حوالے سے الگورتھم کا ثبوت کم عام ہے اور اسے صرف ضمنی حالت کے ساتھ سیاق و سباق کے لیے بنایا جا سکتا ہے۔ مکمل ذمہ داری میں سائیڈ کنڈیشن اس بات سے خطاب کرتی ہے کہ کٹوتی کس طرح کئی اقسام دے سکتی ہے، جبکہ الگورتھم ہمیشہ ایک پیدا کرتا ہے۔ ایک ہی وقت میں، سائیڈ کنڈیشن کا مطالبہ ہے کہ جس قسم کا اندازہ لگایا گیا ہے وہ دراصل سب سے زیادہ عام ہے۔ ذمہ داریوں کو صحیح طریقے سے ثابت کرنے کے لیے سب سے پہلے انہیں مضبوط کرنے کی ضرورت ہے تاکہ متبادل لیما کو فعال کرنے کی اجازت دی جا سکے جس کے ذریعے متبادل کو تھریڈ کیا جا سکے۔ وہاں سے، ثبوت اظہار پر انڈکشن کے ذریعے ہوتے ہیں۔ ایک اور ثبوت کی ذمہ داری خود متبادل لیما ہے، یعنی۔ ٹائپنگ کا متبادل، جو آخر میں تمام مقدار کو قائم کرتا ہے۔ مؤخر الذکر کو باضابطہ طور پر ثابت نہیں کیا جا سکتا، کیونکہ اس طرح کا کوئی نحو موجود نہیں ہے۔ توسیعات تکراری تعریفیں پروگرامنگ کو عملی تکراری افعال بنانے کے لیے ضروری ہیں۔ لیمبڈا کیلکولس کی ایک مرکزی خاصیت یہ ہے کہ تکراری تعریفیں براہ راست دستیاب نہیں ہیں، بلکہ اس کے بجائے ایک فکسڈ پوائنٹ کمبینٹر کے ساتھ اظہار کیا جا سکتا ہے۔ لیکن بدقسمتی سے، فکس پوائنٹ کمبینٹر کو لیمبڈا کیلکولس کے ٹائپ شدہ ورژن میں تشکیل نہیں دیا جا سکتا جس کا نظام پر تباہ کن اثر پڑے جیسا کہ ذیل میں بیان کیا گیا ہے۔ ٹائپنگ رول اصل کاغذ سے پتہ چلتا ہے کہ ریکرشن کو کمبینٹر کے ذریعے محسوس کیا جا سکتا ہے۔ اس طرح ایک ممکنہ تکراری تعریف اس طرح وضع کی جا سکتی ہے۔ متبادل طور پر اظہار نحو کی توسیع اور ایک اضافی ٹائپنگ اصول ممکن ہے: جہاں بنیادی طور پر ضم ہوتا ہے اور مونوٹائپ پوزیشنوں میں بار بار بیان کردہ متغیرات کو شامل کرتے ہوئے جہاں وہ بائیں طرف ہوتے ہیں لیکن اس کے دائیں طرف پولی ٹائپ کے طور پر ہوتے ہیں۔ نتائج اگرچہ مذکورہ بالا سیدھے سادے ہیں لیکن یہ ایک قیمت پر آتے ہیں۔ ٹائپ تھیوری لیمبڈا کیلکولس کو کمپیوٹیشن اور منطق سے جوڑتی ہے۔ مندرجہ بالا آسان ترمیم کا دونوں پر اثر پڑتا ہے: مضبوط نارملائزیشن پراپرٹی کو کالعدم قرار دیا گیا ہے، کیونکہ غیر اختتامی شرائط وضع کی جا سکتی ہیں۔ منطق ختم ہو جاتی ہے کیونکہ قسم آباد ہو جاتی ہے۔ اوور لوڈنگ کا مطلب ہے کہ مختلف افعال کی وضاحت کی جا سکتی ہے اور ایک ہی نام کے ساتھ استعمال کیا جا سکتا ہے۔ زیادہ تر پروگرامنگ زبانیں کم از کم بلٹ ان ریاضی کی کارروائیوں (+، <، وغیرہ) کے ساتھ اوور لوڈنگ فراہم کرتی ہیں۔ )، پروگرامر کو ایک ہی شکل میں ریاضی کے تاثرات لکھنے کی اجازت دینے کے لیے، یہاں تک کہ مختلف عددی اقسام جیسے انٹ یا ریئل کے لیے بھی۔ کیونکہ ایک ہی اظہار کے اندر ان مختلف اقسام کا مرکب بھی مضمر تبدیلی کا مطالبہ کرتا ہے، خاص طور پر ان کارروائیوں کے لیے اوور لوڈنگ اکثر پروگرامنگ زبان میں ہی بنائی جاتی ہے۔ کچھ زبانوں میں، اس خصوصیت کو عام کیا جاتا ہے اور صارف کو دستیاب کرایا جاتا ہے، مثال کے طور پر۔ C + + میں۔ اگرچہ فنکشنل پروگرامنگ میں ٹائپ چیکنگ اور انفریشن دونوں میں کمپیوٹیشن کے اخراجات کے لیے ایڈہاک اوورلوڈنگ سے گریز کیا گیا ہے، لیکن اوورلوڈنگ کو منظم کرنے کا ایک ذریعہ متعارف کرایا گیا ہے جو شکل اور نام دونوں میں آبجیکٹ پر مبنی پروگرامنگ سے ملتا جلتا ہے، لیکن ایک سطح سے اوپر کی طرف کام کرتا ہے۔ اس نظام میں "مثالیں" اشیاء نہیں ہیں (یعنی۔ قدر کی سطح پر)، بلکہ اقسام۔ تعارف میں مذکور فوری ترتیب کی مثال آرڈرز میں اوور لوڈنگ کا استعمال کرتی ہے، جس میں ہاسکل میں درج ذیل قسم کی تشریح ہوتی ہے: فوری ترتیب:: آرڈ a => [a]-> [a] یہاں، قسم a نہ صرف پولیمورفک ہے، بلکہ کسی قسم کی کلاس آرڈ کی مثال تک محدود ہے، جو فنکشنز باڈی میں استعمال ہونے والی ترتیب پیش گوئی فراہم کرتی ہے۔ ان پیش گوئیوں کے مناسب نفاذ کو اضافی پیرامیٹرز کے طور پر کوئکسورٹس کو منتقل کیا جاتا ہے، جیسے ہی زیادہ ٹھوس اقسام پر کوئکسورٹ کا استعمال کیا جاتا ہے جو اوورلوڈڈ فنکشن کوئیکسورٹ کا واحد نفاذ فراہم کرتا ہے۔ چونکہ "کلاسز" صرف ایک ہی قسم کو اپنی دلیل کے طور پر اجازت دیتے ہیں، اس کے نتیجے میں آنے والا قسم کا نظام اب بھی اندازہ فراہم کر سکتا ہے۔ مزید برآں، ٹائپ کلاسوں کو پھر کسی قسم کے اوور لوڈنگ آرڈر سے لیس کیا جا سکتا ہے جس سے کلاسوں کو جالی کے طور پر ترتیب دیا جا سکتا ہے۔ اعلی درجے کی اقسام پیرامیٹرک پولیمرفزم کا مطلب یہ ہے کہ اقسام کو خود پیرامیٹرز کے طور پر منتقل کیا جاتا ہے جیسے کہ وہ مناسب اقدار ہوں۔ کسی مناسب فنکشن کے لیے دلائل کے طور پر پاس کیا جاتا ہے، بلکہ "پیرامیٹرک" قسم کے مستقلات کی طرح "ٹائپ فنکشنز" میں بھی، اس سوال کی طرف لے جاتا ہے کہ خود کو زیادہ مناسب طریقے سے ٹائپ کیسے کیا جائے۔ اعلی درجے کی اقسام کو اس سے بھی زیادہ اظہار خیال کا نظام بنانے کے لیے استعمال کیا جاتا ہے۔ بدقسمتی سے، اتحاد اب میٹا اقسام کی موجودگی میں فیصلہ کن نہیں ہے، جس سے عام طور پر اس توسیع میں قسم کا اندازہ لگانا ناممکن ہے۔ مزید برآں، ہر قسم کی ایک قسم کو فرض کرتے ہوئے جو خود کو ایک قسم کے طور پر شامل کرتی ہے وہ ایک تضاد کی طرف لے جاتی ہے، جیسا کہ تمام سیٹوں کے سیٹ میں ہوتا ہے، لہذا کسی کو تجریدی سطح کے مراحل میں آگے بڑھنا چاہیے۔ سیکنڈ آرڈر لیمبڈا کیلکولس میں تحقیق، ایک قدم اوپر کی طرف، سے پتہ چلتا ہے کہ اس قسم کا تخمینہ اس عامیت میں ناقابل فیصلہ ہے۔ ایک اضافی سطح کے حصوں کو ہاسکل نامی قسم میں متعارف کرایا گیا ہے، جہاں اسے موناڈ ٹائپ کرنے میں مدد کے لیے استعمال کیا جاتا ہے۔ اقسام کو مضمر چھوڑ دیا جاتا ہے، جو توسیعی قسم کے نظام کے اندرونی میکانکس میں پردے کے پیچھے کام کرتے ہیں۔ سب ٹائپنگ سب ٹائپنگ اور ٹائپ انفریشن کو یکجا کرنے کی کوششوں نے کافی مایوسی کا باعث بنا ہے۔ ذیلی ٹائپنگ کی رکاوٹوں کو جمع کرنا اور ان کی تشہیر کرنا سیدھا ہے (ٹائپ مساوات کی رکاوٹوں کے برخلاف)، جس کے نتیجے میں آنے والی رکاوٹوں کو قیاس شدہ ٹائپنگ اسکیموں کا حصہ بناتا ہے، مثال کے طور پر، جہاں ٹائپ متغیر پر رکاوٹ ہے۔ تاہم، چونکہ ٹائپ متغیرات اب اس نقطہ نظر میں بے تابی سے متحد نہیں ہیں، اس لیے یہ بہت سے بیکار قسم کے متغیرات اور رکاوٹوں پر مشتمل بڑی اور بھاری ٹائپنگ اسکیمیں پیدا کرتا ہے، جس سے انہیں پڑھنا اور سمجھنا مشکل ہو جاتا ہے۔ لہذا، اس طرح کی ٹائپنگ اسکیموں اور ان کی رکاوٹوں کو آسان بنانے کے لیے کافی کوشش کی گئی، جس میں غیر متعین محدود آٹومیٹن (این ایف اے) کی آسان کاری (قیاس شدہ تکراری اقسام کی موجودگی میں مفید) جیسی تکنیکوں کا استعمال کیا گیا۔ ابھی حال ہی میں، ڈولن اور مائکرافٹ نے ٹائپنگ اسکیم کو آسان بنانے اور این ایف اے کو آسان بنانے کے درمیان تعلقات کو باقاعدہ بنایا اور یہ ظاہر کیا کہ ذیلی ٹائپنگ کو باضابطہ بنانے پر الجبرائی عمل نے ایم ایل جیسی زبان (جسے ایم ایل سب کہا جاتا ہے) کے لیے کمپیکٹ پرنسپل ٹائپنگ اسکیمیں تیار کرنے کی اجازت دی۔ خاص طور پر، ان کی مجوزہ ٹائپنگ اسکیم میں واضح رکاوٹوں کے بجائے یونین اور چوراہے کی اقسام کی ایک محدود شکل کا استعمال کیا گیا۔ پیررو نے بعد میں دعوی کیا کہ یہ الجبرائی تشکیل الگورتھم ڈبلیو سے مشابہت رکھنے والے نسبتا سادہ الگورتھم کے مساوی تھی، اور یہ کہ اتحاد اور چوراہے کی اقسام کا استعمال ضروری نہیں تھا۔ دوسری طرف، آبجیکٹ پر مبنی پروگرامنگ زبانوں کے تناظر میں ٹائپ انفریشن زیادہ مشکل ثابت ہوا ہے، کیونکہ آبجیکٹ طریقوں کو سسٹم ایف کے انداز میں فرسٹ کلاس پولیمرفزم کی ضرورت ہوتی ہے (جہاں ٹائپ انفریشن ناقابل فیصلہ ہے) اور ایف باؤنڈڈ پولیمرفزم جیسی خصوصیات کی وجہ سے۔ نتیجتا، سب ٹائپنگ کے ساتھ آبجیکٹ پر مبنی پروگرامنگ کو فعال کرنے والے ٹائپ سسٹم، جیسے کارڈلی کا سسٹم، ایچ ایم طرز کی قسم کے تخمینے کی حمایت نہیں کرتا ہے۔ ساختی ریکارڈز جیسی معاون زبان کی خصوصیات کے لیے ذیلی ٹائپنگ کے متبادل کے طور پر رو پولیمرفزم کا استعمال کیا جا سکتا ہے۔ اگرچہ پولیمرفزم کا یہ انداز کچھ طریقوں سے ذیلی ٹائپنگ سے کم لچکدار ہے، خاص طور پر قسم کی رکاوٹوں میں سمت کی کمی سے نمٹنے کے لیے سختی سے ضروری سے زیادہ پولیمرفزم کی ضرورت ہوتی ہے، لیکن اس کا فائدہ یہ ہے کہ اسے معیاری ایچ ایم الگورتھم کے ساتھ آسانی سے مربوط کیا جا سکتا ہے۔ نوٹ حوالہ جات بیرونی لنکس گٹ ہب پر اس کے سورس کوڈ کے ساتھ الگورتھم ڈبلیو کا ایک خواندہ ہاسکل نفاذ۔ ازگر میں ہندلے ملنر الگورتھم کا ایک آسان نفاذ۔ ٹائپ سسٹمز ٹائپ تھیوری ٹائپ انفریشن لیمبڈا کیلکولس نظریاتی کمپیوٹر سائنس رسمی طریقے 1969 کمپیوٹنگ میں 1978 کمپیوٹنگ میں 1985 کمپیوٹنگ الگورتھم میں