Pure type system (original) (raw)
Чиста система типів (система узагальнених типів) - форма типізованого лямбда-числення, яка припускає довільну кількість сортів змінних і залежностей між ними. Розробили незалежно Стефан Берарді (1988) і Ян Терлов (1989). Чисту систему типів можна розглядати як узагальнення лямбда-куба, маючи на увазі, що кожній з його вершин відповідає примірник чистої системи типів з двома сортами змінних (подібний погляд висловлював автор ідеї лямбда-куба Генк Барендрегт).
Property | Value |
---|---|
dbo:abstract | Στους κλάδους της μαθηματικής λογικής γνωστούς ως και θεωρία τύπων, ένα αμιγές σύστημα τύπων (pure type system), παλαιότερα γνωστό ως γενικευμένο σύστημα τύπων, είναι μια μορφή του λ-λογισμού με τύπους που επιτρέπει έναν αυθαίρετο αριθμό από είδη και εξαρτήσεις ανάμεσα σε αυτά. Το πλαίσιο μπορεί να θεωρηθεί σαν μία γενίκευση του του , με την έννοια ότι όλες οι γωνίες του κύβου μπορούν να αναπαρασταθούν σαν στιγμιότυπα του αμιγούς συστήματος τύπων με μόνο δύο είδη. Πράγματι ο Barendregt (1991) σχημάτισε τον κύβο του με αυτήν την ρύθμιση. Τα αμιγή συστήματα τύπων μπορεί να κάνουν δυσδιάκριτη την διαφορά ανάμεσα στου τύπους και στους όρους, η καταρρέει, όπως και στην περίπτωση του , αλλά αυτό δεν είναι η γενική περίπτωση, όπως ο λ-λογισμός με απλούς τύπους που επιτρέπει μόνο στους όρους να εξαρτώνται από τύπους. Τα αμιγή συστήματα τύπων εισήχθησαν ανεξάρτητα από τους Stefano Berardi (1988) και Jan Terlouw (1989). Η περιγράφηκαν για πρώτη φορά ως αμιγή συστήματα τύπων από τον Barendregt. Στην διδακτορική του διατριβή, ο Berardi όρισε ένα κλασικό λογικό κύβο που περιέχει παρόμοιες με τον λάμδα κύβο (αυτές οι προδιαγραφές είναι μη-ανεξαρτώμενες). Μία τροποποίηση αυτού του κύβου ονομάστηκε αργότερα Λ-κύβος από τον Geuvers, o οποίος στην διδακτορική του διατριβή επέκτεινε την σε αυτόν τον σχεδιασμό. Βασισμένος σε αυτές της ιδέες, ο Barthe και άλλοι όρισαν τα κλασικά αμιγή συστήματα τύπων προσθέτοντας έναν τελεστή διπλής άρνησης. Παρόμοια, το 1998, ο Tijn Borghuis εισήγαγε τα τροπικά αμιγή συστήματα τύπων. Ο Roorda συζήτησε την εφαρμογή των αμιγών συστημάτων τύπων στον συναρτησιακό προγραμματισμό; και οι Roorda και Jeuring πρότειναν μία γλώσσα προγραμματισμού βασισμένη στα αμιγή συστήματα τύπων. Τα συστήματα που στηρίζονται στον λ-κύβο είναι . Τα αμιγή συστήματα τύπων σε γενικές γραμμές δεν χρειάζεται να είναι, όπως για παράδειγμα το U από το παράδοξο του Girard δεν είναι. Επιπλέον, όλα τα αμιγή συστήματα τύπων που δεν είναι ισχυρά κανονικοποιήσιμα δεν είναι ούτε (ασθενώς) κανονικοποιήσιμα: περιέχουν εκφράσεις οι οποίες δεν έχουν κανονικές μορφές, ακριβώς όπως ο λαμδα λογισμός χωρίς τύπους. Το αν αυτό είναι πάντα η περίπτωση είναι ένα σημαντικό ανοικτό πρόβλημα στον τομέα αυτό, δηλαδή το αν ένα (ασθενώς) κανονικοποιήσιμο αμιγες σύστημα τύπων είναι πάντα ισχυρά κανονικοποιήσιμο. Αυτό είναι γνωστό ως η εικασία των Barendregt–Geuvers–Klop (από τους Henk Barendregt, Herman Geuvers και Jan Willem Klop). (el) In the branches of mathematical logic known as proof theory and type theory, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of typed lambda calculus that allows an arbitrary number of sorts and dependencies between any of these. The framework can be seen as a generalisation of Barendregt's lambda cube, in the sense that all corners of the cube can be represented as instances of a PTS with just two sorts. In fact, Barendregt (1991) framed his cube in this setting. Pure type systems may obscure the distinction between types and terms and collapse the type hierarchy, as is the case with the calculus of constructions, but this is not generally the case, e.g. the simply typed lambda calculus allows only terms to depend on terms. Pure type systems were independently introduced by Stefano Berardi (1988) and Jan Terlouw (1989). Barendregt discussed them at length in his subsequent papers. In his PhD thesis, Berardi defined a cube of constructive logics akin to the lambda cube (these specifications are non-dependent). A modification of this cube was later called the L-cube by Geuvers, who in his PhD thesis extended the Curry–Howard correspondence to this setting. Based on these ideas, Barthe and others defined classical pure type systems (CPTS) by adding a double negation operator. Similarly, in 1998, Tijn Borghuis introduced modal pure type systems (MPTS). Roorda has discussed the application of pure type systems to functional programming; and Roorda and Jeuring have proposed a programming language based on pure type systems. The systems from the lambda cube are all known to be strongly normalizing. Pure type systems in general need not be, for example System U from Girard's paradox is not. (Roughly speaking, Girard found pure systems in which one can express the sentence "the types form a type".) Furthermore, all known examples of pure type systems that are not strongly normalizing are not even (weakly) normalizing: they contain expressions that do not have normal forms, just like the untyped lambda calculus. It is a major open problem in the field whether this is always the case, i.e. whether a (weakly) normalizing PTS always has the strong normalization property. This is known as the Barendregt–Geuvers–Klop conjecture (named after Henk Barendregt, , and Jan Willem Klop). (en) Чиста система типів (система узагальнених типів) - форма типізованого лямбда-числення, яка припускає довільну кількість сортів змінних і залежностей між ними. Розробили незалежно Стефан Берарді (1988) і Ян Терлов (1989). Чисту систему типів можна розглядати як узагальнення лямбда-куба, маючи на увазі, що кожній з його вершин відповідає примірник чистої системи типів з двома сортами змінних (подібний погляд висловлював автор ідеї лямбда-куба Генк Барендрегт). (uk) Чистая система типов (система обобщенных типов) — форма типизированного лямбда-исчисления, допускающая произвольное количество сортов переменных и зависимостей между ними. Разработана независимо Стефано Берарди (1988) и Яном Терловым (1989). Чистую систему типов можно рассматривать как обобщение лямбда-куба, подразумевая, что каждой из его вершин соответствует экземпляр чистой системы типов с двумя сортами переменных (подобный взгляд высказывал автор идеи лямбда-куба Барендрегт). (ru) |
dbo:wikiPageExternalLink | http://www.rbjones.com/rbjpub/logic/cl/tlc004.htm https://books.google.com/books%3Fid=Ax2QXEwXhzQC&pg=PA255 |
dbo:wikiPageID | 17870536 (xsd:integer) |
dbo:wikiPageLength | 9184 (xsd:nonNegativeInteger) |
dbo:wikiPageRevisionID | 1101031121 (xsd:integer) |
dbo:wikiPageWikiLink | dbr:Typed_lambda_calculus dbc:Lambda_calculus dbr:Double_negation dbc:Proof_theory dbr:Mathematical_logic dbr:Normal_form_(abstract_rewriting) dbr:Normalization_property_(abstract_rewriting) dbr:Calculus_of_constructions dbr:Simply_typed_lambda_calculus dbr:Functional_programming dbr:Henk_Barendregt dbr:Structure_(mathematical_logic) dbr:Type_theory dbr:Lambda-mu_calculus dbr:Lambda_cube dbr:Curry–Howard_correspondence dbr:Proof_theory dbr:Jan_Willem_Klop dbr:Jean-Yves_Girard dbc:Type_theory dbr:System_U dbr:Type_hierarchy dbr:Strongly_normalizing dbr:Constructive_logic dbr:Herman_Geuvers |
dbp:id | pure+type+system (en) |
dbp:title | Pure type system (en) |
dbp:wikiPageUsesTemplate | dbt:Cite_techreport dbt:Citation_needed dbt:Cite_book dbt:Cite_document dbt:Cite_web dbt:Nlab dbt:Refbegin dbt:Refend dbt:Reflist dbt:Unsolved |
dcterms:subject | dbc:Lambda_calculus dbc:Proof_theory dbc:Type_theory |
gold:hypernym | dbr:Form |
rdf:type | yago:WikicatConjectures yago:WikicatUnsolvedProblemsInComputerScience yago:Abstraction100002137 yago:Attribute100024264 yago:Cognition100023271 yago:Concept105835747 yago:Condition113920835 yago:Content105809192 yago:Difficulty114408086 yago:Hypothesis105888929 yago:Idea105833840 yago:Problem114410605 yago:PsychologicalFeature100023100 yago:Speculation105891783 yago:State100024720 |
rdfs:comment | Чиста система типів (система узагальнених типів) - форма типізованого лямбда-числення, яка припускає довільну кількість сортів змінних і залежностей між ними. Розробили незалежно Стефан Берарді (1988) і Ян Терлов (1989). Чисту систему типів можна розглядати як узагальнення лямбда-куба, маючи на увазі, що кожній з його вершин відповідає примірник чистої системи типів з двома сортами змінних (подібний погляд висловлював автор ідеї лямбда-куба Генк Барендрегт). (uk) Чистая система типов (система обобщенных типов) — форма типизированного лямбда-исчисления, допускающая произвольное количество сортов переменных и зависимостей между ними. Разработана независимо Стефано Берарди (1988) и Яном Терловым (1989). Чистую систему типов можно рассматривать как обобщение лямбда-куба, подразумевая, что каждой из его вершин соответствует экземпляр чистой системы типов с двумя сортами переменных (подобный взгляд высказывал автор идеи лямбда-куба Барендрегт). (ru) Στους κλάδους της μαθηματικής λογικής γνωστούς ως και θεωρία τύπων, ένα αμιγές σύστημα τύπων (pure type system), παλαιότερα γνωστό ως γενικευμένο σύστημα τύπων, είναι μια μορφή του λ-λογισμού με τύπους που επιτρέπει έναν αυθαίρετο αριθμό από είδη και εξαρτήσεις ανάμεσα σε αυτά. Το πλαίσιο μπορεί να θεωρηθεί σαν μία γενίκευση του του , με την έννοια ότι όλες οι γωνίες του κύβου μπορούν να αναπαρασταθούν σαν στιγμιότυπα του αμιγούς συστήματος τύπων με μόνο δύο είδη. Πράγματι ο Barendregt (1991) σχημάτισε τον κύβο του με αυτήν την ρύθμιση. Τα αμιγή συστήματα τύπων μπορεί να κάνουν δυσδιάκριτη την διαφορά ανάμεσα στου τύπους και στους όρους, η καταρρέει, όπως και στην περίπτωση του , αλλά αυτό δεν είναι η γενική περίπτωση, όπως ο λ-λογισμός με απλούς τύπους που επιτρέπει μόνο στους όρους να (el) In the branches of mathematical logic known as proof theory and type theory, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of typed lambda calculus that allows an arbitrary number of sorts and dependencies between any of these. The framework can be seen as a generalisation of Barendregt's lambda cube, in the sense that all corners of the cube can be represented as instances of a PTS with just two sorts. In fact, Barendregt (1991) framed his cube in this setting. Pure type systems may obscure the distinction between types and terms and collapse the type hierarchy, as is the case with the calculus of constructions, but this is not generally the case, e.g. the simply typed lambda calculus allows only terms to depend on terms. (en) |
rdfs:label | Αμιγές σύστημα τύπων (el) Pure type system (en) Чистая система типов (ru) Чиста система типів (uk) |
owl:sameAs | freebase:Pure type system wikidata:Pure type system dbpedia-el:Pure type system dbpedia-ru:Pure type system dbpedia-uk:Pure type system https://global.dbpedia.org/id/4tmZh |
prov:wasDerivedFrom | wikipedia-en:Pure_type_system?oldid=1101031121&ns=0 |
foaf:isPrimaryTopicOf | wikipedia-en:Pure_type_system |
is dbo:wikiPageDisambiguates of | dbr:PTS |
is dbo:wikiPageRedirects of | dbr:L-cube dbr:Barendregt–Geuvers–Klop_conjecture dbr:Barendregt-Geuvers-Klop_conjecture dbr:Pure_type_systems dbr:Generalized_type_system |
is dbo:wikiPageWikiLink of | dbr:Typed_lambda_calculus dbr:Dependent_type dbr:De_Bruijn_notation dbr:Nuprl dbr:L-cube dbr:Calculus_of_constructions dbr:PTS dbr:Type_theory dbr:Lambda-mu_calculus dbr:Lambda_cube dbr:Barendregt–Geuvers–Klop_conjecture dbr:Kind_(type_theory) dbr:Lambda_calculus dbr:System_U dbr:Barendregt-Geuvers-Klop_conjecture dbr:Pure_type_systems dbr:Generalized_type_system |
is foaf:primaryTopic of | wikipedia-en:Pure_type_system |