Русская Википедия:Типизированное лямбда-исчисление

Материал из Онлайн справочника
Перейти к навигацииПерейти к поиску

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

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

<math>\lambda</math>-исчисление с типами является языком декартово-замкнутой категории, что устанавливает прямую связь с такой моделью вычислений, как категориальная абстрактная машина. С одной точки зрения типовые <math>\lambda</math>-исчисления могут рассматриваться как специализации бестиповых <math>\lambda</math>-исчислений, а с другой — наоборот, типовые языки могут считаться более фундаментальными, из которых бестиповые получаются как частные случаи. Анализ этого явления дает теория вычислений Д. Скотта[1].

<math>\lambda</math>-исчисление с типами служит основой для разработки новых систем типизации для языков программирования, поскольку именно средствами типов и зависимостей между ними выражаются желаемые свойства программ.

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

См. также

Примечания

Шаблон:Примечания

Литература

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

  1. Scott D.S. The lattice of flow diagrams.- Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.- Berlin, Heidelberg, New York: Springer-Verlag, 1971, pp. 311—372.