Typentheorie – Wikipedia

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 intuitionistische Typentheorie.

Zwischen 1902 und 1908 schlug Bertrand Russell verschiedene Typentheorien vor, mit denen die Russellsche Antinomie der naiven Mengenlehre Gottlob Freges vermieden werden sollte. Seine „verzweigte“ Typentheorie und das Reduzibilitätsaxiom spielten eine wichtige Rolle in den zwischen 1910 und 1913 veröffentlichten Principia 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 schlugen Leon Chwistek und Frank P. Ramsey eine einfachere Theorie vor, die heute als „einfache Typentheorie“ bekannt ist.

Üblicherweise besteht eine Typentheorie aus Typen und einem Termersetzungssystem. Ein bekanntes Beispiel ist der Lambda-Kalkül. Auf ihm basiert die Logik höherer Stufe.

In einigen Bereichen der konstruktiven Mathematik und auch für den Beweisassistenten Agda wird die intuitionistische Typentheorie verwendet. Dagegen beruht der Beweisassistent Coq auf dem Konstruktionskalkül CoC. Ein aktives Forschungsgebiet ist die Homotopietypentheorie.

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

Eine Funktion wird in der Typentheorie durch einen Pfeil ${\displaystyle \to }$ bezeichnet. Die Nachfolger-Funktion ${\displaystyle \mathrm {addOne} }$ hat das Urteil ${\displaystyle \mathrm {addOne} \colon \mathrm {Nat} \to \mathrm {Nat} }$. Der Aufruf einer Funktion wird gelegentlich auch ohne Klammer geschrieben, also ${\displaystyle \mathrm {addOne} \,2}$ anstelle von ${\displaystyle \mathrm {addOne} (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 das Entscheidungsproblem 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 eine berechenbare 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, um Logik höherer Stufe darzustellen. Der Lambda-Kalkül hat die Entwicklung funktionaler Programmiersprachen, die Forschung um Typsysteme von Programmiersprachen im Allgemeinen sowie moderne Teildisziplinen in der Logik wie die Typtheorie wesentlich beeinflusst.

Die intuitionistische Typentheorie nach Per Martin-Löf ist eine auf den Prinzipien des Konstruktivismus aufbauende Typentheorie und alternative Grundlegung der Mathematik.

Sie beruht auf einer Analogie zwischen Propositionen und Typen: eine Proposition wird mit dem Typ ihres Beweises identifiziert. So ist z. B. der Typ aller geordneten Paare vergleichbar mit logischer 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 die natürlichen Zahlen: Sie werden explizit als Konstruktion aus der Null und einer Nachfolgerfunktion definiert. Diese werden nicht wie in der Mengenlehre speziell definiert, sondern ihre Existenz wird angenommen oder durch eine verallgemeinerte Konstruktion erlaubt. Zusammen mit diesen Konstruktoren existiert auch ein Induktionsschema, 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 jegliches mathematisches Objekt als Menge betrachtet wird.

Die Typentheorie Calculus of Constructions (CoC) nach Thierry 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 Beweissystem Coq ist.

Die Homotopietypentheorie (HoTT) bezeichnet Entwicklungen der intensionalen Typentheorie von Martin-Löf, basierend auf der Interpretation von Typen als Objekte der Homotopietheorie (Vladimir Voevodsky). Homotopietypentheorie kann als Alternative zur Mengenlehre 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 in Beweisassistenten.

Im akademischen Jahr 2012/2013 entstand in einem gemeinsamen Forschungsprojekt am Institute 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 einem Typkonstruktor lassen sich aus vorhandenen (einfachen) Typen neue konstruieren. Beispiele sind setof^[2] entsprechend der Russellschen Typhierarchie (auch iteriert zu einem Basistyp) und Konstruktoren für geordnete Paare oder auch n-Tupel: Wenn Komponenten verschiedene Typen haben,^[3] ist eine Paardarstellung nach Kuratowski (oder ähnlich) nicht möglich und es muss die Existenz eines Paartyps axiomatisch (per Paaraxiom) gefordert werden. In der Anwendung bei Programmiersprachen werden ähnliche Konstruktoren record oder struct genannt, allerdings haben deren Komponenten gewöhnlich Namen statt Indexnummern wie bei Tupelkoordinaten.^[4] Siehe dazu auch Monaden, 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. ↑ siehe PL/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 einer Feature-Logik.