18 Oct 2002 23:44:40 -0400

Related articles |
---|

[8 earlier articles] |

Re: Formal semantics of language semantics nmm1@cus.cam.ac.uk (Nick Maclaren) (2002-10-13) |

Re: Formal semantics of language semantics haberg@matematik.su.se (Hans Aberg) (2002-10-13) |

Re: Formal semantics of language semantics scgupta@solomons.cs.uwm.edu (Satish C. Gupta) (2002-10-13) |

Re: Formal semantics of language semantics lex@cc.gatech.edu (Lex Spoon) (2002-10-13) |

Re: Formal semantics of language semantics anw@merlot.uucp (Dr A. N. Walker) (2002-10-18) |

Re: Formal semantics of language semantics whopkins@alpha2.csd.uwm.edu (Mark) (2002-10-18) |

Re: Formal semantics of language semantics whopkins@alpha2.csd.uwm.edu (Mark) (2002-10-18) |

Re: Formal semantics of language semantics nmm1@cus.cam.ac.uk (Nick Maclaren) (2002-10-20) |

Re: Formal semantics of language semantics nmm1@cus.cam.ac.uk (Nick Maclaren) (2002-10-20) |

Re: Formal semantics of language semantics merlot!anw@mailbox1.ucsd.edu (Dr A. N. Walker) (2002-10-25) |

Re: Formal semantics of language semantics whopkins@alpha2.csd.uwm.edu (Mark) (2002-10-25) |

Re: Formal semantics of language semantics whopkins@alpha2.csd.uwm.edu (Mark) (2002-10-25) |

Re: Formal semantics of language semantics nmm1@cus.cam.ac.uk (Nick Maclaren) (2002-11-06) |

[2 later articles] |

From: | "Mark" <whopkins@alpha2.csd.uwm.edu> |

Newsgroups: | comp.compilers |

Date: | 18 Oct 2002 23:44:40 -0400 |

Organization: | University of Wisconsin - Milwaukee, Computing Services Division |

References: | 02-09-149 02-09-169 02-10-012 |

Keywords: | semantics |

Posted-Date: | 18 Oct 2002 23:44:40 EDT |

"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)

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.