Два правила завершаемости поодиночке дают 54 и 74, а вместе — 574: узкое место в их произведении

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

Почему сумма больше слагаемых. Цикл рекурсии доказывается ЦЕЛИКОМ или не доказывается вовсе, и в компиляторе на flang эти циклы огромные: обход AST в self/emit-c.flang — одна компонента примерно на 60 функций. Достаточно одного ребра, на котором спуск не виден, чтобы отказала вся компонента. Первое правило чинит рёбра, где спуск виден, но стоит не на той позиции; второе — рёбра, где спуск спрятан за «Взять поле» от узел. В больших компонентах есть и те, и другие, поэтому каждое правило поодиночке оставляет компоненту красной.

Что именно проверялось.

1. Размерные графы. На каждом ребре вызова строится отношение «довод вызванного j получен из довода зовущего i» с пометкой «строго меньше» (часть значения) или «не больше» (тот же довод). Цикл доказан, если у всякого идемпотентного состава этих отношений есть строго убывающая петля. Нынешнее правило требует куда больше: ОДНУ И ТУ ЖЕ позицию и СТРОГОЕ убывание на КАЖДОМ ребре.
2. Потолок вызова. Считается, что всякий вызов возвращает строгую часть своего первого довода. Это неправда вообще — это ровно та оценка сверху, которую дал бы типизированный AST: спуск через поиск поля стал бы виден анализу как поле образца, а сегодня он не виден никак.

Чем подтверждено. Ветка vypusk/zavershaemost. Копии flang/src/totality.mjs правились ВНЕ дерева, в рабочем каталоге, и прогонялись тем же приёмом, что в only-293-of-2242-functions-lacked-a-mark-the-rest-lack-rules (все функции помечены тотальными). Прогон каждого опыта — 25–57 с по 284 файлам. Опорное число до опытов: 1951 обычная функция (счётом опыта), из них 1019 корней.

Чем ограничено. Второй опыт — оценка СВЕРХУ, а не готовое правило: принять его как правило нельзя, это сделало бы анализ неверным. Он отвечает на вопрос «сколько стоит долг про типизированный AST», а не «какое правило написать». Первый опыт — настоящий критерий (size-change termination), но написать его надо дважды: в flang/src/totality.mjs и в flang/self/totality.flang, с побайтово совпадающими текстами отказов.

Третье правило дешевле обоих и меряется отдельно. Нынешнее числовое правило принимает «довод убывает постоянным шагом и ограничен снизу». Зеркало — «растёт постоянным шагом и ограничен сверху доводом, который вдоль цикла не меняется» — верно тем же рассуждением: цепочка не длиннее (K − v₀)/шаг. Потолок этого правила измерен так же, как остальные (в опыте верхняя граница не проверялась вовсе, поэтому число — оценка сверху): 152 функции. Из них 120 — в восьми слоях печати self/emit-*.flang, остальные в примерах, где живёт «Числа от и до» и её близнецы на четырёх поверхностях. Настоящее правило даст меньше, и цена его — проверка во время работы на каждом таком вызове, кроме случая, когда растущий довод объявлен нат: там потолок 2⁵³−1 даёт сам тип.

Отсюда следует заказ. Порядок «сначала размерные графы, потом типизированный AST» и обратный ему дают на первом шаге 54 и 74 функции. Оба шага стоят недёшево, а окупаются только вместе — поэтому браться за один из них ради числа в ведомости смысла нет, и это главный вывод замера.

Связано: only-293-of-2242-functions-lacked-a-mark-the-rest-lack-rules, structural-size-becomes-total-when-you-descend-into-the-pattern-field, the-bottleneck-is-rule-strength