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

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

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

Примечания

  1. Марков А. А . О конструктивной математике. Проблемы конструктивного направления в математике. 2.Конструктивный математический анализ, Сборник работ. Тр. МИАН СССР, 67, Изд-во АН СССР
  2. Д. Д. Рогозин ; А. В. Родин . Теория типов в логике и основаниях математике. Москва , Институт философии РАН . 2016
Источник —

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