For computing there are three standard models for presenting semantics: axiomatic, denotational, and operational.
Denotational semantics was originated by Christopher Strachey in the 1960s and 1970s. After Strachey's untimely death, Dana S. Scott continued guiding the development. The worldview of is the λ-calculus. The lambda calculus is fundamental to logic and was introduced by Alonzo Church in the 1930s. The use of lambda calculus was popularized by John McCarthy through the first functional language, Lisp. The basic concept in denotational semantics is that what a statement means is whatever it computes. The λ-calculus can be used as a sound basis for recursive functions.
The denotational model is comprised of three parts: the concept of abstract syntax trees (AST), the valuation function, and the constructive support algebra.
We will use this approach in developing our project, although axiomatic semantics come into play when developing tests.
In the literature, the abstract syntax graphs are called abstract syntax trees. The purpose of this abstraction is to remove the discussion of parsing method from the discussion of the resulting data structures. In the simplest version, programming languages are developed using context-free grammars. From work in formal languages, we have a theorem that says every parse of a sentence in a context-free grammar generates a tree called a parse tree. The proof of this theorem is constructive, meaning that it generates an algorithm but not necessarily a unique algorithm. These different algorithms produce slightly different parse trees. Therefore, the term abstract syntax tree (AST) denotes a tree of a particular form that removes intermediate structure information. Non context-free grammars generate other graphs, not necessarily a tree; therefore, to be complete we call the whole class of graphs abstract syntax graphs (ASG). The most obvious ASG that is not also an AST is a directed acyclic graph (DAG). DAGs are central to optimization phases of compilers.
The valuation function, call it V, is a recursive function from abstract syntax graphs to meanings. Whoa: That's a load to take all at once. But the idea should be clear. The parsers put programs into graphs. The trick is now to decide what each possible form of the tree means. We do this by defining a valuation function that traverses abstract syntax graphs looking for forms that can be translated. These valuation functions are actually a form of production system because they check the tree for a particular form and if they find that form, they execute a particular action.
The programming language ML was designed with these requirements in mind. For imperative style languages, the issue is more difficulty because there is not a natural way to define the appropriate data structures. A short explanation of how ML works with abstract syntax graphs is a helpful meta-language. N. B. Prolog uses a similar construct.
In ML (and Prolog), you can actually define a function several times in one scope, but with a caveat. Each time you define a function, it needs to have a pattern that can be matched at runtime to the input. This approach can be used by the top-down recursive descent parser by mapping each production into a definition. In our case, the S categorical symbol is the only one with an interesting possibilities.
ML is a functional language and this leads to using equations as definitions. Functional languages, as a group, tend to not use parentheses to indicate a function application; this is a standard mathematical convention. sin x, for example, means that the function sin should be applied to the value of the variable of x. Normal mathematical practice is also a pattern match; again using sin, sin 2nπ = 0 is clear enough to understand.
Now what I'm going to do is separate the various possible definitions by the '|' (bar). So I could do something like this for sine:
sin 0 = 0 | sin π/2 = 1 | sin π/4 = √2/2 | ....
Now what I'm going to do is use the same idea to define semantic functions on graphs.
semF endoffile = termination |
semF ( X ) = semT X .
Using these ideas, define semS assuming that you have only integers and assuming that you know the semantics of '+' and '*'.