גרפי e של תיקון אבטיפוס מוסיפים שוויון באופטימיזציה של מהדר

שכתוב מהדר כתיקון

האבטיפוס מציג קישור שוויון מוטמע, שסטטוסו קרוב לקישור השוויון השורשי של e-graph. המוטיבציה היא ששכתובי מהדר מכוונים לעתים קרובות: הם הופכים תוכנית מופשטת או לא מוגדרת מספיק לצורה יותר קונקרטית שניתנת להרצה על מכונה. שפות המקור עשויות להגדיר סדר הערכה או להישאר לגבי גלישת מספר שלם וחלוקה באפס, מה שיוצר אפשרויות לאופטימיזציה ותרגום.

המקור מציג אבטיפוס שנוצר על בסיס microegg של מקס וילסי, יחד עם הדגמת WASM. הקוד שלו ב-Python מכסה מודל מכוון שוויון עם פעולות union-find של שוויון, כולל באמצעות הוספת קישורי "קטן או שווה", בדיקה ודרכי רישום.

משמעויות ערכי בלתי תאומים בסכימה

דוגמה מרכזית היא ערך "לא הוגיח" בסכימות דיגיטליות. אם ערך בלתי תאום אינו נתמך, ניתן להחשיב אותו כ"לא הוגיח", מה שמאפשר לאופטימיזטור לבחור את התוצאה שיוצרת את הסכימה הטובה ביותר. האבטיפוס יכול לתקן ערך זה כאמת או שקר כך שהשוויון הגלובלי שלו לא יתרחש עם אחר כלשהו, מה שמעניק לשימושים בודדים זכות בחירה עצמאית.

הסמנטיקה שלו משקפת את המונח כחבילה של משמעויות לוגיות, שבה "קטן או שווה" מסמן הכללה של חבילה נקודתית. כללי rewrite-le ו-rewrite-ge מעבדים תיקון מכוון. תהליך החילוץ עשוי לחפש למעלה, למטה או רק שוויון, בהתאם לסוג המונח המתוקן הנדרש.

תנודתיות ב-e-graph

להפצה עם סמלי פונקציית הקישור, היישום שומר על כל ארגומנט: מונוטוני, אנטי-מונוטוני או אף לא אחד. לדוגמה נעשה שימוש בהפרש חבילות: הוא מונוטוני בארגומנט הראשון ואנטי-מונוטוני בשני. הצהרות אלה מבטיחות סגירת תיקון, e-matching עם התחשבות בשוויון וחילוץ.

מלבד סכימות, המשפט בודק שימושים אפשריים כאימפליקציה לוגית, אלגברת יחסים, תת-סוגים, הכללת דרישות וניתוח סידורי מחלקה ראשונה. המחבר מתאר את התיקון כהרחבה ישירה בהשוואה למושגי e-graph סטנדרטיים, אם כי מציין שאלות לגבי תחביר תבנית מדויק יותר ותצוגה אלגברית של חבילות יחסים עליונים ותחתונים.