Интуиционистская теория типов

Интуиционистская теория типов (также известна, как теория Мартина-Лёфа или конструктивная теория типов) — теория типов, разработанная шведским математиком и философом Пером Мартином-Лёфом, была опубликована в 1972 году. Целью теории послужила формализация конструктивной математики, конструктивные объекты которой, согласно Маркову-младшему, являются «некоторыми фигурами, составленными из элементарных конструктивных объектов»[1]. В данном направлении логика математики может рассматриваться как часть философии математики, в составе которой и используется[2].

Имеются несколько версий интуиционистской теории типов. Самим Мартином-Лёфом предложены как интенсиональный, так и экстенсиональный варианты теории. В начале были также представлены непредикативные версии, не совместимые с парадоксом Жирара. Тем не менее, все версии сохраняют базовый стиль конструктивной логики с использованием зависимых типов.

Примечания
  1. Марков А. А. О конструктивной математике. Проблемы конструктивного направления в математике. 2.Конструктивный математический анализ, Сборник работ. Тр. МИАН СССР, 67, Изд-во АН СССР
  2. Д. Д. Рогозин; А. В. Родин. Теория типов в логике и основаниях математике. Москва, Институт философии РАН. 2016
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.