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

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]pzz
2007-06-22 05:09 (ссылка)
Java и C# конечно лучше. В них хоть строки не надо конструировать руками из подручных запчастей.

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

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


[info]yushi
2007-06-22 10:32 (ссылка)
В них хоть строки не надо конструировать руками из подручных запчастей.

Эхм. Вы char* имеете в виду? Но, вообще-то, класс string входит в стандарт ISO C++, это типа часть языка (как и STL). Хотя, конечно, избавление от рудиментов C (типа тех же указателей или функций-неметодов), несомненно, пошло Жабе и C# на пользу.

Виртовский Паскаль сконструирован с довольно глупыми ошибками.

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

Хотя что касается меня, то мне возвращать указатели на функции хочется регулярно…

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


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