Левая свёртка упирается не в индукцию, а в то, что правило свёртки не читает постусловие вызванной функции

Заметка left-fold-gives-no-list-induction говорит, что к левой свёртке индукцию по списку прицепить нельзя, и это по-прежнему верно как общее утверждение. Но у самого частого случая — «длина результата равна длине входа» — у ядра есть отдельное правило («свёртка, растущая ровно на один»), и упирается оно в другое место: правило читает шаг свёртки только синтаксически и не берёт постусловие той функции, которую шаг зовёт.

Разница выделена до ОДНОЙ строки. Одна и та же сортировка вставками, одна и та же «Вставить» с уже ДОКАЗАННЫМ постусловием «длина плюс один», одно и то же утверждение (длина результат) равен (длина элементы):

разбор элементов
  случай пусто → пустой список
  случай голова и хвост → «Вставить» от голова и («Сорт» от хвост)
⇒ доказано индукцией по списку

свёртка элементы начиная с пустой список как акк и эл → «Вставить» от эл и акк
⇒ НЕ доказано

Механика. Правилу свёртки нужно, чтобы мера тела шага стала длина(акк) плюс 1. Развернуть длина оно умеет только через встроенные конструкторы — добавить, приписать, выписанный список. Для длина(«Вставить»(эл, акк)) у него нет хода: постусловие вызванной функции здесь не читается, хотя на пути структурной рекурсии оно читается и доводит доказательство до конца (см. callee-postcondition-is-a-fact-only-after-it-is-proved).

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

Обход, который просится, не годится. Усилить утверждение до инварианта накопителя («длина накопителя плюс длина остатка равна длине входа») нельзя потому, что накопитель свёртки — внутреннее имя: снаружи о нём сказать нечего, а обеспечивает говорит только о результате. Это тот же класс, что unstatable-costs-more-than-unprovable.

Тело переписывать со свёртки на разбор не следует бездумно: ответ меняется на минус нуле. «Сортировать» от [0, −0] свёрткой даёт [−0, 0], разбором — [0, −0], потому что вставка идёт с разных концов, а равен — это Object.is.

Чем подтверждено. Ветка vypusk/utv-lists на основании df055a6b. Проба из четырёх функций в одном файле, прогон flang check --proof --json двумя двоичными: собранным из дерева и напечатанным из сегодняшних flang/self/ (второй сильнее, см. the-bootstrap-seed-lags-the-kernel-by-one-goal-kind). Оба ответили одинаково: разбор — доказано, свёртка — сетка.

Чем ограничено. Речь только про меру «длина». Про накопитель-число правило не работает вовсе и по другой причине — точность сложения.

Связано: left-fold-gives-no-list-induction, callee-postcondition-is-a-fact-only-after-it-is-proved, claims-about-length-are-two-thirds-of-what-the-kernel-refuses

Снято 20 августа: правило свёртки теперь читает постусловие вызванного

Ветка u/svyortka, основание ff8ad5d0, коммит «Сортировка вставками доказана». Правка — в «Шаг ровно на один» (flang/self/proof-kernel.flang): меру тела шага перед сличением переписывают ТЕ ЖЕ равенства, которыми правило тождества уже переписывает обе стороны цели. Новых источников доверия ноль: в этих равенствах лежит только постусловие, которое ядро УЖЕ доказало и у которого снято требует, — за отбор отвечает восьмой ход, а не правило свёртки.

Числом. flang/stdlib: доказано ядром 62 → 65, из них содержательных 39 → 42, высказано те же 454; ни одно прежде доказанное не потерялось (списки доказанных сверены diff-ом целиком). Закрылись ровно три, и все три — одно и то же утверждение о сортировке:

lists.flang — «сортировка не теряет и не добавляет элементов»;
higher-order.flang — «сортировка по порядку не теряет и не добавляет элементов» и то же у «Сортировать», которая зовёт «Сортировать по».

Примеры библиотеки 1216 из 1216. Точка раскрутки сходится байт в байт.

Вся законность хода в одной границе, и она проверяется, а не предполагается. Тело шага стоит ПОД СВЯЗЫВАТЕЛЕМ: акк и эл внутри витка значат не то, что снаружи. Поэтому близнец («Начало и шаг») вычёркивал «Снаружи свёртки» ВСЯКИЙ факт, упомянувший имя витка. Здесь вычёркивание сужено двумя условиями:

слева у равенства стоит длина(В), где В — ВЫЗОВ, стоящий ДОСЛОВНО в теле шага: значит имена в нём написаны автором внутри витка;
ни накопитель, ни элемент не встречаются в цели нигде, кроме тела шага — ни в правой стороне, ни в списке свёртки, ни в её начале.

Без второго условия правило доказывает ЛОЖЬ, и это не рассуждение, а работающая программа: flang/test/fixtures/poddelka-svyortka-shagom.flang, функция «Ложь именем витка». Параметр там назван акк — так же, как накопитель витка, — а требует говорит правду про ВНЕШНЕЕ акк (при начале из одного элемента удвоение и правда даёт на один длиннее). Утверждение «длина итога есть длина начала плюс длина списка» при этом ложно: на [7] и [1, 2] итог длиной 4, а обещано 3, и прогон примера отвечает FLANG_PROPERTY. Сторож — node flang/scripts/poddelki-yadra.mjs, 8 файлов, аксиом ноль.

Половина «обязано быть ДОКАЗАНО» в подделке не украшение. Правило, которое отвергает всё подряд, отвергнет и ложь, и правду, и подделка о нём не скажет ничего. Поэтому в том же файле лежит честная пара — «нулей ровно столько, сколько элементов», — и сторож требует у неё вердикта «доказано». Пара сделана РЕКУРСИВНОЙ нарочно: у плоского определения (тела без единого вызова) есть своя развёртка, и на первой попытке пара зеленела и БЕЗ правила, ничего не измерив.

Чего это НЕ дало, и это тоже число. Замер двадцати функций (benchmarks/proof-cost/schyot-20.mjs) как показывал 10 содержательных из 20, так и показывает: среди двадцати нет ни одной функции этой формы. И цена при работе не сдвинулась — см. the-guard-that-costs-the-time-is-not-the-one-you-proved.

Связано: one-action-written-two-ways-was-proved-differently, the-guard-that-costs-the-time-is-not-the-one-you-proved