In this story we start from the known definition for Expressive power to extend its scope to semantics programming languages, which have numerous ways to express the specific meanings (below 8 formalismis are listed) of tems of languages. We suggest that (near) all of these semantic principles can be combined in the atomistic semantics, which is a novel hybrid construction, a high-abstraction way to simulate source code.
What is Expressive power
Expressive power is in computer science a feature of a language, which refers to:
- what can be said in the language (at all)
- how concisely it can be said.
Formal discussions mostly use the term in the first sense, leaving conciseness as a less important factor. This is the case in areas of mathematics that deal with the exact description of languages and their meaning, such as formal language theory, mathematical logic and process algebra.
In informal discussions, the term often refers to the second sense, or to both. This is often the case when discussing programming languages. Efforts have been made to formalize these informal uses of the term .
The notion of expressive power is always relative to a particular kind of thing that the language in question can describe, and the term is normally used when comparing languages that describe the same kind of things, or at least comparable kinds of things.
The design of languages and formalisms involves a trade-off between expressive power and analyzability. The more a formalism can express, the harder it becomes to understand what instances of the formalism say. Decision problems become harder to answer or completely undecidable.
Formal language theory mostly studies formalisms to describe sets of strings, such as context-free grammars and regular expressions. Each instance of a formalism, e.g. each grammar and each regular expression, describes a particular set of strings. In this context, the expressive power of a formalism is the set of sets of strings its instances describe, and comparing expressive power is a matter of comparing these sets.
An important yardstick for describing the relative expressive power of formalisms in this area is the Chomsky hierarchy.
Expressive power means one quality attribute of programming language semantics
There are some ways to describe expressive power of each language term (e.g. clause).
1) Axiomatic semantics
- Axiomatic semantics define the meaning of a command in a program by describing its effect on assertions about the program state. The assertions are logical statements – predicates with variables, where the variables define the state of the program.
2) Algebraic semantics
- In logic, algebraic semantics is a formal semantics based on algebras.
3) Operational semantics
- Operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics.
4) Denotational semantics
- Denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects (called denotations) which describe the meanings of expressions from the languages. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and operational semantics.
- Denotational semantics is concerned with finding mathematical objects called domains that represent what programs do. For example, programs (or program phrases) might be represented by partial functions, or by Actor event diagram scenarios, or by games between the environment and the system
5) Action semantics
- Action semantics 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
6) WP-semantics / Predicate transformer semantics
- Predicate transformer semantics is an extension of Floyd-Hoare Logic invented by Dijkstra and extended and refined by other researchers. It was first introduced in Dijkstra’s paper “Guarded commands, nondeterminacy and formal derivation of programs”. It is a method for defining the semantics of an imperative programming language by assigning to each command in the language a corresponding predicate transformer. A predicate transformer is a total function mapping between two predicates on the state space of a program.
- The canonical predicate transformer of sequential imperative programming is the so-called “weakest precondition” wp(S,R). Here S denotes a list of commands and R denotes a predicate on the space, called the “postcondition“. The result of applying this function gives the “weakest pre-condition” for S terminating with R true. An example is the following definition of the assignment statement:
This gives a predicate that is a copy of R with the value of x replaced by E.
- Refinement calculus is a formalized approach to stepwise refinement for program construction. The required behaviour of the final executable program is specified as an abstract and perhaps non-executable “program”, which is then refined by a series of correctness-preserving transformations into an efficiently executable program.
7) Hoare’s axiomatic semantics e.g. Hoare logic
- Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers. The original ideas were seeded by the work of Robert Floyd, who had published a similar system for flowcharts.
- The central feature of Hoare logic is the Hoare triple. A triple describes how the execution of a piece of code changes the state of the computation. A Hoare triple is of the form
- where P and Q are assertions and C is a command. P is called the precondition and Q the postcondition: if the precondition is met, the command establishes the postcondition. Assertions are formulas in predicate logic.
- Hoare logic has axioms and inference rules for all the constructs of a simple imperative programming language. In addition to the rules for the simple language in Hoare’s original paper, rules for other language constructs have been developed since then by Hoare and many other researchers. There are rules for concurrency, procedures, jumps, and pointers.
Atomistic semantics is a hybrid construction, whose expressive power comes from Prolog, a first order predicate logic extended for logic programming. Its type system is rich in expressing any axiomatic feature. The other side of that semantics is object-oriented. That makes it possible to define algebraic equations, formulas or any dependendies using object handles and their static counterparts, tree-based Prolog references, as the base.
There is no research to compare atomistic semantics with denotational semantics, but there are many comparisons between Lisp and Prolog. They are rather compatible to express complicated models and functions, even Lisp is more generic in expressing meta-features. The latter one is not important in expressing features from source code (when ignoring macros and precompilers).
Operational semantics is the hardest one, having two levels.
Below our summary as a picture.
Expressive power of a formalism
If two formalisms have equal power, then it is possible to express same kind of methods (working practices from the user point-of-view) using tools of the corresponding formalisms. In program comprehension (PC) there are multiple needs for the user to do: to define hypotheses, to learn structures, to navigate, to understand behavior, to prove correctness and to simulate and evaluate specific expressions. Therefore, for so many different purposes of program comprehension, atomistic semantics is a remarkable suggestion.
- Programming language semantics: http://en.wikipedia.org/wiki/Formal_semantics_of_programming_languages
- Axiomatic semantics: http://en.wikipedia.org/wiki/Axiomatic_semantics
- Denotational semantics: http://en.wikipedia.org/wiki/Denotational_semantics
- Atomistic semantics: https://symbolicanalysis.wordpress.com/2009/11/19/unified-semantics-to-meet-numerous-challenges-of-computer-science/