Semantics (computer science)

Last updated November 30, 2024

In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages.^[1] Semantics assigns computational meaning to valid strings in a programming language syntax. It is closely related to, and often crosses over with, the semantics of mathematical proofs.

Semantics describes the processes a computer follows when executing a program in that specific language. This can be done by describing the relationship between the input and output of a program, or giving an explanation of how the program will be executed on a certain platform, thereby creating a model of computation.

History

In 1967, Robert W. Floyd published the paper Assigning meanings to programs; his chief aim was "a rigorous standard for proofs about computer programs, including proofs of correctness, equivalence, and termination".^[2]^[3] Floyd further wrote:^[2]

A semantic definition of a programming language, in our approach, is founded on a syntactic definition. It must specify which of the phrases in a syntactically correct program represent commands, and what conditions must be imposed on an interpretation in the neighborhood of each command.

In 1969, Tony Hoare published a paper on Hoare logic seeded by Floyd's ideas, now sometimes collectively called axiomatic semantics .^[4]^[5]

In the 1970s, the terms operational semantics and denotational semantics emerged.^[5]

Overview

The field of formal semantics encompasses all of the following:

The definition of semantic models
The relations between different semantic models
The relations between different approaches to meaning
The relation between computation and the underlying mathematical structures from fields such as logic, set theory, model theory, category theory, etc.

It has close links with other areas of computer science such as programming language design, type theory, compilers and interpreters, program verification and model checking.

Approaches

There are many approaches to formal semantics; these belong to three major classes:

Denotational semantics ,^[6] whereby each phrase in the language is interpreted as a denotation , i.e. a conceptual meaning that can be thought of abstractly. Such denotations are often mathematical objects inhabiting a mathematical space, but it is not a requirement that they should be so. As a practical necessity, denotations are described using some form of mathematical notation, which can in turn be formalized as a denotational metalanguage. For example, denotational semantics of functional languages often translate the language into domain theory. Denotational semantic descriptions can also serve as compositional translations from a programming language into the denotational metalanguage and used as a basis for designing compilers.
Operational semantics ,^[7] whereby the execution of the language is described directly (rather than by translation). Operational semantics loosely corresponds to interpretation, although again the "implementation language" of the interpreter is generally a mathematical formalism. Operational semantics may define an abstract machine (such as the SECD machine), and give meaning to phrases by describing the transitions they induce on states of the machine. Alternatively, as with the pure lambda calculus, operational semantics can be defined via syntactic transformations on phrases of the language itself;
Axiomatic semantics ,^[8] whereby one gives meaning to phrases by describing the axioms that apply to them. Axiomatic semantics makes no distinction between a phrase's meaning and the logical formulas that describe it; its meaning is exactly what can be proven about it in some logic. The canonical example of axiomatic semantics is Hoare logic.

Apart from the choice between denotational, operational, or axiomatic approaches, most variations in formal semantic systems arise from the choice of supporting mathematical formalism.^{[ citation needed ]}

Variations

Some variations of formal semantics include the following:

Action semantics ^[9] is an approach that tries to modularize denotational semantics, splitting the formalization process in two layers (macro and microsemantics) and predefining three semantic entities (actions, data and yielders) to simplify the specification;
Algebraic semantics ^[8] is a form of axiomatic semantics based on algebraic laws for describing and reasoning about program semantics in a formal manner. It also supports denotational semantics and operational semantics;
Attribute grammars ^[10] define systems that systematically compute "metadata" (called attributes) for the various cases of the language's syntax. Attribute grammars can be understood as a denotational semantics where the target language is simply the original language enriched with attribute annotations. Aside from formal semantics, attribute grammars have also been used for code generation in compilers, and to augment regular or context-free grammars with context-sensitive conditions;
Categorical (or "functorial") semantics^[11] uses category theory as the core mathematical formalism. Categorical semantics is usually proven to correspond to some axiomatic semantics that gives a syntactic presentation of the categorical structures. Also, denotational semantics are often instances of a general categorical semantics;^[12]
Concurrency semantics ^[13] is a catch-all term for any formal semantics that describes concurrent computations. Historically important concurrent formalisms have included the actor model and process calculi;
Game semantics ^[14] uses a metaphor inspired by game theory;
Predicate transformer semantics ,^[15] developed by Edsger W. Dijkstra, describes the meaning of a program fragment as the function transforming a postcondition to the precondition needed to establish it.

Describing relationships

For a variety of reasons, one might wish to describe the relationships between different formal semantics. For example:

To prove that a particular operational semantics for a language satisfies the logical formulas of an axiomatic semantics for that language. Such a proof demonstrates that it is "sound" to reason about a particular (operational) interpretation strategy using a particular (axiomatic) proof system.
To prove that operational semantics over a high-level machine is related by a simulation with the semantics over a low-level machine, whereby the low-level abstract machine contains more primitive operations than the high-level abstract machine definition of a given language. Such a proof demonstrates that the low-level machine "faithfully implements" the high-level machine.

It is also possible to relate multiple semantics through abstractions via the theory of abstract interpretation.^{[ citation needed ]}

Related Research Articles

In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules called a formal grammar.

In computer science, denotational semantics is an approach of formalizing the meanings of programming languages by constructing mathematical objects that describe the meanings of expressions from the languages. Other approaches providing formal semantics of programming languages include axiomatic semantics and operational semantics.

In mathematics and logic, an axiomatic system is any set of primitive notions and axioms to logically derive theorems. A theory is a consistent, relatively-self-contained body of knowledge which usually contains an axiomatic system and all its derived theorems. An axiomatic system that is completely described is a special kind of formal system. A formal theory is an axiomatic system that describes a set of sentences that is closed under logical implication. A formal proof is a complete rendition of a mathematical proof within a formal system.

In linguistics and philosophy, the denotation of a word or expression is its strictly literal meaning. For instance, the English word "warm" denotes the property of having high temperature. Denotation is contrasted with other aspects of meaning including connotation. For instance, the word "warm" may evoke calmness, coziness, or kindness but these associations are not part of the word's denotation. Similarly, an expression's denotation is separate from pragmatic inferences it may trigger. For instance, describing something as "warm" often implicates that it is not hot, but this is once again not part of the word's denotation.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification is a key incentive for formal specification of systems, and is at the core of formal methods. It represents an important dimension of analysis and verification in electronic design automation and is one approach to software verification. The use of formal verification enables the highest Evaluation Assurance Level (EAL7) in the framework of common criteria for computer security certification.

Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms. Operational semantics are classified in two categories: structural operational semantics formally describe how the individual steps of a computation take place in a computer-based system; by opposition natural semantics describe how the overall results of the executions are obtained. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics.

A formal system is an abstract structure and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms by a set of inference rules.

Computational semiotics is an interdisciplinary field that applies, conducts, and draws on research in logic, mathematics, the theory and practice of computation, formal and natural language studies, the cognitive sciences generally, and semiotics proper. The term encompasses both the application of semiotics to computer hardware and software design and, conversely, the use of computation for performing semiotic analysis. The former focuses on what semiotics can bring to computation; the latter on what computation can bring to semiotics.

Axiomatic semantics is an approach based on mathematical logic for proving the correctness of computer programs. It is closely related to Hoare logic.

Concurrency refers to the ability of a system to execute multiple tasks through simultaneous execution or time-sharing, sharing resources and managing interactions. Concurrency improves responsiveness, throughput, and scalability in modern computing, including:

In semantics, mathematical logic and related disciplines, the principle of compositionality is the principle that the meaning of a complex expression is determined by the meanings of its constituent expressions and the rules used to combine them. The principle is also called Frege's principle, because Gottlob Frege is widely credited for the first modern formulation of it. However, the principle has never been explicitly stated by Frege, and arguably it was already assumed by George Boole decades before Frege's work.

In logic and mathematics, a formal proof or derivation is a finite sequence of sentences, each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence, according to the rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable. If the set of assumptions is empty, then the last sentence in a formal proof is called a theorem of the formal system. The notion of theorem is generally effective, but there may be no method by which we can reliably find proof of a given sentence or determine that none exists. The concepts of Fitch-style proof, sequent calculus and natural deduction are generalizations of the concept of proof.

<span class="mw-page-title-main">Joseph Goguen</span> American computer scientist

Joseph Amadee Goguen was an American computer scientist. He was professor of Computer Science at the University of California and University of Oxford, and held research positions at IBM and SRI International.

Gordon David Plotkin is a theoretical computer scientist in the School of Informatics at the University of Edinburgh. Plotkin is probably best known for his introduction of structural operational semantics (SOS) and his work on denotational semantics. In particular, his notes on A Structural Approach to Operational Semantics were very influential. He has contributed to many other areas of computer science.

Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is closely related to other fields including mathematics, software engineering, and linguistics. There are a number of academic conferences and journals in the area.

The term "information algebra" refers to mathematical techniques of information processing. Classical information theory goes back to Claude Shannon. It is a theory of information transmission, looking at communication and storage. However, it has not been considered so far that information comes from different sources and that it is therefore usually combined. It has furthermore been neglected in classical information theory that one wants to extract those parts out of a piece of information that are relevant to specific questions.

Logic is the formal science of using reason and is considered a branch of both philosophy and mathematics and to a lesser extent computer science. Logic investigates and classifies the structure of statements and arguments, both through the study of formal systems of inference and the study of arguments in natural language. The scope of logic can therefore be very large, ranging from core topics such as the study of fallacies and paradoxes, to specialized analyses of reasoning such as probability, correct reasoning, and arguments involving causality. One of the aims of logic is to identify the correct and incorrect inferences. Logicians study the criteria for the evaluation of arguments.

In computer science, algebraic semantics is a form of axiomatic semantics based on algebraic laws for describing and reasoning about program specifications in a formal manner.

In linguistics, the term formalism is used in a variety of meanings which relate to formal linguistics in different ways. In common usage, it is merely synonymous with a grammatical model or a syntactic model: a method for analyzing sentence structures. Such formalisms include different methodologies of generative grammar which are especially designed to produce grammatically correct strings of words; or the likes of Functional Discourse Grammar which builds on predicate logic.

References

↑ Goguen, Joseph A. (1975). "Semantics of computation". Category Theory Applied to Computation and Control. Lecture Notes in Computer Science. Vol. 25. Springer. pp. 151–163. doi:10.1007/3-540-07142-3_75. ISBN 978-3-540-07142-6.
1 2 Floyd, Robert W. (1967). "Assigning Meanings to Programs" (PDF). In Schwartz, J.T. (ed.). Mathematical Aspects of Computer Science. Proceedings of Symposium on Applied Mathematics. Vol. 19. American Mathematical Society. pp. 19–32. ISBN 0821867288.
↑ Knuth, Donald E. "Memorial Resolution: Robert W. Floyd (1936–2001)" (PDF). Stanford University Faculty Memorials. Stanford Historical Society.
↑ Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming". Communications of the ACM . 12 (10): 576–580. doi: 10.1145/363235.363259 . S2CID 207726175.
1 2 Winskel, Glynn (1993). The formal semantics of programming languages : an introduction. Cambridge, Mass.: MIT Press. p. xv. ISBN 978-0-262-23169-5.
↑ Schmidt, David A. (1986). Denotational Semantics: A Methodology for Language Development. William C. Brown Publishers. ISBN 9780205104505.
↑ Plotkin, Gordon D. (1981). A structural approach to operational semantics (Report). Technical Report DAIMI FN-19. Computer Science Department, Aarhus University.
1 2 Goguen, Joseph A.; Thatcher, James W.; Wagner, Eric G.; Wright, Jesse B. (1977). "Initial algebra semantics and continuous algebras". Journal of the ACM . 24 (1): 68–95. doi: 10.1145/321992.321997 . S2CID 11060837.
↑ Mosses, Peter D. (1996). Theory and practice of action semantics (Report). BRICS Report RS9653. Aarhus University.
↑ Deransart, Pierre; Jourdan, Martin; Lorho, Bernard (1988). "Attribute Grammars: Definitions, Systems and Bibliography. Lecture Notes in Computer Science 323. Springer-Verlag. ISBN 9780387500560.
↑ Lawvere, F. William (1963). "Functorial semantics of algebraic theories". Proceedings of the National Academy of Sciences of the United States of America . 50 (5): 869–872. Bibcode:1963PNAS...50..869L. doi: 10.1073/pnas.50.5.869 . PMC 221940 . PMID 16591125.
↑ Andrzej Tarlecki; Rod M. Burstall; Joseph A. Goguen (1991). "Some fundamental algebraic tools for the semantics of computation: Part 3. Indexed categories". Theoretical Computer Science . 91 (2): 239–264. doi: 10.1016/0304-3975(91)90085-G .
↑ Batty, Mark; Memarian, Kayvan; Nienhuis, Kyndylan; Pichon-Pharabod, Jean; Sewell, Peter (2015). "The problem of programming language concurrency semantics" (PDF). Proceedings of the European Symposium on Programming Languages and Systems. Springer. pp. 283–307. doi: 10.1007/978-3-662-46669-8_12 .
↑ Abramsky, Samson (2009). "Semantics of interaction: An introduction to game semantics". In Andrew M. Pitts; P. Dybjer (eds.). Semantics and Logics of Computation. Cambridge University Press. pp. 1–32. doi:10.1017/CBO9780511526619.002. ISBN 9780521580571.
↑ Dijkstra, Edsger W. (1975). "Guarded commands, nondeterminacy and formal derivation of programs". Communications of the ACM . 18 (8): 453–457. doi: 10.1145/360933.360975 . S2CID 1679242.

External links

Aaby, Anthony (2004). Introduction to Programming Languages. Archived from the original on 2015-06-19. Semantics.

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[1] Goguen, Joseph A. (1975). "Semantics of computation". Category Theory Applied to Computation and Control. Lecture Notes in Computer Science. Vol. 25. Springer. pp. 151–163. doi:10.1007/3-540-07142-3_75. ISBN 978-3-540-07142-6.

[floyd-2] 1 2 Floyd, Robert W. (1967). "Assigning Meanings to Programs" (PDF). In Schwartz, J.T. (ed.). Mathematical Aspects of Computer Science. Proceedings of Symposium on Applied Mathematics. Vol. 19. American Mathematical Society. pp. 19–32. ISBN 0821867288.

[3] Knuth, Donald E. "Memorial Resolution: Robert W. Floyd (1936–2001)" (PDF). Stanford University Faculty Memorials. Stanford Historical Society.

[hoare-4] Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming". Communications of the ACM . 12 (10): 576–580. doi: 10.1145/363235.363259 . S2CID 207726175.

[winskel-5] 1 2 Winskel, Glynn (1993). The formal semantics of programming languages : an introduction. Cambridge, Mass.: MIT Press. p. xv. ISBN 978-0-262-23169-5.

[Schmidt1986-6] Schmidt, David A. (1986). Denotational Semantics: A Methodology for Language Development. William C. Brown Publishers. ISBN 9780205104505.

[Plotkin1981-7] Plotkin, Gordon D. (1981). A structural approach to operational semantics (Report). Technical Report DAIMI FN-19. Computer Science Department, Aarhus University.

[Goguen77-8] 1 2 Goguen, Joseph A.; Thatcher, James W.; Wagner, Eric G.; Wright, Jesse B. (1977). "Initial algebra semantics and continuous algebras". Journal of the ACM . 24 (1): 68–95. doi: 10.1145/321992.321997 . S2CID 11060837.

[Mosses1996-9] Mosses, Peter D. (1996). Theory and practice of action semantics (Report). BRICS Report RS9653. Aarhus University.

[10] Deransart, Pierre; Jourdan, Martin; Lorho, Bernard (1988). "Attribute Grammars: Definitions, Systems and Bibliography. Lecture Notes in Computer Science 323. Springer-Verlag. ISBN 9780387500560.

[Lawvere1963-11] Lawvere, F. William (1963). "Functorial semantics of algebraic theories". Proceedings of the National Academy of Sciences of the United States of America . 50 (5): 869–872. Bibcode:1963PNAS...50..869L. doi: 10.1073/pnas.50.5.869 . PMC 221940 . PMID 16591125.

[12] Andrzej Tarlecki; Rod M. Burstall; Joseph A. Goguen (1991). "Some fundamental algebraic tools for the semantics of computation: Part 3. Indexed categories". Theoretical Computer Science . 91 (2): 239–264. doi: 10.1016/0304-3975(91)90085-G .

[13] Batty, Mark; Memarian, Kayvan; Nienhuis, Kyndylan; Pichon-Pharabod, Jean; Sewell, Peter (2015). "The problem of programming language concurrency semantics" (PDF). Proceedings of the European Symposium on Programming Languages and Systems. Springer. pp. 283–307. doi: 10.1007/978-3-662-46669-8_12 .

[Abramsky2009-14] Abramsky, Samson (2009). "Semantics of interaction: An introduction to game semantics". In Andrew M. Pitts; P. Dybjer (eds.). Semantics and Logics of Computation. Cambridge University Press. pp. 1–32. doi:10.1017/CBO9780511526619.002. ISBN 9780521580571.

[Dijkstra1975-15] Dijkstra, Edsger W. (1975). "Guarded commands, nondeterminacy and formal derivation of programs". Communications of the ACM . 18 (8): 453–457. doi: 10.1145/360933.360975 . S2CID 1679242.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]