Типизированное лямбда-исчисление
Лямбда-исчисление с типами -- это ти́повый формализм, применяющий символ абстракции „λ“ для записи выражений, обозначающих безымянные функции. Ти́повые λ-исчисления являются фундаментальными примитивными языками программирования, которые обеспечивают основу ти́повым языкам функционального программирования -- аппликативным языкам,-- среди которых ML и Haskell, а также ти́повым императивным языкам программирования.
λ-исчисление с типами является языком декартово-замкнутой категории (д.з.к.), что устанавливает прямую связь с такой моделью вычислений, как категориальная абстрактная машина. С одной точки зрения ти́повые λ-исчисления могут рассматриваться как специализации бестиповых λ-исчислений, а с другой -- наоборот, типовые языки могут считаться более фундаментальными, из которых бестиповые получаются как частные случаи. Анализ этого явления дает теория вычислений Д. Скотта[1]. Построение λ-исчисления с типами, выполненное элементарными средствами имеется в[2].
λ-исчисление с типами служит основой для разработки новых систем типизации для языков программирования, поскольку именно средствами типов и зависимостей между ними выражаются желаемые свойства программ.
В программировании самостоятельные вычислительные блоки (функции, прицедуры, методы) языков программирования с сильной типизацией соответствуют ти́повым λ-выражениям.
См. также
- Лямбда-исчисление
- Модели вычислений
- Теория вычислений
- Декартово-замкнутая категория
- Аппликативный подход к программированию
- Категориальная абстрактная машина
Ссылки
- ↑ 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.
- ↑ Вольфенгаген В.Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы. -- М.: JurInfoR Ltd., АО “Центр ЮрИнфоР”, 2004. -- xvi+789 с. ISBN 5-89158-100-0.
Литература
- Henk Barendregt Lambda Calculi with Types, Handbook of Logic in Computer Science, Volume II, Oxford University Press.
- Вольфенгаген В.Э. Комбинаторная логика в программировании. Вычисления с объектами в примерах и задачах. -- М.: МИФИ, 1994. – 204 с.; 2-е изд., М.: АО "Центр ЮрИнфоР", 2003. – 336 с. ISBN 5-89158-101-9.