search

bmstu-iu9 / refal-5-lambda

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

Древесные оптимизации нарушают семантику #276

Open Mazdaywik opened 4 years ago

Mazdaywik commented 4 years ago

Введение. Гарантии для равенства замыканий

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

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

Например:

Eq {
  t.Eq t.Eq = True;
  t.X t.Y = False;
}

F {
  e.X = <Eq (e.X) (e.X)>;
}

Функция F всегда должна возвращать True.

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

Рефал-5λ поддерживает вложенные функции в результатных выражениях. Во время выполнения для вложенных функций порождаются замыкания — значения типа «символ» (сопоставимые с s-переменными), которые можно вызывать как функции. Замыкания могут захватывать контекст.

Возникает вопрос: как сравниваются на равенство два замыкания? Для Простого Рефала в manul.pdf были определены следующие ограничения:

  1. Экземпляры функций, как и другие атомы, копируются за константное время.
  2. Передача управления на указатель на функцию выполняется за константное время. Передача управления на замыкание может выполняться как за константное время, так и за время пропорциональное размеру контекста. Последнее возможно, если в поле зрения присутствует несколько копий данного замыкания, поэтому для вызова каждого из экземпляров требуется своя копия контекста — такова списковая реализация. 〈…〉
  3. Два экземпляра функции, полученные путём копирования одного атома, равны.
  4. Два замыкания, построенные из текстуально разных функциональных блоков, не равны.
  5. Два замыкания, имеющие разное содержимое элементов контекста, не равны.
  6. Указатели на функцию равны тогда и только тогда, когда они указывают на одну и ту же функцию.

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

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

F1 { = { = } }
F2 { e.X = { = e.X } }

Eq { 〈см. выше〉 }

Test {
  e.X
    = <Prout <Eq <F1> <F1>>>
      <Prout <Eq <F2 e.X> <F2 e.X>>>
}

Функция F1 создаёт замыкание с пустым контекстом, а для таких случаев вместо объекта замыкания создаётся просто указатель на неявную глобальную функцию (&F1\1). Поэтому первый вызов распечатает True. Так было сделано с самой первой реализации вложенных функций в Simple Refal.004.

Второй вызов по умолчанию распечатает False, поскольку два вызова <F2 e.X> создадут два объекта замыкания, которые сравнятся по ссылке. Но если функции F2 и Eq прогнать (или даже встроить), то мы получим <Prout True>. Реализованный алгоритм обобщённого сопоставления с образцом допускает повторные переменные любого типа, причём сопоставление считается успешным, если значения этих переменных текстуально совпадают (если не совпадают и тип переменной не s — результат не определён). Поэтому здесь сопоставление будет успешным.

Далее, мы рассмотрим три примера. Один с мнимым нарушением семантики, два других — с реальным.

Воспроизведение ошибки

Пример 1. Мнимое нарушение семантики при прогонке

$ENTRY Go {
  e.X
    = <Eq <Clo e.X> <Clo e.X>> : False
    = /* пусто */
}

$INLINE Clo, Eq;

Clo { e.X = { = e.X } }

Eq {
  s.X s.X = True;
  s.X s.Y = False;
}

Скачать: closures-neq-drive.ref.

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

Пример 2. Реальное нарушение семантики при прогонке

$ENTRY Go {
  e.X
    = <Eq <Dup { = e.X }>> : True
    = /* пусто */
}

$INLINE Dup;

Dup { e.X = e.X e.X }

Eq {
  s.X s.X = True;
  s.X s.Y = False;
}

Скачать: closures-eq-drive.ref.

Здесь встраивается вызов Dup, в результате чего Eq вызывается с аргументом

<Eq {{ &Go\1 e.X }} {{ &Go\1 e.X }}>

Во время выполнения создаются два одинаковых объекта замыкания. Но, поскольку замыкания сравниваются по ссылке, они оказываются не равны.

Пример 3. Реальное нарушение семантики при специализации

$ENTRY Go {
  e.X = <S { = e.X }>;
}

$SPEC S s.STAT;

S {
  s.X = <Eq s.X s.X> : True = /* пусто */;
}

Eq {
  s.X s.X = True;
  s.X s.Y = False;
}

Скачать: closures-neq-spec.ref.txt.

Причина похожа на предыдущую — строятся два одинаковых экземпляра замыкания вместо копирования одного. Только теперь путём размножения значения статической переменной. Специализированная функция S@1 выглядит так:

S@1 {
  e.X#1 = <S=1 <Eq {{&Go\1 (e.X#1)}} {{&Go\1 (e.X#1)}}>>;

  e.X#1 = <S@0 {{&Go\1 (e.X#1)}}>;
}

Решение

А вот однозначного решения тут пока не видно — везде есть компромиссы.

Приемлемыми мне видятся только последние три варианта. А может даже, последние два.

Буду думать летом после завершения #260, #256, #252, #253.

Mazdaywik commented 4 years ago

Варианты с запретом на сравнение замыканий и нарушением аксиоматики отбрасываем. Рассмотрим приемлемые варианты.

Научить прогонку и специализацию не нарушать семантику

Тут возможны два пути: сужения и расширения.

Путь сужения — не генерировать опасные конструкции

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

Нечто похожее уже делается — в прогонке запрещены сужения в замыкания, а в специализации построенные функции проверяются на «осмысленность». Цель одна и та же — не дать замыканиям просочиться в образец, что синтаксически некорректно.

К сожалению, такой консервативный подход лишит возможности оптимизировать многие полезные функции, вроде, Map. А ведь древесные оптимизации создавались фактически ради них.

Путь расширения — усложнить логику для сохранения семантики

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

Правая часть вида

<F {{ &G\1 (e.X) }}> <H {{ &G\2 (e.Y) }}>

будет неявно преобразовываться к виду

$genkey : s.k1, $genkey : s.k2, <F {{ &G\1 s.k1 (e.X) }}> <H {{ &G\2 s.k2 (e.Y) }}>

Здесь $genkey генератор ключа, ключи добавляются в объекты замыканий и используются для сравнения на равенство. Теперь, если функции F и H имеют вид

$INLINE F { s.X = s.X '+' s.X }

$SPEC H s.STAT;
H { s.X = s.X '*' s.X }

то правая часть преобразуется в

$genkey : s.k1,
$genkey : s.k2,
{{ &G\1 s.k1 (e.X) }} '+' {{ &G\1 s.k1 (e.X) }} <H@1 s.k2 e.Y>
…
H@1 {
  s.k2 e.Y = {{ &G\2 s.k2 (e.Y) }} '*' {{ &G\2 s.k2 (e.Y) }};
}

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

Заметим, что в этом случае оптимизация сохраняет поведение и для «зеркального» случая: когда в разные моменты времени создаются два замыкания с одинаковым контекстом.

Пример:

F { e.X = <G e.X> <G e.X> }

$INLINE G { e.X = { = e.X } }

После рассахаривания получим:

F { e.X = <G e.X> <G e.X> }

$INLINE G {
  e.X = $genkey : s.k, {{ &G\1 s.k (e.X) }};
}
G\1 { s.k (e.X) = e.X }

После встраивания получим:

F {
  e.X = $genkey : s.k1, $genkey : s.k2, {{ &G\1 s.k1 (e.X) }} {{ &G\1 s.k2 (e.X) }}
}

Ключи будут разные, а значит, объекты замыканий также будут не равны.

Причём ключом может являться сам указатель на объект замыкания. Операция $genkey создаёт «пустое» замыкание. Операция создания замыкания смотрит, пустое ли оно. Если пустое, ему присваивается контекст. Если не пустое — то ничего не делается. Фактически, на замыкание можно смотреть как на динамический ящик, который создаётся пустым, и которому можно присвоить только один раз.

Сейчас Рефал-5λ поддерживает только безымянные вложенные функции. Предлагаемая реализация с разделением создания замыкания на две фазы позволяет реализовать и именованные взаимно-рекурсивные вложенные функции.

Сравнивать замыкания по значению

Самый простой в реализации подход к решению этой проблемы. Минимальные правки рантайма.

Недостаток — быстродействие. Но, с другой стороны, пока на Рефале-5λ никто не использует стиль программирования, требующий сравнения замыканий на равенство. Приравниваются обычно пассивные значения (или глобальные функции как метки АТД-скобок), функции обычно только вызываются.

Отказаться от символов-замыканий

Почему замыкания представляются s-переменными? Потому что так было в Рефале-7 s-переменная — это значение, которое невозможно при помощи сопоставления с образцом разбить на составные части.

Замыкание состоит из указателя на глобальную функцию и контекста в виде объектного выражения определённого формата. При этом глобальная функция ожидает именно такого формата от контекста. Если дать возможность пользователю манипулировать содержимым замыкания, то он может нарушить инварианты. Поэтому для скрытия реализации замыкания считаются s-переменными. В общем, как-то так это рационализируются. На самом деле, я списал из Рефала-7, когда делал вложенные функции в Простом Рефале.

Но Рефал-5λ допускает и другую форму инкапсуляции — АТД-скобки. Получить доступ к содержимому можно только записав имя функции после открывающей квадратной скобки.

Если имя АТД-терма не будет доступно пользователю (вроде F\1), то инкапсуляция также будет обеспечена. Замыкания будут просто скобочными термами, поэтому приравниваться по значению будут совершенно естественным образом. Копироваться они будут за линейное время, при этом явно. Вызов будет осуществляться за константное время.

Также потребуется определить семантику для вызова АТД-термов. Тут возможны два варианта:

  1. <[Func e.X] e.Y> → <Func e.X e.Y>
  2. <[Func e.X] e.Y> → <Func [Func e.X] e.Y>

Какой из них предпочесть, пока неясно.

Преимуществом подхода является упрощение и языка, и компилятора. В языке получается на один конструкт меньше (объекты-замыкания), АТД-термы становятся богаче по возможностям (не только инкапсуляция). Компилятор и рантайм станут немного проще.

Недостаток — существенная переделка языка и компилятора.

Что выбрать?

Не знаю.

Mazdaywik commented 4 years ago

В задаче #160 рассматривается вариант, когда после специализации замыкания у него не остаётся контекста (https://github.com/bmstu-iu9/refal-5-lambda/issues/160#issuecomment-623350268). Для такого замыкания можно или строить вырожденный объект замыкания, или заменять на указатель на функцию.

В случае замены на указатель на функцию в https://github.com/bmstu-iu9/refal-5-lambda/issues/160#issuecomment-623350268 рассматривается слабое изменение поведения программы — функция Type возвращает не тип замыкания, а тип указателя на функцию. Но есть и более сложная проблема в контексте настоящей задачи.

Рассмотрим программу:

$ENTRY Test {
  e.X
    = { e.Y = e.X e.Y } : s.Func
    = <Eq s.Func <S s.Func e.X>>;
}

$SPEC S s.FUNC e.ARG;

S {
  s.F e.X = s.F <D e.X>;
}

$DRIVE D;

D {
  'abc' = ;
  'a' e._ = ;
  e._ = ;
}

Eq {
  s.Eq s.Eq = True;
  s._ s._ = False;
}

После специализации, прогонки и специализации замыкания мы получим следующую функцию S:

S@1 {
  'abc' = &Test=1\1@1;  /* № 1 */
  'a' e.X = {{ &Test=1\1@2 (e.X) }};  /* № 2 */
  e.X = {{ &Test=1\1 (e.X) }};  /* № 3 */
}

* Неспециализированная функция
Test=1\1 {
  (e.X) e.Y = e.X e.Y;
}

Test=1\1@1 {
  e.Y = 'abc' e.Y;
}

Test=1\1@2 {
  (e.X) e.Y = 'a' e.X e.Y;
}

В неоптимизированной программе замыкание формируется один раз — в функции Test, затем оно «просеивается» через S, откуда возвращается неизменным. Функция Eq вернёт True.

В оптимизированной программе присваивание встроится — конструкторы одного и того же замыкания будут находиться в аргументах Eq и S. Функция S проспециализируется, конструктор упадёт в неё. А там размножится в результате прогонки.

В трёх ветвях функции S@1 мы будем строить для замыкания:

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

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

Запрет на дублирование замыканий слишком жёсткий — не даёт специализировать такие функции, как Map. Можно придумать и более сложный анализ, который позволял бы и Map оптимизировать, и сохранять семантику. Для этого нужно при специализации функции передавать в неё и переменные из контекста, и указатель на замыкание, создаваемый вовне. При этом внутри функции нужно помнить, что эта s-переменная хранит уже известное значение. Для таких «заимствованных» замыканий специализация замыканий работать уже не должна. Но всё это дико сложно, особенно в рамках текущего формализма, поэтому рассматривать дальше этот вариант не будем.

Mazdaywik commented 4 years ago

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

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

Mazdaywik commented 3 years ago

Замыкания — типы значений, квадратные скобки?

В последнее время я склоняюсь к мысли реализовать замыкания как квадратные скобки, как в Модульном Рефале:

https://github.com/Mazdaywik/mrefal/blob/a0e62511207544ca6102a1e6b0fb94eee7c93681/Documentation/%D0%96%D1%83%D1%80%D0%BD%D0%B0%D0%BB/Changes.txt#L8413-L8534

Преимущества и недостатки:

Также потребуется определить семантику для вызова АТД-термов. Тут возможны два варианта:

  1. <[Func e.X] e.Y> → <Func e.X e.Y>
  2. <[Func e.X] e.Y> → <Func [Func e.X] e.Y>

Можно добавить и третий вариант:

<[Func e.X] e.Y> → <Func (e.X) e.Y>

Его преимущества: по сравнению с 1 не сливается содержимое терма с аргументом, по сравнению с 2 не требуется дополнительных аллокаций памяти.

Mazdaywik commented 3 years ago

Развитие идей предыдущего комментария

Про специализацию замыканий

Наивный способ специализации замыканий работать не будет

Если «наивно» заменить (ClosureBrackets …) на (ADT-Brackets …), то специализация замыканий как таковая станет невозможной. Ведь квадратные скобки могут использоваться не только для представления замыканий компилятором, их может использовать программист для создания собственных типов данных. В качестве тега инкапсулирующих скобок может быть использована не только пустая функция, но и вообще любая локальная (а почему бы и нет?). Такие скобочные термы, очевидно, специализировать нельзя, т.к. пользователь будет немало удивлён.

Можно придумать и более изощрённые варианты, например, угадывать специализируемые квадратные скобки по суффиксу. Имена без суффиксов или с суффиксом ~N оптимизировать нельзя, остальные — можно.

Сложные случаи специализации замыканий

Я пока затрудняюсь исчерпывающе описать ситуации, когда специализировать замыкания безопасно. Однако, можно выделить ситуацию, когда специализировать их опасно. Рассмотрим сначала примеры:

Из приведённых примеров можно сделать такой вывод: нельзя специализировать замыкания в экземплярах специализированных функций. Пример из https://github.com/bmstu-iu9/refal-5-lambda/issues/276#issuecomment-623372133 демонстрирует специализацию «чужого» замыкания, который попал внутрь экземпляра из сигнатуры. Второй пример демонстрирует специализацию «своего» замыкания (замыкания функции F\1).

$ENTRY F {
  (e.X) (e.Y) = <{ s.F = <Eq <s.F e.X> <s.F e.Y>> } { e.A = { = e.A } }> <D e.X>
}

$DRIVE D, Eq;

D {
  'abc' = 1;
  'a' e._ = 2;
  e._ = 3;
}

Eq {
  t.X t.X = True;
  t._ t._ = False;
}
$EXTERN F;

$ENTRY Go {
  /* пусто */
    = <Prout
        <F ('abc') ('abc')>
        <F ('abcd') ('abcd')>
        <F ('bcd') ('bcd')>
      >
}

Актуальная реализация в неоптимизированном варианте напечатает False 1 False 2 False 3, в оптимизированном — False 1 False 2 True 3. Предполагаемая реализация с абстрактными скобками без оптимизации выдаст True 1 True 2 True 3 с оптимизацией — False 1 False 2 True 3. Предполагаемая реализация с предполагаемой оптимизацией #322 может выдать и True 1 True 2 True 3. Но в более хитрых примерах и #322 не спасёт.

Но и в этом примере можно сказать, что выполняется специализация «чужого» замыкания — функции F\2\1 внутри функции F. «Родной» функцией для F\2\1 является функция F\2.

Со «своими» замыканиями всё проще:

$ENTRY F {
  e.X = { = e.X } <D e.X>
}

$DRIVE D;

D {
  'abc' = 1;
  'a' e._ = 2;
  e._ = 3;
}

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

В оптимизированной версии инварианты сохранятся. Актуальная реализация для <F 'abc'> будет возвращать один и тот же указатель на глобальную функцию, но это никто не запрещает. У предполагаемой реализации ссылочная прозрачность (в определении Андрея Климова) тоже сохранится.

Вызов <Type <F 'abc'>> в актуальной реализации меняет свой результат при оптимизации. В предполагаемой будет менять, если построение [F\1@1] будет сокращаться до &F\1@1.

Так что следует запрещать специализацию тех замыканий, стирание одного суффикса имени которого даёт имя, отличное от имени функции, внутри которой находится замыкание. Отдельный вопрос с замыканиями в условиях — тут мне пока не очевидно.

Однако обратное неверно. Можно привести пример, когда специализация «своего» замыкания опасна. (Это не комментарий сам себе противоречит, это моя мысль развивается в процессе написания.) Это слегка модифицированный первый пример:

$ENTRY F {
  e.X = <G { = e.X }> <D e.X>
}

$DRIVE G, D, Eq;

G {
  s.F = <Eq <S s.F> s.F>
}

D {
  'abc' = 1;
  'a' e._ = 2;
  e._ = 3;
}

Eq {
  t.X t.X = True;
  t._ t._ = False;
}

$SPEC S t.STAT;

S { t.F = t.F }

Вызов G раскроется, получится <Eq <S {{ &F\1 e.X }}> {{ &F\1 e.X }}> <D e.X>. Потом прогонится вызов D, сужения для e.X горизонтально распространятся. Прогонять нечего. Выполнится проход специализации. Сначала он построит экземпляры для S, а потом для замыкания F\1.

Если в S проспециализировать экземпляр тоже, то для АТД-замыканий семантика программы сохранится. Но мы выше решили, что специализировать замыкания в экземплярах нельзя, но тогда семантика будет нарушаться.

Вывод

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

Возможно, единственный вариант сохранить и семантику, и эту оптимизацию — хранить в замыканиях уникальные идентификаторы (см. $genkey в https://github.com/bmstu-iu9/refal-5-lambda/issues/276#issuecomment-612976116) и при сравнении на равенство использовать их, а не ссылку на объект (как сейчас) или содержимое (как предполагается).

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

Скобки каррирования?

Рассмотрим случай, когда замыкания всё-таки станут типами-значениями. Семантика их вызова будет выглядеть так:

<[F e.X] e.Y> → <F e.X e.Y>

(поведение по аналогии с Apply)

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

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

Однако, инкапсуляция при помощи квадратных скобок становится наоборот хаком, а синтаксические ограничения на квадратные скобки повисают в воздухе. Во-первых, неочевидным становится потребность разбирать каррированное значение в образце. Во-вторых, почему, если в переменной s.f или t.f находится функция, нельзя писать в результатном выражении [s.f e.a] или [t.f e.a]? В третьих, почему нельзя писать образцы вида [s.f e.a], почему известное имя функции обязательно?

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

Mazdaywik commented 3 years ago

Сегодня в ИПМ имени М.В. Келдыша онлайн проходил семинар — я читал доклад о проблеме и предложил два варианта решения:

https://mazdaywik.github.io/direct-link/2021-05-17-Konovalov-Closures-and-Optimizations-Refal-5-lambda.pdf

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