Интуиционистская теория типов
-
Основы теории типов
- Теория типов — это формализм для описания структуры и свойств математических объектов.
- Она была разработана Мартином-Лефом и является основой для интуиционистской логики.
- Теория типов включает в себя типы, объекты и отношения, а также суждение о равенстве.
-
Типы и объекты
- Тип — это абстрактное понятие, которое представляет множество объектов с определенными свойствами.
- Объект — это конкретный элемент, который принадлежит определенному типу.
- Существуют различные способы создания новых типов и объектов, включая рекурсивные типы и зависимые типы.
-
Суждения и доказательства
- Суждения используются для выражения формул и создания новых объектов и типов.
- Доказательства представляют собой объекты, которые подтверждают истинность утверждений.
- Теория типов позволяет создавать новые типы и объекты на основе существующих.
-
Категориальные модели
- Р. А. Г. Сили предложил использовать локально декартову замкнутую категорию в качестве базовой модели теории типов.
- Хофман и Дайбьер усовершенствовали эту модель до категорий с семействами.
- Категория с семействами включает в себя контексты, функторы и аксиомы, которые обеспечивают гармонию с подстановкой.
- Пересказана только часть статьи. Для продолжения перейдите к чтению оригинала.