- Formale Semantik
-
Formale Semantik beschäftigt sich mit der exakten Bedeutung von künstlichen oder natürlichen Sprachen. Dabei kann sowohl die Bedeutung bestehender Sprachen untersucht als auch die Bedeutung neu geschaffener Sprachen festgelegt werden. In Abgrenzung zur Semantik im allgemeinen Sinn, wie sie vor allem in Philosophie und Linguistik betrieben wird, arbeitet die formale Semantik mit rein formalen, logisch-mathematischen Methoden.
Formale Semantik wird in der Logik, in der theoretischen Informatik und in der Linguistik betrieben. Wegen der Wichtigkeit exakter Bedeutungstheorie für die genannten drei Disziplinen und wegen unterschiedlicher Schwerpunkte und Zielsetzungen – teils auch wegen unterschiedlicher Methoden – hat jede dieser Wissenschaften heute ein eigenes Teilgebiet, das als formale Semantik bezeichnet wird. Die formale Semantik aus Logik, jene aus theoretischer Informatik und die formale Semantik aus Linguistik sind jedoch in vielerlei Hinsicht miteinander verflochten und greifen häufig aufeinander bzw. auf die Ergebnisse der jeweils anderen zurück.
Die moderne formale Semantik hat ihren Ursprung in Arbeiten von Alfred Tarski, Richard Montague, Alonzo Church und anderen.
Inhaltsverzeichnis
Formale Semantik in der Logik
In der formalen Logik ist die Semantik ein Teilgebiet, das unter den Begriff Modelltheorie fällt. Das Gegenstück zur formalen Semantik ist in der Logik die formale Syntax, bei der es um mechanische, das heißt inhaltlich unbestimmte Operationen mit bedeutungslosen Symbolen im Rahmen von Kalkülen geht. Erst durch eine zur Syntax passende Semantik werden die Symbole und Operationen der syntaktischen Ebene mit Bedeutungen versehen. Damit wird es möglich, im Rahmen der Modelltheorie die Zusammenhänge zwischen Syntax und Semantik eines formalen Systems zu untersuchen und Aussagen über (semantische) Vollständigkeit und Korrektheit zu beweisen. Der Pionier der modernen formalen Semantik in der Logik war Alfred Tarski.[1]
Formale Semantik in der Informatik
Die formale Semantik ist ein Teilgebiet der theoretischen Informatik, das sich damit beschäftigt, Bedeutung von Computerprogrammen und Spezifikationen zu formalisieren. Dies wird zum Beispiel für den Nachweis der Korrektheit von Computerprogrammen benötigt (Verifikation). Anders als die linguistische Semantik, die ein Teil der Linguistik ist, arbeitet die formale Semantik mit vollständig mathematischen Methoden. Sie ist eng verwandt mit der Berechenbarkeitstheorie, die sich damit beschäftigt, welche Probleme mit Computerprogrammen überhaupt gelöst werden können.
Die formale Semantik hat zum Ziel, die Bedeutung von Computerprogrammen in einer formalen Sprache auszudrücken – sie soll also die Semantik eines Computerprogramms syntaktisch ausdrücken, so dass sich über das Anwenden von Ableitungsregeln (Kalkülen) Aussagen über das Programm beweisen lassen.
In der formalen Semantik finden folgende Kalküle Verwendung:
- denotationelle Semantik: Konstruktion der Semantik mittels mathematischer Räume aus der Bereichstheorie; die Semantik eines Programms wird durch eine Funktion zugewiesen.
- axiomatische Semantik: Beschreibung der Semantik durch ihre logischen Eigenschaften, wobei im Allgemeinen nur einige Eigenschaften betrachtet werden.
- operationelle Semantik: durch eine Zustandsübergangsfunktion oder Relation werden die möglichen Ausführungsschritte als Paare (Zustand, Nachfolgezustand) beschrieben.
- algebraische Semantik: ist eine Verbindung von Algebra und formalen Sprachen.
- Attributierte Grammatiken: Definition einer formalen Semantik mit Hilfe von Attributgleichungen.
- Referenzimplementierungen
Formale Semantik in der Linguistik
In der Linguistik ist die formale Semantik eine Semantik, die mit Hilfe der Logik und Mathematik betrieben wird. Die Bedeutung von Sätzen wird mit Hilfe einer formalen Metasprache erfasst. Aufbauend auf dem Kompositionalitätsprinzip von Gottlob Frege wird erforscht, was die einzelnen Teile eines Satzes zu dessen Gesamtbedeutung beitragen. Das Zusammenwirken der einzelnen Bestandteile des Satzes wird durch eine Formalisierung der natürlichen Sprache mit Hilfe von Montaguegrammatiken und ähnlichen Methoden erreicht.
Die formale Semantik ist mit verschiedenen syntaktischen Modellen wie dem minimalistischen Programm, der Kategorialgrammatik oder der Functional Grammar kompatibel.
In der formalen Semantik dient die Lambda-Abstraktion dazu, "aus einer Formel Prädikate zu erzeugen, Individuen als generalisierte Quantoren darzustellen und die Semantik von Quantoren und Determinanten [zu] formalisieren."[2] Das Gegenteil der Lambda-Abstraktion ist die Lambda-Konversion.
Siehe auch
Literatur
Linguistik
- Johannes Heinrichs: Sprache. Band 2: Die Bedeutungsdimension.(Semantik), Philosophische Semiotik Teil II, Steno München 2008. ISBN 978-954-449-351-6
- Irene Heim und Angelika Kratzer: Semantics in Generative Grammar Oxford: Blackwell, 1998.
- Horst Lohnstein: Formale Semantik und natürliche Sprache: einführendes Lehrbuch Opladen: Westdeutscher Verlag, 1996. ISBN 3-531-12818-3
- Monika Schwarz, Jeanette Chur: Semantik: ein Arbeitsbuch, 5. Aufl., Tübingen: Gunter Narr, 2007. ISBN 978-3-8233-6296-8 (Einführung; Seite 115 -191)
Informatik
- Joseph E. Stoy: Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge, Massachusetts, 1977.
- Jan van Leeuwen: Handbook of Theoretical Computer Science, Volume B. Elsevier / MIT Press, 1990.
- Michael Main: Mathematical Foundations of Programming Language Semantics. Springer, 1988.
- Austin Melton: Mathematical Foundations of Programming Semantics. Springer, 1986.
- Manfred Droste, Yuri Gurevich: Semantics of Programming Languages and Model Theory. CRC Press, 1993.
Weblinks
Einzelnachweise
- ↑ Tarski, A. 1983, Logic, Semantics, Metamathematics, papers from 1923 to 1938, ed. John Corcoran, Indianapolis : Hackett Publishing Company.
- ↑ Monika Schwarz, Jeanette Chur: Semantik. - 5. Aufl. - G. Narr, Tübingen 2007, S. 156
Kategorien:- Theoretische Informatik
- Semantik (Philosophie)
- Semantik
Wikimedia Foundation.
