Semantik (Logik)

In der Logik beschäftigt sich die Semantik mit der exakten Bedeutung von Termen in Sprachen. In der Informatik soll sie die Semantik eines Computerprogramms syntaktisch ausdrücken und so mathematischen Beweisen zugänglich machen.

In Abgrenzung zur Semantik im allgemeinen Sinn, wie sie vor allem in Philosophie und Linguistik betrieben wird, arbeitet die Semantik in der Logik mit rein formalen, logisch-mathematischen Methoden. Die moderne formale Semantik (in der Linguistik) hat ihren Ursprung in Arbeiten von Alfred Tarski, Richard Montague, Alonzo Church und anderen.

Semantik in der Mathematischen Logik

In der formalen Logik ist die Semantik ein Teilgebiet, das in das Gebiet der 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 erhalten die Symbole und Operationen der syntaktischen Ebene eine Bedeutung. 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]

Semantik in der Theoretischen Informatik

Als Semantik bezeichnet man ein Teilgebiet der theoretischen Informatik, in dem die Bedeutung von Computerprogrammen und Spezifikationen formalisiert wird, um beispielsweise den Nachweis der Korrektheit von Computerprogrammen zu erbringen (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, welche die Lösbarkeit von Problemen durch Computerprogramme untersucht.

Die 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.

Dabei 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.

Literatur

  • Joseph E. Stoy: Denotational Semantics. The Scott-Strachey Approach to Programming Language Semantics (The MIT Press Series in Computer Sciences; Bd. 1). 5. Aufl. MIT Press, Cambridge, Mass. 1989, ISBN 0-87630-751-9 (EA Cambridge 1977).
  • Jan van Leeuwen (Hrsg.): Handbook of Theoretical Computer Science, Bd. B: Formal models and semantics. Elsevier MIT Press, Cambridge, Mass. 1990, ISBN 0-262-22039-3.
  • Michael Main (Hrsg.): Mathematical Foundations of Programming Language Semantics (Lecture Notes in Computer Science; Bd. 298). Springer, Berlin 1988, ISBN 3-540-19020-1.
  • Austin Melton (Hrsg.): Mathematical Foundations of Programming Semantics (Lecture Notes in Computer Science; Bd. 239). Springer, Berlin 1986, ISBN 3-540-16816-8.
  • Manfred Droste, Yuri Gurevich (Hrsg.): Semantics of Programming Languages and Model Theory (Algebra, Logic, and Application; Bd. 5). CRC Press, Langhorne, Pa. 1993, ISBN 2-88124-935-3.

Einzelnachweise

  1. ↑ Alfred Tarski (Autor), John Corcoran (Hrsg.): Logic, Semantics, Metamathematics. Papers from 1923 to 1938. Hackett Publ., Indianapolis, Ind. 1983, ISBN 0915144-75-1.