Quelltext der Seite Typentheorie

In [[Mathematische Logik|mathematischer Logik]] und [[Theoretische Informatik|theoretischer Informatik]] sind '''Typentheorien''' [[Formales System|formale Systeme]], in denen jeder Term einen Typ hat und Operationen auf bestimmte Typen beschränkt sind. Einige Typentheorien werden als Alternative zur [[Axiomatische Mengenlehre|axiomatischen Mengenlehre]] als Grundlage für die moderne Mathematik benutzt.

Typentheorien haben Überschneidungen mit [[Typisierung (Informatik)#Typsystem|Typsystemen]], die ein Merkmal von [[Programmiersprache]]n zur Fehlervermeidung darstellen.

Zwei populäre Typentheorien, die als mathematische Grundlagen genutzt werden, sind [[Alonzo Church]]s [[Lambda-Kalkül#Typisierter Lambda-Kalkül|typisierter Lambda-Kalkül]] und [[Per Martin-Löf]]s [[intuitionistische Typentheorie]].

== Geschichte ==
Zwischen 1902 und 1908 schlug [[Bertrand Russell]] verschiedene Typentheorien vor, mit denen die [[Russellsche Antinomie]] der [[Naive Mengenlehre|naiven Mengenlehre]] [[Gottlob Frege]]s vermieden werden sollte. Seine „verzweigte“ Typentheorie und das [[Reduzibilitätsaxiom]] spielten eine wichtige Rolle in den zwischen 1910 und 1913 veröffentlichten [[Principia Mathematica]]. [[Alfred North Whitehead|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 [[Konstruktive Mathematik|konstruktiven Mathematik]] und auch für den Beweisassistenten [[Agda]] wird die intuitionistische Typentheorie verwendet. Dagegen beruht der Beweisassistent [[Coq (Software)|Coq]] auf dem [[Konstruktionskalkül]] CoC. Ein aktives Forschungsgebiet ist die [[Homotopietypentheorie]].

== Grundlegende Konzepte ==
In einer Typentheorie hat jeder Term einen Typ und Operationen werden nur für Terme eines bestimmten Typs definiert. Ein Typurteil <math>M\colon A</math> besagt, dass der Term <math>M</math> vom Typ <math>A</math> ist. Zum Beispiel ist <math>\mathrm{Nat}</math> der Typ der [[Natürliche Zahl|natürlichen Zahlen]] und <math>0,1,2,\ldots</math> sind Terme von diesem Typ. <math>2\colon \mathrm{Nat}</math> ist das Urteil, dass <math>2</math> vom Typ <math>\mathrm{Nat}</math> ist.

Eine Funktion wird in der Typentheorie durch einen Pfeil <math>\to</math> bezeichnet. Die [[Nachfolger (Mathematik)|Nachfolger-Funktion]] <math>\mathrm{addOne}</math> hat das Urteil <math>\mathrm{addOne}\colon \mathrm{Nat}\to\mathrm{Nat}</math>. Der Aufruf einer Funktion wird gelegentlich auch ohne Klammer geschrieben, also <math>\mathrm{addOne}\,2</math> anstelle von <math>\mathrm{addOne}(2).</math>

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

== Typentheorien ==
=== Lambda-Kalkül (nach Church) ===
{{Hauptartikel|Lambda-Kalkül}}

[[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 [[Berechenbarkeit|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 [[Funktionale Programmierung|funktionaler Programmiersprachen]], die Forschung um Typsysteme von Programmiersprachen im Allgemeinen sowie moderne Teildisziplinen in der [[Logik]] wie die Typtheorie wesentlich beeinflusst.

=== Intuitionistische Typentheorie (nach Martin-Löf) ===
{{Hauptartikel|Intuitionistische Typentheorie}}

Die intuitionistische Typentheorie nach [[Per Martin-Löf]] ist eine auf den Prinzipien des [[Konstruktive Mathematik|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.&nbsp;B. der Typ aller [[Geordnetes Paar|geordneten Paare]] vergleichbar mit [[Konjunktion (Logik)|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ürliche Zahl|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.

=== Calculus of Constructions (nach Coquand) ===
{{Hauptartikel|Calculus of Constructions}}

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 (Software)|Coq]] ist.

=== Homotopietypentheorie ===
Die '''Homotopietypentheorie''' ('''HoTT''') bezeichnet Entwicklungen der intensionalen Typentheorie von Martin-Löf, basierend auf der Interpretation von Typen als Objekte der [[Homotopie]]theorie ([[Vladimir Voevodsky]]). Homotopietypentheorie kann als Alternative zur [[Mengenlehre]] als Grundlage für jegliche Mathematik benutzt werden. Aktuelle Forschung umfasst deshalb u.&#8239;a. die Formulierung herkömmlicher Mathematik auf Grundlage von Typentheorie und die Umsetzung in [[Maschinengestütztes Beweisen|Beweisassistenten]].

Im akademischen Jahr 2012/2013 entstand in einem gemeinsamen Forschungsprojekt am [[Institute for Advanced Study]] ein Buch über die Grundlagen dieser Disziplin.<ref>[https://homotopytypetheory.org/book/ Homotopy Type Theory: Univalent Foundations of Mathematics]</ref>

== Spezielle Typen ==
* [[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)

== Typkonstruktoren ==
Mit einem [[Typkonstruktor]] lassen sich aus vorhandenen (einfachen) Typen neue konstruieren. Beispiele sind '''setof'''<ref>siehe [[PL/pgSQL#Rückgabe der Funktion|PL/PostgreSQL]]</ref> entsprechend der Russellschen Typhierarchie (auch iteriert zu einem Basistyp) und Konstruktoren für geordnete Paare oder auch ''n''-Tupel: Wenn Komponenten verschiedene Typen haben,<ref>Jedenfalls wenn die Basistypen entsprechend der Russellschen Typhierarchie verschieden sind; bei verschiedenen Typstufen innerhalb derselben Hierarchie kann man die Paardarstellung noch geeignet modifizieren.</ref> ist eine [[Geordnetes Paar#Darstellung geordneter Paare|Paardarstellung]] nach [[Kazimierz Kuratowski|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.<ref>Entsprechend einer [[Feature-Logik]].</ref> Siehe dazu auch [[Monade (Informatik)|Monaden]], [[Lambda-Kalkül#Typisierter Lambda-Kalkül|Lambda-Kalkül §Typisierter Lambda-Kalkül]], [[Haskell (Programmiersprache)#Typsystem|Typkonstruktoren in der Programmiersprache Haskell]].

== Siehe auch ==
* [[Von-Neumann-Hierarchie]] der kumulativen Typen
== Literatur ==
* Bertrand Russell: <!--http://isites.harvard.edu/fs/docs/icb.topic1341338.files/Russell1908.pdf PDF--><!--http://www.cfh.ufsc.br/~dkrause/pg/cursos/selecaoartigos/Russell(1905).pdf-->[https://web.archive.org/web/20140813072910/http://www.cfh.ufsc.br/~dkrause/pg/cursos/selecaoartigos/Russell(1905).pdf ''Mathematical logic as based on the theory of types.''] (englisch; PDF; 1,9&nbsp;MB), in: ''{{lang|en|American Journal of Mathematics.}}'' 30, 1908, S. 222–262 (im Web-Archiv vom 23. August 2014).
* Álvaro Pelayo, Michael A. Warren: [http://www.ams.org/journals/bull/2014-51-04/S0273-0979-2014-01456-9/S0273-0979-2014-01456-9.pdf ''Homotopy type theory and Voevodsky's univalent foundations.''] (englisch; PDF), in: ''Bull. Amer. Math. Soc. (N.S.).'' 51, no. 4, 2014, S. 597–648.

== Weblinks ==
* [https://ncatlab.org/nlab/show/type+theory Type Theory] (nLab)
* {{SEP|https://plato.stanford.edu/entries/type-theory/|Type Theory|Thierry Coquand}}
* {{SEP|https://plato.stanford.edu/entries/type-theory-church/|Church’s Type Theory|Christoph Benzmüller, Peter Andrews}}
* {{SEP|https://plato.stanford.edu/entries/type-theory-intuitionistic/|Intuitionistic Type Theory|Peter Dybjer,  Erik Palmgren}}
* http://glossar.hs-augsburg.de/Typentheorie zur Typentheorie

== Einzelnachweise ==
<references />

[[Kategorie:Typentheorie| ]]
[[Kategorie:Mengenlehre]]
[[Kategorie:Bertrand Russell]]
[[Kategorie:Teilgebiet der Mathematik]]