Спектральная(ое) теорема/разложение в приближённом формате

[amarsianin]

g______d в сообщении #1121061 писал(а):

Мне кажется, что во всех содержательных работах в этой области (например, https://pdfs.semanticscholar.org/a669/d ... 9f0183.pdf ) используется, по сути, такой подход.

Ничего подобного. Там используется прицнип Маркова, но не более. Что такое "часть классической математики" - я не знаю, как понимать. Прочитайте тогда про ТТЕ, если есть вопросы.

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

[Someone]

amarsianin в сообщении #1121146 писал(а):

Что такое "часть классической математики" - я не знаю, как понимать.

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

[amarsianin]

Я не очень знаком с анализом Маркова. Только с принципом Маркова. А у Вайрауха я таких методов доказательства не видел.

[g______d]

amarsianin в сообщении #1121146 писал(а):

ничего похожего на ваш метод рассуждения нет

amarsianin в сообщении #1121265 писал(а):

А у Вайрауха я таких методов доказательства не видел.

Короче говоря:

1) Вы не спорили (и, по-видимому, согласились) с тем, что я привёл достаточно явное описание итераций алгоритма и явную оценку их количества (либо подробное описание способа получить эту оценку, из которой очевидно, что она будет явной).

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

Если вдруг окажется, что существует набор корректных входных данных, на которых алгоритм работает неправильно, можно подставить эти данные в доказательство и получить противоречие в классическом анализе и ZFC, на фоне которых вопрос о работоспособности этого тривиального алгоритма померкнет.

Если вы не признаёте доказательства с помощью классического анализа, вы изолируете себя от 99.9% математиков и 100% прикладников. Я не знаю, какая у вас мотивация, но ни к каким потенциальным практическим приложениям она отношения не имеет. Я думаю, если вы спросите у авторов статьи, они вам пояснят, признают ли они классический анализ (уверен, что да) и, возможно, объяснят, чего именно вы не понимаете.

[amarsianin]

g______d в сообщении #1121340 писал(а):

1) Вы не спорили (и, по-видимому, согласились) с тем, что я привёл достаточно явное описание итераций алгоритма и явную оценку их количества (либо подробное описание способа получить эту оценку, из которой очевидно, что она будет явной).

Ну, алгоритм элементарный, если все данные наперёд известны. С этим я не спорю. Другое дело - насколько он вообще имеет отношение к моему вопросу.

g______d в сообщении #1121340 писал(а):

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

Классически, да, думаю, результат верен.

g______d в сообщении #1121340 писал(а):

Если вы не признаёте доказательства с помощью классического анализа, вы изолируете себя от 99.9% математиков и 100% прикладников. Я не знаю, какая у вас мотивация, но ни к каким потенциальным практическим приложениям она отношения не имеет. Я думаю, если вы спросите у авторов статьи, они вам пояснят, признают ли они классический анализ (уверен, что да) и, возможно, объяснят, чего именно вы не понимаете.

Ну, это уже сильно субъективное суждение. Вы, видимо, плохо знакомы с предметом. Я не буду вам рассказывать, что такое вычислимый анализ в ТТЕ и конструктивная математика (не по образцу Маркова/Шанина), а также о том, сколько групп в мире занимается ею, скажу лишь, что есть такая вещь как формальная верификация. Любую теорему, например, из двух книг, что я цитировал, вы можете имплементировать, скажем, в coq и оттуда генерировать рабочий код. А вот ваш алгоритм провалит формальную верификацию, т. е. его правильность недоказуема средствами пруф-ассистанта. Ещё раз, я ни в коем разе не рассчитывал тут вести философские дискуссии. Просто, видимо, в российской школе какое-то своё причудливое понимание предмета и мне стоило об этом догадаться, не знаю.

Как итог, считаю, что тред зашёл в тупик. Вопрос считаю открытым.

[g______d]

amarsianin в сообщении #1121470 писал(а):

Ну, алгоритм элементарный, если все данные наперёд известны.

Странная формулировка. Если имеются в виду входные данные (матрицы с рациональными элементами), то непонятно, как алгоритму работать без них. Если какие-то другие данные, то алгоритму для работы они не нужны.

amarsianin в сообщении #1121470 писал(а):

оттуда генерировать рабочий код.

Я и так могу генерировать рабочий код.

amarsianin в сообщении #1121470 писал(а):

А вот ваш алгоритм провалит формальную верификацию, т. е. его правильность недоказуема средствами пруф-ассистанта.

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

amarsianin в сообщении #1121470 писал(а):

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

Довольно странно слышать такие выводы от специалиста (которым вы, несомненно, являетесь, скрываясь под вымышленным именем на mathoverflow).

Напоминаю, что вы ранее предлагали мне закодить алгоритм и проверить, что он разваливается. По-прежнему думаете, что разваливается?

[amarsianin]

Ну, ладно, давайте поболтаем.

g______d в сообщении #1121623 писал(а):

входные данные

Ряд конкретных свойств предела посл-ти (выразимых численно, разумеется).

g______d в сообщении #1121623 писал(а):

Я и так могу генерировать рабочий код.

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

g______d в сообщении #1121623 писал(а):

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

Есть аксиомы, которые не допускают генерацию кода. Аксиома выбора, например. Вы можете её формально загрузить. Но программу вы в итоге не получите. Не говоря уже о непредикативных аксиомах. Если вы будете работать чисто во всленной типов, то, конечно, аксиомы ZFC вы просто не сможете даже определить. Так что если нужна формальная верификация И генерация программ - то только конструктивная логика.

g______d в сообщении #1121623 писал(а):

Довольно странно слышать такие выводы от специалиста (которым вы, несомненно, являетесь, скрываясь под вымышленным именем на mathoverflow).

Ну, у вас же тоже псевдоним. Это нормальная практика в интернете.

g______d в сообщении #1121623 писал(а):

Напоминаю, что вы ранее предлагали мне закодить алгоритм и проверить, что он разваливается. По-прежнему думаете, что разваливается?

Не готов ответить.

[g______d]

amarsianin в сообщении #1121771 писал(а):

Ряд конкретных свойств предела посл-ти (выразимых численно, разумеется).

Не понял. Какие свойства предела? Алгоритм видит только конечную последовательность вполне конкретной длины.

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

amarsianin в сообщении #1121771 писал(а):

Ну, у вас же тоже псевдоним.

На mathoverflow -- нет. А я что, угадал, и у вас там таки псевдоним?

amarsianin в сообщении #1121771 писал(а):

Есть аксиомы, которые не допускают генерацию кода. Аксиома выбора, например. Вы можете её формально загрузить. Но программу вы в итоге не получите. Не говоря уже о непредикативных аксиомах. Если вы будете работать чисто во всленной типов, то, конечно, аксиомы ZFC вы просто не сможете даже определить. Так что если нужна формальная верификация И генерация программ - то только конструктивная логика.

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

-- Сб, 07 май 2016 02:31:18 --

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

[amarsianin]

g______d

Прошу прощения, у меня нет ни времени, ни желания беседовать на не относящиеся к треду темы. Быть может, в другом месте, в другом треде. Хотите - создайте.

Благодарю за участие. За сим тред покидаю, пока, быть может, не будет новостей по существу.