POPLmark challenge
پروگرامنگ زبان کے نظریہ میں، پی او پی ایل مارک چیلنج ("پروگرامنگ زبانوں کے اصولوں کے معیار" سے، جو پہلے عوام کے لیے میکانائزڈ میٹا تھیوری تھا!) (آیڈیمیر، 2005) معیارات کا ایک مجموعہ ہے جو پروگرامنگ زبانوں کے میٹا تھیوری میں خودکار استدلال (یا میکانائزیشن) کی حالت کا اندازہ کرنے اور رسمی طریقوں کی کمیونٹی کے متنوع کراس سیکشن کے درمیان بحث اور تعاون کو متحرک کرنے کے لیے ڈیزائن کیا گیا ہے۔ بہت آسانی سے بات کرتے ہوئے، چیلنج اس پیمائش کے بارے میں ہے کہ پروگراموں کو کس طرح برتاؤ کرنے کا ارادہ کیا گیا ہے (اور اس میں شامل بہت سے پیچیدہ مسائل) کی وضاحت سے ملنے کے لیے کتنی اچھی طرح سے ثابت کیا جا سکتا ہے۔ یہ چیلنج ابتدائی طور پر پنسلوانیا یونیورسٹی میں پی ایل کلب کے اراکین نے دنیا بھر کے تعاون کاروں کے ساتھ مل کر پیش کیا تھا۔ میکانائزڈ میٹا تھیوری پر ورکشاپ چیلنج میں حصہ لینے والے محققین کی اہم میٹنگ ہے۔ پی او پی ایل مارک بینچ مارک کا ڈیزائن پروگرامنگ زبانوں کے بارے میں استدلال کے لیے عام خصوصیات سے رہنمائی کرتا ہے۔ چیلنج کے مسائل کو بڑی پروگرامنگ زبانوں کی رسمی شکل دینے کی ضرورت نہیں ہے، لیکن ان کے بارے میں استدلال میں نفاست کی ضرورت ہوتی ہے: بائنڈنگ زیادہ تر پروگرامنگ زبانوں میں بائنڈنگ کی کوئی نہ کوئی شکل ہوتی ہے، جس میں پیچیدگی صرف ٹائپ شدہ لیمبڈا کیلکولس کے سادہ بائنڈر سے لے کر پیچیدہ، ممکنہ طور پر ریکارڈ پیٹرن کے علاج میں درکار لامحدود بائنڈر تک ہوتی ہے۔ انڈکشن پراپرٹیز جیسے سبجیکٹ میں کمی اور مضبوط نارملائزیشن کے لیے اکثر پیچیدہ انڈکشن دلائل کی ضرورت ہوتی ہے۔ تعاون کو آگے بڑھانا چیلنج کا ایک کلیدی مقصد ہونے کے ناطے، حل میں دوبارہ استعمال کے قابل اجزاء شامل ہونے کی توقع کی جاتی ہے جو محققین کو زبان کی خصوصیات اور ڈیزائن کو ہر بار شروع سے شروع کرنے کی ضرورت کے بغیر شیئر کرنے کی اجازت دے گا۔ مسائل، پی او پی ایل مارک چیلنج تین حصوں پر مشتمل ہے۔ حصہ 1 کا تعلق صرف سسٹم F <: (سب ٹائپنگ کے ساتھ سسٹم F) کی اقسام سے ہے، اور اس میں مسائل ہیں جیسے: یہ چیک کرنا کہ ٹائپ سسٹم سب ٹائپنگ کی منتقلی کو تسلیم کرتا ہے۔ ریکارڈ کی موجودگی میں ذیلی ٹائپنگ کی منتقلی کی جانچ پڑتال حصہ 2 سسٹم F <: کے نحو اور الفاظ سے متعلق ہے۔ اس کا تعلق پیٹرن میچنگ پارٹ 3 کی موجودگی میں خالص ٹکڑے کے لیے ٹائپ سیفٹی کے ثبوت سے ہے جو سسٹم F <: کے رسمی استعمال کی اہلیت سے متعلق ہے۔ خاص طور پر، چیلنج میں کہا گیا ہے: آپریشنل سیمنٹکس کی نقل اور متحرک کرنا رسمی طریقوں سے مفید الگورتھم نکالنا پی او پی ایل مارک چیلنج کے کچھ حصوں کے لیے درج ذیل ٹولز کا استعمال کرتے ہوئے متعدد حل تجویز کیے گئے ہیں: اسابیل/ایچ او ایل، ٹویلف، کوک، αپرولوج، اے ٹی ایس، ابیلا اور میٹیٹا۔ مزید دیکھیں ایکسپریشن مسئلہ کیو ای ڈی منشور پی او پی ایل کانفرنس حوالہ جات برائن ای آئڈیمیر، ایرون بوہنن، میتھیو فیئربیرن، جے ناتھن فوسٹر، بینجمن سی پیئرس، پیٹر سیویل، دیمیتریوس وائٹینیوٹس، جیفری واشبرن، اسٹیفنی سی ویرچ، اور اسٹیفن اے زیڈانسویک۔ عوام کے لیے میکانائزڈ میٹا تھیوری: پی او پی ایل مارک چیلنج۔ تھیوریم پروونگ ان ہائر آرڈر لاجکس میں، 18 ویں بین الاقوامی کانفرنس، ٹی پی ایچ او ایل 2005، کمپیوٹر سائنس میں لیکچر نوٹس کا حجم 3603، صفحات 50-65۔ سپرنگر، برلن/ہیڈلبرگ/نیویارک، 2005۔ بینجمن سی پیئرس، پیٹر سیویل، اسٹیفنی ویرچ، اسٹیو زیڈانسویک، پروگرامنگ لینگویج میٹا تھیوری کو میکانائز کرنے کا وقت آگیا ہے، ان برٹرینڈ میئر، جم ووڈکاک (ایڈز۔) تصدیق شدہ سافٹ ویئر: نظریات، اوزار، تجربات، ایل این سی ایس 4171، سپرنگر برلن/ہیڈلبرگ، 2008، پی پی۔ 26-30، بیرونی روابط دی پی او پی ایل مارک چیلنج رسمی طریقے پروگرامنگ لینگویج تھیوری آٹومیٹڈ تھیوریم ثابت کرنے والے معیارات (کمپیوٹنگ)