This work benefits from Dana Scott's work on complete partial orders and fixed points. For more see Nielsen and Nielsen 92
In my approach you present a set of equations that for each statement S define a relationship between s and s' in terms of the components of S. Thus we get a set of compositional equations for the natural semantics. To show this I define the syntax and semantics the classic "While" Language used in all theoretical work and textbooks of programming language semantics: [ grammar_of_While ]
Relations
This form of semantics benefits from the well developed theory and calculus of binary relations. I exploit the isomorphism between relations and sets of pairs, and the fact that functions (partial or total) are special kinds of relations. The key
concepts and notations are listed below:
[ Calculus of Relations ]
The set of relations on a set is a ready made domain or complete partial ordered set in the following sense. First, the set of binary relations on a set X is a partial order under inclusion(==>). The relations form a poset. Second, there is a unique bottom and top element: the bottom(greatest lower bound) of the poset is the null relation and the top(least upper bound) the anything-to-anything relation. Finally, given any relation, R on X, the Kleene sequence:
Syntax and Semantics
Method
I use a generalized version of BNF to define Syntax and Semantics called XBNF. The syntax is defined in a form close to traditional EBNF. The semantics is defined by a grammar of functions and relations. The details are below:
[ XBNF ]
I use the same symbol m to indicate denotations: m(C) indicates the "meaning of C". The symbol m indicates the function that maps C into m(C). For each syntactic category Syn, there is a set of meanings - a semantic domain Sem say, and m maps each element of Syn into and element of Sem:
The semantic domain is determined by the Syntax of the argument to which m is applied: For example m("101") gives a number but m("while 1<x do x:=x-1") is a relationship between describing what can possibly happen. See [ CoProducts ] for the justification of this idea.
Two items C1, C2 in the same syntactic category are equivalent if and only if m(C1) = m(C2). Items in different syntactic categories can not be equivalent.
Abstract Syntax of While
After Neilsen & Neilsen 92.
Suppose Var={"x", "y" , "z" } and
The following words are used for talking about the language:
Semantic Domains
In the following I assume that we have the whole of abstract algebra available to us when we wish to define how a program behaves. The alternative is to spend time re-inventing wheels. The necessary algebras are listed in this section. They are used in
the following section:
[ Semantic Equations ]
I assume that a number is in a ring with addition, subtraction, multiplication, zero, and unit - with the usual rules and assumptions:
We normally assume some extra rules: Here I need there exist a distinct number
Normally the numbers are taken to be the integers, however see Hoare ??
Coleman ??
Variables
In the While language without declarations, each identifier always identifies the same variable. I introduce a function that associates each symbol in Var with a corresponding name of a field in record structure (or labelled tuple). The set of all
possible records is called the State:
Here ${...v:S...} is a notation for the mathematical objects normally implemented as records or structures. For details see [ State Space ]
This is not the traditional approach where a state is a function mapping elements of Var into current values.
Example of a State Space
Suppose Var={"x", "y" , "z" } then State = ${ x,y,z::number }, and an typical state would by State(x=>1, y=>2, z=>3). The function m is then ("x"+>x | "y"+>y | "z"+> z) or equivalently {("x", x) , ("y", y), ( "z", z) }.
Expressions
The semantic domain for Aexp is typically those of numbers - values in the target algebra. However because I start from assuming that we have an abstract algebra (not just an abstarct data type) we can associate each Aexp in While to an
expression in the algebra of number -- in the set expression(number). We can now use these expressions in predicates and get simpler rules defining the behavior of assignments.
Change of State
The heart of relational semantics is the natural model for change: a relation between two states, before and after:
A relation R:Change is [ determinstic ] when for each s there is no more thn one s' such that s R s'. A relation is [ total ] when for each s the is at least on s'. Functions are both total and deterministic. Partial functions a determinsic but not total.
Exercise: Show that all conditions are deterministic. Show that all Actions are deterministic.
Exercise: Are all Actions functions? Are any Conditions functions?
. . . . . . . . . ( end of section Semantic Domains) <<Contents | Index>>
Semantic Equations
Semantic Equations for Num
These are a simple introduction to the method, not a useful notation.
For n:Num, m(n)::number.
Exercises on the Semantics of Num
Exercise: Is m on Num a total function or a partial function? Is it a one-to-one function or many-to-one function? If many to one derive a congruence so that modulus the congruence semantically equivalent.
Semantics of Var
Suppose Var={"x", "y" , "z" } then State = Net x,y,z::number End Net, and an typical state would by s=State(x=>1, y=>2, z=>3). The function m=("x"+>x | "y"+>y | "z"+> z) relates each symbolic string to its componet in the state space. Hence, m("x) =x
and s.m("x")=1 and s.m("y")=2 and s.m("z")=3.
Semantics of Aexp
However, m("x+y") is not 3 but x+y. In state s=(x=>1, y=>2, z=>3), though, x+y does have the value 3. By mapping strings in While into mathematical expressions (rather than values) this approach uses the algebra of the expressions to reason about them.
Exercises on Semantics of Aexp
Exercise: Is m on Aexp a total function or a partial function? Is it a one-to-one function or many-to-one function? If one to one prove that it, therwise find a equivalence relation so that semantically equivalent Aexp's are equivalent.
Exercise: How do you prove the following Aexp are equivalent?
Exercise: Do these semantics force the implementor to provid infinite precision arithmetic or not? Prove your claim.
.Semantics of Bexp
The Boolean operations (and,or) on predicates define conditions that are related to the set theoretic operators of intersection and union: { s || P and Q} = {s||P} & {s||Q} and so to the [ Calculus of Relations ]
I define m:(Aexp Op Aexp)->Condition in terms of two auxilary functions:
This definition constructs a predicate on the state, and this predicate defines the set of states that satisfy the relationship. The underlying formalism is described below: [ Dynamic Predicates ]
Example of Semantics of Bexp
Suppose Var={"x", "y" , "z" } then State = Net x,y,z::number End Net, and a typical state would by s=State(x=>1, y=>2, z=>3). The function m=("x"+>x | "y"+>y | "z"+> z) relates each symbolic string to its componet in the state space. Hence, m("x) =x
and s.m("x")=1 and s.m("y")=2 and s.m("z")=3. So
:. m("x>y /\ z<2") = (m("x") >m("y")) and (m("z") < m("2") ) = ( x>y and z <2 ).
So "x>y /\ z<2" means the relation that does not change states and where (x>y and x<2) and does not permit any other state to proceed: () rel[s,s']( s=s' and s.x>y.x and s.z<2) = Id & {(s,s')|| s.x>y.x} & {(s,s')|| s.z<2}.
Exercises on Semantics of Bexp
Exercise: Is m on Bexp a total function or a partial function? Is it a one-to-one function or many-to-one function? If one to one prove that it, therwise find a equivalence realtion so that semantically equivalent Aexp's are equivalent.
Exercise: Show that for all b, m(b) is a Condition. Prove that it is there deterministic but not total. For which Bexp is m(b) a function? and which function is it?
Relational Semantics of Stm
The following relation semantics of While a natural semantics. The meaning of a statement is a relation that is defined to hold between s and s' precisely when the statement terminates in state s' when started in s'. It seems possible to develop
a set of relational equations that define the structural operational semantics of a statement - where the relation holds between successive states as the program executes. To find out more see
[ Structural Operational Semantics ]
below.
Notation: Id, ;, |, do, no, ;, etc. are from the calculus of Relations, see [ Calculus of Relations ]
Note. These are a compositional definition: the meaning of each statement is expressed in terms of the meanings of its components in the syntax. In other words the definition is driven by the structure of the data.
Example of Semantics of a Program
When Var={"x", "y" , "z" } and F="(z:=1; y:=x); while ( y > 1 ) do ( z:=z*y; y:=y-1 ))".
then
Exercises on the Relational Semantics of Aexp
Exercise: Is m on Stm a total function or a partial function? Is it a one-to-one function or many-to-one function? If many to one derive a congruence so that modulus the congruence semantically equivalent, , otherwise prove that the function is
one-one.
Exercise: Show that all assignents are Actions.
A statement S is deterministic if m(S) is deterministic in tha above syntax.
Exercise: Show that x:=a and skip are deterministic. Show that if the components of a sequence, selection, or itteration are deterministic then so are the compounds.
Exercise: From the previous exercise, can we deduce that all While programs are deterministic? Can you explain your answer? Can you present a formal proof of your answer?
Exercise(For Mathematicians) : In how many different senses is m a homomorphism between two systems? Is it a isomorphism, monomorphism, homeomorphism, etc.
Exercise(Advanced) : Suppose one started by defining m as function mapping some strings into a family of disjoint meanings, as above. Further suppose that every partial definition is compositional. Show that a context free grammar can be deconstructed from the functions. Show that m is total on the language of your deconstructed grammar.
. . . . . . . . . ( end of section Semantic Equations) <<Contents | Index>>
. . . . . . . . . ( end of section Syntax and Semantics) <<Contents | Index>>
Conclusion
In the above collection of semantic equations m is nearly always distributed to all the parts of the construct being assigned a meaning. A few examples would show that every construct in While is mapped directly into a simple expression in the
calculus of relations.
I conclude that we could use the calculus of relations as our ultimate semantic metalanguage. I claim that, relations even forms an uniquely interesting and powerful programming language of their own. They are interesting because they are the only piece of existing mathematics is already a programming language. They are powerful because they can express concurrency and non-determinism.
. . . . . . . . . ( end of section Main Text) <<Contents | Index>>
Footnotes
XBNF
EBNF uses
The general XBNF form is For D, term(p)::T=e.
where D declares the names and types of the parameters p (if any) and T is the type. In theory however this is the same as term:: P->T = fun[D](e).
The notation term::T associates a type with a term.
. . . . . . . . . ( end of section XBNF) <<Contents | Index>>
The defining property of do(R) is a second order property that if x do(R) y then all invariant(or closed) sets under R that contain x also contain y. Whitehead & Russell Circa 1930
For more information see:
[ logic_41_HomogenRelations.html ]
(deterministic)A Relation R is deterministic if for all x, there is no more than one y such that x R y. (total) A Relation R is total if for all x, there is at least one y such that x R y.
For more information [ Relations in math_10_STANDARD ]
. . . . . . . . . ( end of section Calculus of Relations) <<Contents | Index>>
State Space
The formal model usually presented of a variable is a function s:Var->Val for some set of values. Thus if v:Var then s(v) \in Val. I assume that there is a labelled Cartesian Product or tuple where each v:Var has an associated label l and if
's:State' then s.l \in Val indicates the value of v in state s. I claim that this is effectively a simple change of notation.
The notation is described informally in [ intro_records.html ]
. . . . . . . . . ( end of section State Space) <<Contents | Index>>
Dynamic Predicates
new state. For more see
[ math_14_Dynamics.html ]
Conditions as Static Predicates
When a predicate has no dynamic variables then it expresses a condition - a set of states that will not change, but can only be satsified by some states and not others (in general). For example x+y>0 is satisfied by the set of states `{ s || s.x+s.y >0} and defines the relationship { s,s' || s=s' and s.x+s.y >0}`.
Assignments
The formula
(sample) x'= e
is an example of a dynamic predicate that describes a change in variable x with other variables being held constant. The new value of x is the value of the expression e using the old value of x. Or to be more precise: e is evaluated using
values from the old state, and then the x component of the state is changed to the value of e.
General Form
This section goes beyond the goal of expressing the semantics of a simple programming language.
It is worth developing a theory of general dynamic predicates because they form a precise yet concise way of documenting and specifying code.
. . . . . . . . . ( end of section Dynamic Predicates) <<Contents | Index>>
CoProducts
oduct that is the theoretical model of the discriminated union (Ada), union(Algol 68 and C), or tagged record(Pascal). The theory of such coproducts is part of category theory.
. . . . . . . . . ( end of section CoProducts) <<Contents | Index>>
Structural Operational Semantics
Here I explore a less abstract and more detailed form of semantics. I want to see how a relation between successive states can be defined using the calculus of relations.
Here a change is expressed in terms of a change in two components: the statement being executed and the state in which the execution starts. This is called a configuration and is written: (S,s)
The configurations of form ( done, s) are called terminal states and indicate that the program has terminated:
In texts (done, s) is often written s.
where x'=e is defined above: [ Dynamic Predicates ]
For S1,S2,S3:Stm, s1,s2:State, if (S1, s1) N (S3, s2) then (S1 ";" S2, s1) N (S3 ";" S2, s2).
For b:Bexp, S1,S2:Stm, s1,s2:State, if m(b)=Id then ("if" b "then" S1 "else" S2, s1) N (S1, s1). For b:Bexp, S1,S2:Stm, s1,s2:State, if m(b)={} then ("if" b "then" S1 "else" S2, s1) N (S2, s1).
For b:Bexp, S:Stm, s:State, ("while" b "do" S, s) N ("if" b "then" "(" S";" "while" b "do" S")" "else" "skip", s).
Exercise on Structural Operational Semantics
Prove that for all S:Stm, s1,s2:State, (S,s1) do(N) (done, s2) iff s1 m(S) s2.
Note: this is true for While, but is not true for soem extensions of While.
It might be wondered why it is worth have a more complex and less abstract way of stating the semantics of a programming language. One reason is that Natural semantics can not express the idea of a single step in a program and so can not define the idea of interleaving the steps from two parallel programs.
An interesting question for further research is to find a set of compostional equations for the N relation to replace the derivation rules for ";", "if", and "while".
. . . . . . . . . ( end of section Structural Operational Semantics) <<Contents | Index>>
. . . . . . . . . ( end of section Footnotes) <<Contents | Index>>
. . . . . . . . . ( end of section Relational Semantics of The While Language) <<Contents | Index>>