Feb. 7th, 2008

akuklev: (Default)

[livejournal.com profile] shmel39
Мне всегда было интересно как верифицировать программы математически. То есть я теоретически представляю как это должно происходить, но мозг отказывается представить верификацию чего-то больше чем на несколько экранов :-( Или все гораздо проще?


ответ » )
akuklev: (Default)
Исходя из школьных знаний часто кажется, что математическое доказательство — это что-то нечёткое, написанное словами и проверяемое бородатыми дядями. И доказательство считается верным только если бородатые дяди не нашли ошибки. Какой-то негодный субъективный критерий.

На самом же деле доказательство легко формализуется. Впервые это сделали Гильберт и Фреге, но у них получилось не очень элегантно. Много лет спустя, в 1969 году было открыто соответствие Карри-Говарда (Curry-Howard), которое поставило всё на место.

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

Для описания какой-то конкретной теории в математике в первую очередь вводится подходящий язык, состоящий из общих для всей математики слов связок и грамматики, и специального для каждой теории словаря «существительных», «прилагательных» и «глаголов». Любое высказывание в рамках теории легко записывается и читается, будучи записано этими значками. Это просто язык.

Кроме языка теорию ещё определяет набор аксиом. Это набор высказываний, которые мы именуем какими-нибудь буквами типа w и q. Мы принимаем их правильными. Из них будут исходить наши доказательства. Это не значит, что мы "в них верим" или ещё чего-то в этом роде. Это просто посылки одной отдельно взятой теории, которая может ничего общего не иметь с реальным миром.

Ну вот с высказываниями разобрались, теперь перейдём к доказательствам.
Есть такая штука — называется лямбда-исчисление. Это просто способ записывать композицию функций. Если у нас есть на руках функции f и g, мы можем сделать функцию, которая вначале применяет g, а потом f. Записывается это, например, так:
h = ( x -> f(g(x)) )

Т.е. h = такая штука, которая берёт Х и выдаёт f(g(X)).

Если у функций f и g задан тип, мы можем вычислить тип этой вот новой функции h.

Дык вот выясняется, что мы можем считать наши аксиомы w и q "функциями", у которых типом является их высказывание. А любое доказательство мы можем записать как композицию элементарных аксиом. А ещё мы можем вычислить "тип" получившейся композиции и таким образом узнать, что же мы доказали. Если получившееся высказывание совпало с тем, которое мы хотели — эврика и ура. Доказательство верно. Проверялка доказательств без помощи всяких бородатых дяденек — это программа, занимающия на Perl'е примерно 20 строк. Её можно написать на коленке за полдня.

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

Следующая серия: http://akuklev.livejournal.com/605005.html
akuklev: (Default)
В предыдущем посте мы разобрались с тем, что такое доказательства и как их объективным образом проверять. Выяснилось, что это очень просто. Я рекомендую вначале прочитать его.
http://akuklev.livejournal.com/604920.html

Теперь поговорим о золотой мечте Гильберта. Давиду Гильберту хотелось вначале взять и переложить все основы математики на тот солидный фундамент, который я выше описал. Избавиться от несовершенного человеческого языка, больного многозначностями и недосказанностями, и перейти к использованию формального, а затем записать доказательства всех теорем так, чтобы их можно было механически проверить. И это было to great extent действительно сделано двумя независимыми группами — трёхтомником Principia Mathematica Уайтхеда и Рассела (1910-1913гг) и многотомником Николя Бурбаки (псевдоним группы французских математиков, 1930ые).

К сожалению, и то и другое было написано до открытия соответствия Карри-Говарда, появления читабельных формальных языков и компьютеров, поэтому читать эти книжки практически невозможно. Но тем не менее, свои задачи они выполнили — поставили математику на солидную основу. Посмотреть на тысячи формализованных и компьютерно проверенных доказательств в их современном виде можно вот тут: http://au.metamath.org/index.html

Второй пункт программы Гильберта состоял в том, чтобы доказать полноту и непротиворечивость основ математики, из которых растёт всё остальное — теории множеств и арифметики.

С первым Гильберта ждал крупный облом. Полнота теории — это когда мы можем любое высказывание в рамках теории доказать или опровергнуть. Гильберт сам бы мог догадаться, что полных теорий не бывает.
Помните парадокс Лжеца? Там человек говорит «я сейчас лгу». Если он говорит правду, значит он лжет. Если лжет — значит говорит правду. Короче, это высказывание — вовсе не высказывание, оно не может быть ни истинно, ни ложно. Подобное высказывание можно сформулировать в рамках любой теории, и звучит оно «это высказывание невозможно доказать». Если его возможно доказать, значит оно ложное, если невозможно — истинное. Итого:
Всякая теория, способная к рефлексии (т.е. такая, что высказывание «это высказывание невозможно доказать» можно написать её языком) неполна. И в принципе нету в этом ничего страшного или удивительного. Нельзя зафиксировать конечным количеством аксиом ответы на все-все вопросы.
* Это, кстати, называется, первой теоремой Гёделя о неполноте.

Но есть ещё второй пункт. Там, где про непротиворечивость основ математики. Но как доказывать непротиворечивость, из чего исходить? Не можем же мы исходить из самих основ. Мы ещё не знаем, что они непротиворечивые. Гильберт предложил исходить из теории, содержащей очень-очень-очень простой набор аксиом, самый простой из возможных — чтобы каждый поверил, что уж тут точно не может быть противоречия. И в рамках этой теории нужно доказать две вещи:
1) Что она сама непротиворечива.
2) Что непротиворечива теория множеств и арифметика.

Народ ещё не успел заняться этим делом вплотную, как Гёдель доказал свою вторую теорему о неполноте. И её содержание было ужасно:
«В рамках теории, содержащей арифметику, нельзя доказать её собственную непротиворечивость»

Доказательство непротиворечивости теории её же методами просто было бы бесконечно длинным, а это уже не доказательство, а фигня какая-то.

После этой теоремы семь десятилетий считалось, что это Гильбертовский подход обречён, что нас всегда будет преследовать арифметическая иерархия и доказать непротиворечивость как-то нормально не получится. Оказалось, ничего подобного. В 2001 году Дан Виллард обнаружил, что можно придумать теорию, которая рефлексивна in appropriate sense, но не содержит арифметики. В рамках этой самой системы удалось доказать оба высказывания:
- и то, что эта система сама непротиворечива,
- и то, что непротиворечива теория множеств.*

http://en.wikipedia.org/wiki/Self-verifying_theories

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

Следующая серия: http://akuklev.livejournal.com/605330.html
_____
* — тут есть тонкость, описываемая в следующей серии. На самом деле доказывается непротиворечивость арифметики Пеано на определимых внутри неё объектах. Это доказывает непротиворечивость NBG-теории множеств в рамках её constructable universe.
akuklev: (Default)
Из прошлых двух постов стало ясно, что с основаниями математики вроде бы, всё в порядке. Высказывания можно записывать точно, избегая субъективной трактовки и неточностей описания. Доказательства тоже можно записывать на специальном языке и проверять несложной компьютерной программкой или вручную на листе бумаги, избегая всякой субъективности. Я рекомендую вначале прочитать их.
http://akuklev.livejournal.com/604920.html
http://akuklev.livejournal.com/605005.html

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

Но вот беда. Все рефлексивные теории неполны. Т.е. в них есть высказывания, которые не докажешь и не опровергнешь. Что же это за такой ужас? Неужели математика слишком слаба, чтобы отвечать на свои внутренние вопросы?!
Оказывается, что нет. Всё хорошо. Дело не в том, что мы не можем доказать и опровергнуть высказывание из-за слабости наших методов. Дело в том, что ответ на этот вопрос просто не зафиксирован набором аксиом. Самый известный пример: Гипотеза Континуума.

В рамках теории множеств существуют бесконечные множества разной величины. Множества, объекты в к которых можно пронумеровать, называются счётными. У них такой же размер, как у множества натуральных чисел. Однако бывают множества, объекты которых не пронумеруешь хоть убейся. Такие множества называются несчётными. Самое известное из них — множество действительных чисел.
Гипотеза континуума гласит: Не существует множеств, которые больше множества натуральных чисел и меньше множества действительных.

Выясняется, что эту гипотезу в рамках теории множеств нельзя ни доказать, ни опровергнуть. Как же так? А дело на самом деле вот в чём. Множства, которые несчётны, но меньше множества действительных чисел, нельзя в рамках теории множеств сконструировать. Но с другой стороны, если нам пошлют такое множество с неба, теория множеств сможет с ним работать без всяких противоречий.
То есть, нет никаких оснований полагать, что их нету: если нам их дадут — будут. Но и нет никаких оснований полагать, что они есть, потому что сделать их сами мы не можем. Гипотеза континуума просто абсолютно независима от остальных аксиом теории множеств. Она является открытым вопросом, ответ на который не зафиксирован другими аксиомами.

С этим вроде бы, всё понятно. Но как быть с высказыванием «теория множеств непротиворечива»? Ведь мы его доказали в рамках другой, более простой теории. Т.е. по-существу оно верное, а доказать в рамках, собственно, теории множеств не можем. На лицо какой-то непорядок.

И как обычно, корень зла лежит в недостаточно глубоком анализе. Для того, чтобы изучить вопрос, что такое верность высказываний «по существу» (а не их доказуемости) была разработана Теория Моделей. Она прояснила множество вопросов. Однако, разработана она была намного позже работ Гёделя, поэтому мы простим ему неверную трактовку «верности по-существу».

Выясняется, что когда мы доказали непротиворечивость теории множеств/арифметики Пеано, мы доказали её только для области конструируемых объектов. А вот если допускать существование всяких «упавших с неба», то непротиворечивость теории множеств является существенно открытым вопросом.

Не менее известный существенно открытый вопрос — это аксиома выбора. Она независима от других аксиом. Если её не принимать, у нас получается одна математика, если принимать — немного другая. Математика без аксиомы выбора бедновата. Математика с — весьма богата, в том числе и не парадоксы. Но не смотря на эти кажущиеся парадоксы, она совершенно непротиворечива. Часто возникает вопрос — а как же оно "на самом деле"? Верна всё-таки аксиома выбора или нет?

Я открою страшную тайну. Там где начинаются бесконечные множества и действительные числа, «на самом деле» кончается. Вы когда нибудь видели действительное число? Нет? И я не видел. Пока мы оперируем конечными множествами простых объектов, мы остаёмся в рамках исчисления предикатов. Курт Гёдель доказал, что в рамках исчисления предикатов как раз имеет место полнота. Т.е. тут-то как раз нету открытых вопросов, в всё можно доказать или опровергнуть. В них просто гипотетически всё можно "проверить".
А теория множеств и всё остальное — это мысленные идеализации. Они ничего не рассказывают нам об устройстве мира, они просто служат нам плацдармом для построения моделей — физических, экономических, биологических моделей. И всякая такая теория ровно настолько хороша, насколько она удобна для своих целей. Математика с аксиомой выбора гораздо удобнее для построения современной физики, и поэтому мы пользуемся ей.
akuklev: (Default)
Прелестное via [livejournal.com profile] sharp_idler:
A dying mosquito exclaimed,
“A chemist has poisoned my brain!”
The cause of his sorrow
Was para-dichloro-
Diphenyl-trichloroethane.
akuklev: (Default)
В прошлых сериях мы обсудили основания математики. Мы выяснили, что такое формальный язык и доказательство; узнали, что вся современная математика была поставлена на верифицируемую (лишенную субъективности проверки) основу, что была доказана непротиворечивость основ математики и хорошо понята их неполнота. Ещё мы поняли, что теория множеств — это идеализация, помогающая строить модели — в первую очередь модели для естественных наук.

Назовём мир теории множеств платоническим раем. В нем нёту объектов, в нем есть только значения. В смысле есть values и нет objects. В чём разница?
Вот яблоко — это яблоко. Его можно потрогать. Если у вас два разных яблока — это два разных яблока. Вас можно спросить — «а сколько у тебя яблок» — и вы скажете, что два. Можно поинтересоваться, сколько в мире вообще есть яблок и всё это будет иметь смысл. Яблоко — это объект.
А вот если у вас есть число 5 — это значение, с ним всё совсем иначе. Во-первых число пять не бывает «у вас». Оно бывает только "вообще". Во-вторых, вопрос «а сколько есть чисел пять?» — вопрос идиотский и бессмысленный. И даже сам вопрос «а существует ли число пять?» начисто лишён привычного смысла. В математике просто нету понятия «существует ли в принципе». Слово «существует» используется в совершенно другом смысле. Вот в таком: «Существует ли натуральное число, равное 4 + 1» — да, существует. «А существует ли натуральное число, равное 3/2» — нет, не существует. Т.е. мы интересуемся, являются ли указанные нами свойства взаимоисключающими. В первом случае эти свойства «является натуральным числом» и «равняется 4 + 1». И в данном случае они не являются взаимоисключающими. Во втором — являются. Согласитесь, ничего общего с существованием яблока.

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



дальше » )
Page generated Aug. 29th, 2025 06:43 am
Powered by Dreamwidth Studios