В математике , логике и компьютерных науках теория типов — это формальное представление конкретной системы типов , [a] , а в общей теории типов — это академическое исследование систем типов. Некоторые теории типов служат альтернативой теории множеств в качестве основы математики . В качестве основы были предложены две влиятельные теории типов: типизированное λ-исчисление Алонсо Черча и интуиционистская теория типов Пера Мартина-Лёфа . Большинство компьютеризированных систем корректуры используют теорию типов дляих фундамент . Распространенным является «Исчисление индуктивных построений» Тьерри Коканда .
Теория типов была создана, чтобы избежать парадокса в математической основе, основанной на наивной теории множеств и формальной логике . Парадокс Рассела , обнаруженный Бертраном Расселом , существовал потому, что множество можно было определить, используя «все возможные множества», включая себя. Между 1902 и 1908 годами Бертран Рассел предложил различные «теории типов», чтобы решить эту проблему. К 1908 году Рассел пришел к «разветвленной» теории типов вместе с « аксиомой сводимости », обе из которых занимают видное место в « Принципах математики» Уайтхеда и Рассела .опубликовано между 1910 и 1913 годами. Эта система позволила избежать парадокса Рассела, создав иерархию типов, а затем присвоив каждому конкретному математическому объекту тип. Сущности данного типа строятся исключительно из подтипов этого типа, [b] таким образом предотвращая определение сущности с использованием самой себя. Теория типов Рассела исключала возможность того, что множество является членом самого себя.
Типы не всегда использовались в логике. Были и другие способы избежать парадокса Рассела. [3] Типы получили признание при использовании с одной конкретной логикой, лямбда-исчислением Алонзо Чёрча .
Самый известный ранний пример — просто типизированное лямбда-исчисление Черча . Теория типов Чёрча [4] помогла формальной системе избежать парадокса Клини-Россера , который поразил исходное нетипизированное лямбда-исчисление. Черч продемонстрировал, что она может служить основой математики, и ее назвали логикой высшего порядка .
Фраза «теория типов» теперь обычно относится к типизированной системе, основанной на лямбда-исчислении. Одной из влиятельных систем является интуиционистская теория типов Пера Мартина-Лёфа , которая была предложена в качестве основы для конструктивной математики . Другим является исчисление конструкций Тьерри Коканда , которое используется в качестве основы Coq , Lean и другими «помощниками по проверке» (компьютеризированными программами для написания корректуры). Теории типов являются областью активных исследований, о чем свидетельствует теория гомотопических типов .
Существует много теорий типов, что затрудняет создание всеобъемлющей таксономии; эта статья не является исчерпывающей категоризацией. Далее следует введение для тех, кто не знаком с теорией типов, охватывающее некоторые из основных подходов.