Про неподвижную точку суперкомпиляции

[Mazdaywik]

(продолжаем разговор, начатый здесь #328)

@TonitaN:

Кстати, по поводу неподвижной точки — никто не знает, есть ли она у суперкомпилятора SCP4 при многократном пропускании через inref. Интуитивно вроде есть, а теоретически непонятно.
А первый вариант алгоритма Хигмана-Крускала (где имена переменных не просто стирались, а нумеровались) тоже интересный был, хотя и сырой. Будет очень интересно, если кто-нибудь докажет про него, что это almost-well-relation (не знаю, как сейчас называют wqo без транзитивности).

Это новая функция GitHub’а — дискуссии. Типа заявок (issues), но они не обязывают к выполнению. @TonitaN, давай опробуем её?

Кстати, по поводу неподвижной точки. А есть ли она у MSCP-A, хотя бы интуитивно?

Я могу сказать про необходимое условие неподвижной точки — это перестройка сверху. Поскольку перестройка снизу будет гарантированно на каждом применении суперкомпилятора разворачивать виток цикла (рекурсии).

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

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

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

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

Кстати, знаешь как сформулировать бездревесную форму для Рефала? В ИПМ я мудрил много, а на самом деле её определение гораздо проще.

По поводу суперкомпиляции. Я вручную просчитывал примеры суперкомпиляции программ, где используется отношение Хигмана-Крускала как отношение похожести и вариант ГСО как алгоритм обобщения. У меня в процессе складывалось впечатление, что такая суперкомпиляция неизбежно будет идемпотентной. Повторная суперкомпиляция будет выявлять сходство тех же конфигураций, и их обобщение будет тем же самым, базисные конфигурации будут в тех же местах. Доказать не могу, но такое ощущение при просчёте примеров было.