In dieser Bachelorarbeit geht es um die moderne Typentheorie. Vorab wird die veraltete Typentheorie vorgestellt und wird mit der modernen Typentheorie verglichen. Auf die Einleitung folgend werden im zweiten Kapitel zunächst die Grundprinzipien und -regeln von MTTs sowie von STTs vorgestellt. Darauffolgend wird im dritten Kapitel gezeigt, wie eine MTT und die Montague-Grammatik mit linguistischen Phänomenen und diversen Wortarten umgehen. Darauf schließen wir im vierten Teil der Arbeit mit einem kontrastiven Vergleich der beiden Ansätze und der Bewertung ihrer Vorzüge und Defizite im Hinblick auf die Untersuchungskriterien Effizienz und Akkuratheit und damit der Beantwortung der Forschungsfrage: "Hat sich das Opfern der Eigenschaften von simplen Typentheorien gelohnt?"
Inhaltsverzeichnis
1 Einleitung
1.1 Problemlage
1.2 Vorhandene Ansätze
1.3 Forschungsfrage
1.4 Methodisches Vorgehen
2 Grundprinzipien und Methoden von MTT
2.1 Universen und Typen
2.1.1 Many-Sortedness
2.2 Embedded Logic
2.3 Coercions und Subtyping
2.3.1 Subsumptive Subtyping
2.3.2 Coercive Subtyping
2.3.3 Lokale Coercions
2.3.4 Coercion-Kontexte
2.4 Abhängige Typen
2.4.1 Summentypen
2.4.2 Produkttypen
2.5 Simple Typentheorie
2.5.1 Lambda-Kalkül
2.5.2 Church-Rosser-Eigenschaft
2.5.3 Curry-Howard-Isomorphismus
3 Behandlung von lexikalischen Kategorien und Koprädikation mit Typentheorien
3.1 Adjektive
3.1.1 Modifizierte Common Nouns
3.1.2 Intersektive Adjektive
3.1.3 Subsektive Adjektive
3.1.4 Privative Adjektive
3.1.4.1 Meaning Postulates
3.1.4.2 Disjoint Union Type
3.1.5 Non-committal Adjektive
3.1.6 Temporale Adjektive
3.2 Adverbien
3.2.1 Veridikale Adverbien
3.2.2 Nicht-veridikale Adverbien
3.3 Koprädikation in MTT
3.3.1 Punkttypen
3.3.2 Koprädikation mit Quantifizierern
3.3.2.1 Individuation und Identitätskriterien
3.3.2.2 Setoide und Subsetoide
3.3.2.3 Generische Semantik von numerischen Quantifizierern
3.3.2.4 Behandlung von Koprädikation mit Quantifizierern
3.3.2.5 Behandlung von Koprädikation mit Quantifizierer und Adjektiv
3.3.3 Lineare Punkttypen
3.4 STT: Eignung für linguistische Phänomene
4 Schluss
4.1 Kontrastiver Vergleich der beiden Typentheorien
4.2 Beantwortung der Forschungsfrage
Zielsetzung und Themen
Die Arbeit untersucht die Eignung moderner Typentheorien (MTT) im Vergleich zur klassischen simplen Typentheorie (STT) für die formale Repräsentation natürlicher Sprache. Der Fokus liegt dabei auf der Forschungsfrage, ob das "Opfern" der vorteilhaften Eigenschaften der STT durch die MTT zugunsten einer genaueren Modellierung linguistischer Phänomene gerechtfertigt ist, wobei insbesondere die Kriterien Effizienz und Akkuratheit bewertet werden.
- Grundlagen moderner Typentheorien (MTT) wie Universen, Coercive Subtyping und abhängige Typen
- Behandlung lexikalischer Kategorien (Adjektive, Adverbien) in MTTs
- Analyse der Koprädikation mithilfe von Punkttypen und Setoiden
- Kontrastiver Vergleich von MTT und STT (Montague-Grammatik)
- Beurteilung der Effizienz und Akkuratheit bei der formalen Semantik
Auszug aus dem Buch
2.3.2 Coercive Subtyping
Der Subtyping-Mechanismus, den MTTs in der Regel stattdessen nutzen, heißt Coercive Subtyping. Der Begriff Coercion ist hierbei ein zentraler Begriff in einer modernen Typentheorie, der zunächst erläutert werden muss. Eine Coercion wird dann angewendet, wenn eine Nichtübereinstimmung zwischen dem Typen des Prädikats und dem Typen des Arguments vorliegt (vgl. Pustejovsky & Jezek, 2008, S. 186). Zur Demonstration der Wirkungsweise einer Coercion bzw. des Coercive Subtyping dient folgendes Beispiel:
(9) Markus redet.
Dabei nehmen wir an, dass Markus und reden so interpretiert werden:
(10) Markus: [[mann]]
(11) reden: [[mensch]] → Prop
An diesem Beispiel und anhand der dazugehörigen Definitionen lässt sich erkennen, dass hier ein sogenannter Type Clash entstanden ist (vgl. Pustejovsky & Jezek, 2008, S. 186). Die Lösung besteht darin, dass man eine Coercion vom Typ [[mann]] zum Typ [[mensch]] ansetzt (vgl. Luo, 2012, S. 498):
(12) [[mann]] < [[mensch]]
Das bedeutet, dass [[mann]] nun ein Subtyp von [[mensch]] ist und dementsprechend als Argument für das Verb reden verwendet werden kann. Den in (12) vorgestellten Prozess nennt man Coercive Subtyping, da wir erzwungen haben, dass [[mann]] ein Subtyp von [[mensch]] sein soll, damit der Satz in (9) gebildet werden kann. Da [[mann]] ein Subtyp von [[mensch]] ist, bezeichnet man den Beispielsatz auch als well-typed (vgl. Xue & Luo, 2012, S. 238).
Zusammenfassung der Kapitel
1 Einleitung: Definiert das Problem der Repräsentation natürlicher Sprache in formalen Systemen und stellt die Forschungsfrage zur Effizienz und Akkuratheit von MTTs gegenüber STTs.
2 Grundprinzipien und Methoden von MTT: Erläutert die theoretischen Grundlagen der MTT, einschließlich Universen, Coercive Subtyping, eingebetteter Logik sowie abhängiger und simpler Typentheorien.
3 Behandlung von lexikalischen Kategorien und Koprädikation mit Typentheorien: Detaillierte Untersuchung der Modellierung von Adjektiven, Adverbien und komplexer Koprädikation unter Verwendung von Punkttypen und Setoiden.
4 Schluss: Zieht einen kontrastiven Vergleich zwischen MTT und STT und beantwortet die Forschungsfrage zugunsten der Akkuratheit moderner Typentheorien.
Schlüsselwörter
Moderne Typentheorie, MTT, Simple Typentheorie, STT, Coercive Subtyping, Koprädikation, Punkttypen, Formale Semantik, Montague-Grammatik, Induktive Typen, Setoide, Identitätskriterien, Sprachphilosophie, Computerlinguistik, Polysemie.
Häufig gestellte Fragen
Worum geht es in dieser Arbeit grundsätzlich?
Die Arbeit untersucht formale Systeme zur Repräsentation der Bedeutung natürlicher Sprache, wobei sie moderne Typentheorien (MTT) mit der klassischen Montague-Grammatik (basierend auf der simplen Typentheorie, STT) kontrastiert.
Was sind die zentralen Themenfelder?
Die zentralen Themen sind die theoretischen Grundlagen der MTT, deren Anwendung auf lexikalische Kategorien wie Adjektive und Adverbien sowie die komplexe Behandlung von Koprädikation.
Was ist das primäre Ziel oder die Forschungsfrage?
Die Arbeit möchte klären, ob sich das "Opfern" der vorteilhaften Eigenschaften der simplen Typentheorie durch moderne Typentheorien im Hinblick auf eine präzisere, akkuratere Abbildung natürlicher Sprache gelohnt hat.
Welche wissenschaftliche Methode wird verwendet?
Es wird eine kontrastive Analyse verwendet, bei der die beiden Ansätze (MTT und STT) theoretisch eingeführt und anschließend anhand ihrer Vor- und Nachteile bei der Formalisierung linguistischer Phänomene bewertet werden.
Was wird im Hauptteil behandelt?
Der Hauptteil widmet sich der detaillierten Einführung von MTT-Prinzipien (Subtyping, Typen) und der Anwendung dieser auf schwierige linguistische Phänomene wie die Koprädikation, inklusive der Nutzung von Punkttypen und Setoiden.
Welche Schlüsselwörter charakterisieren die Arbeit?
Wichtige Begriffe sind Moderne Typentheorie (MTT), Montague-Grammatik, Coercive Subtyping, Koprädikation, Punkttypen, Setoide und Formale Semantik.
Wie unterscheidet sich die Behandlung der Koprädikation in MTT von anderen Ansätzen?
MTTs verwenden dafür spezielle Mechanismen wie "Punkttypen" und "Setoide", die es erlauben, einem Wort mehrere miteinander assoziierte Bedeutungen zuzuweisen, ohne dass die syntaktische Korrektheit verloren geht.
Warum spielt das Konzept der Identitätskriterien eine so große Rolle bei Quantifizierern?
Identitätskriterien sind entscheidend, um bei Sätzen, die sowohl Koprädikation als auch Quantifizierer enthalten, präzise zwischen verschiedenen Arten von Identität (z. B. physisch vs. informationell) zu unterscheiden.
- Quote paper
- Eray Özbey (Author), Aaron Micha (Author), 2021, Computationelle Perspektive auf moderne Typentheorie, Munich, GRIN Verlag, https://www.grin.com/document/1148625
