Здравствуйте, koenig, Вы писали:
K> ты к чему-нибудь практическому пруверы или какие-нибудь там модел-чекеры смог пристягнуть?
Если не играться, а так чтобы практика-практика, у меня был проектик на Идрисе, который генерировал код на C#, который потом использовался в одном из продуктов (GraphEditPlus). Но там примерно с тем же успехом мог бы использоваться и хаскель, и другие подобные. Особого пруверства не было, а зависимые типы использовались по мелочам, вроде сделать число аргументов у ф-ии различным в зависимости от содержания строки в первом (а-ля printf).
Re[3]: Про формализация математических теорем и язык Coq
K>я вот думаю маленькую распределенную системку на дотнете накалякать и ищу чем формальные методы могут мне помочь K>и получается, что ничем
Tla+ Лэмплрта чем не то? Можно найти введение в это дело+видео лекции Лэмпорта. Использовались в амазон для валидации DynamoDb. Да много где использовалась, в том числе и им.
Кодом людям нужно помогать!
Re[4]: Про формализация математических теорем и язык Coq
K>>я вот думаю маленькую распределенную системку на дотнете накалякать и ищу чем формальные методы могут мне помочь K>>и получается, что ничем
S>Tla+ Лэмплрта чем не то? Можно найти введение в это дело+видео лекции Лэмпорта. Использовались в амазон для валидации DynamoDb. Да много где использовалась, в том числе и им.
я так понимаю, кодогенерации там нет
т.е. построил модель — а дальше ручками. тут то я всё и испохаблю.
я не пытаюсь что-то очень сложное сделать (для чего tla в самый раз), я пытаюсь извести баги в коде, который нормально протестировать я не смогу
это всё, видимо, очень наивно
Re[5]: Про формализация математических теорем и язык Coq
K>я так понимаю, кодогенерации там нет K>т.е. построил модель — а дальше ручками. тут то я всё и испохаблю. K>я не пытаюсь что-то очень сложное сделать (для чего tla в самый раз), я пытаюсь извести баги в коде, который нормально протестировать я не смогу K>это всё, видимо, очень наивно
Реализацию нет, а вот алгоритм, точнее модель, да.
Кодом людям нужно помогать!
Re[2]: Про формализация математических теорем и язык Coq
DM>Если я все правильно путаю, то в Коке и аналогах математика конструктивная, логика интуиционистская, не булева. Т.е. не работают доказательства от противного, и нужно уметь из одних утверждений производить другие гарантированно завершающимся алгоритмом (нет Тьюринг-полноты, и это важно, т.к. Тьюринг-полная программа может всегда зависнуть и тем самым служить недовычисленным доказательством любого утверждения). А посему вещественные числа и обычный матан уже довольно сложно описать (если вообще можно). Привычные определения и теоремы из матана часто подразумевают "бесконечные циклы" — пределы бесконечных последовательностей и операции с ними. Хорошо идет всякая дискретка, а с континуальными вещами уже сложно.
Классическую логику тоже можно
example (h : ¬¬p) : p :=
by_contradiction
(assume h1 : ¬p,
show false, from h h1)
см. 3.5. Classical Logic здесь
DM>Ну и чисто организационно: заставить всех математиков освоить такой язык и переучиться на его использование малореально. Очень по-другому там строятся и выглядят доказательства, сам ход мысли часто очень отличается.
Всех математиков и не надо наверно, но если не проверять доказательства программно, нельзя поручиться, что в них не закралась ошибка. Не зря Воеводский занялся этой областью, его очень беспокоил этот вопрос.
Re: Про формализация математических теорем и язык Coq
Здравствуйте, Shmj, Вы писали:
S>Почему до сих пор не обязали всех математиков представлять свои доказательства в строго формальном виде, к примеру на языке Coq? Тогда сразу будет видно верно доказательство или нет.
S>Ну и второе. Кто с этим вообще сталкивался, насколько оно удобно как универсальный язык математики? Почему до сих пор не перевели доказательство Великой Теоремы на этот язык?
В тему: вот цитата старого поста одного профессионального математика на форуме dxdy.ru:
Я думаю, что идея о том, что математический дедуктивный вывод можно формализовать (логически) это идеализация. Я думаю, что логическая формализация сделала бы математические рассуждения очень громоздкими и почти непонятными. Обычно математики рассуждают не на формальном уровне, а на уровне идей, интуиций, пусть даже очень простых, вроде интуиции арифметических операций с натуральными числами. Иногда эти рассуждения даже заведомо формально неправильны (впрочем, лично я, в отличие от некоторых своих коллег, избегаю подобных рассуждений). Например, один мой друг под моим рецензентским давлением выдвинул принцип: «в рамках соответствующей теории изоморфные математические структуры можно рассматривать как тождественные».
По идее, математические доказательства это строгие, правильные математические дедуктивные рассуждения. В реальной, развивавшейся математике они не всегда были окончательно формализованы (например, «Начала» Евклида содержат довольно туманные определения), и Рассел даже заявил, что «Законы мысли» Буля были «первой книгой, когда-либо написанной по математике».
Для своего времени и вплоть до (примерно) XIX века «Начала» считались образцом логического изложения математической теории. Структура трудов Декарта, Ньютона и даже Спинозы строилась по образцу «Начал». Однако уже в античные времена были критически отмечены некоторые недостатки евклидовского труда — например, Архимед обосновал необходимость добавить «аксиому Архимеда» (которую сформулировал ещё Евдокс, живший до Евклида). Со временем число признанных недостатков постепенно увеличивалось. Современные взгляды на обоснование, содержание и методы как геометрии, так и арифметики существенно отличаются от античных[13].
Прежде всего, следует отметить, что сейчас прямая понимается как линия бесконечной длины. Античные учёные полностью избегали понятия актуальной бесконечности, у Евклида всюду используются только конечные отрезки прямой[14]. Видимо, по этой причине постулат параллельности Евклида сформулирован довольно громоздко — зато он имеет локальный характер, то есть описывает событие на ограниченном участке плоскости, в то время как, например, аксиома Прокла («через точку вне прямой проходит только одна прямая, параллельная данной») утверждает факт параллельности, который требует рассмотрения всей бесконечной прямой[15]. Ещё одной архаичной особенностью «Начал» является ограничение только двумя видами кривых — прямыми и окружностями, которые греки считали единственно совершенными[16], а также чрезмерно узкое понятие числа, которое не включало иррациональных чисел и поэтому вынудило античных математиков без особой нужды ввести параллельное с арифметикой исчисление «геометрических величин» («геометрическая алгебра», книга II «Начал»)[17].
Многие комментаторы Евклида отмечали, что данные им определения геометрических понятий бессодержательны и создают не более чем наглядный образ — например, «линия есть длина без ширины». Фактически подобные «определения» нигде далее в тексте не используются, ни одна теорема на них не опирается[13]. Излишним оказался, как уже говорилось выше, и IV постулат Евклида о равенстве всех прямых углов, его можно доказать как теорему[18][19].
Далее, по замыслу все доказательства теорем должны вытекать из явно сформулированных аксиом. На самом деле многие факты у Евклида опираются на подразумеваемую или наглядную очевидность. Прежде всего это касается понятия движения, которое неявно используется во многих местах — например, при наложении треугольников для доказательства признаков их равенства. Уже Прокл отметил этот факт как существенный методический пробел. Аксиом движения Евклид не дал — возможно, чтобы не смешивать высокую геометрию с «низкой» механикой. Современные авторы аксиоматики предусматривают специальную группу «аксиом конгруэнтности» [20][21].
Уже в доказательстве самого первого предложения («на любом отрезке можно построить равносторонний треугольник») Евклид подразумевает, что две окружности радиуса R, чьи центры находятся на расстоянии R, пересекаются в двух точках. Ни из каких аксиом это не следует[22]; для логической полноты следовало бы добавить аксиому непрерывности. Аналогичные упущения имеют место для пересечения прямой и окружности[23], в употреблении неопределяемого понятия «находиться между» (для точек) и в ряде иных мест. Аксиоматика Евклида не позволяет, например, доказать, что не существует прямой, проходящей через все три стороны треугольника.
Многочисленные комментаторы Евклида делали неоднократные попытки исправить отмеченные недочёты — было увеличено число аксиом, уточнены формулировки и доказательства[13]. Некоторые комментаторы (например, Теон Александрийский и Христофор Клавиус) при переиздании вносили свои поправки прямо в евклидовский текст. Пересмотренная и значительно дополненная версия аксиоматики, предложенная Пьером Эригоном в 1632 году, оказалась неудачной[24]. Первым крупным достижением в этом направлении стала монография «Лекции по новой геометрии» немецкого математика Морица Паша (1882)[25]. Завершением стала современная аксиоматика Гильберта для геометрии (1899 год). Она, а также различные её вариации логически полны и нигде не опираются на интуитивную очевидность[26].
"Ты должен сделать добро из зла, потому что его больше не из чего сделать." Р.П. Уоррен
Re[3]: Про формализация математических теорем и язык Coq
K>есть сияющая вершина в виде coq, в котором есть code extraction. к сожалению, он в ocaml экстрактит, и попытка написать экстрактор в f# (что меня бы устроило полностью), кажется, сдохла. ну и coq уже тяжеловат для моих слабых мозгов.
есть F*, умеет экстрактить в F#, и имеет Ocaml-овский (или F# синтаксис). я как-то игрался, довольно интересная штука, хороший и понятный туториал.
Re[4]: Про формализация математических теорем и язык Coq
K>>есть сияющая вершина в виде coq, в котором есть code extraction. к сожалению, он в ocaml экстрактит, и попытка написать экстрактор в f# (что меня бы устроило полностью), кажется, сдохла. ну и coq уже тяжеловат для моих слабых мозгов.
MH>есть F*, умеет экстрактить в F#, и имеет Ocaml-овский (или F# синтаксис). я как-то игрался, довольно интересная штука, хороший и понятный туториал.
а компилировать код экстракченый в f# получалось?
Re[5]: Про формализация математических теорем и язык Coq
Здравствуйте, Shmj, Вы писали:
S>Почему до сих пор не обязали всех математиков представлять свои доказательства в строго формальном виде, к примеру на языке Coq? Тогда сразу будет видно верно доказательство или нет.
S>Ну и второе. Кто с этим вообще сталкивался, насколько оно удобно как универсальный язык математики? Почему до сих пор не перевели доказательство Великой Теоремы на этот язык?
всем девкам под юбку не заглянешь, но к этому нужно стремиться.
также и с формализацией, потихоньку, полегоньку можно её навязать.
начать можно с того, что должен быть канонический список утверждений,
далее требовать, чтоюы к доказательству в свободной форме автор решения добавлял разметку предложений откуда они следуют.
далее формулы и системы уравнений писал в нормальном виде, тогда хоть вольфрамальфа на лету будет упрощать док-ва.
