Прототипні e-graph-и уточнення додають рівність в оптимізацію компілятора

Переписування компілятора як уточнення

Прототип впроваджує вбудований зв'язок рівності, статус якого близький до кореневого зв'язку рівності e-graph-а. Мотивація полягає в тому, що переписування компілятора часто спрямовані: вони перетворюють абстрактні або недостатньо визначені програми на більш конкретну форму, яку можна виконати на машині. Вихідні мови можуть мати невизначений порядок обчислень або залишати переповнення цілого числа та ділення на ноль, що створює можливості для оптимізації та трансляції.

Джерело представляє прототип, створений на основі microegg Макса Віллса разом із демо на WASM. Його код на Python охоплює орієнтовану на рівність модель за допомогою операцій union-find над рівністю, зокрема додавання, перевірку та перелік зв'язків «менше або дорівнює».

Значення несумісних схем

Центральним прикладом є значення «недосяжне» в цифрових схемах. Якщо значення не підтримується, вихід можна вважати «недосяжним», що дозволяє оптимізатору обрати той результат, який створює найкращу схему. Прототип може виправити це значення на істинне або хибне так, щоб його глобальна рівність не збігалася ні з одним окремим, що надає окремим застосуванням право незалежного вибору.

Його семантика відображає терміни на множини логічних значень, де «менше або дорівнює» позначає включення точкової множини. Правила rewrite-le та rewrite-ge обробляють спрямовані уточнення. Процес вилучення може шукати вгору, вниз або лише за рівністю, залежно від того, який тип виправленого терміна вимагається.

Варіативність в e-graph-і

Для розповсюдження через символи функцій відношень реалізація відстежує, яким є кожен аргумент: монотонним, антимонотонним або ні тим, ні іншим. Наприклад, використовується різниця множин: вона монотонна за першим аргументом та антимонотонна за другим. Ці оголошення забезпечують замкнення уточнення, врахування рівності через e-matching та вилучення.

Окрім схем, речення перевіряє можливі застосування для логічної імплікації, реляційної алгебри, підтипів, включення вимог та аналізу розташувань першого класу. Автор описує уточнення як пряме розширення порівняно зі стандартними поняттями e-graph, однак зазначає питання щодо більш точного синтаксису шаблонів та алгебраїчного погляду на множини верхніх і нижніх відношень.