deep-econom (deep_econom) wrote,
deep-econom
deep_econom

Category:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

ps Могу быть очень сильно неправ.
Tags: искин, понимание
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic
  • 35 comments