Чтение условий если закрывает ноль целей, и причина в идиоме кода
Заказ выглядел очевидным: научить ядро читать условия ветвления, чтобы факты из если становились известными. Замер сказал «ноль», и разложил почему.
Ветвь иначе читать НЕЛЬЗЯ: на NaN ложны обе стороны сравнения, а функции нужна ровно эта ветвь.
Законная половина — читать ветвь то:
функций в корпусе 4009
условий «если» 3454
из них читаемых 199
целей это закрывает 0Причина — идиома. В коде всегда пишут если <мало> то <база> иначе <работа>, и нужный факт всегда лежит в той ветви, которую читать нельзя. Замер прогнан и по 18 посылкам индукции — тоже ноль.
Что при этом сработало. Позже ту же механику применили иначе: в ветви спуска индукции условие дна ложно по построению, и вот этот факт оказался полезен — на нём замкнулся «Факториал». То есть правило не бесполезно, бесполезна была его первоначальная постановка.
Дополнение 16 августа: другой ход по тем же условиям дал не ноль. Ветка work/formy-tela завела РАЗБОР ЦЕЛИ ПО УСЛОВИЮ: цель, у которой на верхнем уровне стоит если, делится надвое подстановкой ЗНАЧЕНИЯ условия, и обе половины сводятся теми же тремя правилами.
Отличие от отвергнутого хода существенное и его стоит держать в голове: ни один факт из условия не выводится. Ловушка не число была про перевод отрицания сравнения в другое сравнение («не (х меньше у)» ⟹ «х не меньше у»); а здесь отрицания нет вовсе — есть подстановка да и нет, и у признака значений ровно два.
Этим закрылось утверждение «это классическая импликация» о «Следует» из stdlib/logic.flang — ПОЛНЫЙ смысл функции, и закрылось без теоремы вовсе: цена доказательства ноль строк. Тел-условий в flang/stdlib 37 из 208.
Мораль не «прошлый замер был неверен», а «ноль был у ХОДА, а не у условий»: отрицательный результат отвергает конкретный способ, и переносить его на всю тему — ошибка того же рода, что переносить успех.
Связано: a-measured-zero-is-valuable, nan-is-reachable, the-bottleneck-is-rule-strength, bottleneck-moved-to-claim-shape