Теория типов

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск


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

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

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

Доктрина типов[править | править исходный текст]

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

Теория типов в логике[править | править исходный текст]

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

Некоторая теория типов[править | править исходный текст]

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

Чистая теория типов[править | править исходный текст]

Среди теорий типов имеется одна выделенная теория, называемая чистой теорией типов, в которой нет никаких дополнительных типов, термов и/или допущений, кроме необходимых для формулирования именно теории типов.

См. также[править | править исходный текст]

Литература[править | править исходный текст]

  • Вольфенгаген В. Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы. — М.: JurInfoR Ltd., АО «Центр ЮрИнфоР», 2004. — xvi+789 с. ISBN 5-89158-100-0.

Примечания[править | править исходный текст]

  1. «Основания математики» — фундаментальный трёхтомник математической логики (Уайтхед, Альфред  Н. Основания математики: В 3 т./ А. Н. Уайтхед, Б. Рассел; Под ред. Г. П. Ярового, Ю. Н. Радаева. — Самара: Изд-во «Самарский университет», 2005—2006. — ISBN 5-86465-359-4)

Ссылки[править | править исходный текст]