Інтуїціоністська теорія типів
Інтуїціоні́стська тео́рія ти́пів (також відома як теорія Мартіна-Льофа або конструктивна теорія типів) — теорія типів, яку розробив шведський математик і філософ Пер Мартін-Льоф, опублікована в 1972 року. Метою теорії послужила формалізація конструктивної математики, конструктивні об'єкти якої, згідно з Марковим-молодшим, є «деякими фігурами, складеними з елементарних конструктивних об'єктів»[1]. У цьому напрямі логіку математики можна розглядати як частину філософії математики, у складі якої використовується[2].
Є кілька версій інтуїціоністської теорії типів. Сам Мартін-Льоф запропонував як інтенсійний[en], так і екстенсійний[en] варіанти теорії. На початку також представлено непредикативні версії, не сумісні з парадоксом Жірара. Проте всі версії зберігають базовий стиль конструктивної логіки з використанням залежних типів.
Примітки
ред.- ↑ Марков А. А. О конструктивной математике. Проблемы конструктивного направления в математике. 2.Конструктивный математический анализ, Сборник работ. Тр. МИАН СССР, 67, Изд-во АН СССР
- ↑ Д. Д. Рогозин; А. В. Родин. Теория типов в логике и основаниях математике. Москва, Институт философии РАН. 2016
В іншому мовному розділі є повніша стаття Intuitionistic type theory(англ.). Ви можете допомогти, розширивши поточну статтю за допомогою перекладу з англійської.
|