Inmathematischer Logik undtheoretischer Informatik sindTypentheorienformale Systeme, in denen jeder Term einen Typ hat und Operationen auf bestimmte Typen beschränkt sind. Einige Typentheorien werden als Alternative zuraxiomatischen Mengenlehre als Grundlage für die moderne Mathematik benutzt.

Typentheorien haben Überschneidungen mitTypsystemen, die ein Merkmal vonProgrammiersprachen zur Fehlervermeidung darstellen.

Zwei populäre Typentheorien, die als mathematische Grundlagen genutzt werden, sindAlonzo Churchstypisierter Lambda-Kalkül undPer Martin-Löfsintuitionistische Typentheorie.

Zwischen 1902 und 1908 schlugBertrand Russell verschiedene Typentheorien vor, mit denen dieRussellsche Antinomie dernaiven MengenlehreGottlob Freges vermieden werden sollte. Seine „verzweigte“ Typentheorie und dasReduzibilitätsaxiom spielten eine wichtige Rolle in den zwischen 1910 und 1913 veröffentlichtenPrincipia Mathematica.Whitehead und Russell versuchten dort, Russells Paradoxon durch eine Hierarchie von Typen zu vermeiden, wobei jeder mathematischen Entität ein Typ zuzuordnen ist. Objekte eines bestimmten Typs können nur aus Objekten niederen Typs aufgebaut sein, so dass Schleifen vermieden werden. In den 1920er Jahren schlugenLeon Chwistek undFrank P. Ramsey eine einfachere Theorie vor, die heute als „einfache Typentheorie“ bekannt ist.

Üblicherweise besteht eine Typentheorie aus Typen und einemTermersetzungssystem. Ein bekanntes Beispiel ist derLambda-Kalkül. Auf ihm basiert dieLogik höherer Stufe.

In einigen Bereichen derkonstruktiven Mathematik und auch für den BeweisassistentenAgda wird die intuitionistische Typentheorie verwendet. Dagegen beruht der BeweisassistentCoq auf demKonstruktionskalkül CoC. Ein aktives Forschungsgebiet ist dieHomotopietypentheorie.

In einer Typentheorie hat jeder Term einen Typ und Operationen werden nur für Terme eines bestimmten Typs definiert. Ein Typurteil${\displaystyle M:A}$ besagt, dass der Term${\displaystyle M}$ vom Typ${\displaystyle A}$ ist. Zum Beispiel ist${\displaystyle \mathrm{N}\mathrm{a}\mathrm{t}}$ der Typ dernatürlichen Zahlen und${\displaystyle 0,1,2,\dots }$ sind Terme von diesem Typ.${\displaystyle 2:\mathrm{N}\mathrm{a}\mathrm{t}}$ ist das Urteil, dass${\displaystyle 2}$ vom Typ${\displaystyle \mathrm{N}\mathrm{a}\mathrm{t}}$ ist.

Eine Funktion wird in der Typentheorie durch einen Pfeil${\displaystyle \to }$ bezeichnet. DieNachfolger-Funktion${\displaystyle \mathrm{a}\mathrm{d}\mathrm{d}\mathrm{O}\mathrm{n}\mathrm{e}}$ hat das Urteil${\displaystyle \mathrm{a}\mathrm{d}\mathrm{d}\mathrm{O}\mathrm{n}\mathrm{e}:\mathrm{N}\mathrm{a}\mathrm{t}\to \mathrm{N}\mathrm{a}\mathrm{t}}$. Der Aufruf einer Funktion wird gelegentlich auch ohne Klammer geschrieben, also${\displaystyle \mathrm{a}\mathrm{d}\mathrm{d}\mathrm{O}\mathrm{n}\mathrm{e}2}$ anstelle von${\displaystyle \mathrm{a}\mathrm{d}\mathrm{d}\mathrm{O}\mathrm{n}\mathrm{e}(2).}$

Eine Typentheorie kann auch Termumformungsregeln enthalten. Zum Beispiel sind${\displaystyle 2+1}$ und${\displaystyle 3}$ syntaktisch unterschiedliche Terme, der erste lässt sich aber auf den zweiten reduzieren. Man schreibt${\displaystyle 2+1\twoheadrightarrow 3}$.

Alonzo Church benutzte den Lambda-Kalkül, um 1936 sowohl eine negative Antwort auf dasEntscheidungsproblem zu geben als auch eine Fundierung eines logischen Systems zu finden, wie es den Principia Mathematica von Bertrand Russell und Alfred North Whitehead zugrunde lag. Mittels des untypisierten Lambda-Kalküls kann man klar definieren, was eineberechenbare Funktion ist. Die Frage, ob zwei Lambda-Ausdrücke(s. u.) äquivalent sind, kann im Allgemeinen nicht algorithmisch entschieden werden. In seiner typisierten Form kann der Kalkül benutzt werden, umLogik höherer Stufe darzustellen. Der Lambda-Kalkül hat die Entwicklungfunktionaler Programmiersprachen, die Forschung um Typsysteme von Programmiersprachen im Allgemeinen sowie moderne Teildisziplinen in derLogik wie die Typtheorie wesentlich beeinflusst.

Die intuitionistische Typentheorie nachPer Martin-Löf ist eine auf den Prinzipien desKonstruktivismus aufbauende Typentheorie und alternative Grundlegung derMathematik.

Sie beruht auf einer Analogie zwischen Propositionen und Typen: eine Proposition wird mit dem Typ ihres Beweises identifiziert. So ist z. B. der Typ allergeordneten Paare vergleichbar mitlogischer Konjunktion: Ein solches geordnetes Paar kann nur existieren, falls beide Typen mindestens ein Element besitzen. Hierdurch können viele logische Prinzipien verallgemeinert werden.

Ein ebenfalls sehr relevanter Aspekt der Typentheorie sind induktive Definitionen. Ein Beispiel dafür sind dienatürlichen Zahlen: Sie werden explizit als Konstruktion aus der Null und einer Nachfolgerfunktion definiert. Diese werden nicht wie in derMengenlehre speziell definiert, sondern ihre Existenz wird angenommen oder durch eine verallgemeinerte Konstruktion erlaubt. Zusammen mit diesen Konstruktoren existiert auch einInduktionsschema, das die Erstellung von Funktionen über die natürlichen Zahlen oder auch Beweisen, die für jede natürliche Zahl gelten, erlaubt.

Im Allgemeinen wird die intuitionistische Typentheorie oft als näher zur mathematischen Praxis gesehen als fundamentale Mengenlehre, da in dieser jeglichesmathematisches Objekt als Menge betrachtet wird.

Die Typentheorie Calculus of Constructions (CoC) nachThierry Coquand ist ein Lambda-Kalkül höherer Ordnung, der die Grundlage sowohl für einen konstruktiven Aufbau der Mathematik als auch für das computerisierte BeweissystemCoq ist.

DieHomotopietypentheorie (HoTT) bezeichnet Entwicklungen der intensionalen Typentheorie von Martin-Löf, basierend auf der Interpretation von Typen als Objekte derHomotopietheorie (Vladimir Voevodsky). Homotopietypentheorie kann als Alternative zurMengenlehre als Grundlage für jegliche Mathematik benutzt werden. Aktuelle Forschung umfasst deshalb u. a. die Formulierung herkömmlicher Mathematik auf Grundlage von Typentheorie und die Umsetzung inBeweisassistenten.

Im akademischen Jahr 2012/2013 entstand in einem gemeinsamen Forschungsprojekt amInstitute for Advanced Study ein Buch über die Grundlagen dieser Disziplin.^[1]

• Einheitstyp – void oder 0-Tupel (Englisch: void type), hat nur einen einzigen Wert, ähnlich:
• Bottom-Typ – leerer Typ ohne Werte (null oder ⊥) (hat keinen Wert)
• Top-Typ – der universelle Typ (object oder ⊤) (alle anderen Typen sind Subtypen)

Mit einemTypkonstruktor lassen sich aus vorhandenen (einfachen) Typen neue konstruieren. Beispiele sindsetof^[2] entsprechend der Russellschen Typhierarchie (auch iteriert zu einem Basistyp) und Konstruktoren für geordnete Paare oder auchn-Tupel: Wenn Komponenten verschiedene Typen haben,^[3] ist einePaardarstellung nachKuratowski (oder ähnlich) nicht möglich und es muss die Existenz eines Paartyps axiomatisch (per Paaraxiom) gefordert werden. In der Anwendung bei Programmiersprachen werden ähnliche Konstruktorenrecord oderstruct genannt, allerdings haben deren Komponenten gewöhnlich Namen statt Indexnummern wie bei Tupelkoordinaten.^[4] Siehe dazu auchMonaden,Lambda-Kalkül §Typisierter Lambda-Kalkül,Typkonstruktoren in der Programmiersprache Haskell.

• Von-Neumann-Hierarchie der kumulativen Typen

• Bertrand Russell:Mathematical logic as based on the theory of types. (englisch; PDF; 1,9 MB), in:American Journal of Mathematics. 30, 1908, S. 222–262 (im Web-Archiv vom 23. August 2014).
• Álvaro Pelayo, Michael A. Warren:Homotopy type theory and Voevodsky's univalent foundations. (englisch; PDF), in:Bull. Amer. Math. Soc. (N.S.). 51, no. 4, 2014, S. 597–648.

• Type Theory (nLab)
• Thierry Coquand: Type Theory. In: Edward N. Zalta (Hrsg.):Stanford Encyclopedia of Philosophy.
• Christoph Benzmüller, Peter Andrews: Church’s Type Theory. In: Edward N. Zalta (Hrsg.):Stanford Encyclopedia of Philosophy.
• Peter Dybjer, Erik Palmgren: Intuitionistic Type Theory. In: Edward N. Zalta (Hrsg.):Stanford Encyclopedia of Philosophy.
• http://glossar.hs-augsburg.de/Typentheorie zur Typentheorie

1. ↑Homotopy Type Theory: Univalent Foundations of Mathematics
2. ↑siehePL/PostgreSQL
3. ↑Jedenfalls wenn die Basistypen entsprechend der Russellschen Typhierarchie verschieden sind; bei verschiedenen Typstufen innerhalb derselben Hierarchie kann man die Paardarstellung noch geeignet modifizieren.
4. ↑Entsprechend einerFeature-Logik.

• Typentheorie
• Mengenlehre
• Bertrand Russell
• Teilgebiet der Mathematik