Эта формулировка была вытащена из комментария https://github.com/bmstu-iu9/refal-5-lambda/issues/249#issuecomment-528339722.

Постановка задачи расширенного алгоритма сопоставления

Рассмотрим уравнение

P : L

Где 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, а будет выдавать правильный ответ.

Сам расширенный алгоритм я позже сформулирую в комментариях.

Кроме того, алгоритм должен поддерживать механизм динамического обобщения, см. https://github.com/bmstu-iu9/refal-5-lambda/issues/251#issuecomment-644238141.

Немного терминологии

Требуется решить уравнение

E : P

где E — параметризованное пассивное выражение, P — образец. Выражение E построено из символов, скобок (круглых и абстрактных), переменных и конструктора замыкания. Конструктор замыкания и отличает его от образца (в образце он запрещён). На самом деле, E может быть и активным, см. #230, но здесь этот вопрос мы рассматривать не будем.

Также будем обозначать T иPt, соответственно, параметризованный терм и образец, Sym и Psym — параметризованный символ и образец символа.

Будем использовать следующую терминологию: переменные в E будем называть параметрами, переменные в P — переменными. Эта терминология пришла из суперкомпиляции, из школы Турчина — Немытых.

Подстановка — это отображение некоторого множества переменных или параметров в некоторые выражения. Подстановку, отображающую параметры из E в некоторые образцы, мы будем называть сужениями и обозначать Ct, подстановку, отображающую переменные из P в некоторые параметризованные выражения, — присваиваниями и обозначать As.

Вслед за Турчиным сужения мы будем записывать как par → P′, присваивания — E′ ← var, т.е. подстановки присваиваний будем записывать задом-наперёд. Так здесь принято.

Применение подстановки к выражению будем обозначать косой чертой: E / Ct, P / As. Композицию подстановок будем обозначать как S1 · S2: E / (S1 · S2) = E / S1 / S2.

Частным решением уравнения E : P будем называть пару (Ct, As), такую что

E / Ct = P / As

Полным решением уравнения E : P будем называть конечный набор непересекающихся частных решений (Ct1, As1), …, (CtN, AsN), такой, что для любого частного решения уравнения (Ct′, As′) найдётся такое j и такая подстановка S, что

E / Ctj / S = E / Ct′ = P / As′ = P / Asj / S

Иначе говоря:

Ct′ = Ctj / S, As′ = Asj / S

т.е. любое частное решение уравнения будет частным случаем одного из частных решений полного решения уравнения.

Частные решения полного решения не должны пересекаться, т.е. для любых i, j, что i ≠ j, верно, что

E / Cti  ∩ E / Ctj = ∅

или, что тоже самое

P / Asi ∩ P / Asj = ∅

Полное решение будем обозначать как Sol.

Заметим, что не для всех уравнений существует полное решение. Например

(s.1 e.2) (e.2 s.1) : (e.X) (e.X)

Для данного уравнения непересекающихся частных решений будет бесконечное количество:

( { s.1 → s.3, e.2 → ε       },  {         s.3 ← e.X } )
( { s.1 → s.3, e.2 → s.3     },  {     s.3 s.3 ← e.X } )
( { s.1 → s.3, e.2 → s.3 s.3 },  { s.3 s.3 s.3 ← e.X } )

Обобщением выражения (параметризованного выражения или образца) E назовём такое выражение E′, что существует подстановка S, такая что E′ / S = E. Уточнением выражения E назовём выражение E′, такое что E — обобщение E′.

Если для подстановки S существует обратная подстановка S*, такая что для любого E: E / S / S* = E, то S — подстановка-переименовка. Подстановка-переименовка согласованно переименовывает переменные в E.

Если обобщение E для E′ переводится в E′ не подстановкой-переименовкой, то такое обобщение будем называть нетривиальным. Любое нетривиальное обобщение приводит к потере информации: множество объектных выражений в результате расширяется.

Для уравнения E : P динамическим обобщением будем называть пару из параметризованного выражения E′ и подстановки S такую, что E = E′ / S и уравнение E′ : P имеет полное решение.

Если уравнение E : P имеет полное решение, то достаточно пустой подстановки S. Интерес возникает, если исходное уравнение не имело полного решения.

Динамическое обобщение существует для любого уравнения. Доказательство: E′ = e.X и S = { E ← e.X } является динамическим обобщением, т.к. уравнение e.X : P имеет решение Ct = ∅, As = { e.X → P }. Такое динамическое обобщение будем называть тривиальным.

(Почему я написал S как присваивание? Потому что в контексте использования это будет именно присваивание.)

Если уравнение E : P не имеет решения, то в динамическом обобщении E′, S обобщение E′ будет нетривиальным. Любое обобщение есть потеря информации, поэтому имеет смысл искать такое обобщение E′, которое стирает минимум информации.

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

Если есть два динамических обобщения E1, S1 и E2, S2 и E2 есть обобщение E1, то, очевидно, E1 теряет меньше информации и более предпочтительно.

Пример. Для уравнения

(s.1 e.2) (e.2 s.1) : (e.X) (e.X)

динамическим обобщением будет E′ = (s.1 e.2) (e.3 s.1), S = { e.2 ← e.3 } и полным решением для него

Ct1 = { e.2 → ε, e.3 → ε },              As1 = { s.1 ← e.X }
Ct2 = { e.2 → e.4 s.1, e.3 → s.1 e.4 },  As2 = { s.1 e.4 s.1 ← e.X }

Постановка задачи

Требуется разработать и реализовать в компиляторе алгоритм, который для данного уравнения E : P или находит полное решение, или находит приемлемое динамическое обобщение и строит полное решение для него. Приемлемое динамическое обобщение интуитивно должно стирать минимум информации.

При этом, алгоритм должен давать решение, пригодное для выполнения расширенной специализации, т.е. не нарушать семантику программы. Из этого следует, что полное решение должно представлять собой упорядоченный набор частных решений.

Пример:

F {
  … = … <G (e.X) '+' (e.X)> …;
}

G {
  (e.A '@' e.B) s.R (e.C '#' e.D) = (e.A) s.R (e.B) s.R (e.C) s.R (e.D);
}

Для уравнения

(e.X) '+' (e.X) : (e.A '@' e.B) s.R (e.C '#' e.D)

полное решение будет иметь вид

Ct1 = { e.X → e.1 '@' e.2 '#' e.3 },  As1 = { e.1 ← e.A, e.2 '#' e.3 ← e.B, '+' ← s.R, e.1 '@' e.2 ← e.C, e.3 ← e.D }
Ct2 = { e.X → e.1 '#' e.2 '@' e.3 },  As2 = { e.1 '#' e.2 ← e.A, e.3 ← e.B, '+' ← s.R, e.1 ← e.C, e.2 '@' e.3 ← e.D }

Однако, оно нам даст неприемлемый результат при специализации:

F {
  … = … <G@1 e.X> …;
}

G@1 {
  e.1 '@' e.2 '#' e.3 = (e.1) '+' (e.2 '#' e.3) '+' (e.1 '@' e.2) '+' (e.3);
  e.1 '#' e.2 '@' e.3 = (e.1 '#' e.2) '+' (e.3) '+' (e.1) '+' (e.2 '@' e.3);
}

Вызов исходной G при `e.X = '#@#' даст

<G ('#@#') '+' ('#@#')> → ('#') '+' ('#') '+' () '+' ('@#')

Вызов специализированной:

<G@1 '#@#'> → ('#') '+' ('#') '+' ('#@') '+' ()

Если поменять местами порядок решений (а значит, и предложения), то функция будет неправильно работать при e.X = '@#@'.

Однако, правильный результат даёт динамическое обобщение (e.X) '+' (e.1), { e.X ← e.1 }:

Ct = { e.X → e.2 '@' e.3, e.1 → e.4 '#' e.5 },  As = { e.2 ← e.A, e.3 ← e.B, '+' ← s.R, e.4 ← e.C, e.5 ← e.D }

Специализация для него:

F {
  … = … <G@1 (e.X) e.X> …;
}

G@1 {
  (e.2 '@' e.3) e.4 '#' e.5 = (e.2) '+' (e.3) '+' (e.4) '+' (e.5);
}

И это обобщение теряет минимум информации.

Некоторые нюансы

Читать их не обязательно, поэтому они убраны в складки.

Почему обобщение динамическое?

Потому что сейчас для специализации используется статическое обобщение — задан шаблон специализации. Шаблон специализации задаётся статически до компиляции. Есть несколько простых частных случаев, когда уравнение решается легко и однозначно: * `E : e.X`, решение: `Ct = ∅, As = { E ← e.X }`, * `T : t.X`, решение: `Ct = ∅, As = { T ← t.X }`, * `Sym : s.X`, решение: `Ct = ∅, As = { Sym ← s.X }`, * `e.X : P`, решение `Ct = { e.X → P }, As = ∅`, * `t.X : Pt`, решение `Ct = { t.X → Pt }, As = ∅`, * `s.X : Psym`, решение `Ct = { s.X → Psym }, As = ∅`. Синтаксис директивы `$SPEC` требует, чтобы образцы предложения были уточнениями шаблона, и статическим параметрам соответствовали различные переменные в образцах. Оптимизации подвергаются только те вызовы, чьи фактические аргументы являются уточнениями шаблона. Таким образом, при использовании шаблона для статических параметров решается уравнение `E : var`, а для динамических — `par : P`. В случае динамического обобщения, обобщение будет вычисляться для каждого вызова своё. Обобщение будет вычисляться динамически во время компиляции. Впрочем, элементы динамического обобщения есть и сейчас. Если аргумент не подпадает под шаблон, он обобщается до `e.X`, иначе говоря, вызов становится тривиальным и специализировать там нечего. Если при построении экземпляра замыкания оказываются в образцах, то весь аргумент тоже обобщается до `e.X` (логичнее обобщать сами замыкания до s-параметров, но это пока не реализовано). Но вообще, это схоластика. В принципе, для статических параметров технически можно задавать не переменные, а L-образцы — в этом случае тоже всё было бы разрешимо. Но специализацию писала в рамках ВКР @StrixSeloputo параллельно с @InfiniteDisorder, поэтому к моменту написания в компиляторе не было готовой логики для обобщённого сопоставления с образцом, а времени на ВКР мало. Настоящая задача (вернее, её родительская задача #251) и есть расширение специализации.

Динамическое обобщение и несколько образцов

Вообще, для нужд специализации (#251) правильнее решать задачу динамического обобщения в следующей формулировке: Дано выражение `E` и набор образцов `P1`, …, `Pn`. Требуется найти такое динамическое обобщение `E′`, `S`, что уравнения `E′ : P1`, …, `E′ : Pn` имеют полные решения, пригодные для специализации. Предлагается решать задачу следующим образом. Рассмотреть уравнение `E : P1`, найти для него динамическое обобщение `E¹`, рассмотреть уравнение `E¹ : P2`, найти для него динамическое обобщение `E²`, рассмотреть уравнение `E² : P3` и т.д. Понятно, что в таком случае велик риск переобобщения, когда конечное обобщение, полученное по предложенной процедуре, будет гораздо дальше от оптимального. Аналогично, как если при вычислении обобщения нескольких образцов вычислять `ГСО (…ГСО(ГСО(P1, P2), P3), …, Pn)` вместо `ГСО(P1, P2, …, Pn)` разом. В первом случае может получиться даже не ЛСО! Но, как решить задачу динамического обобщения сразу для нескольких образцов разом, я пока не знаю.

Алгоритм решения

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

В процессе решения будут обнаруживаться ситуации, требующие динамического обобщения левой части. Чтобы это обобщение выполнить, нужно отслеживать каким-то образом позиции в параметризованном выражении. Предлагается навтыкать в E метки координат в начало, конец и между каждыми двумя токенами записи E (спускаться ли вглубь конструкторов замыканий — вопрос открытый). Пример:

  (   s.A   e.B   )   (   e.B   s.A   )   : (e.X) (e.X)
₁ ( ₂ s.A ₃ e.B ₄ ) ₅ ( ₆ e.B ₇ s.A ₈ ) ₉ : (e.X) (e.X)

В выкладках эти позиции мы будем обозначать как {n}.

В исходном уравнении метки и токены чередуются. Однако, в процессе решения к параметризованному выражению будут применяться подстановки и чередование будет нарушаться. При подстановке e.X → e.Y t.Z появится пара смежных переменных без метки посередине, стирающая подстановка e.X → ε может привести к тому, что две метки окажутся по соседству.

Буквой E (иногда с номерами) мы будем обозначать выражения из левых частей клэшей или обеих частей уравнений в словах, которые помимо термов могут содержать координаты. Буквой E* (иногда с номерами: E1*, E2*…) мы будем обозначать выражения, на верхнем уровне которых (вне скобок) нет координатных меток.

Клэши и уравнения в словах

Мы будем рассматривать два вида уравнений.

Клэшем будем называть уравнение вида

{m} E {n} : P

В процессе решения у нас будут возникать новые клэши, набор клэшей следует хранить упорядоченным по возрастанию левой координаты {m} — их порядок будет важен при анализе открытых переменных.

Уравнением в словах будем называть уравнение вида

{k} E1 {l} = {m} E2 {n}

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

Состояние решателя и обзор алгоритма

Алгоритм выполняется в два этапа:

Сопоставление выражения с образцом без учёта повторных переменных.
Разрешение повторных переменных.

На первом этапе разрешаются клэши, на втором — формируются и решаются уравнения в словах.

Состояние алгоритма на первом этапе содержит следующие значения:

текущий набор сужений Ct,
систему клэшей,
текущий набор присваиваний As, при этом присваивания являются мультисловарём — одному имени переменной могут соответствовать несколько значений.

Присваивания содержат выражения с координатами.

Состояние алгоритма на втором этапе содержит:

текущий набор сужений Ct,
систему уравнений в словах,
текущий набор присваиваний As, который уже является обычным словарём.

В процессе решения алгоритм ветвится — строится упорядоченный набор ветвей. Набор ветвей упорядочен — это важно для правильного анализа сопоставлений с открытыми переменными.

Каждая ветвь может завершиться одной из трёх ситуаций:

успешное решение — даёт пару (Ct, As) полного решения,
отсутствием решения — данная ветвь решений не имеет,
запросом на обобщение — указывает координаты обобщаемого участка параметризованного выражения E.

Если хотя бы одна из ветвей решения вернула запрос на обобщение — E обобщается. Если разные ветви предлагают обобщить разные участки аргумента, выбирается один из вариантов, он применяется и делается новая попытка решения. Выбор оптимального варианта обобщения не очевиден, в первой версии алгоритма достаточно будет выбирать произвольный вариант.

Ветки с отсутствием решений усекаются в процессе решения. Может так оказаться, что все ветки оказались усечены. Это значит, что решений нет, например '2*2' : 5.

Про сужения

При преобразовании системы клэшей могут формироваться новые сужения и присваивания. Если формируется новое сужение, то оно применяется ко всему состоянию решателя: и к набору сужений, и к клэшам (левым частям), и к левым частям присваиваний (слева от ←). Если формируется новое присваивание, то оно просто добавляется к набору As. Применение сужения к набору сужений сводится к двум операциям: применение сужения к правым частям Ct (к частям справа от →) и добавление сужения к набору.

При преобразовании уравнений в словах могут формироваться только сужения. Они применяются к Ct, уравнениям в словах (обоим частям) и присваиваниям.

При генерации сужений часто будут требоваться новые переменные. Эти переменные будут получать индекс .NEW. Если требуется несколько новых переменных, будут использоваться индексы .NEW1, .NEW2.

Упрощение координат

В ходе преобразований как клэшей, так и уравнений в словах, могут возникать в аргументе избыточные метки координат. Смысл меток координат в том, что пара меток в E ограничивает некоторый участок, который при необходимости можно обобщить. Иногда может быть достаточно обобщить повторную переменную слева или справа от метки, дав этому вхождению новый индекс.

При подстановке сужений некоторые параметры могут схлопываться до ε, из-за чего может возникнуть скопление координат, которые уже не будут нести осмысленной нагрузки. Поэтому координаты нужно упрощать.

Координаты упрощаются по следующим правилам:

{k} {m} E {n}      ↦   {m} E {n}
    {k} E {m} {n}  ↦   {k} E {m}
{m} {n}            ↦   ε

 Ê1{k} {m} {n}Ê2   ↦  Ê1{k} {n}Ê2

Здесь Ê1, Ê2 — части записи E, которые, однако, могут не быть правильными выражениями Рефала. В частности, в них могут быть незакрытые и неоткрытые скобки.

Третье правило говорит о том, что у пустого выражения нет координат. Смысл координат — указание точек для динамического обобщения, а пустоту нигде обобщать не требуется.

Упрощение координат выполняется в клэшах, уравнениях в словах и присваиваниях после каждой подстановки сужения, а также после некоторых операций преобразования уравнений.

Разрешение клэшей — L-образцы

Существует подмножество образцов — т.н. L-образцы, для которых уравнение E : P всегда разрешимо (при этом в E должны отсутствовать конструкторы замыканий). L-образцы описаны Турчиным ещё в лохматые 70-е годы прошлого века (Турчин, Киев — Алушта, 1972).

L-образцы по Турчину запрещают любые t-переменные, а также открытые и повторные e-переменные. Однако, подход Турчина несложно расширить и на неповторные t-переменные.

В этом параграфе мы рассмотрим только сопоставление с L-образцами. Сопоставление с открытыми переменными мы рассмотрим в следующем параграфе, с повторными — в параграфе, посвящённом уравнениям в словах.

Операции преобразования системы клэшей, рассмотренные в этом разделе, мы назовём L-операциями. L-операции выполняются в указанном ниже порядке до тех пор, пока можно применить хотя бы одну из них.

Клэши «терм : терм»

 {m} T {n}  : t.X   ↦  {m} T {n} ← t.X
{m} Sym {n} : s.X   ↦  {m} Sym {n} ← s.X

{m} (E) {n} : (P)   ↦  {m} E {n} : P
{m} (E) {n} : Psym  ↦  нет решений
{m} Sym {n} : (P)  ↦  нет решений

{m} t.X {n} : (P)   ↦  t.X → (e.NEW)
{m} t.X {n} : Psym  ↦  t.X → s.NEW

{m} s.X {n} :  X    ↦  s.X → X

 {m} X {n}  :  X    ↦  стираем
 {m} X {n}  :  Y    ↦  нет решений

Заодно и условимся с обозначениями.

Если справа от ↦ находится присваивание, значит, клэш стирается, а присваивание добавляется к набору присваиваний.
Если справа от ↦ находится новый клэш, то он подменяет собой исходный. Если несколько новых клэшей, разделённых знаком && (дальше будет), то они подменяют собой исходный в указанном порядке, т.к. порядок клэшей важен.
Если справа от ↦ находится сужение, то оно применяется к набору сужений, клэшей и присваиваний, включая текущий клэш. В результате применения сужения клэш может быть разрешён на следующем шаге (пример дальше). Несколько сужений могут быть разделены знаком || (дальше будет) — это означает порождение новых веток решений в указанном порядке (порядок важен).
Если справа находится фраза стираем, клэш удаляется как разрешённый.
Фраза нет решений говорит об усечении текущей ветки решений.
Знаки X и Y означают произвольные символы, при этом X ≠ Y. Предпоследнее правило говорит о том, что слева и справа находится одинаковый символ, такой клэш тождественно истинен и поэтому стирается. Последнее — что клэш противоречив.

Пример на сужение

Клэш ``` ₁ t.X ₂ : X ``` даёт сужение `t.X → s.1`. Сужение преобразует клэш ``` ₁ s.1 ₂ : X ``` Этот клэш даёт сужение `s.1 → X`, получаем тривиальный клэш и его стираем. Другой пример: ``` ₁ t.X ₂ : (e.Y) ``` Сужение `t.X → (e.1)`: ``` ₁ (e.1) ₂ : (e.Y) ``` Правило для скобок: ``` ₁ e.1 ₂ : e.Y ``` Разрешается в присваивание ``` ₁ e.1 ₂ ← e.Y ```

Отделение термов

Эта простая операция неожиданно формулируется весьма громоздко.

{m} T {n} E : Pt P   ↦  {m} T {n} : Pt  &&  {n} E : P
E {m} T {n} : P  Pt  ↦  E {m} : P   &&  {m} T {n} : Pt

{m} T E* {n} E : Pt P   ↦  {m} T {n} : Pt  &&  {m} E* {n} E : P
E {m} E* T {n} : P  Pt  ↦  E {m} E* {n} : P   &&  {m} T {n} : Pt

При этом выражение E* в двух последних правилах не содержит меток координат на верхнем уровне.

Впрочем, несложно показать, что оно не содержит меток координат на верхнем уровне тогда и только тогда, когда оно вообще их не содержит. Выражение E* возникает в результате применения сужений, раскрывающих исходный параметр в некоторое подвыражение, а подстановки сужений координат не содержат. Поэтому и нужна эта возня (два нижних правила) для того, чтобы сохранить координаты исходного параметра в обоих дочерних клэшах.

Анализ e-параметров

Тут уже мы впервые сталкиваемся с ветвлением

{m} e.X E {n} : Pt P   ↦  e.X → t.NEW1 e.NEW2  ||  e.X → ε
{m} E e.X {n} : P  Pt  ↦  e.X → e.NEW1 t.NEW2  ||  e.X → ε

Порядок ветвей здесь важен, иначе сопоставления с открытыми переменными отработают неправильно.

Заметим, что первая ветка в обоих правилах даст на следующем шаге сопоставление T E : Pt P или E T : P Pt, логика которого описана в предыдущем параграфе. Можно было обе операции (сужение и отделение терма) объединить в одну, но это усложнит последующее описание.

Прочие случаи

{m}   E   {n} : e.X  ↦  {m} E {n} ← e.X

{m} e.X E {n} : ε    ↦  e.X → ε
{m}  T E  {n} : ε    ↦  решений нет

Два последних правила можно было бы описать фразой «Если в уравнении E : ε выражение E состоит только из e-параметров, то накладывается сужение e.X → ε на каждый параметр, иначе решений нет». Но парой формул получается лаконичнее.

Сопоставление с открытыми переменными

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

{m} E {n} : e.X P e.Y

Сопоставления с открытыми переменными, в отличие от предыдущих операций, могут привести к динамическому обобщению. При этом есть общее правило, влекущее обобщение, и есть отдельный частный случай. Частный случай необходим, поскольку общее правило будет в этом случае приводить к переобобщению.

Частный случай динамического обобщения

Частный случай заключается в том, что нельзя сопоставлять с открытой переменной открытую переменную. Пример:

(e.X) (e.X)  :  (e._ '@' e._) (e._ '#' e._)

Это сопоставление нам даст два клэша:

e.X : e._ '@' e._
e.X : e._ '#' e._

Решением первого клэша будет сужение e.X → e.1 '@' e.2. Подстановка сужения во второй клэш даст

e.1 '@' e.2 : e._ '#' e._

Решением будут сужения e.1 → e.3 '#' e.4 или e.2 → e.3 '#' e.4. Вот! Первое из них запрещено, т.к. e.1 — открытая переменная (вернее, открытый параметр). Решением проблемы является обобщение одного из параметров e.X путём его переименования.

Индексы параметров-открытых переменных нужно как-то помечать. Мы будем помечать, добавляя к индексу восклицательный знак.

Теперь опишем это правило формально.

E1 {m} E2* e.X! E3* {n} E4  :  e.L P e.R  ↦  обобщаем {m–n}

где фрагменты E2* и E3* не содержат координат.

Общее правило работы с открытыми переменными

Общий принцип описан в препринте Романенко (Романенко, 1987), однако довольно кратко и неочевидно. Мы его здесь распишем подробнее. Кроме того, способ Романенко будет порождать избыточные проверки, что будет важно в предложениях с условиями. Условия могут иметь побочный эффект, а значит их лишние вычисления нарушат семантику. Также у нас учитываются динамические обобщения, которых не было в наборе эквивалентных преобразований Рефала-4.

Если мы имеем клэш вида

E : e.X P e.Y

то мы должны рассмотреть различные разбиения E на две части. Левую часть мы должны будем присвоить переменной e.X, правую — сопоставить с P e.Y. Точки разбиения выбираются по следующему принципу:

Если E начинается на терм, то точка разбиения располагается перед первым термом.
Точки разбиения добавляются между двумя смежными термами.
Точки разбиения находятся «внутри» e-параметров.
Если E заканчивается на терм, то точка разбиения добавляется в конец.

Если точка разбиения располагается между термами, в начале или в конце, применяется следующие правила:

{m} E {n} : e.X P e.Y  ↦  ε ← e.X,  {m} E {n} : P e.Y
 ↑

{k} E1 T2 {m} T3 E4 {n} : e.X P e.Y  ↦  {k} E1 T2 {m} ← e.X,  {m} T3 E4 {n} : P e.Y
           ↑

E1 {m} E2* T3 . T4 E5* {n} E6 : e.X P e.Y  ↦  E1 {m} E2* T3 {n} ← e.X,  {m} T4 E5* {n} e.6 : P e.Y
              ↑

{m} E {n} : e.X P e.Y  ↦  {m} E {n} ← e.X,  ε : P e.Y
       ↑

ε : e.X P e.Y  ↦  ε ← e.X, ε : P e.Y
↑

Выражения E2* и E5* не содержат координат на верхнем уровне. Стрелками показаны точки разбиения. Если в точке разбиения находится координата, то стрелка показывает на неё. В случае, когда между термами координаты нет, точка разбиения обозначена точкой.

Если точка разбиения находится внутри e-параметра, то для параметра строится сужение с открытой переменной. При этом, если в левой части находится несколько смежных e-параметров, то последний из них подвергается сужению e.X → e.1 e.2, а все предшествующие — e.X → e.1 t.2 e.3. Формально:

E1 e.X {m} e.Y E2 : e.L P e.R  ↦  e.X → e.NEW1! t.NEW2 e.NEW3,
    ↑                              E1 e.NEW1! {m} ← e.L,
                                   {n} t.NEW2 e.NEW3 {m} e.Y E2 : P e.R
                где E1 = E3 {n} E4*
E1 e.X E2 : e.L P e.R  ↦  e.X → e.NEW1! e.NEW2,
    ↑                  E1 e.NEW1! {m} ← e.L,
                       {n} e.NEW2 E2 : P e.R
                где E1 = E3 {n} E4*
                    E2 = E5* {m} E6

Для каждой из точек разбиения, слева направо, решатель вызывается рекурсивно. Если рекурсивный вызов на одной из точек вернул запрос на обобщение — возвращаем запрос на обобщение.

~~Если решатель вернул более чем одно решение, обобщаем следующий клэш в системе:~~

{m′} E′ {n′} : e.L′ P′ e.R′  ↦  обобщаем {m′–n′}

Почему следующий? Потому что если несколько ветвей порождает третий, четвёртый и т.д. терм, то их ветвление увидит рекурсивный вызов для второго клэша и вернёт признак обобщения.

УТОЧНИТЬ!!!

Задача переносится на ВКР.

Уточняю про открытые e-переменные и добавляю про уравнения в словах (симметричные термы).

Сопоставление с открытыми e-переменными (уточнение)

Правила разрешения клэша с открытыми переменными описаны в целом правильно, но не полностью.

Сначала мелкие замечания

Выше описано правило

E1 e.X {m} e.Y E2 : e.L P e.R  ↦  e.X → e.NEW1! t.NEW2 e.NEW3,
    ↑                              E1 e.NEW1! {m} ← e.L,
                                   {n} t.NEW2 e.NEW3 {m} e.Y E2 : P e.R
                где E1 = E3 {n} E4*

Оно говорит о том, что если есть несколько смежных e-переменных, то все, кроме последней, разбиваются как e.X → e.NEW1! t.NEW2 e.NEW3.

Почему тут предполагается, что между двумя смежными e-переменными обязательно должна быть координата? Почему координата может отсутствовать между t-переменными?

Между e.X e.Y координата может отсутствовать, если пара переменных появились в результате сужения e.Z → e.X e.Y. Такое сужение могло возникнуть, если ранее уже разрешался клэш с открытыми переменными. Но, как сказано ранее, такие ситуации нужно запрещать. Поэтому при решении клэшей с открытыми переменными такой ситуации быть не должно.

Для каждой из точек разбиения, слева направо, решатель вызывается рекурсивно. Если рекурсивный вызов на одной из точек вернул запрос на обобщение — возвращаем запрос на обобщение.

Нет, тут достаточно простого итеративного решения безо всякой рекурсии.

Потом замечания существенные

Если у нас есть несколько клэшей на открытые переменные, то первый клэш может иметь слева произвольное выражение, а остальные должны иметь тривиальную левую часть. Иначе фигня получится. (Фигня не получится при использовании Рефала-4 в качестве промежуточного языка, но для этого нужно менять весь back-end.) Под клэшем с открытой переменной и тривиальной левой частью подразумеваем клэши вида

{m} e.X {n} : e.L P e.R
ε : e.L P e.R

Как это обеспечить?

Самый простой вариант. Можно при получении системы клэшей

{a} E1′ e.Z E1″ {b} : e.L1 P1 e.R1
…
{q} Em {r} : e.Lm Pm Rm
…

первый разрешать, а остальные, где Em ≠ e.X (причём e.X не входит в Ek, левую часть k-го клэша, в том числе и первого) или Em ≠ ε, обобщать. Но этот вариант сложен и груб.

Более точный вариант. Если мы дошли до системы клэшей с открытыми переменным справа, то смотрим на первый клэш. Если он тривиальный, то разрешаем тривиально:

{m} e.X {n} : e.L P e.R  ↦  e.X → e.NEW1! e.NEW2, {m} e.NEW1 {n} ← e.X, {m} e.NEW2 {n} : P e.R
ε : e.L P e.R  ↦  ε ← e.L, ε : P e.R

Если клэш нетривиальный и среди сужений ранее было сужение вида e.X → e.Y e.Z (сужение открытой переменной), то формируем запрос на обобщение для текущего клэша.

Кстати, о запросах на обобщение. Их можно записывать как

Generalize ('{' s.NUMBER s.NUMBER '}')+

(Их может быть более одной пары, в частности, для симметричных клэшей ≡ уравнений в словах их два.)

В актуальной реализации все для сужений на лету вычисляется композиция. Поэтому информация о том, что ранее было сужение e.X → e.Y e.Z, если не теряется, то глубоко прячется. Чтобы её выявить, можно либо просканировать все сужения на наличия смежных e-переменных, либо изменить способ хранения сужений. Я предлагаю так:

e.Contractions ::= s.OpenFlag t.Contraction
s.OpenFlag ::= None | AfterOpen

AddContraction-Spec {
  t.toAdd (s.OpenFlag e.Contractions) e.Clashes (e.Assigns)
    , t.toAdd : ((Var 'e' e._) ':' (Var 'e' e._) (Var 'e' e._))
    = <SimplifyCoordinates
        (AfterOpen <Map (&ApplyContraction-toContraction t.toAdd) e.Contractions> t.toAdd)
        <Map (&ApplyContraction-toEquation t.toAdd) e.Clashes>
        (<Map (&ApplyContraction-toAssign t.toAdd) e.Assigns>)
      >

  t.toAdd (s.OpenFlag e.Contractions) e.Clashes (e.Assigns)
    = <SimplifyCoordinates
        (AfterOpen <Map (&ApplyContraction-toContraction t.toAdd) e.Contractions> t.toAdd)
        <Map (&ApplyContraction-toEquation t.toAdd) e.Clashes>
        (<Map (&ApplyContraction-toAssign t.toAdd) e.Assigns>)
      >
}

Ну и поменять представление сужений в других местах.

Уравнения в словах в следующем комментарии

Решение симметричных клэшей (уравнений в словах)

Уравнения вида

{a} E1 {b} = {c} E2 {d}

выше предлагалось называть уравнениями в словах. Термин этот немного неточный, т.к. уравнения в словах могут содержать только символы, s- и e-переменные, а у нас есть ещё t-переменные и парные скобки. Поэтому будем называть их симметричными клэшами.

У симметричных клэшей есть два отличия от обычных клэшей:

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

Решение обычных клэшей зациклиться не может, т.к. длина правой части на каждом шаге либо уменьшается (отщепляется один элемент), либо подготавливается к отщеплению. Например, e.X E : Pt P, сужение даёт e.X → t.NEW1 e.NEW2, получается клэш t.1 e.2 E : Pt P, от которого слева отбрасывается терм.

Для уравнений в словах (частных случаев симметричных клэшей) это неверно: при применении сужений длина уравнения может и сохраняться, и расти. Например:

A e.X = e.X A,  |  e.X → A e.1
A A e.1 = A e.1 A
A e.1 = e.1 A

получили зацикливание. Антонина Николаевна aka @TonitaN может привести примеры уравнений в словах, где выражение будет распухать.

В общем случае, решение уравнений в словах требует построения графа суперкомпиляции с распознаванием зацикливаний, решение будет иметь вид не конечного набора сужений, а набора функций, проверяющих некоторое условие. Исследованию этого вопроса посвящён модельный суперкомпилятор MSCP-A, научная работа @TonitaN.

Но наша задача решать симметричные клэши только для частных случаев, которые можно выразить в виде конечного набора сужений. Либо мы можем отказаться решать симметричный клэш, обобщив соответствующие участки исходного выражения до новых e-переменных. После обобщения нам, скорее всего повезёт, и вместо неразрешимого уравнения получим простое уравнение вида e.1 = e.2, которое разрешается в e.1 → e.NEW, e.2 → e.NEW (в одну и ту же новую переменную).

Поэтому правила решения симметричных клэшей должны быть сформулированы таким образом, чтобы решать на столько, на сколько возможно, но при этом не зацикливаться.

Зарождение симметричных клэшей

Симметричные клэши возникают кратных вхождений переменных в правую часть исходного уравнения. Пусть у нас есть переменная v.X (далее индекс v будет использоваться для обозначения переменной произвольного индекса) и в процессе решения мы получили несколько присваиваний:

E1 ← v.X, …, Ek ← v.X, …, Em ← v.X

Из этих присваиваний мы в качестве результата оставляем одно (не важно какое, пусть будет первое, E1 ← v.X), а для остальных строим уравнения Ei = Ej каждый с каждым. Для 2 присваиваний — одно уравнение (E1=E2), для 3 — 3 (E1=E2, E1=E3, E2=E3), для 4 — 6 и т.д. Для N, соответственно, N×(N−1)/2 уравнений.

Вообще, в теории достаточно и N−1 уравнений, но рассмотрение уравнений каждый с каждым позволит раньше обнаруживать некоторые полезные трансформации, которые не нашлись бы при построении меньшего их числа.

Вспомогательные функции

Функция CLEAR(E) удаляет все координаты из выражения.

Функция TERM_LEFT(E) = T, E′ отделяет терм слева от выражения.

TERM_LEFT({a} T {b} E)      = {a} T {b}, {b} E
TERM_LEFT({a} T E1* {b} E2) = {a} T {b}, {a} E1* {b} E2

Фактически, эту функцию можно использовать в правиле «Отделение термов» для обычных, ассиметричных клэшей.

Функция TERM_RIGHT(E) = E′, T определяется аналогично

TERM_RIGHT(E {a} T {b})       = E {a},          {a} T {b}
TERM_RIGHT({E1 {a} E2* T {b}) = E1 {a} E2* {b}, {a} T {b}

Тавтологии

E1 = E2  ↦  стираем, если этом CLEAR(E1) ≡ CLEAR(E2)

Если сужение изменило клэш, то его нужно проверить на тавтологию и стереть при необходимости.

Клэши типа «переменная = переменная»

Если слева и справа находится переменная, то выбираем наименьший вид переменной, генерируем новую переменную этого типа и порождаем два сужения. Клэш стираем (он очевидно станет тавтологией).

{a} e.X {b} = {c} e.Y {d}  ↦  e.X → e.NEW, e.Y → e.NEW
{a} e.X {b} = {c} t.Y {d}  ↦  e.X → t.NEW, t.Y → t.NEW
{a} e.X {b} = {c} s.Y {d}  ↦  e.X → s.NEW, s.Y → s.NEW
{a} t.X {b} = {c} t.Y {d}  ↦  t.X → t.NEW, t.Y → t.NEW
{a} t.X {b} = {c} s.Y {d}  ↦  t.X → s.NEW, s.Y → s.NEW
{a} s.X {b} = {c} s.Y {d}  ↦  s.X → s.NEW, s.Y → s.NEW

Здесь и далее уравнения описаны с точностью до симметрии. Т.е. случаи, когда левая и правая части обменяны местами, не написаны, а подразумеваются. Одинаковая переменная с обоих сторон здесь появиться не может, т.к. это уравнение будет тавтологией и сотрётся раньше.

Пример. Правило

{c} s.Y {d} = {a} t.X {b}   ↦  t.X → s.NEW, s.Y → s.NEW

для случая, когда s-переменная слева, а t-переменная — справа, получается из предпоследнего правила обменом левой и правой частей.

На самом деле, в качестве оптимизации эти преобразования можно выполнять ещё на стадии зарождения симметричных уравнений. Например,

E1 ← e.R, …, e.X ← e.R, …, Ek ← e.R, …, t.Y ← e.R, …, Em ← e.R

Здесь среди всех присваиваний переменной e.R мы видим два присваивания одиночных переменных: e.X и t.Y. Наименьший тип у них — t, поэтому мы сразу можем построить сужения e.X → t.NEW, t.Y → t.NEW, применить их к набору присваиваний и заменить присваивания e.X и t.Y на t.NEW:

E1 ← e.R, …, t.NEW ← e.R, …, Ek ← e.R, …, Em ← e.R

Примечание. На первый взгляд, для уравнения e.X = e.Y можно генерировать не два сужения e.X → e.NEW, e.Y → e.NEW, а одно e.X → e.Y. Более того, в рамках данной задачи такое сужение будет работать. Но не будет работать задача #231, в которой нужно запрещать прогонку, если сужения применяются к некоторым конкретным переменным. Может так оказаться, что переменная e.Y «неразменная» и поэтому её нельзя с чем-то сравнивать. При использовании двух сужений (e.X → e.NEW, e.Y → e.NEW) мы этот случай распознаем (увидим, что переменная сужается), а при использовании сужения e.X → e.Y проблемы не увидим.

Сопоставление с пустотой

ε : {m} e.X E {n}  ↦  e.X → ε && ε = {m} E {n}
ε : {m}  T  E {n}  ↦ решений нет

Случай ε = ε — тавтология, которая стёрлась раньше.

Сопоставления типа «терм = терм»

{a} t.X {b} = {c} {{ &F e.X }} {d}  ↦  обобщаем {c−d}
{a} s.X {b} = {c} {{ &F e.X }} {d}  ↦  обобщаем {c−d}
{a}  X  {b} = {c} {{ &F e.X }} {d}  ↦  решений нет
{a} (E) {b} = {c} {{ &F e.X }} {d}  ↦  решений нет
{a} t.X {b} = {c} X {d}  ↦  t.X → X
{a} s.X {b} = {c} X {d}  ↦  s.X → X
{a} X {b} = {c} Y {d}  ↦  решений нет
{a} (E1) {b} = {c} (E2) {d}  ↦  {a} E1 {b} = {c} E2 {d}  /* просто снимаем скобки */
{a} ({b} E {c}) {d} = {e} t.X {f}  ↦  t.X → (e.NEW)
{a} (E) {b} = {c} Sym {d}  ↦  решений нет

Здесь X и Y — некоторые символы, причём X ≠ Y. Случаи, когда слева и справа переменные, рассмотрены ранее. Особого комментария требуют следующее правило:

{a} ({b} E {c}) {d} = {e} t.X {f}  ↦  t.X → (e.NEW)

Мы допускаем сужение только когда внутри скобок есть координаты (включая пустые скобки, тогда {b} ≡ {c}, между скобками будет одна координата). Если координаты нет, то сужать нельзя.

Почему?

Почему? Предотвращаем зацикливание. Рассмотрим программу: ```Refal5 $ENTRY F { t.X = } Eq { t.Eq t.Eq = True; t._ t._ = False; } ``` Проспециализируем функцию `Eq`. Рассмотрим уравнение для первого предложения: ``` ₁ ( ₂ t.X ₃ ) ₄ t.X ₅ : t.Eq t.Eq ``` Решением этого ассиметричного клэша будет пара присваиваний: ``` ₁ ( ₂ t.X ₃ ) ₄ ← t.Eq ₄ t.X ₅ ← t.Eq ``` Пара присваиваний даст нам уравнение: ``` ₁ ( ₂ t.X ₃ ) ₄ = ₄ t.X ₅ ``` Сужение применить можем: `t.X → (e.1)`. Получим: ``` ₁ ( ₂ (e.1) ₃ ) ₄ = ₄ (e.1) ₅ ``` Снимаем скобки ``` ₁ ₂ (e.1) ₃ ₄ = ₄ e.1 ₅ ₂ (e.1) ₃ = ₄ e.1 ₅ ``` сужаем `e.1 → t.2 e.3` и отделяем терм: ``` ₂ (e.1) ₃ = ₄ t.2 ₅ ``` Если дальше продолжим сужать, как для `t.X`, то зациклимся. Поэтому обобщаем `{2−3}` и `{4−5}`. Исходное уравнение примет вид ``` t.X ← t.1, t.X ← t.2 ₁ ( ₂ t.1 ₃ ) ₄ t.2 ₅ : t.Eq t.Eq ``` и успешно решится: `t.1 → t.3, t.2 → (t.3)`. Исходное уравнение решений не имеет, но наши правила это доказать не могут. Мы обобщаем левую часть уравнения и получаем уравнение, которое имеет решения. В результате специализации у нас получится предложение, которое никогда не выполняется — мёртвый код. Обобщение теряет информацию. Мы во время выполнения проспециализировали функцию: устранили построение скобок. Сопоставление с предложением по-прежнему будет выполняться во время выполнения, оно всегда будет неуспешным, но при этом вызов функции будет чуть более эффективным (скобки не строятся). Второе предложение я не рассматриваю, т.к. оно очевидно. ```Refal5 $ENTRY F { t.X = } /* ≡ */ Eq@1 { t.3 (t.3) = True; t.1 t.2 = False; } ```

Отделения термов

{a} T1 E1 = {b} T2 E2  ↦  {c} T1 {d} = {e} T2 {f} && {g} E1′ = {h} E2′
  где {c} T1 {d}, {g} E1′ := TERM_LEFT({a} T1 E1)
      {e} T2 {f}, {h} E2′ := TERM_LEFT({b} T2 E2)

E1 T1 {a} = E2 T2 {b}  ↦  E1′ {c} = E2′ {d} && {e} T1 {f} = {g} T2 {h}
  где E1′ {c}, {e} T1 {f} := TERM_RIGHT(E1 T1 {a})
      E2′ {d}, {g} T2 {h} := TERM_RIGHT(E2 T2 {b})

по идее всё просто, но много возни с координатами.

Анализ e-параметров

{a} T {b} E1 = {c} e.X E2  ↦  e.X → t.NEW1 e.NEW2  ||  e.X → ε
E1 {a} T {b} = E2 e.X {c}  ↦  e.X → e.NEW1 t.NEW2  ||  e.X → ε

Здесь, как и в случае скобок, мы требуем, чтобы терм был окружён координатами. Иначе применение данного правила приведёт к зацикливанию.

Пример

Рассмотрим программу: ```Refal5 $ENTRY AllA { e.X = } Eq { t.Eq t.Eq = True; t._ t._ = False; } ``` Функция `AllA` возвращает `True`, если аргумент состоит из нуля или более символов `A`.Специализируем функцию `Eq` в этой программе. Второе предложение неинтересное (сужений не будет, одни присваивания, которые не используются в правой части). Первое предложение ``` ₁ ( ₂ e.X ₃ A ₄ ) ₅ ( ₆ A ₇ e.X ₈ ) ₉ : t.Eq t.Eq ``` Пропуская очевидные этапы решения, получим симметричный клэш ``` ₁ ( ₂ e.X ₃ A ₄ ) ₅ = ₅ ( ₆ A ₇ e.X ₈ ) ₉ ₁ ₂ e.X ₃ A ₄ ₅ = ₅ ₆ A ₇ e.X ₈ ₉ ₂ e.X ₃ A ₄ = ₆ A ₇ e.X ₈ ``` Терм `₆ A ₇` справа окружён координатами. Строим сужения `e.X → t.1 e.2` и `e.X → ε`: ``` e.X → t.1 e.2 && ₂ t.1 e.2 ₃ A ₄ = ₆ A ₇ t.1 e.2 ₈ || e.X → ε && ₃ A ₄ = ₆ A ₇ e.X → t.1 e.2 && ₂ t.1 ₃ = ₆ A ₇ && ₂ e.2 ₃ A ₄ = ₇ t.1 e.2 ₈ || e.X → ε /* тавтология стёрта */ e.X → t.1 e.2 && t.1 → A && ₂ e.2 ₃ A ₄ = ₇ A e.2 ₈ || e.X → ε e.X → t.1 e.2 && t.1 → A && ₂ e.2 ₃ A ₄ = ₇ A e.2 ₈ || e.X → ε ``` Терм `₃ A ₄` окружён координатами. Продолжаем: ``` e.X → t.1 e.2 && t.1 → A && ₂ e.2 ₃ A ₄ = ₇ t.1 e.2 ₈ || e.X → ε e.X → t.1 e.2 && t.1 → A && ₂ e.2 ₃ A ₄ = ₇ t.1 e.2 ₈ && e.2 → e.3 t.4 || e.X → t.1 e.2 && t.1 → A && ₂ e.2 ₃ A ₄ = ₇ t.1 e.2 ₈ && e.2 → ε || e.X → ε e.X → t.1 e.2 && t.1 → A && e.2 → e.3 t.4 && ₂ e.3 t.4 ₃ A ₄ = ₇ A e.3 t.4 ₈ || e.X → t.1 e.2 && t.1 → A && e.2 → ε && ₃ A ₄ = ₇ A ₈ || e.X → ε e.X → t.1 e.2 && t.1 → A && e.2 → e.3 t.4 && ₂ e.3 t.4 ₃ = ₇ A e.3 ₈ && ₃ A ₄ = ₇ t.4 ₈ || e.X → t.1 e.2 && t.1 → A && e.2 → ε || e.X → ε e.X → t.1 e.2 && t.1 → A && e.2 → e.3 t.4 && t.4 → A && ₂ e.3 A ₃ = ₇ A e.3 ₈ || e.X → t.1 e.2 && t.1 → A && e.2 → ε || e.X → ε ``` Получили неразрешимое уравнение `₂ e.3 A ₃ = ₇ A e.3 ₈`. Если бы мы, не взирая на отсутствие координат, продолжили бы его решать, то зациклились бы. Но мы его решить не можем, т.к. ни один из символов `A` в нём не окружён координатами. Мы вынуждены обобщить `{2−3}` и `{7−8}`. ``` e.X ← e.1, e.X ← e.2 ₁ ( ₂ e.1 ₃ A ₄ ) ₅ ( ₆ A ₇ e.2 ₈ ) ₉ : t.Eq t.Eq ``` Получим клэш ``` ₁ ( ₂ e.1 ₃ A ₄ ) ₅ = ₅ ( ₆ A ₇ e.2 ₈ ) ₉ ₁ ₂ e.1 ₃ A ₄ ₅ = ₅ ₆ A ₇ e.2 ₈ ₉ ₂ e.1 ₃ A ₄ = ₆ A ₇ e.2 ₈ e.1 → t.3 e.4 && ₂ e.1 ₃ A ₄ = ₆ A ₇ e.2 ₈ || e.1 → ε && ₂ e.1 ₃ A ₄ = ₆ A ₇ e.2 ₈ e.1 → t.3 e.4 && ₂ t.3 e.4 ₃ A ₄ = ₆ A ₇ e.2 ₈ || e.1 → ε && ₃ A ₄ = ₆ A ₇ e.2 ₈ e.1 → t.3 e.4 && ₂ t.3 ₃ = ₆ A ₇ && ₂ e.4 ₃ A ₄ = ₇ e.2 ₈ || e.1 → ε && ε = ₇ e.2 ₈ e.1 → t.3 e.4 && t.3 → A && ₂ e.4 ₃ A ₄ = ₇ e.2 ₈ || e.1 → ε && e.2 → ε e.1 → t.3 e.4 && t.3 → A && e.2 → e.5 t.6 && ₂ e.4 ₃ A ₄ = ₇ e.2 ₈ || e.1 → t.3 e.4 && t.3 → A && e.2 → ε && ₂ e.4 ₃ A ₄ = ₇ e.2 ₈ || e.1 → ε && e.2 → ε e.1 → t.3 e.4 && t.3 → A && e.2 → e.5 t.6 && ₂ e.4 ₃ A ₄ = ₇ e.5 t.6 ₈ || e.1 → t.3 e.4 && t.3 → A && e.2 → ε && ₂ e.4 ₃ A ₄ = ε || e.1 → ε && e.2 → ε e.1 → t.3 e.4 && t.3 → A && e.2 → e.5 t.6 && ₂ e.4 ₃ = ₇ e.5 ₈ && ₃ A ₄ = ₇ t.6 ₈ || e.1 → t.3 e.4 && t.3 → A && e.2 → ε && решений нет || e.1 → ε && e.2 → ε e.1 → t.3 e.4 && t.3 → A && e.2 → e.5 t.6 && e.4 → e.7 && e.5 → e.7 && t.6 → A || e.1 → ε && e.2 → ε ``` Сворачивая сужения, получаем ``` e.1 → A e.7 && e.2 → e.7 A || e.1 → ε && e.2 → ε ``` Результат специализации: ```Refal5 $ENTRY AllA { e.X = } /* ≡ */ Eq@1 { (A e.7) e.7 A = True; (/* пусто */) /* пусто */ = True; (e.1) e.2 = False; } ``` В исходной программе строились 4 скобки и 2 символа `A`. В оптимизированной — только две скобки, которые необходимы для задания формата.

Больше правил нет

Если остались какие-либо симметричные клэши, к которым не применимо ни одно из вышеперечисленных правил, то мы берём произвольный из них:

{a} E1 {b} = {c} E2 {d}

и объявляем результатом запрос динамического обобщения для диапазонов {a−b} и {c−d}. В свёрнутых примерах выше так и делалось.

Итог

Правил, описанных выше, достаточно для всех трёх углов треугольника (E : L, Oe : P, e.X : P). Более того, их достаточно для тех случаев, когда ранее выполнялась специализация с явным шаблоном. Есть ощущение, что если работала специализация со статическим обобщением по шаблону, то динамическое обобщение будет не хуже.

Ad hoc-правила

На самом деле, уравнения в словах — очень широкая тема и для их решения можно придумать ещё кучу вспомогательных правил. Например, такие:

{a} e.X E1 {b} = {c} e.X E2 {d}  ↦  {a} E1 {b} = {c} E2 {d}
{a} E1 e.X {b} = {c} E2 e.X {d}  ↦  {a} E1 {b} = {c} E2 {d}

Т.е. если обе части уравнения начинаются или кончаются на одну и ту же e-переменную, то её можно стереть. Расширять это правило для термов нет необходимости, т.к. есть правила отделения термов и стирания тавтологий.

Можно предложить и другие правила, допускающие более глубокий анализ. Тут нам может помочь @TonitaN, она в этом специалист.

Насчет симметричных клэшей. Есть такой всенародно любимый SMT-солверами класс уравнений в словах, как straight-line word equations. Это как раз уравнения, решения которых могут быть записаны в виде набора сужений. В чем их особенность? Хотя бы одна сторона этих уравнений линейна, т.е. все переменные, входящие в нее, входят в уравнение ровно 1 раз. При этом вторая сторона уравнения может иметь сколько угодно кратных вхождений.

Правильно ли я понимаю, что такие уравнения, скорее всего, будут обобщаться, потому что в них почти наверняка встретится сопоставление типа е-переменная + что-то другое vs. е-переменная + что-то другое? Например, тут мы обобщаемся?

e.X A e.Y = e.Z e.Z

Да, для уравнений вида

{a} e.1 E1 e.2 {b} = {c} e.3 E2 e.4 {d}

никаких правил не описано, поэтому они будут принудительно обобщаться.

К тому же, мы имеем дело с системой уравнений, причём с заведомо избыточной, где равенства построены по принципу «каждый с каждым» (см. «Зарождение симметричных клэшей»). И поэтому понять, что переменная линейная для системы, довольно проблематично. Тем более, что в процессе решения могут появляться новые уравнения при отделении термов:

T1 E1 = T2 E2  ↦  T1 = T2 && E1 = E2

(правильный учёт координат упустил)

Хотя, если для таких прямолинейных уравнений в словах достаточно линейности переменной в отдельно взятом уравнении из системы, то, наверное, можно добавить для них дополнительные правила. Но я не уверен, что достаточно линейности переменной в отдельно взятом уравнении.

Я так понимаю, что для уравнения вида

e.L E1 e._ = e.X E2 e._

где e.L — линейная, нужно сгенерировать три сужения

e.L → e.NEW1 e.NEW2 t.NEW3 && e.X → e.NEW1,
e.L → e.NEW && e.X → e.NEW,
e.L → e.NEW1 && e.X → e.NEW1 e.NEW2 t.NEW3.

(для случая линейной переменной справа e._ E1 e.L = e._ E2 e.X уравнения аналогичны)

В первом и последнем случае нужна e.NEW1 по техническим причинам в связи с задачей #231 (см. «Примечание» в комментарии выше).

В частности, для уравнения

₁ e.X ₂ A ₃ e.Y ₄ = ₅ e.Z ₆ e.Z ₇

будут построены три сужения

e.X → e.1 e.2 t.3 && e.Z → e.1  ||  e.X → e.1 && e.Z → e.1  ||  e.X → e.1 && e.Z → e.1 e.2 t.3

Получатся три системы

e.X → e.1 e.2 t.3 && e.Z → e.1 && ₁ e.X ₂ A ₃ e.Y ₄ = ₅ e.Z ₆ e.Z ₇
  || e.X → e.1 && e.Z → e.1 &&  ₁ e.X ₂ A ₃ e.Y ₄ = ₅ e.Z ₆ e.Z ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && ₁ e.X ₂ A ₃ e.Y ₄ = ₅ e.Z ₆ e.Z ₇

e.X → e.1 e.2 t.3 && e.Z → e.1 && ₁ e.1 e.2 t.3 ₂ A ₃ e.Y ₄ = ₅ e.1 ₆ e.1 ₇
  || e.X → e.1 && e.Z → e.1 &&  ₁ e.1 ₂ A ₃ e.Y ₄ = ₅ e.1 ₆ e.1 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && ₁ e.1 ₂ A ₃ e.Y ₄ = ₅ e.1 e.2 t.3 ₆ e.1 e.2 t.3 ₇

/* пользуясь первым ad hoc правилом */

e.X → e.1 e.2 t.3 && e.Z → e.1 && ₁ e.2 t.3 ₂ A ₃ e.Y ₄ = ₆ e.1 ₇
  || e.X → e.1 && e.Z → e.1 &&  ₂ A ₃ e.Y ₄ = ₆ e.1 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && ₂ A ₃ e.Y ₄ = ₅ e.2 t.3 ₆ e.1 e.2 t.3 ₇

Для первой системы e.2 линейная, можем повторить приём. Для второй и третьей можем проанализировать переменную в правой части, пользуясь тем, что в левой части терм окружён координатами ₂ A ₃.

e.X → e.1 e.2 t.3 && e.Z → e.1 && ₁ e.2 → e.4 e.5 t.6 && e.1 → e.4 && ₁ e.2 t.3 ₂ A ₃ e.Y ₄ = ₆ e.1 ₇
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 && ₁ e.2 t.3 ₂ A ₃ e.Y ₄ = ₆ e.1 ₇
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && ₁ e.2 t.3 ₂ A ₃ e.Y ₄ = ₆ e.1 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 &&  ₂ A ₃ e.Y ₄ = ₆ e.1 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → ε && ₂ A ₃ e.Y ₄ = ₆ e.1 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && ₂ A ₃ e.Y ₄ = ₅ e.2 t.3 ₆ e.1 e.2 t.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && ₂ A ₃ e.Y ₄ = ₅ e.2 t.3 ₆ e.1 e.2 t.3 ₇

e.X → e.1 e.2 t.3 && e.Z → e.1 && ₁ e.2 → e.4 e.5 t.6 && e.1 → e.4 && ₁ e.4 e.5 t.6 t.3 ₂ A ₃ e.Y ₄ = ₆ e.4 ₇
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 && ₁ e.4 t.3 ₂ A ₃ e.Y ₄ = ₆ e.4 ₇
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && ₁ e.4 t.3 ₂ A ₃ e.Y ₄ = ₆ e.4 e.5 t.6 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 &&  ₂ A ₃ e.Y ₄ = ₆ t.2 e.3 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → ε && ₂ A ₃ e.Y ₄ = ε
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && ₂ A ₃ e.Y ₄ = ₅ t.4 e.5 t.3 ₆ e.1 e.2 t.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && ₂ A ₃ e.Y ₄ = ₅ t.3 ₆ e.1 e.2 t.3 ₇

/* ad hoc правило */

e.X → e.1 e.2 t.3 && e.Z → e.1 && ₁ e.2 → e.4 e.5 t.6 && e.1 → e.4 && ₁ e.5 t.6 t.3 ₂ A ₃ e.Y ₄ = ε
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 && ₁ t.3 ₂ A ₃ e.Y ₄ = ε
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && ₁ t.3 ₂ A ₃ e.Y ₄ = ₆ e.5 t.6 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 &&  ₂ A ₃ e.Y ₄ = ₆ t.2 e.3 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → ε && ₂ A ₃ e.Y ₄ = ε
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && ₂ A ₃ e.Y ₄ = ₅ t.4 e.5 t.3 ₆ e.1 e.2 t.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && ₂ A ₃ e.Y ₄ = ₅ t.3 ₆ e.1 e.2 t.3 ₇

/* учёт правил про ε */

e.X → e.1 e.2 t.3 && e.Z → e.1 && ₁ e.2 → e.4 e.5 t.6 && e.1 → e.4 && e.5 → ε && ₁ t.6 t.3 ₂ A ₃ e.Y ₄ = ε
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 && решений нет
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && ₁ t.3 ₂ A ₃ e.Y ₄ = ₆ e.5 t.6 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 &&  ₂ A ₃ e.Y ₄ = ₆ t.2 e.3 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → ε && решений нет
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && ₂ A ₃ e.Y ₄ = ₅ t.4 e.5 t.3 ₆ e.1 e.2 t.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && ₂ A ₃ e.Y ₄ = ₅ t.3 ₆ e.1 e.2 t.3 ₇

e.X → e.1 e.2 t.3 && e.Z → e.1 && ₁ e.2 → e.4 e.5 t.6 && e.1 → e.4 && e.5 → ε && ₁ решений нет
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 && решений нет
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && ₁ t.3 ₂ A ₃ e.Y ₄ = ₆ e.5 t.6 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 &&  ₂ A ₃ e.Y ₄ = ₆ t.2 e.3 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → ε && решений нет
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && ₂ A ₃ e.Y ₄ = ₅ t.4 e.5 t.3 ₆ e.1 e.2 t.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && ₂ A ₃ e.Y ₄ = ₅ t.3 ₆ e.1 e.2 t.3 ₇

e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && ₁ t.3 ₂ A ₃ e.Y ₄ = ₆ e.5 t.6 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 &&  ₂ A ₃ e.Y ₄ = ₆ t.2 e.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && ₂ A ₃ e.Y ₄ = ₅ t.4 e.5 t.3 ₆ e.1 e.2 t.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && ₂ A ₃ e.Y ₄ = ₅ t.3 ₆ e.1 e.2 t.3 ₇

/* отделения термов */

e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8 && ₁ t.3 ₂ A ₃ e.Y ₄ = ₆ e.5 t.6 ₇
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → ε && ₁ t.3 ₂ A ₃ e.Y ₄ = ₆ e.5 t.6 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 && ₂ A ₃ = ₆ t.2 ₇ && ₂ e.Y ₄ = ₆ e.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && ₂ A ₃ = ₅ t.4 ₆ && ₃ e.Y ₄ = ₅ e.5 t.3 ₆ e.1 e.2 t.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && ₂ A ₃ = ₅ t.3 ₆ && ₃ e.Y ₄ = ₆ e.1 e.2 t.3 ₇

e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && ₁ t.3 ₂ A ₃ e.Y ₄ = ₆ t.7 e.8 t.6 ₇
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → ε
    && ₁ t.3 ₂ A ₃ e.Y ₄ = ₆ t.6 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 && t.2 → A && e.Y → e.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && t.4 → A && ₃ e.Y ₄ = ₅ e.5 t.3 ₆ e.1 e.2 t.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && t.3 → A && ₃ e.Y ₄ = ₆ e.1 e.2 t.3 ₇

e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && ₁ t.3 ₂ = ₆ t.7 ₇ && ₂ A ₃ e.Y ₄ = ₆ e.8 t.6 ₇
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → ε
    && ₁ t.3 ₂ = ₆ t.6 ₇ && ₂ A ₃ e.Y ₄ = ε
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 && t.2 → A && e.Y → e.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && t.4 → A && ₃ e.Y ₄ = ₅ e.5 t.3 ₆ e.1 e.2 t.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && t.3 → A && ₃ e.Y ₄ = ₆ e.1 e.2 t.3 ₇

e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && t.3 → t.8 && t.7 → t.8 && ₂ A ₃ e.Y ₄ = ₆ e.8 t.6 ₇
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → ε
    && t.3 → t.8 && t.6 → t.8 && ₂ A ₃ e.Y ₄ = ε
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 && t.2 → A && e.Y → e.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && t.4 → A && ₃ e.Y ₄ = ₅ e.5 t.3 ₆ e.1 e.2 t.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && t.3 → A && ₃ e.Y ₄ = ₆ e.1 e.2 t.3 ₇

e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && t.3 → t.8 && t.7 → t.8 && ₂ A ₃ e.Y ₄ = ₆ e.8 t.6 ₇
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → ε
    && t.3 → t.8 && t.6 → t.8 && решений нет
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 && t.2 → A && e.Y → e.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && t.4 → A && ₃ e.Y ₄ = ₅ e.5 t.3 ₆ e.1 e.2 t.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && t.3 → A && ₃ e.Y ₄ = ₆ e.1 e.2 t.3 ₇

e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && t.3 → t.8 && t.7 → t.8 && ₂ A ₃ e.Y ₄ = ₆ e.8 t.6 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 && t.2 → A && e.Y → e.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && t.4 → A && ₃ e.Y ₄ = ₅ e.5 t.3 ₆ e.1 e.2 t.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && t.3 → A && ₃ e.Y ₄ = ₆ e.1 e.2 t.3 ₇

Из оставшихся четырёх систем, в первой нужно анализировать e.8 (т.к. справа терм окружён координатами), вторая решена (уравнений нет, остались одни сужения), в двух последних формально нужно применять правила про линейные переменные, хотя можно сразу построить сужение e.Y → правая часть. Если формально применить правило про линейные переменные, то надо рассмотреть три случая: e.Y короче чем e.5/e.1, e.Y равна и e.Y длиннее. Первые два отсекутся правилами про ε, последнее «e.Y длиннее» в конечном счёте даст аналог e.Y → правая часть, но с лишними расщеплениями некоторых e-переменных.

Дальше лень думать, дорешаю завтра.

Но могу пока сделать вывод, что прямолинейные уравнения в словах можно прорешать независимо от всей системы. Получится конечный набор сужений, уравнений станет на 1 меньше, конечный набор сужений применится к остальным. И, если повезёт, то новая система успешно решится. Это второе полезное ad hoc правило.

И третье полезное правило, которое вылезло из уравнений

… && ₃ e.Y ₄ = ₅ e.5 t.3 ₆ e.1 e.2 t.3 ₇
… && ₃ e.Y ₄ = ₆ e.1 e.2 t.3 ₇

Что если симметричный клэш имеет вид

{a} e.X {b} = {c} E {d}

и v.i — все переменные из E, то для каждой v.i генерируем новую переменную v.NEW_i, строим сужения v.i → v.NEW_i и сужение e.X → E / { v.i → v.NEW_i }. Уравнение стираем.

@TonitaN, спасибо за интересные и полезные подсказки. @VladisP, для начала реализуйте и отладьте до фразы «Итог» в предыдущем комментарии, а потом уже добавим и отладим 3 ad hoc правила.

А ведь тут правда интересный вопрос возникает, в каком порядке применять правила решения симметричных клэшей, если у нас есть прямолинейное уравнение, и есть еще что-то, куда входят переменные, являющиеся линейными в нем. Ну во-первых, если можно такие переменные в соседних клэшах сопоставить с выражением типа терм+переменная или символ+переменная, то это ничего не портит. Прямолинейность 100% сохранится. Поэтому большинство описанных тобой правил можно безопасно применить до решения нашего уравнения. Во-вторых, если прямолинейных уравнений несколько и с одной и той же, скажем, правой частью, причем линейной (принцип каждого с каждым) - то понятно, придется выбирать только какое-то одно, остальные обобщать. Похоже, что это всё равно выгоднее, чем обобщать всё. На расщепление, кажется, можно особо не смотреть - оно не поменяет ситуацию. Во всяком случае, я уже привыкла, что для уравнений в словах расщепление - вообще одна из самых безопасных операций, которая никогда не ухудшает класс уравнения, наравне с подстановками e.x → символ e.x

Мне кажется, всё в порядке будет.

Можно прорешать отдельно линейное уравнение, допустим, оно решится. Получится несколько решений — несколько отдельных наборов сужений. Их применить к оставшейся системе и посмотреть, что получится дальше. Дальше, очевидно, в системе будет на одно уравнение меньше.

Так что процедура: выбрать линейное уравнение, решить по отдельности, повторить, не приведёт к зацикливанию, т.к. число уравнений при этом убывает.

Продолжу выкладки:

e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && t.3 → t.8 && t.7 → t.8 && ₂ A ₃ e.Y ₄ = ₆ e.8 t.6 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 && t.2 → A && e.Y → e.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && t.4 → A && ₃ e.Y ₄ = ₅ e.5 t.3 ₆ e.1 e.2 t.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && t.3 → A && ₃ e.Y ₄ = ₆ e.1 e.2 t.3 ₇

Вчера я не до конца подставил сужения для повторных переменных. В последних двух уравнениях осталась e.2, хотя для неё есть сужения. Подставлю:

e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && t.3 → t.8 && t.7 → t.8 && ₂ A ₃ e.Y ₄ = ₆ e.8 t.6 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 && t.2 → A && e.Y → e.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && t.4 → A && ₃ e.Y ₄ = ₅ e.5 t.3 ₆ e.1 A e.5 t.3 ₇
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && t.3 → A && ₃ e.Y ₄ = ₆ e.1 t.3 ₇

В первом анализируем e.8, в двух последних заменяем равенство переменной на сужение этой переменной. Формально для каждой из переменных справа нужно сгенерировать новую переменную, но тут они уже все новые и вообще это ручные выкладки.

e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && t.3 → t.8 && t.7 → t.8 && e.8 → t.9 e.10 && ₂ A ₃ e.Y ₄ = ₆ e.8 t.6 ₇
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && t.3 → t.8 && t.7 → t.8 && e.8 → ε && ₂ A ₃ e.Y ₄ = ₆ e.8 t.6 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 && t.2 → A && e.Y → e.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && t.4 → A && e.Y → e.5 t.3 e.1 A e.5 t.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && t.3 → A && e.Y → e.1 t.3

e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && t.3 → t.8 && t.7 → t.8 && e.8 → t.9 e.10 && ₂ A ₃ e.Y ₄ = ₆ t.9 e.10 t.6 ₇
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && t.3 → t.8 && t.7 → t.8 && e.8 → ε && ₂ A ₃ e.Y ₄ = ₆ t.6 ₇
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 && t.2 → A && e.Y → e.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && t.4 → A && e.Y → e.5 t.3 e.1 A e.5 t.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && t.3 → A && e.Y → e.1 t.3

e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && t.3 → t.8 && t.7 → t.8 && e.8 → t.9 e.10 && ₂ A ₃ = ₆ t.9 ₇ && ₃ e.Y ₄ = ₆ e.10 t.6 ₇
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && t.3 → t.8 && t.7 → t.8 && e.8 → ε && ₂ A ₃ = ₆ t.6 ₇ && ₃ e.Y ₄ = ε
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 && t.2 → A && e.Y → e.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && t.4 → A && e.Y → e.5 t.3 e.1 A e.5 t.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && t.3 → A && e.Y → e.1 t.3

e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && t.3 → t.8 && t.7 → t.8 && e.8 → t.9 e.10 && t.9 → A && e.Y → e.10 t.6
  || e.X → e.1 e.2 t.3 && e.Z → e.1 && e.2 → e.4 && e.1 → e.4 e.5 t.6 && e.5 → t.7 e.8
    && t.3 → t.8 && t.7 → t.8 && e.8 → ε && t.6 → A && e.Y → ε
  || e.X → e.1 && e.Z → e.1 && e.1 → t.2 e.3 && t.2 → A && e.Y → e.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → t.4 e.5 && t.4 → A && e.Y → e.5 t.3 e.1 A e.5 t.3
  || e.X → e.1 && e.Z → e.1 e.2 t.3 && e.2 → ε && t.3 → A && e.Y → e.1 A

/* упрощаем */

e.X → e.4 t.8 A e.10 t.6 e.4 t.8 && e.Z → e.4 t.8 A e.10 t.6 &&  e.Y → e.10 t.6
  || e.X → e.4 t.8 A e.4 t.8 && e.Z → e.4 t.8 A && e.Y → ε
  || e.X → A e.3 && e.Z → A e.3 && e.Y → e.3
  || e.X → e.1 && e.Z → e.1 A e.5 t.3 && e.Y → e.5 t.3 e.1 A e.5 t.3
  || e.X → e.1 && e.Z → e.1 A && e.Y → e.1 A

Это 5 решений уравнения

e.X A e.Y = e.Z e.Z

Проверю:

e.X → e.4 t.8 A e.10 t.6 e.4 t.8 && e.Z → e.4 t.8 A e.10 t.6 && e.Y → e.10 t.6 e.4 t.8 A e.10 t.6 e.4 t.8 A e.10 t.6 = e.4 t.8 A e.10 t.6 e.4 t.8 A e.10 t.6 Верно.
e.X → e.4 t.8 A e.4 t.8 && e.Z → e.4 t.8 A && e.Y → ε e.4 t.8 A e.4 t.8 A = e.4 t.8 A e.4 t.8 A Верно.
e.X → A e.3 && e.Z → A e.3 && e.Y → e.3 A e.3 A e.3 = A e.3 A e.3 Верно.
e.X → e.1 && e.Z → e.1 A e.5 t.3 && e.Y → e.5 t.3 e.1 A e.5 t.3 e.1 A e.5 t.3 e.1 A e.5 t.3 = e.1 A e.5 t.3 e.1 A e.5 t.3 Верно.
e.X → e.1 && e.Z → e.1 A && e.Y → e.1 A e.1 A e.1 A = e.1 A e.1 A Верно.

Динамическое обобщение

Псевдокод динамического обобщения:

def SOLVE-SPEC(expr, pat):
    assignments := ∅
    while sol := SOLVE-SPEC-AUX(expr, pat); Undefined _ ∈ sol:
        if Undefined {a–b} ∈ sol:
            <assignments, expr> := GENERALIZE(assignments, expr, {a–b})
        elif Undefined {a–b}, {c–d} ∈ sol:
            <assignments, expr> := GENERALIZE(assignments, expr, {a–b})
            <assignments, expr> := GENERALIZE(assignments, expr, {c–d})
    return <sol, assignments, expr>

GENERALIZE(assignments, expr, {x–y})
    Ê1 {x} E2 {y} Ê3 := expr
    varval := CLEAR(E2 / assignments)
    if E2 == {{ &F e.Content }}:
        varname := s.NEW
    else:
        varname := e.NEW
    assignments = assignments ⋃ { varval ← varname }
    return <assignments, Ê1 {x} varname {y} Ê2>

bmstu-iu9 / refal-5-lambda

Расширенный алгоритм обобщённого сопоставления #322

Постановка задачи расширенного алгоритма сопоставления

Немного терминологии

Постановка задачи

Некоторые нюансы

Почему обобщение динамическое?

Динамическое обобщение и несколько образцов

Алгоритм решения

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

Клэши и уравнения в словах

Состояние решателя и обзор алгоритма

Про сужения

Упрощение координат

Разрешение клэшей — L-образцы

Клэши «терм : терм»

Отделение термов

Анализ e-параметров

Прочие случаи

Сопоставление с открытыми переменными

Частный случай динамического обобщения

Общее правило работы с открытыми переменными

Сопоставление с открытыми e-переменными (уточнение)

Сначала мелкие замечания

Потом замечания существенные

Решение симметричных клэшей (уравнений в словах)

Зарождение симметричных клэшей

Вспомогательные функции

Тавтологии

Клэши типа «переменная = переменная»

Сопоставление с пустотой

Сопоставления типа «терм = терм»

Отделения термов

Анализ e-параметров

Больше правил нет

Итог

Ad hoc-правила

Динамическое обобщение