Здравствуйте, Cyberax, Вы писали:
C>С теоремой Ферма — доказательства недоказуемости пока нет. Можно взять C>другое утверждение, уже с доказаной недоказуемостью.
Да, такие утверждения бывают. Более того, у меня в лекциях где-то есть конструктивное доказательство теоремы Гёделя о неполноте. Пользуясь им можно таких утверждений пачку составить.
Но и человек такое утверждения не сможет доказать (важное замчание: оставаясь в пределах тех же аксиом, т.е в пределах той же теории!). Если я правильно понимаю, можно брать подобное утверждение и добавлять его как новую аксиому (а можно брать отрицание этого утверждения) и получать более богатую, непротиворечивую теорию.
(собственно, претензия к Пенроузу именно насчет этого и была — он использовал "внешние" аксиомы, т.е по сути брал более богатую теорию и доказывал в ней, а затем переносил утверждение обратно в "меньшую" теорию).
Так что пока что я не понял твоего доказательства, что не существует универсального решателя (эквивалентного "математику").
Эквивалетность определим как совпадение множеств доказанных утверждений математика М(Т) и решателя Р(Т) для любой теории Т (набор аксиом).
Здравствуйте, chukichuki, Вы писали:
C>Стоит фантастическая задача: разработать алгоритм (программу) при помощи которой можно было бы показать, что два указанных алгоритма эквиваленты с точки зрения выполняемой операции. Анализ алгоритмов должен производится без их выполнения т.е. в статическом режиме. Как вы думаете, решение такой задачи возможно ?
Эта задача относится к категории halting-problem (проблема остановки) машин Тьюринга.
wikipedia.ru:
При обсуждении машины Тьюринга выделяют такое понятие, как проблема остановки машины Тьюринга. Проблема формулируется следующим образом: имея таблицу состояний машины Тьюринга, мы не можем с уверенностью сказать — остановит ли данная машина свою работу, или нет. Тьюринг доказал, что эта задача является неразрешимой. Чёткий ответ на этот вопрос возможен только в двух вырожденных случаях — когда в машине не объявлено ни одного конечного состояния, либо, когда все состояния машины Тьюринга являются конечными.
См. в частности теорему Rice-Myhill-Shapiro (не знаю как правильно товарищей обозвать, кроме последнего конечно).
Одно из следствий таково:
Не существует такой машины (т.е. алгоритма) которая всегда правильно может определить что входной язык данной конкретной машины Тьюринга (твоя функция например) имеет какое-то определнное нетривиальное свойство — например выполняет одинаковую задачу (имеется ввиду что мы знаем что это означает).
Я конечно могу ошибаться в проекции абстракции на конкретное описание задачи но это по-моему оно.
Здравствуйте, Glоbus, Вы писали:
G>Думается мне, это нереально, потому что машина не знает — что такое сортировки, да и вообдще что такое алгоритмы. Длятого, чтобы понять, что делает алгоритм, нужно обладать дополнительными знаниями — например значть что такое сортировка.
Inductive lelistA (a:A) : list A -> Prop :=
| nil_leA : lelistA a nil
| cons_leA : forall (b:A) (l:list A), leA a b -> lelistA a (b :: l).
Hint Constructors lelistA.
В соседних модулях есть определение перестановки списка, сортировки кучей и того, что heapsortом из любого списка можно получить его перестановку, являющаяся отсортированным списком.
Возможно — по крайней мере двух этих алгоритмов — но без их трассировки — никак
Опишиите действия человека в данной ситуации — да , он должен знать назначение этих алгоритмов — аналогично и с машиной — она тоже должна знать назначение.
Соответственно если не знать назначение алгоритма — доказать эквивалентость сложнее — и человек не всегда это сможет сделать.
Здравствуйте, Кодёнок, Вы писали: Кё>А я и не говорю о теоретической возможности построить для машины Тьюринга алгоритм определения эквивалентности алгоритмов (тоже наверное для машины Тьюринга которой не существует). Я о возможной реализации.
Кстати, очень точное замечание. Многие образованные разработчики не берутся за некоторые задачи, зная их теоретическую неразрешимость. В частности, за проблему останова.
Тем не менее, нельзя забывать о том, что машина Тьюринга — суть математическая абстракция. Она не может существовать в природе. Мы работаем с ограниченными машинами. И для них можно решить многие неразрешимые задачи. В частности, проблема останова легко разрешима для машины с конечным состоянием: достаточно исполнять программу на второй машине вдвое быстрее и на каждом такте сравнивать состояния. Если состояния совпали — значит программа вошла в бесконечный цикл (в силу детерминированности автомата). Для такой системы мы получим либо останов, либо цикл. На практике держать под рукой еще один синхронный пентиум 4 никто не будет, да и состояние машины (с учетом размера винта) позволяет писать циклы с неприлично большой длиной. Но для маленьких машин (например, для вычислений в рамках одного листа Excel) задача останова решается на раз-два.
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
Здравствуйте, Cyberax, Вы писали:
C>Для автоматического доказательства теорем. Используется, например, при C>доказательстве правильности алгоритмов.
C>Естественно, доказывать он умеет далеко не все
Здравствуйте, Sinclair, Вы писали:
S>Но для маленьких машин (например, для вычислений в рамках одного листа Excel) задача останова решается на раз-два.
По моим подсчетам число состояний для одного листа Excel значительно превосходит количество колебаний, совершенных всеми атомами Вселенной за время её существования.
Здравствуйте, Трурль, Вы писали: Т>По моим подсчетам число состояний для одного листа Excel значительно превосходит количество колебаний, совершенных всеми атомами Вселенной за время её существования.
Да. На практике можно даже для листа ексель построить несложный алгоритм, который имеет длину цикла, близкую к полному числу состояний. Естественно, решение проблемы останова в данном случае не будет иметь практического смысла
К счастью, природа этого алгоритма такова, что его построение невозможно выполнить случайно. Подавляющее большинство безостановочных алгоритмов, которые возникают в процессе разработки, имеют намного более короткие циклы.
... << RSDN@Home 1.1.4 stable rev. 510>>
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
которой не существует). Я о возможной реализации.
