Типизированное лямбда-исчисление: различия между версиями
| [отпатрулированная версия] | [отпатрулированная версия] |
Addbot (обсуждение | вклад) м Перемещение 7 интервики на Викиданные, d:q2607208 |
РоманСузи (обсуждение | вклад) неясно, как использовано в статье |
||
| Строка 1: | Строка 1: | ||
'''Типизированное лямбда-исчисление''' |
'''Типизированное лямбда-исчисление''' — это версия [[лямбда-исчисление|лямбда-исчисления]], в которой лямбда-термам приписываются специальные синтаксические метки, называемые типами. Допустимы различные наборы правил конструирования и приписывания таких меток, они порождают различные системы типизации. |
||
Типовые λ-исчисления являются фундаментальными примитивными [[язык программирования|языками программирования]], которые обеспечивают основу типовым [[функциональный язык программирования|языкам функционального программирования]] |
Типовые λ-исчисления являются фундаментальными примитивными [[язык программирования|языками программирования]], которые обеспечивают основу типовым [[функциональный язык программирования|языкам функционального программирования]] — [[аппликативный подход к программированию|аппликативным языкам]], — среди которых [[ML]] и [[Haskell]], а также типовым императивным языкам программирования. |
||
λ-исчисление с типами является языком [[декартово-замкнутая категория|декартово-замкнутой категории]], что устанавливает прямую связь с такой [[модели вычислений|моделью вычислений]], как [[категориальная абстрактная машина]]. С одной точки зрения типовые λ-исчисления могут рассматриваться как специализации [[лямбда-исчисление|бестиповых λ-исчислений]], а с другой |
λ-исчисление с типами является языком [[декартово-замкнутая категория|декартово-замкнутой категории]], что устанавливает прямую связь с такой [[модели вычислений|моделью вычислений]], как [[категориальная абстрактная машина]]. С одной точки зрения типовые λ-исчисления могут рассматриваться как специализации [[лямбда-исчисление|бестиповых λ-исчислений]], а с другой — наоборот, типовые языки могут считаться более фундаментальными, из которых бестиповые получаются как частные случаи. Анализ этого явления дает [[теория вычислений]] [[Скотт, Дана Стюарт|Д. Скотта]]<ref>''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.</ref>. |
||
λ-исчисление с типами служит основой для разработки новых [[системы типизации|систем типизации]] для языков программирования, поскольку именно средствами типов и зависимостей между ними выражаются желаемые свойства программ. |
λ-исчисление с типами служит основой для разработки новых [[системы типизации|систем типизации]] для языков программирования, поскольку именно средствами типов и зависимостей между ними выражаются желаемые свойства программ. |
||
| Строка 16: | Строка 16: | ||
== Примечания == |
== Примечания == |
||
{{примечания}} |
|||
<references/> |
|||
== Литература == |
== Литература == |
||
* ''Friedman H.'' Equality between functionals. LogicColl. '73, pages 22-37, LNM 453, 1975. |
* ''Friedman H.'' Equality between functionals. LogicColl. '73, pages 22-37, LNM 453, 1975. |
||
* ''Barendregt H.'' [ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps Lambda Calculi with Types], Handbook of Logic in Computer Science, Volume II, Oxford University Press. |
* ''Barendregt H.'' [ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps Lambda Calculi with Types], Handbook of Logic in Computer Science, Volume II, Oxford University Press. |
||
* {{книга |
|||
|автор = Вольфенгаген В. Э. |
|||
|заглавие = Методы и средства вычислений с объектами. Аппликативные вычислительные системы |
|||
|серия = |
|||
|ссылка = |
|||
|издание = |
|||
|место = М. |
|||
|издательство = JurInfoR Ltd., АО «Центр ЮрИнфоР» |
|||
|год = 2004 |
|||
|том = |
|||
|страниц = 789 |
|||
|isbn = 5-89158-100-0 |
|||
}} |
|||
[[Категория:Лямбда-исчисление]] |
[[Категория:Лямбда-исчисление]] |
||
Версия от 14:19, 23 ноября 2014
Типизированное лямбда-исчисление — это версия лямбда-исчисления, в которой лямбда-термам приписываются специальные синтаксические метки, называемые типами. Допустимы различные наборы правил конструирования и приписывания таких меток, они порождают различные системы типизации.
Типовые λ-исчисления являются фундаментальными примитивными языками программирования, которые обеспечивают основу типовым языкам функционального программирования — аппликативным языкам, — среди которых ML и Haskell, а также типовым императивным языкам программирования.
λ-исчисление с типами является языком декартово-замкнутой категории, что устанавливает прямую связь с такой моделью вычислений, как категориальная абстрактная машина. С одной точки зрения типовые λ-исчисления могут рассматриваться как специализации бестиповых λ-исчислений, а с другой — наоборот, типовые языки могут считаться более фундаментальными, из которых бестиповые получаются как частные случаи. Анализ этого явления дает теория вычислений Д. Скотта[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.