Здравствуйте, deniok, Вы писали:
D>Совершенно не вынуждены. Если бы мне по работе необходимо было существенным образом полагаться на эту теорему, мне бы пришлось разбираться в ее доказательстве.
Что значит "существенным образом полагаться на эту теорему"? На непротиворечивость теории множеств ты полагаешься? Почему же тогда гипотезу континуума не самому проверить? Взять книжку Коэна и почитать. Может, конечно, не хватить знаний, придется лет 5-15 подучиться. Я только об этом и говорю.
D>Я принимаю во внимание тот факт, что из десятка специалистов, разбиравшихся в этом доказательстве, ни один не выдвинул возражений против него; тем не менее, полагаю, что там могут быть тонкие и неочевидные места.
Вполне разумная позиция. Я придерживаюсь той же: мнение авторитета -- это не абсолютная истина, он также может ошибиться.
D>Меня бы устроил, скажем, COQ-овский файл с формальным доказательством. Такая работа (по формальному доказательству всех известных теорем) последние десять лет тихо и спокойно идет в ряде европейских университетов (Франция, Швеция, Голландия).
Здесь не уверен, что формальное синтаксическое доказательство так уже полезно. В доказательстве важно, кроме формального выяснения истинности утверждения, еще методы, которые использовались при проведении этого доказательства. Например, кому было бы нужно доказательство гипотезы Пуанкаре, сделанное машиной? Доказательство Перельмана ценно тем, что в нем предложены новые методы, подходы. Какой смысл в тексте на полторы тысячи, в котором просто записаны переходы от одной формулы к другой?
D>Ну-ка, где это давно перешли к такой научной практике? В каком-таком научном учреждении/организации?
Вообще, в любой стране существуют т.н. реферируемые журналы. Прежде, чем теорема будет там опубликована, ее прочитает по крайней мере один специалист в данной области. Попытается проверить доказательство и не факт, что обнаружит ошибку, если таковая имеется. Когда теорема будет опубликована, то ее прочитают еще с десяток специалистов в данной области, но также не факт, что обнаружат ошибку. Неспециалисты будут эту теорему использовать и на нее ссылаться, как на доказанный факт. Конечно, при этом будут принимать во внимание, что в доказательстве может быть допущена ошибка. Это и есть отказ от греческой традиции проверять все своими руками. Какая разница, читаю я текст теоремы в реферируемом журнале или на стене пирамиды? В обоих случаях я вхожу в особое психологическое состояние, в котором имеется ощущение "знания" того или иного факта.
Здравствуйте, mefrill, Вы писали:
M>Здравствуйте, deniok, Вы писали:
D>>Совершенно не вынуждены. Если бы мне по работе необходимо было существенным образом полагаться на эту теорему, мне бы пришлось разбираться в ее доказательстве.
M>Что значит "существенным образом полагаться на эту теорему"? На непротиворечивость теории множеств ты полагаешься?
"За неимением гербовой пишем на простой" (c)
M> Почему же тогда гипотезу континуума не самому проверить? Взять книжку Коэна и почитать. Может, конечно, не хватить знаний, придется лет 5-15 подучиться. Я только об этом и говорю.
Ну а я отвечаю, что если выполнение/невыполнение континуум-гипотезы (и ее зависимость/независимость от от системы аксиом (ZFC или какой другой)) существенным образом влияет на твою работу, то да надо Коэна читать. А в плане общего образования — естественно получать знания из авторитетных источников, кто же спорит.
Мой point в том, что ссылка на авторитет плоха как универсальный методологический принцип. В отличие от предоставления доказательства (хотя бы не в виде сведения к первопринципам, а к утверждениям, которые все участники дискуссии считают верными.)
Быстрая сортировка используется часто не потому же, что Хоар наиболее авторитетный писатель алгоритмов сортировки.
Здравствуйте, Klapaucius, Вы писали:
K>>>И который язык в списке тот самый "простой, но мощный"? Вот схема, например, МЛ и смолток — именно простые, но мощные. LVV>>Паскаль по сравнению с Алголом-68. K>Паскаль по сравнению с Алголом 68, конечно, проще, но мощным, по сравнению с Алголом 68 он вовсе не является.
Как было написано, Вирт ставил две задачи: 1. создание языка для обучения (кстати, никто до него такой задачи не ставил!); 2. продемонстрировать, что компилятор может быть простым для достаточно мощного языка.
Я думаю, Вирт решил обе задачи. Паскаль получился для своего времени достаточно мощным (хотя Алгол-68 — это, конечно, ВЕСЧЬ!). Но компилятор по сравнению с компилятором Алгола-68 — это просто песня! Первый компилятор написан студентом(!) под руководством Вирта.
Хочешь быть счастливым — будь им!
Без булдырабыз!!!
Здравствуйте, mefrill, Вы писали:
M>Может и не верно, но что делать? Научные знания сложны, один человек их обнять не может. Проверить доказательство теоремы, как это делали в Древней Греции уже затратно, можно задержаться лет этак на 15. Поэтому, приходится полагаться на авторитетов. Конечно, их мнение -- не абсолютная истина, которую нельзя подвергать сомнению. Вообще, рациональный метод познания не признает абсолютных истин. На мнение авторитета полагаются ровно в той степени, в какой полагаются на свое собственное, полученное при чтении той или иной теоремы. Если доказательство сложно, то кто может поручиться, что в доказательстве не сделана ошибка, которую я пропустил? Тоже самое и с мнением авторитета: он также может ошибиться, но вероятность его ошибки намного ниже.
Что-то в твоих рассуждениях есть, но принять итоговый вывод я все же не могу. Но нет желания сейчас развернуть подробную дискуссию на эту тему
Здравствуйте, WolfHound, Вы писали:
WH>Здравствуйте, Pavel Dvorkin, Вы писали:
WH>>>Пожалуйста перечисли его достижения. PD>>http://chernykh.net/content/view/472/684/. WH>Там перечислены исключительно инженерные работы. Причем весьма примитивные. Научной новизны в них 0 целых 0 десятых. WH>От себя добавлю что он еще немного усовершенствовал синтаксис BNF. WH>На этом его достижения заканчиваются. WH>Чуть не забыл еще он автор кучи неадекватных наездов на синтаксис С и все функциональные языки разом.
WH>Да я с этим не согласен. Я считаю что его авторитет мягко говоря сильно раздут.
Имеешь право. Но все же
Есть два мнения. Одно твое. Другое вот этих
Американский Совет Магистров присвоил ему звание член-корреспондента; Компьютерное Общество Института Инженеров по электронике и радиотехнике — звание компьютерного пионера; он получил приз IBM европейской науки и техники; стал членом Швейцарской Академии Инженерии и иностранным партнером Американской Академии Инженерии, а также получил орден "Pur le merte" и премию Тьюринга. Вирт получил почетные докторские степени от многих университетов: университет Лавапь, Квебек (Канада), университет Калифорнии, Беркли, университет Йорк (Англия), университет Лине Иоганна Кеплера (Австрия), университет Новосибирска (Россия), Открытый университет Англии, университет Пре-тории (Южная Африка).
Допустим, я чего-то не понимаю (хотя если уж мое личное мнение взять — за один только Паскаль он заслужил, чтобы его имя осталось в истории). Ну а все же — эти все тоже что-то не понимали?
Почему я должен предпочесть твое мнение их мнению ? Пока аргументов я не вижу. Кроме демагогии о виртопоклонничестве и раскатывании оберона.
WH>Вот для сравнения идея http://en.wikipedia.org/wiki/Intuitionistic_type_theory но почему то я не вижу толп фанатиков размахивающих флагами с именем Per Erik Rutger Martin-Löf.
Здравствуйте, LaptevVV, Вы писали:
LVV>Как было написано, Вирт ставил две задачи: 1. создание языка для обучения (кстати, никто до него такой задачи не ставил!);
Ну конечно ставил! И не только ставил задачу, но и решал ее.LOGO появился на три года раньше Паскаля, да и то это, вероятно, не первый язык для обучения.
Конечно неправильно, когда забывают о достижениях Вирта, но приписывать ему достижения других людей тоже не следует.
LVV>2. продемонстрировать, что компилятор может быть простым для достаточно мощного языка. LVV>Я думаю, Вирт решил обе задачи. Паскаль получился для своего времени достаточно мощным (хотя Алгол-68 — это, конечно, ВЕСЧЬ!).
Получился с мощностью на уровне ревизии Алгол 60.
LVV>Но компилятор по сравнению с компилятором Алгола-68 — это просто песня! Первый компилятор написан студентом(!) под руководством Вирта.
Это вполне логично, учитывая разницу в мощности. Тем более не стоит ориентироваться на худшие примеры — алгол 68 действительно представляет головную боль для разработчика компиляторов, и этим он и прославился, в основном, хотя позже появились более выдающиеся образцы — по сравнению с ним многие языки в плане построения компилятора для них будут хорошо выглядеть.
... << RSDN@Home 1.2.0 alpha 4 rev. 1228>>
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Здравствуйте, mefrill, Вы писали:
D>>Совершенно не вынуждены. Если бы мне по работе необходимо было существенным образом полагаться на эту теорему, мне бы пришлось разбираться в ее доказательстве. M>Что значит "существенным образом полагаться на эту теорему"? На непротиворечивость теории множеств ты полагаешься? Почему же тогда гипотезу континуума не самому проверить? Взять книжку Коэна и почитать. Может, конечно, не хватить знаний, придется лет 5-15 подучиться. Я только об этом и говорю.
Формальная логика до континуум-гипотезы и неполноты по Гёделю учится за полгода в университете.
D>>Меня бы устроил, скажем, COQ-овский файл с формальным доказательством. Такая работа (по формальному доказательству всех известных теорем) последние десять лет тихо и спокойно идет в ряде европейских университетов (Франция, Швеция, Голландия). M>Здесь не уверен, что формальное синтаксическое доказательство так уже полезно.
Очень полезно.
M>В доказательстве важно, кроме формального выяснения истинности утверждения, еще методы, которые использовались при проведении этого доказательства. Например, кому было бы нужно доказательство гипотезы Пуанкаре, сделанное машиной?
Ценность в том, что COQ проверяет доказательство на корректность. Т.е. логических дыр в нём гарантированно не будет.
Ты будешь удивлён, но в ходе работ по проверке доказательств было выявлена куча мелких ошибок в большом числе очень традиционных доказательств.
M>Доказательство Перельмана ценно тем, что в нем предложены новые методы, подходы. Какой смысл в тексте на полторы тысячи, в котором просто записаны переходы от одной формулы к другой?
А кто мешает записать доказательство Перельмана в машинно-верифицируемом виде?
Скажем, доказательство Великой Теоремы Ферма было так проверено.
D>>Ну-ка, где это давно перешли к такой научной практике? В каком-таком научном учреждении/организации? M>Вообще, в любой стране существуют т.н. реферируемые журналы. Прежде, чем теорема будет там опубликована, ее прочитает по крайней мере один специалист в данной области. Попытается проверить доказательство и не факт, что обнаружит ошибку, если таковая имеется. Когда теорема будет опубликована, то ее прочитают еще с десяток специалистов в данной области, но также не факт, что обнаружат ошибку.
Вот поэтому сейчас постепенно становится традицией использовать формальные методы проверки доказательств.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Допустим, я чего-то не понимаю (хотя если уж мое личное мнение взять — за один только Паскаль он заслужил, чтобы его имя осталось в истории).
Вот пусть там и остается.
Так ведь нет же... лезет со своими примитивными поделками во все дырки.
PD>Ну а все же — эти все тоже что-то не понимали?
Поздравляю. И ты тоже свалился на размахивание авторитетом.
PD>Почему я должен предпочесть твое мнение их мнению ? Пока аргументов я не вижу. Кроме демагогии о виртопоклонничестве
Тебе еще раз Лаптева процитировать?
Так мне не сложно:
Видимо, вы совсем не умеете общаться с великими людьми...
Не вам судить о разработках мировой величины в программировании. Значит, не доросли еще до его идей. Сделайте хотя бы тысячную час того, что сделал Вирт, а потом и судить будете.
Здравствуйте, Cyberax, Вы писали:
C>Ценность в том, что COQ проверяет доказательство на корректность. Т.е. логических дыр в нём гарантированно не будет.
А существует доказательство корректности работы COQ, которое можно проверить на корректность?
K>не смотря на то, что в алгол 68 понапихали всяких ужасов, сегодня отчетливо видно, что язык этот опередил свое время и выглядит чуть ли не самым изящным и мощным статически типизированным языком своего времени.
По сравнению, скажем, с CPL мощь алгола-68 не так уж впечатляет.
K>Алгол 68, например, expression-based, а не statement-based.
Правильнее сказать "не различает операторы и выражения". Сомнительное достоинство.
K>
K># ФВП. В стат. типизированном языке. В 68-м году. В Виртовских языках ссылки на функцию
K> еще долго не появятся. #
K>PROC map = (PROC(INT)INT f, LIST xs)LIST:
K> (xs IS NIL | NIL | cons(f(head(xs)), map(f,tail(xs))));
K>
А зачем ссылки на функцию?
function map = (f:function(integer):integer; xs:LIST ):LIST;
begin
if xs = nil then map := nil else map := cons(f(head(xs)), map(f,tail(xs)));
end;
Здравствуйте, Трурль, Вы писали:
C>>Ценность в том, что COQ проверяет доказательство на корректность. Т.е. логических дыр в нём гарантированно не будет. Т>А существует доказательство корректности работы COQ, которое можно проверить на корректность?
Пока нет. Но работа над этим идёт.
Это код на паскале ISO 7185 82-го года (с ошибками). На первых версиях паскаля так писать было нельзя.
Очевидно, было принято решение, что более-менее нормальный функциональный тип это лишняя сущность, которую нужно отсечь. Минимализм и все такое. Можно было писать так:
function map(function f:integer; xs:LIST ):LIST;
begin
if xs = nil then map := nil else map := cons(f(head(xs)), map(f,tail(xs)));
end;
Кол-во и тип параметров не указываются и компилятором не проверяются — если что, в рантайме будет сюрприз, о чем Энди Таненбаум негодовал еще в 77-ом году в своем сравнении Паскаля и Алгола 68
Такие вещи, впрочем, волнуют только теоретиков, ведь в основных имплементациях (P-машины, UCSD Pascal, Apple Pascal) никаких проблем с функциональными параметрами не было — потому, что самих параметров не было ни в каком виде даже еще в 80 годы.
... << RSDN@Home 1.2.0 alpha 4 rev. 1228>>
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Здравствуйте, Klapaucius, Вы писали:
LVV>>Как было написано, Вирт ставил две задачи: 1. создание языка для обучения (кстати, никто до него такой задачи не ставил!); K>Ну конечно ставил! И не только ставил задачу, но и решал ее.LOGO появился на три года раньше Паскаля, да и то это, вероятно, не первый язык для обучения. K>Конечно неправильно, когда забывают о достижениях Вирта, но приписывать ему достижения других людей тоже не следует.
Ну,тогда можно сказать, что в Европе Вирт все равно был первый. Или можно сказать, что первый императивный язык для обучения. LVV>>2. продемонстрировать, что компилятор может быть простым для достаточно мощного языка. LVV>>Я думаю, Вирт решил обе задачи. Паскаль получился для своего времени достаточно мощным (хотя Алгол-68 — это, конечно, ВЕСЧЬ!). K>Получился с мощностью на уровне ревизии Алгол 60.
Да, скорее всего, именно это он и хотел сделать. LVV>>Но компилятор по сравнению с компилятором Алгола-68 — это просто песня! Первый компилятор написан студентом(!) под руководством Вирта. K>Это вполне логично, учитывая разницу в мощности. Тем более не стоит ориентироваться на худшие примеры — алгол 68 действительно представляет головную боль для разработчика компиляторов, и этим он и прославился, в основном, хотя позже появились более выдающиеся образцы — по сравнению с ним многие языки в плане построения компилятора для них будут хорошо выглядеть.
Да, конечно.
Но надо попробовать реализовать Си силами студентов...
Хочешь быть счастливым — будь им!
Без булдырабыз!!!
Здравствуйте, WolfHound, Вы писали:
LVV>>Покажите ваши не примитивные достижения, за которые вам вручили премию Тьюринга! WH>Перевожу: Да ты пес смердящий! Да как ты посмел гавкать на нашего обожаемого гуру!?
Андрей! Ну не следует приписывать мне мыслей, которые высказываете вы!
Я не видел ваших достижений. А достижения Вирта, Хоора, Страуструпа, Дейкстры — известны всем. WH>Вы уже не в первый раз скатываетесь на антинаучные приемы ведения дискуссии.
У нас не научный спор. Я всего лишь заступился за авторитет Вирта. а меня тут начали обвинять в виртопоклонничестве.
Давайте тогда откажемся от ВСЕХ достижений уважаемых людей и каждый раз будем начинать все сначала. LVV>>Ну, на оберонском форуме можно встретить аналогичные обвинения в Страусопоклонничестве. Или в Биллипоклонничестве... WH>Я не подвержен поклоннечеству.
Ну и прекрасно! WH>Вы хотите сказать что нельзя перейти на уровень технических аргументов которыми мы в свое время раскатали приверженцев оберонов?
Еще раз: я возмутился высказыванием пацана о Вирте.
И не собирался обсуждать технические достоинства Оберона и всего остального. WH>В прочем история опять повторяется. Как тогда так и сейчас нет ничего кроме визга и апелляций к "авторитетам".
Вирт — авторитет. А вот вы — еще пока нет. LVV>>Как не видать толп фанатиков, размахивающих флагами Замулина, Клещева, Хоара и др. WH>Вот именно. WH>А вот толпы виртопоклонников очевидны.
Как и поклонников Билла, и Страуструпа.
Хочешь быть счастливым — будь им!
Без булдырабыз!!!
Здравствуйте, LaptevVV, Вы писали:
LVV>Андрей! Ну не следует приписывать мне мыслей, которые высказываете вы!
Что вы. Я просто перевожу с "вежливого" на понятный.
LVV>Я не видел ваших достижений. А достижения Вирта, Хоора, Страуструпа, Дейкстры — известны всем.
Еще авторитеты появились... скоро тут целая армия будет.
WH>>Вы уже не в первый раз скатываетесь на антинаучные приемы ведения дискуссии. LVV>У нас не научный спор.
Спор идет либо по научным правилам либо превращается в ругонь базарных бабок.
Третьего не дано.
LVV>Я всего лишь заступился за авторитет Вирта. а меня тут начали обвинять в виртопоклонничестве.
А как еще можно интерпретировать совершенно неадекватное возмущение?
LVV>Давайте тогда откажемся от ВСЕХ достижений уважаемых людей и каждый раз будем начинать все сначала.
Пожалуйста цитату где я предлагаю отказаться от достижений.
Единственное о чем я говорю в этой теме это то что на мой взгляд значимость достижений конкретного человека сильно преувеличена.
LVV>Еще раз: я возмутился высказыванием пацана о Вирте.
И что же вас там так сильно задело?
Ну не понравился человеку Вирт. Бывает.
Книга Вирта ему тоже не понравилась. Тоже бывает.
Что такого то?
Кстати выделенное это опять принижение оппонента.
LVV>И не собирался обсуждать технические достоинства Оберона и всего остального.
Кто бы сомневался. Ибо в очереной раз выяснится что нет там никаких технических достоинств.
WH>>В прочем история опять повторяется. Как тогда так и сейчас нет ничего кроме визга и апелляций к "авторитетам". LVV>Вирт — авторитет. А вот вы — еще пока нет.
И снова давление на оппонента авторитетом.
Это уровень гопоты и звучит примерно так: Да я Николу Швецарскогого знаю, а ты ваще кто такой?!
LVV>Как и поклонников Билла, и Страуструпа.
Да мне плевать кто каких авторитетов знает.
В научной дискуссии все авторитеты идут лесом.
Хотя если вы предпочитаете ругонь базарных бабок то боюсь вам уже ничто не поможет.
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, WolfHound, Вы писали:
LVV>>У нас не научный спор. WH>Спор идет либо по научным правилам либо превращается в ругонь базарных бабок. WH>Третьего не дано. WH>В научной дискуссии все авторитеты идут лесом.
LVV>>У нас не научный спор.
WH>Хотя если вы предпочитаете ругонь базарных бабок то боюсь вам уже ничто не поможет.
Да ладно...
Сравнить можно только на практике.
Взять одну задачу и сделать на разных платфолрмах. А потом описать выводы.
К концу года, если успею доделать — отпишу.
Хочешь быть счастливым — будь им!
Без булдырабыз!!!
Здравствуйте, WolfHound, Вы писали:
PD>>Допустим, я чего-то не понимаю (хотя если уж мое личное мнение взять — за один только Паскаль он заслужил, чтобы его имя осталось в истории). WH>Вот пусть там и остается. WH>Так ведь нет же... лезет со своими примитивными поделками во все дырки.
Стоп, стоп, стоп. Вот тут уже мое отношение иное. Я вовсе не утверждаю, что сейчас он вполне соответствует текущему состоянию дел. И если бы вопрос был поставлен так — я бы, пожалуй, согласился с тобой — он действительно отстал. ИМХО. Но это не основание, чтобы отвергать его роль в становлении ИТ. Ньютон тоже вряд ли смог принять участие в дискуссиях о квантовой механике, окажись он чудом в 1920-х годах, но это не основание, чтобы принижать его роль.
WH>Поздравляю. И ты тоже свалился на размахивание авторитетом.
Да никуда я не свалился.
PD>>Почему я должен предпочесть твое мнение их мнению ? Пока аргументов я не вижу. Кроме демагогии о виртопоклонничестве WH>Тебе еще раз Лаптева процитировать?
Здравствуйте. Я тебе задал конкретный вопрос, а ты вместо цитируешь Лаптева. Я хочу твой ответ на этот вопрос получить. Вопрос выделен выше
WH>И это тоже констатация факта... просто пересказывать все проблемы оберона в нацатый раз мне лень. Если интересно можешь поискать.
Вообще-то последние два примера неубедительны. Я о нем ничего не знаю, поэтому поиск могу вести только по имени.
PD>>Так что его просто мало кто знает. Что такое Science Citation Index (SCI) — знаешь ? WH>Поправка: Ты не знаешь.
Что за чепуха ? Что я не знаю ? Что такое SCI ? Уж поверь, знаю — как-никак, а в прошлом я научный сотрудник.
Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Здравствуйте. Я тебе задал конкретный вопрос, а ты вместо цитируешь Лаптева. Я хочу твой ответ на этот вопрос получить. Вопрос выделен выше
Да предпочитай ты чего хочешь мне то что?
PD>Нет, абсолютно неинтересно. Здесь я с тобой вполне согласен — это не есть мэйнстрим.
Причем тут вообще мэйнстрим?
Мэйнстрим ужасен и внутри и снаружи.
Особенно твой любимый С++.
PD>Вообще-то последние два примера неубедительны. Я о нем ничего не знаю, поэтому поиск могу вести только по имени.
Человеку преподающему в университете программирование должно быть стыдно не знать основы наиболее перспективного направления теории вычислительной техники.
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
