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

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

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

Например:
```Refal5
Eq {
t.Eq t.Eq = True;
t.X t.Y = False;
}

F {
e.X = ;
}
```
Функция `F` всегда должна возвращать `True`.

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

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

Возникает вопрос: как сравниваются на равенство два замыкания? Для Простого Рефала в [`manul.pdf`](https://github.com/bmstu-iu9/refal-5-lambda/blob/a5b0b5bf6f8ddc451c6f5ef5be1129fa5befa196/doc/historical/manul.pdf) были определены следующие ограничения:

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

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

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

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

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

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

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

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

Воспроизведение ошибки
==================
Пример 1. Мнимое нарушение семантики при прогонке
-----------------------------------------------------------------
```Refal5
$ENTRY Go {
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](https://github.com/bmstu-iu9/refal-5-lambda/files/4469142/closures-neq-drive.ref.txt).

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

Пример 2. Реальное нарушение семантики при прогонке
------------------------------------------------------------------
```Refal5
$ENTRY Go {
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](https://github.com/bmstu-iu9/refal-5-lambda/files/4469117/closures-eq-drive.ref.txt).

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

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

Пример 3. Реальное нарушение семантики при специализации
-------------------------------------------------------------------------
```Refal5
$ENTRY Go {
e.X = ;
}

$SPEC S s.STAT;

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

Eq {
s.X s.X = True;
s.X s.Y = False;
}
```
Скачать: [closures-neq-spec.ref.txt](https://github.com/bmstu-iu9/refal-5-lambda/files/4469160/closures-neq-spec.ref.txt).

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

e.X#1 = ;
}
```

Решение
======
А вот однозначного решения тут пока не видно — везде есть компромиссы.
* Запретить сравнивать на равенство замыкания — останавливать аварийно программу при таком сравнении. Решение слишком контринтуитивное — программа будет падать «на ровном месте» с точки зрения пользователя. При написании повторных переменных придётся задумываться: а не могут ли там оказаться замыкания?
* Отказаться от принципа, что значения, созданные копированием, равны. Тоже контринтуитивное решение, да и прогонка повисает без серьёзных оснований.
* Усложнить прогонку и специализацию — придумать «фокусы», которые отслеживали бы равные ссылки во время преобразований.
* Сравнивать замыкания по значению. Это отказ от сравнения s-переменных за константное время. В принципе, отказ не такой страшный, поскольку для замыканий и вызов функции не выполняется за константу (копируется контекст).
* Вообще отказаться от символов-замыканий. Можно сделать замыкания t-переменными, скрестив их с абстрактными скобками. Решение красиво тем, что существенно упрощает и семантику языка, и реализацию компилятора. Недостаток — слишком большое изменение.

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

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