Re: Formal semantics of language semantics

"Satish C. Gupta" <scgupta@solomons.cs.uwm.edu> writes:
>I think nobody in the industry uses formal semantics because of two
>reasons:
>1. most of the formal semantics papers/books start with defining
> a notation and then build a type system framework on top of it.
>
>2. formal semantics is not as easy as formal syntax, simply because
> semantic rules are much more complex than syntax rules.


The real problem, as I related in a nearby article, is simply that the
field is not very well-developed and at this stage in history there is
still a somewhat illucid attempt to try and cram things that don't
belong together into a single monolithic formalism, without further
factoring out


In particular, as related in the last article: control flow is a
purely syntatic phenomenon that should be factored out at the syntatic
level before you get to the semantics. A semantics should see nothing
but pure expressions.


Without recognition of even that basic fact, you end up mangling things
that don't belong together. That's the origin of problem 2 you cited.
The inability to handle the mess in a clean and consistent fashion is
then the driving force behind the divergence of notations and
formalisms.


The first thing is to remove the cobwebs and reinvent the old 20th
century Algol notation. That's what I showed in outline form in the
last article, where the notation was practically pulled out of the hat
starting from something much deeper and more fundamental (a syntax of
infinitary expressions).


Now, I'll take this one step further and show how ALL the major
semantic formalisms are subsumed, with respect to the explication
cited, and simply eliminated in favor of a more fundamental, primarily
syntatic, representation of the algol-like notation of imperative
programming languages.


Contents:
(1) The Reduction Of Denotational Semantics For Control Flow To The
        Infinitary Lambda Calculus
(2) Path Expression Semantics Via The Infinitary Lambda Calculus
(3) Continuation Semantics Via The Infinitary Lambda Calculus
(4) Transition Semantics Via The Infinitary Lambda Calculus
(5) The Reduction Of Method Of Assertions To The Infinitary Lambda Calculus
(6) Synthesis Of Programs Via The Infinitary Lambda Calculus
(7) Array Semantics Via The Infinitary Lambda Calculus


------------------


(1) The Reduction Of Denotational Semantics For Control Flow To The
        Infinitary Lambda Calculus


Historically, the method of denotational semantics that came to be applied
to imperative languages arose following Landin's failure to extend the
correspondence
                          Control Flow Construct <==> Context, or Syntatic Operator
beyond the rudimentary stage
                                                x := e <==> (lambda x.<>) e
to a correspondence that could deal with assignments to structure components
and assignments in the context of non-trivial control flow structures such
as loops and subroutines.


First, the correspondence appeared to run into problems is in the
interpretation of assignments to structure components (e.g. array components,
particularly for nested arrays). But this is seen to be a non-issue, since a
purely syntatic explication for array assignments as syntatic lambda operators
is readily available as well (as shown below).


Second, even the second issue can be removed and the the programme actually
completed. The result leads to equivalence theorems that roughly take the
form:
            For each control flow structure s there is a context s<> such that
                                            [v].[s] = [s<v>]
                                            [s]: state -> state
                                            [v]: state -> value
            s<v> is the "value of v after s is executed".


thereby re-diverting the historical line of progression along its original
(and more natural and intuitive) course and obviating the entire line of
development that took place since then in the area of denotational semantics.


The semantics of control flow completely factors out at the syntatic level
and does not ever need to be seen or incorporated in any semantic formalism.


The extension takes place via an extension of the base language to an
infinitary language. The fixed point denotational semantics for control
flow structures is inherited from the semantics of the infinitary language
and no longer need be postulated. It can be derived.


The infinitary expression
                      x = 0, y = 1,
                      x < n?
                          x = x + 1, y = y * x,
                          x < n?
                              x = x + 1, y = y * x,
                              x < n?
                                  x = x + 1, y = y * x, (...): Q:
                              Q:
                          Q:
                      Q
can be compactly denoted
                      x = 0, y = 1, W
where W is a GNUbreviation for the infinite expression:
                      W: x < n? (x = x + 1, y = y * x, W): Q


One may also think of W is being a limit of a sequence of (non-deterministic)
expressions of increasing order of generality with
                          W(0) = # (= the "non-expression")
                          W(n+1) = (x < n? (x = x + 1, y = y * x, W(n)): Q)
                          W = lim W(n) as n -> infinity


This fixed point takes place entirely at the syntatic level of infinitary
expressions and is, essentially, the characteristic concept that underlies
the whole notion of infinitary expressions.


It's the syntax where the fixed point properties belong, not the semantics.


-------------------------------


(2) Path Expression Semantics Via The Infinitary Lambda Calculus


One also arrives at a concrete representation of path expression semantics via
the correspondences to the (partial) Kleene algebra of contexts:


                                      st<.> = s<t<q>>
                                (s+t)<.> = s<q> | t<q>
                                    (0)<.> = #
                                        1<q> = q
                                      s*<.> = least upper bound of x >= s<x> | q


This extension takes place via a non-deterministic extension of the base
language. In the extension, e | f denotes the non-deterministic union of
two expressions e and f (which, themselves, may be non-deterministic
expressions); and # denotes the "non-expression" -- identity of |.


The expression # is the minimal element of the non-deterministic extension
of the infinitary lambda calculus, and "|" the least upper bound.


A suitable extension of the infinitary lambda calculus then would be to
a non-deterministic infinitary lambda calculus, where one has the
ordering relation >=, minimal element #, and least upper bounds "|"
and "*".


This actually removes the largest chunk of the standard denotational
semantic formalism (which has to do with the ordering relation >=,
least upper bounds, etc.) out of the semantics, and places it entirely
within the syntax of the non-deterministic infinitary lambda calculus.


-------------------------------


(3) Continuation Semantics Via The Infinitary Lambda Calculus


A continuation semantics establishes a denotational semantics S[s] for
statements s, using continuations q, such that:


If s never "relinquishes control", then S[s]q is independent of q
If s relinquishes control & transforms r -> r', then S[s]qr = q(r')


Continuation semantics, too, can be eliminated at a purely syntatic
level by drawing the correspondence:


                  Continuation <-> Context
                  Every continuation q corresponds to a context q<>
                  such that S[s]q = s<q<>>.


-------------------------------


(4) Transition Semantics Via The Infinitary Lambda Calculus


In transition semantics, a configuration is either a state or a command
sequence followed by a state. For example.
      x = x + 1, y = y + x, x = x + 1, (x<-3, y<-7)
-> y = y + x, x = x + 1, (x<-4, y<-7)
-> x = x + 1, (x<-4, y<-11)
-> (x<-5, y<-11)


The correspondence is:
                        Command Sequence <-> Context
                        State <-> Substitution
                        Configuration <-> Substitution
with
                        If s<> is the context corresponding to statement
                        sequence s, and (E,_) the substitution corresponding to the
                        configuration E, then
                                                      s, E (q) = (E, s<q>)


Thus, in the example above, this yields the result:
                  (x = x + 1, y = y + x, x = x + 1, (x<-3, y<-7)) <q>
              = (x<-3, y<-7, (\x. (\y. (\x.q) (x+1)) (y+x)) (x+1))
              = (\x.(\y.(\x.q) (x+1)) (7+x)) (3+1))
where \x is being used here as an ASCII rendition of "lambda x". This is
beta-equivalent to the following:
              = (\x.(\y.(\x.q) (x+1)) (7+x)) 4)
              = (\y.(\x.q) (4+1)) (7+4)
              = (\y.(\x.q) 5) 11
              = (x<-5, y<-11, q)
thus showing that the context
                            (x = x + 1, y = y + x, x = x + 1, (x<-3, y<-7)) <_>
is equal to the context
                            (x<-5, y<-11, _).


-------------------------------


(5) The Reduction Of Method Of Assertions To The Infinitary Lambda Calculus


The basic correspondences are as follows:


Theorem: Corresponding to each control flow structure s is a context
                  s<> over an infinitary language such that:


                  [p]s[q] iff (p => s<q> defined and s<q>) --- Total Correctness
                  {p}s{q} iff (p and s<q> defined => s<q>) --- Partial Correctness


Here, then, the expression s<q> provides a canonical expression for the
"strongest precondition", subject to defineability. The correspondence, itself
also suggests an extension of the method to larger classes of s<q> which would
be considered ill-defined otherwise; i.e., s<q> for those s that correspond to
infinite computations.


Example:
[p] while (a < b) (a = a + 1, y = x + y) [y == x*b]


This reduces to
                                                  p & W defined -> W,


where W is the infinitary conditional expression


                          W = (a < b)? (a = a + 1, y = x + y, W): (y == x*b)


The free variables of W are a, b, x and y. Therefore W can be equivalently
described by the recursive function


                            W(a,b,x,y) = (a < b)? W(a+1,b,x,x+y): (y == x*b)


Letting a(0) = a, y(0) = y, a(n+1) = a(n) + 1, y(n+1) = x + y(n), we arrive
at the specification


                        W = W(a,b,x,y) = (y(N) == b*x),
                        where N = least n >= 0 such that a(n) >= b


The semantics of the loop reduces to the Diophantine equations for a(n) and
y(n). Though Diophantine equations are generally unsolveable, linear ones
are solveable. In fact, any Diophantine system over the finite base
arithmetic (which also means: the arithmetic of any actual computing machine)
is solveable.


More general control structures are likewise solveable in terms of systems
of Diophantine equations. This means, ultimately, the semantics of programs
for a given physical machine forms a decideable theory; since its underlying
numeric and address arithmetic are both finite base.


Solving for a(n) and y(n), we get a(n) = a + n, y(n) = y + n*x. Therefore,


                        N = max(b - a, 0) = b - min(a, b)
Thus
                        W = y + b*x - min(a,b)*x == b*x
or
                        W = (y == min(a,b)*x)


W is defined if the intervening arithmetic operations are well-defined in
the underlying implementation; and it coincides with its naive mathematical
expression if the operations do not overflow. These assertions can be
checked separately by the same methods as illustrated, given the knowledge
of the actual bounds and properties of the underlying machine arithmetic.


Thus, we arrive at the result (under the assumption of well-definedness)
for the weakest precondition:


            [y == min(a,b)*x] while (a < b) (a = a + 1, y = x + y) [y == x*b]


-------------------------------


(6) Synthesis Of Programs Via The Infinitary Lambda Calculus


The basic correspondences are as follows:


Theorem: Corresponding to each control flow structure s is a context s<>
                  over an infinitary language such that:


                [p]s[q] <==> p -> (s<q> defined & s<q>) --- Total Correctness
                {p}s{q} <==> (p & s<q> defined) -> s<q> --- Partial Correctness


Here, we will work in the opposite direction. Given the assertion


                              [a >= 0 && b >= 0] s [c == gcd(a,b)]


find a segment s such that this holds true. In other words, we want a
context s<> such that


                                a >= 0 && b >= 0 --> s<c == gcd(a,b)>


Again, we'll assume all the intervening arithmetic is well-defined. This,
too, can be checked separately (after the fact) by applying the same
methods being illustrated. Here, we use the properties that under the
assumption of x, y >= 0:
                                                  gcd(y, x%y) == gcd(x,y)
                                                  gcd(x, 0) == x
                                                  0 <= x%y < y


Again, under this assumption, we have


                                      gcd(x, y) == gcd(y, x) if x < y
                                      gcd(x, y) == gcd(y, x%y) if x > y
                                      gcd(x, 0) == x
or
                    gcd(x,y) = x < y? gcd(y,x): y > 0? gcd(y, x%y): x


One can go two ways with this. One can eliminate the recursion in favor
of two infinitary expressions W1 for gcd(x,y) and W2 for gcd(y,x) or
otherwise a single infinitary expressions W for gcd(x,y).


The recursion in gcd(x,y) can be removed by directly converting this into
the infinitary expression W by first normalizing te dependence of gcd().
First, we note that where z is an otherwise unused variable:


                        gcd(y,x) = (z = y, gcd(z,x))
                                          = (z = y, y = x, gcd(z, y))
                                          = (z = y, y = x, x = z, gcd(x, y))
and
                        gcd(y,x%y) = (z = y, gcd(z, x%y))
                                              = (z = y, y = x%y, gcd(z, y))
                                              = (z = y, y = x%y, x = z, gcd(x, y))


                    W = x < y? (z = y, y = x, x = z, W):
                            y > 0? (z = y, y = x%y, x = z, W): x
                        = (x < y || y > 0)?
                                  (x < y? (z = y, y = x, x = z, W): (z = y, y = x%y, x = z, W)):
                                  x
                        = (x < y || y > 0)?
                                  (z = y, (x < y? (y = x, x = z, W): (y = x%y, x = z, W))):
                                  x
                        = (x < y || y > 0)?
                                  (z = y, y = (x < y? x: x%y), x = z, W):
                                  x
Thus
                  W = while (x < y || y > 0) z = y, y = (x < y? x: x%y), x = z;
                          x


Noting that x%y == x when x < y, we can reduce the embedded conditional
expression to just x%y, thus arriving at:


                  W = while (x < y || y > 0) z = y, y = x%y, x = z;
                          x


This, however, introduces an extra variable. Since the desired
assertion is s<c == gcd(a,b)>, we can represent the variables
as x = a, y = b, z = c and arrive at the desired control flow
structure:


                  s = while (a < b || b > 0) c = b, b = a%b, a = c;
                          c = a;


If we wanted to preserve a and b, we could revert to x, y and z,
taking c as x, the original x as z, and initializing appropriately to get:


                  s = c = a, y = b;
                          while (c < y || y > 0) x = y, y = c%y, c = x;


The variables x and y can be localized to yield:


                  s = {
                                new y = b; c = a;
                                while (c < y || y > 0) {
                                      new x = y; y = c%y, c = x;
                                }
                          }


The second method is to eliminate the recursion in favor of


                    W1: gcd(x,y) = x < y? gcd(y,x): y > 0? gcd(y, x%y): x
                    W2: gcd(y,x) = y < x? gcd(x,y): x > 0? gcd(x, y%x): y


which we'll leave as an exercise. This can be done without introducing
any new variables. But the control flow structure is more complicated.


-------------------------------


(7) Array Semantics Via The Infinitary Lambda Calculus


The Hoare approach to array semantics consists of two basic principles:


(A) An array is just a function over an integer interval
(B) The update A[I] := X is interpreted as the function update let operator
                          A(I) = X, <...>


A function update is defined by
                      A(I) = X, <...> <==> A = ((I)<-X,A), <...>
where the "update expression" is defined as the lambda expression
                      ((I)<-X,A) = lambda Z.(Z == I? X: A(I))


Array and function semantics can, in fact, be fully unified by providing
a common generalization to both:


                An "updatable function":
                This is essentially an array which is initialized to a function


The array semantics can be readily extended to provide a syntatic explication
for nested arrays. Let Z stand for a (possibly empty) sequence of indexes.
Define by induction,
                                                                  (Z<-X,A)
by
                                              ( <-X,A) = X
                                        (Z(I)<-X,A) = (Z<-((I)<-X,AZ),A)
and define the let expression "AZ = X, <...>" as
                              AZ = X, <...> <==> A = (Z<-X,A), <...>


Then one obtains, as a special case, the simple assignment (where Z = empty):
                    A() = X, <...> <==> A = (()<-X,A), <...> <==> A = X, <...>
Also, for the indexing AZ[I], one obtains
                  A(Z[I]) = X, <...> <==> A = (Z(I)<-X,A), <...>
                                                        <==> A = (Z<-((I)<-X,AZ),A), <...>
                                                        <==> AZ = ((I)<-X,AZ), <...>
                                                        <==> (AZ)[I] = X, <...>
which is what we want.


Example: The Reynolds Paradox
The following is possible


                                              A[A[0]] = 1; { A[A[0]] == 0 }


That is: A[A[0]] becomes 0 immediately after A[A[0]] is set to 1. This can
be proven by making use of the correspondence


                                      {p}s{q} <==> p & s<q> defined -> s<q>


where s<> is the context corresponding to the statement s. Here, the
context is given by


                          A(A(0)) = 1, <...> <==> A = (A(0)<-1,A), <...>


and so s<q> is well-defined and we get:


                                p -> (lambda A. A(A(0)) == 0) (A(0)<-1,A) = p*


defining the right hand side as p*. The statement p* is then the weakest
precondition consistent with the assertion.


Expanding this out, we get:


                  (A(0)<-1,A) = lambda Z . Z == A(0)? 1: A(Z)


Therefore p* is equivalent (by beta equivalence) to:


                                                        B(B(0)) == 0
where
                                          B = lambda Z. Z == A(0)? 1: A(Z)


or, introducing an auxillary variable M = B(0) to make this more tractible:


                                    M == B(0) && B(M) == 0 &&
                                    B == lambda Z. Z == A(0)? 1: A(Z).


Thus
                    *p = (0 == A(0)? M == 1: M == A(0)) &&
                              (M == A(0)? 0 == 1: 0 == A(M))


The second condition reduces to


                                            A(0) != M && A(M) == 0


Under this condition, the first condition reduces to


                                                A(0) == 0 && M == 1


Combined, this is equivalent to the condition (after removing M):


                                        *p = (A(0) == 0 && A(1) == 0).


Thus
                                        p -> (A(0) == 0 && A(1) == 0).


is the unique solution to the paradox. When the initial values of A[0]
and A[1] are 0, then after assigning 1 to A[A[0]], the resulting value of
A[A[0]] will be 0. No other initial values for A[0] and A[1] will make
this happen.


The same reasoning shows that
                                            A[A[0]] = 0; { A[A[0]] == 1 }
is impossible under normal array semantics. In general, the solution for
                                            A[A[0]] = a; { A[A[0]] == b }
is seen to be:
                                    *p = (A[0] == 0? A[a] == b: a == b)

Return to the comp.compilers page.
Search the comp.compilers archives again.