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

λ-исчисление с типами является языком декартово-замкнутой категории, что устанавливает прямую связь с такой моделью вычислений, как категориальная абстрактная машина. С одной точки зрения типовые λ-исчисления могут рассматриваться как специализации бестиповых λ-исчислений, а с другой в наоборот, типовые языки могут считаться более фундаментальными, из которых бестиповые получаются как частные случаи. Анализ этого явления дает теория вычислений Д. Скотта^[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.

[править] Литература

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.
Вольфенгаген В. Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы. в М.: JurInfoR Ltd., АО «Центр ЮрИнфоР», 2004. в 789 с. в ISBN 5-89158-100-0

[0] в‘ 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.

[1]

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

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

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

[править] Литература

Личные инструменты

Пространства имён

Варианты

Просмотры

Действия

Поиск

Навигация

Участие

Печать/экспорт

Инструменты

На других языках