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

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

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

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

Сообщества

Настроить S2

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



Пишет kouzdra ([info]kouzdra)
@ 2007-07-02 17:26:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Про основания математики
Почитал дискуссии и то, что там дальше по ссылкам.
Зрелище грустное. Сначала дисклеймер - я не математик, а компьютерщик, тем не менее - скорее всего в subj разбираюсь лучше чем все прочие участники данной темы. Дело в том, что у очень многих, кто с математикой дело имеет, рано или поздно появляется зуд в жопе про "философию математики", и так уж вышло, что я не поленился в этом разобраться. Там вполне можно разобраться.

Что я хочу сказать по поводу:

1) Математика imho нужна для получения практических результатов. Если из теории нет и не предвидится никаких выходов в практику (прямых или там через десять уровней косвенности) - это род интеллектуального онанизма. Понятно, что к подобному онанизму как и в любой серьезной науке надо относится терпимо - а вдруг чего-нибудь когда-нибудь выйдет, но цель она все-таки внешняя. Не обязательно суперструны, конечно, Миша тут необоснованно сужает тему. Просто в суперструнах математика сложная, поэтому ее любят, а в том же функциональном программировании - простая, там другая проблема - не вполне понятно как и куда именно там дальше двигаться. Хотя ясно, что в принципе вроде есть куда.

С другой стороны - что до компутерщины - двигаться там, по крайней мере в России, imho некому, просто потому что afaik даже той математике, которая на эту тему уже есть ни в ЛГУ ни в МГУ практически никого не учат. То есть - компутерщиков как-то учат, если повезет - но из них математики понятно какие.

2) Конструктивная математика давно и прочно является разновидностью духовного онанизма. Практических выходов из нее нет и не предвидится. Они имела содержательный смысл в 30-е - когда со всем этим разбирались и было неясно, что вообще из этого выйдет.

3) Основания математики - это проблематика 20-30 годов, к 50-60 гг ее предмет практически исчерпан (по крайней мере на современном уровне) и вместо того, чтобы заниматься пустопорожним философствованием надо просто разобраться в том, что тогда сделано. Или забить. Вероятно за этим матлогику было бы полезно преподавать в обязательном курсе. Чтобы фигней не страдали.

Философские рассуждения Пуанкаре, Гильберта etc значение имеют скорее историческое - потому после той же теоремы Геделя и проч. представления на эту тему естетсвенно сильно поменялись.

4) Какие-то выходы в компутерщину из всего этого есть - но, как обычно, они имеют мало отношения к философии "конструктивной математике". Зато имеют ко всяким извращенным логикам, вопросам их разрешимости и непротиворечивости и к категорной логике, которую товарищи с МГУ полагают "полной фигней". Математика там не бог весть какая - но все-таки.

Ну всякая традиционная прикладуха с теорией информации и т.п. тоже естественно.


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


[info]kouzdra
2007-07-02 22:24 (ссылка)
Это бессмысленный повтор: я тоже полагаю, что применяется или применима, но так как дело недостаточно поставлено (по крайней мере в известных нам случаях), оперировать мы можем слишком конкретными вопросами (а потому можно спорить в духе: "Ан нет! Применяют другое!") сколь угодно "глубоко"

Мне зато это хорошо известно. Без приличного знания базовой логики (ну то есть - именно всяких разных логических исчисленей - позитивной логики, интуиционалской etc), хотя бы минимального (а желательно - более основательного) бэкграунда в теории категорий и знания лямбда-исчисления (там все не так просто, как кажется) в оьласти языков программирования сейчас делать нечего.

Уже лет 15 как. Это мэйнстрим и просто язык, на котором все сколько-нибудь содержательные результаты в обасли связанной с языками программирования формулируются. То, что у нас этим никто не занимается и знать даже не хочет - это практический факт.

Ситуация очень похожа на ту, о которой говорит Вербицкий применительно к своей колокольне. Дело доходит до смешного - что какие-то совсем базовыве сведения мне самому приходилось рассказывать - без этого функциональное программирование сколько-нибудь осмысленно читать невозможно. И статьи читать невозможно. Ну и еще один из основных источников идей.

Недаром ликбезы вроде "Basic category theory for computer scientists" пачками в сети валяются.

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

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


[info]polytheme
2007-07-03 12:21 (ссылка)
в околовербицкой науке их использовали для доказательства гипотез Вейля, очень хороших :) проблема на самом деле в том (возвращаясь к тексту поста), что считать практическим результатом. математика сама по себе - это такая огромная местность, и у нее у самой есть критерии "практичности". ну, грубо говоря, когда человек придумывает протирку для пластиковых окон, это не очень практично в масштабе, а когда придумывает новый принцип летательного аппарата, практично, да. и в этом смысле результат Матиясевича (который, собственно, подытожил работу Робинсон) очень хороший, да, но совершенно не практичный, потому что в механическую разрешимость диофантовых уравнений никто давно не верил; а доказательство гипотез Вейля практично очень - собственно, топосы для их доказательства и придумали (Ловера, если я не ошибаюсь, довольно сильно стимулировало ознакомление с топологиями Гротендика).

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


[info]ppkk
2007-07-03 13:39 (ссылка)
Вообще-то это скорее дооколовербицкая наука: в 1974-ом году их доказали полностью (в результате разработки сложных теорий, которые качественно такими до сих пор и остались в основном).

Эндрю Вайлс и компания имел отношение к другой "гипотезе Вейля", которую обычно называют "гипотеза Таниямы-Шимуры", а о числах Тамагавы доказал что-то Черноусов. Я это сейчас в википедии прочитал, хотя в принципе об этом (всех трёх) слыхал в связи с теорией чисел, естественно.

Что из этого "околовербицкое"?

О практичности: разве в связанной с этим математикой (в частности: алгебраической теорией чисел) не действует замечательный принцип развития по пути наименьшего сопротивления (исследовать не то, что может быть осмысленным, а то, что получается [следя за достаточно высоким уровнем сложности, естественно, чтобы оставаться элитой])? А ещё принципом инерции: если занимался этим 20 лет и стало ясно, что больших успехов не будет, то надо продолжать копать, ибо в этом уже крутой специалист?

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


[info]polytheme
2007-07-03 17:07 (ссылка)
я имел в виду серию гипотез о дзета-функциях кривых в характеристике p. они изначально были "доказаны" Вейлем в предположении о существовании достаточно хорошей теории когомологий в характеристике p (которой тогда не было).
вот их как раз и доказали при помощи этальных когомологий, придуманных Гротендиком; они строятся на сайте Гротендика, и этот сайт и есть первый исторический пример топоса.

а где я писал про Уайлза ? Гипотеза Таниямы-Вейля - это действительно совершенно отдельная наука, из теории эллиптических кривых; полагаю, что там ни этальные когомологии, ни топосы никак не фигурируют.

я бы скорее говорил о критерии "интересности" : конечно, одному человеку интересно одно, а другому - другое. но периодически вспыхивают в математике вещи, которые сильно удивляют. так было с конструкцией непрерывных дробей и уравнением Пелля (что вылилось в теорию диофантовых приближений), с квадратичным законом взаимности (про который Гаусс настолько хотел выяснить, откуда он взялся, что придумал пару десятков различных доказательств; сей закон и его "продолжения" были одной из главных действующих сил, создавших современную теорию алгебраических чисел - другими, видимо, были теория Галуа, теорема Дирихле о простых в прогрессии (тут уход в аналитику; нормального "неаналитического" доказательства вроде бы нет до сих пор (Сельберг не считается), хотя есть удивительно простое для an+1 - но в ТАЧ этот мотив весьма важен, оттуда растет теорема Чеботарева о плотности), наплыв Куммера с теорией дивизоров и т.д.

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

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

потом также было с mirror symmetry в алгебраической геометрии - из физики, кажется, был взят только вычислительный результат и "интуитивное" оправдание.

т.е. вначале идет удивление - откуда берется такая простая штука ? ну, иногда она оказывается очень сложной технически, а внутри себя не особенно интересной - как было с теоремой Ферма (в отличие от гипотезы Т.-В., которая как раз интересна "внутри", но насчет этого "внутри", насколько я понимаю, до ясности еще очень далеко). а иногда оказывается, что там внутри совсем простая, но совершенно неочевидная машинерия

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


[info]ppkk
2007-07-03 17:39 (ссылка)
Ну да, эти "гипотезы" доказаны были в 1974-м.

Этальные когомологии — замечательно, но великого с помощью них с тех пор не достигали, по-моему. Как тест великости: в википедии ссылки после 1974-го года только на учебники по сути. Не на то, что кто-то ещё что-то доказал. Некоторые особо умные люди считают их полезными, изучают их, не спорю.

К теореме Дирихле Зельберг сложный не нужен: я лично рассказывал школьникам её доказательство этим самым методом, это не запредельно (хотя и сложно). Один точно понял (всего было несколько, занятия были не только про это).
Сложно доказывать теорему Чебышёва методом Зельберга, но сложно лишь доказать существование предела и равенство единице, а, например, оценить сверху-снизу довольно точно его методом довольно просто (если мы говорим о сложности, а не о перспективах математики 21-го века: этальные когомологии — тоже не хухры-мухры).

Мотивные когомологии я тоже не знаю, но их очень любят некоторые иностранцы. Есть ощущуние, что это по инерции… Всё-таки целыми институтами изучать Воеводского явно нецелесообразно (что же они понадоказывали с помощью неё?!).

Меня отрывают от компьютера, возможно напишу ещё по сути.

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


[info]polytheme
2007-07-03 18:00 (ссылка)
по-моему у математики нет цели доказать что-то "великое"; это как-то глупо.
хотя у математика, конечно, такая цель ввиду престижа может быть.
как я уже говорил, периодически возникают удивительные совпадения, за которыми часто скрываются потайные связи. этальные когомологии (а есть еще кристальные :) были действительно просто важным шагом (вроде изобретения мнимых чисел), одновременно Гротендик придумал, как определять фундаментальную группу в характеристике p, но, полагаю, в теории мотивов ЭК вполне себе фигурируют. вся эта махина существует ввиду одной большой сверхзадачи : классификация алгебраических многообразий. эту задачу решить, конечно, нельзя полностью. но возникающие подходы очень интересны.

да, Чебышевские оценки вроде бы вполне элементарны, если я не ошибаюсь - тут еще нужно понимать, что слово "элементарный" двусмысленно - "просто" либо "не использует ТФКП". только я не понял, вы рассказывали Дирихле через L-ряды (это просто, но неэлементарно), или по Сельбергу (это элементарно, но совсем не просто).

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


[info]ppkk
2007-07-03 19:49 (ссылка)
У нас их называли "кристаллические":)

По Зельбергу. По книжке рассказывал, Rose, "A Course in Number Theory" http://www.amazon.com/Course-Number-Theory-Science-Publications/dp/0198523769/ref=sr_1_31/103-7116757-3909443?ie=UTF8&s=books&qid=1183477538&sr=1-31. Книжку дал (года три назад, так и не забирал) логик (чуть за тридцать), который с живым Коэном говорил:)

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

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


[info]ppkk
2007-07-03 13:10 (ссылка)
Схемы к топосам имеют прямое отношение, в алгебраической геометрии вовсю используются. Я их толком не изучал

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

Наверное, всё-таки несколько разные люди должны заниматься разработкой алгоритмов, математику потребляя, и собственно программировать. А третьи — организацией на разных уровнях (имея, видимо, опыт первых и/или вторых).

Сейчас посмотрю что-нибудь про "B c th f c sc".

Так зачем реально нужно функциональное программирование (я честно не в курсе, спрашиваю в третий раз)?

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


[info]polytheme
2007-07-03 17:10 (ссылка)
функциональное программирование нужно за тем же, зачем и любые другие технологии - чтобы программирование было проще, а программы короче и правильнее. грубо говоря, это способ записывать алгоритмы так, что вероятность ошибки становится гораздо меньше

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


[info]ppkk
2007-07-03 19:27 (ссылка)
Не уверен. Всё-таки во многих случаях переиспользование переменных упрощает алгоритмы и делает меньше вероятность ошибки. (Здесь и в другом комментарии я исхожу из своего убогого знания основ функционального программирования: главным считаю однократное присвоение значения "переменной". А конструкции типа "i = 1 + old i" считаю погаными. Также я полагал, что дело может быть в распараллеливании и оптимизации, но почти любую программу можно привести к "функциональной" на стадии "прекомпиляции" [кроме слишком системной].)

Проще говоря: можно подробнее?

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


[info]polytheme
2007-07-03 19:36 (ссылка)
ну то есть вопрос был с секретом, да ? на самом деле вы считаете, что fp - это очередная бессмысленная заумь, не имеющая практического применения :) (поправьте, если я ошибаюсь)

давайте попробуем так (конкретно) : вы предлагаете конкретный алгоритм, я его записываю в функциональном виде :) а то так это будет махание понтами ненужное

в описываемой вами ситуации есть два момента - во-первых, в функциональных языках переменных нет вообще (там концепция другая), во-вторых, есть конструкция let

let a = f in (a a x); этот let только кажется введением переменной (я некоторое время и думал, что это происходит), на самом деле это просто синтаксическая конструкция.

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


[info]ppkk
2007-07-03 19:43 (ссылка)
Скорее я просто не в теме.

По сути мне кажется, что оптимизации single static use/single static assignment полностью отделяют реального программиста от функционального программирования, если ему неинтересно, либо дают ему возможность делать то же самое в "обычных" языках.

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

Математику я изучал долго, а программированием занимаюсь меньше полутора лет. Я даже Яву не знаю:)

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


[info]kouzdra
2007-07-03 20:02 (ссылка)
В Яве, кстати, generic'и прямиком из FP. Я просто знаю, кто их туда засовывал. Если коротко - то отсуствие переменных в принципе не главное, что в FP есть. Там вообще философствования всякой в отличие от ООП очень мало.

Реально FP (в современном смысле) просто набор некоторых фич, которые возникли и живут вокруг функциональных языков. Опять же - в принципе - это все активно развивалось где-то с конца 70-х до первой половины 90-х. Сейчас там скорее застой, зато быстро идет процесс миграции всего этого в промышленное программирование. Как обычно бывает - криво донельзя.

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

Во-вторых - такая забавная вещь, как автоматическое определение типов - в ML типы писать не надо практически нигде, в Haskell - довольно мало где надо. Помимо того, что это удобно, есть такой довольно странный побочный эффект - программа с логическми ошибками как правильно не проходит контроль типов.

Некоторое количество просто удобных вещей - например описание типа для бинарного дерева:
type 'a tree = Leaf of 'a | Node of 'a tree * 'a tree
И там допустим суммирование целочисленного дерева:
let rec sum = function Leaf n -> n | Tree (l, r) -> sum a + sum b

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

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

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

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

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


[info]polytheme
2007-07-04 13:19 (ссылка)
насчет отсутствия декларации типов, на мой взгляд, ситуация неоднозначная.
я уже на эти грабли наступил, когда читал исходники camlp4.
иногда совершенно непонятно, какого рода входные параметры
принимает функция - потому что она сама что-то вызывает, и нужно долго
лазать по коду.
с другой стороны, можно сгенерировать по исходнику полный заголовочный
файл, и смотреть прототипы там (если я не ошибаюсь).
а вообще OCaml очень сильно не хватает современной IDE. с учетом
его собственных фич - Cameleon слишком слабенький (и собирать его
тоже морока).

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


[info]dmitri83
2007-07-04 15:40 (ссылка)
в добаление к тому, что уже сказали: для программ на функциональных языках проще (формально) доказывать их корректность.

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


[info]kouzdra
2007-07-03 17:20 (ссылка)
Университет все-таки по идее должен давать знания, позволяющие заниматься не только прикладным программированием, но исследованиями в профильной области. Или как минимум, такие исследования понимать. Тем от ВТУЗа и отличается.

Так что FP надо учить хотя бы потому, что сейчас это основное направление развития языков программирования. А нужно оно затем, просто что единственное сейчас содержательное направление развития языков. И да - они становятся и проще и мощнее.

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


[info]ppkk
2007-07-03 19:21 (ссылка)
Согласен: для простого кодирования даже высшее образование не очень нужно.

А можно подробнее? Чем недостаточно просто в компиляторах предусмотреть оптимизации SSA/SSU?

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


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