OnionGrief / Chipollino

преобразования регулярных выражений и конечных автоматов
Other
20 stars 4 forks source link

Кэширование минимального автомата #212

Open mathhyyn opened 1 year ago

mathhyyn commented 1 year ago

Меня пробило на внезапные рассказы посреди ночи. Жаль конечно что приходится соблюдать приличия, придерживаться изначальной темы и ставить минимальные знаки препинания... Как обычно мои слепые похождения по проекту сопровождаются тщетными и долгими попытками вникнуть что же я сделала не так. Эти сомнения преследуют меня каждый раз, когда нахожу моменты, в которых программа работает не так, как я ожидала. Может это временно, может остальные уже знают об этой проблеме, может это как всегда злосчастный моноид или арден. А я как обычно трачу неприемлемо много времени на донесение своих мыслей. Собственно, предыстория: в то время, как я тестировала обновленный интерпретатор, я наткнулась на подозрительный пример: N2 = Disambiguate {((|((a(b*|(b*)baa)((a((((|b)))))))*)))} !! который выдал в отчете: 1-однозначное регулярное выражение, описывающее язык: (ab*a|b*ab|b)* тогда мне эти регулярки показались совсем не эквивалентными, но я отложила их до лучших времен (на завтра (на тот момент), но что-то тогда не срослось и взялась за это только сегодня). Я думала, может скинуть в лс и сказать "посмотри, пожалуйста. оно кажется мне странным", но и это я отложила на "завтра", чтобы проверить не запуталась ли я в скобочках. И вот, пожалуйста, я даже не знаю кого пинать. Возможно эта проблема на подобие копирования регулярок, к которому причастен каждый второй, и никому уже не хочется вспоминать про него спустя три года. А возможно очередная ерунда, которой я уделяю слишком много внимания, она исправится за 2 минуты конкретным человеком. Часть из моих экспериментов:

N2 = Disambiguate {|(a(b*|b*baa)a(|b))*} !!
Equiv {|(a(b*|b*baa)a(|b))*} N2
Equiv {(ab*a|b*ab|b)*} N2
Equiv (Minimize.Glushkov N2) (Minimize.Glushkov {|(a(b*|b*baa)a(|b))*})

1ый equiv: image но как бы.. если вписать напрямую Equiv {|(a(b*|b*baa)a(|b))*} {(ab*a|b*ab|b)*}

image ну и вполне очевидна неэквивалентность невооруженным взглядом

Можно подумать: опять преобразование регулярки to_txt шалит (его отчасти делала я, а я себе не доверяю) тогда попробуем посмотреть на автомат output1 и правда описывает второй язык.

2ой equiv: image Обойдемся без комментариев

Собака явно глубоко зарыта Что-то все же тут не то -_ - так ведь не должно работать.. Построила автоматы Equiv (Glushkov N2) (Glushkov {(ab*a|b*ab|b)*}) - false (при идентичных картинках) Equiv (Glushkov N2) (Glushkov {|(a(b*|b*baa)a(|b))*}) - true (хотя первый позволяет получить b*, а второй обязывает букву а быть первым символом) (P.S почему так происходило мне уже стало ясно, но тогда я была в недоумении) Подумала на минимальные автоматы будет смотреть попроще Но запутали они меня только больше image (кстати, что за повторения в эквивалентных состояниях, вроде норм, вроде нет) в минимальном автомате как-то не сходятся названия состояний оказывается, минимизируется автомат, построенный по изначальной регулярке. image (для сравнения)

Ради интереса решила убрать кэширование в минимизации и половина сюрпризов исчезла. 👍 конец пасты, аня выдохлась. мораль ищите сами

mathhyyn commented 1 year ago

ладно вывод все же нужен

1) вред кэширования взяла пример из Example.cpp:

N = Minimize.Glushkov.Disambiguate {(a|b)*a} !!

1-однозначное регулярное выражение, описывающее язык: b*a(a|b(b*a))*

image

может после Disambiguate как-то сообщать, что автомат поменялся, или вообще не кэшировать. потому что я не представляю как в таком случае делать рендеринг автоматов, выделять эквивалентные состояния

(а, меня только сейчас смутила эта подпись "эквивалентные классы" вместо "классы эквивалентности" 🙂)

2) баг Disambiguate

N2 = Disambiguate {|(a(b*|b*baa)a(|b))*} !!

получается неэквивалентная регулярка (ab*a|b*ab|b)*

и верификатор гипотез перед этим багом был бы бессилен, т.к. equiv сделает совершенно бессмысленную проверку равна ли регулярка сама себе, а не ее 1-однозначной версии

Equiv (Disambiguate {|(a(b*|b*baa)a(|b))*}) {|(a(b*|b*baa)a(|b))*}
TonitaN commented 1 year ago

Спасибо, что обратили внимание на проблему кэширования.

Кэширование позволяет сильно ускорить вспомогательные операции, т.к. минимизация достаточно дорогая, а некоторые другие - ещё дороже (например, синт.моноид, и я сейчас не о конкретных реализациях, а об асимптотике), а они нужны как промежуточные в разных других. Но если соответствующего вывода не было явно (т.е. пользователь не вызывал минимизацию для конкретного языка до этого), это действительно выглядит странно, потому что откуда он знает, что в том же Disambiguate была ещё и минимизация, он о ней не просил. Но если бы для Disambiguate были нормальные логи, он бы об этом внезапно узнал, и проблема бы отпала - просто нужно было бы говорить о том, что минимальный автомат не поменялся, т.к. язык остался тем же (а как построился минимальный автомат в Disambiguate, мы уже видели). И верить логам, как мне кажется, более логично, чем отключать или подключать кэширование по эвристике. А кэширование в верификаторе, которому скорость не нужна, а нужна точность, либо можно отключить явно, либо можно сломать тождественными преобразованиями, меняющими язык, а потом меняющими его обратно. Главное, сначала убедиться, что оно в контексте конкретных реализаций правда тождественное.

xendalm commented 1 year ago

потому что я не представляю как в таком случае делать рендеринг автоматов

Вообще мы про это давно знаем, там даже какое-то TODO было подписано)

mathhyyn commented 1 year ago

На заметку: можно ли закэшировать изображения графа для автоматов? (хранить путь к файлу) на рендеринг нескольких одинаковых тоже уходит много времени...

TonitaN commented 1 year ago

Давно есть мысль, что те объекты, которые относятся к языку, а не конкретному преобразованию (минимальный автомат, синт.моноид, и прочее), должны храниться в максимально абстрактной форме, без привязки к способу их получения, а история их построения должна остаться в соответствующих логах. То есть состояния минимального автомата должны иметь простые имена, а не по объединённым состояниям, поскольку при доставании из кэша важно, что минимальный автомат существует, а не история его вычисления. Это легко исправить, если добавить последним шагом минимизации альфа-преобразование (вроде, в синтаксисе других языковых объектах история вычислений и так не видна). И тогда и рендерить кэшированные объекты будет сильно проще, и неожиданностей, откуда такие странные метки узлов, для пользователя не будет (тем более, он будет предупреждён, что автомат достали из кэша).

Вот стоит ли делать альфа-преобразование на некоторых других промежуточных шагах (например, после детерминизации и перед бисимуляцией), пока непонятно. Лучше не торопиться с этим - изменение небольшое, всегда успеется, если надо будет. С одной стороны, это даст возможность более чётко видеть результат последнего преобразования, с другой - общая картина станет несколько более трудно обозримой.