Почему существует разница на единицу в функции вниз обозначения Z для решения задачи 8 Queen?

Question

Я читал книгу под названием «Путь Z: Практическое программирование с помощью формальных методов, автор Джонатан Джеки» и в главе 18 (проблема 8 королев) автор представил формальное решение известной проблемы 8 ферзей, основанное на Z-нотации. Он попытался решить диагональную часть, соединив ее с уравнением прямой. Переменные, используемые в решениях:

Тогда уравнения прямой линии для решения диагональной части: где файл представляет собой строку здесь, а ранг представляет собой столбец. Изображение, которое предоставлено, чтобы помочь нам понять диагонали:

Решение работает следующим образом: файл (строка) номер 1 выделен синим цветом. Ранг (столбец) 1 выделен красным. Решение идет снизу вверх и слева направо.

Я хочу вычислить значения функции вверх и вниз для квадрата в файле (строка) = 4 и ранг (столбец) = 6 (выделено желтым цветом) ).

Итак,

вверх = ранжирование = 6-4 = 2

вниз = ранг + звание = 6 + 4 = 10

как видно на изображении выше, диагональная линия вверх действительно обрезает левый край для точки пересечения по оси Y в точке 2. Но диагональная линия вниз разрезает точку пересечения по оси Y в точке 9 (вместо 10). Есть разница в 1. И эта разница для всех квадратов. Я хочу знать, какой кусок мне не хватает в этом случае? Почему всегда есть разница в случае стрелки вниз (а не в случае стрелки вверх)?

Я также прилагаю полное решение на основе Z-нотации для справки:

Answer 1

Проекции, изображенные на картинке и в тексте, различаются, но, похоже, это не имеет особого значения: единственные свойства, которые необходимо сохранить, - это 1. up()/down() проекция двух ферзей на одну диагональ одинакова 2. up()/down() проекция двух ферзей на другую диагональ отличается.

Отрывок из книги, который вы поместили в вопрос, кажется, не так ясен по этому поводу, но (насколько я могу судить) up() (соответственно down()) проекцию Королевы следует сравнивать только с up() (соответственно, down()) проекции других ферзей, чтобы определить, находятся ли они на одной диагонали. В противном случае достоверность такого сравнения будет тривиально опровергнута, например, с учетом q1 := Queen(1, 1) и q2 := Queen(6, 4), легко увидеть, что down(q1) == up(q2), но q1, q2 не атакуют друг друга *. 1021 *