Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет Misha Verbitsky ([info]tiphareth)
@ 2007-06-20 23:11:00
Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Настроение: sick
Музыка:Куклы Напрокат - ПОВЕРИЛА
Entry tags:logic, math

тезис о формализации математики
Неожиданно сообразил:
а ведь убежденность в возможности формализации
математических доказательств есть примерно то же самое,
что тезис Черча, утверждающий, что любой алгоритм (в
житейском смысле этого слова) сводится к
машинам Тьюринга. Сейчас считается, что это
определение алгоритма, в силу очевидной
недоказуемости тезиса. Люди пишут на языках
высокого уровня, предполагая, что перевести программу
на машинные коды или к машине Тьюринга или
свести доказательство к формальным языкам
при желании всегда можно. Хотя этого никто не
проверял, и проверить не может (трансляторы
в машинные коды существуют, но доказать их
безошибочность - задача такой же сложности,
как и проверка формализуемости доказательства).

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

Привет


(Добавить комментарий)


[info]kouzdra
2007-06-21 01:27 (ссылка)
Есть разница - тезис Тьюринга - где-то опытный факт - пока никто не смог предъявить пример алгоринтма (в интуитивно ясном смысле слвоа), который бы не подходил под тезис.

С возможностью формализаций доказателств ситуация прямо противоположная - вторая теорема о неполноте утверждает существование истинного, но формально не доказуемого утверждения. И предъявляет его.

(Ответить) (Ветвь дискуссии)

Perelman in a Subway
(Анонимно)
2007-06-21 01:35 (ссылка)
http://englishrussia.com/?p=998

(Ответить) (Уровень выше)


[info]tiphareth
2007-06-21 01:50 (ссылка)
А вот нифига. Число Омега Хайтина невычислимо
теоретически, практически же очень просто вычисляется -
пишешь N случайных программ, запускаешь, считаешь процент тех,
которые остановились за K ходов, устремляешь N и K к
пределу. Типа метод Монте-Карло.

Ну или еще проще - воспользуйся тем, что множество
рациональных чисел меньше Омеги перечислимое.

Такие дела
Миша

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]gaz-v-pol.livejournal.com
2007-06-21 11:19 (ссылка)
Забавно, а как так может быть? Вообще, казалось бы, множество программ счетно, поэтому из этого множество нельзя случайно выбрать одну (или 100) программ ?

Кроме того, не вполне ясно, как проверять, является ли данный конкретный набор символов текстом программы ?

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]polytheme
2007-06-22 11:25 (ссылка)
http://en.wikipedia.org/wiki/Chaitin_Omega
:)
привет, Сережа

(Ответить) (Уровень выше)


[info]polytheme
2007-06-22 11:23 (ссылка)
а, вы опять шутите.

(Ответить) (Уровень выше)


[info]kaledin
2007-06-21 01:41 (ссылка)
Nu, tezis Church'a ehto formal'no ne to -- vernee, tam dve sostavlyayushchie (1) chto ty skazal, i (2) chto tri ne to chetyre izvestnykh na tot moment sovershenno raznykh opredelenij vychislimosti ehkvivalentny. I (2) togda zhe bylo strogo (khotya i mutorno) dokazano, chto i porodilo (1).

(Ответить) (Ветвь дискуссии)


[info]tiphareth
2007-06-21 04:13 (ссылка)
Википедия по ссылке только про первое значение

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2007-06-21 05:04 (ссылка)
Nu mozhet byt', vopros chisto terminologicheskij. No vazhno, chto est' (2) -- a priori sovershenno ne ochevidno, chto mashina Turing'a, \lambda-calculus i rekursivnye funkcii dayut odno i to zhe. Ehto tipa falsifiable prediction.

(Ответить) (Уровень выше)


[info]pzz
2007-06-21 01:41 (ссылка)
Всю свою сознательную программисткую жизнь я разделял идею Дейскстры о том, что тесты могут показать наличие в программе ошибок, но не их отсутствие.

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

С практической точки зрения доказывать для любого P не обязательно. Достаточно, чтобы P было достаточно мало (sorry за тавтологию). Например, на несколько порядков меньше вероятности сбоя железа.

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

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

(Ответить) (Ветвь дискуссии)


[info]belater
2007-06-21 16:53 (ссылка)
Дык, про вероятность Р того, что программа не содержит ошибок, давно известно. Называется good enough software - т.е. мы признаем, что да, в программе могут содержаться ошибки, но все равно наш софт достаточно хорош.

Только мне сложно понять мысль о том, как 2 теста могут давать одинаковую вероятность безошибончсти. Вы имеете ввиду, что они покрывают один кусок задач? Так зачем вообще такие тесты создавать изначально?

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]pzz
2007-06-21 17:16 (ссылка)
Good enough понятие маркетинговое, а не техническое. Оно означает, что даже с учетом тех, кто будет не доволен и вернет программу (а так же тех, кто под их влиянием программу не купит), все равно выгодно начинать продавать свою вонючую недоделку прямо сейчас, а не когда заработает.

Забавным следствием этого является то, что good enough для недорогих и массовых коробочных програм гораздо более жесткий, чем для програм, которые стоят, например, $10,000. Это получается потому, что содержательно поддерживать по телефону миллионы пользователей очень дорого. А у програм за $10K будет всего несколько сотен покупателей в год, ими можно заниматься и персонально. Т.е., если вы покупаете программу за $100, скорее всего она хоть как-то, но будет работать прямо из коробки. Если за $10K, то работать в конечном итоге будет, но заставить ее это делать будет непросто. Если за $100K, то работать не будет совсем, но зато у вас будет персональный консультант (а за $1000K разработчики переедут жить в Ваш оффис).

Меня же сейчас интересуют критерии корректности софтвария именно в техническом смысле, а не в финансовом.

Чтобы всерьез рассматривать тестирование как способ проверки корректности программы, надо научиться как-то оценивать осмысленность самих тестов. Ведь очевидно, что если уж даже программы теперь пишут "на глазок", то тесты в среднем совсем ни про что. Занимаются ими (к сожалению!) люди, которых в программисты не взяли.

Я вот предложил более-менее формальный способ такой оценки.

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

Тестировать методом Монте-Карло занятие безнадежное. Потому что чтобы убедиться в безошибочности с вероятностью 1/10000, надо сделать порядка 10000 разных тестов. А вот если бы каждый следующий тест делил вероятность незамеченной ошибки пополам, хватило бы 13-и с половиной тестов.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]polytheme
2007-06-22 12:08 (ссылка)
самая большая проблема, насколько я понимаю, не в проверке правильности, а в формализации задачи. т.е. для обычной программы проблемы правильности вообще стоять не может, потому что чего она должна делать, никому не известно.

(Ответить) (Уровень выше)


[info]bigturtle
2007-06-21 18:47 (ссылка)
http://www.inria.fr/rapportsactivite/RA2006/vertecs/uid18.html

(Ответить) (Уровень выше)


[info]zemsky.livejournal.com
2007-06-30 23:49 (ссылка)
Всю свою сознательную программисткую жизнь я разделял идею Дейскстры о том, что тесты могут показать наличие в программе ошибок, но не их отсутствие.

Вобщем-то, как тестировщик, согласен с этим. Да и как доказать отсутствие чего-либо?

(Ответить) (Уровень выше)


[info]pzz
2007-06-21 01:48 (ссылка)
Насколько я понял тезис Черча, он эквиавалентен утверждению, что любой алгоритм в житейском смысле слова может быть записан в виде программы на языке высокого уровня.

Насколько я понимаю, написать формально доказанный компилер, скажем, с C в ассемблер MIX это вполне подъемная задача. Значительно сложнее написать доказанный компилер, который кроме корректности обладает всякими другими полезными свойствами, которые мы ждем от современного компилятора - например, выдает более-менее оптимизированный код для настоящего процессора, сравнимого по сложности с Пентиумом.

(Ответить) (Ветвь дискуссии)


[info]tiphareth
2007-06-21 01:52 (ссылка)

Нам нужен транслятор из C в машину Тьюринга. Доказанный.
Это возможно, но потребует не один год работы. К тому же
не факт, что любой алгоритм может быть записан на C.
То есть это предмет веры скорее.

Такие дела
Миша

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]pzz
2007-06-21 04:49 (ссылка)
C не самый удачный пример. У него достаточно сложная спецификация, с многочисленными тонкостями. Доказать что что-то соответствует этой спецификации достаточно тяжкий труд. Но можно сконструировать язык не менее юзабельный, чем C, но при этом более простой (более преспособленный для всяких формалных действий с ним). Собственно, LISP такой язык, но, не желая обидеть пользователей Емакса, я тем не менее не очень уверен в его юзабельности :-)

Разницы между трансляцией в машину Тьюринга и в какой-нибудь незамысловатый ассемблер особой нет. В машину Тьюринга даже проще.

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

Или, иными словами, я не очень понимаю разницу между терминами computation и алгоритм. Хотя нутром чую, что это не одно и то же :-)

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]euk
2007-06-21 08:57 (ссылка)
Собственно, LISP такой язык, но, не желая обидеть пользователей Емакса, я тем не менее не очень уверен в его юзабельности :-)

Greenspun's Tenth_Rule
наивно было с Вашей стороны полагать, что за ЛИСП могут вступиться только пользователи Емакса. А транслировать в машину Тьюринга смысла особого нет. Есть диалекты ЛИСПа, использующие лямбда-исчисление в чистом виде, и смысла хвататься за постылый C, юзабилити которого также можно ставить под сомнение, лично я не вижу.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]pzz
2007-06-21 16:02 (ссылка)
Это был реверанс в сторону Миши :-)

(Ответить) (Уровень выше)


[info]nikto
2007-06-21 12:53 (ссылка)
Насчет того, что любой алгоритм может быть написан на C, да, в этом-то и загвоздка.
А понятие Тьюринг-полноты разве не это подразумевает? (как я его понимаю, по крайней мере)

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]pzz
2007-06-21 15:52 (ссылка)
Нет, понятие Тьюринг-полноты подразумевает, что любой алгоритм, который можно записать на C может быть выполнен на машине Тьюринга (или переписан на любом другом Тьюринг-полном языке).

Но это вовсе не означает, что любое вычисление может быть записано в виде алгоритма на C. Впрочем, я не понимаю, как в принципе могло бы выглядеть вычисление, которое нельзя сформулировать в виде алгоритма (но тем не менее можно вычислить).

(Ответить) (Уровень выше)


[info]kaledin
2007-06-21 05:05 (ссылка)
Ya podozrevayu, chto dlya Algola-68 takoj translyator est'. S nikh stanetsya. Lisp zhe, vrode by, perevoditsya v \lambda-calculus sovershenno pryamolinejno (i sobstvenno im i yavlyaetsya).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]pzz
2007-06-21 15:56 (ссылка)
Ну скорее уж для Ады. Я вообще не уверен в том, что компилятор Алгола-68 существует в природе. Говорят, они там немножко перестарались, когда придумывали этот язык. А Адовские компилеры точно существуют, и вроде как даже обязательны к использованию в военном программировании.

P.S. Аду часто критикуют за чрезмерную сложность и т.п. Однако надо заметить, что в стравнении с современным C++ Ада это маленький, простой, изящный язык с ясным синтаксисом и понятной семантикой. Более того, даже PL/1 на фоне C++ не так уж и плохо смотрится :-)

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]yushi
2007-06-22 01:24 (ссылка)
Ада — совершенно не тот язык, корректность программ на котором удобно доказывать. А удобно это, насколько я понимаю, для чего-нибудь типа OCaml и Haskell.

Кто-то из апологетов ФП ([info]smilga@lj, кажется, хотя не скажу наверняка) как-то сказал замечательную фразу: "И Perl, и Ада — помойка; просто Perl — это помойка университетского кампуса, а Ада — помойка казармы". Сразу скажу, что я с ним не полностью согласен, по результатам недолгих экспериментов с GNAT Ада мне вполне глянулась — этакий доведённый до ума Паскаль (хотя Оберон в этом смысле ещё симпатичнее, да и синтаксис там поприятнее), но до действительно строгих языков типа того же Haskell ей и правда очень далеко.

(Ответить) (Уровень выше)


[info]yushi
2007-06-22 01:39 (ссылка)
Но C++ и правда чудовищен. Впрочем, как и всякий "индустриальный" язык, наверное — Java, C# и Object Pascal в версии от Борланд, по-моему, ещё гаже (ну, честно говоря, вообще из популярных языков рвотного рефлекса не вызывает, пожалуй, только Python). C++ кто-то обозвал "ассемблер с классами" ([info]lispnik@lj, кажется, но я опять же не уверен), и это очень точно характеризует этот язык. Я на одной из работ вынужден участвовать в разработке довольно крупного приложения на плюсах, и в полный рост наблюдаю истинность уже упомянутого здесь 10 правила Гринспуна. Видимо, единственная программа из известных, которая написана правильно — это как раз Emacs: Столлман сразу начал с написания LISP-машины вместо того, чтобы позже выдумывать её кривой рукосуйный аналог.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]pzz
2007-06-22 05:09 (ссылка)
Java и C# конечно лучше. В них хоть строки не надо конструировать руками из подручных запчастей.

Про Object Pascal мне трудно рассуждать. Виртовский Паскаль сконструирован с довольно глупыми ошибками. Например, то, что вызов функции без параметров синтаксически неотличим от присваивания переменной в совокупности с тем, что вызов функции по указателю неотличим от вызова функции по имени приводит к тому, что функция не может вернуть в качестве значения указатель на функцию (передать при этом функцию в качестве параметра можно).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]yushi
2007-06-22 10:32 (ссылка)
В них хоть строки не надо конструировать руками из подручных запчастей.

Эхм. Вы char* имеете в виду? Но, вообще-то, класс string входит в стандарт ISO C++, это типа часть языка (как и STL). Хотя, конечно, избавление от рудиментов C (типа тех же указателей или функций-неметодов), несомненно, пошло Жабе и C# на пользу.

Виртовский Паскаль сконструирован с довольно глупыми ошибками.

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

Хотя что касается меня, то мне возвращать указатели на функции хочется регулярно…

(Ответить) (Уровень выше)


[info]yushi
2007-06-22 01:09 (ссылка)
Дадад. На мой дилетантский взгляд, машина Тьюринга — наиболее уродливый из способов формализовать понятие вычислимости, и чего Миша к нему прицепился — непонятно. В то время как \lambda-исчислением народ вполне пользуется на практике; собственно, я в каком-то хорошем учебнике по программированию читал подробное объяснение, почему операция присваивания — это зло и пользоваться ей не надо. И в качестве одной из причин называлась как раз невозможность формального доказательства правильности программ с присваиванием.

При этом следует заметить, что в функциональных языках присваивание действительно нахрен не нужно, а в каких-то из них его так и просто нет.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]polytheme
2007-06-22 11:48 (ссылка)
потому что обычный компьютер (а не Лисп-машина, например, хотя и она, подозреваю, тоже) и есть машина Тьюринга без бесконечной ленты.

"невозможность формального доказательства правильности программ с присваиванием" ???
вообще-то любую программу с присваиванием можно переписать в программу без присваивания

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]yushi
2007-06-22 21:06 (ссылка)
потому что обычный компьютер (а не Лисп-машина, например, хотя и она, подозреваю, тоже) и есть машина Тьюринга без бесконечной ленты.

Ну, как верно замечают выше по треду, машина Тьюринга и то же \lambda-исчисление эквивалентны по всем полезным математическим свойствам; так что, собственно, после констатации этого факта мы можем забыть про это угробище, как про страшный сон.

вообще-то любую программу с присваиванием можно переписать в программу без присваивания

Ага. Я даже это понял, когда уже написал коммент; но решил далее не флудить.

(Ответить) (Уровень выше)


[info]polytheme
2007-06-22 12:05 (ссылка)
более того, формальное доказательство правильности любой программы с присваиванием тоже невозможно.
меня тут смущает слово "невозможность" :)
на самом деле ты наверное имел в виду большую сложность ?

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]yushi
2007-06-22 21:18 (ссылка)
Ну да. На самом деле, я вспомнил, что это за учебник — SICP в переводе известного тебе [info]gogabr. Там аж несколько параграфов в начале третьей главы посвящены вреду присваивания; но самое сильное утверждение, действительно, выглядит всего лишь как:

Как мы только что видели, операция set! позволяет моделировать объекты, обладающие внутренним состоянием. Однако за это преимущество приходится платить. Наш язык программирования нельзя больше описывать при помощи подстановочной модели применения процедур, которую мы ввели в разделе 1.1.5. Хуже того, не существует простой модели с "приятными" математическими свойствами, которая бы адекватно описывала работу с объектами и присваивание в языках программирования.

В целом, как видно из отрывка, там речь о том, что референциально прозрачные языки (вроде Haskell или Clean; или Scheme без set! и аналогов, которая собственно и изучалась в первых главах SICP) изоморфны лямбда-исчислению, и это очень удобно для тех, кто про программы на них хочет что-то доказать.

(Ответить) (Уровень выше)


[info]yushi
2007-06-22 21:26 (ссылка)
более того, формальное доказательство правильности любой программы с присваиванием тоже невозможно.

Хм. Ну что такое "проблема остановки" я всё же знаю, иначе что бы я делал в комментариях к этому посту?

(Ответить) (Уровень выше)


[info]polytheme
2007-06-22 12:05 (ссылка)
пардон, без присваивания

(Ответить) (Уровень выше)


[info]qwerty
2007-06-23 04:13 (ссылка)
С Алгола-68 было написано 3 транслятора, все неполные, один в Манчестере, один в ЛГУ. Формальным доказательством, насколько мне известно, никто себя не утруждал. В общем-то, даже и не вполне понятно, что это значит. От ограничений реализации и машины избавиться нельзя. Память, например, вполне конечная, но в Ван Вейнгаарденовских грамматиках никаких ограничений нет.

(Ответить) (Уровень выше)


[info]dmitri83
2007-06-21 14:46 (ссылка)
Существует компилятор некоторого C-подобного языка, сертифицированный (он написан на proof assistant-е Coq, а тот устроен так, что все программы, написанные на нём, грубо говоря, содержат доказательство своей корректности). Компилирует для PowerPC, а оттуда уже думаю несложно построить трансляцию в машину Тьюринга и доказать её корректность.

http://pauillac.inria.fr/~xleroy/publi/compiler-certif.pdf

(Ответить) (Уровень выше)

Какую страну просрали!
[info]svgmzr.livejournal.com
2007-06-21 02:34 (ссылка)
В википедии попалась ссылка на брошюру про теорему о неполноте. 82 год, тираж - 100,000.

(Ответить) (Ветвь дискуссии)

Re: Какую страну просрали!
[info]tiphareth
2007-06-21 02:39 (ссылка)
Успенского? Я читал ее, если не путаю. Офигительно понятный текст.

Да, феноменальные сволочи. Страна была классная.

(Ответить) (Уровень выше)


[info]vadvad
2007-06-21 03:20 (ссылка)
http://vt.samgtu.ru/PrepodsVt/thestch.htm
Забавное, хотя ФТ математикой не является.

(Ответить) (Ветвь дискуссии)


[info]tiphareth
2007-06-21 03:23 (ссылка)
Угу. Но в принципе, доказывать особо нечего:
квантовый компьютер нечерчевский

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2007-06-21 03:26 (ссылка)
Впрочем, у него, кажется, есть черчевская модель
в виде обычного компьютера, который делает астрономическое
количество вычислений. Но гипотетический квантово-гравитационный
компьютер, придуманный Пенроузом, уже никак не моделируется.

Такие дела
Миша

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]vadvad
2007-06-21 10:19 (ссылка)
Крылов насколько мне известно довел свой аналоговый процессор до действующей модели, что весьме небесполезно для некоторых приложений, но производить некому.

(Ответить) (Уровень выше)

Если я правильно понимаю
[info]belater
2007-06-21 17:01 (ссылка)
Любой алгоритм, написанный на современном компьютере, в конечном итоге сведется к простым арифметическим операциям. А их машина Тюринга делать умеет.

(Ответить) (Ветвь дискуссии)

Re: Если я правильно понимаю
[info]polytheme
2007-06-22 12:03 (ссылка)
тут некоторая путаница. идеальный компьютер действительно подчиняется ТЧ просто по той причине, что он по конструкции - кастрированная МТ.
но реальный - нет, не подчиняется, потому что у него там унутре искорки скачуть, и parity control в микросхемы памяти вставлен неспроста.

(Ответить) (Уровень выше)


[info]ded_maxim
2007-06-22 19:08 (ссылка)
Миша, с прошедшим днем рождения!

(Ответить)