Можно ли так доказывать правильность алгоритмов?

Question

[floppa322]

Проблема несложная, но на её примере проще всего показать, что имеется в виду

Проблема: Есть прямоугольники с шириной и высотой. Найти максимальное количество таких прямоугольников, что их можно вложить друг в друга (условие вкладки: widthA <= widthB, heightA <= heightB).

Решение: отсортировать массив по координате X, а при равенстве X по коопдинате Y и найти в получившемся массиве НВП по Y


Доказательство: Пусть в отсортированном массиве где-то располагается правильная последовательность прямоугольников максимальной длины (обозначена зелёными кружками на картинке). Тогда в этом отсортированном массиве относительный порядок элементов последовательности (как подпоследовательности) не нарушен: если xi > xj, значит элемент i правее в массиве, а если xi = xj, и yi > yj, то элемент i правее в массиве, а значит у максимальной длины последовательности в отсортированном таким образом массиве относительный порядок элементов такой же, как у правильной последовательности. Значит, если в этом массиве искать НВП по Y, то мы обязательно найдём эту последовательность (зелёные кружки)

Часто приходилось именно таким образом доказывать правильность работы алгоритма, что есть какой-то оптимум в проблеме, то алгоритм обязательно его не пропускает.

Вопрос: с формальной точки зрения является ли такое доказательство (когда доказательство основывается на том, что есть какой-то оптимум в проблеме и алгоритм всегда находит его) правильным, в том смысле что не упускает ли каких-то краеугольных вещей?

Comments

[Alexandroppolus]

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

[floppa322]

Alexandroppolus, вот как раз оптимальность оно и обосновывает потому что если именно таким образом отсортировать массив, то относительный порядок элементов оптимальной последовательности будет правильным (таким же как в отсортированном массиве), а значит после её найдёт НВП

Но я больше спрашивал про абстрактный подход, а не про конкретную задачу

[hint000]

Проблема абстрактного подхода в этом:

Пусть в отсортированном массиве где-то располагается правильная последовательность прямоугольников максимальной длины

Но из чего формально следует, что правильная последовательность там содержится? Это нигде не доказано, но вы пользуетесь этим предположением как доказанным фактом. Пусть даже для вас это очевидно, но формальное доказательство нельзя так строить, Очевидное для вас может быть не очевидно для всех остальных.

Однажды великий математик Пьер Ферма сделал пометку на полях книги: "...Я нашёл этому поистине чудесное доказательство, но поля книги слишком узки для него."
Эта шуточка затянулась на 357 лет, пока доказательство действительно нашли.

[floppa322]

hint000, ну потому что среди объектов есть какая-то максимальная последовательность

[Михаил Ливач]

floppa322, откуда Вы взяли это утверждение?
Например, у Вас есть 10 прямоугольников: 1*10, 2*9 и так далее ( ширина всё время растёт, а высота всё время убывает ). Насколько я вижу, никакой последовательности тут не найти.

[floppa322]

Михаил Ливач, ну тут 2 максимальных последовательности из 1-го элемента

Answer 1

[Wataru]

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

Comments

[floppa322]

а почему недостаточно того, что у оптимальной последовательности сохранится относительный порядок в отсортированном массиве, а значит её обязательно найдёт НВП ?

[floppa322]

если для k измерений, то в общем случае тут сортировка (за k * n * logn) нужна просто для того, чтобы сделать перед НПВ (по k параметрам) правильный относительный порядок элементов, чтобы НВП этим пользоваться могла и перебирать только предыдущие элементы

[floppa322]

ну а если можно переворачивать то вроде достаточно отсортировать ещё этим k измерениям каждый объект и рассматривать конкретный поворот k мерного прямоугольника с отсортированными координатами
как здесь, например

[Wataru]

floppa322, а вдруг более длинная последовательность, найденная НВП даст невкладывающиеся прямоугольники? Вам надо в обе стороны доказать соответствие последлвательности в массиве и последоватеньности матрешки.

Перевооачивать, да, но это же отдельный прием для борьбы с этим.

[floppa322]

Wataru, а ну доказательство, что алгоритм выдаёт неправильный ответ (находит лишние прямоугольники) здесь и так понятно, что чтобы такое было нужно чтобы нвп неравенства неправильно проверяла. Я больше говорил в целом, про подход доказательства, когда оно строится на том, что есть какой то opt (например подпоследовательность) и алгоритм не может её пропустить, а значит обязательно найдёт

[Wataru]

floppa322, да это частый подход. Рассматриваем оптимальный ответ и что-то про него доказываем

[floppa322]

Wataru, ок, спасибо :)

Answer 2

[vadimr]

Не очень понятно, что вы в данном случае называете доказательством правильности. С формальной точки зрения, тут надо начинать доказывать с того, что представления чисел в вашей машине образуют строго упорядочиваемую операцией ">" последовательность, а это, кстати, неправда (для примера рассмотрим прямоугольники с размерами, равными NaN).

Comments

[floppa322]

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

[vadimr]

Что значит “невалидными”? Вы готовы гарантировать, что ваш процессор сравнивает все числа именно так, как вы считаете правильным?

В качестве интуитивной идеи ваше рассуждение верное, но доказательством правильности алгоритма в формальном смысле оно не является. Хотите доказывать правильность – начинайте с аксиоматики в лямбда-исчислении, я так считаю.

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

[floppa322]

Что значит “невалидными”? Вы готовы гарантировать, что ваш процессор сравнивает все числа именно так, как вы считаете правильным?

при доказательстве алгоритмов никто не предполагает, что процессор может как-то не так себя повести

[vadimr]

floppa322, вы сейчас оперируете не имеющим конкретного содержания сочетанием слов. Что значит "так" или "не так"?

По своей проблематике ваша задача относится к материалу третьего тома Кнута. Посмотрите, как Кнут строит доказательства таких алгоритмов. Сначала он аксиоматически определяет архитектуру некой абстрактной вычислительной машины и точно задаёт формальные свойства её команд. Дальше он в этой придуманной им аксиоматически заданной системе команд пишет алгоритм и уже относительно свойств вычислительной машины доказывает свойства алгоритма. Это и есть формальное доказательство. А то, что вы пишете - просто некие рассуждения по поводу.

[floppa322]

vadimr, речь шла о доказательства вроде такого, они не вводят абстрактную машину (это избыточно), а просто доказывают алгоритм как таковой

[vadimr]

floppa322, ну что я могу сказать - не надо сложные вопросы теории вычислений изучать по Википедии. Дейкстра был умный мужик, хоть и не все его идеи я разделяю, и вряд ли ограничился в своих рассуждениях страничкой Википедии, если вообще доказывал свой алгоритм, что, кстати, не факт.

А так в Википедии, например, написано, что Дейкстра запретил goto, а это всего лишь частное допущение из середины его сложной математической статьи на сотню страниц.

[floppa322]

vadimr, ИТМО это не википедия Википедия :)

[vadimr]

floppa322, по ИТМО тоже не надо. Эти вопросы выходят за рамки высшего образования и находятся примерно на уровне аспирантуры института Стеклова. Лекции академика Беклемишева, например, можно послушать на ютубе по такому предмету.

В высшем техническом образовании все алгоритмы даются без формальных доказательств.

[floppa322]

vadimr, я думаю, в конкретно в этой статье, и так достаточно формальное доказательство, более формально (например, через машину Тьюринга) было бы избыточно для понимания работы дейкстры

[vadimr]

floppa322, я не читал работу Дейкстры и не являюсь специалистом по теории вычислений, поэтому не готов в деталях обсуждать вопрос доказательства его алгоритма, хотя знаю сам этот алгоритм. Но имея высшее образование, аспирантуру, некоторый опыт преподавания и научных публикаций в области программирования, я всё же в состоянии увидеть границы своего незнания в данном случае.

В вашем же исходном вопросе проблема упорядоченности просто бросается в глаза.

Цель доказательства-то какая? Если чисто математическая, то надо начинать от аксиом. Если это вопрос надёжности программного обеспечения, то тем более жизни людей, или что там ещё, что тоебует формальных доказательств, нельзя ставить в зависимость от неизвестных обстоятельств работы процессора.

[floppa322]

vadimr, вы говорили про упорядоченность в контексте абстрактной выч. машины, а до этого я говорил про то, что вводить асбтрактную машину это избыточно )

[vadimr]

floppa322, это не избыточно, а совершенно необходимо, если мы говорим о формальном доказательстве. Необязательно именно через абстрактную машину, можно через лямбда-исчисление, что равнозначно. Но для доказательства должна быть формальная аксиоматика.

Я, кстати, покуда учился в институте, тоже не догонял, зачем Кнуту понадобилась гипотетическая машина MIX. Только намного позже понял.

[floppa322]

vadimr, я не стал уточнять в вопросе, но речь шла о доказательстве "для себя", а не для публикации куда-либо
Хотя, например, когда я читал публикацию какого-то уважаемого вуза про Robin Hood hashing, они тоже не вводили ни лямбда-исчисление, ни абстрактную машину

[vadimr]

floppa322, вопрос доказательства правильности алгоритмов вообще очень сложный. Дай бог если его хорошо понимает тысяча человек, владеющих русским языком, и десять тысяч во всём мире. Я вот лично не понимаю. А скорее я бы снизил обе эти оценки на порядок.

Иначе бы в программах почти не было ошибок. Вот у того же Кнута за несколько десятков лет 7 ошибок в его программах Tex и Metafont нашли, притом, что он назначил экспоненциально увеличивающиеся премии, а пользователей этих программ очень много.