Топология, алгебра, логика и программирование

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

Общая Топология 515.12

Считаю, что теорию категорий нужно сразу преподавать как продолжение топологии при строительстве топоса. По УДК книги по топосам так и классифицируются, как книги по общей топологии. Причина этому то, что топос содержит информацию о топологи (система открытых и закрытых множеств), которая зашита либо в пулбеке классификатора (топос Ловера-Тернье), либо в покрытиях сайта, на котором создается предпучек (топос Гротендика).

Предварительные исследования по топологии. И.Листинг. 1932. УДК 515.12
Начальний курс топологии. Геометрические главы В.Рохлин, Д.Фукс. 1977. УДК 515.12
Топология. Том 1. К.Куратовский. 1969. УДК 515.12
Топология. Том 2. К.Куратовский. 1969. УДК 515.12
Основы комбинаторной топологии Л.Понтрягин. 1947. УДК 515.12
Основы общей топологии в задачах и упражнениях.
А.Архангельский, В.Пономарев. 1974. УДК 515.12
Общая топология Дж.Келли. 1981. УДК 515.12
Общая топология Р.Александрян, Э.Мирзаханян. 1979. УДК 515.12
Общая топология. Р.Энгелькинг. 1986. УДК 515.12
Общая топология. Основные конструкции. В.Федорчук, В.Филлипов. 1988. УДК 515.12
Теория шейпов. К.Борсук. 1986. УДК 515.12 + 515.14
Теория ретрактов. К.Борсук. 1971. УДК 515.12 + 515.14
Введение в кусочно-линейную топологию. К.Рурк, Б.Сандерсон. 1974. УДК 515.164
Мемуар о компактных топологических пространствах.
П.Александров, П.Урысон. 1971. УДК 515.1
Книжка с картинками по топологии Дж.Френсис. 1991. УДК 515.1
Россыпи головоломок. С.Барр. 1978. УДК 51
Теория топосов. П.Джонстон. 1986. УДК 515.12
Топосы. Категорный анализ логики. Р.Голдблатт. 1986. УДК 515.12
Topology and Groupoids. R.Brown. 2006. УДК 515.12

Алгебра 512

Французская математика — топчик. Двухтомник Шварца по анализу (517) и 21-томник Бурбаки по различным разделам математики: алгебре (512), топология (515.12), анализе (517), дифференциальной геометрии (519.4) в непринужденной форме раскрывают всю историю математики вместе с комментариями в абстрактном и последовательно-академическом французском стиле. Думаю, что все математики с удачной судьбой учили матанализ по Шварцу, а алгебру по Бурбаки. Да и не только математика, теоретическая информатика и ее продукты в виде OCaml, Coq, работы Кокана, его учеников — все это очень приятные вещи (Coq только большой слишком, идея с развитой макросистемой поверх компактного ядра на фактортипах в Lean гораздо изящнее). Если вы соберётесь формализировать математику с помощью компьютера, то эти "сводки резульатов" все ещё остаются актуальны. Изданее пережило несколько редакций, но ни разу тираж не был больше 20,000. Что-то из этого принадлежит перу Гротендика.

Основы теории групп. М.Каргаполов, Ю.Мерзляков. 1982. УДК 512.8
Теория групп. М.Холл. 1962. УДК 512.54
Теория групп. А.Курош. 1967. УДК 512.54
Теория Галуа. М.Постников. 1963. УДК 517.1
Теорія Галуа. Е.Артін. 1963. УДК 517
Группы автоморфизмов алгебраических систем. Б.Плоткин. 1966. УДК 512.80
Теория представлений конечных групп. У.Фейт. 1990. УДК 512.542
Элементы теории представлений. А.Кириллов. 1978. УДК 517.5
Когомологии групп. К.Браун. 1982. УДК 512.54
Алгебра. С.Ленг. 1968. УДК 512
Конечные простые группы. Введение в их классификацию.
Д.Горенстейн. 1990. УДК 512.542
Группы и геометрический анализ.
С.Хелгасон. 1987. УДК 512.81
Элементы математики. Очерки по истории математики. Н.Бурбаки. 1963.
Элементы математики. Глава 1. Теория множеств. Н.Бурбаки. 1965. УДК 512
Элементы математики. Глава 2. Алгебра. Часть 1. Алгебраические структуры. Линейная и полилинейная алгебры.
Н.Бурбаки. 1962. УДК 512
Элементы математики. Глава 2. Алгебра. Часть 2. Алгебра. Многочлены и поля. Упорядоченные группы.
Н.Бурбаки. 1965. УДК 512.8
Элементы математики. Глава 2. Алгебра. Часть 3. Модули. Кольца. Формы.
Н.Бурбаки. 1965. УДК 512.8
Элементы математики. Глава 3. Общая топология. Часть 1. Основные структуры.
Н.Бурбаки. 1968. УДК 515.12
Элементы математики. Глава 3. Общая топология. Часть 2. Топологические группы. Числа и связанные с ними группы пространства.
Н.Бурбаки. 1969. УДК 515.12
Элементы математики. Глава 3. Общая топология. Часть 3. Использование вещественных чисел в общей топологии. Функциональные пространства. Сводка результатов. Словарь.
Н.Бурбаки. 1975. УДК 515.12
Элементы математики. Глава 4. Функции действительного переменного.
Н.Бурбаки. 1965. УДК 517.51
Элементы математики. Глава 5. Топологические векторные пространства.
Н.Бурбаки. 1959. УДК 517
Элементы математики. Глава 6. Интегрирование. Часть 1. Интегрирование мер.
Н.Бурбаки. 1977. УДК 517.397
Элементы математики. Глава 6. Интегрирование. Часть 2. Векторное интегрирование. Мера Хаара. Свертка предствалений.
Н.Бурбаки. 1977. УДК 517.397
Элементы математики. Глава 6. Интегрирование. Часть 3. Меры на локально-компактных пространствах. Продолжение меры. Интегрирование мер. Меры на отделимых пространствах.
Н.Бурбаки. 1977. УДК 517
Элементы математики. Глава 7. Комутативная алгебра.
Н.Бурбаки. 1971. УДК 512
Элементы математики. Глава 8. Группы и алгебры Ли. Часть 1. Алгебры Ли. Свободные алгебры Ли. Группы Ли.
Н.Бурбаки. 1976. УДК 512
Элементы математики. Глава 8. Группы и алгебры Ли. Часть 2. Группы Кокстера и система Титса. Группы порожденные отражениями. Системы корней.
Н.Бурбаки. 1972. УДК 512
Элементы математики. Глава 8. Группы и алгебры Ли. Часть 3. Подалгебра Картана, регулярные элементы. Расщепляемые полупростые алгебры Ли.
Н.Бурбаки. 1978. УДК 512
Элементы математики. Глава 8. Группы и алгебры Ли. Часть 4. Компактные вещественные группы Ли.
Н.Бурбаки. 1986. УДК 512.81
Элементы математики. Глава 9. Спектральная теория.
Н.Бурбаки. 1972. УДК 512.8
Элементы математики. Глава 10. Гомологическая алгебра.
Н.Бурбаки. 1987. УДК 512.8
Элементы математики. Глава 11. Дифференцируемые и аналитические многообразия. Сводка результатов.
Н.Бурбаки. 1972. УДК 519.4

Логика и основания математики 510

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

Введение в метаматематику. С.Клини. 1957. УДК 510
Математическая логика. С.Клини. 1973. УДК 510
Рекурсивные функции. Р.Петер. 1954. УДК 510
Введение в математическую логику. Том 1. А.Чёрч. 1960. УДК 510
Основания математической логики. Х.Карри. 1969 УДК 510
Математическая логика и автоматическое доказательство теорем.
Ч.Чень, Р.Ли. 1973. УДК 510
Основы теоретической логики. Д.Гильберт, В.Аккерман. 2009. УДК 510
Интуиционизм. А.Гейтинг. 2010. УДК 510
Очерки по конструктивной математике. П.Мартин-Лёф. 2075. УДК 510.25
Foundation of Constructive Analysis. E.Bishop. 1967. УДК 517 + 510.25
Теория моделей. Г.Кейслер, Ч.Чэн. 1977. УДК 510
Теория формальных систем. Р.Смальян. 1981. УДК 510
Homotopy Type Theory. V.Voevodsky et al. 2010. УДК 510
Modal Homotopy Type Theory. D.Corfield. 2020. УДК 510

Этого вполне достаточно для восхождения по лестнице HoTT — еще одной последовательности из работ, которая является основой современного computer science или теоретической информатики, нашедшей отображение в математических функциональных языках программирования. Провереный, надежный, долгий и понятный путь.

Дальше идут те темы, которые являются ландшафтом атаки для HoTT и ее модальной версии, т.е. алгебраическая топология и дифференциальная геометрия.

Программирование 004

Никакого смысла хранить книги по программированию нет, так как вещи в книгах устаревают быстрее чем ты пытаешься их попробовать. Список физически сохраненных сформировался сугубо по сентиментальными принчинам. По PL/1 у меня была курсовая, "Книгу дракона" я использовал на двух проектах, некоторые книги прилипли еще со школы и т.д. Я предупреждаю --- это полный, аутдейтнутый, треш! Нет ни одного даже букинистического издания, но книги не полная чушь, как минимум приложение к компьютерной археологии.

Теория синтаксического анализа, перевода и компиляции. Том 1. Синтаксический анализ А.Ахо, Дж.Ульман. 1978. УДК 004
Теория синтаксического анализа, перевода и компиляции. Том 2. Компиляция А.Ахо, Дж.Ульман. 1978. УДК 004
Генератор компиляторов. У.Маккиман, Дж.Хорнинг, Д.Уортман. 1980. УДК 004
Цифровые ЭВМ. Практикум.
К.Самофалов, В.Корнейчук,В.Тарасенко,В.Жабин. 1990. УДК 004
Алгебраическая алгоритмика. П.Ноден, К.Китте. 1999. УДК 004
Операционная система UNIX. А.Робачевский. 1997. УДК 004
Системное программирование на С++ для UNIX. Т.Чан. 1999. УДК 004
Недокументированные возможности Windows NT. А.Коберниченко. 1998. УДК 004
Практический курс программирования на языке PL/1.
Г.Фролов, В.Олюнин. 1980. УДК 004