Теория типов

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

Теория типов — математически формализованная база для проектирования, анализа и изучения систем типов данных в теории языков программирования (раздел информатики). Многие программисты используют это понятие для обозначения любого аналитического труда, изучающего системы типов в языках программирования. В научных кругах под теорией типов чаще всего понимают более узкий раздел дискретной математики, в частности λ-исчисление с типами.

Современная теория типов была частично разработана в процессе разрешения парадокса Рассела и во многом базируется на работе Бертрана Рассела и Альфреда Уайтхеда «Principia mathematica»[1].

Доктрина типовПравить

Доктрина типов восходит к Б. Расселу, согласно которому всякий тип рассматривается как диапазон значимости пропозициональной (высказывательной) функции. Помимо того, считается, что у всякой функции имеется тип (её домен, область определения). В доктрине типов соблюдается выполнимость принципа замены типа (высказывания) на дефинициально эквивалентный тип (высказывание).

Теория типов в логикеПравить

В основе этой теории лежит принцип иерархичности. Это означает, что логические понятия — высказывания, индивиды, пропозициональные функции — располагаются в иерархию типов. Существенно, что произвольная функция в качестве своих аргументов имеет лишь те понятия, которые предшествуют ей в иерархии.

Некоторая теория типовПравить

Под некоторой теорией типов обычно понимают прикладную логику высших порядков, в которой имеется тип N натуральных чисел и в которой выполняются аксиомы арифметики Пеано[источник не указан 1355 дней].

Разветвлённая теория типовПравить

Исторически первой предложенной теорией типов (период с 1902 по 1913) является Разветвлённая теория типов (Ramified Theory of Types, RTT), построенная Уайтхедом и Расселом, и окончательно сформулированная в фундаментальной работе «Principia Mathematica». В основе данной теории лежит принцип ограничения числа случаев, когда объекты принадлежат единому типу. Явным образом объявляется восемь таких случаев и различаются две иерархии типов: (просто) «типы» и «порядки». При этом сама нотация «типа» не определена, и имеется ряд других неточностей, т.к. главным намерением было объявить неравными типы функций от разного числа аргументов или от аргументов разных типов[2]. Неотъемлемой составляющей теории является аксиома редуцируемости.

Простая теория типовПравить

В 1920-х Чвистек и Рамси предложили неразветвлённую теорию типов, ныне известную как «Теория простых типов» или Простая теория типов (Simple Type Theory), которая сворачивает иерархию типов, устраняя необходимость в аксиоме редуцируемости.

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

Интуиционистскую теорию типов (Intuitionistic Type Theory, ITT) построил Пер Мартин-Лёф.

Чистые системы типовПравить

Теория чистых систем типов[en] (англ. pure type systems, PTS) обобщает все исчисления лямбда-куба и формулирует правила, позволяющие вычислить их как частные случаи. Её независимо построили Берарди (Berardi) и Терлоу (Terlouw). Чистые системы типов оперируют только понятием типа, рассматривая все понятия других исчислений только в виде типов — потому они и называются «чистыми». Не производится разделения между термами и типами, между различными слоями (т.е. рода́ типов также называются типами, только относящимися к другой вселенной), и даже сами слои называются не сортами, а типами (точнее, вселенными типов). В общем виде, чистая система типов задаётся понятием спецификации, пятью жёсткими правилами и двумя гибкими (меняющимися от системы к системе). Спецификация чистой системы типов представляет собой тройку (S,A,R), где S — множество сортов (Sorts), A — множество аксиом (Axioms) над этими сортами и R — множество правил (Rules).[3][4][5]

Многомерные теории типовПравить

Теории типов высших размерностей (англ. higher-dimensional type theories) или просто Высшие теории типов (higher type theories, HTT) обобщают традиционные теории типов, разрешая устанавливать нетривиальные отношения равенства между типами. Например, если взять множество пар (декартовых произведений) натуральных чисел nat × nat и множество функций, возвращающих натуральное число nat -> nat, то нельзя утверждать, что элементы этих множеств попарно равны, но можно утверждать, что эти множества эквивалентны. Изоморфизмы между типами и изучаются в двухмерной, трёхмерной и т.д. теориях типов. Весь необходимый базис для формулировки этих теорий был заложен ещё Жираром — Рейнольдсом, но сами теории были сформулированы много позже.[6][7]

Гомотопическая теория типовПравить

Гомотопическая теория типов (англ. homotopy type theory, HoTT) обобщает многомерные теории, устанавливая равенства типов на уровне топологий. В многомерных теориях понятия «эквивалентности типов» и «равенства типов» считаются различными. Радикальным нововведением гомотопической теории является аксиома унивалентности, постулирующая, что если типы топологически эквивалентны, то они топологически равны.

См. такжеПравить

ПримечанияПравить

  1. «Основания математики» — фундаментальный трёхтомник математической логики (Уайтхед, Альфред  Н. Основания математики: В 3 т./ А. Н. Уайтхед, Б. Рассел; Под ред. Г. П. Ярового, Ю. Н. Радаева. — Самара: Изд-во «Самарский университет», 2005—2006. — ISBN 5-86465-359-4)
  2. Modern Perspective on Type Theory, 2004, 2b The Ramified Theory of Types RTT, с. 35.
  3. Barendregt, "Lambda Calculi with Types", 1992, 5.2. Pure type system, с. 96-114.
  4. Modern Perspective on Type Theory, 2004, 4c Pure Type Systems, с. 116.
  5. Пирс, 2002, с. 493.
  6. Harper, "Higher-Dimensional Type Theory", 2011.
  7. Robert Harper Research Papers (недоступная ссылка). Дата обращения 20 октября 2016. Архивировано 30 октября 2016 года.

ЛитератураПравить

  • Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur ( (фр.)). — Université Paris 7, 1972.
  • Henk Barendregt. Introduction to Generalized Type Systems. — 1991.
  • Henk Barendregt. Lambda Calculi with Types (англ.). — Oxford University Press, 1992. — Vol. Handbook of Logic in Computer Science, vol.2. — P. 117—309.
  • Fariouz Kamareddine, Twan Laan, Rob Nederpelt. A Modern Perspective on Type Theory. From its Origins until Today. — Kluwer Academic Publishers, 2004. — ISBN 1-4020-2334-0 (print), 1-4020-2335-9 (eBook).
  • Вольфенгаген В. Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы. — М.: JurInfoR Ltd., АО «Центр ЮрИнфоР», 2004. — xvi+789 с. ISBN 5-89158-100-0.

СсылкиПравить