Чистая система типов: различия между версиями
Перейти к навигации
Перейти к поиску
| [отпатрулированная версия] | [отпатрулированная версия] |
Содержимое удалено Содержимое добавлено
Pilot Ang (обсуждение | вклад) Нет описания правки |
Pilot Ang (обсуждение | вклад) источники |
||
| Строка 1: | Строка 1: | ||
{{редактирую | user=[[Служебная:Contributions/Pilot Ang|Pilot Ang]] | date=27 сентября 2020 }} |
{{редактирую | user=[[Служебная:Contributions/Pilot Ang|Pilot Ang]] | date=27 сентября 2020 }} |
||
В разделах [[Математическая логика|математической логики]], известных как [[теория доказательств]] и [[теория типов]], система чистых типов ('''pure type system, PTS'''), ранее известная как система обобщенных типов ('''generalized type system, GTS'''), представляет собой форму [[Типизированное лямбда-исчисление|типизированного лямбда-исчисления]], которая допускает произвольное количество сортов переменных и зависимостей между ними. Чистую систему типов можно рассматривать как обобщение [[Лямбда-куб|лямбда-куба]], подразумевая, что каждому из углов лямбда-куба соответствует экземпляр PTS с двумя сортами переменных. |
В разделах [[Математическая логика|математической логики]], известных как [[теория доказательств]] и [[теория типов]], система чистых типов ('''pure type system, PTS'''), ранее известная как система обобщенных типов ('''generalized type system, GTS'''), представляет собой форму [[Типизированное лямбда-исчисление|типизированного лямбда-исчисления]], которая допускает произвольное количество сортов переменных и зависимостей между ними. Чистую систему типов можно рассматривать как обобщение [[Лямбда-куб|лямбда-куба]], подразумевая, что каждому из углов лямбда-куба соответствует экземпляр теории PTS с двумя сортами переменных<ref>{{Книга|ссылка=https://www.worldcat.org/oclc/51958338|автор=Pierce, Benjamin C.|заглавие=Types and programming languages|год=2002|место=Cambridge, Mass.|издательство=MIT Press|страниц=1 online resource (xxi, 623 pages)|isbn=0-585-44269-X, 978-0-585-44269-3, 0-262-25681-9, 978-0-262-25681-0, 9786612096693, 6612096691, 1-282-09669-9, 978-1-282-09669-1, 0-262-30382-5, 978-0-262-30382-8}}</ref><ref>{{Книга|ссылка=https://www.worldcat.org/oclc/57468759|автор=Kamareddine, Fairouz D.|заглавие=A modern perspective on type theory : from its origins until today|год=2004|место=Dordrecht|издательство=Kluwer Academic Publishers|страниц=1 online resource (xiv, 357 pages)|isbn=1-4020-2334-0, 978-1-4020-2334-7, 1-4020-2335-9, 978-1-4020-2335-4}}</ref>. |
||
[[Категория:Теория типов]] |
[[Категория:Теория типов]] |
||
Версия от 01:17, 27 сентября 2020
 | Эту страницу в данный момент активно редактирует участник Pilot Ang. |
В разделах математической логики, известных как теория доказательств и теория типов, система чистых типов (pure type system, PTS), ранее известная как система обобщенных типов (generalized type system, GTS), представляет собой форму типизированного лямбда-исчисления, которая допускает произвольное количество сортов переменных и зависимостей между ними. Чистую систему типов можно рассматривать как обобщение лямбда-куба, подразумевая, что каждому из углов лямбда-куба соответствует экземпляр теории PTS с двумя сортами переменных[1][2].
- ↑ Pierce, Benjamin C. Types and programming languages. — Cambridge, Mass.: MIT Press, 2002. — 1 online resource (xxi, 623 pages) с. — ISBN 0-585-44269-X, 978-0-585-44269-3, 0-262-25681-9, 978-0-262-25681-0, 9786612096693, 6612096691, 1-282-09669-9, 978-1-282-09669-1, 0-262-30382-5, 978-0-262-30382-8.
- ↑ Kamareddine, Fairouz D. A modern perspective on type theory : from its origins until today. — Dordrecht: Kluwer Academic Publishers, 2004. — 1 online resource (xiv, 357 pages) с. — ISBN 1-4020-2334-0, 978-1-4020-2334-7, 1-4020-2335-9, 978-1-4020-2335-4.