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.

Formale Semantik in der Informatik

Die formale Semantik ist ein Teilgebiet der theoretischen Informatik, das sich mit dem Nachweis der Korrektheit von Computerprogrammen beschäftigt (Verifikation). Anders als die linguistische Semantik, die ein Teil der Linguistik ist, arbeitet die formale Semantik mit vollständig mathematischen Methoden, um die Bedeutung von Computerprogrammen und Spezifikationen zu formalisieren. 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:

denotationale Semantik: Konstruktion der Semantik mittels mathematischer Räume aus der Bereichstheorie; die Semantik eines Programms ist eine Funktion.
axiomatische Semantik: Beschreibung der Semantik durch ihre logischen Eigenschaften, wobei i.Allg. nur einige Eigenschaften betrachtet werden.
operationale Semantik: durch eine Relation werden die möglichen Ausführungsschritte als Paare (Programm, Zustand) beschrieben.

Formale Semantik in der Linguistik

Die formale Semantik als Teilgebiet der Linguistik befasst sich mit der Bedeutung von Sätzen. 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.

Die formale Semantik unterscheidet sich grundlegend von der kognitiven Semantik.

Siehe auch

Literatur (Linguistik)

Irene Heim und Angelika Kratzer: Semantics in Generative Grammar Oxford: Blackwell, 1998.

Literatur (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.

Weblinks

http://www.csse.monash.edu.au/~lloyd/tilde/Semantics/
http://www.risc.uni-linz.ac.at/people/schreine/courses/densem/densem.html
http://www.cl.cam.ac.uk/Teaching/Lectures/dens/

Theoretische Informatik | Semantik