Типизированное лямбда-исчисление

Типизированное , лямбда-исчисление — это типизированный формализм в котором используется лямбда-символ ( $\lambda$ ) для обозначения абстракции анонимной функции. В этом контексте типы обычно представляют собой объекты синтаксической природы, которые присваиваются лямбда-термам; точная природа типа зависит от рассматриваемого исчисления (см. виды ниже). С определенной точки зрения типизированные лямбда-исчисления можно рассматривать как усовершенствования нетипизированного лямбда-исчисления , но с другой точки зрения их также можно считать более фундаментальной теорией, а нетипизированное лямбда-исчисление - частным случаем только с одним типом. ^[1]

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

Типизированные лямбда-исчисления тесно связаны с математической логикой и теорией доказательств через изоморфизм Карри-Говарда , и их можно рассматривать как внутренний язык определенных классов категорий . Например, просто типизированное лямбда-исчисление является языком декартовых закрытых категорий (CCC). ^[2]

Виды типизированных лямбда-исчислений [ править ]

Были изучены различные типизированные лямбда-исчисления. Просто типизированное лямбда-исчисление имеет только один конструктор типа — стрелку. $\to$ , и его единственными типами являются базовые типы и типы функций. $\sigma \to \tau$ . Система T расширяет просто типизированное лямбда-исчисление за счет натуральных чисел и примитивной рекурсии более высокого порядка; в этой системе все функции, доказуемо рекурсивные в арифметике Пеано определимы . Система F допускает полиморфизм за счет использования универсальной количественной оценки всех типов; с логической точки зрения он может описать все функции, которые являются доказуемо полными в логике второго порядка . Лямбда-исчисления с зависимыми типами — это основа интуиционистской теории типов , исчисления конструкций и логической структуры (LF), чистого лямбда-исчисления с зависимыми типами. Основываясь на работе Берарди по системам чистых типов , Хенк Барендрегт предложил лямбда-куб для систематизации отношений чисто типизированных лямбда-исчислений (включая просто типизированное лямбда-исчисление, систему F, LF и исчисление конструкций). ^[3]

Некоторые типизированные лямбда-исчисления вводят понятие подтипирования , т.е. если $A$ является подтипом $B$ , то все члены типа $A$ также есть тип $B$ . Типизированные лямбда-исчисления с подтипами — это просто типизированные лямбда-исчисления с конъюнктивными типами и системой F _<: .

Все системы, упомянутые до сих пор, за исключением нетипизированного лямбда-исчисления, являются строго нормализующими : все вычисления завершаются. Следовательно, они не могут описать все функции , вычислимые по Тьюрингу . ^[4] Как еще одно следствие, они логически последовательны, т.е. существуют необитаемые типы. Однако существуют типизированные лямбда-исчисления, которые не являются строго нормализующими. Например, зависимо типизированное лямбда-исчисление с типом всех типов (Тип: Тип) не является нормализуемым из-за парадокса Жирара . Эта система также является простейшей системой чистого типа, формализмом, который обобщает лямбда-куб. Системы с явными комбинаторами рекурсии, такие как » Плоткина « Язык программирования для вычислимых функций (PCF), не являются нормализующими, но они не предназначены для интерпретации как логики. Действительно, PCF — это прототип типизированного функционального языка программирования, в котором типы используются для обеспечения правильного поведения программ, но не обязательно для их завершения.

Приложения к языкам программирования [ править ]

В компьютерном программировании подпрограммы (функции, процедуры, методы) строго типизированных языков программирования близко соответствуют типизированным лямбда-выражениям. ^[5]

См. также [ править ]

Каппа-исчисление - аналог типизированного лямбда-исчисления, исключающий функции высшего порядка.

Примечания [ править ]

^ Брандл, Хельмут (27 апреля 2024 г.). «Типизированное лямбда-исчисление / Конструкционное исчисление» (PDF) . Расчет конструкций . Проверено 27 апреля 2024 г.
^ Ламбек, Дж.; Скотт, П.Дж. (1986), Введение в категориальную логику высшего порядка , издательство Кембриджского университета , ISBN 978-0-521-35653-4 , МР 0856915
^ Барендрегт, Хенк (1991). «Введение в системы обобщенных типов» . Журнал функционального программирования . 1 (2): 125–154. дои : 10.1017/S0956796800020025 . hdl : 2066/17240 . ISSN 0956-7968 .
^ поскольку проблема остановки для последнего класса оказалась неразрешимой
^ «Что нужно знать перед обсуждением систем типов | Овидий [blogs.perl.org]» . blogs.perl.org . Проверено 26 апреля 2024 г.

Дальнейшее чтение [ править ]

Барендрегт, Хенк (1992). «Лямбда-исчисления с типами» . В Абрамский С. (ред.). Предыстория: Вычислительные структуры . Справочник по логике в информатике. Том. 2. Издательство Оксфордского университета. стр. 117–309. ISBN 9780198537618 .
Брандл, Хельмут (2022). Строительное исчисление / Типизированное лямбда-исчисление

[1] Брандл, Хельмут (27 апреля 2024 г.). «Типизированное лямбда-исчисление / Конструкционное исчисление» (PDF) . Расчет конструкций . Проверено 27 апреля 2024 г.

[2] Ламбек, Дж.; Скотт, П.Дж. (1986), Введение в категориальную логику высшего порядка , издательство Кембриджского университета , ISBN 978-0-521-35653-4 , МР 0856915

[3] Барендрегт, Хенк (1991). «Введение в системы обобщенных типов» . Журнал функционального программирования . 1 (2): 125–154. дои : 10.1017/S0956796800020025 . hdl : 2066/17240 . ISSN 0956-7968 .

[4] поскольку проблема остановки для последнего класса оказалась неразрешимой

[5] «Что нужно знать перед обсуждением систем типов | Овидий [blogs.perl.org]» . blogs.perl.org . Проверено 26 апреля 2024 г.

[1]

[2]

[3]

[4]

[5]