search

bmstu-iu9 / refal-5-lambda

Компилятор Рефала-5λ
https://bmstu-iu9.github.io/refal-5-lambda
Other
79 stars 35 forks source link

Ad hoc расширения прогонки #249

Open Mazdaywik opened 5 years ago

Mazdaywik commented 5 years ago

Проблема

Турчин когда-то описал прогонку функций (Турчин, 1972, Турчин, 1974), однако, описанный алгоритм прогонки работает только для ограниченного Рефала — базисного Рефала, в образцах которого запрещены t-переменные и открытые и повторные e-переменные (т.н. L-выражения).

Алгоритм естественно расширяется на неповторные t-переменные, поэтому далее мы будем под L-выражениями подразумевать образцы, в которых запрещены открытые e-переменные и повторные t- и e-переменные.

Прогонка для функций Рефала-5 общего вида в общем случае не разрешима. Нужен переход как минимум в формализм Рефала-4 или Рефала Плюс (последний основан на Рефале-4 и включает возможности Рефала-5 как синтаксический сахар над Рефалом-4), но и там всё не так просто. Формально в Рефале Плюс (и в Рефале-6) можно встроить тело функции на место её вызова, но теории достижения содержательной цели прогонки не сформулировано (Романенко, 1987а, Романенко, 1987б).

Напомним, что есть содержательная цель прогонки. Выполнение программы на Рефале в общем случае есть цепь операций синтеза (построения результатных выражений) и последующего анализа (сопоставления с образцом). В случае базисного Рефала результатные выражения строятся только для аргументов функции, для Рефала-5 операции синтеза также включают и левые части условий (см. также #248). В общем, имеем цепочку:

S A S A S A S A …

Содержательная цель прогонки — заменить участок A′ S′ A″ S″ участком A* S*, где A* включает в себя в некотором смысле композицию анализа A′ и A″, а S* — композицию S′ и S″. Т.е. устранить необходимость в построении выражения S′, которое затем снова начнёт разбираться.

Так вот. Теории, позволяющей в рамках Рефала-4/Рефала Плюс полностью прогнать функцию пока не разработано. Исследования Сергея Романенко прервались на препринте Романенко, 1987б, где в конце так и написано:

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

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

Решение

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

Переходить в формализм Рефала-4 на уровне промежуточного представления пока не предлагается, предлагается так и оставаться в рамках базисного Рефала с условиями, которое сейчас используется между рассахаривателем и генератором RASL’а.

На самом деле уже заложены возможности для обработки частных случаев. Так например, алгоритм обобщённого сопоставления не требует L-выражения справа, вместо этого пытается решить уравнение до тех пор, пока методы решения с L-выражениями работают. Если эти методы становятся неприменимы, возвращается признак Undefined, говорящий о том, что решения нет (см. #156).

Кроме того, алгоритм уже имеет некоторые простые расширения, выводящие его за рамки L-выражений. Например, обнаруживается, что уравнение A e.X : B e.1 X e.2 решений не имеет. Если повторная переменная в правой части получила два s-значения (символы или s-переменные), то разрешается пара SVAL′ : SVAL″ (а она всегда разрешается) независимо от типа повторной переменной. Исходный алгоритм Турчина разрешает быть повторными только s-переменным.

Турчинский алгоритм прогоняет все предложения исходной функции за раз. Реализованный алгоритм прогоняет за раз по одному предложению. Если какое-то предложение прогнать нельзя, строится вызов «остаточной» функции Func*N, полученной из исходной вычёркиванием первых N предложений. Это тоже ad hoc расширение, позволяющее оптимизировать функции, у которых только часть предложений относятся к ограниченному Рефалу.

Предлагаемые расширения

Ревизия алгоритма обобщённого сопоставления

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

Открытые переменные в правой части уравнения

Пусть у нас есть такие две функции:

F {
  Pf = Rf1 <G e.X> Rf2;
}

G {
  Pg = Rg;
  …
}

Тогда, если Pf является L-выражением, а Pg содержит ровно одну открытую переменную, то к Pf можно применить подстановку e.X → Pg и таким образом прогнать G на одно предложение (получив вызов G*1).

В примере аргументом функции G является переменная e.X, но случай можно обобщить и для более сложных аргументов. В общем случае, если в наборе сужений для уравнения arg : Pg есть только одна открытая переменная, то подстановку набора сужений в L-выражение применять безопасно.

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

F {
  (e.X) e.Y (e.Z) = <G e.X (e.Y)>;
}

$DRIVE G;

G {
  e.A 1 e.B (e.C 2 e.D) = e.A e.D;
}

Но если в вызове заменить e.X на e.Z, семантика нарушится.

Кроме того, безопасно решать уравнение вида T1 … Tn : e.1 P e.2, где T1 … Tn — термы (символы, s-, t-переменные, скобочные термы). Можно статически перебрать все возможные удлинения переменной e.1 и получить упорядоченный набор решений. Случай на практике распространён, особенно в виде условий

Pat, A B C D : e.B s.X e.E = Res;

где переменная s.X входит в образец. На прогонку условий есть отдельная задача #248.

Не-L-образцы в вызывающей функции

Тема затронута в #231, там же есть примеры.

Если мы имеем не-L-образец в вызывающей функции, то можем применять сужения только к t- и e-переменным, которые (а) входят в образец один раз и (б) означиваются до цикла удлинения открытой переменной. Реализация этого расширения требует понятия неразменных переменных, предложенных в #231.

Повторные t- или e-переменные в правой части уравнения

Будем говорить, что выражение L-подобно, если стирание имён переменных обращает его в жёсткое выражение. Повторные переменные следует по-разному рассматривать в L-подобных образцах и не-L-подобных.

Текущая реализация алгоритма сначала рассматривает правую часть как жёсткое выражение, т.е. имена переменных в правой части не учитывает. Если правая часть оказалась не-L-подобной, то возвращается Undefined (либо «решений нет», если это удалось выявить). В противном случае в построенном наборе присваиваний находятся присваивания кратным переменным вида E1 ← var и E2 ← var, одно из присваиваний сохраняется в результате, второе стирается и решается уравнение вида E1 : E2.

Это уравнение, в отличие от исходного, симметрично и потенциально содержит слева и справа переменные одного сорта. В текущей реализации оно решается либо для случая, когда и E1, и E2 являются s-значениями (s-переменные или символы), или дословно совпадают. Способ решения уравнения S1 : S2 описан ещё Турчиным, он приводит либо к успеху, либо к сужению s.X → S2, либо к неуспеху. Второй случай, очевидно, тождество.

Поэтому первое направление ad hoc-расширений — это развитие методов решения уравнений вида E1 : E2.

Второе направление расширений — решение уравнений с не-L-подобной правой частью. Например, уравнений вида E : e.X e.Y (e.Y). Здесь нет открытых переменных, т.к. второе вхождение закрытое, а первое — повторное. Можно ли объединить методы решения уравнений с открытыми переменными с расширенными методами решения уравнений E1 : E2 предыдущего абзаца, чтобы решать уравнения этого вида — тут нужно разбираться.

Прогонка функций в предложениях с условиями

Текущая версия эти предложения просто игнорирует. (Это неправильно, поскольку должна на самом деле остужать функции drive и inline с холодными аргументами, поскольку они могут блокировать другие функции, которые можно специализировать.)

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

Но наиболее общее решение — учитывать разновидности переменных. Переменные из первого образца можно сужать, последующие — неразменные. Подробности в уже упомянутой задаче #231.

Прогонка функций с условиями

Если предложение прогоняемой функции имеет вид Pat = Res, то всё понятно. Сопоставляем аргумент с Pat, получаем набор присваиваний и сужений. Присваивания применяем к Res, сужения к вызывающей функции, вызов заменяем на модифицированный Res. Понятно, что тут тоже вагон нюансов, которые рассматрваются, например, здесь или в #230 и в #231.

Но вот если прогоняемое предложение имеет вид Pat, Res1 : Pat1 = Res;, становится уже сложнее. Допустим, мы решили уравнение arg : Pat. Что дальше? Подставить Res1 : Pat1 = Res на место вызова нельзя. Добавлять условие к предложению вызывающей функции? Наверное, можно в каких-то случаях, но слишком не очевидно влияние на семантику. Можно, наверное, подставить условие, если оно пассивно, но тоже надо думать.

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

Возврат условий из функции обобщённого сопоставления

Функция обобщённого сопоставления в норме или возвращает набор пар наборов сужений и присваиваний (в том числе пустой, если решений нет), или признак невозможности сопоставления Undefined.

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

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

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

Неразрешённые уравнения могут быть двух видов: вида E : L, где E — фрагмент аргумента, а L — фрагмент образца прогоняемой функции, и E1 : E2, где обе части — фрагменты аргумента, присвоенные повторной переменной. Для этих двух видов уравнений, очевидно, потребуются разные способы построить условие.

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

Mazdaywik commented 5 years ago

Задача подходит для курсовой работы по компиляторам. Какие пункты выносятся в учебную работу и в каком объёме — обсудим позже.

Mazdaywik commented 5 years ago

Соображение про расширения алгоритма обобщённого сопоставления

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

P : L

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

  1. L — L-выражение. Решается алгоритмом обобщённого сопоставления Турчина.
  2. P ≡ E — объектное выражение (не содержит переменных). Решение уравнения E : L есть обычное сопоставление с образцом, происходящее во время выполнения программы.
  3. P ≡ e.X — e-переменная. Решение уравнения есть сужение e.X → L (с точностью до имён переменных)

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

Вообще, если наоборот P — L-выражение, а L — произвольное выражение, то можно поменять местами части уравнения и решить обычным алгоритмом обобщённого сопоставления. Однако, надо иметь ввиду порядок удлинения открытых e-переменных и соответствующим образом упорядочить решения. Случай, когда P — L-выражение, покрывает граничные случаи 2 и 3.

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

UPD: вынесено в отдельную задачу: https://github.com/bmstu-iu9/refal-5-lambda/issues/322.

Mazdaywik commented 5 years ago

Задача не была выбрана в качестве курсовой.

Mazdaywik commented 4 years ago

Задача не была выбрана в качестве ВКР.

Mazdaywik commented 4 years ago

Про повторные переменные

Можно разрешить сопоставления с повторными te-переменными в сужениях, если они потом подставляются в L-образец. Проблем быть не должно.

Система присваиваний v.L1 ← v.R ⋀ v.L2 ← v.R означает, что переменные левой части v.L1 и v.L2 равны. Предлагается следующий алгоритм для этого частного случая:

Зачем нужна новая переменная и почему нельзя v.L1 → v.L2 или v.L2 → v.L1 в зависимости от того, какой тип меньше? Чтобы проще было проверять на неразменные переменные (#231). Неразменная переменная не может быть повторной. Если у нас есть список сужений v.L1 → v.New, v.L2 → v.New и список неразменных переменных, то достаточно проверить только левые части сужений. Для случаев вида v.L1 → v.L2 нужно (а) искать сужения с повторными переменными, (б) в них проверять обе стороны. Первый вариант проще.

Таким же образом нужно будет переделать и сопоставление с повторными s-переменными, т.к. и они тоже могут быть неразменными. Например, если s-переменная появилась в образце условия:

F {
  s.X e.Y, <G e.Y> : s.Z = <Eq s.X s.Z>;
}

$DRIVE Eq {
  s.1 s.1 = True;
  s.1 s.2 = False;
}

Если разрешать сужения s.X → s.Z или s.Z → s.X или s.X → s.New ⋀ s.Z → s.New, то получится вот что:

F {
  s.New e.Y, <G e.Y> : s.New = True;
  s.X e.Y, <G e.Y> : s.Z = False;
}

Вызов <G e.Y> в условии будет вычисляться дважды.

Mazdaywik commented 4 years ago

Соображение про открытые переменные

Допустим, у нас есть уравнение вида e.X : e.B P e.E в системе уравнений. Мы делаем шаг решения вида e.X → e.1 e.2, e.1 ← e.B, e.2 : P e.E и продолжаем решать систему.

Ограничение: в продолжении решения этой системы должно быть не более одного решения.