Critical pair (term rewriting)
[[فائل: کریٹ پیئر svg.svg |thumb |400px |Triangle ایک اہم جوڑے کا خاکہ جو دو دوبارہ لکھنے والے اصولوں s → t (اوپری صف، بائیں) اور l → r (دائیں) سے حاصل کیا گیا ہے۔ متبادل σ ذیلی اصطلاح s|p کو l کے ساتھ متحد کرتا ہے۔ اس کے نتیجے میں اوورلے کی اصطلاح sσ [lσ] p (نچلی صف، درمیانی) کو بالترتیب tσ اور sσ [rσ] p (نچلی صف، بائیں اور دائیں) کی اصطلاح میں دوبارہ لکھا جا سکتا ہے۔ مؤخر الذکر دو اصطلاحات تنقیدی جوڑی بناتی ہیں۔ انہیں بالآخر ایک مشترکہ اصطلاح میں دوبارہ لکھا جا سکتا ہے، اگر دوبارہ لکھنے کا قاعدہ سیٹ متصادم ہے۔] ایک تنقیدی جوڑا اصطلاح دوبارہ لکھنے کے نظام میں اس وقت پیدا ہوتا ہے جب دو دوبارہ لکھنے کے اصول دو مختلف اصطلاحات حاصل کرنے کے لیے اوورلیپ ہوتے ہیں۔ مزید تفصیل سے، (t1، t2) ایک اہم جوڑا ہے اگر کوئی اصطلاح t ہے جس کے لیے دوبارہ لکھنے کے اصول کی دو مختلف ایپلی کیشنز (یا تو ایک ہی اصول مختلف طریقے سے لاگو ہوتا ہے، یا دو مختلف اصول) اصطلاحات t1 اور t2 حاصل کرتے ہیں۔ تعریفیں ایک اہم جوڑے کی اصل تعریف قدرے زیادہ شامل ہے کیونکہ اس میں ایسے جوڑے شامل نہیں ہیں جو متبادل کے ذریعے اہم جوڑوں سے حاصل کیے جا سکتے ہیں اور جوڑے کو اوورلیپ کی بنیاد پر ترتیب دیتے ہیں۔ خاص طور پر، اوور لیپنگ قوانین کی ایک جوڑی کے لیے اور، اوور لیپ کے ساتھ کچھ غیر خالی سیاق و سباق کے لیے، اور اصطلاح (جو متغیر نہیں ہے) کچھ متبادلات کے تحت ملتی ہے جو سب سے زیادہ عام ہیں، اہم جوڑی ہے۔ جب اہم جوڑے کے دونوں اطراف ایک ہی اصطلاح تک کم ہو سکتے ہیں، تو اہم جوڑے کو کنورجنٹ کہا جاتا ہے۔ جہاں تنقیدی جوڑے کا ایک رخ دوسرے سے ملتا جلتا ہے، تنقیدی جوڑے کو ٹریوئل کہا جاتا ہے۔ مثال کے طور پر، دوبارہ لکھنے کے نظام کی اصطلاح میں قواعد کے ساتھ {|-| f (g (x, y), z) | | → g (x, z) |-| g (x, y) | | → x, |} واحد اہم جوڑا ±g (x, z), f (x, z) ω ہے۔ ان دونوں اصطلاحات کو ایک ہی دوبارہ لکھنے کے اصول کو لاگو کرکے اصطلاح f (g (x, y)، z) سے اخذ کیا جا سکتا ہے۔ ایک اور مثال کے طور پر، ایک ہی اصول {|-| f (x, y) | | → x کے ساتھ دوبارہ لکھنے کے نظام کی اصطلاح پر غور کریں۔ |-|} اس اصول کو اصطلاح f (f (x (x, x), x) پر دو مختلف طریقوں سے لاگو کرنے سے، ہم دیکھتے ہیں کہ (f (x (x, x), f (x, x)) ایک (معمولی) تنقیدی جوڑا ہے۔ کریٹیکل جوڑی لیما کنفلوینس واضح طور پر کنورجنٹ کریٹیکل جوڑوں کا اشارہ کرتی ہے: اگر کوئی کریٹیکل جوڑا अमلو اے، بی ایل او پیدا ہوتا ہے، تو اے اور بی میں ایک مشترکہ کمی ہوتی ہے اور اس طرح کریٹیکل جوڑا کنورجنٹ ہوتا ہے۔ اگر اصطلاح دوبارہ لکھنے کا نظام متزلزل نہیں ہے، تو اہم جوڑا یکجا نہیں ہوسکتا ہے، لہذا اہم جوڑے ممکنہ ذرائع ہیں جہاں سنگم ناکام ہو جائے گا۔ تنقیدی جوڑی لیما میں کہا گیا ہے کہ ایک اصطلاح دوبارہ لکھنے کا نظام کمزور ہے (یعنی۔ مقامی طور پر) کنفلوینٹ اگر اور صرف اس صورت میں جب تمام اہم جوڑے متغیر ہوں۔ اس طرح، یہ معلوم کرنے کے لیے کہ آیا کوئی اصطلاح دوبارہ لکھنے کا نظام کمزور طور پر متصل ہے، تمام اہم جوڑوں کی جانچ کرنا اور یہ دیکھنا کافی ہے کہ آیا وہ متغیر ہیں۔ اس سے الگورتھم کے لحاظ سے یہ معلوم کرنا ممکن ہو جاتا ہے کہ آیا کوئی اصطلاح دوبارہ لکھنے کا نظام کمزور طور پر متصل ہے یا نہیں، یہ دیکھتے ہوئے کہ کوئی الگورتھم کے لحاظ سے چیک کر سکتا ہے کہ آیا دو اصطلاحات یکجا ہوتی ہیں یا نہیں۔ نوتھ-بینڈیکس تکمیل بھی دیکھیں، ایک الگورتھم جو تنقیدی جوڑوں پر مبنی ہے جو ایک متصل اور اختتامی اصطلاح کے دوبارہ لکھنے کے نظام کا حساب لگانے کے لیے ہے جو ایک دیئے گئے بیرونی لنک کے مساوی ہے۔ حوالہ جات فرانز باڈر اور ٹوبیاس نپکو، اصطلاح دوبارہ لکھنا اور وہ سب، "کیمبرج یونیورسٹی پریس، 1998 (بک ویب لنک) دوبارہ لکھنے کے نظام