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