Автоматическая индукция по разбору закрыла 9 утверждений, а из двенадцати заказанных — 5
Заказ из what-blocks-the-kernel-now-is-induction-without-a-theorem выполнен: ядро теперь ведёт индукцию по телу-разбору само, с пути постусловия, без единого нового слова в языке. Закрылось 9 утверждений корпуса, но не те 12, что были заказаны — из них взялось 5, и разница объясняется формой тела, а не силой правила.
Чем подтверждено. node flang/scripts/proof-ledger.mjs до и после, ветка work/indukciya, коммит ccc4ebb1 (правило) поверх ствола e56d33d7: доказано ядром 185 → 192, из них индукцией по объявленной сумме 27 → 34, сеткой примеров 124 → 117. Отвергнутых ядром 0 и нарушенных на примерах 0 — как было. После слияния ствола d3153122 (там же приехало правило порядка) числа стали 319 высказано / 213 доказано / 34 индукцией по сумме / 101 сеткой.
Кто именно закрылся — поимённо, by === "cases" по всему корпусу:
| файл | функция | утверждение | база/шаг |
|---|---|---|---|
| stdlib/lists.flang | «Длина» | длина списка неотрицательна | 1/1 |
| stdlib/lists.flang | «Индекс» | индекс неотрицателен | 1/1 |
| stdlib/higher-order.flang | «Позиция где» | позиция неотрицательна | 1/1 |
| stdlib/strlists.flang | «Номер строки» | номер строки неотрицателен | 1/1 |
| stdlib/numtree.flang | «Высота» | высота дерева неотрицательна | 1/1 |
| stdlib/optional.flang | «Умножить значение» | умножение не создаёт и не теряет значения | 2/0 |
| examples/import-check.flang | «Длина», «Индекс» | те же две | 1/1 |
| examples/paths/shortest-path.flang | «Через ребро» | стоимость неотрицательна | 1/0 |
Почему из двенадцати взялось только пять — это про форму тела, а не про правило. Замер по flang/stdlib (node flang/scripts/claim-scan.mjs неотрицательность stdlib): 53 пробы, закрыто без теоремы было 2, стало 5. Из девяти рекурсивных функций библиотеки, которым эта цель подходит, тело-разбор у пяти («Глубина словаря», «Найти первое», «Элемент», «Размер дерева», «Глубина дерева»), а у четырёх — тело-если («Поиск в диапазоне», «НОД», «Степень», «Факториал»). По если принципа индукции взять неоткуда: разбор под условием отвечает не за все значения, а спуск по числу требует меры, которую называет автор словом убывает. Из пяти взялись три — «Найти первое» и «Элемент» остались, потому что их рекурсивный вызов меняет не только разбираемый параметр, и построенное допущение с ним не сличается.
Оракул перестал что-либо находить, и это успех, а не потеря. До правила claim-scan показывал «доказано с теоремой 2» — те самые lists «длина списка неотрицательна» и numtree «высота дерева неотрицательна», которые оракул умел доказать, а вписать было некуда. Теперь их закрывает сам путь постусловия, и строка стала «закрыто без теоремы 5, доказано с теоремой 0».
Правило доказывает, а не допускает. Пять условий, каждое проверено подделкой (flang/test/proof-cases.test.mjs, 8 проверок):
- носитель — разбираемое имя объявлено суммой или встроенным списком; отрезок
натсюда НЕ входит; - разбор на верхнем уровне тела — не под условием;
- покрытие — у каждого конструктора есть ветвь и заключение;
- база есть — тип, у которого все варианты рекурсивные, отвергается отдельным условием: свёртка принципа считает пустую базу законной (у теоремы её вправе закрыть автор), а здесь закрывать некому, и вывод опёрся бы только на себя;
- все посылки свелись — одна несведённая рвёт вывод целиком.
Подделки: шаг, зовущий себя на построенном заново значении (Ф(Звено(х)) вместо Ф(х)); шаг, зовущий себя на чужом параметре; тип без базы; цель на не-числе ((0 делить на 0) не больше (0 делить на 0)). Все четыре остались недоказанными. Рядом — различающая проверка: (0 делить на 0) равно (0 делить на 0) берётся, потому что равен языка есть Object.is и тождеству посылка «не NaN» не нужна, а порядку нужна.
Снять правило и посмотреть, что покраснеет. Убрано второе слагаемое из поОбъявленномуТипу(…) ?? разборомПоСлучаям(…) — краснеют РОВНО три проверки раздела «БЕРЁТ», все четыре подделки остаются зелёными. Правило держит то, о чём заявлено, и ничего сверх.
Чем ограничено, и это стоит сказать прямо. Две из девяти закрытых целей («Умножить значение», «Через ребро») имеют шаг 0 — то есть допущения индукции там не понадобилось, это простой разбор случаев. Ведомость всё равно печатает о них «доказано индукцией», потому что поле induction общее с путём теоремы, где то же самое бывает у перечисления без рекурсивных вариантов. Слово сильнее того, что произошло; это не ложь о доказанности, но неточность о способе.
Список аксиом остался пустым: flang/src/proofterm.mjs, АКСИОМЫ = Object.freeze([]). Правило не добавляет ни одной посылки сверх тех, что строит принципИндукции по полям-местам варианта, — то есть по значению, уменьшившемуся по построению.
Сторона на flang сошлась. Зеркало (flang/self/proofterm.flang, «Разбором по случаям» и шесть спутников) переиспользует свод посылок, свёртку принципа и свод индукции как есть; расходится путь ровно в одном месте — «Сведение посылки допущением» передаёт в сведение допущения индукции, чего путь теоремы не делает намеренно. Побайтовая сверка flang/test/self-proofterm.test.mjs: расхождений 2 — те же две, что и на стволе e56d33d7 до всякой правки (обе про вычисление замкнутой цели, это чужой давний зазор), ни одной новой. Совпало побайтово 315 из 317 программ, доказанных строк 295 → 306. Точка раскрутки перепечатана (node scripts/bootstrap-c.mjs).
Что стало узким местом теперь. Не индукция. Самый крупный оставшийся кусок — по-прежнему 26 целей «равно» (симметричный близнец правила роста: «растёт РОВНО на один»), и он не тронут вовсе. Второй — тело-если у рекурсии по числу: четыре функции библиотеки из девяти. Прямой путь к нему — не чтение условия (это уже измерено в ноль, reading-if-conditions-closed-zero-goals), а автоматический выбор принципа по отрезку нат там, где мера читается из самого условия дна; но мера — слово автора, и брать её молча нельзя.
Связано: what-blocks-the-kernel-now-is-induction-without-a-theorem, bottleneck-moved-to-body-shape, proof-words-live-on-two-surfaces-of-four, no-induction-for-builtin-types