October 1st, 2017

книги по психологии

любопытные книги по названиям (я не читал), вероятно молодым людям могут пригодиться
---
http://litvak.me/statyi

http://fit4brain.com/9067

http://litvak.me/knigi/article_post/esli-hochesh-byt-schastlivym

Первый том мы нaзвaли "Кaк узнaть и изменить свою судьбу", где объединялись все приемы рaботы нaд собой.

Второй том "Психологический вaмпиризм" посвящен был проблеме общения с одним человеком и мехaнизмaм конфликтa.

Третий том "Комaндовaть или подчиняться" дaвaл рекомендaции нa тему, кaк упрaвлять людьми без криков и нервотрепки, дa тaк, чтобы они не зaмечaли, что ими упрaвляют.
---

Гомотопическая теория типов

Оригинал взят у akuklev в По просьбе os80 пишу ещё раз об унивалентности в ЖЖ
(P.S. Кажется, я научился быстро писать. Весь нижеследующий пост написался за 15 минут за едой.)

Гомотопическая теория типов HoTT это такой фреймворк для деланья математики и одновременно язык программирования. Среди довольно обширного семейства таких систем* HoTT примечательна тем, что gets equality right. Collapse )

Гомотопическая теория типов на пальцах.

Гомотопическая теория типов на пальцах.
Могу быть сильно неправ, но расскажу на пальцах что это такое.

Как обычно, в математике все довольно просто, но математики иногда запутывают ) им и так немного платят )) должна же быть маленькая компенсация ))

===
книга
Homotopy Type Theory:
Univalent Foundations of Mathematics
https://homotopytypetheory.org/book/

Унивалентные основания математики
В. А. Воеводский
ролик на русском от автора
http://www.mathnet.ru/present4281
===

Типы это точно такие же типы данных как и у программистов
Теория типов это какието теоретизирования по вопросу какихто свойств этих типов данных

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

помните я вам в двух словах рассказывал в жж что теория категорий это такие специальные направленные графы

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

унивалентная, что это?
валентность=связь
уни= один
т.е. односвязная

далее вводится некое преобразование которое и называется односвязным, это преобразование и есть переписывание цепочки или преобразование цепочки символов разных типов

а односвязная это потому что выполняется свойство
если a=b , то f(a)=f(b)
такое f есть унивалентное или односвязное, можно сказать однозначное

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

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

итого это дает нам универсальный язык формализации и программирования
в целом и все вроде )
======

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

собственно я сказал все это к тому, что мы идем примерно правильным путем и независимым образом воспроизводим примерно такие же структуры
всё )

ps Могу быть очень сильно неправ.

Гомотопическая теория типов на пальцах.

Гомотопическая теория типов Воеводского — это оригинальная попытка взглянуть на «классические» теории типов со стороны топологии. В HoTT тип — это теперь категория с изоморфизмами, тут же подключаются гомотопии, определяющие отношения эквивалентности, и т. д. Примитивно выражаясь, мы оперируем группоидами из теории категорий (преобразованиями пространств типов друг в друга), или даже группами отображений исходного множества состояний системы объектов на целевое (отображения возможны в обе стороны).

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

Пожалуй, главный недостаток HoTT в том, что она явно провозглашает (пока) отсутствие в себе известных редукций (примитивно говоря, механизмов упрощений) со свойством Чёрча-Россера — именно из-за аксиомы унивалентности. Теорема Чёрча-Россера позволяет доказывать равенства групп/полугрупп, корректность различных теорий формальных алгебр; обычно, считают, что эта теорема задаёт свойство конфлюентности (если в процессе вычислений мы, выйдя из некоторой вершины, можем пройти в разные вершины, то в будущем обязательно сможем и сойтись снова), но корректнее сказать, что она также определяет и конечность вычислений.

И вот без этого свойства HoTT пока смотрится преимущественно теоретической, так как отбрасывается огромный пласт ранее наработанных механизмов редукций. По этой причине многое в самой HoTT приходится изобретать с нуля, и до относительно массового (как Agda или Coq) применения ей пока далеко (годы и годы).

Но конечно гениальный Воеводский эти проблемы предвидел. Он исходно замыслил HoTT не только как чистую теорию, но и сразу же как формальный язык, отлично пригодный для реализации на компьютере. Можно сказать, что математикам теперь становится существенно проще выражать различные формализации на математическом языке, аки на языке программирования. По сей день для этого используется теория множеств, и вот на замену ей предлагается существенно более высокоуровневая HoTT. По этой причине то расстояние, что Coq прошёл за 10 лет, HoTT может преодолеть гораздо быстрее.

Сделаем теперь небольшую итерацию по HoTT применительно к нашим нуждам. Пока компьютерный движок Воеводского весьма далёк от прозаических нужд IT-мэйнстрима, может быть, сама теория нам даст какие-то полезные рекомендации?

Ключевой момент HoTT — это способ установления эквивалентности между типами (под типом мы понимаем также допустимые над объектом операции). У нас есть некий набор частных преобразований типов друг в друга (например, отображение модели базы данных на модель логики вычислений), и если эти преобразования непрерывны и возможны в обе стороны, то мы можем считать типы эквивалентными.

Вот тут мы приходим к концепции identity types — сам этот набор преобразований мы считаем таким «типом идентичности»! Identity type (по сути, топологические пути) доказывает, что два типа эквивалентны. В свою очередь, эквивалентность можно задавать и для этих identity types, и т. д.

Что это нам даёт? HoTT разрешает нам определить identity type, в частности, как индуктивный (определяемый единственной рекурсивной функцией). И вот в результате мы теперь можем утверждать, что такой identity type всегда будет вычислим (хотя и не известно, как)!

Это означает, что если некоторая функция/программа реализует identity type, то она является доказанной — корректно вычислимой! Для этого нам надо «всего лишь» организовать нашу функцию так, чтобы она использовала только корректно рекурсивно реализованные внутренние «типы идентичности».
http://naufsb.ru/mathematics/m45_hott/