Логотип IRF

Вентиль И не отсекает: пробел в корректности конструкции условия победы

Техническая заметка IRF № 15 — исправление к разделу 6 работы «Raumschach и вычислительная сложность»

Международная федерация Raumschach  ·  Технические заметки IRF, № 15  ·  2026

Раздел 6 сводной работы (Raumschach и вычислительная сложность) описывает механизм вентиля И / условия победы, в котором Ладья V, стоящая на линии атакующей фигуры, отступает тогда и только тогда, когда каждый из нескольких булевых входных токенов вдоль её рядовой линии ответвился в сторону. Продолжающаяся работа по полной сборке нетривиальной формулы впервые проверила этот механизм на реальном генераторе легальных ходов с более чем одним входным токеном в подлинной последовательности — конфигурация, которую, судя по всему, ни одна прежняя проверка, включая собственную проверку раздела 6, не задействовала. Результат — подлинный пробел в корректности: механизм ставит мат, как только ближайший к V токен ответвляется, независимо от состояния любого токена дальше по линии, что представляет собой логическую противоположность заявленному И. Настоящая заметка документирует находку, прослеживает её причину до допущения о луче атакующей фигуры, не выполняющегося при частичном отступлении, определяет, какие из прочих конструкций проекта затронуты, а какие нет, и представляет проверенное решение: собственный вентиль V корректен ровно для одного смежного токена, а произвольные булевы формулы можно корректно составлять, вычисляя всю логику подформул полностью вне поля V и подключая результат к присутствию или отсутствию этого единственного токена — ценой той композиции с «тройной нагрузкой» на один токен, к которой стремился этот проект.

I. Резюме

Сводная работа (Raumschach и вычислительная сложность, раздел 6) описывает механизм вентиля И / условия победы следующим образом: Ладья V стоит в точке, где её собственная рядовая линия пересекается с триагональной линией, ведущей к Королю, при этом дальше по той же рядовой линии расположены булевы входные токены, каждый из которых блокирует отступление V, когда он Ложен, и ответвляется от линии, когда он Истинен; отступление V легально «тогда и только тогда, когда каждый токен ответвился». Как утверждает работа, после того как отступление становится легальным, оно открывает триагональную линию для атакующего Единорога, который объявляет шах и одновременно закрывает последнее поле бегства Короля.

Продолжающаяся вычислительная работа, направленная на полную сборку нетривиальной формулы, впервые проверила этот механизм на реальном генераторе легальных ходов с более чем одним входным токеном в подлинной последовательности — случай, который, судя по всему, не был задействован в исходной проверке (заметка № 9 и собственные тесты раздела 6 сводной работы), поскольку все прежние проверки проверяли лишь, может ли V достичь одного конкретного, полностью отступленного поля бегства при единственном заранее выбранном присвоении значений. Эта проверка обнаружила подлинный пробел в корректности: механизм в том виде, как он специфицирован, не реализует И для более чем одного входного токена. Он ставит мат, как только ответвляется любой отдельный ближайший к V токен, независимо от состояния любого токена дальше по линии. Это противоположность заявленному поведению, ближе к ИЛИ, чем к И.

II. Первопричина

Корректность вентиля опирается на допущение, которое, как выясняется, не выполняется: что V должен отступить полностью до конца, до своего назначенного поля бегства, прежде чем луч атакующего Единорога окажется открыт. На деле луч атакующего Единорога проходит именно через домашнее поле V — ту единственную точку, где рядовая линия V пересекается с триагональной линией Короля, — а не через поле бегства. В тот момент, когда V покидает это единственное домашнее поле по любой причине и на любое поле назначения, луч Единорога оказывается свободен, и объявляется вскрытый шах. Это было подтверждено напрямую: перемещение V на одно поле от его домашней позиции, с атакующим Единорогом, размещённым где угодно дальше по той же триагональной линии со свободным путём, порождает немедленный мат — ещё до того, как сам Единорог сделал хоть один ход, и независимо от того, насколько далеко в действительности продвинулся V.

Это разрушает задуманное многотокенное И. Рассмотрим два входных токена: T1, ближайший к V, и T2, следующий за ним, оба размещены вплотную друг к другу без зазора между ними (сильнейшее возможное размещение, проверенное напрямую, а не предположенное). Если x1 Истинен, T1 ответвляется и освобождает поле, смежное с V. Теперь у V есть легальный ход — на одно поле, на прежнюю позицию T1, — независимо от того, Истинен ли x2 или Ложен, поскольку легальность для Ладьи сделать какой-либо ход в направлении зависит только от того, присутствует ли ближайшее препятствие, а не от какого-либо препятствия дальше по линии. Этого хода на одно поле достаточно: он освобождает домашнее поле V, и мат следует немедленно, независимо от того, ответвился ли T2 (представляющий x2) вообще.

Это было проверено напрямую и точно: при x1 = Истина и x2 = Ложь у V есть ровно один легальный ход (на поле, освобождённое T1); совершение этого хода порождает позицию, в которой Король находится под шахом без легальных ответов — мат, — хотя конъюнкция x1 ∧ x2 Ложна. Контрольный случай (x1 = Ложь, x2 = Истина) подтверждает, что одного лишь ближайшего токена достаточно, чтобы полностью заблокировать V, независимо от токенов дальше по линии: у V ноль легальных ходов. Между этими двумя случаями паттерн однозначен: исход отслеживает лишь состояние токена, ближайшего к V. Каждый другой токен в цепочке логически инертен.

III. Почему более ранняя проверка это не выявила

Каждый тест со времён собственной проверки раздела 6 — вплоть до последующей работы этого проекта над композицией, выравниванием темпа и деревом партии — проверял легальность V, задавая вопрос, может ли V достичь одного конкретного, полностью отступленного поля назначения, при этом входные токены размещались (или опускались) напрямую в соответствии с заранее выбранным булевым присвоением. Такая проверка случайно даёт похожий на верный ответ всякий раз, когда геометрия никогда не даёт V частичный, нетерминальный легальный ход взамен, — что было верно для каждой протестированной конфигурации, как правило, потому что токены располагались с зазорами, либо потому что в игре был лишь один токен, либо потому что тесты композиции подключали значения истинности напрямую, а не строили подлинную многотокенную цепочку со смежным расположением. Пробел проявляется лишь тогда, когда (а) более одного токена стоит в подлинной последовательности на линии V, (б) ближайший из них способен ответвиться независимо от прочих, и (в) проверка условия победы задаёт тот вопрос, на который механизм в действительности отвечает — «есть ли у V вообще хоть какой-либо легальный ход» — а не вопрос-заместитель — «может ли V достичь этого одного конкретного поля». Ни один тест до настоящего не задавал вопрос (в) при одновременном наличии (а) и (б).

IV. Что затронуто, а что нет

Не затронуто: конструкции коридора, межуровневого перехода и вентиля ИЛИ (разделы 5 и 7), которые не зависят от приёма «домашнее поле / триагональная линия» V. Общий вывод о том, что третье измерение Raumschach устраняет присущее плоским шахматам препятствие пересечения проводников (раздел 3), — структурный, обусловленный геометрией доски аргумент, независимый от этого механизма, и он также не затронут.

Затронуто: конструкция вентиля И / условия победы раздела 6, в частности её утверждение о корректном вентилировании произвольного числа булевых входов. Конструкция корректна ровно для одного входного токена (второму токену попросту не относительно чего быть инертным). Она не корректна, в том виде, как специфицирована, для двух и более.

Также затронуто, в ожидании повторного рассмотрения: заявленное в разделе 6 масштабирование на три входа («проверено на масштабирование до трёх входов без изменений») и собственная корректность вентиля ИЛИ при композиции, поскольку механизм выхода вентиля ИЛИ в более поздней работе этого проекта по композиции был подключён непосредственно к той же рядовой линии в качестве входа вентиля И с использованием той же самой логики «освободить линию», которая теперь показана некорректной для последовательного многотокенного вентилирования. Любая составная конструкция, построенная на test_assembly_composite.py, test_double_composite.py или test_single_token_composition.py этого проекта, наследует этот пробел по той же причине: каждая подключала вычисленное булево значение к присутствию или отсутствию одного токена-заместителя на линии V, что в точности является тем однотокенным случаем, который эта заметка показывает корректным, — но ни одна из них не проверяла два или более независимо подвижных токена на одной линии в подлинной последовательности, а именно там и находится пробел.

V. Решение: корректная конструкция, с реальной ценой

Обновление, добавленное после дальнейшей работы: корректное решение существует, хотя оно более ограничено, чем исходное утверждение. Ни одно из двух направлений, названных выше (каскадные попарные вентили, отделение атакующего луча от дальнего поля V), не потребовалось; исправление проще и обходится ценой охвата. Оно было подтверждено напрямую на генераторе:

Цена: это подлинное исправление корректности, а не исходных амбиций. Более не верно, что одна физическая фигура может нести двойную или тройную нагрузку — одновременно быть собственным подвижным токеном подформулы, блокиратором рядовой линии и фигурой, стоящей на атакующем луче, — как предполагали раздел 6 и собственные test_single_token_composition.py и test_double_composite.py этого проекта. Композиция теперь требует явного, отдельного шага подключения между проверенной подформулой и тем единственным токеном, который в действительности важен для мата. Остаётся открытым вопрос, существует ли конструкция, восстанавливающая однотокенную композицию без подключения, не возрождая при этом исходный изъян настоящей заметки; более не открыт вопрос, существует ли какая-либо корректная конструкция для произвольных формул такого вида — она существует и была проверена.

VI. Заключение

Механизм вентиля И / условия победы в разделе 6 сводной работы, в исходной спецификации, не вентилирует корректно более одного булева входа: мат ставится, как только ответвляется ближайший к V токен, независимо от всех прочих токенов в цепочке, что ближе к ИЛИ, чем к заявленному И. Это было напрямую проверено на генераторе легальных ходов с токенами, размещёнными вплотную к V, — сильнейшей из доступных расстановок, — что исключает расположение как причину. Пробел не был виден ни в одном тесте до настоящего, поскольку каждый более ранний тест, включая собственную работу этого проекта по композиции и дереву партии, проверял условие-заместитель (может ли V достичь одного конкретного поля), совпадающее с реальным условием победы (есть ли у V вообще хоть какой-либо легальный ход) лишь в однотокенном случае. Корректное исправление было найдено и проверено для произвольных формул, построенных из ИЛИ и И: сохранить собственный вентиль V ровно для одного смежного токена и вычислять всю логику подформулы полностью вне поля V, подключая результат. Это восстанавливает корректность ценой однотокенной композиции с тройной нагрузкой, к которой стремился этот проект; восстановление этого более сильного свойства, если оно вообще возможно, остаётся открытым вопросом.

Источники