Теория типов

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


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

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

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

Содержание

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

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

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

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

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

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

Чистая теория типов

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

См. также

Литература

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

Примечания

  1. ↑

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

Ссылки


Логика

Wikimedia Foundation. 2010.

Игры ⚽ Нужен реферат?

Полезное


Смотреть что такое "Теория типов" в других словарях:

  • ТЕОРИЯ ТИПОВ — англ. theory, types; нем. Typentheorie. Способ построения формальной (математической) логики, при к ром вводится различение объектов нескольких уровней (типов). Ее суть состоит в различении по типам: индивидов (тип 1), их свойств (тип 2), свойств …   Энциклопедия социологии

  • теория типов — — [http://www.iks media.ru/glossary/index.html?glossid=2400324] Тематики электросвязь, основные понятия EN theory of types …   Справочник технического переводчика

  • ТЕОРИЯ ТИПОВ — англ. theory, types; нем. Typentheorie. Способ построения формальной (математической) логики, при к ром вводится различение объектов нескольких уровней (типов). Ее суть состоит в различении по типам: индивидов (тип 1), их свойств (тип 2), свойств …   Толковый словарь по социологии

  • Теория типов Кювье — была предложена как противовес защищавшейся тогда трансформистами (см. Трансформизм) Т. единства плана строения животных. По Кювье, присматриваясь к разнообразию строения органов, можно заметить, что одни из них являются более постоянными в своей …   Энциклопедический словарь Ф.А. Брокгауза и И.А. Ефрона

  • ТЕОРИЯ ЛИТОГЕНЕЗА — обобщающий раздел литологии, выясняющий общие закономерности осадко и породообразования и дающий их истолкование. Т. л. начала впервые создаваться в советской литологии около четверти века тому назад, причем к настоящему времени предложено… …   Геологическая энциклопедия

  • Теория множеств — Теория множеств  раздел математики, в котором изучаются общие свойства множеств. Теория множеств лежит в основе большинства математических дисциплин; она оказала глубокое влияние на понимание предмета самой… …   Википедия

  • ТИПОВ ТЕОРИЯ — формальная теория 1 го порядка (см. Формальная система), один из вариантов к рой простая теория типов описан ниже. Термин лТ. т …   Математическая энциклопедия

  • ТЕОРИЯ ПОЗНАНИЯ — Гносеология (от греч. gno sis знание, logos слово, понятие), Эпистемолог и я (от греч. episteme знание) раздел философии, исследующий природу человеческого познания, его источники и предпосылки, отношение знания к предмету познания, условия… …   Философская энциклопедия

  • Теория привязанности — Теория привязанности  это психологическая, эволюционная, и этологическая теория о взаимоотношениях между людьми. Основное положение теории привязанности состоит в том, что для нормального социального и эмоционального развития ребенку… …   Википедия

  • Теория струн — Теория суперструн Теория …   Википедия


Поделиться ссылкой на выделенное

Прямая ссылка:
… Нажмите правой клавишей мыши и выберите «Копировать ссылку»