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

Типовые ${\displaystyle \lambda }$ -исчисления являются фундаментальными примитивными языками программирования , которые обеспечивают основу типовым языкам функционального программирования — аппликативным языкам , — среди которых ML и Haskell , а также типовым императивным языкам программирования.

${\displaystyle \lambda }$ -исчисление с типами является языком декартово-замкнутой категории , что устанавливает прямую связь с такой моделью вычислений , как категориальная абстрактная машина . С одной точки зрения типовые ${\displaystyle \lambda }$ -исчисления могут рассматриваться как специализации бестиповых ${\displaystyle \lambda }$ -исчислений, а с другой — наоборот, типовые языки могут считаться более фундаментальными, из которых бестиповые получаются как частные случаи. Анализ этого явления дает теория вычислений Д. Скотта .

${\displaystyle \lambda }$ -исчисление с типами служит основой для разработки новых для языков программирования, поскольку именно средствами типов и зависимостей между ними выражаются желаемые свойства программ.

В программировании самостоятельные вычислительные блоки (функции, процедуры, методы) языков программирования с сильной типизацией соответствуют типовым ${\displaystyle \lambda }$ -выражениям.

См. также

• Лямбда-куб
• Каррирование
• Просто типизированное лямбда-исчисление
• Полиморфное лямбда-исчисление

Примечания

Литература

• Friedman H. Equality between functionals. LogicColl. '73, pages 22-37, LNM 453, 1975.
• Barendregt H. , Handbook of Logic in Computer Science, Volume II, Oxford University Press.