Аксиомы для оптимизатора

[Mazdaywik]

Эта задача является логическим продолжением задачи #122.

Философия глубокой оптимизации в Рефале-5λ

Сложилось (#91), что глубокие оптимизации программ в Рефале-5λ осуществляются при помощи пользовательских подсказок — какие функции можно прогонять, какие — только встраивать, какие специализировать и по каким аргументам.

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

Хотя, если какая-то разметка сравнительно тривиальна — её можно доверить и компьютеру (#165).

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

Мотивация

Есть такая интересная оптимизация — сокращённая дефорестация. Подробное её описание применительно к Рефалу я давал здесь (рекомендую почитать):

https://groups.google.com/forum/#!topic/refal/UWAVx6wY35c

Если кратко: если одну функцию описать в терминах катаморфизма Fold, а вторую — в терминах построения представления Чёрча, то их композиция избегает построения промежуточных структур данных. Например, для объектных выражений без скобок:

/*
  <Fold (e.Z s.T s.C) t.Term*> == e.Res
  e.Z == e.Res
  <s.T t.Term> == e.Res
  <s.C (e.Res) (e.Res)> == e.Res
  s.C ассоциативна, e.Z — нейтральный элемент для s.C
*/
Fold {
  (e.Z s.T s.C) /* пусто */ = e.Z;
  (e.Z s.T s.C) t.Term = <s.T t.Term>;
  (e.Z s.T s.C) e.Terms
    = <Split e.Terms> : (e.Left) e.Right
    = <s.C
        (<Fold (e.Z s.T s.C) e.Left>)
        (<Fold (e.Z s.T s.C) e.Right>)
      >;
}

Id { t.X = t.X }
Cat { (e.X) (e.Y) = e.X e.Y }

/*
  <Build s.Func e.Arg> == <s.Func (пусто &Id &Cat) e.Arg>
  <s.Func (e.Z s.T s.C) e.Arg> == …
  e.Z, s.T и s.C см. в описании Fold
*/
Build {
  s.Func e.Args = <s.Func (/* пусто */ &Id &Cat) e.Args>;
}

Здесь правилом сокращения будет

<Fold (e.Z s.T s.C) <Build s.Func e.Args>> == <s.Func (e.Z s.T s.C) e.Args>

Чтобы оптимизация работала, компилятор должен знать это правило. Авторы основополагающей статьи предлагали описывать foldr и build (для их компилятора Хаскеля) как «интринсики» (intrinsic function), которые распознаются компилятором.

Но это костыль. Более того, он ограничивает пользователя только одной сокращаемой структурой данных — той, для которой эти интринсики определены. Тем более, что функции Fold и Build высокоуровневые, в то время как интринсики (в компиляторах Си/Си++) обычно определяются для таких низкоуровневых вещей, которые условно оборачивают одну инструкцию процессора. Например, атомарные инструкции или memcpy.

Более общее решение — определить синтаксис для задания подобных правил сокращения.

Предлагаемый синтаксис

Предлагается расширить синтаксис функций — в теле функции могут указываться не только предложения, генерирующие целевой код, но и «аксиомы», которые кодогенератор игнорирует, но оптимизатор использует:

Function {
  pattern = result;
  . . .
  pattern = result;

$AXIOMS
  axiom-pattern = result;
  . . .
  axiom-pattern = result;
}

Предложения после ключевого слова $AXIOMS описывают правила преобразования программ для оптимизатора. Семантика таких образцов отличается от обычной. Например, не работает правило выбора сопоставления для открытой e-переменной. Кроме того, в левых частях предложений могут присутствовать скобки активации!

Например, пусть у нас есть функция фильтрации:

<Filter s.Filter t.Term*> == t.Term*
<s.Filter t.Term> == True | False

Очевидно, для такой функции справедливы следующие аксиомы:

<Filter s.F e.Terms1 e.Terms2> == <Filter s.F e.Terms1> <Filter s.F e.Terms2>
<Filter s.F1 <Filter s.F2 e.Terms>> == <Filter <And s.F1 s.F2> e.Terms>

где функция And порождает новую функцию, которая возвращает True, когда возвращают True и s.F1, и s.F2. Здесь e.Terms1 и e.Terms2 означают произвольные результатные выражения.

Функция Filter с аксиомами может быть определена так:

/*
  <Filter s.Filter t.Term*> == t.Term*
  <s.Filter t.Term> == True | False
*/
Filter {
  s.Filter t.Term e.Terms
    = <s.Filter t.Term>
    : {
        True = t.Term <Filter s.Filter e.Terms>;
        False = <Filter e.Terms>;
      };

  s.Filter /* пусто */ = /* пусто */;

$AXIOMS
  s.Filter e.Terms1 e.Terms2
    = <Filter s.Filter e.Terms1> <Filter s.Filter e.Terms2>;

  s.Filter1 <Filter s.Filter2 e.Terms>
    = <Filter
        {
          t.Term, <s.Filter1 t.Term> : False = False;
          t.Term = <s.Filter2 t.Term>;
        }
        e.Terms
      >;
}

Образец s.Filter e.Terms1 e.Terms2 в первой аксиоме можно понимать так: «если можно найти какую-нибудь подстановку, что s.Filter e.Terms1 e.Term2 превращается в аргумент <Filter …>, то вызов <Filter …> можно заменить на два вызова». Причём, очевидно, обе переменных должны быть непустые, иначе это будет не оптимизация. А как именно делить аргумент — деталь реализации. Но если пользователь позволил аргумент делить, значит, понимает, что любое деление допустимо.

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

Примеры:

<Filter &Even <Load 'numbers1.txt'> <Load 'numbers2.txt'>>
  ↓  ↓  ↓
<Filter &Even <Load 'numbers1.txt'>> <Filter &Even <Load 'numbers2.txt'>>

<Filter &Even <Filter &NotPrime e.Numbers>>
  ↓  ↓  ↓
<Filter
  {
    t.Term, <Even t.Term> : False = False;
    t.Term = <NotPrime t.Term>;
  }
  e.Numbers
>

Пример описания сокращённой дефорестации:

/*
  <Fold (e.Z s.T s.C) t.Term*> == e.Res
  e.Z == e.Res
  <s.T t.Term> == e.Res
  <s.C (e.Res) (e.Res)> == e.Res
  s.C ассоциативна, e.Z — нейтральный элемент для s.C
*/
Fold {
  (e.Z s.T s.C) /* пусто */ = e.Z;
  (e.Z s.T s.C) t.Term = <s.T t.Term>;
  (e.Z s.T s.C) e.Terms
    = <Split e.Terms> : (e.Left) e.Right
    = <s.C
        (<Fold (e.Z s.T s.C) e.Left>)
        (<Fold (e.Z s.T s.C) e.Right>)
      >;

$AXIOMS
  (e.Z s.T s.C) e.Terms1 e.Terms2 = <Fold (e.Z s.T s.C) e.Terms1> <Fold (e.Z s.T s.C) e.Terms2>;

  (e.Z s.T s.C) <Build s.Func e.Args> = <s.Func (e.Z s.T s.C) e.Args>;
}

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

Нюанс: порядок вычисления

Очевидно, применение аксиом должно работать вместе со встраиваниями и специализациями (#91). Поскольку если одна функция определена через Fold, а другая — через Build, то сократить их можно только после встраивания (inline) их определений в точку вызова.

При этом, некоторые функции, содержащие аксиомы, могут сами и встраиваться, и специализироваться. Например, функцию Filter имеет смысл специализировать по предикату, а функцию Fold — по e.Z s.T s.C. Если специализировать раньше, то в специализации также должны сохраняться аксиомы, но в специализированном виде.

Саму функцию Build тоже имеет смысл встраивать, ведь она достаточно проста для этого (одно простое предложение). Также имеет смысл объявлять специализируемыми функции, которые Build вызывает, по тем же e.Z s.T s.C (даже в письме в рассылку я специализировал Range-B).

Другой нюанс в том, что вызов функции перестаёт быть вызовом в чистом виде. Он также становится неким конструктором, который разбирается в левой части аксиомы. И если мы функцию Build раскроем раньше времени, то аксиому в Fold уже не увидим. И не упростим. Это очень тонкий нюанс.

Корректность и верификация аксиом

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

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

[Mazdaywik]

@TonitaN, как тебе?

[Mazdaywik]

Нюанс 2: семантика переменных в аксиомах

При сопоставлении с образцом объектного выражения s-переменная сопоставляется с символом, t-переменная — с символом или скобочным термом (круглыми скобками), e-переменная — с произвольным выражением.

При сопоставлении результатного выражения с образцом аксиомы может ли s-переменная результатного выражения сопоставляться с s-переменной образца? Что может сопоставляться с t-переменной: могут ли с ней сопоставляться термы в угловых скобках и переменные?

Вероятно, надо ввести специфические типы переменных для аксиом, которые сопоставляются с синтаксическими конструкциями вроде «переменная» или «вызов функции».

Или поступить иначе: аксиомы описывать в метакоде. Выглядит очень многообещающе, надо обдумать, к каким чудесам это приведёт… Но могут понадобиться переменные «с поднятием 1» (в терминах MST-схем) для описания значений без переменных и вызовов функций. Или можно без этого обойтись…

[Mazdaywik]

Всё уже придумано для нас, но только для Хаскеля:

https://www.microsoft.com/en-us/research/wp-content/uploads/2001/09/rules.pdf

Надо изучить эту статью.

[Mazdaywik]

Задача в некоторой степени пересекается с #260 (интринсики для встроенных функций). Просто добавляю перекрёстную ссылку, дополнительных мыслей у меня нет.

[Mazdaywik]

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

Ещё соображение. Возможно, аксиомы не нужно внедрять в язык, а вместо этого написать какой-нибудь интерфейс плагинов, который позволяет писать плагины переписывания кода.