Semantics (computer science)

Formal semantics is concerned with the exact meaning of artificial or natural languages. It can be set both the importance of existing languages ​​studied as well as the importance of newly created languages. In contrast to the semantics in a general sense, as it is practiced mainly in philosophy and linguistics, formal semantics works with purely formal, logical- mathematical methods.

Formal semantics is operated in logic, in theoretical computer science and in linguistics. Because of the importance of exact theories of meaning for these three disciplines and because of different priorities and objectives - partly because of different methods - has any of these sciences today a private subspecialty that is called formal semantics. The formal semantics of logic, those from theoretical computer science and the formal semantics of linguistics, however, are intertwined in many ways and are frequently engage each other back or on the results of each other.

The modern formal semantics has its origins in the work of Alfred Tarski, Richard Montague, Alonzo Church, and others.

Formal semantics in logic

In formal logic, the semantics is a branch that falls under the concept of model theory. The counterpart to the formal semantics is the formal syntax in which it comes to mechanical, ie content indefinite operations with meaningless symbols in the context of calculi in the logic. Only by matching the syntax semantics of the symbols and operations of the syntactic level are provided with meanings. This makes it possible to investigate 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.

Formal semantics in computer science

The formal semantics is a branch of theoretical computer science, which deals with the formalizing importance of computer programs and specifications. This is for example for the detection of the correctness of computer programs required (verification). Unlike the linguistic semantic, which is a part of linguistics, the formal semantics uses full mathematical methods. It is closely related to computability theory, which is busy, what problems can be solved with computer programs at all.

The formal semantics aims to express the importance of computer programs in a formal language - so they should express the semantics of a computer program syntactically, so that it is possible through the application of inference rules ( calculi ) prove statements about the program.

In the formal semantics following calculi are used:

• Denotational semantics: construction of the semantics by means of mathematical spaces from the field theory; the semantics of a program is assigned by a function.
• Axiomatic semantics: The semantics through their logical properties, generally only be considered some properties.
• Operational semantics: by a state transition function or relation, the possible execution steps described as pairs ( state, successor state ).
• Algebraic semantics: is a compound of algebra and formal languages ​​.

Formal semantics in linguistics

In linguistics, the formal semantics is a semantics that is operated with the help of logic and mathematics. The meaning of sentences is captured using a formal meta-language. Building on the compositionality of Gottlob Frege is researching what the different parts of a sentence contribute to its overall significance. The interaction of the individual components of the sentence is achieved by a formalization of natural language with the help of Montaguegrammatiken and similar methods.

The formal semantics is compatible with various syntactic models such as the minimalist program, the categorial or Functional Grammar.

In the formal semantics of the lambda - abstraction is used " from a formula to generate predicates that represent individuals as generalized quantifiers and formalize the semantics of quantifiers and determinants [ to ]. " The opposite of the lambda abstraction is the lambda conversion.