| dbo:abstract
|
- نظرية النمط أو التنويع (بالإنجليزية: Type theory) في الرياضيات، المنطق والمعلوماتية هي أي نظام شكلي بإمكانه القيام مكان ، أو دراسة التشكيل بشكل عام، وهي أيضاً منهج لبناء المنطق الصوري توضع بواسطته تفرقة بين الموضوعات ذات المستويات المختلفة (الأنماط)، ويهدف هذا المنهج إلى استبعاد المفارقات أو التناقضات من المنطق ونظرية الأعداد وكان أول من وضع نظرية الأنماط، وطبقها على منطق الفئات (1890)، وفي الأعوام 1908 - 1910 بنى برتراند راسل نسقاً تفصيلياً من نظرية الأنماط وطبقة على أساس التفرقة (طبقاً للأنماط)بين :
* الافراد (نمط 1)
* الصفات (نمط 2)
* صفات الصفات (نمط 3) وكذلك أدخل راسل تقسيم الأنماط إلى رتب، وليست نظرية النمط سوى واحدة من المناهج لإزالة التناقضات عن الأبنية في والمنطق الصوري وصاغ بيرتراند راسل نظرية النمط وكان ذلك بسبب اكتشافه تعارضا paradoxon في نظرية المجموعات البسيطة سمية بمفارقة راسل. تعريف النمط: هو أساس تكرار قيمة، إما بالشكل أو بالأرقام. (ar)
- V matematice se logika vyššího řádu odlišuje od predikátové logiky prvního řádu několika způsoby. Jeden z nich je typ , přes které se kvantifikuje; v logice prvního řádu se kvantifikuje pouze pro proměnné pro individua a nelze kvantifikovat (volně řečeno) přes proměnné pro predikátové symboly. To lze v a dalších systémech. Další vlastnost, kterou se logika vyššího řádu liší od logiky prvního řádu, jsou dovolené konstrukce v typové teorii, na které je (případně) založena. Predikát vyššího řádu je takový predikát, který má jeden nebo víc jiných predikátů jako argumenty. Obecně, predikát vyššího řádu, který má řád n, má jeden nebo víc predikátů řádu (n − 1) jako svoje argumenty (pro n > 1). Podobnou vlastnost mají funkce vyšších řádů, běžně využívané ve funkcionálním programování Logiky vyšších řádů mají větší vyjadřovací sílu, ale kvůli svým vlastnostem, zvláště vzhledem k teorii modelů, mají méně vhodné chování pro mnoho aplikací. Gödel dokázal, že klasická logika vyššího řádu nedovoluje (rekurzivně ) korektní a úplný . Ale existuje takový důkazový systém, který je korektní a úplný vzhledem k Henkinovým modelům. Příklady logik vyšších řádů jsou Churchova jednoduchá teorie typů (angl. 'Simple Theory of Types') a (angl. 'calculus of constructions'). (cs)
- Teorie typů je teorie na pomezí matematiky, filosofie a , kterou jako první předložil Bertrand Russell za účelem vyřešení paradoxů teorie množin, ačkoliv zárodky lze najít již u Bernarda Bolzana. Nejjednodušším příkladem použití je typovaný lambda kalkul. V teorie typů existuje univerzum typů a jejich hodnot, přičemž každá proměnná má určený typ, například ve formuli . Teorie typů hraje důležitou roli v Henkinově důkazu faktu, že každá bezesporná teorie vyššího řádu má obecný model.Hintikka o několik let později dokázal, že každá teorie libovolně velkého konečného řádu je sémanticky ekvivalentní odpovídající reifikované teorii druhého řádu, tedy přechodem na vyšší řád nezískáme silnější logický systém. Existují různá rozšíření původní Russellovy teorie typů, například obsahující závislostní typy. Algebraické datové typy tvoří algebru, která je polookruhem. (cs)
- In mathematischer Logik und theoretischer Informatik sind Typentheorien formale Systeme, in denen jeder Term einen Typ hat und Operationen auf bestimmte Typen beschränkt sind. Einige Typentheorien werden als Alternative zur axiomatischen Mengenlehre als Grundlage für die moderne Mathematik benutzt. Typentheorien haben Überschneidungen mit Typsystemen, die ein Merkmal von Programmiersprachen zur Fehlervermeidung darstellen. Zwei populäre Typentheorien, die als mathematische Grundlagen genutzt werden, sind Alonzo Churchs typisierter Lambda-Kalkül und Per Martin-Löfs . (de)
- Στα Μαθηματικά, στη Λογική και στη Επιστήμη των Υπολογιστών, η Θεωρία Τύπων είναι ένα από τα τα οποία χρησιμοποιούνται στην , ή στη μελέτη τέτοιων φορμαλισμών γενικότερα. Στη Θεωρία των Γλωσσών Προγραμματισμού, ενός κλάδου της Επιστήμης των Υπολογιστών, η Θεωρία Τύπων μπορεί να αναφέρεται στο σχεδιασμό, στην ανάλυση και στη μελέτη των Συστημάτων Τύπων, παρόλο που κάποιοι επιστήμονες της Πληροφορικής περιορίζουν τη σημασία του όρου στη μελέτη των αφηρημένων φορμαλισμών όπως ο λ-λογισμός με τύπους. Ο Μπέρτραντ Ράσελ εφηύρε την πρώτη θεωρία τύπων μετά την ανακάλυψή του πως η εκδοχή της του Γκότλομπ Φρέγκε υπόκειντο στο Παράδοξο του Ράσελ. Αυτή η θεωρία τύπων βρίσκεται σε περίοπτη θέση στο των Άλφρεντ Νορθ Γουάιτχεντ και Ράσελ. Αποφεύγει το Παράδοξο του Ράσελ με το να δημιουργεί πρώτα μία ιεραρχία τύπων, και κατόπιν να αναθέτει κάθε μαθηματική (και πιθανώς άλλη) οντότητα σε έναν τύπο. Τα αντικείμενα ενός δοσμένου τύπου δημιουργούνται αποκλειστικά από αντικείμενα προηγούμενων τύπων (αυτών που είναι χαμηλότερα στην ιεραρχία), αποφεύγοντας έτσι τις επαναλήψεις. Ο , εφευρέτης του λ-λογισμού, ανέπτυξε μια Λογική Υψηλής Τάξης γνωστότερη ως Θεωρία Τύπων του Τσερτς, με σκοπό να αποφύγει το Παράδοξο Κλέινι-Ρόσερ που ταλαιπωρούσε τον αρχικό αμιγή λ-λογισμό. Η θεωρία τύπων του Τσερτς είναι μια παραλλαγή του λ-λογισμού στην οποία οι εκφράσεις (που επίσης καλούνται φόρμουλες ή λ-όροι) κατηγοριοποιούνται σε τύπους, και οι τύποι των εκφράσεων περιορίζουν τους τρόπους με τους οποίους μπορούν να συνδυαστούν. Με άλλα λόγια, είναι ένας λ-λογισμός με τύπους. Το άρθρο Η Θεωρία Τύπων του Church στην Εγκυκλοπαίδεια την Φιλοσοφίας του Στάνφορντ είναι αφιερωμένο σε αυτό το θέμα. Σήμερα χρησιμοποιούνται πολλοί άλλοι παρόμοιοι λογισμοί, συμπεριλαμβανομένης της του , του Συστήματος F του και του . Στον λ-λογισμό με τύπους, οι τύποι παίζουν ένα ρόλο παρόμοιο με αυτό των συνόλων στη Θεωρία Συνόλων. (el)
- Στα μαθηματικά και τη λογική, μία λογική ανώτερου βαθμού ή λογική ανώτερης τάξης (higher-order logic) διακρίνεται από μία λογική πρώτου βαθμού με βάση αρκετά χαρακτηριστικά. Ένα από αυτά είναι ο τύπος των μεταβλητών που εμφανίζονται στους ποσοδείκτες: γενικά, στην πρωτοβάθμια λογική, απαγορεύεται οι ποσοδείκτες να αναφέρονται σε κατηγορήματα, ενώ αυτό επιτρέπεται στη . Η λογική ανώτερου βαθμού διαφέρει επίσης από τη λογική πρώτου βαθμού στις δομές που η θεωρία τύπων της επιτρέπει να κατασκευάζονται. Ένα κατηγόρημα ανώτερου βαθμού είναι ένα κατηγόρημα που δέχεται σαν παραμέτρους κατηγορήματα. Γενικά, ένα κατηγόρημα βαθμού n παίρνει ένα ή περισσότερα κατηγορήματα βαθμού n − 1 σαν παραμέτρους, όπου n > 1. Παρόμοια ισχύουν και για τις συναρτήσεις ανώτερης τάξης. Ο όρος λογική ανώτερης τάξης (Higher-order logic, συντομογραφία HOL), συχνά χρησιμοποιείται για απλές λογικές κατηγορημάτων ανώτερου βαθμού, δηλαδή λογικές των οποίων η θεωρία τύπων είναι απλή, όχι πολυμορφική ή με εξαρτώμενους τύπους. Οι λογικές ανώτερου βαθμού είναι πιο εκφραστικές, αλλά οι ιδιότητές τους, ειδικά όσον αφορά τη θεωρία μοντέλων, τις κάνουν δυσκολότερες στο χειρισμό για πολλές εφαρμογές. Λόγω ενός αποτελέσματος του Γκέντελ, η κλασική λογική ανώτερου βαθμού δεν επιδέχεται ενός (αναδρομικού και αξιωματικού) λογισμού αποδείξεων που να είναι συνεπής (sound) και πλήρης (complete) - ένας τέτοιος λογισμός όμως υπάρχει και είναι συνεπής και πλήρης όσον αφορά τα μοντέλα Χένκιν (Henkin models). Παραδείγματα λογικών ανώτερου βαθμού είναι ο λ-λογισμός με απλούς τύπους του Τσερτς (Απλή Θεωρία των Τύπων), ο (calculus of constructions) του Κοκάν, που επιτρέπει εξαρτώμενους και πολυμορφικούς τύπους, και φυσικά η HOL. (el)
- En programlingva teorio, branĉo de komputiko, la teorio de tipoj provizas la formalan bazon por la dizajno, analitiko kaj studo de tipo-sistemoj. Ja, multaj komputilo-sciencistoj uzas la terminon teorio de tipoj por nomi la formalan studon de tipo-sistemoj por programlingvoj, kvankam iuj limigas ĝin al la studo de pli abstraktaj formalismoj kiel tipitaj λ-kalkuloj. Je la plej larĝa nivelo, teorio de tipoj estas la branĉo de matematiko kaj logiko, kiu koncernas sin kun klasigi entojn en kolektojn nomitajn kiel tipoj. En ĉi tiu senco, ĝi rilatas al la metafizika nocio de 'tipo'. La moderna teorio de tipoj estis inventita parte en respondo al la paradokso de Russell, kaj estas esprimitas elstare en far Russell kaj . (eo)
- Unter Logik höherer Stufe (englisch Higher-Order Logic, HOL), auch Stufenlogik, versteht man eine Erweiterung der Prädikatenlogik erster Stufe.Sie basiert auf dem typisierten Lambda-Kalkül und geht auf Alonzo Churchs Theory of Simple Types zurück. Entwickelt um 1940 als ein Versuch der Formalisierung der Logik in der Principia Mathematica von Whitehead und Russell, ist sie von Leon Henkin und eingehend untersucht worden. Anfang der 1970er Jahre wurden nicht-klassische Versionen der Logik höherer Stufe entwickelt, die die Grundlage der modernen Typtheorie (Per Martin-Löf, Jean-Yves Girard) und Beweistheorie (Jean-Yves Girard, Gérard Huet, , ) bilden.Da die Logik höherer Stufe sowohl mächtig als auch relativ einfach auf einem Computer zu implementieren ist, wurden in letzter Zeit einige Theorembeweiser hierfür entwickelt, die gleichermaßen für die Mathematik als auch für die Informatik von Interesse sind. (de)
- En matematiko kaj logiko, logiko de supera ordo estas formo de predikatkalkulo distingata de la predikata logiko de la unua ordo pere de aldonaj kvantigiloj kaj, fojfoje, per pli forta semantiko. Logiko de supera ordo kun sia norma semantiko estas pli esprimkapabla, sed ĝiaj model-teoriaj ecoj estas pli kompleksaj ol tiuj de la unuaorda logiko. La anglalingva termino por logiko de supera ordo nome "higher-order logic", mallongigita kiel HOL, estas ofte uzata por referenci simplan predikatkalkulon de supera ordo. Tie "simpla" indikas, ke subkuŝa teorio de tipoj estas la teorio de simplaj tipoj, nomata ankaŭ simpla teorio de tipoj. Leon Chwistek kaj Frank P. Ramsey proponis tion kiel simpligon de la komplika kaj aspra branĉigita teorio de tipoj specifita en la Principia Mathematica de Alfred North Whitehead kaj Bertrand Russell. Nuntempe simplaj tipoj estas rimedo por ekskludi plurformajn kaj dependajn tipojn. (eo)
- En matemáticas, lógica y ciencias de la computación, la teoría de tipos es cualquiera de varios sistemas formales que pueden servir como alternativas a la teoría de conjuntos como fundamento de las matemáticas constructivas, o al estudio de tales formalismos en general. En la teoría de lenguajes de programación, una rama de las ciencias de la computación, la teoría de tipos puede referirse al diseño, análisis y estudio de los sistemas de tipos, aunque algunos teóricos de la computación limitan el significado del término al estudio de formalismos abstractos como el . (es)
- En mathématiques, logique et informatique, une théorie des types est une classe de systèmes formels, dont certains peuvent servir d'alternatives à la théorie des ensembles comme fondation des mathématiques. Ils ont été historiquement introduits pour résoudre le paradoxe d'un axiome de compréhension non restreint. En théorie des types, il existe des types de base et des constructeurs (comme celui des fonctions ou encore celui du produit cartésien) qui permettent de créer de nouveaux types à partir de types préexistant. Une différence notable avec la théorie des ensembles est que chaque terme possède un type, ce qui est un jugement subjectif et non pas une proposition . En d'autres termes la question de savoir si un terme appartient ou non à un type n'est pas réputée objective. Des types sont utilisés dans certains langages de programmation, ce qui permet d'éviter des bugs. Toutefois, la théorie des types fait plus souvent références à l'étude des systèmes de types qui servent de fondation alternative aux mathématiques. Le λ-calcul typé d'Alonzo Church et ses extensions permettent de faire de la logique à différents ordres ; ainsi elles servent à formaliser le système F. Dans la même ligne, la théorie des types intuitionniste de Per Martin-Löf ainsi que le calcul des constructions inductif offrent d'autres perspectives. Ceux-ci sont notamment à la base d' (en) ou de Coq qui sont des assistants de preuve. (fr)
- Les logiques d'ordre supérieur (en anglais, higher-order logic ou HOL) sont des logiques formelles permettant d'utiliser des variables qui réfèrent à des fonctions ou à des prédicats. Elles étendent le calcul des prédicats. (fr)
- 型理論（かたりろん、英: Type theory）は、集合論を数学基礎論の視点から代替する理論である。階型理論（かいけいりろん、英: Theory of Types）とも呼ばれる。アロンゾ・チャーチの型付きラムダ計算と、マルティン・レーフの直観主義型理論が有名である。計算機科学やコンピュータプログラミングで用いられる型システムの学術研究として知られる。 20世紀初頭にバートランド・ラッセルが発見した、ラッセルのパラドックスによるフレーゲの素朴集合論の欠陥を説明する中で提起されたtheories of typeが型理論の起源であり、後年にAxiom of reducibilityが付随された型理論は、ホワイトヘッドとラッセルの 『プリンキピア・マテマティカ』に収録されている。 (ja)
- In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of mathematics. Two influential type theories that were proposed as foundations are Alonzo Church's typed λ-calculus and Per Martin-Löf's intuitionistic type theory. Most computerized proof-writing systems use a type theory for their foundation. A common one is Thierry Coquand's Calculus of Inductive Constructions. (en)
- 高階述語論理（こうかいじゅつごろんり、英: Higher-order logic）は、一階述語論理と様々な意味で対比される用語である。 例えば、その違いは量化される変項の種類にも現われている。一階述語論理では、大まかに言えば述語に対する量化ができない。述語を量化できる論理体系については二階述語論理に詳しい。 その他の違いとして、基盤となる型理論で許されている型構築の違いがある。高階述語（higher-order predicate）とは、引数として1つ以上の別の述語をとることができる述語である。一般に n 階の高階述語の引数は1つ以上の (n − 1) 階の述語である（ここで n > 1）。同じことは高階関数（higher-order function）にも言える。 高階述語論理は表現能力が高いが、その特性、特にモデル理論に関わる部分では、多くの応用について性格が良いとは言えない。クルト・ゲーデルの業績により、古典的高階述語論理の任意の標準モデルで真となる命題のみ、そしてそれらの全てを証明できるような（帰納的に公理化された）健全で完全な証明計算は存在しない。一方、モデルの範囲を（非標準的モデルを含む）ヘンキンモデルに拡大すれば、任意のモデルで真となる命題のみ、そしてそれらの全てを証明できるような、健全で完全な証明計算は存在する。 高階述語論理の例として、アロンゾ・チャーチの Simple Theory of Types や Calculus of Constructions (CoC) がある。 (ja)
- ( 비슷한 이름의 유형론에 관해서는 해당 문서를 참조하십시오.) 수학, 논리학, 컴퓨터 과학에서 유형 이론(類型理論, 영어: type theory) 또는 유형론은 유형의 개념을 사용하여, 합법적으로 사용 가능한 논리식에 제한을 두는 논리 체계들의 총칭이다. 최초의 유형 이론은 버트런드 러셀이 만든 분지 유형 이론이다. (ko)
- 고차 논리(高次論理, 영어: higher-order logic)는 관계 또는 관계의 관계 등을 지칭하는 변수에 전칭·존재 기호를 가할 수 있는 일련의 논리 체계들이다. 모든 고차 논리는 ω차 논리(ω次論理, 영어: ω-order logic)의 부분 논리 체계로 생각할 수 있다.:Chapter 5, §50 (ko)
- 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 . 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 Bertrand Russell e Alfred North Whitehead. (it)
- In de wiskunde, logica en informatica houdt de typetheorie zich bezig met formele typesystemen. Sommige typesystemen kunnen dienen als grondslagen van de wiskunde, als alternatief voor de verzamelingenleer. Voorbeelden van typesystemen zijn de getypeerde lambdacalculus en . Sommige informatici beschouwen ook het ontwerp, de analyse en het gebruik van datatypes, die in programmeertalen gebruikt worden, als onderdeel van de typetheorie. (nl)
- Teorią typów (ang. Type theory, niem. Typentheorie) – określa się w informatyce teoretycznej i logice matematycznej klasę systemów formalnych, w których każdy termin (ang. term, niem. Term) ma typ (ang. type, niem. Typ), a operacje są ograniczone do terminów określonego typu. Teoria typów może służyć jako alternatywa dla teorii zbiorów jako podstawy dla całej matematyki. Teoria typów jest ściśle związana z systemami typów (i częściowo pokrywa się z nimi), które są funkcją języków programowania zmniejszającą liczby błędów. Dwie najbardziej znane teorie typów to typ rachunku λ Alonzo Churcha i Per Martina-Löfa (ang. intuitionistic type theory, niem. intuitionistische Typentheorie). (pl)
- Теорией типов считается какая-либо формальная система, являющаяся альтернативой наивной теории множеств, сопровождаемая классификацией элементов такой системы с помощью типов, образующих некоторую иерархию. Также под теорией типов понимают изучение подобных формализмов. Теория типов — математически формализованная база для проектирования, анализа и изучения систем типов данных в теории языков программирования (раздел информатики). Многие программисты используют это понятие для обозначения любого аналитического труда, изучающего системы типов в языках программирования. В научных кругах под теорией типов чаще всего понимают более узкий раздел дискретной математики, в частности λ-исчисление с типами. Современная теория типов была частично разработана в процессе разрешения парадокса Рассела и во многом базируется на работе Бертрана Рассела и Альфреда Уайтхеда «Principia mathematica». (ru)
- Логика высшего порядка в математике и логике — форма предикатной логики, которая отличается от логики первого порядка дополнительными предикатами над предикатами, кванторами над ними, и, соответственно, более богатой семантикой. Логики высшего порядка с их стандартными семантиками более выразительны, но их модельно-теоретические свойства значительно более сложны для изучения и применения по сравнению с логикой первого порядка. Логика первого порядка квантифицирует только переменные; логика второго порядка допускает также квантификацию предикатов и функциональных символов (над множествами); логика третьего порядка использует и квантифицирует предикаты над предикатами (множества множеств), и так далее. Например, предложение второго порядка выражает принцип математической индукции. Логика высшего порядка включает все логики более низкого порядка; иначе говоря, логика высшего порядка допускает высказывания с предикатами (над множествами) более низкой глубины вложенности. (ru)
- Na matemática e na lógica, uma lógica de ordem superior é uma forma de lógica de predicados que se distingue da lógica deprimeira ordem por permitir a presença de quantificadores sobre predicados, e por possuir uma semântica mais forte. Lógicas desse tipo, com sua semântica padrão, são mais expressivas, mas suas propriedades na teoria dos modelos são "menos bem-comportadas" do que as da lógica de primeira ordem em relação a certas aplicações. Um predicado de ordem superior seria um predicado que tem um ou mais predicados como argumentos. Em geral, um predicado de ordem superior de ordem n toma um ou mais predicados de ordem (n − 1) como argumentos, onde n > 1. (pt)
- 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, a 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 variam, mas a seguinte definição dada por Benjamin C. Pierce - na obra Types and Programming Languages, MIT Press, 2002 - 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 comportamentosem um programa através da classificação de frases de acordo com as espécies de valores que elas computam." 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, a instrução "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 para 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 (e.g Haskell)
* 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
* Sistemas Modulares
* Sistemas Baseados em Provas de Tipos (e.g. ELF)
* … (muito mais) Impacto prático da teoria dos tipos
* Linguagem de
* Análise e otimização de programas orientadas a tipos
* Mecanismos de verificação de segurança de tipos e.g., TAL, verificação de bytecode do Java) Conexões com lógica construtivista Isomorfismos entre sistemas de provas lógicas e sistemas de tiposRef: Wadler's "Programs are proofs"Curry-Howard IsomorphismIntuitionistic Type Theory Outros tópicos:
* 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é condição, pós condição e invariantes (pt)
- Теорія типів — це будь-яка формальна система, що може слугувати альтернативою наївній теорії множин. У теорії типів кожен «терм» має «тип», а операції виконуються в узгодженості з цими типами. Теорія типів тісно пов'язана з системами типів — особливістю мов програмування, яка призначена для зменшення кількості помилок. Теорія типів була розроблена для обходження парадоксів формальної логіки. Однією з найвідоміших теорій типів є типізоване лямбда-числення Алонзо Черча та інтуїціоністська теорія типів . (uk)
- 在数学中，高阶逻辑在很多方面有别于一阶逻辑。 其一是变量类型出现在量化中；粗略的说，一阶逻辑中禁止量化谓词。允许这么做的系统请参见二阶逻辑。 高阶逻辑区别于一阶逻辑的其他方式是在构造中允许下层的类型论。高阶谓词是接受其他谓词作为参数的谓词。一般的，阶为n的高阶谓词接受一个或多个（n − 1）阶的谓词作为参数，这里的n > 1。对高阶函数类似的评述也成立。 高阶逻辑更加富有表达力，但是它们的性质，特别是有关模型论的，使它们对很多应用不能表现良好。作为哥德尔的结论，经典高阶逻辑不容许（递归的公理化的）可靠的和完备的；这个缺陷可以通过使用模型来修补。 高阶逻辑的一个实例是构造演算。 (zh)
- 類型論，數學、邏輯和電腦科學以下的一個分支，是研究不同類型系統及其表達形式的學科。某些類型系統適合用作數學基礎，取代數學家一般使用的集合論，其中最具影響力的有阿隆佐·邱奇的有類型λ演算和佩爾·馬丁-洛夫的直覺類型論。許多函式語言和工具都建立在類型論的基礎上，如Agda、Coq、Idris、等等。 類型論的核心概念是，每一條合乎語法規則的表達式（或稱「项」）都有其所屬的「類型」。通過結合多個基礎類型，可以定義更加複雜的類型。如此得出的類型可以代表林林總總的數學結構，如自然數、群、拓撲空間等等。在集合論中，這些結構都是含有元素（或稱成員）的集合，它的定義純粹就是指定其所含的所有元素。在類型論中，這些結構的定義並不羅列屬於它的所有項，而是指定如何建構它的項的一套規則。 集合論建基於一階邏輯，有「集合」和「命題」兩個主要概念。任何一套集合論公理（如策梅洛-弗蘭克爾集合論）和命題都是以一階邏輯的語言所表達。類型論則只有「類型」的概念，每一條邏輯命題都是一個類型。要證明任何一條命題，就需要建構屬於此類型的項，是為命題為類型原理。換言之，證明定理的過程只不過是建構符合指定數學結構的數學對象的過程的一個特例。 (zh)
|
| rdfs:comment
|
- In mathematischer Logik und theoretischer Informatik sind Typentheorien formale Systeme, in denen jeder Term einen Typ hat und Operationen auf bestimmte Typen beschränkt sind. Einige Typentheorien werden als Alternative zur axiomatischen Mengenlehre als Grundlage für die moderne Mathematik benutzt. Typentheorien haben Überschneidungen mit Typsystemen, die ein Merkmal von Programmiersprachen zur Fehlervermeidung darstellen. Zwei populäre Typentheorien, die als mathematische Grundlagen genutzt werden, sind Alonzo Churchs typisierter Lambda-Kalkül und Per Martin-Löfs . (de)
- En programlingva teorio, branĉo de komputiko, la teorio de tipoj provizas la formalan bazon por la dizajno, analitiko kaj studo de tipo-sistemoj. Ja, multaj komputilo-sciencistoj uzas la terminon teorio de tipoj por nomi la formalan studon de tipo-sistemoj por programlingvoj, kvankam iuj limigas ĝin al la studo de pli abstraktaj formalismoj kiel tipitaj λ-kalkuloj. Je la plej larĝa nivelo, teorio de tipoj estas la branĉo de matematiko kaj logiko, kiu koncernas sin kun klasigi entojn en kolektojn nomitajn kiel tipoj. En ĉi tiu senco, ĝi rilatas al la metafizika nocio de 'tipo'. La moderna teorio de tipoj estis inventita parte en respondo al la paradokso de Russell, kaj estas esprimitas elstare en far Russell kaj . (eo)
- En matemáticas, lógica y ciencias de la computación, la teoría de tipos es cualquiera de varios sistemas formales que pueden servir como alternativas a la teoría de conjuntos como fundamento de las matemáticas constructivas, o al estudio de tales formalismos en general. En la teoría de lenguajes de programación, una rama de las ciencias de la computación, la teoría de tipos puede referirse al diseño, análisis y estudio de los sistemas de tipos, aunque algunos teóricos de la computación limitan el significado del término al estudio de formalismos abstractos como el . (es)
- Les logiques d'ordre supérieur (en anglais, higher-order logic ou HOL) sont des logiques formelles permettant d'utiliser des variables qui réfèrent à des fonctions ou à des prédicats. Elles étendent le calcul des prédicats. (fr)
- 型理論（かたりろん、英: Type theory）は、集合論を数学基礎論の視点から代替する理論である。階型理論（かいけいりろん、英: Theory of Types）とも呼ばれる。アロンゾ・チャーチの型付きラムダ計算と、マルティン・レーフの直観主義型理論が有名である。計算機科学やコンピュータプログラミングで用いられる型システムの学術研究として知られる。 20世紀初頭にバートランド・ラッセルが発見した、ラッセルのパラドックスによるフレーゲの素朴集合論の欠陥を説明する中で提起されたtheories of typeが型理論の起源であり、後年にAxiom of reducibilityが付随された型理論は、ホワイトヘッドとラッセルの 『プリンキピア・マテマティカ』に収録されている。 (ja)
- In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of mathematics. Two influential type theories that were proposed as foundations are Alonzo Church's typed λ-calculus and Per Martin-Löf's intuitionistic type theory. Most computerized proof-writing systems use a type theory for their foundation. A common one is Thierry Coquand's Calculus of Inductive Constructions. (en)
- ( 비슷한 이름의 유형론에 관해서는 해당 문서를 참조하십시오.) 수학, 논리학, 컴퓨터 과학에서 유형 이론(類型理論, 영어: type theory) 또는 유형론은 유형의 개념을 사용하여, 합법적으로 사용 가능한 논리식에 제한을 두는 논리 체계들의 총칭이다. 최초의 유형 이론은 버트런드 러셀이 만든 분지 유형 이론이다. (ko)
- 고차 논리(高次論理, 영어: higher-order logic)는 관계 또는 관계의 관계 등을 지칭하는 변수에 전칭·존재 기호를 가할 수 있는 일련의 논리 체계들이다. 모든 고차 논리는 ω차 논리(ω次論理, 영어: ω-order logic)의 부분 논리 체계로 생각할 수 있다.:Chapter 5, §50 (ko)
- 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 . 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 Bertrand Russell e Alfred North Whitehead. (it)
- In de wiskunde, logica en informatica houdt de typetheorie zich bezig met formele typesystemen. Sommige typesystemen kunnen dienen als grondslagen van de wiskunde, als alternatief voor de verzamelingenleer. Voorbeelden van typesystemen zijn de getypeerde lambdacalculus en . Sommige informatici beschouwen ook het ontwerp, de analyse en het gebruik van datatypes, die in programmeertalen gebruikt worden, als onderdeel van de typetheorie. (nl)
- Teorią typów (ang. Type theory, niem. Typentheorie) – określa się w informatyce teoretycznej i logice matematycznej klasę systemów formalnych, w których każdy termin (ang. term, niem. Term) ma typ (ang. type, niem. Typ), a operacje są ograniczone do terminów określonego typu. Teoria typów może służyć jako alternatywa dla teorii zbiorów jako podstawy dla całej matematyki. Teoria typów jest ściśle związana z systemami typów (i częściowo pokrywa się z nimi), które są funkcją języków programowania zmniejszającą liczby błędów. Dwie najbardziej znane teorie typów to typ rachunku λ Alonzo Churcha i Per Martina-Löfa (ang. intuitionistic type theory, niem. intuitionistische Typentheorie). (pl)
- Теорія типів — це будь-яка формальна система, що може слугувати альтернативою наївній теорії множин. У теорії типів кожен «терм» має «тип», а операції виконуються в узгодженості з цими типами. Теорія типів тісно пов'язана з системами типів — особливістю мов програмування, яка призначена для зменшення кількості помилок. Теорія типів була розроблена для обходження парадоксів формальної логіки. Однією з найвідоміших теорій типів є типізоване лямбда-числення Алонзо Черча та інтуїціоністська теорія типів . (uk)
- 在数学中，高阶逻辑在很多方面有别于一阶逻辑。 其一是变量类型出现在量化中；粗略的说，一阶逻辑中禁止量化谓词。允许这么做的系统请参见二阶逻辑。 高阶逻辑区别于一阶逻辑的其他方式是在构造中允许下层的类型论。高阶谓词是接受其他谓词作为参数的谓词。一般的，阶为n的高阶谓词接受一个或多个（n − 1）阶的谓词作为参数，这里的n > 1。对高阶函数类似的评述也成立。 高阶逻辑更加富有表达力，但是它们的性质，特别是有关模型论的，使它们对很多应用不能表现良好。作为哥德尔的结论，经典高阶逻辑不容许（递归的公理化的）可靠的和完备的；这个缺陷可以通过使用模型来修补。 高阶逻辑的一个实例是构造演算。 (zh)
- 類型論，數學、邏輯和電腦科學以下的一個分支，是研究不同類型系統及其表達形式的學科。某些類型系統適合用作數學基礎，取代數學家一般使用的集合論，其中最具影響力的有阿隆佐·邱奇的有類型λ演算和佩爾·馬丁-洛夫的直覺類型論。許多函式語言和工具都建立在類型論的基礎上，如Agda、Coq、Idris、等等。 類型論的核心概念是，每一條合乎語法規則的表達式（或稱「项」）都有其所屬的「類型」。通過結合多個基礎類型，可以定義更加複雜的類型。如此得出的類型可以代表林林總總的數學結構，如自然數、群、拓撲空間等等。在集合論中，這些結構都是含有元素（或稱成員）的集合，它的定義純粹就是指定其所含的所有元素。在類型論中，這些結構的定義並不羅列屬於它的所有項，而是指定如何建構它的項的一套規則。 集合論建基於一階邏輯，有「集合」和「命題」兩個主要概念。任何一套集合論公理（如策梅洛-弗蘭克爾集合論）和命題都是以一階邏輯的語言所表達。類型論則只有「類型」的概念，每一條邏輯命題都是一個類型。要證明任何一條命題，就需要建構屬於此類型的項，是為命題為類型原理。換言之，證明定理的過程只不過是建構符合指定數學結構的數學對象的過程的一個特例。 (zh)
- نظرية النمط أو التنويع (بالإنجليزية: Type theory) في الرياضيات، المنطق والمعلوماتية هي أي نظام شكلي بإمكانه القيام مكان ، أو دراسة التشكيل بشكل عام، وهي أيضاً منهج لبناء المنطق الصوري توضع بواسطته تفرقة بين الموضوعات ذات المستويات المختلفة (الأنماط)، ويهدف هذا المنهج إلى استبعاد المفارقات أو التناقضات من المنطق ونظرية الأعداد وكان أول من وضع نظرية الأنماط، وطبقها على منطق الفئات (1890)، وفي الأعوام 1908 - 1910 بنى برتراند راسل نسقاً تفصيلياً من نظرية الأنماط وطبقة على أساس التفرقة (طبقاً للأنماط)بين :
* الافراد (نمط 1)
* الصفات (نمط 2)
* صفات الصفات (نمط 3) (ar)
- Teorie typů je teorie na pomezí matematiky, filosofie a , kterou jako první předložil Bertrand Russell za účelem vyřešení paradoxů teorie množin, ačkoliv zárodky lze najít již u Bernarda Bolzana. Nejjednodušším příkladem použití je typovaný lambda kalkul. V teorie typů existuje univerzum typů a jejich hodnot, přičemž každá proměnná má určený typ, například ve formuli . Existují různá rozšíření původní Russellovy teorie typů, například obsahující závislostní typy. Algebraické datové typy tvoří algebru, která je polookruhem. (cs)
- V matematice se logika vyššího řádu odlišuje od predikátové logiky prvního řádu několika způsoby. Jeden z nich je typ , přes které se kvantifikuje; v logice prvního řádu se kvantifikuje pouze pro proměnné pro individua a nelze kvantifikovat (volně řečeno) přes proměnné pro predikátové symboly. To lze v a dalších systémech. Příklady logik vyšších řádů jsou Churchova jednoduchá teorie typů (angl. 'Simple Theory of Types') a (angl. 'calculus of constructions'). (cs)
- Στα μαθηματικά και τη λογική, μία λογική ανώτερου βαθμού ή λογική ανώτερης τάξης (higher-order logic) διακρίνεται από μία λογική πρώτου βαθμού με βάση αρκετά χαρακτηριστικά. Ένα από αυτά είναι ο τύπος των μεταβλητών που εμφανίζονται στους ποσοδείκτες: γενικά, στην πρωτοβάθμια λογική, απαγορεύεται οι ποσοδείκτες να αναφέρονται σε κατηγορήματα, ενώ αυτό επιτρέπεται στη . Η λογική ανώτερου βαθμού διαφέρει επίσης από τη λογική πρώτου βαθμού στις δομές που η θεωρία τύπων της επιτρέπει να κατασκευάζονται. Ένα κατηγόρημα ανώτερου βαθμού είναι ένα κατηγόρημα που δέχεται σαν παραμέτρους κατηγορήματα. Γενικά, ένα κατηγόρημα βαθμού n παίρνει ένα ή περισσότερα κατηγορήματα βαθμού n − 1 σαν παραμέτρους, όπου n > 1. Παρόμοια ισχύουν και για τις συναρτήσεις ανώτερης τάξης. (el)
- Στα Μαθηματικά, στη Λογική και στη Επιστήμη των Υπολογιστών, η Θεωρία Τύπων είναι ένα από τα τα οποία χρησιμοποιούνται στην , ή στη μελέτη τέτοιων φορμαλισμών γενικότερα. Στη Θεωρία των Γλωσσών Προγραμματισμού, ενός κλάδου της Επιστήμης των Υπολογιστών, η Θεωρία Τύπων μπορεί να αναφέρεται στο σχεδιασμό, στην ανάλυση και στη μελέτη των Συστημάτων Τύπων, παρόλο που κάποιοι επιστήμονες της Πληροφορικής περιορίζουν τη σημασία του όρου στη μελέτη των αφηρημένων φορμαλισμών όπως ο λ-λογισμός με τύπους. (el)
- Unter Logik höherer Stufe (englisch Higher-Order Logic, HOL), auch Stufenlogik, versteht man eine Erweiterung der Prädikatenlogik erster Stufe.Sie basiert auf dem typisierten Lambda-Kalkül und geht auf Alonzo Churchs Theory of Simple Types zurück. (de)
- En matematiko kaj logiko, logiko de supera ordo estas formo de predikatkalkulo distingata de la predikata logiko de la unua ordo pere de aldonaj kvantigiloj kaj, fojfoje, per pli forta semantiko. Logiko de supera ordo kun sia norma semantiko estas pli esprimkapabla, sed ĝiaj model-teoriaj ecoj estas pli kompleksaj ol tiuj de la unuaorda logiko. (eo)
- En mathématiques, logique et informatique, une théorie des types est une classe de systèmes formels, dont certains peuvent servir d'alternatives à la théorie des ensembles comme fondation des mathématiques. Ils ont été historiquement introduits pour résoudre le paradoxe d'un axiome de compréhension non restreint. Des types sont utilisés dans certains langages de programmation, ce qui permet d'éviter des bugs. (fr)
- 高階述語論理（こうかいじゅつごろんり、英: Higher-order logic）は、一階述語論理と様々な意味で対比される用語である。 例えば、その違いは量化される変項の種類にも現われている。一階述語論理では、大まかに言えば述語に対する量化ができない。述語を量化できる論理体系については二階述語論理に詳しい。 その他の違いとして、基盤となる型理論で許されている型構築の違いがある。高階述語（higher-order predicate）とは、引数として1つ以上の別の述語をとることができる述語である。一般に n 階の高階述語の引数は1つ以上の (n − 1) 階の述語である（ここで n > 1）。同じことは高階関数（higher-order function）にも言える。 高階述語論理は表現能力が高いが、その特性、特にモデル理論に関わる部分では、多くの応用について性格が良いとは言えない。クルト・ゲーデルの業績により、古典的高階述語論理の任意の標準モデルで真となる命題のみ、そしてそれらの全てを証明できるような（帰納的に公理化された）健全で完全な証明計算は存在しない。一方、モデルの範囲を（非標準的モデルを含む）ヘンキンモデルに拡大すれば、任意のモデルで真となる命題のみ、そしてそれらの全てを証明できるような、健全で完全な証明計算は存在する。 (ja)
- 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, a Teoria dos Tipos tem encontrado aplicação prática no desenvolvimento de sistemas de tipos de linguagens de programação. (pt)
- Теорией типов считается какая-либо формальная система, являющаяся альтернативой наивной теории множеств, сопровождаемая классификацией элементов такой системы с помощью типов, образующих некоторую иерархию. Также под теорией типов понимают изучение подобных формализмов. Современная теория типов была частично разработана в процессе разрешения парадокса Рассела и во многом базируется на работе Бертрана Рассела и Альфреда Уайтхеда «Principia mathematica». (ru)
- Na matemática e na lógica, uma lógica de ordem superior é uma forma de lógica de predicados que se distingue da lógica deprimeira ordem por permitir a presença de quantificadores sobre predicados, e por possuir uma semântica mais forte. Lógicas desse tipo, com sua semântica padrão, são mais expressivas, mas suas propriedades na teoria dos modelos são "menos bem-comportadas" do que as da lógica de primeira ordem em relação a certas aplicações. (pt)
- Логика высшего порядка в математике и логике — форма предикатной логики, которая отличается от логики первого порядка дополнительными предикатами над предикатами, кванторами над ними, и, соответственно, более богатой семантикой. Логики высшего порядка с их стандартными семантиками более выразительны, но их модельно-теоретические свойства значительно более сложны для изучения и применения по сравнению с логикой первого порядка. (ru)
|
