WikiSort.ru - Программирование

Эта статья или раздел нуждается в переработке. Пожалуйста, улучшите статью в соответствии с правилами написания статей.

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

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

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

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

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

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

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

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

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

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

Этот раздел не завершён. Вы поможете проекту, исправив и дополнив его.

Разветвлённая теория типов (Ramified Theory of Types, RTT)^[2]

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

Этот раздел не завершён. Вы поможете проекту, исправив и дополнив его.

Интуиционистскую теорию типов (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) обобщает многомерные теории, устанавливая равенства типов на уровне топологий.

См. также

• Система типов
• Типобезопасность
• Логицизм
• Many-sorted logic^[en]

Примечания

Литература

• Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur ( (фр.)). — Université Paris 7, 1972.

• Robin Milner. A Theory of Type Polymorphism in Programming. — Journal of Computer and System Sciences^[en], 1978. — Т. 17, вып. 3. — С. 348—375. — DOI:10.1016/0022-0000(78)90014-4.

• John C. Reynolds. Theories of programming languages. — Cambridge University Press, 1998. — ISBN 978-0-521-59414-1 (hardback), 978-0-521-10697-9 (paperback).

• Henk Barendregt. Introduction to Generalized Type Systems. — 1991.

• Henk Barendregt. Lambda Calculi with Types. — Oxford University Press, 1992. — Т. Handbook of Logic in Computer Science, vol.2. — С. 117—309.

• Benjamin Pierce. Types and Programming Languages. — MIT Press, 2002. — ISBN 0-262-16209-1.
  • Перевод на русский язык: Бенджамин Пирс. Типы в языках программирования. — Добросвет, 2012. — 680 с. — ISBN 978-5-7913-0082-9.

• 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.

• Robert Harper^[en]. Higher-Dimensional Type Theory. — 2011.

• Robert Harper^[en]. Practical Foundations for Programming Languages. — version 1.37 (revised 01.11.2014). — licensed under the Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 United States License., 2012. — 544 с. Архивировано 24 октября 2015 года.

Ссылки

• Лекция: Теория типов и комбинаторная логика

Это заготовка статьи по логике. Вы можете помочь проекту, дополнив её.