Explicación de Language syntax & Informal Semantics - Domains for Denotational Semantics

Alguien me puede explicar estos dos temas de David A. Schmidt.

Semantical Principles of Programming Languages
The semantics methods shine when they are applied to programming languages—primary features
of a language are made prominent, and subtle features receive proper mention. Ambiguities and
anomalies stand out like the proverbial sore thumb. In this section, we use a classic block-structured
imperative language to demonstrate. Denotational semantics will be emphasized, but excerpts from
the other semantics formalisms will be provided for comparison.

3.1 Language Syntax and Informal Semantics
The syntax of the programming language is presented in Figure 2. As stated in the figure, there
are four “levels” of syntax constructions in the language, and the topmost level, Program, is the
primary one. The language is a while-loop language with local, nonrecursive procedure definitions.
For simplicity, variables are predeclared and there are just three of them—X, Y, and Z. A program,
C., operates as follows: an input number is read and assigned to X’s location. Then the body, C, of
the program is evaluated, and upon completion, the storage vector holds the results. For example,
this program computes n2 for a positive input n; the result is found in Z’s location:
begin proc INCR = Z:= Z+X; Y:= Y+1
in Y:= 0; Z:= 0; while Y not= X do call INCR od end.
It is possible to write nonsense programs in the language; an example is: A:=0; call B. Such
programs have no meaning, and we will not attempt to give semantics to them.

3.2 Domains for Denotational Semantics
To give a denotational semantics to the sample language, we must state the sets of meanings, called
domains, that we use. Our imperative, block-structured language has two primary domains: (i) the
domain of storage vectors, called Store, and (ii) the domain of symbol tables, called Environment.
There are also secondary domains of booleans and natural numbers. The primary domains and
their operations are displayed in Figure 3.
The domains and operations deserve study. First, the Store domain states that a storage
vector is a triple. (Recall that programs have exactly three variables.) The operation lookup
extracts a value from the store, e.g., lookup(2, h1, 3, 5i) = 3, and update updates the store, e.g.,
update(2, 6, h1, 3, 5i) = h1, 6, 5i. Operation init store creates a starting store. We examine check
momentarily.
The environment domain states that a symbol table is a list of identifier-value pairs. For
example, if variable X is the name of location 1, and P is the name of a procedure that is a “noop,”
Then the environment that holds this information would appear (X, 1) :: (P, id) :: nil, where
id(s) = s. (Procedures will be discussed momentarily.) Operation find locates the binding for an
identifier in the environment, e.g., find(X, (X, 1) :: (P, id) :: nil) = 1, and bind adds a new binding,
e.g., bind(Y, 2, (X, 1) :: (P, id) :: nil) = (Y, 2) :: (X, 1) :: (P, id) :: nil. Operation init env creates an
environment to start the program.
In the next section, we will see that the job of a command, e.g., an assignment, is to update
the store—the meaning of a command is a function that maps the current store to the updated

one. (That’s why a “no-op” command is the identity function, id(s) = s, where s ∈ Store.)
But sometimes commands “loop,” and no updated store appears. We use the symbol, ⊥, read
“bottom,” to stand for a looping store, and we use Store⊥ = Store ∪ {⊥} as the possible outputs
from commands. Therefore, the meaning of a command is a function of form Store → Store⊥.
It is impossible to recover from looping, so if there is a command sequence, C1;C2, and C1 is
looping, then C2 cannot proceed. The check operation is used to watch for this situation.
Finally, here are two commonly used notations. First, functions like id(s) = s are often reformatted
to read id = s.s; in general, for f(a) = e, we write f = a.e, that is, we write the argument
to the function to the right of the equals sign. This is called lambda notation, and stems from the
lambda calculus, an elegant formal system for functions [4]. The notation f = a.e emphasizes that
(i) the function a.e is a value in its own right, and (ii) the function’s name is f.
Second, it is common to revise a function that takes multiple arguments, e.g., f(a, b) = e, so
that it takes the arguments one at a time: f = a.b.e. So, if the arity of f was A × B → C, its
new arity is A → (B → C). This reformatting trick is named currying, after Haskell Curry, one
of the developers of the lambda calculus.