Semantics (logic)
In logic , semantics deals with the exact meaning of terms in languages. In computer science , it should express the semantics of a computer program syntactically and thus make mathematical proofs accessible.
In contrast to semantics in the general sense, as it is mainly used in philosophy and linguistics , semantics in logic works with purely formal, logical-mathematical methods. Modern formal semantics (in linguistics) has its origins in the work of Alfred Tarski , Richard Montague , Alonzo Church, and others.
Semantics in Mathematical Logic
In formal logic , semantics is a sub-area that falls into the area of model theory . The counterpart to formal semantics in logic is formal syntax , which deals with mechanical (i.e., content-indefinite) operations with meaningless symbols in the context of calculi . The symbols and operations of the syntactic level are only given meaning through semantics that match the syntax. This makes it possible to examine the relationships between syntax and semantics of a formal system within the framework of model theory and to prove statements about (semantic) completeness and correctness . The pioneer of modern formal semantics in logic was Alfred Tarski .
Semantics in Theoretical Computer Science
Semantics is a branch of theoretical computer science that deals with formalizing the meaning of computer programs and specifications . This is required , for example, to prove the correctness of computer programs ( verification ). Unlike linguistic semantics , which is part of linguistics , formal semantics work with entirely mathematical methods. It is closely related to computability theory , which deals with which problems can be solved with computer programs at all.
The aim of semantics is to express the meaning of computer programs in a formal language - it is supposed to express the semantics of a computer program syntactically so that statements about the program can be proven by applying derivation rules ( calculi ).
The following calculations are used:
- denotational semantics : construction of semantics using mathematical spaces from area theory ; the semantics of a program are assigned by a function.
- axiomatic semantics : description of semantics by their logical properties, whereby in general only some properties are considered.
- Operational semantics : the possible execution steps are described as pairs (state, successor state) through a state transition function or relation .
- algebraic semantics : is a combination of algebra and formal languages.
literature
- Joseph E. Stoy: Denotational Semantics. The Scott-Strachey Approach to Programming Language Semantics (The MIT Press Series in Computer Sciences; Vol. 1). 5th ed. MIT Press, Cambridge, Mass. 1989, ISBN 0-87630-751-9 (EA Cambridge 1977).
- Jan van Leeuwen (Ed.): Handbook of Theoretical Computer Science, Vol. B: Formal models and semantics . Elsevier MIT Press, Cambridge, Mass. 1990, ISBN 0-262-22039-3 .
- Michael Main (Ed.): Mathematical Foundations of Programming Language Semantics (Lecture Notes in Computer Science; Vol. 298). Springer, Berlin 1988, ISBN 3-540-19020-1 .
- Austin Melton (Ed.): Mathematical Foundations of Programming Semantics (Lecture Notes in Computer Science; Vol. 239). Springer, Berlin 1986, ISBN 3-540-16816-8 .
- Manfred Droste, Yuri Gurevich (Ed.): Semantics of Programming Languages and Model Theory (Algebra, Logic, and Application; Vol. 5). CRC Press, Langhorne, Pa. 1993, ISBN 2-88124-935-3 .
Web links
- "Denotational Semantics" L. Allison, Faculty of Information Technology (Clayton), Monash University, Australia, 1996, 1997, 2001
- "Structure of Programming Languages I: Denotational Semantics" Wolfgang Schreiner, RISC: Research Institute for Symbolic Computation institute of the Johannes Kepler University Linz, Austria, 1995
Individual evidence
- ^ Alfred Tarski (author), John Corcoran (ed.): Logic, Semantics, Metamathematics. Papers from 1923 to 1938 . Hackett Publ., Indianapolis, Ind. 1983, ISBN 0915144-75-1 .