Метод получает размеченный датасет — например, доски крестиков-ноликов с исходом партии — и выдаёт функцию, которая его объясняет. Ничего про геометрию поля, про линии и про правила игры в метод не заложено. Заложено другое: какие наблюдения над объектом вообще доступны. Эта страница показывает, что именно выбор доступных наблюдений — а не количество данных и не алгоритм поиска — решает, будет ли индукция успешной.
Структура S — это конечный носитель плюс набор типизированных примитивов. Примитивы и есть «доступные наблюдения»: аксессоры, выделенные точки, кванторы по конечным индексным типам, операции. Объект непрозрачен — заглянуть в его внутреннее представление иначе как через примитивы нельзя.
Гипотеза о функции f : G → T — это типизированный терм с единственной свободной переменной g : G. Гипотезы упорядочены по приору кратности:
Ответ = первая согласованная с датасетом гипотеза в этом порядке. Никакой подгонки параметров, никакого обучения весов: только перечисление термов в порядке убывания приора. Функция от структуры к структуре, а не от чисел к числам — крестики-нолики здесь лишь конкретный носитель.
Носитель фиксирован: 958 терминальных досок 3×3, каждая размечена исходом (WIN_X, WIN_O, DRAW). Датасет один и тот же. Меняется только сигнатура — набор примитивов, через которые доску можно наблюдать.
Точность считается на всей вселенной из 958 досок, включая невиданные. Пунктиром — там, где согласованной гипотезы не существует вовсе.
Короткий вертикальный штрих у нижней оси означает, что при этом n согласованной гипотезы нет. У cells таких штрихов шесть из шести — линии нет вообще, поэтому в легенде она помечена отдельно.
Метод не «ищет правило» — он перечисляет гипотезы по убыванию приора и берёт первую, которая согласована с данными. Вот начало этого перечисления для структуры geom: стоимость — это −log P, размер — число листьев терма. Переключатель меняет объём данных: порядок остаётся тем же самым, меняется лишь то, какие гипотезы выборка успевает отсеять.
У всего, что выше, есть методологическая слабость, и её надо назвать прямо: в сигнатуре geom список из восьми линий вписан руками (LINES = ROWS + COLS + DIAGS). То есть geom выигрывает не потому, что метод вывел геометрию поля, а потому что геометрию ему сообщили. Это ровно та «лишняя структура», которой при постановке задачи хотелось избежать.
Поэтому — тот же метод, но линий нет вовсе. Есть только типы:
Позиция — это функция из осей в координаты, а не абстрактная девятка и не голое произведение. «Форма» — предикат на позиции p с параметром c : Coor; строки, столбцы и диагонали должны появиться как короткие термы, а не как данные. Меняется ровно одно: какая структура есть на Coor.
Все формы малого размера, порождённые перебором. Подсвеченные — те, что оказались настоящими линиями; остальные метод породил там же и должен отсеять сам.
oppositeCoor и getCoorType задают тождественную группу симметрий — порядок 2, {id, (A C)}. Орбитный взгляд их не различает вообще. Приор по длине терма различает: побочная диагональ стоит 4 листа против 14, то есть примерно 810 ≈ 109 раз по вероятности. И различие видно в поведении.