Расширенный алгоритм обобщённого сопоставления #322
Comments
Немного терминологииТребуется решить уравнение где Также будем обозначать Будем использовать следующую терминологию: переменные в Подстановка — это отображение некоторого множества переменных или параметров в некоторые выражения. Подстановку, отображающую параметры из Вслед за Турчиным сужения мы будем записывать как Применение подстановки к выражению будем обозначать косой чертой: Частным решением уравнения Полным решением уравнения Иначе говоря: т.е. любое частное решение уравнения будет частным случаем одного из частных решений полного решения уравнения. Частные решения полного решения не должны пересекаться, т.е. для любых или, что тоже самое Полное решение будем обозначать как Заметим, что не для всех уравнений существует полное решение. Например Для данного уравнения непересекающихся частных решений будет бесконечное количество: Обобщением выражения (параметризованного выражения или образца) Если для подстановки Если обобщение Для уравнения Если уравнение Динамическое обобщение существует для любого уравнения. Доказательство: (Почему я написал Если уравнение Однако, как определить объём информации, содержащейся в произвольном параметризованном выражении, я пока не знаю. Объём информации легко определить для жёсткого или L-выражения, оно вычисляется по формуле сложности (не буду её приводить). Как для выражения общего вида определить сложность, я пока не знаю. И вообще не уверен, что её определить можно. Если есть два динамических обобщения Пример. Для уравнения динамическим обобщением будет Постановка задачиТребуется разработать и реализовать в компиляторе алгоритм, который для данного уравнения При этом, алгоритм должен давать решение, пригодное для выполнения расширенной специализации, т.е. не нарушать семантику программы. Из этого следует, что полное решение должно представлять собой упорядоченный набор частных решений. Пример: Для уравнения полное решение будет иметь вид Однако, оно нам даст неприемлемый результат при специализации: Вызов исходной Вызов специализированной: Если поменять местами порядок решений (а значит, и предложения), то функция будет неправильно работать при Однако, правильный результат даёт динамическое обобщение Специализация для него: И это обобщение теряет минимум информации. Некоторые нюансыЧитать их не обязательно, поэтому они убраны в складки. Почему обобщение динамическое?
Потому что сейчас для специализации используется статическое обобщение — задан шаблон специализации. Шаблон специализации задаётся статически до компиляции.
Есть несколько простых частных случаев, когда уравнение решается легко и однозначно:
Синтаксис директивы Таким образом, при использовании шаблона для статических параметров решается уравнение В случае динамического обобщения, обобщение будет вычисляться для каждого вызова своё. Обобщение будет вычисляться динамически во время компиляции. Впрочем, элементы динамического обобщения есть и сейчас. Если аргумент не подпадает под шаблон, он обобщается до В принципе, для статических параметров технически можно задавать не переменные, а L-образцы — в этом случае тоже всё было бы разрешимо. Но специализацию писала в рамках ВКР @StrixSeloputo параллельно с @InfiniteDisorder, поэтому к моменту написания в компиляторе не было готовой логики для обобщённого сопоставления с образцом, а времени на ВКР мало. Настоящая задача (вернее, её родительская задача #251) и есть расширение специализации. Динамическое обобщение и несколько образцовВообще, для нужд специализации (#251) правильнее решать задачу динамического обобщения в следующей формулировке: Дано выражение Предлагается решать задачу следующим образом. Рассмотреть уравнение Аналогично, как если при вычислении обобщения нескольких образцов вычислять Но, как решить задачу динамического обобщения сразу для нескольких образцов разом, я пока не знаю. |
Алгоритм решенияКоординаты участков параметризованного выраженияВ процессе решения будут обнаруживаться ситуации, требующие динамического обобщения левой части. Чтобы это обобщение выполнить, нужно отслеживать каким-то образом позиции в параметризованном выражении. Предлагается навтыкать в В выкладках эти позиции мы будем обозначать как В исходном уравнении метки и токены чередуются. Однако, в процессе решения к параметризованному выражению будут применяться подстановки и чередование будет нарушаться. При подстановке Буквой Клэши и уравнения в словахМы будем рассматривать два вида уравнений. Клэшем будем называть уравнение вида В процессе решения у нас будут возникать новые клэши, набор клэшей следует хранить упорядоченным по возрастанию левой координаты Уравнением в словах будем называть уравнение вида Вообще, уравнения в словах — это целый раздел математики (школа Маканина), и, в отличие от Рефала, в них рассматриваются только плоские равенства параметризованных выражений, т.е. без структурных скобок. Но, поскольку при выполнении обобщённого сопоставления будут возникать такие уравнения, и для их решения будут применяться основы теории уравнений в словах, мы такие уравнения будем условно называть уравнениями в словах. Состояние решателя и обзор алгоритмаАлгоритм выполняется в два этапа:
На первом этапе разрешаются клэши, на втором — формируются и решаются уравнения в словах. Состояние алгоритма на первом этапе содержит следующие значения:
Присваивания содержат выражения с координатами. Состояние алгоритма на втором этапе содержит:
В процессе решения алгоритм ветвится — строится упорядоченный набор ветвей. Набор ветвей упорядочен — это важно для правильного анализа сопоставлений с открытыми переменными. Каждая ветвь может завершиться одной из трёх ситуаций:
Если хотя бы одна из ветвей решения вернула запрос на обобщение — Ветки с отсутствием решений усекаются в процессе решения. Может так оказаться, что все ветки оказались усечены. Это значит, что решений нет, например Про суженияПри преобразовании системы клэшей могут формироваться новые сужения и присваивания. Если формируется новое сужение, то оно применяется ко всему состоянию решателя: и к набору сужений, и к клэшам (левым частям), и к левым частям присваиваний (слева от При преобразовании уравнений в словах могут формироваться только сужения. Они применяются к При генерации сужений часто будут требоваться новые переменные. Эти переменные будут получать индекс Упрощение координатВ ходе преобразований как клэшей, так и уравнений в словах, могут возникать в аргументе избыточные метки координат. Смысл меток координат в том, что пара меток в При подстановке сужений некоторые параметры могут схлопываться до Координаты упрощаются по следующим правилам: Здесь Третье правило говорит о том, что у пустого выражения нет координат. Смысл координат — указание точек для динамического обобщения, а пустоту нигде обобщать не требуется. Упрощение координат выполняется в клэшах, уравнениях в словах и присваиваниях после каждой подстановки сужения, а также после некоторых операций преобразования уравнений. Разрешение клэшей — L-образцыСуществует подмножество образцов — т.н. L-образцы, для которых уравнение L-образцы по Турчину запрещают любые t-переменные, а также открытые и повторные e-переменные. Однако, подход Турчина несложно расширить и на неповторные t-переменные. В этом параграфе мы рассмотрим только сопоставление с L-образцами. Сопоставление с открытыми переменными мы рассмотрим в следующем параграфе, с повторными — в параграфе, посвящённом уравнениям в словах. Операции преобразования системы клэшей, рассмотренные в этом разделе, мы назовём L-операциями. L-операции выполняются в указанном ниже порядке до тех пор, пока можно применить хотя бы одну из них. Клэши «терм : терм»Заодно и условимся с обозначениями.
Пример на сужениеКлэш даёт сужение Этот клэш даёт сужение Другой пример: Сужение Правило для скобок: Разрешается в присваивание Отделение термовЭта простая операция неожиданно формулируется весьма громоздко. При этом выражение Впрочем, несложно показать, что оно не содержит меток координат на верхнем уровне тогда и только тогда, когда оно вообще их не содержит. Выражение Анализ e-параметровТут уже мы впервые сталкиваемся с ветвлением Порядок ветвей здесь важен, иначе сопоставления с открытыми переменными отработают неправильно. Заметим, что первая ветка в обоих правилах даст на следующем шаге сопоставление Прочие случаиДва последних правила можно было бы описать фразой «Если в уравнении Сопоставление с открытыми переменнымиЕсли к системе клэшей нельзя применить ни одну из вышеописанных операций, значит имеем одно из двух. Либо клэши закончились и нужно переходить ко второму этапу, либо все клэши имеют вид Сопоставления с открытыми переменными, в отличие от предыдущих операций, могут привести к динамическому обобщению. При этом есть общее правило, влекущее обобщение, и есть отдельный частный случай. Частный случай необходим, поскольку общее правило будет в этом случае приводить к переобобщению. Частный случай динамического обобщенияЧастный случай заключается в том, что нельзя сопоставлять с открытой переменной открытую переменную. Пример: Это сопоставление нам даст два клэша: Решением первого клэша будет сужение Решением будут сужения Индексы параметров-открытых переменных нужно как-то помечать. Мы будем помечать, добавляя к индексу восклицательный знак. Теперь опишем это правило формально. где фрагменты Общее правило работы с открытыми переменнымиОбщий принцип описан в препринте Романенко (Романенко, 1987), однако довольно кратко и неочевидно. Мы его здесь распишем подробнее. Кроме того, способ Романенко будет порождать избыточные проверки, что будет важно в предложениях с условиями. Условия могут иметь побочный эффект, а значит их лишние вычисления нарушат семантику. Также у нас учитываются динамические обобщения, которых не было в наборе эквивалентных преобразований Рефала-4. Если мы имеем клэш вида то мы должны рассмотреть различные разбиения
Если точка разбиения располагается между термами, в начале или в конце, применяется следующие правила: Выражения Если точка разбиения находится внутри e-параметра, то для параметра строится сужение с открытой переменной. При этом, если в левой части находится несколько смежных e-параметров, то последний из них подвергается сужению
УТОЧНИТЬ!!! |
|
Задача переносится на ВКР. |
Смысл в том, что в рамках задач #251 и #322 потребуется разработать функцию обобщённого сопоставления с другим интерфейсом — Solve-Spec. Эта функция будет возвращать либо просто решение (когда решение существует), либо динамическое обобщение левой части аргумента и результат для него. Функции Solve-Drive и Solve-Spec будут обёртками над некоторым внутренним кодом в GenericMatch.ref.
|
Уточняю про открытые e-переменные и добавляю про уравнения в словах (симметричные термы). Сопоставление с открытыми e-переменными (уточнение)Правила разрешения клэша с открытыми переменными описаны в целом правильно, но не полностью. Сначала мелкие замечанияВыше описано правило Оно говорит о том, что если есть несколько смежных e-переменных, то все, кроме последней, разбиваются как Почему тут предполагается, что между двумя смежными e-переменными обязательно должна быть координата? Почему координата может отсутствовать между t-переменными? Между
Нет, тут достаточно простого итеративного решения безо всякой рекурсии. Потом замечания существенныеЕсли у нас есть несколько клэшей на открытые переменные, то первый клэш может иметь слева произвольное выражение, а остальные должны иметь тривиальную левую часть. Иначе фигня получится. (Фигня не получится при использовании Рефала-4 в качестве промежуточного языка, но для этого нужно менять весь back-end.) Под клэшем с открытой переменной и тривиальной левой частью подразумеваем клэши вида Как это обеспечить? Самый простой вариант. Можно при получении системы клэшей первый разрешать, а остальные, где Более точный вариант. Если мы дошли до системы клэшей с открытыми переменным справа, то смотрим на первый клэш. Если он тривиальный, то разрешаем тривиально: Если клэш нетривиальный и среди сужений ранее было сужение вида Кстати, о запросах на обобщение. Их можно записывать как (Их может быть более одной пары, в частности, для симметричных клэшей ≡ уравнений в словах их два.) В актуальной реализации все для сужений на лету вычисляется композиция. Поэтому информация о том, что ранее было сужение Ну и поменять представление сужений в других местах. Уравнения в словах в следующем комментарии |
Решение симметричных клэшей (уравнений в словах)Уравнения вида выше предлагалось называть уравнениями в словах. Термин этот немного неточный, т.к. уравнения в словах могут содержать только символы, s- и e-переменные, а у нас есть ещё t-переменные и парные скобки. Поэтому будем называть их симметричными клэшами. У симметричных клэшей есть два отличия от обычных клэшей:
Решение обычных клэшей зациклиться не может, т.к. длина правой части на каждом шаге либо уменьшается (отщепляется один элемент), либо подготавливается к отщеплению. Например, Для уравнений в словах (частных случаев симметричных клэшей) это неверно: при применении сужений длина уравнения может и сохраняться, и расти. Например: получили зацикливание. Антонина Николаевна aka @TonitaN может привести примеры уравнений в словах, где выражение будет распухать. В общем случае, решение уравнений в словах требует построения графа суперкомпиляции с распознаванием зацикливаний, решение будет иметь вид не конечного набора сужений, а набора функций, проверяющих некоторое условие. Исследованию этого вопроса посвящён модельный суперкомпилятор MSCP-A, научная работа @TonitaN. Но наша задача решать симметричные клэши только для частных случаев, которые можно выразить в виде конечного набора сужений. Либо мы можем отказаться решать симметричный клэш, обобщив соответствующие участки исходного выражения до новых e-переменных. После обобщения нам, скорее всего повезёт, и вместо неразрешимого уравнения получим простое уравнение вида Поэтому правила решения симметричных клэшей должны быть сформулированы таким образом, чтобы решать на столько, на сколько возможно, но при этом не зацикливаться. Зарождение симметричных клэшейСимметричные клэши возникают кратных вхождений переменных в правую часть исходного уравнения. Пусть у нас есть переменная Из этих присваиваний мы в качестве результата оставляем одно (не важно какое, пусть будет первое, Вообще, в теории достаточно и N−1 уравнений, но рассмотрение уравнений каждый с каждым позволит раньше обнаруживать некоторые полезные трансформации, которые не нашлись бы при построении меньшего их числа. Вспомогательные функцииФункция Функция Фактически, эту функцию можно использовать в правиле «Отделение термов» для обычных, ассиметричных клэшей. Функция ТавтологииЕсли сужение изменило клэш, то его нужно проверить на тавтологию и стереть при необходимости. Клэши типа «переменная = переменная»Если слева и справа находится переменная, то выбираем наименьший вид переменной, генерируем новую переменную этого типа и порождаем два сужения. Клэш стираем (он очевидно станет тавтологией). Здесь и далее уравнения описаны с точностью до симметрии. Т.е. случаи, когда левая и правая части обменяны местами, не написаны, а подразумеваются. Одинаковая переменная с обоих сторон здесь появиться не может, т.к. это уравнение будет тавтологией и сотрётся раньше. Пример. Правило для случая, когда s-переменная слева, а t-переменная — справа, получается из предпоследнего правила обменом левой и правой частей. На самом деле, в качестве оптимизации эти преобразования можно выполнять ещё на стадии зарождения симметричных уравнений. Например, Здесь среди всех присваиваний переменной Примечание. На первый взгляд, для уравнения Сопоставление с пустотойСлучай Сопоставления типа «терм = терм»Здесь Мы допускаем сужение только когда внутри скобок есть координаты (включая пустые скобки, тогда Почему?Почему? Предотвращаем зацикливание. Рассмотрим программу: Проспециализируем функцию Решением этого ассиметричного клэша будет пара присваиваний: Пара присваиваний даст нам уравнение: Сужение применить можем: Снимаем скобки сужаем Если дальше продолжим сужать, как для и успешно решится: Исходное уравнение решений не имеет, но наши правила это доказать не могут. Мы обобщаем левую часть уравнения и получаем уравнение, которое имеет решения. В результате специализации у нас получится предложение, которое никогда не выполняется — мёртвый код. Обобщение теряет информацию. Мы во время выполнения проспециализировали функцию: устранили построение скобок. Сопоставление с предложением по-прежнему будет выполняться во время выполнения, оно всегда будет неуспешным, но при этом вызов функции будет чуть более эффективным (скобки не строятся). Второе предложение я не рассматриваю, т.к. оно очевидно. Отделения термовпо идее всё просто, но много возни с координатами. Анализ e-параметровЗдесь, как и в случае скобок, мы требуем, чтобы терм был окружён координатами. Иначе применение данного правила приведёт к зацикливанию. ПримерРассмотрим программу: Функция Пропуская очевидные этапы решения, получим симметричный клэш Терм Терм Получили неразрешимое уравнение Получим клэш Сворачивая сужения, получаем Результат специализации: В исходной программе строились 4 скобки и 2 символа Больше правил нетЕсли остались какие-либо симметричные клэши, к которым не применимо ни одно из вышеперечисленных правил, то мы берём произвольный из них: и объявляем результатом запрос динамического обобщения для диапазонов ИтогПравил, описанных выше, достаточно для всех трёх углов треугольника ( Ad hoc-правилаНа самом деле, уравнения в словах — очень широкая тема и для их решения можно придумать ещё кучу вспомогательных правил. Например, такие: Т.е. если обе части уравнения начинаются или кончаются на одну и ту же e-переменную, то её можно стереть. Расширять это правило для термов нет необходимости, т.к. есть правила отделения термов и стирания тавтологий. Можно предложить и другие правила, допускающие более глубокий анализ. Тут нам может помочь @TonitaN, она в этом специалист. |
|
Насчет симметричных клэшей. Есть такой всенародно любимый SMT-солверами класс уравнений в словах, как straight-line word equations. Это как раз уравнения, решения которых могут быть записаны в виде набора сужений. В чем их особенность? Хотя бы одна сторона этих уравнений линейна, т.е. все переменные, входящие в нее, входят в уравнение ровно 1 раз. При этом вторая сторона уравнения может иметь сколько угодно кратных вхождений. Правильно ли я понимаю, что такие уравнения, скорее всего, будут обобщаться, потому что в них почти наверняка встретится сопоставление типа е-переменная + что-то другое vs. е-переменная + что-то другое? Например, тут мы обобщаемся? |
|
Да, для уравнений вида никаких правил не описано, поэтому они будут принудительно обобщаться. К тому же, мы имеем дело с системой уравнений, причём с заведомо избыточной, где равенства построены по принципу «каждый с каждым» (см. «Зарождение симметричных клэшей»). И поэтому понять, что переменная линейная для системы, довольно проблематично. Тем более, что в процессе решения могут появляться новые уравнения при отделении термов: (правильный учёт координат упустил) Хотя, если для таких прямолинейных уравнений в словах достаточно линейности переменной в отдельно взятом уравнении из системы, то, наверное, можно добавить для них дополнительные правила. Но я не уверен, что достаточно линейности переменной в отдельно взятом уравнении. Я так понимаю, что для уравнения вида где
(для случая линейной переменной справа В первом и последнем случае нужна В частности, для уравнения будут построены три сужения Получатся три системы Для первой системы Из оставшихся четырёх систем, в первой нужно анализировать Дальше лень думать, дорешаю завтра. Но могу пока сделать вывод, что прямолинейные уравнения в словах можно прорешать независимо от всей системы. Получится конечный набор сужений, уравнений станет на 1 меньше, конечный набор сужений применится к остальным. И, если повезёт, то новая система успешно решится. Это второе полезное ad hoc правило. И третье полезное правило, которое вылезло из уравнений Что если симметричный клэш имеет вид и @TonitaN, спасибо за интересные и полезные подсказки. @VladisP, для начала реализуйте и отладьте до фразы «Итог» в предыдущем комментарии, а потом уже добавим и отладим 3 ad hoc правила. |
|
А ведь тут правда интересный вопрос возникает, в каком порядке применять правила решения симметричных клэшей, если у нас есть прямолинейное уравнение, и есть еще что-то, куда входят переменные, являющиеся линейными в нем. |
|
Мне кажется, всё в порядке будет. Можно прорешать отдельно линейное уравнение, допустим, оно решится. Получится несколько решений — несколько отдельных наборов сужений. Их применить к оставшейся системе и посмотреть, что получится дальше. Дальше, очевидно, в системе будет на одно уравнение меньше. Так что процедура: выбрать линейное уравнение, решить по отдельности, повторить, не приведёт к зацикливанию, т.к. число уравнений при этом убывает. Продолжу выкладки: Вчера я не до конца подставил сужения для повторных переменных. В последних двух уравнениях осталась В первом анализируем Это 5 решений уравнения Проверю:
|
Динамическое обобщениеПсевдокод динамического обобщения: |
Внутри аварийных вызовов <F@0 …> все символы-функции заменяются
на заглушки:
<F@0 <G &H>> → <F@0 <G@0 &H@0>>
Почему-то при этом возникают функции вида F@n@0, для которых заглушки
отсутствуют. Правильное решение — разобраться в проблеме и исправить
её (или они создаются по ошибке, или по ошибке для функций не создаются
заглушки). Но правильное решение ждёт завершения переделки специализации
в рамках #322. Поэтому делаем маленькую временную заглушку, которая,
по идее, не должна конфликтовать с веткой vladisp-generic-match.
Временная заглушка переименовывает имена экземпляров по схеме F@n → F@0.
Это неправильно, но работает.
Заглушка помечена комментарием TODO, так что будет исправлена после
завершения работ над задачами #340 и #322.
Внутри аварийных вызовов <F@0 …> все символы-функции заменяются
на заглушки:
<F@0 <G &H>> → <F@0 <G@0 &H@0>>
Почему-то при этом возникают функции вида F@n@0, для которых заглушки
отсутствуют. Правильное решение — разобраться в проблеме и исправить
её (или они создаются по ошибке, или по ошибке для функций не создаются
заглушки). Но правильное решение ждёт завершения переделки специализации
в рамках #322. Поэтому делаем маленькую временную заглушку, которая,
по идее, не должна конфликтовать с веткой vladisp-generic-match.
Временная заглушка переименовывает имена экземпляров по схеме F@n → F@0.
Это неправильно, но работает.
Заглушка помечена комментарием TODO, так что будет исправлена после
завершения работ над задачами #340 и #322.
• Первая ошибка в том, что функция расстановки координат не учитывала холодные скобки вызова, из-за чего координаты размечала неправильно. (Неправильно она размечала координаты из-за неправильного выхода из рекурсии). • Вторая ошибка, которая выявила первую ошибку, была допущена в коммите add183e. В функции определения типов выражений для некоторых аргументов открытые переменные имели приоритет над наличием скобок вызова.
Эта формулировка была вытащена из комментария #249 (comment).
Постановка задачи расширенного алгоритма сопоставления
Рассмотрим уравнение
Где
PиLмогут быть любыми образцовыми выражениями. Есть три граничных случая, когда решение уравнения можно записать в виде набора наборов сужений и присваиваний.L— L-выражение. Решается алгоритмом обобщённого сопоставления Турчина.P ≡ E— объектное выражение (не содержит переменных). Решение уравненияE : Lесть обычное сопоставление с образцом, происходящее во время выполнения программы.P ≡ e.X— e-переменная. Решение уравнения есть сужениеe.X → L(с точностью до имён переменных)Нужно разработать алгоритм обобщённого сопоставления, который работал бы в этих трёх граничных случаях, а также где-то рядом с ними. Например, случай 2 можно расширить, разрешив в P s-переменные.
Вообще, если наоборот
P— L-выражение, аL— произвольное выражение, то можно поменять местами части уравнения и решить обычным алгоритмом обобщённого сопоставления. Однако, надо иметь ввиду порядок удлинения открытых e-переменных и соответствующим образом упорядочить решения. Случай, когдаP— L-выражение, покрывает граничные случаи 2 и 3.Но не нужно делать проверку, что если
L— не L-выражение, аP— L-выражение, то нужно поменять их местами и решать. Нужно разработать алгоритм обобщённого сопоставления, который в этой ситуации не будет выдаватьUndefined, а будет выдавать правильный ответ.Сам расширенный алгоритм я позже сформулирую в комментариях.
Кроме того, алгоритм должен поддерживать механизм динамического обобщения, см. #251 (comment).
The text was updated successfully, but these errors were encountered: