مخططات e-graph للتصحيح الأولي تضيف مساواة في تحسين المترجم

إعادة كتابة المترجم كتصحيح

يقدم النموذج الأولي رابط مساواة مدمج، ترتبط حالته ارتباطاً وثيقاً برابط المساواة الجذري في e-graph. تتمثل الدافعية في أن إعادة كتابة المترجم غالباً ما تكون موجهة: إذ تتحول من برنامج تجريدي أو غير محدد بشكل كافٍ إلى شكل أكثر تحديداً يمكن تشغيله على الآلة. قد تحدد لغات المصدر ترتيب التقييم أو تتجنب تجاوز العدد الصحيح والقسمة على صفر، مما يخلق إمكانيات للتحسين والترجمة.

يمثل المصدر نموذجاً أولياً أنشأه ماكس ويلس على أساس microegg، مع عرض توضيحي لـ WASM. يغطي كود Python الخاص به نموذجاً موجهاً نحو المساواة بعمليات union-find للمساواة، بما في ذلك إضافة روابط "أقل من أو يساوي" والتحقق وسرد المسارات.

معاني القيم غير المعرفة في المخططات غير المتوافقة

المثال المركزي هو القيمة "غير معرف" في المخططات الرقمية. إذا لم تكن القيمة غير المعرفة مدعومة، يمكن اعتبار الناتج "غير معرف"، مما يتيح للمُحسِّن اختيار النتيجة التي تنشئ أفضل مخطط. يمكن للنموذج الأولي تصحيح هذه القيمة إلى صواب أو خطأ بحيث لا تتساوى مساواته العالمية مع أي قيمة أخرى منفصلة، مما يمنح التطبيقات الفردية حرية الاختيار المستقل.

تعكس دلالاته المصطلحات كمجمّعات من القيم المنطقية، حيث تشير "أقل من أو يساوي" إلى احتواء مجمّعات نقطية. تعمل قاعدتا rewrite-le وrewrite-ge على التصحيح الموجه. قد تبحث عملية الاستخراج للأعلى أو للأسفل أو فقط على المساواة، اعتماداً على نوع المصطلح المصحح المطلوب.

التباين في e-graph

يحتفظ التنفيذ للانتشار باستخدام رموز دالة العلاقات بما إذا كانت كل وسيطة رتيبة أو مضادة للرتيبة أو لا شيء منهما. على سبيل المثال، يُستخدم فرق المجموعات: فهو رتيب في الوسيطة الأولى ومضاد للرتيبة في الثانية. تضمن هذه التصريحات إغلاق التصحيح، وe-matching مع مراعاة المساواة، والاستخراج.

بالإضافة إلى المخططات، يفحص البيان التطبيقات المحتملة للاستلزام المنطقي، وجبر العلاقات، والأنواع الفرعية، واحتواء المتطلبات، وتحليلات التعيينات من الدرجة الأولى. يصف المؤلف التصحيح كامتداد مباشر لمفاهيم e-graph القياسية، رغم إشارته إلى أسئلة حول بناء جملة القالب الأكثر دقة والرؤية الجبرية لمجمّعات العلاقات العليا والسفلى.