Featured

Начальная страница

Все переводы разделены на 2 группы: «Книги» и «Статьи». Каждая из групп содержит список названий-ссылок (с указанием авторов) на соответствующие записи (если название не превращено в ссылку, запись только запланирована).

Все записи структурированы единообразно, в соответствии со следующим шаблоном:

Это перевод … (предыдущий раздел — <URL-ссылка>, оглавление — <URL-ссылка>)

<URL-ссылка содержимого> [включает подразделы: …]

Следующий раздел — <URL-ссылка>

где, <URL-ссылка> — название-ссылка; квадратные скобки указывают на необязательность соответствующего текста; <URL-ссылка содержимого> — название-ссылка, начинающаяся с «Содержимое …» и указывающая на текст данного раздела в pdf-формате.

Текст в pdf-формате не содержит непосредственно возможности его комментирования. Комментарии можно размещать в записи, откуда исходит <URL-ссылка содержимого>. Сделано это для того, чтобы формирование комментариев и просмотр содержимого можно было осуществлять параллельно, поскольку содержимое всегда открывается в новом окне.

Просьба в комментарии указывать номер страницы комментируемого текста.

Книги

Статьи

Реклама
Featured

Теория категорий для программистов (перевод глав книги Б. Милевски)

Предисловие редактора перевода

Исходный авторский текст расположен по адресу:

https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/

В основу перевода первых глав включены варианты, подготовленные М.Страховым (Monnoroch на Хабрахабр: предисловие и гл.1-4), А.Бирюковым совместно с Bodigrim (leshabirukov, Bodigrim на Хабрахабр: гл.5-7). Комплектность перевода соответствует текущему состоянию книги у автора. Активное участие в вычитке переводов принимает А.Бирюков.

Основная особенность переводов, отличающая текст от авторского, заключается в цветовом выделении формальных фрагментов. Синим цветом выделены математические формулы и символы, а также программные фрагменты, набранные моноширинным шрифтом, на псевдо Haskell. Пурпурный цвет выделяет программные фрагменты на C++ и Haskell. Помимо этого везде черным полужирным начертанием выделены обозначения категорий. (Цель этой самодеятельности — улучшить восприятие текста; убрать это, при необходимости, будет нетрудно).

С благодарностью принимаются любые замечания по переводу и офрмлению текста. (Согласование текста из разных глав, например, существуют повторы при введении новых терминов, будет произведено после авторского завершения работы; возможно Милевски внесет некоторые изменения после завершения).


Предисловие

Часть I

  1. Категория: суть композиции
  2. Типы и функции
  3. Большие и малые категории
  4. Категории Клейсли
  5. Произведения и копроизведения
  6. Простые алгебраические типы данных
  7. Функторы
  8. Функториальность
  9. Функциональные типы
  10. Естественные преобразования

Часть II

  1. Теория категорий и декларативное программирование
  2. Пределы и копределы
  3. Свободные моноиды
  4. Представимые функторы
  5. Лемма Йонеды
  6. Вложение Йонеды

Часть III

  1. Все о морфизмах
  2. Сопряжения
  3. Свободные / забывающие сопряжения
  4. Монады: определение программиста
  5. Монады и эффекты
  6. Монады с категорной точки зрения
  7. Комонады
  8. F-алгебры
  9. Алгебры для монад
  10. Концы и коконцы
  11. Расширения Кана
  12. Обогащенные категории
  13. Топосы
  14. Теории Ловера
  15. Монады, моноиды и категории

 

(HoTT) Гомотопические n-типы

Это перевод 7 главы книги (предыдущий раздел — (HoTT) Высшие индуктивные типы, оглавление — Гомотопическая теория типов).

Содержимое текущего раздела включает подразделы:

  • Определение n-типов
  • Доказательства единственности тождественности
  • Усечения
  • Копределы n-типов
  • Связность
  • Ортогональная факторизация
  • Модальности

(HoTT) Высшие индуктивные типы

Это перевод 6 главы книги (предыдущий раздел — (HoTT) Индукция, оглавление — Гомотопическая теория типов).

Содержимое текущего раздела включает подразделы:

  • Введение
  • Принципы индукции и зависимые пути
  • Интервал
  • Окружности и сферы
  • Надстройки
  • Клеточные комплексы
  • Концентраторы и спицы
  • Амальгамы
  • Усечения
  • Частные
  • Алгебра
  • Лемма сглаживания
  • Общий синтаксис высших индуктивных определений

Следующий раздел — (HoTT) Гомотопические n-типы

(HoTT) Индукция

Это перевод 5 главы книги (предыдущий раздел — (HoTT) Эквивалентность, оглавление — Гомотопическая теория типов).

Содержимое текущего раздела включает подразделы:

  • Введение в индуктивные типы
  • Единственность индуктивных типов
  • W-типы
  • Индуктивные типы являются инициальные алгебры
  • Гомотопически-индуктивные типы
  • Общий синтаксис индуктивных определений
  • Обобщения индуктивных типов
  • Типы тождественности и системы тождественности

Следующий раздел — (HoTT) Высшие индуктивные типы

(Rutten) Универсальная коалгебра

Это перевод статьи Раттена (J.J.M.M. Rutten, Universal coalgebra: a theory of systems, 1996) об универсальных коалгебрах, рассматриваемых в контексте описания систем (исходный текст расположен по адресу — Текст оригинальной статьи).

Содержимое перевода статьи включает:

  1. Введение
  2. Коалгебры, гомоморфизмы и взаимоподобие
  3. Системы
  4. Пределы и копределы систем
  5. Основные сведения о взаимоподобиях
  6. Подсистемы
  7. Три теоремы об изоморфизмах
  8. Простые системы и коиндукция
  9. Терминальные системы
  10. Существование терминальных систем
  11. Примеры коиндуктивных определений
  12. Примеры доказательств по коиндукции
  13. Индукция и коиндукция
  14. Сравнение систем
  15. Косвободность и комногообразие систем
  16. Динамические системы и символическая динамика
  17. Замечания и связанные с этим работы
  18. Дополнения о множествах и категориях

(HoTT) Эквивалентность

Это перевод 4 главы книги (предыдущий раздел — (HoTT) Множества и логика, оглавление — Гомотопическая теория типов).

Содержимое текущего раздела включает подразделы:

  • Квазиобратные
  • Полусопряженные эквивалентности
  • Би-обратимые отображения
  • Стягиваемые слои
  • Об определении эквивалентностей
  • Сюръекции и вложения
  • Свойства замкнутости эквивалентностей
  • Классификатор объектов
  • Унивалентность означает функциональную экстенсиональность
  • Примечания
  • Упражнения

Следующий раздел — (HoTT) Индукция

(HoTT) Множества и логика

Это перевод 3 главы книги (предыдущий раздел — (HoTT) Гомотопическая теория типов, оглавление — Гомотопическая теория типов).

Содержимое текущего раздела включает подразделы:

  • Множества и n-типы
  • Высказывания как типы?
  • Простые высказывания
  • Классическая и интуиционистская логики
  • Подмножества и пропозициональное изменение размера
  • Логика простых высказываний
  • Пропозициональное усечение
  • Аксиома выбора
  • Принцип единственности выбора
  • Когда высказывания усекаются?
  • Стягиваемость
  • Примечания
  • Упражнения

Следующий раздел — (HoTT) Эквивалентность

(FreeTrm) «Бесплатные» теоремы

Это перевод пересмотренного варианта статьи Уодлера (Philip Wadler), представленной на 4 Международном симпозиуме по языкам функционального программирования и компьютерной архитектуре в Лондоне, сентябрь 1989 года (исходный текст расположен по адресу — https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf).

Содержимое перевода статьи включает:

  1. Введение
  2. Объяснение параметричности
  3. Применение параметричности
  4. Полиморфное λ-исчисление
  5. Семантика полиморфного λ-исчисления
  6. Теорема о параметричности
  7. Неподвижные точки