BRICS RS-98-42 P. D. Mosses: Semantics, Modularity, and Rewriting Logic BRICS

Basic Research in Computer Science

Semantics, Modularity, and Rewriting Logic

Peter D. Mosses BRICS Report Series RS-98-42 ISSN 0909-0878 December 1998 See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/98/42/

Semantics, Modularity, and Rewriting Logic

Peter D. Mosses^{∗}

BRICS,^{†}Dept. of Computer Science, University of Aarhus Ny Munkegade bldg. 540, DK-8000 Aarhus C, Denmark

Abstract

A complete formal semantic description of a practical programming language (such as Java) is likely to be a lengthy document, regardless of which semantic framework is being used. Good modularity of the description is important to the person(s) developing it, to facilitate reuse, change, and extension. Unfortunately, the conventional versions of the major semantic frameworks have rather poor modularity.

In this paper, we first recall some approaches that improve the modularity of denotational semantics, namely action semantics, modular monadic semantics, and a hybrid framework that combines these: modular monadic action semantics. We then address the issue of modularity in operational semantics, which appears to have received comparatively little attention so far, and report on some preliminary investigations of how one might achieve the same kind of modularity in structural operational semantics as the use of monad transformers can provide in denotational semantics—this is the main technical contribution of the paper. Finally, we briefly consider the representation of structural operational semantics in rewriting logic, and speculate on the possibility of using it to interpret programs in the described language. Providing powerful meta-tools for such semantics-based interpretation is an interesting potential application of rewriting logic; good modularity of the semantic descriptions may be crucial for the practicality of using the tools.

Much of the paper consists of (very) simple examples of semantic descriptions in the various frameworks, illustrating the degree of reformulation needed when extending the described language—a strong indicator of modularity. Throughout, it is assumed that the reader has some familiarity with the concepts and notation of denotational and structural operational semantics. Familiarity with the basic notions of monads and monad transformers is not a prerequisite.

∗E-mail: pdmosses@brics.dk †Basic Research in Computer Science, Centre of the Danish National Research Foundation

1 Modularity in Denotational Semantics

It is well-known [5, 12, 13, 22] that the cause of poor modularity in conventional denotational semantic descriptions is the unrestricted use of (typed) λ-notation to specify semantic entities. When the described language is extended with unanticipated new constructs, the domains of denotations may need to be changed, and then the description of the old constructs may have to be completely reformulated to adapt it to the new domains. A small-scale illustration of the poor extensibility in denotational semantics is provided in Appendix A.

Action semantics [15, 16, 18, 23] improves the modularity of denotational semantics by taking denotations to be so-called actions, which are expressed using a fixed action notation consisting of various primitives and combinators—a few of them are listed in Appendix B. The primary interpretation of action notation is, in contrast to that of λ-notation, operational, and it is defined [15] using structural operational semantics (and a derived testing equivalence). Action notation provides direct support for specifying control flow, data flow, scopes of bindings, side-effects, procedural abstraction, and (asynchronous) communication between concurrent processes. The high degree of extensibility obtained in action semantics is illustrated in Appendix C; larger-scale illustrations have been given elsewhere [15, 17].

Also the use of monads in denotational semantic descriptions can improve their modularity [12]. Briefly, a monad distinguishes between values and computations, and provides a (polymorphic) operator, here written as infix >>=, for composing computations, as well as one, written return, that turns a value into a computation which simply computes that value. The use of this composition operator is independent of how computations are represented— in marked contrast to ordinary function composition.

Complex monads can generally be built systematically by composing a series of monad transformers, each of which may provide various operators (apart from composition and returning a value). A systematic approach to lifting operators through monad transformers has been developed in the framework called modular monadic semantics [5]; its implementation in the higher-order functional programming language Gofer provides modular semantics-based interpreters. The high degree of extensibility obtained in modular monadic semantics is illustrated in Appendix D. This framework appears to be simpler to use than other approaches to lifting monad transformers [3, 20], even though (or perhaps because?) the latter are based more directly on sophisticated category-theoretical foundations.

The framework of modular monadic action semantics [21, 22] combines the two approaches of modular monadic semantics and action semantics by using the former to give a modular denotational definition of action notation—replacing its original structural operational semantics, which has rather poor modularity (see the next section). This approach facilitates the extension of action notation to support constructs that it currently lacks, such as first-class continuations. (A disciplined—but not explicitly monadic—use of action combinators in denotational descriptions has also been proposed by the present author [14].) However, the part of action notation concerned with communication and concurrency has been omitted, and may be difficult to incorporate: a proper semantic treatment would seem to require non-(ω-)continuous functions on power domains to model fairness. Another drawback is that the operational consequences of the monadic semantics for action notation may be excessively difficult to grasp for those not already well-versed in the usual techniques for encoding computations as higher-order functions.

Modular monadic action semantics was motivated by the lack of modularity of the original structural operational semantics of action notation. Is that description is inherently non-modular? or could it perhaps be reformulated so as to have an acceptable degree of modularity and extensibility? Could one achieve good modularity, comparable to that obtained by the use of action notation or monads in denotational semantics, generally in structural operational semantics?

2 Modularity in Structural Operational Semantics

In his Aarhus lecture notes [19], where he first proposed structural operational semantics (SOS) as a general framework for describing programming languages, Gordon Plotkin wrote:

As regards modularity we just hope that if we get the other things in a reasonable shape, the current ideas for imposing modularity on specifications will prove useful.

Unfortunately, that hope appears to have been in vain: conventional SOS descriptions have just as poor modularity as conventional denotational descriptions, since the semantic components of the transition relation (environments, stores, etc.) are made explicit in every rule, and a complete reformulation is needed when adding further components. A simple illustration of the problem is provided in Appendix E.

The problem of poor modularity seems not to arise when using SOS to give descriptions of process algebras—the huge success of this application of SOS may explain why modularity has not been as much as concern here as in denotational semantics. Incidentally, so-called natural semantics [4] seems to suffer just as much from poor modularity as SOS does.

In denotational semantics, good modularity has been obtained simply by adopting a more disciplined notation, avoiding any reference to irrelevant semantic components when defining the semantics of each construct. The author has recently tried to do something similar for structural operational semantics; the approach is illustrated below.

Its main features are as follows:

• Whereas the values computed by program constructs are added directly to the abstract syntax of the language being described (and regarded as terminal configurations, following Plotkin [19]), all the other semantic arguments of the transition relation (e.g., environments, current and subsequent stores) are hidden in abstract transitions.

By this means, the transition relation is always ternary, taking as arguments: (i) the current syntax; (ii) the semantic “action” of the transition being made; and (iii) the subsequent syntax or computed value.

A special case of the “actions” here could be simply input and output labels on transitions, as needed when using SOS for process algebra; but in general, the algebra of actions includes sequencing:

• Sequencing of semantic actions a_{1} ; a_{2} is associative, and silent actions τ are units.

Sequencing of actions is usually partial, since a_{1} may be followed by a_{2} only if the information left by a_{1} is consistent with that from which a_{2} starts. Thus a; τ = a only when a; τ is defined, and similarly for τ; a = a. N.B. τ is regarded as a variable, not a constant: there is a whole family of silent actions (one for each semantic state).

The introduction of fixed notation for sequencing actions corresponds roughly to the introduction of monads in denotational semantics; the silent actions distinguish transitions that are inherently unobservable, not affecting the semantic components of the current state but allowing gradual propagation of the flow of control.

• The transitive and reflexive-transitive closures of the transition relation are always available.

These closures correspond closely to the notion of an entire computation in a monad; they are easily definable in terms of single transitions. Plotkin used them for letting a (terminating) sequence of transitions for expression evaluation give rise to a single transition for an enclosing statement, and for giving particularly simple descriptions of iterative constructs.

Natural semantics [4] may be obtained when the only relation for which rules are given is the reflexive-transitive closure (the second “syntactic” argument of which is always a computed value). By using different notation for the single transition relation and its closure, it should be possible to integrate natural and structural operational semantics (see also [1]).

Adoption of the above discipline for SOS appears to provide the desired degree of modularity—at least for the kind of examples given in Plotkin’s notes. It remains to be seen whether this approach can be applied to provide a modular operational semantics of the full action notation, and whether it can also be used to describe further constructs, such as first-class continuations. It should also be compared to other approaches [2, 8] which obtain some degree of modularity in a rather different way to that explored here, using so-called evaluation contexts.

Let us now illustrate the extensibility obtained, taking the same example language extension as for the other approaches considered above.

2.1 Initial Description

The abstract syntax of the initial language is given in Appendix A.1.1. By adding computed values to each syntactic category we obtain the configurations, exactly as in Appendix E.1.2.

For our transition relations, let us take, for each configuration set X whose elements evaluate to semantic values in V ⊆ X, a ternary (singlestep) transition relation involving semantic action arguments from A_{X}:

→ : X × A_{X} × X and its reflexive-transitive closure:

→^{∗} : X × A_{X} × V the latter being specified in terms of the former by:

\frac{X →^{a} X′ X′ →^{∗}^{a′} v a; a′ = a′′}{X →^{∗}^{a′′} v}  \overline{v →^{∗}^{τ} v}

Our example language includes declarations (of constants), so we shall have to include the current environment somehow. For expressions, the computed values do not include environments, and the discipline of our restriction to ternary transition relations forces us to take the current environment as a component of the second argument of the relation; here, it turns out to be the only component needed.

For declarations, the computed values are themselves environments—but just small ones, reflecting the bindings produced by the declarations, and not including the current environment; so again we let the current environment be the only component of the second argument of the transition relation.

Thus we take sets A_{Exp} = A_{Dcl} = Env of semantic actions. We have now to define sequencing on them. The appropriate definition appears to be to let a; a′ = ρ when a = a′ = ρ, otherwise undefined. In this simple example, all the actions are essentially silent—changes to the current environment are not directly observable.

We shall need two further bits of notation, associated with environments and not depending on the language being defined. The first is an extra configuration lookup(I ) for requesting the value currently bound to a particular identifier; its only transition is specified by:

\frac{ρ(I ) = v}{lookup(I ) →^{ρ} v}

The second overlays an environment ρ′ on top of the current environment component ρ of an action a, which is here simply a itself:

overlay(a, ρ′) = a[ρ′], using the same notation for combining environments as in the other approaches illustrated in the appendices.

This completes our preparations—now for specifying the the transition rules. Note that “side-conditions” on rules are here written as premisses, for notational convenience, as in Appendix E.

\frac{E_{1} →^{a} E′_{1}}{E_{1} O E_{2} →^{a} E′_{1} O E_{2}}  \frac{E_{2} →^{a} E′_{2}}{e_{1} O E_{2} →^{a} e_{1} O E′_{2}}  \frac{e_{1} O e_{2} = e}{e_{1} O e_{2} →^{τ} e}

\frac{lookup(I ) →^{τ} e}{I →^{τ} e} \frac{D →^{a} D′}{let D in E →^{a} let D′ in E} \frac{overlay(a, ρ) = a′ E →^{a′} E′}{let ρ in E →^{a} let ρ in E′}

\overline{let ρ′ in e →^{τ} e}

\frac{E →^{a} E′}{const I = E →^{a} const I = E′}
const I = e →^{τ} (I ↦ e)
\frac{D_{1} →^{a} D′_{1}}{D_{1} and D_{2} →^{a} D′_{1} and D_{2}}  \frac{D_{2} →^{a} D′_{2}}{ρ_{1} and D_{2} →^{a} ρ_{1} and D′_{2}}

\frac{dom(ρ_{1} ) ∩ dom(ρ_{2} ) = ∅}{ρ_{1} and ρ_{2} →^{τ} ρ_{1} ∪ ρ_{2}}

2.2 A Simple Extension

The abstract syntax of the extended language is given in Appendix A.2.1. By adding computed values to each syntactic category we obtain the configurations, exactly as in Appendix E.2.2.

To cater for variable declarations and assignment commands, we need to add components to our semantic actions for holding both the current store and the subsequent store. For simplicity of notation, let us take uniform sets A_{Exp} = A_{Dcl} = A_{Cmd} = Env × S × S of semantic actions (in fact the second store component for expressions could just as well be eliminated).

We have now to define sequencing on them. The appropriate definition is now to let a_{1} ; a_{2} = (ρ, σ, σ′′) when a_{1} = (ρ, σ, σ′) and a_{2} = (ρ, σ′, σ′′), otherwise undefined. The silent actions are those of the form (ρ, σ, σ).

We shall need to redefine the two bits of notation associated with environments:

\frac{ρ(I ) = v}{lookup(I ) →^{(ρ,σ,σ)} v} overlay((ρ, σ, σ′), ρ′) = (ρ[ρ′], σ, σ′)

These changes correspond roughly to the lifting of operators through monad transformers that is provided in modular monadic semantics.

Finally, we introduce three new configurations, concerned entirely with stores: new, for allocating a new location; update(l, s), for overwriting the contents of the store at location l with value s; and contents(l), for inspecting the value stored at location l. Their transitions are specified as follows:

\frac{(l ∉ dom(σ) σ[l ↦ ⊥] = σ′}{new →^{(ρ,σ,σ′)} l}  \frac{l ∈ dom(σ) σ[l ↦ s] = σ′}{update(l, s) →^{(ρ,σ,σ′)} ()}

\frac{contents(l) →^{(ρ,σ,σ′)} s}{σ(l) = s σ = σ′}

Now, no changes to the original rules are needed at all—one simply adds the following new rules:

\frac{new →^{a} l}{var I →^{a} (I ↦ l)} \frac{lookup(I ) →^{τ} l}{I := E →^{τ} l := E} \frac{E →^{a} E′}{l := E →^{a} l := E′} \frac{update(l, s) →^{a} ()}{l := s →^{a} ()}
\frac{lookup(I ) →^{τ} l contents(l) →^{τ} s}{I →^{τ} s}  \frac{C_{1} →^{a} C′_{1}}{C_{1} ; C_{2} →^{a} C′_{1} ; C_{2}}  \overline{(); C_{2} →^{τ} C_{2}}

3 Prototyping Semantics using Rewriting Logic

Since SOS can be represented straightforwardly in rewriting logic [7], one may in principle use systems such as Maude and ELAN (see the other papers in this volume for current references) for interpreting programs according to their specified semantics. Perhaps also Maude’s object-oriented modules could be exploited to express the intended operational semantics more concisely, following the specification style for concurrent object-oriented systems illustrated in [6, 9, 10]. But an SOS description of a practical programming language is likely to be rather large—regardless of its degree of modularity— and this might provoke problems with the efficiency of the interpretation.

An alternative approach would be to exploit action semantics as an intermediate step. The action semantics of a practical programming language may itself be quite large; but the map that it specifies from programs to actions is purely functional, and can be implemented efficiently, e.g. by term rewriting. It remains to interpret actions according to the SOS of action notation, using the representation of SOS in rewriting logic. The primary advantage of this two-stage approach is that the SOS of action notation may be (at least) an order of magnitude smaller than the SOS of the programming language. The size of the actions would be somewhat larger (by a constant factor) than the corresponding programs, but at least for prototyping purposes, this expansion of the term to be interpreted should not be a source of undue inefficiency.

These proposals are currently still quite speculative, and need much further investigation and experimentation. Potentially, they could lead to a significant application of rewriting logic, providing useful meta-tools for semantics-based interpretation of programs. Comments and suggestions concerning the approach outlined above are especially welcome at this early stage of the work.

4 Conclusion

We have considered some aspects of the connections between semantics, modularity, and rewriting logic. We have found that it seems possible to make a considerable improvement to the modularity of structural operational semantics by insisting on a disciplined use of notation for transitions, making the transition rules independent of the presence or absence of particular semantic components of the transition relations. The development of such a modular form of operational semantics is a contribution to a recently-started project at SRI International and Stanford University, which aims to exploit rewriting logic in providing useful meta-tools for logics and programming languages.

Acknowledgement

The author is grateful to the organizers of WRLA’98 for the invitation to give a talk on applications of rewriting logic to semantics, and for funding to attend the workshop; also to José Meseguer and Carolyn Talcott for the invitation to participate in their meta-tools project. After reading a draft version of this paper, Andrzej Filinski, John Hamer, José Meseguer, and David Watt provided valuable suggestions for improving not only the presentation, but also some technical details concerning the proposed approach to modular operational semantics; any remaining defects are, of course, entirely the author’s own responsibility.

The author is supported by BRICS (Centre for Basic Research in Computer Science), established by the Danish National Research Foundation in collaboration with the Universities of Aarhus and Aalborg, Denmark; by an International Fellowship from SRI International; and by DARPA-ITO through NASA-Ames contract NAS2-98073.

References

[1] E. Astesiano. Inductive and operational semantics. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts, IFIP State-of-the-Art Report, pages 51–136. Springer-Verlag, 1991.

[2] R. Cartwright and M. Felleisen. Extensible denotational language specifications. In M. Hagiya and J. C. Mitchell, editors, Symposium on Theoretical Aspects of Computer Software, number 789 in LNCS, pages 244–272, Sendai, Japan, Apr. 1994. Springer-Verlag.

[3] P. Cenciarelli and E. Moggi. A syntactic approach to modularity in denotational semantics. In Proceedings of the Conference on Category Theory and Computer Science, Amsterdam, The Netherlands, Sept. 1993. CWI Tech. Report.

[4] G. Kahn. Natural semantics. In STACS’87, Proc. Symp. on Theoretical Aspects of Computer Science, volume 247 of LNCS. Springer-Verlag, 1987.

[5] S. Liang and P. Hudak. Modular denotational semantics for compiler construction. In Programming Languages and Systems – ESOP’96, Proc. 6th European Symposium on Programming, Linköping, volume 1058 of LNCS, pages 219–234. Springer-Verlag, 1996.

[6] N. Martí-Oliet and J. Meseguer. Action and change in rewriting logic. In R. Pareschi and B. Fronhoefer, editors, Dynamic Worlds: From the Frame Problem to Knowledge Management. Kluwer Academic Publishers, 1998. To appear. Also Technical Report SRI-CSL-94-07, SRI International, April 1994.

[7] N. Martí-Oliet and J. Meseguer. Rewriting logic as a logical and semantic framework. In D. Gabbay, editor, Handbook of Philosophical Logic, volume 6. Kluwer Academic Publishers, 1998. To appear. Also Technical Report SRI-CSL-93-05, SRI International, August 1993.

[8] I. Mason and C. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1(3):287–327, 1991.

[9] J. Meseguer. A logical theory of concurrent objects and its realization in the Maude language. In G. Agha, P. Wegner, and A. Yonezawa, editors, Research Directions in Object-Based Concurrency, pages 314–390. The MIT Press, 1993.

[10] J. Meseguer. Solving the inheritance anomaly in concurrent objectoriented programming. In O. M. Nierstrasz, editor, Proc. ECOOP’93, 7th European Conf., Kaiserslautern, Germany, volume 707 of LNCS, pages 220–246. Springer-Verlag, 1993.

[11] R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, 1990.

[12] E. Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

[13] P. D. Mosses. Denotational semantics. In Handbook of Theoretical Computer Science, volume B, chapter 11. Elsevier Science Publishers, Amsterdam; and MIT Press, 1990.

[14] P. D. Mosses. A practical introduction to denotational semantics. In Formal Description of Programming Concepts, IFIP State-of-the-Art Report, pages 1–49. Springer-Verlag, 1991.

[15] P. D. Mosses. Action Semantics. Number 26 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.

[16] P. D. Mosses. Theory and practice of action semantics. In MFCS ’96, Proc. 21st Int. Symp. on Mathematical Foundations of Computer Science (Cracow, Poland, Sept. 1996), volume 1113 of LNCS, pages 37–61. Springer-Verlag, 1996.

[17] P. D. Mosses and M. A. Musicante. An action semantics for ML concurrency primitives. In FME’94, Proc. Formal Methods Europe: Symposium on Industrial Benefit of Formal Methods, Barcelona, volume 873 of LNCS, pages 461–479. Springer-Verlag, 1994.

[18] P. D. Mosses and D. A. Watt. The use of action semantics. In Formal Description of Programming Concepts III, Proc. IFIP TC2 Working Conference, Gl. Avernæs, 1986, pages 135–166. North-Holland, 1987.

[19] G. D. Plotkin. A structural approach to operational semantics. Lecture Notes DAIMI FN–19, Dept. of Computer Science, Univ. of Aarhus, 1981.

[20] J. Power. Modularity in denotational semantics. In Proc. MFPS XIII, volume 5 of ENTCS, 1997. http://www.elsevier.nl/locate/ entcs/volume5.html.

[21] K. Wansbrough. A modular monadic action semantics. Master’s thesis, Dept. of Computer Science, Univ. of Auckland, Feb. 1997. WWW^{1}.

1http://www.dcs.gla.ac.uk/˜ keithw/research/msc/thesis

[22] K. Wansbrough and J. Hamer. A modular monadic action semantics. In Conference on Domain-Specific Languages, pages 157–170. The USENIX Association, 1997.

[23] D. A. Watt. Programming Language Syntax and Semantics. Prentice-Hall, 1991.

Appendices

For the sake of brevity, some tedious notational details are omitted below. Moreover, the possibility of program errors is ignored.

A Conventional Denotational Semantics

A.1 Initial Description

A.1.1 Abstract Syntax

(Exp) E ::= N | E_{1} O E_{2} | I | let D in E
(Nml) N ::= …
(Opr) O ::= + | − | ∗ | = | <
(Dcl) D ::= const I = E | D_{1} and D_{2}
(Ide) I ::= …

A.1.2 Domains

e ∈ EV = N + B (expressible values)
n ∈ N = …  (natural numbers)
b ∈ B = … (Boolean truth-values)
ρ ∈ Env = Ide → DV (environments)
d ∈ DV = N  (denotable values)

A.1.3 Semantic Functions

E : Exp → (Env → EV)
N: Nml → N
O: Opr → (EV × EV → EV)
D: Dcl → (Env → Env)

E[[N ]]  = λρ.N [[N ]]
E[[E_{1} O E_{2} ]]  = λρ.O[[O]](E[[E_{1} ]]ρ, E[[E_{2} ]]ρ)
E[[I ]]  = λρ.ρ(I )
E[[let D in E]] = λρ.E[E]](ρ[D[[D]]ρ])
D[[const I = E]] = λρ.(I ↦ E[[E]]ρ)
D[[D_{1} and D_{2} ]] = λρ.D[[D_{1} ]]ρ ∪ D[[D_{2} ]]ρ

… (definitions of N , O omitted)

A.2 A Simple Extension

A.2.1 Abstract Syntax

(Dcl) D ::= … | var I
(Cmd) C ::= I := E | C_{1} ; C_{2}

A.2.2 Domains

d ∈ DV = … + Loc (denotable values)
σ ∈ S = Loc → SV  (stores)
s ∈ SV = N  (storable values)
l ∈ Loc = N  (locations)

A.2.3 Auxiliary Functions new : S → Loc × S (allocation)

A.2.4 Semantic Functions The previous definitions of E, D are no longer well-formed—the changes that have to be made in them are underlined below.

E : Exp → (Env → (\underline{S →} EV))
D: Dcl → (Env → (\underline{S →} Env \underline{× S}))
C : Cmd → (Env → (S → S))

E[[N ]]  = λρ.\underline{λσ.}N [[N ]]
E[[E_{1} O E_{2} ]]  = λρ.\underline{λσ.}O[[O]](E[[E_{1} ]]ρ\underline{σ}, E[[E_{2} ]]ρ\underline{σ})
E[[I ]]  = λρ.\underline{λσ.}\underline{[λe.e, λl.σ(l)]}(ρ(I ))
E[[let D in E]] = λρ.\underline{λσ.}\underline{(λ(ρ′, σ′).E[E]](ρ[ρ′])σ′)}(D[[D]]ρ\underline{σ})
D[[const I = E]] = λρ.\underline{λσ.}((I ↦ E[[E]]ρ\underline{σ})\underline{, σ})
D[[D_{1} and D_{2} ]] = λρ.\underline{λσ.}\begin{matrix}\underline{(λ(ρ_{1} , σ_{1} ).}\underline{(λ(ρ_{2} , σ_{2} ).(ρ_{1} ∪ ρ_{2} , σ_{2} ))}(D[[D_{2} ]]ρ\underline{σ_{1}} )) \\ (D[[D_{1} ]]ρ\underline{σ}) \end{matrix}
D[[var I ]]  = λρ.λσ.(λ(l, σ′).(I ↦ l, σ′))(new(σ))
C[[I := E]]  = λρ.λσ.σ[ρ(I ) ↦ E[[E]]ρσ]
C[[C_{1} ; C_{2} ]]  = λρ.λσ.C[[C_{2} ]]ρ(C[[C_{1} ]]ρσ)

B Action Notation

Here, the symbols of action notation that are used in Appendix C are merely listed. Explanations of their intended operational interpretation may be found in [15, 16] (although the reader may well be able to guess it from the words used, and from the examples in Appendix C, which are for the same language constructs as in Appendix A.)

Action combinators: (arguments and results of sort action)

and , then , and then , or , furthermore , hence , …

Action primitives: (arguments of sort yielder, results of sort action) give , bind to , store in , allocate , …

Yielders: (arguments of sort yielder)

given , given # , it, the bound to , the stored in , …

Data sorts: (subsorts of yielder)

datum, bindable, storable, cell, truth, …

C Action Semantics

C.1 Initial Description

C.1.1 Abstract Syntax See Appendix A.1.1.

C.1.2 Semantic Entities includes: Action Notation [15]. introduces: value, number.

value = number | truth.
bindable = number.
datum ≥ value | bindable.

C.1.3 Semantic Functions includes: Abstract Syntax, Semantic Entities. introduces: evaluate , value of , result of , elaborate .

evaluate : Exp → action[giving a value].
value of : Nml → number.
result of : Opr → yielder[of a value].
elaborate : Dcl → action[binding].
evaluate[[N ]]  = give value of N
evaluate[[E_{1} O E_{2} ]]  = (evaluate E_{1} and then evaluate E_{2} ) then give result of O
evaluate[[I ]]  = give the value bound to I
evaluate[[let D in E]] = (furthermore elaborate D) hence evaluate E
elaborate[[const I = E]] = evaluate E then bind I to the given value
elaborate[[D_{1} and D_{2} ]] = elaborate D_{1} and elaborate D_{2}

… (definitions of valueof , resultof omitted)

C.2 A Simple Extension

Only minor changes, underlined below, are needed to the initial description, to take account of the extension of the language with imperative features.

C.2.1 Abstract Syntax See Appendix A.2.1.

C.2.2 Semantic Entities

bindable = number \underline{| cell}.
storable = number.
datum ≥ value | bindable \underline{| storable | cell}.

C.2.3 Semantic Functions introduces: execute .

elaborate : Dcl → action[binding \underline{| storing}]
execute : Cmd → action[storing]
evaluate[[I ]]  = give the value bound to I \underline{or give the value stored in the cell bound to I}
elaborate[[var I ]] = allocate a cell then bind I to it
execute[[I := E]] = (give the cell bound to I and evaluate E) then store the given value#2 in the given cell#1
execute[[C_{1} ; C_{2} ]] = execute C_{1} and then execute C_{2}

D Modular Monadic Semantics

D.1 Initial Description

D.1.1 Abstract Syntax See Appendix A.1.1.

D.1.2 Monad See Appendix A.1.2 for the domains used below.

return : a → M a
>>= : M a × (a → M b) → M b

type M a = EnvT Env Id a (i.e., M a = Env → a for any type a)

rdEnv : M Env  (returns the current environment)
inEnv : Env → (M a → M a) (computes in the argument environment)

D.1.3 Semantic Functions

E : Exp → M EV
N: Nml → N
O: Opr → (EV × EV → EV)
D: Dcl → M Env
E[[N ]]  = return(N [[N ]])
E[[E_{1} O E_{2} ]]  = E[[E_{1} ]] >>= λe_{1} . E[[E_{2} ]] >>= λe_{2} . return(O[[O]](e_{1} , e_{2} ))
E[[I ]]  = rdEnv >>= λρ. return(ρ(I ))
E[[let D in E]] = rdEnv >>= λρ. D[[D]] >>= λρ′. inEnv(ρ[ρ′])(E[[E]])
D[[const I = E]] = E[[E]] >>= λe. return(I ↦ e)
D[[D_{1} and D_{2} ]] = D[[D_{1} ]] >>= λρ_{1} . D[[D_{2} ]] >>= λρ_{2} . return(ρ_{1} ∪ ρ_{2} )

… (definitions of N , O omitted)

D.2 A Simple Extension

Only minor changes, underlined below, are needed to the initial description, to take account of the extension of the language with imperative features.

D.2.1 Abstract Syntax See Appendix A.2.1.

D.2.2 Monad See Appendix A.2.2 for the domains used below. type M a = EnvT Env (\underline{StateT S} Id) a (i.e., M a = Env → (\underline{S → a × S}) for any type a)

alloc : M Loc  (allocating storage)
read : Loc → M SV  (updating storage)
write : Loc × SV → M () (inspecting storage)

D.2.3 Semantic Functions

C: Cmd → M ()
E[[I ]]  = rdEnv >>= λρ. \underline{[λe. return(e), λl. read(l)]}(ρ(I ))
D[[var I ]] = alloc >>= λl. return(I ↦ l)
C[[I := E]] = rdEnv >>= λρ. E[[E]] >>= λe. write(ρ(I ), e)
C[[C_{1} ; C_{2} ]] = C[[C_{1} ]] >>= λ(). C[[C_{2} ]]

E Structural Operational Semantics

E.1 Initial Description

E.1.1 Abstract Syntax

See Appendix A.1.1.

E.1.2 Configurations

The following productions extend the abstract syntax so that constructs may be replaced by their values (which will be terminal configurations for the corresponding transition relations below):

(Exp) E ::= … | e
(Nml) N ::= … | n
(Dcl) D ::= … | ρ

For brevity and uniformity, let e ∈ EV, n ∈ N, ρ ∈ Env, etc., range over the domains specified in Appendix A.1.2 (although here, the domains should really be regarded as ordinary sets). Note that our example language does not already contain literal constants for all expressible values: truth-values need to be added.

E.1.3 Transition Relations

⊢ → : Env × Exp × Exp ⊢ → : Env × Dcl × Dcl

E.1.4 Transition Rules

“Side-conditions” on rules are here written as premisses, for notational convenience.

\frac{ρ ⊢ E_{1} → E′_{1}}{ρ ⊢ E_{1} O E_{2} → E′_{1} O E_{2}}  \frac{ρ ⊢ E_{2} → E′_{2}}{ρ ⊢ e_{1} O E_{2} → e_{1} O E′_{2}}  \frac{e_{1} O e_{2} = e}{ρ ⊢ e_{1} O e_{2} → e}
\frac{ρ(I ) = e}{ρ ⊢ I → e} \frac{ρ ⊢ D → D′}{ρ ⊢ let D in E → let D′ in E} \frac{ρ[ρ′] ⊢ E → E′}{ρ ⊢ let ρ′ in E → let ρ′ in E′}
\overline{ρ ⊢ let ρ′ in e → e}  \frac{ρ ⊢ E → E′}{ρ ⊢ const I = E → const I = E′}

ρ ⊢ const I = d → (I ↦ d)

\frac{ρ ⊢ D_{1} → D′_{1}}{ρ ⊢ D_{1} and D_{2} → D′_{1} and D_{2}}

\frac{ρ ⊢ D_{2} → D′_{2}}{ρ ⊢ ρ_{1} and D_{2} → ρ_{1} and D′_{2}}  \frac{dom(ρ_{1} ) ∩ dom(ρ_{2} ) = ∅}{ρ ⊢ ρ_{1} and ρ_{2} → ρ_{1} ∪ ρ_{2}}

E.2 A Simple Extension

E.2.1 Abstract Syntax See Appendix A.2.1.

E.2.2 Configurations

(Cmd) C ::= … | ()

The single value () represents merely the termination of a command. Note that our example language does not already contain a null or skip command, which might have been used instead of ().

E.2.3 Transition Relations ⊢ → : Env × (Exp \underline{× S}) × (Exp \underline{× S}) ⊢ → : Env × (Dcl \underline{× S}) × (Dcl \underline{× S}) ⊢ → : Cmd × (Cmd \underline{× S}) × (Cmd \underline{× S}) The set S of stores is as specified in Appendix A.2.2.

E.2.4 Transition Rules The previously-given rules are no longer well-formed—the changes that have to be made in them are underlined below.

\frac{ρ ⊢ ⟨E_{1} , \underline{σ}⟩ → ⟨E′_{1} , \underline{σ′}⟩}{ρ ⊢ ⟨E_{1} O E_{2} , \underline{σ}⟩ → ⟨E′_{1} O E_{2} , \underline{σ′}⟩}  \frac{ρ ⊢ ⟨E_{2} , \underline{σ}⟩ → ⟨E′_{2} , \underline{σ′}⟩}{ρ ⊢ ⟨e_{1} O E_{2} , \underline{σ}⟩ → ⟨e_{1} O E′_{2} , \underline{σ′}⟩}

\frac{e_{1} O e_{2} = e}{ρ ⊢ ⟨e_{1} O e_{2} , \underline{σ}⟩ → ⟨e, \underline{σ}⟩}

\frac{ρ(I ) = e}{ρ ⊢ ⟨I , \underline{σ}⟩ → ⟨e, \underline{σ}⟩}  \frac{ρ(I ) = l σ(l) = s}{ρ ⊢ ⟨I , σ⟩ → ⟨s, σ⟩}

\frac{ρ ⊢ ⟨D, \underline{σ}⟩ → ⟨D′, \underline{σ′}⟩}{ρ ⊢ ⟨let D in E, \underline{σ}⟩ → ⟨let D′ in E, \underline{σ′}⟩}

\frac{ρ[ρ′] ⊢ ⟨E, \underline{σ}⟩ → ⟨E′, \underline{σ′}⟩}{ρ ⊢ ⟨let ρ′ in E, \underline{σ}⟩ → ⟨let ρ′ in E′, \underline{σ′}⟩}  \overline{ρ ⊢ ⟨let ρ′ in e, \underline{σ}⟩ → ⟨e, \underline{σ}⟩}

\frac{ρ ⊢ ⟨E, \underline{σ}⟩ → ⟨E′, \underline{σ′}⟩}{ρ ⊢ ⟨const I = E, \underline{σ}⟩ → ⟨const I = E′, \underline{σ′}⟩}

ρ ⊢ ⟨const I = d, \underline{σ}⟩ → ⟨(I ↦ d), \underline{σ}⟩

\frac{ρ ⊢ ⟨D_{1} , \underline{σ}⟩ → ⟨D′_{1} , \underline{σ′}⟩}{ρ ⊢ ⟨D_{1} and D_{2} , \underline{σ}⟩ → ⟨D′_{1} and D_{2} , \underline{σ′}⟩}

\frac{ρ ⊢ ⟨D_{2} , \underline{σ}⟩ → ⟨D′_{2} , \underline{σ′}⟩}{ρ ⊢ ⟨ρ_{1} and D_{2} , \underline{σ}⟩ → ⟨ρ_{1} and D′_{2} , \underline{σ′}⟩} \frac{dom(ρ_{1} ) ∩ dom(ρ_{2} ) = ∅}{ρ ⊢ ⟨ρ_{1} and ρ_{2} , \underline{σ}⟩ → ⟨ρ_{1} ∪ ρ_{2} , \underline{σ}⟩}
\frac{l ∉ dom(σ))}{ρ ⊢ ⟨var I , σ⟩ → ⟨(I ↦ l), σ[l ↦ ⊥]⟩}  \frac{ρ ⊢ ⟨E, σ⟩ → ⟨E′, σ′⟩}{ρ ⊢ ⟨I := E, σ⟩ → ⟨I := E′, σ′⟩}
\frac{ρ(I ) = l}{ρ ⊢ ⟨I := s, σ⟩ → σ[I ↦ s]}  \frac{ρ ⊢ ⟨C_{1} , σ⟩ → ⟨C′_{1} , σ′⟩}{ρ ⊢ ⟨C_{1} ; C_{2} , σ⟩ → ⟨C′_{1} ; C_{2} , σ′⟩}

\overline{ρ ⊢ ⟨(); C_{2} , σ⟩ → ⟨C_{2} , σ⟩}

Recent BRICS Report Series Publications

RS-98-42 Peter D. Mosses. Semantics, Modularity, and Rewriting Logic. December 1998. 20 pp. Appears in Kirchner and Kirchner, editors, International Workshop on Rewriting Logic and its Applications, WRLA ’98 Proceedings, ENTCS 15, 1998.

RS-98-41 Ulrich Kohlenbach. The Computational Strength of Extensions of Weak König’s Lemma. December 1998. 23 pp.

RS-98-40 Henrik Reif Andersen, Colin Stirling, and Glynn Winskel. A Compositional Proof System for the Modal μ-Calculus. December 1998. 29 pp.

RS-98-39 Daniel Fridlender. An Interpretation of the Fan Theorem in Type Theory. December 1998. 15 pp. To appear in International Workshop on Types for Proofs and Programs 1998, TYPES ’98 Selected Papers, LNCS, 1999.

RS-98-38 Daniel Fridlender and Mia Indrika. An n-ary zipWith in Haskell. December 1998. 12 pp.

RS-98-37 Ivan B. Damgård, Joe Kilian, and Louis Salvail. On the (Im)possibility of Basing Oblivious Transfer and Bit Commitment on Weakened Security Assumptions. December 1998. 22 pp. To appear in Advances in Cryptology: International Conference on the Theory and Application of Cryptographic Techniques, EUROCRYPT ’99 Proceedings, LNCS, 1999.

RS-98-36 Ronald Cramer, Ivan B. Damgård, Stefan Dziembowski, Martin Hirt, and Tal Rabin. Efficient Multiparty Computations with Dishonest Minority. December 1998. 19 pp. To appear in Advances in Cryptology: International Conference on the Theory and Application of Cryptographic Techniques, EURO-CRYPT ’99 Proceedings, LNCS, 1999.

RS-98-35 Olivier Danvy and Zhe Yang. An Operational Investigation of the CPS Hierarchy. December 1998.

RS-98-34 Peter G. Binderup, Gudmund Skovbjerg Frandsen, Peter Bro Miltersen, and Sven Skyum. The Complexity of Identifying Large Equivalence Classes. December 1998. 15 pp.