Algebraic semantics (computer science)
کمپیوٹر سائنس میں، الجبرائی سیمنٹکس رسمی انداز میں پروگرام کی خصوصیات کے بارے میں بیان کرنے اور استدلال کرنے کے لیے الجبرائی قوانین پر مبنی محوری سیمنٹکس کی ایک شکل ہے۔ الجبرائی تفصیلات کا نحو دو مراحل میں وضع کیا جاتا ہے: (1) اعداد و شمار کی اقسام اور عمل کی علامتوں کے رسمی دستخط کی وضاحت، اور (2) سیٹوں اور افعال کے ذریعے دستخط کی تشریح۔ دستخط کی تعریف الجبرائی تفصیلات کے دستخط اس کے رسمی نحو کی وضاحت کرتے ہیں۔ لفظ "دستخطی" موسیقی کے اشارے میں "کلیدی دستخط" کے تصور کی طرح استعمال ہوتا ہے۔ دستخط ڈیٹا کی اقسام کے ایک سیٹ پر مشتمل ہوتا ہے، جسے اقسام کے نام سے جانا جاتا ہے، سیٹ کے ایک خاندان کے ساتھ، ہر سیٹ میں آپریشن کی علامتیں (یا صرف علامتیں) ہوتی ہیں جو اقسام سے متعلق ہوتی ہیں۔ ہم قسموں سے متعلق آپریشن کی علامتوں کے سیٹ کو ظاہر کرنے کے لیے استعمال کرتے ہیں۔ مثال کے طور پر، انٹیجر اسٹیکس کے دستخط کے لیے، ہم دو اقسام کی وضاحت کرتے ہیں، یعنی، اور، اور آپریشن کی علامتوں کا مندرجہ ذیل خاندان: جہاں خالی تار کی نشاندہی ہوتی ہے۔ دستخطی کی سیٹ تھیوریٹک تشریح ایک الجبرا اقسام اور عمل کی علامتوں کی تشریح سیٹوں اور افعال کے طور پر کرتا ہے۔ ہر قسم کی تشریح ایک سیٹ کے طور پر کی جاتی ہے، جسے قسم کا کیریئر کہا جاتا ہے، اور اس میں موجود ہر علامت کو ایک فنکشن میں نقشہ بنایا جاتا ہے، جسے آپریشن آف کہا جاتا ہے۔ انٹیجر اسٹیکس کے دستخط کے حوالے سے، ہم ترتیب کی تشریح انٹیجرز کے سیٹ کے طور پر کرتے ہیں، اور ترتیب کی تشریح انٹیجر اسٹیکس کے سیٹ کے طور پر کرتے ہیں۔ ہم آپریشن کی علامتوں کے خاندان کی مزید تشریح مندرجہ ذیل افعال کے طور پر کرتے ہیں: سیمنٹکس سیمنٹکس سے مراد معنی یا طرز عمل ہے۔ الجبرائی تفصیلات زیر بحث شے کے معنی اور طرز عمل دونوں فراہم کرتی ہیں۔ مساوات الجبری وضاحتیں الجبری وضاحتیں مشروط مساوات کی شکل میں محوریوں کے ذریعہ بیان کی جاتی ہیں۔ انٹیجر اسٹیکس کے دستخط کے حوالے سے، ہمارے پاس درج ذیل محوریات ہیں: کسی بھی اور کے لیے، جہاں "" اشارہ کرتا ہے "" نہیں ملا "۔ ریاضیاتی سیمنٹکس کسی وضاحت کی ریاضیاتی سیمنٹکس (جسے ڈینوٹیشنل سیمنٹکس بھی کہا جاتا ہے) اس کے ریاضیاتی معنی سے مراد ہے۔ الجبرائی تفصیلات کی ریاضیاتی الفاظیات تمام الجبرا کی وہ کلاس ہے جو تفصیلات کو پورا کرتی ہے۔ خاص طور پر، گوگین اور دیگر کا کلاسیکی نقطہ نظر۔ ابتدائی الجبرا (آئسومورفزم تک منفرد) کو الجبرائی تفصیلات کے "سب سے زیادہ نمائندہ" ماڈل کے طور پر لیتا ہے۔ آپریشنل سیمنٹکس کسی تفصیلات کے آپریشنل سیمنٹکس کا مطلب ہے کہ اسے کمپیوٹیشنل مراحل کی ترتیب کے طور پر کیسے تعبیر کیا جائے۔ ہم ایک زمینی اصطلاح کو متغیرات کے بغیر الجبرائی اظہار کے طور پر بیان کرتے ہیں۔ الجبرائی تفصیلات کے آپریشنل سیمنٹکس سے مراد یہ ہے کہ دیئے گئے مساوی محوریات کو بائیں سے دائیں دوبارہ لکھنے کے قواعد کے طور پر استعمال کرتے ہوئے زمینی اصطلاحات کو کیسے تبدیل کیا جاسکتا ہے، جب تک کہ ایسی اصطلاحات اپنی معمول کی شکلوں تک نہ پہنچ جائیں، جہاں مزید دوبارہ لکھنا ممکن نہیں ہے۔ انٹیجر اسٹیکس کے محوریوں پر غور کریں۔ "اشارہ" کو دوبارہ لکھنے دیں۔ کینونکل پراپرٹی الجبرائی تفصیلات کو متمول کہا جاتا ہے (جسے چرچ-راسر بھی کہا جاتا ہے) اگر کسی بھی بنیادی اصطلاح کی دوبارہ تحریر اسی عام شکل کی طرف لے جاتی ہے۔ کہا جاتا ہے کہ یہ ختم ہو رہا ہے اگر کسی بھی بنیادی اصطلاح کی دوبارہ تحریر محدود تعداد میں مراحل کے بعد ایک عام شکل کا باعث بنے گی۔ الجبرائی تفصیلات کو کینونکل کہا جاتا ہے (جسے کنورجنٹ بھی کہا جاتا ہے) اگر یہ کنفلوینٹ اور ٹرمینیٹنگ دونوں ہو۔ دوسرے لفظوں میں، یہ کینونکل ہے اگر کسی بھی زمینی اصطلاح کی دوبارہ تحریر ایک محدود تعداد میں مراحل کے بعد ایک منفرد عام شکل کی طرف لے جاتی ہے۔ کسی بھی کینونکل الجبرائی وضاحت کو دیکھتے ہوئے، ریاضیاتی سیمنٹکس آپریشنل سیمنٹکس سے متفق ہیں۔ نتیجے کے طور پر، پروگرام کی درستگی کے مسائل کو حل کرنے کے لیے کینونکل الجبرائی وضاحتیں وسیع پیمانے پر لاگو کی گئی ہیں۔ مثال کے طور پر، متعدد محققین نے آبجیکٹ پر مبنی پروگرامنگ میں اشیاء کے مشاہداتی مساوات کی جانچ کے لیے اس طرح کی خصوصیات کا اطلاق کیا ہے۔ چن اور سی کو ایک ثانوی ماخذ کے طور پر دیکھیں جو 1981 سے 2013 تک کی ممتاز تحقیق کا تاریخی جائزہ فراہم کرتا ہے۔ الجبرائی سیمنٹکس (ریاضیاتی منطق) او بی جے (پروگرامنگ زبان) جوزف گوگین حوالہ جات رسمی طریقے کمپیوٹر سائنس میں منطق رسمی تفصیلات کی زبانیں پروگرامنگ زبان سیمنٹکس