Войти
Типизированного лямбда - исчисление является типизированным формализм, который использует лямбда-символ () для обозначения анонимную функцию абстракции. В этом контексте типы обычно являются объектами синтаксического характера, которые присваиваются лямбда-терминам; точная природа типа зависит от рассматриваемого исчисления (см. виды ниже). С определенной точки зрения типизированные лямбда-исчисления можно рассматривать как уточнения нетипизированного лямбда-исчисления, но с другой точки зрения их также можно рассматривать как более фундаментальную теорию, а нетипизированное лямбда-исчисление - как частный случай, имеющий только один тип.
Типизированные лямбда-исчисления являются основополагающими языками программирования и составляют основу типизированных функциональных языков программирования, таких как ML и Haskell, и, более косвенно, типизированных императивных языков программирования. Типизированные лямбда-исчисления играют важную роль в разработке систем типов для языков программирования; здесь типизируемость обычно фиксирует желаемые свойства программы (например, программа не вызовет нарушения доступа к памяти).
Типизированные лямбда-исчисления тесно связаны с математической логикой и теорией доказательств через изоморфизм Карри – Ховарда, и их можно рассматривать как внутренний язык классов категорий ; например, просто типизированное лямбда-исчисление - это язык декартовых закрытых категорий (CCC).
Изучены различные типизированные лямбда-исчисления. Просто напечатал лямбда - исчисление имеет только один конструктор типа, стрелка, и только его типы основные типы и типы функций. Система T расширяет просто типизированное лямбда-исчисление с помощью типа натуральных чисел и примитивной рекурсии более высокого порядка; в этой системе все функции, доказуемо рекурсивные в арифметике Пеано, определимы. Система F допускает полиморфизм, используя универсальную количественную оценку по всем типам; с логической точки зрения он может описывать все функции, которые доказуемо являются полными в логике второго порядка. Лямбда-исчисления с зависимыми типами являются основой интуиционистской теории типов, исчисления конструкций и логической основы (LF), чистого лямбда-исчисления с зависимыми типами. Основываясь на работе Берарди над системами чистых типов, Хенк Барендрегт предложил лямбда-куб для систематизации отношений чисто типизированных лямбда-исчислений (включая просто типизированное лямбда-исчисление, систему F, LF и исчисление конструкций).
Некоторые типизированные лямбда-исчисления вводят понятие подтипа, т. Е. Если является подтипом, то все термины типа также имеют тип. Типизированного лямбда - исчислений с подтипов являются просто напечатал лямбда - исчисление с присоединительными типов и System F lt;:.
Все упомянутые до сих пор системы, за исключением нетипизированного лямбда-исчисления, строго нормализуют : все вычисления прекращаются. Следовательно, они не могут описать все функции, вычислимые по Тьюрингу. Как еще одно следствие, они логически последовательны, т. Е. Существуют необитаемые типы. Однако существуют типизированные лямбда-исчисления, которые не являются строго нормализующими. Например, лямбда-исчисление с зависимым типом всех типов (Тип: Тип) не нормализуется из-за парадокса Жирара. Эта система также является простейшей системой чистых типов, формализмом, обобщающим лямбда-куб. Системы с явными комбинаторами рекурсии, такие как « Язык программирования для вычислимых функций » (PCF) Плоткина, не нормализуются, но они не предназначены для интерпретации как логики. Действительно, PCF является прототипом типизированного функционального языка программирования, в котором типы используются для обеспечения правильного поведения программ, но не обязательно для их завершения.
В компьютерном программировании подпрограммы (функции, процедуры, методы) строго типизированных языков программирования близко соответствуют типизированным лямбда-выражениям.
