Тип не держит инвариант, поэтому очевидные утверждения о дереве поиска ЛОЖНЫ — а сузить их до правильных деревьев нечем

Два самых естественных утверждения о дереве поиска написать нельзя, потому что они неправда:

• «ключ есть в дереве ровно тогда, когда он среди ключей дерева» (результат равен ((«Ключи дерева» от дерево) содержит искомый));
• «обход по порядку даёт возрастающую последовательность».

Причина одна и она в типе. тип «Дерево» объявляет форму — узел с ключом и двумя поддеревьями, — но НЕ объявляет порядок. Значение Узел("м", слева = Узел("я")) типу соответствует, а деревом поиска не является. «Ключи дерева» обходит всё дерево и находит «я», а «Есть ключ в дереве» спускается по одной ветви и не находит. Постусловие говорит обо ВСЕХ значениях типа, значит оно ложно.

Проверено на обоих деревьях библиотеки — flang/stdlib/tree.flang (ключи строками) и flang/stdlib/numtree.flang (числа): ловушка одна и та же.

Сузить утверждение нечем. Предусловие требует тут не поможет: нужен предикат «это дерево поиска», а его пришлось бы дописывать функцией, то есть менять состав библиотеки ради формулировки. Это отдельное решение, и его стоит принимать явно, а не походя.

Что вместо этого сказать МОЖНО, и это проверено прогоном. Утверждения, которые правдивы про любое значение типа, потому что говорят про совпадение ДВУХ спусков, а не про инвариант:

• «положенный ключ находится» — вставка и поиск идут по одинаковым сравнениям, а повороты дерева порядок обхода не меняют, поэтому правда даже про испорченное дерево;
• «ключ есть ровно тогда, когда вставка по нему не увеличивает размера»;
• «чего нет СРЕДИ КЛЮЧЕЙ, того поиск не выдумывает» — одна половина равносильности, та, которая правда всегда;
• «в дереве высоты не больше единицы поиск не промахивается» — вторая половина, суженная до случая, где инвариант выполняется по построению.

Порознь вторая и третья даровые (первая переживает заглушку нет), вместе — нет.

Второй запрет, из той же области и найденный рядом: порядок в списке. «Обход отсортирован» нельзя сказать и по другой причине, независимой от инварианта: у языка нет квантора по СОСЕДНИМ парам списка. отфильтровать даёт «все элементы такие-то» через «длина отбора равна нулю», а вложенный отфильтровать внутри условия внешнего (работает, проверено) даёт ещё и «ни один элемент не встречается дважды» — но пары соседей ими не выразить, а элемент N в требует списка номеров, которого взять неоткуда.

Что выразимо взамен и написано у «Сортировать деревом»: первый элемент не больше любого другого, последний не меньше любого другого — два отбора с пустым итогом.

ПОПРАВКА (20 августа, ветка u/kvantor): второй запрет СНЯТ. Квантор по соседним парам в языке есть — СПИСОК не убывает, — и заведён он без единого нового слова: не и убывает ключевые с первого дня, занято лишь МЕСТО, где цепочка этих двух токенов после выражения была ошибкой разбора. Про сортировку при этом выяснилось главное: утверждение «обход отсортирован» о настоящей сортировке ЛОЖНО на «не числе», см. sort-result-is-non-decreasing-is-false-on-not-a-number. Первый и третий запреты остаются в силе.

Третий запрет, найденный там же: равенства над параметром типа нет.

FLANG_TYPE: сравнивать на равенство можно только скаляры, а не «А»

Функция, возвращающая значение ПАРАМЕТРА типа, не может сказать о нём ничего: других отношений над «А» в языке нет вовсе. Таких функций 4 в flang/stdlib/optional.flang и 3 в flang/stdlib/result.flang — семь из двадцати двух остались без единого утверждения именно поэтому. Вдобавок у такой функции единственная возможная заглушка — запасное, и она удовлетворяет всему, что про такую функцию правда.

Чем подтверждено. Ветка vypusk/utv-derevya на основании github/main df055a6b. Ложность обоих утверждений о дереве посчитана вычислителем на испорченных деревьях (Узел("м", слева = Узел("я")) и Развилка(5, меньшие = Развилка(9))), отказ по параметру типа получен прогоном bootstrap/flang check.

СКОЛЬКО ЭТО СТОИЛО БИБЛИОТЕКЕ — ПОСЧИТАНО 20 АВГУСТА 2026. Каждое утверждение ниже посчитано вычислителем на названном значении, а не оценено на глаз: 28 утверждений в шести файлах из двадцати ложны из-за того, что тип шире смысла. Из них четыре уже написаны в библиотеке и проверкой не ловятся (среди примеров автора такого значения нет):

• datetime.flang «День недели», «день недели не больше шести» — 6,5 на Календарный день(1970, 1, 3.5): тип не требует целости суток;
• datetime.flang «Дата верна», «круг через счёт дней её не меняет» — на Календарный день(2026, 8.5, 18);
• hashmap.flang «Развести», «разведение не теряет и не двоит» — при прежний = −0: поле спуск объявлено число, а по смыслу это остаток хеша;
• hashmap.flang «Вложить», «вложенное по спуску по тому же спуску и находится» — там же и по той же причине.

Остальные 24 не написаны именно потому, что были бы ложны: tree.flang — 5, sets.flang — 5, dictionary.flang — 5, hashmap.flang — 4, datetime.flang — 3, numtree.flang — 2. Всего утверждений в flang/stdlib — 454.

Ненаписуемое узнаётся по шрамам в тексте, и их видно глазом: сторож («Высота» от дерево) не больше 1 в numtree.flang (утверждение сужено до дерева из одной развилки), пустая ветка то да в dictionary.flang, односторонние неравенства не меньше (длина первое) там, где по смыслу нужно равенство.

ЛОЖНОСТЬ СНИМАЕТСЯ ОХРАНОЙ, И ПРАВКИ ЯЗЫКА ДЛЯ ЭТОГО НЕ НУЖНО. Фраза «сузить утверждение нечем» выше — УЖЕ, чем сказано, и это посчитано: утверждение, записанное как если («Это дерево поиска» от дерево) то … иначе да, на том же кривом дереве даёт да, а без охраны — false. Охрана при этом не пуста: «Это дерево поиска» от кривого дерева равно нет, от настоящего — да. Написано в flang/stdlib/tree.flang; предикат стоил 29 строк.

Стена, значит, не в выразимости, а в ДОКАЗУЕМОСТИ, и она разобрана поимённо в a-guard-changes-truth-not-provability.

Связано: substantive-and-provable-claims-barely-overlap, unstatable-costs-more-than-unprovable, nan-is-reachable

Поправка 20 августа 2026: сузить УТВЕРЖДЕНИЕ есть чем, сузить ТИП — по-прежнему нечем

Выше сказано «сузить утверждение нечем: предикат пришлось бы дописывать функцией». Дописывать функцию можно, и с 20 августа это ничего не ломает: помощник в постусловии больше не зацикливает проверку (the-postcondition-loop-is-untied-by-a-program-transform-not-a-runtime-flag). Проба целиком прошла на bootstrap/flang 0.5.1 (ветка u/steny-peremer, основание ff8ad5d0):

обеспечивает «под инвариантом поиска ответ совпадает с обходом»
  если («Это дерево поиска» от дерево)
    то (результат равен («Есть ключ обходом» от дерево и ключ))
    иначе да

«Это дерево поиска» — три рекурсивные функции по 8 строк. Утверждение проходит типы, примеры проходят, и главное — оно больше не ЛОЖНО: значения типа, не являющиеся деревом поиска, охрана отсекает.

Что осталось: ядро его не доказывает (вердикт «сетка»), и цена такой охраны — полный обход дерева на каждом возврате, то есть постусловие меняет порядок цены рекурсивной функции (a-postcondition-runs-on-every-call-so-a-walk-inside-it-changes-the-cost-order, пункт 1). То есть беда переехала из «сказать нечем» в «доказать нечем и при работе дорого», а это другая заявка на правку.

Связано: a-hand-copied-wall-list-goes-stale-in-silence unstatable-costs-more-than-unprovable, nan-is-reachable, a-guard-changes-truth-not-provability