| dbpprop:abstract
|
- In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general. In programming language theory, a branch of computer science, type theory can refer to the design, analysis and study of type systems, although some computer scientists limit the term's meaning to the study of abstract formalisms such as typed λ-calculi. Bertrand Russell invented the first type theory in response to his discovery that Gottlob Frege's version of naive set theory was afflicted with Russell's paradox. This type theory features prominently in Whitehead and Russell's Principia Mathematica. It avoids Russell's paradox by first creating a hierarchy of types, then assigning each mathematical (and possibly other) entity to a type. Objects of a given type are built exclusively from objects of preceding types (those lower in the hierarchy), thus preventing loops. Alonzo Church, inventor of the lambda calculus, developed a higher-order logic commonly called Church's Theory of Types, in order to avoid the Kleene–Rosser paradox afflicting the original pure lambda calculus. Church's type theory is a variant of the lambda calculus in which expressions (also called formulas or λ-terms) are classified into types, and the types of expressions restrict the ways in which they can be combined. In other words, it is a typed lambda calculus. Today many other such calculi are in use, including Per Martin-Löf's Intuitionistic type theory, Jean-Yves Girard's System F and the Calculus of Constructions. In typed lambda calculi, types play a role similar to that of sets in set theory.
- Die Typentheorie ist eine von Bertrand Russell entwickelte Form der Mengenlehre, mit der er unter anderem versuchte, die von ihm entdeckte Russellsche Antinomie und andere Widersprüche der naiven Mengenlehre zu beheben. Nach dieser Theorie gibt es einfache Mengen, die nur Urelemente, aber keine Mengen als Elemente enthalten können; Mengen des zweiten Typs können zusätzlich einfache Mengen enthalten, Mengen des dritten Typs zusätzlich Mengen des zweiten Typs usw. Mengen haben also einen höheren Typ als ihre Elemente. Dieses System beruht somit auf einer Stratifikation des Mengenbegriffs und vermeidet dadurch die Russellsche Antinomie, da die Darstellung der Menge aller sich nicht selbst enthaltenden Mengen schon aus syntaktischen Gründen nicht möglich ist, denn die dazu nötigen Aussagen <math>x\in x</math> und <math>x\notin x</math> sind syntaktisch nicht korrekt. Die erste einfache Version der Typentheorie formulierte Russell 1903 im Anhang seiner Principles of Mathematics, die zweite komplexere Version 1908 in Mathematical Logic as based on the Theory of Types. Letztere wurde die Grundlage der berühmten Principia Mathematica, die er nach beinahe zehnjähriger Vorbereitungszeit zusammen mit Alfred North Whitehead ab 1910 veröffentlichte. Die einfache Typentheorie wird seit Ramsey auch Simplified Theory of Types (STT) genannt; sie ist hinreichend zur Vermeidung der logischen Paradoxien wie der Russellschen Antinomie, aber nicht für die Lösung der semantischen Paradoxien wie der Grelling-Nelson-Antinomie; dies vermag erst seine signifikant kompliziertere Version von 1908, die Ramified Theory of Types (RTT), die „verzweigte“ Typentheorie. Diese Version der Typentheorie setzte sich wegen ihrer Kompliziertheit und eingeschränkten Leistungsfähigkeit nicht auf Dauer durch. Als bequemer und leistungsfähiger erwies sich die von Ernst Zermelo 1907 entwickelte axiomatische Mengenlehre, die Abraham Fraenkel 1922 erweiterte und die heute als Zermelo-Fraenkel-Mengenlehre bekannt und als Basis der Mathematik weitgehend anerkannt ist. Eine vereinfachte Variante der Typentheorie entwarf Quine 1937 in seinen New Foundations. Typtheorien spielen eine wichtige Rolle in der Theorie der Programmiersprache und in darauf basierenden Programmiersprachen wie Haskell und ML, sowie in computergestützten Beweissystemen wie Coq und Agda (dependent types).
- La théorie des types est une branche de la logique mathématique qui a pour principales caractéristiques que tout objet (terme, fonction, ensemble) y a un type et que les entités ne peuvent se combiner qu'en respectant des règles de "typage". Une première théorie des types (dite "ramifiée") a été créée par Bertrand Russell pour résoudre les paradoxes logiques, comme celui du menteur et ceux de la théorie des ensembles; lourde d'emploi, elle a d'abord été simplifiée et ensuite supplantée par les théories de Zermelo-Frankel et NF de Quine, et aussi reconsidérée pour des objets plus élémentaires après la découverte du lambda-calcul et de la logique combinatoire. Dans ces derniers cas, les entités mathématiques sont construites à l'aide de fonctions, où chaque fonction a un type qui décrit le type de ses arguments et le type de la valeur retournée. Les entités sont bien formées lorsque les fonctions sont appliquées à des entités ayant le type que la fonction attend. Le concept de type a plusieurs domaines d'applications : les théories des ensembles qui, suivant l'intuition de Russell, classent les ensembles en différents types, la logique pour laquelle on cherche à donner un contenu calculatoire aux propositions et aux démonstrations par la correspondance de Curry Howard, les langages de programmation, surtout les langages fonctionnels typés, les systèmes de démonstration sur ordinateur, la linguistique, à travers le concept de catégorie syntaxique.
- Dal punto di vista più generale, la teoria dei tipi è la branca della matematica e della logica che si occupa di classificare generiche entità, raggruppandole in collezioni chiamate tipi. Sotto questo punto di vista vi sono punti di contatto con la nozione di tipo della metafisica. La moderna formulazione della teoria dei tipi è, in parte, nata dal tentativo di dare una risposta al cosiddetto Paradosso di Russell, ed è estesamente trattata nei Principia Mathematica di Russell e Whitehead. Con la diffusione di computer sempre più potenti e l'introduzione di linguaggi di programmazione per lo sviluppo di programmi da installare su di essi, la teoria dei tipi ha trovato un significativo campo di applicazione, soprattutto nell'ambito della progettazione degli stessi linguaggi di programmazione. In questo contesto esistono diverse definizioni applicabili ad un sistema di tipi, ma la seguente, dovuta a Benjamin C. Pierce è probabilmente quella che raccoglie il maggiore consenso: "Un sistema di tipi è un metodo sintattico modificabile, in grado di dimostrare l'assenza di determinati comportamenti nei programmi mediante la classificazione di espressioni fatta in base alla natura dei valori sottoposti ad elaborazione. " (Types and Programming Languages, MIT Press, 2002) In altre parole, un sistema di tipi divide i valori manipolati dai programmi in insiemi chiamati tipi - eseguendo un'operazione chiamata assegnazione del tipo o tipizzazione - e fa sì che certi determinati comportamenti del programma siano, o non siano, possibili in base al tipo dei valori coinvolti in questi comportamenti. Per esempio, supponiamo che un sistema di tipi classifichi il valore ciao come stringa ed il valore 5 come intero e, sulla base di tali diverse assegnazioni, proibisca al programmatore di sommare ciao a 5. All'interno di questo sistema, l'istruzione di programma: ciao + 5 sarebbe illegale. Il vantaggio di questa proibizione, ovvero dell'impossibilità di far eseguire al programma questa operazione, consiste nel fatto che non potrà mai capitare di sommare stringhe a numeri, operazione che produrrebbe risultati privi di senso. La progettazione e l'implementazione di un sistema di tipi è un argomento vasto e complesso, quasi come lo stesso linguaggio di programmazione che lo utilizza. Gli ideatori e gli studiosi dei sistemi di tipi si spingono ad effermare che si tratta dell'essenza stessa del linguaggio: "Progettate correttamente il sistema dei tipi e vedrete che il linguaggio si progetterà da sè!" È importante notare che la trattazione fin qui fatta si riferisce ai tipi statici: I sistemi di tipi ed i linguaggi che fanno uso di tipi dinamici non sono in grado di verificare a priori che un programma faccia un uso corretto dei valori, e quindi generano un errore ogni volta che il programma si comporta in modo da farne un uso scorretto. Per questa ragione, secondo alcuni, la definizione "tipo dinamico" è intrinsecamente poco appropriata. Comunque, in molti linguaggi orientati agli oggetti che fanno uso di tipi dinamici, un tipo è qualcosa di più di un interfaccia e, finché le classi condividono interfacce, non è necessario preoccuparsi di sapere a quale classe appartiene un dato oggetto.
- 型理論（英: Type theory）は、数学や論理学の一分野であり、「型」の階層を構築し、それぞれの型に数学的（あるいはそれ以外の）実体を割り当てるものである。階型理論（Theory of Types）とも。ある型のオブジェクトはその前提となる型のオブジェクトから構築される。この場合の「型」とは形而上的な意味での「型」である。バートランド・ラッセルは、彼が発見したラッセルのパラドックスにより素朴集合論の問題が明らかにされたことを受けて、型理論を構築した。型理論の詳細はホワイトヘッドとラッセルの 『数学原理』にある。 計算機科学の一分野であるプログラミング言語理論では、型理論が型システムの設計・分析・研究の形式的基盤となっている。実際、多くの計算機科学者がプログラミング言語の型システムの形式的研究を「型理論」と呼ぶが、一部の計算機科学者は型付きラムダ計算などの抽象的形式主義の研究だけを指す。
- In de wiskunde, de logica en de informatica is de typentheorie een van de formele systemen die als alternatief kunnen dienen voor de naïeve verzamelingenleer of voor de studie van formele systemen in het algemeen. In de programmeertaaltheorie, een deelgebied van de informatica, kan de typentheorie verwijzen naar het ontwerp, de analyse en de studie van type systemen, hoewel sommige informatici de betekenis van de term beperken tot de abstracte formele systemen, zoals de getypeerde lambda calculus.
- No sentido mais lato, a teoria dos tipos é o ramo da matemática e da lógica que se preocupa com a classificação de entidades em conjuntos chamados tipos. Neste sentido, está relacionada com a noção metafísica de "tipo". A teoria dos tipos moderna foi inventada em parte em resposta ao paradoxo de Russell, e é muito usada em Principia Mathematica, de Russell e Whitehead. Com o surgimento de poderosos computadores programáveis, e o desenvolvimento de linguagens de programação para os mesmos, Teoria dos Tipos tem encontrado aplicação prática no desenvolvimento de sistemas de tipos de linguagens de programação. Definições de "sistemas de tipos" no contexto de linguagens de programação varia, mas a seguinte definição dada por Benjamin C. Pierce corresponde, aproximadamente, ao consenso corrente na comunidade de Teoria dos Tipos: [Um sistema de tipos é um] método sintático tratável para provar a isenção de certos comportamentos em um programa através da classificação de frases de acordo com as espécies de valores que elas computam. (Types and Programming Languages, MIT Press, 2002) Em outras palavras, um sistema de tipos divide os valores de um programa em conjuntos chamados tipos (isso é o que é denominado uma "atribuição de tipos"), e torna certos comportamentos do programa ilegais com base nos tipos que são atribuídos neste processo. Por exemplo, um sistema de tipos pode classificar o valor "hello" como uma cadeia de caracteres e o valor 5 como um número, e proibir o programador de tentar adicionar "hello" a 5, com base nessa atribuição de tipos. Neste sistema de tipos, o programa "hello" + 5 seria ilegal. Assim, qualquer programa permitido pelo sistema de tipos seria demonstravelmente livre do comportamento errôneo de tentar adicionar cadeias de caracteres a números. O projeto e a implantação de sistemas de tipos é um tópico quase tão vasto quanto o das próprias linguagens de programação. De fato, os proponentes da teoria dos tipos argumentam que o projeto de sistemas de tipos é a própria essência do projeto de linguagens de programação: "Projete o sistema de tipos corretamente, e a linguagem vai projetar a si mesma". Note que teoria dos tipos, como descrita daqui pra frente, se refere a disciplinas de tipagem estática. Sistemas de programação que aplicam tipagem dinâmica não provam a priori que um programa usa valores corretamente; ao invés disso, elas lançam um erro em tempo de execução quando o programa tenta apresentar algum comportamento que use valores incorretamente. Alguns argumentam que "tipagem dinâmica" é uma terminologia ruim por isso. De qualquer forma, as duas não devem ser confundidas. Principais desenvolvedores Russell e Whitehead Sistema de cálculo de tipo Lambda Inferência de tipo Polimórfica (Linguagem de Programação ML; polimorfismo de Hindley-Milner) subtipo Tipagem estática orientada a objetos (grew out of abstract data type and subtyping) F-bounded polimorfismos e esforços para combinar generics com polimorfismo de orientação a objetos Set-constraint-based type systems module systems Type-driven proof systems (e.g. ELF) ... (muito mais) Impacto prático da teoria dos tipos Linguagem de programação fortemente tipadas Análise e otimização de programas orientadas a tipos Type-aided security mechanisms (e.g. , TAL, Java bytecode verification) Conexões com lógica construtivista Isomorphisms between logical proof systems and type systems Ref: Wadler's "Programs are proofs" Curry-Howard Isomorphism Intuitionistic Type Theory Outros tópicos que podemos querer adicionar aqui A noção de tipos de dados abstratos A relação entre tipos e programação orientada a objeto A relação entre tipos e algoritmos Uma definição formal de tipos de dados abstratos - pré-codição, pós-condição e invariantes http://www. nist. gov/dads/HTML/abstractDataType. html - Abstract (em inglês) http://www. cs. ucsd. edu/users/goguen/ps/beatcs-adj. ps. gz - Um paper sobre o basico de ADTs, e uma boa lista de referencias. As pages 3-4 são as mais relevantes. (arquivo compactado)
- В математике, логике и компьютерных науках теорией типов считается либо какая-либо формальная система, являющаяся альтернативой наивной теории множеств, либо изучение подобных формализмов. Теория типов — математически формализованная база для проектирования, анализа и изучения систем типов данных в теории языков программирования. Многие программисты используют это понятие для обозначения любого аналитического труда, изучающего системы типов в языках программирования. В научных кругах под теорией типов чаще всего понимают более узкий раздел дискретной математики, в частности λ-исчисление с типами. Современная теория типов была частично разработана в процессе разрешения парадокса Рассела и во многом базируется на работе Бертрана Рассела и Альфреда Уайтхеда «Principia Mathematica».
- 在最广泛的层面上，类型论是关注把实体分类到叫做类型的搜集中的数学和逻辑分支。在这种意义上，它与类型的形而上学概念有关。现代类型论在部分上是响应罗素悖论而发明的，并在伯特兰·罗素和阿弗烈·诺夫·怀海德的《数学原理》中起到重要作用。 在计算机科学分支中的编程语言理论中，类型论提供了设计分析和研究类型系统的形式基础。实际上，很多计算机科学家使用术语“类型论”来称呼对编程语言的类型语言的形式研究，尽管有些人把它限制于对更加抽象的形式化如有类型 lambda 演算的研究。
|
| rdfs:comment
|
- In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general. In programming language theory, a branch of computer science, type theory can refer to the design, analysis and study of type systems, although some computer scientists limit the term's meaning to the study of abstract formalisms such as typed λ-calculi.
- Die Typentheorie ist eine von Bertrand Russell entwickelte Form der Mengenlehre, mit der er unter anderem versuchte, die von ihm entdeckte Russellsche Antinomie und andere Widersprüche der naiven Mengenlehre zu beheben. Nach dieser Theorie gibt es einfache Mengen, die nur Urelemente, aber keine Mengen als Elemente enthalten können; Mengen des zweiten Typs können zusätzlich einfache Mengen enthalten, Mengen des dritten Typs zusätzlich Mengen des zweiten Typs usw.
- La théorie des types est une branche de la logique mathématique qui a pour principales caractéristiques que tout objet (terme, fonction, ensemble) y a un type et que les entités ne peuvent se combiner qu'en respectant des règles de "typage".
- Dal punto di vista più generale, la teoria dei tipi è la branca della matematica e della logica che si occupa di classificare generiche entità, raggruppandole in collezioni chiamate tipi. Sotto questo punto di vista vi sono punti di contatto con la nozione di tipo della metafisica. La moderna formulazione della teoria dei tipi è, in parte, nata dal tentativo di dare una risposta al cosiddetto Paradosso di Russell, ed è estesamente trattata nei Principia Mathematica di Russell e Whitehead.
- In de wiskunde, de logica en de informatica is de typentheorie een van de formele systemen die als alternatief kunnen dienen voor de naïeve verzamelingenleer of voor de studie van formele systemen in het algemeen.
- No sentido mais lato, a teoria dos tipos é o ramo da matemática e da lógica que se preocupa com a classificação de entidades em conjuntos chamados tipos. Neste sentido, está relacionada com a noção metafísica de "tipo". A teoria dos tipos moderna foi inventada em parte em resposta ao paradoxo de Russell, e é muito usada em Principia Mathematica, de Russell e Whitehead.
- В математике, логике и компьютерных науках теорией типов считается либо какая-либо формальная система, являющаяся альтернативой наивной теории множеств, либо изучение подобных формализмов.
|
![[RDF Data]](/statics/sw-cube.png)
