Русская Википедия:Теория типов
Теорией типов считается какая-либо формальная система, являющаяся альтернативой наивной теории множеств, сопровождаемая классификацией элементов такой системы с помощью типов, образующих некоторую иерархию. Также под теорией типов понимают изучение подобных формализмов.
Теория типов — математически формализованная база для проектирования, анализа и изучения систем типов данных в теории языков программирования (раздел информатики). Многие программисты используют это понятие для обозначения любого аналитического труда, изучающего системы типов в языках программирования. В научных кругах под теорией типов чаще всего понимают более узкий раздел дискретной математики, в частности λ-исчисление с типами.
Современная теория типов была частично разработана в процессе разрешения парадокса Рассела и во многом базируется на работе Бертрана Рассела и Альфреда Уайтхеда «Principia mathematica»[1].
Доктрина типов
Доктрина типов восходит к Б. Расселу, согласно которому всякий тип рассматривается как диапазон значимости пропозициональной (высказывательной) функции. Помимо того, считается, что у всякой функции имеется тип (её домен, область определения). В доктрине типов соблюдается выполнимость принципа замены типа (высказывания) на дефинициально эквивалентный тип (высказывание).
Теория типов в логике
В основе этой теории лежит принцип иерархичности. Это означает, что логические понятия — высказывания, индивиды, пропозициональные функции — располагаются в иерархию типов. Существенно, что произвольная функция в качестве своих аргументов имеет лишь те понятия, которые предшествуют ей в иерархии.
Некоторая теория типов
Под некоторой теорией типов обычно понимают прикладную логику высших порядков, в которой имеется тип N натуральных чисел и в которой выполняются аксиомы арифметики ПеаноШаблон:Нет АИ.
Разветвлённая теория типов
Исторически первой предложенной теорией типов (период с 1902 по 1913) является Разветвлённая теория типов (Шаблон:Lang-en2, RTT), построенная Уайтхедом и Расселом, и окончательно сформулированная в фундаментальной работе «Principia Mathematica». В основе данной теории лежит принцип ограничения числа случаев, когда объекты принадлежат единому типу. Явным образом объявляется восемь таких случаев и различаются две иерархии типов: (просто) «типы» и «порядки». При этом сама нотация «типа» не определена, и имеется ряд других неточностей, т.к. главным намерением было объявить неравными типы функций от разного числа аргументов или от аргументов разных типовШаблон:Sfn. Неотъемлемой составляющей теории является аксиома редуцируемости.
Простая теория типов
В 1920-х Чвистек и Рамси предложили неразветвлённую теорию типов, ныне известную как «Теория простых типов» или Простая теория типов (Шаблон:Lang-en2), которая сворачивает иерархию типов, устраняя необходимость в аксиоме редуцируемости.
Интуиционистская теория типов
Шаблон:Main Шаблон:Заготовка раздела
Интуиционистскую теорию типов (Шаблон:Lang-en2, ITT) построил Пер Мартин-Лёф.
Чистые системы типов
Теория чистых систем типов (Шаблон:Lang-en, PTS) обобщает все исчисления лямбда-куба и формулирует правила, позволяющие вычислить их как частные случаи. Её независимо построили Берарди (Шаблон:Lang-en2) и Терлоу (Шаблон:Lang-en2). Чистые системы типов оперируют только понятием типа, рассматривая все понятия других исчислений только в виде типов — потому они и называются «чистыми». Не производится разделения между термами и типами, между различными слоями (т.е. рода́ типов также называются типами, только относящимися к другой вселенной), и даже сами слои называются не сортами, а типами (точнее, вселенными типов). В общем виде, чистая система типов задаётся понятием спецификации, пятью жёсткими правилами и двумя гибкими (меняющимися от системы к системе). Спецификация чистой системы типов представляет собой тройку (S,A,R), где S — множество сортов (Sorts), A — множество аксиом (Axioms) над этими сортами и R — множество правил (Rules).Шаблон:SfnШаблон:SfnШаблон:Sfn
Многомерные теории типов
Теории типов высших размерностей (Шаблон:Lang-en) или просто Высшие теории типов (Шаблон:Lang-en2, HTT) обобщают традиционные теории типов, разрешая устанавливать нетривиальные отношения эквивалентности между типами. Например, если взять множество пар (декартовых произведений) натуральных чисел nat × nat и множество функций, возвращающих натуральное число nat -> nat, то нельзя утверждать, что элементы этих множеств попарно равны, но можно утверждать, что эти множества эквивалентны. Изоморфизмы между типами и изучаются в двухмерной, трёхмерной и т.д. теориях типов. Весь необходимый базис для формулировки этих теорий был заложен ещё Жираром — Рейнольдсом, но сами теории были сформулированы много позже.Шаблон:Sfn[2]
Гомотопическая теория типов
Гомотопическая теория типов (Шаблон:Lang-en, HoTT) обобщает многомерные теории, устанавливая равенства типов на уровне топологий. В многомерных теориях понятия «эквивалентности типов» и «равенства типов» считаются различными. Радикальным нововведением гомотопической теории является аксиома унивалентности, постулирующая, что если типы топологически эквивалентны, то они топологически равны.
Экономичная теория типов
Экономичная теория типов (Шаблон:Lang-en), сформулированная в 2020 году, расширяет функциональные типы простейшей информацией об алгоритмической сложности — количестве вычислительных шагов, требуемых для получения результата — позволяя верифицировать программы не только по смысловой корректности, но и по закладываемым ограничениям временной сложности.[3] Это делается за счёт конструктора зависимых типов функций funtime. Формализация теории требует в том числе учёт проблемы остановки, для чего в правилах типизации требуется, чтобы рекурсивный вызов имел строго меньшую сложность, чем вызов с текущим значением аргумента. CATT позволяет при построении доказательства производить различие между «абстрактной стоимостью», включающей математические шаги (такие, как рекурсивный вызов) и «машинной стоимостью», учитывающей эффективность физически реализованных инструкций (например, что арифметические операции суммы и произведения на большинстве процессоров выполняются за одинаковое время), а также учитывать параллелизм.
См. также
Примечания
Литература
- Шаблон:Книга
- Перевод на русский язык: Шаблон:Книга
- Вольфенгаген В. Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы. — Шаблон:М.: JurInfoR Ltd., АО «Центр ЮрИнфоР», 2004. — xvi+789 с. ISBN 5-89158-100-0.
Ссылки
- ↑ «Основания математики» — фундаментальный трёхтомник математической логики (Уайтхед, Альфред Н. Основания математики: В 3 т./ А. Н. Уайтхед, Б. Рассел; Под ред. Г. П. Ярового, Ю. Н. Радаева. — Самара: Изд-во «Самарский университет», 2005—2006. — ISBN 5-86465-359-4)
- ↑ Шаблон:Cite web
- ↑ Шаблон:Статья
