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

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]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 транслятора, все неполные, один в Манчестере, один в ЛГУ. Формальным доказательством, насколько мне известно, никто себя не утруждал. В общем-то, даже и не вполне понятно, что это значит. От ограничений реализации и машины избавиться нельзя. Память, например, вполне конечная, но в Ван Вейнгаарденовских грамматиках никаких ограничений нет.

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


(Читать комментарии) -