Как быстро выучить английский язык: эффективные методы
17.08.2016 —
Что такое "капитализм" с точки зрения теории Власти
Любопытное совпадение
schegloff — 18.08.2016
Как вы наверное помните, идея заняться математикой как языком
программирования пришла мне в голову буквально на днях, в
августе 2016. Казалось бы, остальное человечество, и входящие в его
число математики, должны были сообразить то же самое значительно
раньше, и давно уже переделать математику в 146% техническую
дисциплину. Тем более, что необходимость этого известна уже
давно:Много веков что математические доказательства, что математические построения (как в геометрии: помните, там часто достраивают всякие штуки, чтобы доказательство провести) записывали обычными человеческими словами. В 19ом веке случился кризис, стало понятно, что если доказательства записывать недостаточно строго, возможны очень тонкие ошибки, которые очень тяжело заметить.
Возникла необходимость разработать строгий формальный язык для записи утверждений и доказательств. Такой, чтобы в правильности доказательства можно было убедиться алгоритмическим образом. Говоря современным языком, чтобы доказательство можно было скормить компьютеру, а он его верифицировал.
Идеи на эту тему были уже у Декарта и Лейбница, но первая попытка сделать такой язык и такую систему принадлежит Фреге с его Begriffschrift...
Однако выяснилось, что к решению этой задачи математики приблизились лишь совсем недавно, да и то далеко не все:
...мне удалось создать унивалентный подход к формализации, который позволяет использовать программную оболочку UniMath для того, чтобы записывать те утверждения, которые мне нужны. Сейчас я могу запросто записать лемму и проверить ее доказательство, у меня есть этот язык. Точнее, язык был давно - он называется Coq, но теперь я знаю, как его использовать для решения математических задач.
- Как все же родилась UniMath?
- Ее ядро - мои Foundations и еще несколько библиотек, которые использовали “основания” в качестве базиса. Я был инициатором всего этого, потом привлек к работе нескольких людей. Сегодня в команде Unimath Development Team четыре человека. Помимо меня это Бенедикт Аренс, Даниэл Грейсон и Майкл Уоррен. Само название UniMath года полтора назад подсказал Дэн Грейсон.
- Вы же не специалист в программировании, а здесь наверняка приходилось писать коды, программы.
- Кстати, я умею писать программы. Когда-то на первом курсе мехмата я подрабатывал, преподавая программирование. Так что в этой области я себя чувствую комфортно. Но практически мне этого делать не пришлось, потому что я задействовал готовую систему Coq, которая к тому времени существовала лет 20... Она очень общая, ее можно применять для многих целей. В том числе для того, чтобы проверять логические манипуляции. Оттолкнувшись от нее, я придумал новый стиль ее использования, новый способ записывать математику.
- А вы можете сказать: разработанная мною программа уже позволила мне сделать то-то и то-то? Или вы продолжаете работать над совершенствованием системы UniMath, и это сегодня основная ваша задача?
- Я сейчас продолжаю заниматься не столько даже совершенствованием UniMath, сколько тем, чтобы убедить математиков, что способу использования компьютерной системы, который я придумал, действительно можно доверять. То есть если система говорит, что доказательство правильное, то оно действительно правильное. Это неочевидно, в этом надо людей убедить.
Так что не успел я даже собраться поизучать математику - а уже оказался впереди паровоза :)
Сохранено
|
|
</> |
Любопытное совпадение
Оставить комментарий
Популярные посты:
Предыдущие записи блогера :
17.08.2016 —
Экономика и Власть
12.08.2016 —
Все как везде
11.08.2016 —
Как Власть хакает Управление
09.08.2016 —
Вот это по-нашему!
08.08.2016 —
Отличие Управления от Власти на конкретном примере
Архив записей в блогах:
Исторически для написания иврита использовался другой алфавит абджад: оригинальный древнееврейский алфавит, ныне известный как палео-ивритский алфавит, в значительной степени ...
Originally posted by teh_nomad at Местные жители смогли защитить себя от чеченской ордыВторая смена уже была русские (из Ростовской области) и чеченские. Причем чеченцы уезжали раньше. Перед отъездом, когда уже на всё пофиг они совсем дикие были. Мы всю ночь ...
Опять старье, но я предупреждала
Каждую весну к пупсику приходит она. Аллергия. Голос опухает, перестаёт дышать нос, чешутся глаза, а вишенкой на торте поганится и без того не плюшевый характер. Налет цивилизации облетает с первой пыльцой. Словарь обогащается междометиями.
...
Веселый праздник с массовыми гуляньями, играми и забавами. День обжорства и винопития, после которого все просят прощения друг у друга. Церковный праздник, подготовка к великому посту. Языческий праздник, поклонение богу Солнца - Яриле. Проводы зимы, сжигание соломенной Маслёны на ...
Приход к власти на Ближнем Востоке исламистов, как настойчиво повторяет в своих передачах Игорь Прокопенко, – дело рук США. В принципе понятно, что одурманенный радикальным исламом народ не станет вникать в тонкости торговли нефтью. Этим займутся специально обученные люди – в меру ...
