Электронный график

В информатике электронный граф — это структура данных , которая хранит отношение эквивалентности для терминов некоторого языка.

Определение и операции

Позволять $\Sigma$ быть набором неинтерпретируемых функций , где $\Sigma _{n}$ является подмножеством $\Sigma$ состоящий из функций арности $n$ . Позволять $\mathbb {id}$ быть счетным набором непрозрачных идентификаторов, которые можно сравнивать на предмет равенства, называемых идентификаторами e-класса . Применение $f\in \Sigma _{n}$ к идентификаторам электронного класса $i_{1},i_{2},\ldots ,i_{n}\in \mathbb {id}$ обозначается $f(i_{1},i_{2},\ldots ,i_{n})$ и называется электронным узлом .

Затем электронный граф представляет классы эквивалентности электронных узлов, используя следующие структуры данных: ^[1]

объединения поиска Структура $U$ представление классов эквивалентности идентификаторов e-классов с обычными операциями $\mathrm {find}$ , $\mathrm {add}$ и $\mathrm {merge}$ . Идентификатор электронного класса $e$ является каноническим , если $\mathrm {find} (U,e)=e$ ; электронный узел $f(i_{1},\ldots ,i_{n})$ является каноническим, если каждый $i_{j}$ канонично ( $j$ в $1,\ldots ,n$ ).
Ассоциация идентификаторов электронных классов с наборами электронных узлов, называемых электронными классами . Это состоит из
- хешконы $H$ (т.е. сопоставление) канонических электронных узлов с идентификаторами e-классов, и
- карта электронного класса $M$ который сопоставляет идентификаторы электронных классов с электронными классами, так что $M$ сопоставляет эквивалентные идентификаторы с одним и тем же набором электронных узлов: $\forall i,j\in \mathbb {id} ,M[i]=M[j]\Leftrightarrow \mathrm {find} (U,i)=\mathrm {find} (U,j)$

Инварианты

В дополнение к вышеуказанной структуре действительный электронный граф соответствует нескольким инвариантам структуры данных . ^[2] Два e-узла эквивалентны , если они принадлежат одному e-классу. утверждает Инвариант конгруэнтности , что электронный граф должен гарантировать, что эквивалентность замкнута относительно конгруэнтности , где два e-узла $f(i_{1},\ldots ,i_{n}),f(j_{1},\ldots ,j_{n})$ совпадают, когда $\mathrm {find} (U,i_{k})=\mathrm {find} (U,j_{k}),k\in \{1,\ldots ,n\}$ . утверждает Инвариант хэшконов , что хэшконы сопоставляют канонические электронные узлы с их идентификатором электронного класса.

Операции

Электронные графы раскрывают обертки вокруг $\mathrm {add}$ , $\mathrm {find}$ , и $\mathrm {merge}$ операции из поиска объединения, сохраняющие инварианты электронного графа. Последняя операция — электронное сопоставление — описана ниже.

Электронное сопоставление

Позволять $V$ — набор переменных и пусть $\mathrm {Term} (\Sigma ,V)$ быть наименьшим набором, который включает функциональные символы нулевой арности (также называемые константами ), включает переменные и замыкается при применении функциональных символов. Другими словами, $\mathrm {Term} (\Sigma ,V)$ — наименьшее множество такое, что $V\subset \mathrm {Term} (\Sigma ,V)$ , $\Sigma _{0}\subset \mathrm {Term} (\Sigma ,V)$ , и когда $x_{1},\ldots ,x_{n}\in \mathrm {Term} (\Sigma ,V)$ и $f\in \Sigma _{n}$ , затем $f(x_{1},\ldots ,x_{n})\in \mathrm {Term} (\Sigma ,V)$ . Терм, содержащий переменные, называется шаблоном , термин без переменных называется основой .

Электронный график $E$ представляет собой основной термин $t\in \mathrm {Term} (\Sigma ,\emptyset )$ если один из его электронных классов представляет $t$ . Электронный класс $C$ представляет $t$ если какой-то электронный узел $f(i_{1},\ldots ,i_{n})\in C$ делает. Электронный узел $f(i_{1},\ldots ,i_{n})\in C$ представляет собой термин $g(j_{1},\ldots ,j_{n})$ если $f=g$ и каждый электронный класс $M[i_{k}]$ представляет собой термин $j_{k}$ ( $k$ в $1,\ldots ,n$ ).

электронное сопоставление — это операция, которая принимает шаблон $p\in \mathrm {Term} (\Sigma ,V)$ и электронный график $E$ , и дает все пары $(\sigma ,C)$ где $\sigma \subset V\times \mathbb {id}$ является заменой, отображающей переменные в $p$ к идентификаторам электронного класса и $C\in \mathbb {id}$ — это идентификатор электронного класса, такой, что каждый термин $\sigma (p)$ представлен $C$ . Существует несколько известных алгоритмов электронного сопоставления. ^[3]^[4] Алгоритм реляционного электронного сопоставления основан на оптимальных соединениях для наихудшего случая и является оптимальным для наихудшего случая. ^[5]

Сложность

Электронный граф с n равенствами можно построить за время O( n log n ). ^[6]

Равенство насыщения

Насыщение равенством — это метод построения оптимизирующих компиляторов с использованием электронных графов. ^[7] Он работает путем применения набора перезаписей с использованием электронного сопоставления до тех пор, пока электронный граф не станет насыщенным, не будет достигнут тайм-аут, не будет достигнут предел размера электронного графа, не будет превышено фиксированное количество итераций или не будет достигнуто какое-либо другое условие остановки. После перезаписи из электронного графика извлекается оптимальный член в соответствии с некоторой функцией стоимости, обычно связанной с размером AST или соображениями производительности.

Приложения

Электронные графы используются в автоматизированном доказательстве теорем . Они являются важной частью современных решателей SMT, таких как Z3. ^[8] и CVC4 , где они используются для решения пустой теории путем вычисления конгруэнтного замыкания набора равенств, а электронное сопоставление используется для создания экземпляров кванторов. ^[9] В DPLL(T) решателях на основе , которые используют обучение предложений, управляемое конфликтами (также известное как нехронологический возврат), электронные графики расширяются для создания подтверждающих сертификатов. ^[10] Электронные графы также используются в средстве доказательства теорем Simplify ESC/Java . ^[11]

Насыщение равенством используется в специализированных оптимизирующих компиляторах , ^[12] например, для глубокого обучения ^[13] и линейная алгебра . ^[14] Насыщение равенством также использовалось для проверки перевода, применяемого в наборе инструментов LLVM . ^[15]

Электронные графы применялись для решения нескольких задач анализа программ , включая фаззинг, ^[16] абстрактная интерпретация, ^[17] и библиотечное обучение. ^[18]

Ссылки

^ ( Уиллси и др. 2021 )
^ ( Уиллси и др. 2021 )
^ ( де Моура и Бьёрнер, 2007 )
^ Москаль, Михал; Лопушаньский, Якуб; Кинири, Джозеф Р. (6 мая 2008 г.). «Электронное сопоставление для удовольствия и прибыли» . Электронные заметки по теоретической информатике . Материалы 5-го Международного семинара по теориям выполнимости по модулю (SMT, 2007). 198 (2): 19–35. дои : 10.1016/j.entcs.2008.04.078 . ISSN 1571-0661 .
^ Чжан, Ихонг; Ван, Ису Реми; Уиллси, Макс; Тэтлок, Закари (12 января 2022 г.). «Реляционное электронное сопоставление» . Труды ACM по языкам программирования . 6 (ПОПЛ): 35:1–35:22. дои : 10.1145/3498696 . S2CID 236924583 .
^ ( Флэтт и др. 2022 , стр. 2)
^ ( Тейт и др. 2009 )
^ де Моура, Леонардо; Бьёрнер, Николай (2008). «Z3: эффективный решатель SMT». В Рамакришнане, Чехия; Рехоф, Якоб (ред.). Инструменты и алгоритмы построения и анализа систем . Конспекты лекций по информатике. Том. 4963. Берлин, Гейдельберг: Springer. стр. 337–340. дои : 10.1007/978-3-540-78800-3_24 . ISBN 978-3-540-78800-3 .
^ Рюммер, Филипп (2012). «Электронное сопоставление со свободными переменными». В Бьёрнере, Николай; Воронков, Андрей (ред.). Логика для программирования, искусственного интеллекта и рассуждения. Слушания . 18-я Международная конференция, LPAR-18, Мерида, Венесуэла, 11–15 марта 2012 г. Конспекты лекций по информатике. Том. 7180. Берлин, Гейдельберг: Springer. стр. 359–374. дои : 10.1007/978-3-642-28717-6_28 . ISBN 978-3-642-28717-6 .
^ ( Флэтт и др. 2022 , стр. 2)
^ Детлефс, Дэвид; Нельсон, Грег; Сакс, Джеймс Б. (май 2005 г.). «Упростить: средство доказательства теорем для проверки программ». Журнал АКМ . 52 (3): 365–473. дои : 10.1145/1066100.1066102 . ISSN 0004-5411 . S2CID 9613854 .
^ Джоши, Раджив; Нельсон, Грег; Рэндалл, Кейт (17 мая 2002 г.). «Денали: целенаправленный супероптимизатор». Уведомления ACM SIGPLAN . 37 (5): 304–314. дои : 10.1145/543552.512566 . ISSN 0362-1340 .
^ Ян, Ичен; Фотилимта, Пхитчайя Мангпо; Ван, Ису Реми; Уиллси, Макс; Рой, Судип; Пиенаар, Жак (17 марта 2021 г.). «Насыщение равенства для супероптимизации тензорных графов». arXiv : 2101.01332 [ cs.AI ].
^ Ван, Ису Реми; Хатчисон, Шана; Леанг, Джонатан; Хау, Билл; Сучу, Дэн (22 декабря 2020 г.). «СПОРЫ: оптимизация суммы произведения посредством насыщения реляционным равенством для крупномасштабной линейной алгебры». arXiv : 2002.07951 [ cs.DB ].
^ Степп, Майкл; Тейт, Росс; Лернер, Сорин (2011). «Валидатор перевода на основе равенства для LLVM». В Гопалакришнане — Ганеша; Кадир, Шаз (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 6806. Берлин, Гейдельберг: Springer. стр. 737–742. дои : 10.1007/978-3-642-22110-1_59 . ISBN 978-3-642-22110-1 .
^ «Wasm-mutate: фаззинг компиляторов WebAssembly с помощью электронных графиков (EGRAPHS 2022) — PLDI 2022» . pldi22.sigplan.org . Проверено 3 февраля 2023 г.
^ Трус, Сэмюэл; Константинидес, Джордж А.; Дрейн, Тео (17 марта 2022 г.). «Абстрактная интерпретация электронных графиков». arXiv : 2203.09191 [ cs.LO ].
Трус, Сэмюэл; Константинидес, Джордж А.; Дрейн, Тео (30 мая 2022 г.). «Сочетание электронных графиков с абстрактной интерпретацией». arXiv : 2205.14989 [ cs.DS ].
^ Цао, Дэвид; Кункель, Роуз; Нанди, Чандракана; Уиллси, Макс; Тэтлок, Закари; Поликарпова, Надя (9 января 2023 г.). «Бебля: лучшее изучение абстракций с помощью электронных графиков и борьбы с унификацией». Труды ACM по языкам программирования . 7 (ПОПЛ): 396–424. arXiv : 2212.04596 . дои : 10.1145/3571207 . ISSN 2475-1421 . S2CID 254536022 .

де Моура, Леонардо; Бьёрнер, Николай (2007). «Эффективное электронное сопоставление для решателей SMT» . В Пфеннинге, Фрэнк (ред.). Автоматизированный вычет – CADE-21 . Конспекты лекций по информатике. Том. 4603. Берлин, Гейдельберг: Springer. стр. 183–198. дои : 10.1007/978-3-540-73595-3_13 . ISBN 978-3-540-73595-3 .
Уиллси, Макс; Нанди, Чандракана; Ван, Ису Реми; Флэт, Оливер; Тэтлок, Закари; Панчеха, Павел (04.01.2021). «яйцо: быстрое и расширяемое насыщение равенства» . Труды ACM по языкам программирования . 5 (ПОПЛ): 23:1–23:29. arXiv : 2004.03082 . дои : 10.1145/3434304 . S2CID 226282597 .
Тейт, Росс; Степп, Майкл; Тэтлок, Закари; Лернер, Сорин (21 января 2009 г.). «Равенство насыщения» . Материалы 36-го ежегодного симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования . ПОПЛ '09. Саванна, Джорджия, США: Ассоциация вычислительной техники. стр. 264–276. дои : 10.1145/1480881.1480915 . ISBN 978-1-60558-379-2 . S2CID 2138086 .
Флэт, Оливер; Трус, Сэмюэл; Уиллси, Макс; Тэтлок, Закари; Панчеха, Павел (октябрь 2022 г.). «Маленькие доказательства из замыкания сравнения» . У А. Гриджио; Н. Рунгта (ред.). Материалы 22-й конференции по формальным методам в системах автоматизированного проектирования — FMCAD 2022 . TU Wien Academic Press. стр. 75–83. дои : 10.34727/2022/isbn.978-3-85448-053-2_13 . ISBN 978-3-85448-053-2 . S2CID 252118847 .

Внешние ссылки

[1] ( Уиллси и др. 2021 )

[2] ( Уиллси и др. 2021 )

[3] ( де Моура и Бьёрнер, 2007 )

[4] Москаль, Михал; Лопушаньский, Якуб; Кинири, Джозеф Р. (6 мая 2008 г.). «Электронное сопоставление для удовольствия и прибыли» . Электронные заметки по теоретической информатике . Материалы 5-го Международного семинара по теориям выполнимости по модулю (SMT, 2007). 198 (2): 19–35. дои : 10.1016/j.entcs.2008.04.078 . ISSN 1571-0661 .

[5] Чжан, Ихонг; Ван, Ису Реми; Уиллси, Макс; Тэтлок, Закари (12 января 2022 г.). «Реляционное электронное сопоставление» . Труды ACM по языкам программирования . 6 (ПОПЛ): 35:1–35:22. дои : 10.1145/3498696 . S2CID 236924583 .

[6] ( Флэтт и др. 2022 , стр. 2)

[7] ( Тейт и др. 2009 )

[8] де Моура, Леонардо; Бьёрнер, Николай (2008). «Z3: эффективный решатель SMT». В Рамакришнане, Чехия; Рехоф, Якоб (ред.). Инструменты и алгоритмы построения и анализа систем . Конспекты лекций по информатике. Том. 4963. Берлин, Гейдельберг: Springer. стр. 337–340. дои : 10.1007/978-3-540-78800-3_24 . ISBN 978-3-540-78800-3 .

[9] Рюммер, Филипп (2012). «Электронное сопоставление со свободными переменными». В Бьёрнере, Николай; Воронков, Андрей (ред.). Логика для программирования, искусственного интеллекта и рассуждения. Слушания . 18-я Международная конференция, LPAR-18, Мерида, Венесуэла, 11–15 марта 2012 г. Конспекты лекций по информатике. Том. 7180. Берлин, Гейдельберг: Springer. стр. 359–374. дои : 10.1007/978-3-642-28717-6_28 . ISBN 978-3-642-28717-6 .

[10] ( Флэтт и др. 2022 , стр. 2)

[11] Детлефс, Дэвид; Нельсон, Грег; Сакс, Джеймс Б. (май 2005 г.). «Упростить: средство доказательства теорем для проверки программ». Журнал АКМ . 52 (3): 365–473. дои : 10.1145/1066100.1066102 . ISSN 0004-5411 . S2CID 9613854 .

[12] Джоши, Раджив; Нельсон, Грег; Рэндалл, Кейт (17 мая 2002 г.). «Денали: целенаправленный супероптимизатор». Уведомления ACM SIGPLAN . 37 (5): 304–314. дои : 10.1145/543552.512566 . ISSN 0362-1340 .

[13] Ян, Ичен; Фотилимта, Пхитчайя Мангпо; Ван, Ису Реми; Уиллси, Макс; Рой, Судип; Пиенаар, Жак (17 марта 2021 г.). «Насыщение равенства для супероптимизации тензорных графов». arXiv : 2101.01332 [ cs.AI ].

[14] Ван, Ису Реми; Хатчисон, Шана; Леанг, Джонатан; Хау, Билл; Сучу, Дэн (22 декабря 2020 г.). «СПОРЫ: оптимизация суммы произведения посредством насыщения реляционным равенством для крупномасштабной линейной алгебры». arXiv : 2002.07951 [ cs.DB ].

[15] Степп, Майкл; Тейт, Росс; Лернер, Сорин (2011). «Валидатор перевода на основе равенства для LLVM». В Гопалакришнане — Ганеша; Кадир, Шаз (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 6806. Берлин, Гейдельберг: Springer. стр. 737–742. дои : 10.1007/978-3-642-22110-1_59 . ISBN 978-3-642-22110-1 .

[16] «Wasm-mutate: фаззинг компиляторов WebAssembly с помощью электронных графиков (EGRAPHS 2022) — PLDI 2022» . pldi22.sigplan.org . Проверено 3 февраля 2023 г.

[17] Трус, Сэмюэл; Константинидес, Джордж А.; Дрейн, Тео (17 марта 2022 г.). «Абстрактная интерпретация электронных графиков». arXiv : 2203.09191 [ cs.LO ].
Трус, Сэмюэл; Константинидес, Джордж А.; Дрейн, Тео (30 мая 2022 г.). «Сочетание электронных графиков с абстрактной интерпретацией». arXiv : 2205.14989 [ cs.DS ].

[18] Цао, Дэвид; Кункель, Роуз; Нанди, Чандракана; Уиллси, Макс; Тэтлок, Закари; Поликарпова, Надя (9 января 2023 г.). «Бебля: лучшее изучение абстракций с помощью электронных графиков и борьбы с унификацией». Труды ACM по языкам программирования . 7 (ПОПЛ): 396–424. arXiv : 2212.04596 . дои : 10.1145/3571207 . ISSN 2475-1421 . S2CID 254536022 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]