BRICS RS-95-25 S. B. Lassen: Basic Action Theory

BRICS

Basic Research in Computer Science

Basic Action Theory

S�ren B. Lassen

BRICS Report Series RS-95-25 ISSN 0909-0878 May 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. 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@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

Basic Action Theory ^{∗}

S. B. Lassen BRICS^{†} Department of Computer Science University of Aarhus

                email: thales@brics.aau.dk
          URL: http://www.daimi.aau.dk/~thales

Abstract

Action semantics is a semantic description framework with very good pragmatic properties but until now a rather weak theory for reasoning about programs. A strong action theory would have a great practical potential, as it would facilitate reasoning about the large class of programming languages that can be described in action semantics.

This report develops the foundations for a richer action theory, by bringing together concepts and techniques from process theory and from work on operational reasoning about functional programs. Semantic preorders and equivalences in the action semantics setting are studied and useful operational techniques for establishing contextual equivalences are presented. These techniques are applied to establish equational and inequational action laws and an induction rule.

∗A preliminary version was presented at the 6th Nordic Workshop on Programming Theory, Aarhus, October 17–19, 1994, and appeared in the workshop proceedings.

†Basic Research in Computer Science, Centre of the Danish National Research Foundation.

Contents

1 Introduction 1

2 Action Semantics 3 2.1 Action semantic descriptions . . . . . . . . . . . . . . . . . . . . . 3 2.2 Action notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.3 Basic actions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.4 Action laws . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

3 Reduction semantics 7 3.1 Decomposition . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.2 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.3 Properties of evaluation . . . . . . . . . . . . . . . . . . . . . . . 9

4 Contextual testing 11 4.1 Definedness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 4.2 Contextual testing equivalence . . . . . . . . . . . . . . . . . . . . 12 4.3 Basic action theory . . . . . . . . . . . . . . . . . . . . . . . . . . 13

5 Finite testing 16 5.1 Open extension . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 5.2 Precongruence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 5.3 Soundness of open extension . . . . . . . . . . . . . . . . . . . . . 18

6 Alternative characterisation 20 6.1 Experimental order proof technique . . . . . . . . . . . . . . . . . 21 6.2 Basic context lemma . . . . . . . . . . . . . . . . . . . . . . . . . 24 6.3 Stronger characterisations . . . . . . . . . . . . . . . . . . . . . . 27

7 Simulation 28 7.1 may and must simulation . . . . . . . . . . . . . . . . . . . . . . 28 7.2 Simulation proof techniques . . . . . . . . . . . . . . . . . . . . . 30 7.3 Simulation versus contextual testing . . . . . . . . . . . . . . . . . 32 7.4 Identity of all characterisations . . . . . . . . . . . . . . . . . . . 34

8 (In)equational action theory 35 8.1 Equational theory . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 8.2 Inequational theory . . . . . . . . . . . . . . . . . . . . . . . . . . 37

9 Stuck actions 39

10 Generalisations to other facets 40

11 Conclusion 42 References 44 Index of symbols 47

1 Introduction

In this report we develop a richer theory for reasoning about programs in action semantics (AS). Because AS is a general semantic description framework, our work has a wide practical scope. A strong action theory would offer techniques for reasoning about programs in any programming language that can be described in AS.

AS is a denotational-style semantics. An action semantic description (ASD) maps program terms to the semantic entities they denote. The semantic entities are called actions. ASDs are compositional, therefore language terms are contextually equivalent if their denotations, i.e. actions, are equivalent by a suitable notion of action equivalence.

The undertaking of this report is to examine notions of semantic equivalence of actions and techniques for reasoning about these action equivalences.

Existing action theory

Action theory has hitherto mainly consisted of a series of action laws that codify algebraic properties of actions. Mosses [22, App.C] defines a testing equivalence (a sort of may equivalence [13]), based on a structural operational semantics for actions, and develops a bisimulation proof technique. By means of bisimulation, (almost) all action laws can be shown to respect testing equivalence.

This report reworks and strengthens the foundations of Mosses’ approach and rectifies some deficiencies therein. Moreover, we obtain a richer theory by working with a range of preorders and equivalences.

Reasoning with actions

Actions have functional, imperative, as well as concurrent features. There is thus a great range of places to look for inspiration for developing action theory. This report treats a subset of actions focussing on nondeterminism and parallelism but all the theory is set up with a view to future extension to the full set of actions.

Process theory Testing [4] and bisimulation [31] are notions widely used in concurrency. Our definitions of preorders and equivalences for actions are based on testing and some of our proof techniques use (bi)simulation.

Bisimulation is normally the strongest equivalence considered in semantics and is, generally, included in all other equivalences. We shall consider weak bisimulation that abstracts away from unobservable, internal computation steps. Standard weak bisimulation doesn’t guarantee test equivalence, however, because it is insensitive to internal divergence. Therefore we use refined, divergencesensitive (bi)simulations [35, 34, 28].

Operational reasoning about functional programs In recent years, bisimulation has been subject to much study in functional settings, mostly for pure, deterministic languages but also in conjunction with input/output, state, nondeterminism, or parallelism. (Gordon [10] explains and summarises research in this area.) This research has, however, paid scant attention to testing equivalence in the presence of nondeterminism. In this report we wish to develop a testing theory for actions and therefore take a different approach as starting point, namely Ian Mason and Carolyn Talcott’s operational framework for reasoning about impure functional languages which lends itself better to testing. They have developed powerful operational techniques for deciding program equivalences that involve memory [19, 14] and have also applied their techniques to a concurrent Actor language [1].

A drawback of these functional approaches is that they deal with particular, idealised functional languages. Bisimulation techniques seem to be applicable to most operationally defined languages but a considerable amount of work is required to set up the framework. Mason and Talcott have treated a number of programming concepts but it is not clear how to apply their techniques to other programming languages in general—the operational semantics must be of a certain form (does this constrain the class of languages that can be considered?) and, for every language, comprehensive efforts are required to develop the basic theory.

In contrast, if we can develop a strong action theory, it will apply readily to the large class of programming languages that admit an ASD.

Why actions? It may appear paradoxical why we should not be content with a strong theory of λ-calculi and functional languages since λ-calculi are used extensively as meta-language for denotational semantics. However, for large programming languages, the encoding of semantics as higher-order functions, dictated by λ-calculi, tends to yield inaccessible semantic descriptions that are hard to maintain and extend. Actions have been designed to rectify these deficiencies and experience with action semantics substantiates this claim.

We shall in the following apply the various operational techniques to develop an inequational and equational theory for actions. We have managed to fit actions into Mason and Talcott’s framework and to generalise their techniques to nondeterminism as it appears in actions. On the basis of this, we have moreover developed more elegant simulation proof methods.

In what follows only the results for a small subset of actions are reported. The subset serves to illustrate the major interesting points of the theory. We have extended these results to substantial parts of the language of actions but a full presentation becomes very lengthy. We plan to report on further portions of our work in the near future.

Overview

Section 2 introduces AS as well as the ‘basic’ actions and action laws to be treated in the rest of the report. In order to fit actions into Mason and Talcott’s framework, Section 3 defines a so-called reduction semantics for actions. In Section 4, contextual testing preorders and equivalences are defined and the equivalence classes are determined. Section 5 and Section 6 establish a context lemma and, based on this, develops a technique for proving actions preordered. Section 7 develops simulation proof methods which are used to sketch an inequational and equational action theory in Section 8 in terms of action laws and an induction rule. In Section 9 the role of ‘stuck’ actions is discussed. Section 10 surveys the generalisation of the theory to arbitrary actions. A discussion of future and related work concludes the report.

2 Action Semantics

Action semantics (AS) is a semantic description framework with very good pragmatic properties [22]. It has been used to formalise a wide range of realistic programming languages, as demonstrated by complete descriptions of Pascal [25], ANDF [12], most of Occam2 [3], as well as numerous other functional, procedural, object-oriented, and parallel languages. Moreover, a number of compiler generators have been based on AS [30, 5, 27, 29].

2.1 Action semantic descriptions

An action semantic description (ASD) consists of compositional semantic functions that map abstract syntax to the universal domain of actions. Suppose we have an imperative language with a syntactic category Statement in the abstract syntax. We can have a semantic function such as:

• execute :: Statement → action .

Some example semantic equations:

(1) execute “skip” = complete .

(2) execute [[ S_{1}:Statement “;” S_{2}:Statement ]] = execute S_{1} and then execute S_{2} .

(3) execute [[ “loop” S:Statement ]] = ( unfolding ( execute S and then unfold ) )

trap complete .

(4) execute “exit” = escape .

The actions appearing on the right hand sides of the semantic equations will be explained shortly.

2.2 Action notation

Action notation (AN) is the specification language of AS for expressing actions. It is a rich language which expresses common computational notions in a direct way. AN is structured into various facets according to the information being processed:

• The basic facet is concerned with control, no information is processed. Higher-order, exceptional, nondeterministic, and interleaving control flow are expressible.

• The functional facet—processes transient data; features unbounded choice.

• The declarative facet—deals with bindings; control, data, and binding flow may be combined in various ways.

• The imperative facet—operates on a single-threaded storage.

• The communicative facet—connects distributed agents which communi-

cate asynchronously. The semantic equations above employ only the basic facet of AN. For simplicity we shall focus on the basic actions in this report. The operational machinery we shall present is currently developed for all but the communicative facet.

2.3 Basic actions

AN is a combinator-based notation. Actions are either primitives or compounds built using combinators. The outcome of performing an action is: completed, normal termination (subsequent processing continues normally); escaped, exceptional termination (transfers control to an exception handler); failed, abnormal termination (aborts current processing); or divergent, no termination. The basic primitives are: complete, escape, and fail, completes, escapes, and fails, respectively. check , takes a truth value argument and completes if it is true and fails if it is

false. enact , invokes the abstraction yielded by its argument—an abstraction is an

abstracted (or ‘reified’) action. unfold, marks a point of recursion in the body of the unary combinator unfolding (see

below).

The basic combinators are:

and then, binary sequential combinator.

and, binary combinator; performs its two subactions in any, arbitrarily interleaved order.

trap, binary combinator; performs its second subaction as an exception handler if the first subaction escapes.

or, binary choice combinator; if one subaction fails, the other is chosen, if neither subaction fails, one is chosen nondeterministically.

unfolding, unary recursion combinator; the primitive unfold in the subaction of unfolding denotes a recursive unwinding of the subaction. A divergent action is most shortly written unfolding unfold . (Let diverge abbreviate this action.)

A grammar of basic AN can be specified in unified algebras [24] as follows (the vertical bar denotes sort union):

• action-primitive = complete escape fail check yielder enact yielder unfold .

• action = action-primitive action and then action action and action action trap action action or action unfolding action .

• yielder = truth-value abstraction .

The arguments to the parameterised primitives check and enact are called yielders. In the basic facet, yielders are just constants: either truth values,

• truth-value = true false ,

or abstractions, built from actions using the constructor abstraction of ,

• abstraction of :: action → abstraction .

Open and closed actions

An action A is closed if it has no ‘free’ occurrences of the primitive unfold, i.e. occurrences not enclosed by the unary combinator unfolding. Otherwise it is open. Let closed-action denote the action subsort consisting of all closed actions. Open actions are only meaningful as subactions of unfolding. Only closed actions can be performed.

The operator @ substitutes its second argument for all free occurrences of the primitive unfold in the first argument, (A_{1}@A_{2} =“A_{1}[A_{2}/unfold]”).

• @ :: action, action → action (associative, unit is unfold) .

(1) unfold@U = U .

(2) (unfolding A)@U = unfolding A .

(3) O(A_{1} … A_{n})@U = O(A_{1}@U … A_{n}@U) , if O ≠ unfolding .^{1}

(A, A_{i}, U range over actions and O is any action construct other than unfolding.)

A_{1}@A_{2} is closed if A_{1} or A_{2} is. An action A is closed if and only if A@U = A, for all actions U.

Action denotations

To illustrate how actions give semantics to programming language terms, consider two statements from the example language from before:

(i) skip . (ii) loop exit .

The semantic function execute maps them to a primitive and to a compound action, respectively; these actions are the ‘denotations’ of skip and loop exit.

(i) complete .

(ii)

( unfolding ( escape and then unfold ) )

trap complete .

The latter escapes inside the body of unfolding, is then caught by trap, and the whole action completes. We expect (i) and (ii) to be interchangeable and in Section 2.4 below we shall see that the action denotations are indeed equivalent.

Basic actions are not very expressive in themselves. Basic actions can just diverge or terminate in three different ways. In particular, they cannot process data in any way. Only when fused with data processing facets does the expressive power of basic actions become interesting. Nevertheless, the basic facet suffices to illustrate the main concepts and techniques which we shall present, and which apply equally well to the other facets.

2.4 Action laws

There are a series of ‘action laws’ that characterise actions. The following are a sample of basic action laws:

(1) check true = complete ; check false = fail .

1Normally, see [22], @ doesn’t substitute into bodies of abstractions. Our definition can be made to coincide with the usual definition by restricting abstraction to closed actions,

• abstraction = abstraction of closed-action .

(2) unfolding A = A @ unfolding A .

(3) (A_{1} and then A_{2}) and then A_{3} = A_{1} and then (A_{2} and then A_{3}) .

(4) complete and then A = A and then complete = A .

(5) escape and then A = escape ; fail and then A = fail .

(6) (A_{1} trap A_{2}) trap A_{3} = A_{1} trap (A_{2} trap A_{3}) .

(7) escape trap A = A trap escape = A .

(8) complete trap A = complete ; fail trap A = fail .

(9) (A_{1} or A_{2}) or A_{3} = A_{1} or (A_{2} or A_{3}) .

(10) fail or A = A or fail = A .

(11) A_{1} or A_{2} = A_{2} or A_{1} .

(12) A or A = A .

Law (1) characterises check. Law (2) states that unfolding is equal to its own unwinding. Laws (3)–(5) say that and then is associative, has complete as unit, and is left-absorbed by escape and fail. Laws (6)–(8) are corresponding laws for trap. The or combinator is furthermore commutative (11) and idempotent (12).

As an example application of these laws, the example actions (i)–(ii) above can be shown equal using laws (5), (2), (7).

A catalogue of action laws for all facets of AN may be found in [22, App.B]. In abstract semantic algebras [21], a precursor of AS, such laws served as an algebraic semantics of actions. However, establishing laws sufficient to define full action notation in this way doesn’t seem feasible.

3 Reduction semantics

Mason and Talcott operate on the basis of a ‘reduction semantics’ for their language. A reduction semantics is a small-step operational semantics that represents control and state syntactically.

Our first step towards fitting actions into Mason and Talcott’s framework is to define a reduction semantics for basic AN. (A preliminary sketch was presented in [16].) The essential novelty compared to [22, App.C] is that control is represented by means of evaluation contexts.

3.1 Decomposition

An evaluation context [8] (or reduction context [19]) is an action with a hole at a legal point of execution in the action. Either just a hole [ ], a hole to the left of the sequential combinators (seq is either of and then , trap ), or a hole on either side of the symmetric combinators (sym is either of and , or )—as a BNF grammar:

E ::= [ ] | E seq A | E sym A | A sym E ,

where A ranges over actions and E over evaluation contexts.

A redex R is any action that can make a transition directly (see the evaluation rules below). E[R] denotes the action obtained by filling R into the hole in E.

In an action E[R], the evaluation context E corresponds to the point of execution in the program, the program pointer, or current continuation. The redex R is the current instruction.

When an action A can be written as an evaluation context E filled with a redex R, viz. A = E[R], we say that A decomposes into E, R.

Remark 3.1 Decomposition is not unique. For example, there are two possible decompositions of A = check true or (check false and then escape),

namely A = E_{1}[check true] = E_{2}[check false],
where E_{1} = [ ] or (check false and then escape),

E_{2} = check true or ([ ] and then escape).

3.2 Evaluation

The evaluation rules decompose an action and replace the redex with a reduced (or unwound) action. Let A_{1},A_{2}:closed-action, A:action, and Y :yielder,

(1) E[check Y]  ↦ \{ \begin{matrix}E[complete] & if & Y = true \\ E[fail] & if & Y = false . \end{matrix}
(2) E[enact Y]  ↦ E[A_{1}] if Y = abstraction of A_{1} .
(3) E[unfolding A]  ↦ E[A@unfolding A].
(4) E[A_{1} and then A_{2}] ↦ \{ \begin{matrix}E[A_{1}] & if & A_{1} : escape fail \\ E[A_{2}] & if & A_{1} = complete . \end{matrix}
(5) E[A_{1} and A_{2}]  ↦ \{ \begin{matrix}E[A_{1}] & if & A_{1} : escape fail or A_{2} = complete \\ E[A_{2}] & if & A_{1} = complete or A_{2} : escape fail . \end{matrix}
(6) E[A_{1} trap A_{2}]  ↦ \{ \begin{matrix}E[A_{1}] & if & A_{1} : complete fail \\ E[A_{2}] & if & A_{1} = escape . \end{matrix}
(7) E[A_{1} or A_{2}]  ↦ \{ \begin{matrix}E[A_{1}] & if & A_{1} : complete escape or A_{2} = fail \\ E[A_{2}] & if & A_{1} = fail or A_{2} : complete escape . \end{matrix}

Terminology

Let success = complete escape , terminated = success fail .

An action is final if there are no transitions out of it. A computation from (or ‘performed by’) some action A is a sequence of transitions, A ↦ A_{1} ↦ A_{2} ↦ · · · .

Computations are successful and terminated if they end in final actions in success and terminated, respectively.

A non-terminated, final action is stuck, so is a computation ending in a stuck action. enact false is an example of a stuck action. In the following we shall assume that all actions are well-behaved: A closed action is well-behaved if it never gets stuck and all its subterms are well-behaved. (Section 9 discusses how stuck actions fit into our theory.)

An action A must converge, written A⇓, if all computations from A are finite.

Definition 3.2 ⇓ is the least predicate on closed actions satisfying

A⇓ iff, for all B, A ↦ B implies B ⇓ .

⇑ denotes the negation of ⇓ , A⇑ ⇔^{def} ¬(A⇓) .

⇓ can be expressed inductively:

⇓ = ⋃_{μ<ω} ⇓^{μ} where ⇓^{μ} = { A | (∀ B|A ↦ B) B ∈ ⋃_{ν<μ}⇓^{ν} } .

Basic action notation is finitely branching and by König’s lemma we only need to do induction over the finite ordinals (all μ<ω). If we add the functional facet which introduces countably branching nondeterminism, induction over all recursive ordinals is required [2].

3.3 Properties of evaluation

We need to develop some machinery for reasoning about evaluation. Our observations and results about evaluation rules and transitions are similar to Plotkin’s activity lemma [33] and Mason and Talcott’s ‘cr’ lemma [14], except for our focus on nondeterminism.

Evaluation contexts are special instances of arbitrary contexts C with any number of holes anywhere (also inside abstractions, unfoldings, etc.) In particular, actions are contexts with no holes. Contexts can be composed by filling the innermost into the outermost, C_{outer}[C_{inner}], and this composition is associative. Whenever E_{1} and E_{2} are evaluation contexts, so is their composition, E_{1}[E_{2}]. Consequently, by inspection of the evaluation rules above, A ↦ B implies E[A] ↦ E[B], for all evaluation contexts E.

Remark 3.3 Notice that, given a transition A ↦ B, the reduced redex need not be uniquely determined, as witnessed by the transition

diverge and diverge ↦ diverge and diverge ,

by reduction of either of the two occurrences of redex diverge = unfolding unfold.

Recall that @ substitutes its second argument for all free occurrences of unfold in its first argument. With the obvious extension of @ to contexts we have, for all contexts C and actions U, that C@U is a context and C[A]@U = (C@U)[A], for all closed A. The definition of open/closed actions naturally generalises to contexts too. Unless otherwise stated, evaluation contexts are always assumed to be closed.

Call a context ‘finite’ if no holes occur inside the combinator unfolding, in particular, all evaluation contexts are finite. Finite contexts F satisfy F [A]@U = (F @U)[A@U], for arbitrary actions A, U. Open actions A and closed, finite contexts F are in a one-to-one correspondence, A = F [unfold] and F = A@[ ], such that A@U = F [U], for all U.

We are going to use some properties of the interplay between evaluation and composition, i.e. how do actions composed of a context filled with an action evaluate? Consider such an action C[A] where C and A are closed. The contribution of C and A to the processing capabilities of C[A] is explicated by the following lemmas which we state without proofs. For notational convenience we restrict ourselves to the case when C is a finite context F.

The first lemma says that a context either (i) has a hole at an evaluation point in the context, i.e. the context E obtained by replacing all other holes of F by unfold is an open evaluation context, or (ii) can evaluate without reference to what is filled into its holes.

Lemma 3.4 For all closed, finite contexts F,

either (i) (∃ open E) F = E@[ ] ,

or else (ii) (∀ closed A, B′ | F [A] ↦ B′)

(∃ closed F′ | B′ = F′[A]) (∀ closed A′) F [A′] ↦ F′[A′] ,

where E is a (possibly open) evaluation context, and F′ a finite context.

The next lemma describes the role of A in a transition F [A] ↦ B′.

Lemma 3.5 Assume F, A are closed and F [A] ↦ B′. If A is not terminated,

(i) (∃ open E | F = E@[ ]) (∃ closed B | A ↦ B) B′ = (E@A)[B] ,
or (ii) (∃ closed F′ | B′ = F′[A]) (∀ closed A′) F [A′] ↦ F′[A′] .

(i) and (ii) are not mutually exclusive, as illustrated by remark 3.3:

diverge and diverge ↦ diverge and diverge ,

where F = E = F′ = (diverge and [ ]), A = B = diverge.

We shall mainly be interested in the special instance where F is an evaluation context. Then in case (i) E = F, and in case (ii) F′ is either an evaluation context or F′ = B′ (a context with no holes). Thus if an action makes a transition and the action decomposes into an evaluation context filled with a non-terminated subaction, then (i) the transition chooses a redex in the subaction, or a parallel redex is used which either (ii) doesn’t affect the subaction, or (iii) eliminates it:

Lemma 3.6 (Choice of execution point) If E[A] ↦ B′ and A is not terminated, then (i) (∃ closed B | A ↦ B) B′ = E[B] , or (ii) (∃ E′ | B′ = E′[A]) (∀ closed A′) E[A′] ↦ E′[A′] , or (iii) (∀ closed A′) E[A′] ↦ B′ .

4 Contextual testing

In this section, we define contextual test preorders and equivalences for actions.

4.1 Definedness

Let us introduce two ‘definedness’ predicates for actions. Action A may succeed, A↓_{may} , if there exists a successful computation from A. A must succeed, A↓_{must} , if all computations from A are successful.

Definition 4.1 (Defined) ↓_{may} and ↓_{must} are the least predicates satisfying

A↓_{may} if A ↦^{∗} S for some S:success .
A↓_{must} if A ≠ fail and ( A ↦ B implies B ↓_{must} ) .

↓_{must} is defined negatively: A ↓_{must} if no computation from A fails or diverges. (Consequently A↓_{must} if A is stuck, cf. Section 9).

Recall success = complete escape. These are the two ‘positive’ action outcomes that can be used constructively. I.e., a context may test whether an action completes or escapes and respond accordingly,

C_{complete} = ([ ] and then Response) , C_{escape} = ([ ] trap Response) .

It is impossible to respond deterministically to failed and divergent outcome. A simple consequence of the definition of ↓_{may} and ↓_{must} is:

Fact 4.2 If A ↦ B, then B ↓_{may} implies A↓_{may}, and A↓_{must} implies B ↓_{must}.

Let the preorders ≪_{may} and ≪_{must} order definedness of actions:

Definition 4.3 For closed actions A_{1}, A_{2} and m ∈ {may, must},

A_{1} ≪_{m} A_{2} iff A_{1} ↓_{m} ⇒ A_{2} ↓_{m} .

We will need the following inductive formulation of the definedness predicates and relations for induction proofs:

↓_{may} = ⋃_{λ<ω} ↓_{may}^{λ} where ↓_{may}^{λ} = success ∪ { A | ∃ B ∈ ⋃_{κ<λ}↓_{may}^{κ} . A ↦ B } .

↓_{must} = ⋃_{λ<ω} ↓_{must}^{λ} where ↓_{must}^{λ} = \{ A | \begin{matrix}A ≠ fail ∧ \\ (∀ B|A ↦ B) B ∈ ⋃_{κ<λ}↓_{must}^{κ} \} . \end{matrix}

≪_{m} = ⋂_{λ<ω} ≪_{m}^{λ} where A_{1} ≪_{m}^{λ} A_{2} ⇔ A_{1} ↓_{m}^{λ} ⇒ A_{2} ↓_{m} .

If countable nondeterminism is added, ↓_{must} and ≪_{must} run over all recursive ordinals as in definition 3.2. We shall phrase all induction proofs so that they also hold for transfinite induction and thus carry over to the more general case.

4.2 Contextual testing equivalence

Now we can define three contextual testing equivalences. They are derived from may and must preorders defined as the weakest precongruences ordering divergent actions below convergent ones, i.e. included in ≪_{may} and ≪_{must} .

Definition 4.4 (Contextual preorders) For arbitrary actions A_{1}, A_{2},

A_{1} ⊏ ∼_{may} A_{2} iff ∀ closing contexts C. C[A_{1}] ≪_{may} C[A_{2}] ,
A_{1} ⊏ ∼_{must} A_{2} iff ∀ closing contexts C. C[A_{1}] ≪_{must} C[A_{2}] ,

where C is closing if C[A_{i}] is closed, for i = 1, 2.

These contextual testing preorders generalise conventional contextual preorder to the nondeterministic case. Notice that these preorders are defined for both open and closed actions. We shall focus on the ‘closed’ preorders, i.e. these preorders restricted to closed actions only. (Section 5.3 will explain how to generalise our results to the general case.)

Let ≃_{may} and ≃_{must} denote the induced equivalences. Define ‘contextual equivalence’ as ≃ = ≃_{may} ∩ ≃_{must} .

These equivalences are, by definition, the weakest equivalences such that, in any context, equivalent subterms are interchangeable without any observable effect. One chooses may, must, or their intersection ‘≃’, dependent on one’s view of observation: whether one ignores divergence, regards divergence as catastrophic, or demands equal divergence properties, respectively.

As a rough intuition of the ⊏ ∼_{may} and ⊏ ∼_{must} preorders, they both mean ‘the left argument is more divergent than the right argument’, and both ⊐ ∼_{may} and ⊏ ∼_{must} mean ‘left argument is less deterministic than right argument’. Thus the divergent action diverge is both ⊥_{may} and ⊥_{must}, and the completely unpredictable action chaos is both ⊤_{may} and ⊥_{must}. Refer to the latter as the ‘implementation’ preorder, ⊏ ∼_{impl} = ⊐ ∼_{may} ∩ ⊏ ∼_{must} , i.e. specification S is implemented by the more deterministic implementation I if S ⊏ ∼_{impl} I. Notice that ≃ = ⊏ ∼_{impl} ∩ ⊐ ∼_{impl} .

Having all the contextual preorders, we can express more properties of actions by a variety of inequational laws. This will be exemplified in Section 8.

⊏ ∼_{may} and ⊏ ∼_{must} can be viewed as testing preorders, in the sense of [13], by taking the set of ‘tests’ or ‘experimenters’ to be all action contexts. A test or experiment C is performed on an action A by performing C[A]. If the computation is successful, A ‘passes’ test C.

The testing equivalence defined for actions in [22, C.4] corresponds to our may equivalence. (Both the notion of test and the notion of observation used there are a little less standard.) We shall instead take contextual equivalence, ≃ , as basic. It is a stronger equivalence, and thus a ‘safe compromise’ between the may and the must view of divergence, and it turns out that the action laws hold even for contextual equivalence.

Remark 4.5 (Reactive formulation) We would like our theory to generalise to AN’s communicative facet also. Testing for some reactive behaviour would seem more appropriate in that setting. In [13] a special action w signals success. Similarly, the test setup in [1] has an observer primitive event(). Suppose we define a special action event, that may occur in test contexts only, and check whether event may or must be performed during testing, then the resulting preorders will be the same as in definition 4.4. It is easy to see that the new preorders are as discriminating as the old: just replace every old context C_{success} by

C_{event} = (C_{success} and then event) trap event .

The opposite is less direct: in every new context, replace occurrences of event by escape and ensure that this exception is not trapped (somehow resolve conflicts with traps and other escapes in the context).

4.3 Basic action theory

There are, in fact, only 4 may and 8 must equivalence classes for closed basic actions. Define diverge, succeed, terminate, and chaos.

diverge = unfolding unfold . succeed = complete or escape . terminate = succeed trap (escape and fail) .

chaos = (diverge and fail and escape) trap succeed .

The or combinator discards any failing argument, i.e. if one argument fails the other is chosen. This gives or an ‘angelic’ flavour and makes it inapplicable for straightforward formulations of some of the actions above. To further the intuition behind the latter three, suppose we had a binary nondeterministic ‘internal’ or ‘demonic’ choice operator ⊕ (as in [13]) which chooses any of its two arguments without inspection of the other, then

succeed = complete ⊕ escape . terminate = success ⊕ fail . chaos = terminate ⊕ diverge .

complete ⊕ fail, escape ⊕ fail can be coded as

complete ⊕ fail = succeed trap fail . escape ⊕ fail = succeed and then fail .

The closed may and must orderings can be depicted as follows:^{2}

[figure: succeed = terminate = chaos = ⊤_{may}; complete; escape; diverge = ⊥_{may} = fail; complete; fail; escape; complete ; ⊕ fail; succeed; escape ; ⊕ fail; terminate; diverge = ⊥_{must} = chaos]

(Notice that ⊕ is the may least upper bound operator, ‘⊔_{may}’, and the must greatest lower bound, ‘⊓_{must}’, hence also the impl greatest lower bound, ‘⊓_{impl}’.)

In Section 7 we will show that the diagrams exactly describe the closed preorders. Here we only show that the may and must preorders are at least as discriminative as illustrated by the diagrams. To this end we define simple preorders that are in exact correspondence with the diagrams.

Definition 4.6 For closed actions A_{1}, A_{2}, define

A_{1} ⇀ ∼_{may} A_{2} iff (∀S:success | A_{1} ↦^{∗} S) A_{2} ↦^{∗} S ,
A_{1} ⇀ ∼_{must} A_{2} iff A_{1} ⇓ ⇒ A_{2} ⇓ ∧ (∀T :terminated | A_{2} ↦^{∗} T) A_{1} ↦^{∗} T .

2In [17] the must picture was erroneous.

These relations are easily shown to be preorders.

Proposition 4.7 The diagrams are exact descriptions of ⇀ ∼_{may} and ⇀ ∼_{must} .

Proof (sketch): By inspection of the diagrams, the preorders can be seen to make all the (implicit) distinctions in the diagrams: no two nodes in the diagrams can be merged and no lines can be added between the nodes.

Conversely, simple combinatorial arguments based on the definitions of ⇀ ∼_{may} and ⇀ ∼_{must} show that there are no more ⇀ ∼ equivalence classes than illustrated in the diagrams (in the must case we exclude the stuck equivalence class, cf. Section 9). It is easily checked that all lines between nodes reflect the preorders.

We shall now prove that the closed contextual preorders are included in ⇀ ∼_{may} and ⇀ ∼_{must} . Thus it follows by proposition 4.7 that the contextual preorders are at least as discriminative as depicted by the diagrams.

Lemma 4.8 For closed actions A_{1}, A_{2},

A_{1} ⊏ ∼_{may} A_{2} implies A_{1} ⇀ ∼_{may} A_{2} .
A_{1} ⊏ ∼_{must} A_{2} implies A_{1} ⇀ ∼_{must} A_{2} .

Proof: Let m ∈ {may, must}. Assume A_{1} ⊏ ∼_{m} A_{2}, hence C[A_{1}]↓_{m} ⇒ C[A_{2}]↓_{m} , for all closed C. Show A_{1} ⇀ ∼_{m} A_{2}:

\underline{m = may:} Let C_{1} = [ ] trap fail , C_{2} = [ ] and then fail . Examination of the evaluation relation shows, for all closed A,

C_{i}[A]↓_{may} ⇔ A ↦^{∗} S_{i} , for i = 1, 2 ,

where S_{1} = complete, S_{2} = escape. Thus C_{i}[A_{1}] ↓_{may} ⇒ C_{i}[A_{2}] ↓_{may} gives A_{1} ↦^{∗} S_{i} ⇒ A_{2} ↦^{∗} S_{i} , for i = 1, 2. This is exactly the definition of A_{1} ⇀ ∼_{may} A_{2}.

\underline{m = must:} Let C_{0} = [ ] or complete , C_{1} = ([ ] or escape) and then fail , C_{2} = ([ ] or complete) trap fail , C_{3} = [ ] .

These contexts satisfy, for all closed A,

C_{0}[A]↓_{must} ⇔ A⇓ ,
C_{i}[A]↓_{must} ⇔ A⇓ ∧ A ↛^{∗} T_{i} , for i = 1, .., 3 ,

where T_{1} = complete, T_{2} = escape, T_{3} = fail. Expand C_{i}[A_{1}] ↓_{must} ⇒ C_{i}[A_{2}]↓_{must} , for i = 0, .., 3, according to the above. Putting it all together yields the definition of A_{1} ⇀ ∼_{must} A_{2}.

5 Finite testing

The contextual test preorders are defined by quantification over arbitrary action contexts which makes it hard to reason about the preorders directly from the definition. In Section 6 we show that it suffices to quantify over evaluation contexts (the basic context lemma 6.10) and use this to show actions preordered. It is advantageous to perform the restriction from arbitrary contexts to evaluation contexts in two steps, namely first to restrict to finite contexts (where no holes occur inside the combinator unfolding). The restriction to finite contexts is most conveniently proved separately because it involves a thorough treatment of open and closed actions and contexts. The further restriction to evaluation contexts need only deal with closed actions and thus becomes more clear.

Before proceeding to Section 6 we carry out this first step. We shall prove the following lemma:

Lemma 5.1 (Finite restriction) For closed A_{1}, A_{2} and m ∈ {may, must},

A_{1} ⊏ ∼_{m} A_{2} if and only if ∀ closed, finite contexts F. F [A_{1}] ≪_{m} F [A_{2}] .

The ‘only if’ direction is immediate because closed, finite contexts are instances of arbitrary closed contexts. (Observe that for closed actions, every closed context is a closing context.) We shall postpone the proof of the ‘if’ direction till Section 5.2.

5.1 Open extension

The contextual preorders ⊏ ∼_{m} and equivalences ≃_{m} are defined for arbitrary actions. Yet, Section 4.3 as well as the following sections deal only with closed actions. In particular, we shall develop alternative characterisations of the semantic preorders that will be defined for closed actions only. In the terminology of Gordon [10], define their ‘open extensions’ as follows:

Given a relation on closed actions, R ⊆ closed-action × closed-action, its open extension is a relation on open actions R^{∘} ⊆ action × action,

A_{1}R^{∘}A_{2} ⇔^{def} ∀ U:closed-action. (A_{1}@U) R (A_{2}@U) ,

for arbitrary actions A_{1}, A_{2}. The open extensions of relations R and S coincide, R^{∘} = S^{∘}, if and only if the restrictions to closed actions of R and S coincide.

The proof of lemma 5.1 will establish that ⊏ ∼_{m}^{∘} is contained in ⊏ ∼_{m} , see Section 5.3. Hence any safe approximation R to ⊏ ∼_{m} on closed actions yields a safe approximation R^{∘} to ⊏ ∼_{m} . Therefore we shall be content with developing characterisations of ⊏ ∼_{m} on closed actions.

5.2 Precongruence

Lemma 5.1 can be restated as ⊏ ∼_{m}^{∘} = <_{@}_{m}^{∘} , for m ∈ {may, must}, where:

Definition 5.2 For all closed A_{1}, A_{2},

A_{1} <_{@}_{m} A_{2} ⇔^{def} ∀ closed, finite F. F [A_{1}] ≪_{m} F [A_{2}] .

Because of the correspondence between closed, finite contexts and open actions,

Fact 5.3 A_{1} <_{@}_{m} A_{2} ⇔ ∀A. A@A_{1} ≪_{m} A@A_{2} .

Our proof of lemma 5.1 follows the approach of Mason, Smith, and Talcott [14]. The crux of the proof consists of showing that <_{@}_{m}^{∘} is a precongruence.

Proposition 5.4 <_{@}_{m}^{∘} is a precongruence, i.e.

A_{1} <_{@}_{m}^{∘} A_{2} implies C[A_{1}] <_{@}_{m}^{∘} C[A_{2}] ,

for arbitrary actions A_{1}, A_{2}, contexts C, and m ∈ {may, must}.

Proof: By structural induction on C.

If C = [ ] or C has no holes, the result is immediate, in the latter case because <_{@}_{m}^{∘} is reflexive.

If C = O(C_{1} … C_{n}) and O ≠ unfolding , then, for all closed, finite contexts F and closed actions U,

F [C[A_{1}]@U] = F [O(C_{1} … C_{n})[A_{1}]]@U , since F is closed and finite
= F_{1}[C_{1}[A_{1}]@U] , where F_{1} = F [O([ ] C_{2}[A_{1}] … C_{n}[A_{1}])]@U
≪_{m} F_{1}[C_{1}[A_{2}]@U] , since C_{1}[A_{1}] <_{@}_{m}^{∘} C_{1}[A_{2}] by I.H. and F_{1} is closed and finite
= F_{2}[C_{2}[A_{1}]@U]
⋮
= F_{n}[C_{n}[A_{1}]@U]
≪_{m} F_{n}[C_{n}[A_{2}]@U] , by I.H. since F_{n} is closed and finite
= F [C[A_{2}]@U] ,

where F_{i} = F [O(C_{1}[A_{2}] … C_{i−1}[A_{2}] [ ] C_{i+1}[A_{1}] … C_{n}[A_{1}])]@U. Conclude

C[A_{1}] <_{@}_{m}^{∘} C[A_{2}].

If C = unfolding C_{0}, let A′_{i} = C_{0}[A_{i}], U_{i} = C[A_{i}] = unfolding A′_{i}, for i = 1, 2. A′_{1} <_{@}_{m}^{∘} A′_{2} by I.H. We must show U_{1} <_{@}_{m}^{∘} U_{2} which is equivalent to U_{1} <_{@}_{m} U_{2} because U_{i} is closed. We show ∀λ<ω. P (λ), where P (λ) ⇔ ∀ closed F. F [U_{1}] ≪_{m}^{λ} F [U_{2}], by induction on λ. Let λ<ω, assume ∀κ<λ. P (κ) and show P (λ): \underline{m = may:} Assume F [U_{1}]↓_{may}^{λ}. Either (1) F [U_{1}]:success, then F :success, hence F [U_{2}]:success and F [U_{2}]↓_{may}. Or (2) F [U_{1}] ↦ B′, B′ ↓_{may}^{κ} for some κ<λ. By lemma 3.5:

Either (i) B′ = (E@U_{1})[B] where F = E@[ ] and U_{1} ↦ B. Then B = A′_{1}@U_{1} by evaluation rule (3). Observe B′ = E[A′_{1}]@U_{1}. By I.H. and fact 5.3, B′ ↓_{may}^{κ} implies E[A′_{1}]@U_{2} ↓_{may} which can be written (E@U_{2})[A′_{1}@U_{2}] ↓_{may}. This implies (E@U_{2})[A′_{2}@U_{2}] ↓_{may} since A′_{1} <_{@}_{may}^{∘} A′_{2}. It is easily checked that

F [U_{2}] ↦ (E@U_{2})[A′_{2}@U_{2}], hence F [U_{2}]↓_{may} by fact 4.2.

Or (ii) B′ = F′[U_{1}] and F [U_{2}] ↦ F′[U_{2}]. Since F′[U_{1}] ↓_{may}^{κ}, F′[U_{2}] ↓_{may} by I.H., hence F [U_{2}]↓_{may} by fact 4.2.

\underline{m = must:} Assume F [U_{1}]↓_{must}^{λ}. F [U_{2}] = fail only if F = fail, in which case F [U_{1}] = fail. So F [U_{1}] ≠ fail implies F [U_{2}] ≠ fail. What remains to be shown is whenever F [U_{2}] ↦ B′, B′ ↓_{must}. By lemma 3.5:

Either (i) B′ = (E@U_{2})[B] where F = E@[ ], U_{2} ↦ B, and B = A′_{2}@U_{2}. Observe B′ = E[A′_{2}]@U_{2} and F [U_{1}] ↦ E[A′_{1}]@U_{1}. Hence E[A′_{1}]@U_{1} ↓_{must}^{κ} for some κ<λ. By I.H. and fact 5.3, E[A′_{1}]@U_{2} ↓_{must}. Now E[A′_{2}]@U_{2} ↓_{must} follows

from A′_{1} <_{@}_{must}^{∘} A′_{2}, i.e. B′ ↓_{must}.

Or (ii) B′ = F′[U_{2}] and F [U_{1}] ↦ F′[U_{1}]. Hence F [U_{1}] ↓_{must}^{κ} for some κ<λ. By I.H. F [U_{2}]↓_{must}, i.e. B′ ↓_{must}.

Thus ∀λ<ω. P (λ) is established which concludes the proof.

We are now in a position to prove the ‘if’ direction of lemma 5.1. Since <_{@}_{m}^{∘} is a precongruence and contained in ≪_{m} (trivial from the definition of <_{@}_{m}^{∘} ), <_{@}_{m}^{∘} ⊆ ⊏ ∼_{m} , because ⊏ ∼_{m} is defined as the weakest precongruence contained in ≪_{m}. In particular, this is the case when restricted to closed actions, <_{@}_{m} ⊆ ⊏ ∼_{m} . More formally:

Proof (lemma 5.1, ‘if’): Let m ∈ {may, must} and A_{1}, A_{2} be closed actions. Assume A_{1} <_{@}_{m} A_{2}, hence A_{1} <_{@}_{m}^{∘} A_{2}, and let C be any closing context and show C[A_{1}] ≪_{m} C[A_{2}]. C is closed so by the precongruence of <_{@}_{m}^{∘} (proposition 5.4), C[A_{1}] <_{@}_{m}^{∘} C[A_{2}]. Conclude since <_{@}_{m}^{∘} is included in ≪_{m}.

Thus <_{@}_{m} and ⊏ ∼_{m} coincide for closed actions and consequently <_{@}_{m}^{∘} and ⊏ ∼_{m}^{∘} coincide for arbitrary actions since the open extension R^{∘} of a relation R by definition is completely determined by the restriction of R to closed actions. Hence proposition 5.4 implies that ⊏ ∼_{m}^{∘} is a precongruence.

5.3 Soundness of open extension

Analogously to the proof of lemma 5.1 we get that ⊏ ∼_{m}^{∘} , being a precongruence, is included in ⊏ ∼_{m} :

Lemma 5.5 For arbitrary actions A_{1}, A_{2},

A_{1} ⊏ ∼_{m}^{∘} A_{2} implies A_{1} ⊏ ∼_{m} A_{2} .

Proof: Assume A_{1} ⊏ ∼_{m}^{∘} A_{2} and C is any closing context. By the precongruence of ⊏ ∼_{m}^{∘} , C[A_{1}] ⊏ ∼_{m}^{∘} C[A_{2}]. Since C[A_{i}] is closed, C[A_{1}] ⊏ ∼_{m} C[A_{2}]. Hence C[A_{1}] ≪_{m} C[A_{2}] because ⊏ ∼_{m} by definition is included in ≪_{m}.

This is the most important direction of implication. It means that for showing open actions preordered, it suffices to show them preordered by the open extension. In many common cases results about closed preorderings generalise straightforwardly to their open extensions.

E.g., for closed actions A_{1}, A_{2}, A_{1}R^{∘}A_{2} ⇔ A_{1}R A_{2}. More generally:

Fact 5.6 Let R be a relation on closed actions. For a clause of the form

∀A_{1}..A_{n}. LHS(A_{1}, .., A_{n}) R^{∘} RHS(A_{1}, .., A_{n}) ,  (1)

(normally the universal quantification over arbitrary actions is left implicit in action laws), in two cases it suffices to show that it holds for the closed relation R.

(i) When LHS and RHS are both ‘closing’, i.e., for arbitrary actions A_{1}, .., A_{n}, LHS(A_{1}, .., A_{n}) and RHS(A_{1}, .., A_{n}) are closed. In particular, this is the case when n = 0 and LHS() and RHS() are closed actions.

(ii) When @ distributes over both LHS and RHS, i.e.

\begin{aligned}LHS(A_{1}, .., A_{n})@U & = & LHS(A_{1}@U, .., A_{n}@U) , \\ RHS(A_{1}, .., A_{n})@U & = & RHS(A_{1}@U, .., A_{n}@U) , \end{aligned}  (2)

for arbitrary A_{1}, .., A_{n} and closed U, then (1) is equivalent to

∀closed A′_{1}..A′_{n}. LHS(A′_{1}, .., A′_{n}) R RHS(A′_{1}, .., A′_{n}) .  (3)

To see this, observe that, by definition of R^{∘}, (1) holds iff

∀A_{1}..A_{n}. ∀closed U. LHS(A_{1}, .., A_{n})@U R RHS(A_{1}, .., A_{n})@U . (4)

This is equivalent to (3) by property (2) and because A′_{i} = A_{i}@U is closed when U is and A′_{i}@U = A′_{i} when A′_{i} is closed.

With regard to (ii), note that @ distributes over all action constructs other than unfolding .

For instance, we only need to prove that the action laws from Section 2.4 hold for ≃ for closed actions (see Section 8): All the laws generalise to arbitrary actions and ≃^{∘} according to fact 5.6, hence also hold for ≃ by lemma 5.5.

The converse of lemma 5.5 is not true for basic actions only, at least not in the must case:

Example 5.7 Let A_{1} = (unfold and then complete), A_{2} = (unfold and then escape). They are distinguished by ⊏ ∼_{m}^{∘} by means of context C = ([ ] trap fail) and closed action U = complete,

C[A_{1}@U] = (complete and then complete) trap fail ≃ complete , C[A_{2}@U] = (complete and then escape) trap fail ≃ fail .

Hence A_{1} ≄_{must}^{∘} A_{2}.

When a closing context C′ is fed with an action A, either C′[A] can only perform without reference to A (A is ‘dead code’), or else performance of C′[A] can reach A. In the latter case, due to the simplicity of basic actions, if performance of A can reach an occurrence of unfold in A, A can necessarily be reached again, hence C′[A] may diverge. Consequently, either C′ doesn’t distinguish actions at all, or else, for all actions A which can reach an occurrence of unfold, C′[A] is equated to ⊥_{must} = diverge in the must ordering. For the example above, since A_{1} and A_{2} both have a reachable occurrence of unfold, A_{1} ≃_{must} A_{2}.

When other facets are added, action contexts become more expressive and the converse does hold. (For every closed context C and closed action U, it is possible to produce a closing context C_{U} such that C[A@U] ≃ C_{U}[A], for all A.)

6 Alternative characterisation

The definition of contextual preorders is difficult to use to prove actions preordered or equivalent. We need an alternative characterisation which gives a tractable way of determining equivalence. This approach is used by Hennessy for test preorders [13] and it is central to Mason and Talcott’s operational work. Inspired by the ‘ciu’ characterisation of the latter [19], define the following preorders for actions. Following Gordon [11], we call them ‘experimental’ preorders.

Definition 6.1 (Experimental preorders) For closed actions A_{1}, A_{2},

A_{1} < ≈_{may} A_{2} iff ∀ E. E[A_{1}] ≪_{may} E[A_{2}] ,
A_{1} < ≈_{must} A_{2} iff ∀ E. E[A_{1}] ≪_{must} E[A_{2}] ,

where E ranges over closed evaluation contexts.

‘Experimental equivalence’, ≈ , denotes the intersection of the two induced equivalences. Let < ≈_{impl} = > ≈_{may} ∩ < ≈_{must} , then ≈ = < ≈_{impl} ∩ > ≈_{impl} .

These preorders only quantify over evaluation contexts, not arbitrary contexts. This turns out to be much more tractable.

Just as for the inductive formulation of ≪_{may} and ≪_{must}, it is possible to express the experimental preorders as limits of sequences of approximations. For m ∈ {may, must},

< ≈_{m} = ⋂_{λ<ω} < ≈_{m}^{λ} where A_{1} < ≈_{m}^{λ} A_{2} ⇔ ∀E. E[A_{1}] ≪_{m}^{λ} E[A_{2}] ,

This gives a useful proof technique for showing actions experimental preordered: Prove ∀λ<ω. A_{1} < ≈_{m}^{λ} A_{2} by induction on λ.

6.1 Experimental order proof technique

The beauty of the experimental preorders is that actions can be proven experimental preordered essentially by induction on the length of their computations. The possibly interleaved performance of actions adds some complications (compared to Mason and Talcott’s sequential setting [14]; their parallel work [1] is not directly comparable to the parallelism of basic actions).

As an illustration of the proof technique employed, we shall prove two ‘evaluation lemmas’.

First the more general and weaker version which is proved by reference to fact 4.2:

Lemma 6.2 (Evaluation) A_{1} ↦ A_{2} implies A_{1} < ≈_{impl} A_{2} .

Proof: If A_{1} ↦ A_{2}, then also E[A_{1}] ↦ E[A_{2}], for all evaluation contexts E.

First show A_{1} > ≈_{may} A_{2}, i.e. ∀E. E[A_{2}]↓_{may} ⇒ E[A_{1}]↓_{may}. If E[A_{2}]↓_{may}, then since E[A_{1}] ↦ E[A_{2}], E[A_{1}]↓_{may}, by fact 4.2.

Next show A_{1} < ≈_{must} A_{2}, i.e. ∀E. E[A_{1}] ↓_{must} ⇒ E[A_{2}] ↓_{must}. If E[A_{1}] ↓_{must}, then since E[A_{1}] ↦ E[A_{2}], E[A_{2}]↓_{must}, by fact 4.2.

In accordance with our intuition that < ≈_{impl} means ‘less deterministic than’, we may read the preceding evaluation lemma as ‘evaluation reduces nondeterminism’.

Corollary 6.3 Some immediate consequences are:

(i) complete or A < ≈_{impl} complete . (ii) escape or A < ≈_{impl} escape . (iii) fail or A < ≈_{impl} A . (iv) complete and A < ≈_{impl} A .

(v) escape and A < ≈_{impl} escape .

(vi) fail and A < ≈_{impl} fail .

In deterministic settings, when one term can make a transition into another, then the terms are equivalent [9, 19]. This demonstrates how the presence of nondeterminism weakens our theory. Under certain conditions we may strengthen the evaluation lemma, however.

The proof of the following ‘determined’ version of the evaluation lemma employs the typical machinery for proofs of experimental orderings, namely induction on the length of computation, λ, using lemma choice of execution point (3.6).

Lemma 6.4 (Determined evaluation) If A_{1} ↦ A_{2} is the only transition out of A_{1}, then A_{1} ≈ A_{2} .

Proof: A_{1} > ≈_{may} A_{2} and A_{1} < ≈_{must} A_{2} follow from lemma 6.2. Note that since A_{1} ↦ A_{2}, A_{1} is not terminated.

A_{1} < ≈_{may} A_{2} follows from ∀λ<ω. A_{1} < ≈_{may}^{λ} A_{2} . Show this by induction on λ. Let λ<ω, assume ∀κ<λ. A_{1} < ≈_{may}^{κ} A_{2} , and show A_{1} < ≈_{may}^{λ} A_{2}: Assume E[A_{1}]↓_{may}^{λ}. We know A_{1} is not terminated, so E[A_{1}] is not in success. By the definition of ↓_{may}^{λ}, there is a B′ such that E[A_{1}] ↦ B′ and B′ ↓_{may}^{κ}, for some κ<λ. Show E[A_{2}]↓_{may} by application of lemma choice of execution point to E[A_{1}] ↦ B′:

Either (i) B′ = E[B] where A_{1} ↦ B. Since A_{1} ↦ A_{2} is the only transition out of A_{1}, B = A_{2}, B′ = E[A_{2}], and E[A_{2}]↓_{may}^{κ}, hence E[A_{2}]↓_{may}.

Or (ii) B′ = E′[A_{1}] and, for all A′, E[A′] ↦ E′[A′]. In particular, E[A_{2}] ↦ E′[A_{2}]. Since E′[A_{1}] ↓_{may}^{κ} we have E′[A_{2}] ↓_{may} by I.H., hence E[A_{2}] ↓_{may} by fact 4.2.

Or (iii) E[A′] ↦ B′ for all A′. In particular, E[A_{2}] ↦ B′, since B′ ↓_{may} we have E[A_{2}]↓_{may} by fact 4.2.

This concludes A_{1} < ≈_{may} A_{2}.

To show A_{1} > ≈_{must} A_{2}, show ∀λ<ω. A_{2} < ≈_{must}^{λ} A_{1} by induction on λ. Let λ<ω, assume ∀κ<λ. A_{2} < ≈_{must}^{κ} A_{1} , and show A_{2} < ≈_{must}^{λ} A_{1}: Assume E[A_{2}] ↓_{must}^{λ}. Since A_{1} is not terminated, E[A_{1}] ≠ fail. What remains to be shown is that E[A_{1}] ↦ B′ implies B′ ↓_{must}, for all B′. By lemma choice of execution point:

Either (i) B′ = E[B] where A_{1} ↦ B. Since A_{1} ↦ A_{2} is the only transition out of A_{1}, B = A_{2}, B′ = E[A_{2}], and B′ ↓_{must}^{κ}, hence B′ ↓_{must}.

Or (ii) B′ = E′[A_{1}] and, for all A′, E[A′] ↦ E′[A′]. In particular, E[A_{2}] ↦ E′[A_{2}]. E[A_{2}]↓_{must}^{λ} implies E′[A_{2}]↓_{must}^{κ} for some κ<λ. By I.H. E′[A_{1}]↓_{must},

hence B′ ↓_{must}.

Or (iii) E[A′] ↦ B′ for all A′. In particular, E[A_{2}] ↦ B′, hence B′ ↓_{must} by fact 4.2.

Conclude A_{1} > ≈_{must} A_{2}.

Corollary 6.5 Some laws from Section 2.4 are direct consequences:

(1) check true ≈ complete ; check false ≈ fail .

(2) unfolding A ≈ A @ unfolding A . (4)a complete and then A ≈ A .

(5) escape and then A ≈ escape ; fail and then A ≈ fail .

(7)a escape trap A ≈ A .

(8) complete trap A ≈ complete ; fail trap A ≈ fail .

Finally, we prove that fail is the least element of < ≈_{may} , a fact that will be used in Section 7. The proof is somewhat involved.

Proposition 6.6 fail < ≈_{may} A , for all closed A.

Proof: Simultaneously, we prove the inequational law A_{1}, A_{2} < ≈_{may} (A_{1} or A_{2}). Show ∀λ<ω. P (λ), where

P (λ) ⇔ ∀ closed A, A′, E. (i) E[fail]↓_{may}^{λ}⇒ E[A]↓_{may}
∧ (ii) E[A]↓_{may}^{λ} ∨ E[A′]↓_{may}^{λ} ⇒ E[A or A′]↓_{may},

by induction on λ. Let λ<ω, assume ∀κ<λ. P (κ) and show P (λ): First (i): Clearly E ≠ [ ] since not fail ↓_{may}. So let E = E_{0}[E_{1}] where E_{1} is the innermost layer of E; either E_{1} = ([ ] seq A_{1}), E_{1} = ([ ] sym A_{1}), or E_{1} = (A_{1} sym [ ]), (cf. the definition of evaluation contexts in Section 3.1).

Clearly E[fail] is not in success. Therefore there must be a transition E[fail] ↦ B′ such that B′ ↓_{may}^{κ} for some κ<λ. We will show that E[A] ↦ B′′ or E[A] = B′′

where (∗) B′′ = B′,
or (∗∗) B′ = E′[fail] and B′′ = E′[A′′] for some A′, E′,
or (∗∗∗) B′ = E′[A_{1}] and either B′′ = E′[A or A_{1}] or B′′ = E′[A_{1} or A].

In any case, conclude B′′ ↓_{may}; in case (∗) because B′ ↓_{may}^{κ}; in case (∗∗) by I.H.(i); in case (∗∗∗) by I.H.(ii). Therefore E[A]↓_{may} by fact 4.2.

We have E_{0}[E_{1}[fail]] = E[fail] ↦ B′ and E_{1}[fail] is not terminated so by lemma choice of execution point:

Either (i) B′ = E_{0}[B] and E_{1}[fail] ↦ B. Tedious examination of the evaluation rules shows either

(a) B = fail, then conclude (∗∗) with E′′ = E_{0}, A′′ = E_{1}[A]; or

(b) B = A_{1} and E_{1}[A] ↦ A_{1}, then (∗); or (c) B = E′_{1}[fail] where E′_{1} = ([ ] sym A′_{1}) or E′_{1} = (A′_{1} sym [ ]) and A_{1} ↦

A′_{1}, then (∗∗) with E′ = E_{0}[E′_{1}] and A′′ = A; or
(d) B = A_{1} and sym = or, then (∗∗∗) with E′ = E_{0}.

Or (ii) B′ = E′′[E_{1}[fail]] and E_{0}[E_{1}[A]] ↦ E′′[E_{1}[A]]. Then (∗∗) holds with E′ = E′′[E_{1}] and A′′ = A.

Or (iii) E_{0}[E_{1}[A]] ↦ B′, thus (∗).

Secondly (ii): Assume E[A]↓_{may}^{λ} (the case where only E[A′]↓_{may}^{λ} is symmetrical). If A = fail, then E[A or A′] ↓_{may} by (i) above. If A:success, evaluation rule (7) gives E[A or A′] ↦ E[A] and conclude E[A or A′]↓_{may} by fact 4.2. If A is not terminated, E[A] is not in success, therefore there is a B′ such that E[A] ↦ B′ and B′ ↓_{may}^{κ} for some κ<λ. Apply lemma choice of execution point to E[A] ↦ B′ and show, by examination of cases (i)–(iii), either E[A or A′] ↦ B′ and conclude by fact 4.2; or else B′ = E′[B] and E[A or A′] ↦ E′[B or A′] and conclude by I.H.

Remark 6.7 The above proof simplifies if < ≈_{may} is defined by quantification only over evaluation contexts without occurrences of the or combinator (see discussion in Section 6.3): Items (ii), (∗∗∗), and (d) above become superfluous.

The proof technique employed in the proofs of the evaluation lemmas and the above proposition is very general and powerful. Currently, everything we can prove about actions can be proved using this technique. But the proofs are lengthy and tedious and, moreover, they follow a common pattern. The simulation proof methods in Section 7 will distill this pattern and are more convenient to work with.

6.2 Basic context lemma

We shall now prove that the experimental preorders coincide with the corresponding closed contextual preorders. Thereby all the results we can show for the experimental orders, including the evaluation lemmas above, apply directly to the contextual orders also.

As explained in Section 5, lemma 5.1 establishes half of the claim. It states that finite contexts suffices for contextual testing, thus it remains to be shown that finite contexts and evaluation contexts are equally discriminative. Analogously to the proof of lemma 5.1, we show that the experimental preorders are preserved by all finite contexts. The coincidence of ⊏ ∼_{m} and < ≈_{m} is an easy consequence by reference to lemma 5.1.

First of all, all action constructs other than unfolding are monotone:

Lemma 6.8 All action constructs other than unfolding are monotone in < ≈_{m} .

Proof: Let A_{1}, A_{2} be closed actions and assume A_{1} < ≈_{m} A_{2}. For all action constructs O ≠ unfolding , let n be its arity and, for i = 1, …, n, let F_{i} = O(A_{1} … A_{i−1} [ ] A_{i+1} … A_{n}), and show F_{i}[A_{1}] < ≈_{m} F_{i}[A_{2}].

case F_{1} = enact abstraction of [ ]. (In the basic subset of AN that we consider, abstractions can only occur as immediate arguments to enact.) By lemma 6.4, F_{1}[A_{i}] = enact abstraction of A_{i} ≈ A_{i}. Conclude from

F_{i}[A_{1}] ≈ A_{1} < ≈_{m} A_{2} ≈ F_{i}[A_{2}] .

case F_{1} = [ ] and then A. For any evaluation context E, E[A_{i} and then A] = F [A_{i}], for i = 1, 2, where F = E[F_{1}] is an evaluation context.

By definition of A_{1} < ≈_{m} A_{2}, we get F [A_{1}] ≪_{m} F [A_{2}], i.e.

E[A_{1} and then A] ≪_{m} E[A_{2} and then A] .

Conclude (A_{1} and then A) < ≈_{m} (A_{2} and then A).

case F_{2} = A and then [ ]. First examine the case when A is terminated. Evaluation rule (4) gives the only out-going transition

A and then A_{i} ↦ \{ \begin{matrix}A & if & A : escape fail , \\ A_{i} & if & A = complete . \end{matrix}

By lemma 6.4,

A and then A_{i} ≈ \{ \begin{matrix}A & if & A : escape fail , \\ A_{i} & if & A = complete . \end{matrix}

Hence

(A and then A_{1}) ≈ (A and then A_{2}) if A : escape fail ,
(A and then A_{1}) < ≈_{m} (A and then A_{2}) if A = complete ,

by transitivity of ≈ and < ≈_{m} , using A_{1} < ≈_{m} A_{2} in the latter case.

For arbitrary closed A, we prove ∀λ<ω. P (λ) where

P (λ) ⇔ ∀ closed A. (A and then A_{1}) < ≈_{m}^{λ} (A and then A_{2}) ,

by induction on λ. Let λ<ω, ∀κ<λ. P (κ) and show P (λ): For terminated A, the conclusion follows by the above argument. So assume A is not terminated, E[A and then A_{1}]↓_{m}^{λ}, and show E[A and then A_{2}]↓_{m}.

\underline{m = may:} Clearly not E[A and then A_{1}]:success. Thus E[A and then A_{1}] ↦ B′_{1} where B′ ↓_{may}^{κ} for some κ<λ. By lemma choice of execution point:

Either (i) B′_{1} = E[B_{1}] where (A and then A_{1}) ↦ B_{1} which must be because A ↦ A′ and B_{1} = (A′ and then A_{1}) since A is not terminated. Hence also E[A and then A_{2}] ↦ E[A′ and then A_{2}] . By I.H. B′_{1} ↓_{may}^{κ} implies E[A′ and then A_{2}]↓_{may} and by fact 4.2, E[A and then A_{2}]↓_{may}.

Or (ii) B′_{1} = E′[A and then A_{1}] and E[A and then A_{2}] ↦ E′[A and then A_{2}]. By I.H. and fact 4.2, E[A and then A_{2}]↓_{may}.

Or (iii) E[A and then A_{2}] ↦ B′_{1} and by fact 4.2, E[A and then A_{2}]↓_{may}.

\underline{m = must:} Clearly E[A and then A_{2}] ≠ fail. We must furthermore show whenever E[A and then A_{2}] ↦ B′_{2}, B′_{2} ↓_{must}. By lemma choice of execution point:

Either (i) B′_{2} = E[B_{2}] and (A and then A_{2}) ↦ B_{2} which must be because A ↦ A′ and B_{2} = (A′ and then A_{2}) since A is not terminated. Hence also E[A and then A_{1}] ↦ E[A′ and then A_{1}] . Since E[A and then A_{1}] ↓_{must}^{λ}, E[A′ and then A_{2}] ↓_{must}^{κ} for some κ<λ and by I.H. B′_{2} ↓_{must}.

Or (ii) B′_{2} = E′[A and then A_{2}] and E[A and then A_{1}] ↦ E′[A and then A_{1}]. E′[A and then A_{1}]↓_{must}^{κ} for some κ<λ, hence B′_{2} ↓_{must} by I.H.

Or (iii) E[A and then A_{1}] ↦ B′_{2} and by fact 4.2, B′_{2} ↓_{must}.

This concludes case F_{2} = A and then [ ] .

The A trap [ ] case is similar to the A and then [ ] case. The remaining cases [ ] and A, A and [ ], [ ] or A, A or [ ], [ ] trap A are similar to the [ ] and then A case (these are evaluation contexts).

Consequently, all finite contexts are monotone:

Proposition 6.9 All closed, finite contexts are monotone in < ≈_{m} .

Proof: Assume A_{1} < ≈_{m} A_{2} and show F [A_{1}] < ≈_{m} F [A_{2}], for all closed, finite F, by structural induction on F.

If F = [ ] or F has no holes, the result is immediate. Otherwise, if F = O(F_{1} … F_{n}), by I.H. F_{i}[A_{1}] < ≈_{m} F_{i}[A_{2}], for i = 1, 2. O is

monotone since O ≠ unfolding, hence

F [A_{1}] = O(F_{1}[A_{1}] F_{2}[A_{1}] … F_{n−1}[A_{1}] F_{n}[A_{1}])
< ≈_{m} O(F_{1}[A_{2}] F_{2}[A_{1}] … F_{n−1}[A_{1}] F_{n}[A_{1}])
⋮
< ≈_{m} O(F_{1}[A_{2}] F_{2}[A_{2}] … F_{n−1}[A_{2}] F_{n}[A_{1}])
< ≈_{m} O(F_{1}[A_{2}] F_{2}[A_{2}] … F_{n−1}[A_{2}] F_{n}[A_{2}]) = F [A_{2}] .

We can now prove the following context lemma by the same proof technique as exercised for lemma 5.1 in Section 5.2.

Lemma 6.10 (Basic context lemma) For closed actions A_{1}, A_{2},

A_{1} ⊏ ∼_{may} A_{2} if and only if A_{1} < ≈_{may} A_{2} .
A_{1} ⊏ ∼_{must} A_{2} if and only if A_{1} < ≈_{must} A_{2} .

Proof: By reference to lemma 5.1 it suffices to show, for m ∈ {may, must},

∀ closed, finite F. F [A_{1}] ≪_{m} F [A_{2}] ⇔ A_{1} < ≈_{m} A_{2} .

‘⇒’ is immediate because evaluation contexts are instances of finite contexts. For ‘⇐’, assume A_{1} < ≈_{m} A_{2} and let C be any closed, finite context. By

proposition 6.9, C[A_{1}] < ≈_{m} C[A_{2}], and the result follows because < ≈_{m} by its definition is included in ≪_{m}.

6.3 Stronger characterisations

The experimental preorders restrict the set of observing contexts to evaluation contexts. Section 6.1 demonstrates how this restriction admits proofs by induction on the length of computation (the pattern of practically all experimental order proofs).

Further restrictions of the set of observing contexts—that still characterise the contextual preorders and still generalise to all facets—may expose general properties of actions but appear to be useful for special cases only. Essential simplifications of the experimental order characterisation cannot be obtained along this path. Nevertheless, let us mention a few possible restrictions:

In the may case (which normally has the simplest characterisation, cf. [13]) one can show that evaluation contexts without occurrences of the or combinator suffice. For an example where this stronger characterisation would be convenient, see remark 6.7.

As long as we have no side-effects allowing interference between interleaved actions—i.e., when we restrict ourselves to the basic, functional, and declarative facets—contexts with no occurrences of the interleaving combinator and suffice.

For basic actions, things are very simple and, in fact, only a small finite number of contexts are needed to distinguish the equivalence classes of the may and must relations. The 2 may contexts and the 4 must contexts listed in Section 4.3 are both sufficient and minimal. This can be verified by examining the pictures in Section 4.3. As soon as other facets are added, infinite collections of contexts are required to characterise the contextual preorders.

7 Simulation

The proofs for showing actions experimental preordered all follow the same pattern: Construct an invariant or relation and show the actions to evaluate to related actions or to the same action. By induction on ↓_{may} or ↓_{must} the result follows.

This is a straightforward but lengthy and tedious technique. Moreover the connection to co-inductive bisimulation proof techniques is striking. In this section, simple simulation proof principles will be established for actions.

7.1 may and must simulation

The ⇀ ∼_{m} preorders (definition 4.6) are simple ‘simulation-style’ preorders, defined in terms of entire computations.

Because of the possibly interleaved performance of actions, their semantics is defined in terms of atomic computation steps and simulation is also most appropriately phrased in terms of individual computation steps.

We define simulation co-inductively, inspired by the bisimulation for actions in [22, C.4]. Our may and must formulation is taken from [34].

Define two operators ⟨ ⟩_{may} and ⟨ ⟩_{must}:

Definition 7.1 Given a relation R ⊆ closed-action × closed-action, define relations ⟨R⟩_{may} , ⟨R⟩_{must} ⊆ closed-action × closed-action as follows

A_{1} ⟨R⟩_{may} A_{2} ⇔^{def} (I) A_{1}:success ⇒ A_{2} ↦^{∗} A_{1}

∧ (II) (∀B_{1} | A_{1} ↦ B_{1})(∃B_{2} | A_{2} ↦^{∗} B_{2}) B_{1}R B_{2} .
A_{1} ⟨R⟩_{must} A_{2} ⇔^{def}
A_{1} ⇓ ⇒ (I) A_{2} ⇓ ∧ (II) A_{2}:terminated ⇒ A_{1} ↦^{∗} A_{2} ∧ (III) (∀B_{2} | A_{2} ↦ B_{2})(∃B_{1} | A_{1} ↦^{∗} B_{1}) B_{1}R B_{2} .

Both ⟨ ⟩_{may} and ⟨ ⟩_{must} are easily seen to be monotone.

Call a post-fixed point of ⟨ ⟩_{may} a ‘may simulation’, and a post-fixed point of ⟨ ⟩_{must} a ‘must simulation’.

Fact 7.2 For m ∈ {may, must}, Id =^{def} {(A, A) | A:closed-action} is a m simulation, and if R and S are m simulations, so is their composition R S.

Definition 7.3

< ∼_{may}  =^{def} ⋃{R | R is a may simulation} ,
< ∼_{must} =^{def} ⋃{R | R is a must simulation} .

Thus A_{1} < ∼_{m} A_{2} if and only if there is a m simulation R such that (A_{1}, A_{2}) ∈ R. Call A_{1} ‘m similar to’ A_{2} if A_{1} < ∼_{m} A_{2}. Fact 7.2 implies Fact 7.4 < ∼_{may} and < ∼_{must} are reflexive and transitive, i.e. preorders.

Let ‘simulation equivalence’ denote the intersection of the induced equivalences of the two preorders. Notice that two actions are simulation equivalent if there is a symmetric relation containing them which is both a may and a must simulation; call such a relation an ‘equivalence simulation’.

Proposition 7.5 < ∼_{may} and < ∼_{must} are the largest may and must simulations, and the largest fixed points of ⟨ ⟩_{may} and ⟨ ⟩_{must}.

Proof: See lemma 1 and theorem 1 in [10].

Remark 7.6 One can also define a bisimulation preorder as in [35]: A_{1} is prebisimilar to A_{2} iff (A_{1}, A_{2}) ∈ νR.(⟨R⟩_{may} ∩ ⟨R⟩_{must}). The induced equivalence is sensitive to divergence and thus stronger than standard weak bisimulation in process calculus [20] and as defined for actions by Mosses [22, C.4]. This makes this pre-bisimulation equivalence stronger than both may and must contextual test equivalence which is not the case for standard weak bisimulation (see [20]).

The simulation preorders correspond to Ulidowski’s ‘copy+refusal testing’. For processes, Ulidowski shows that this refines our contextual preorders (but is coarser than pre-bisimulation).

Because the may and must simulations to some extent ‘mirror’ each other, they naturally combine into impl simulations. These prove very convenient and are used extensively for the development of the equational theory of actions in Section 8.1. As usual, define < ∼_{impl} = > ∼_{may} ∩ < ∼_{must} , that is, < ∼_{impl} = ⋃{R | R is an impl simulation} where R is an impl simulation if R is a must simulation and R^{−1} is a may simulation,

R ⊆ ⟨R⟩_{must} ∩ ⟨R^{−1}⟩_{may}^{−1} .

Define an auxiliary operator ⟨ ⟩_{impl} = ⟨ ⟩_{must} ∩ ⟨ ^{−1}⟩_{may}^{−1} . Notice that every symmetric impl simulation is an equivalence simulation.

Fact 7.7 The definition of ⟨ ⟩_{impl} expands to

A_{1} ⟨R⟩_{impl} A_{2} ⇔ (I) A_{1} ⇓ ⇒ (i) A_{2} ⇓ ∧ (ii) A_{2} = fail ⇒ A_{1} ↦^{∗} fail
∧ (II) A_{2}:success ⇒ A_{1} ↦^{∗} A_{2}
∧ (III) (∀B_{2} | A_{2} ↦ B_{2})(∃B_{1} | A_{1} ↦^{∗} B_{1}) B_{1}R B_{2} .

7.2 Simulation proof techniques

We shall now demonstrate the power of simulations by conducting a number of proofs of simulation orderings, including simulation order versions of the experimental order results from Section 6.1. The simpler simulation proofs demonstrate how may and must simulations expose the inductive backbone of the corresponding experimental order proofs.

It proves convenient to enhance the simulation proof technique in two ways:

• must and impl simulation proofs require arguments about convergence. But we shall escape the development of machinery for reasoning about convergence by defining a ‘hybrid weak/strong’ impl operator; it ensures that similar actions, say A_{1}, A_{2}, simulate each other so closely that whenever A_{2} diverges, so does A_{1}.

• General proof techniques for greatest fixed points of monotone operators will allow us to conduct simulation proofs using improper “simulations” that are smaller than proper post-fixed points of the ⟨ ⟩_{m} operators.

This subsection concludes by applying these techniques for proving simulation versions of the evaluation lemmas (6.2) and (6.4).

Simple examples

First three examples that demonstrate the concise co-inductive simulation proof method of exhibiting simulations:

Proposition 7.8 fail < ∼_{may} A , for all closed A.

Proof: R = {(fail, A) | A:closed-action} is a may simulation, i.e., for all A, fail ⟨R⟩_{may} A , because (I) fail is not in success; and (II) there are no transitions out of fail.

The proof is much simpler than that of proposition 6.6 because ⟨ ⟩_{may} has been defined to make fail the bottom element.

diverge is the must bottom element because diverge⇑:

Proposition 7.9 A_{1} ⇑ implies A_{1} < ∼_{must} A_{2} , for all closed A_{1}, A_{2}.

Proof: {(A_{1}, A_{2}) | A_{1}, A_{2}:closed-action, A_{1} ⇑)} is clearly a must simulation because A_{1} ⇑ implies A_{1} ⟨R⟩_{must} A_{2}, for all R, A_{1}, A_{2}.

chaos is both ⊤_{may} and ⊥_{must} (cf. Section 4.3):

Proposition 7.10 chaos < ∼_{impl} A , for all closed A.

Proof: R = {(chaos, A) | A:closed-action} is an impl simulation, i.e., for all A, chaos ⟨R⟩_{impl} A , because (I) chaos ⇑; (II) chaos ↦ S, for all S:success; (III) whenever A ↦ B_{2}, let B_{1} = chaos.

A ‘hybrid’ impl operator

The ⟨ ⟩_{must} and ⟨ ⟩_{impl} operators involve the convergence predicate, ⇓ , in order to make simulations sensitive to divergence. This obligation to prove actions convergent complicates reasoning. Another solution is to resort to strong (bi)simulation which is also sensitive to divergence but requires that (bi)similar programs make exactly the same number of computation steps.

A hybrid weak/strong impl operator, ⟨ ⟩_{impl}^{hybr}, is a convenient compromise:

Definition 7.11 For every relation R and closed actions A_{1}, A_{2},

A_{1} ⟨R⟩_{impl}^{hybr} A_{2} ⇔^{def} (I) A_{2}:terminated ⇒ A_{1} ↦^{∗} A_{2}

∧ (II) (∀B_{2} | A_{2} ↦ B_{2})(∃B_{1} | A_{1} ↦^{+} B_{1}) B_{1}R B_{2} .

⟨ ⟩_{impl}^{hybr} is monotone. Intuitively, A_{1} may perform no less steps than A_{2}. Whenever A_{1}RA_{2} for some R ⊆ ⟨R⟩_{impl}^{hybr} , if A_{2} may diverge, so may A_{1}.

The following lemma states that, in the course of proving a relation R an impl simulation, i.e. A_{1}R A_{2} implies A_{1} ⟨R⟩_{impl} A_{2}, it suffices to show A_{1} ⟨R⟩_{impl}^{hybr} A_{2}.

Lemma 7.12 R ⊆ ⟨R⟩_{impl} ∪ ⟨R⟩_{impl}^{hybr} implies R ⊆ ⟨R⟩_{impl} .

Proof (sketch): It suffices to show that the antecedent implies ⟨R⟩_{impl}^{hybr} ⊆ ⟨R⟩_{impl}. This is the case if A_{1} ⟨R⟩_{impl}^{hybr} A_{2} implies A_{1} ⇓ ⇒ A_{2} ⇓. The latter follows from ∀μ<ω. A_{1} ⇓^{μ} ⇒ A_{2} ⇓ and is shown by induction on μ.

In particular, every post-fixed point of ⟨ ⟩_{impl}^{hybr} is an impl simulation. E.g., Id ⊆ ⟨ ⟩_{impl}^{hybr} shows not only that the greatest fixed point of ⟨ ⟩_{impl}^{hybr} is reflexive but also that < ∼_{impl} is reflexive.

Lemma 7.12 allows impl simulation proofs to eschew direct reasoning about convergence by establishing both the necessary convergence properties and similarity in one co-inductive argument. This idea resembles Gordon’s ‘refined’ treatment of divergence for bisimulation of functional programs [11].

Properties of greatest fixed points

Paulson [32] and Gordon [11] use the following general properties of greatest fixed points:

Proposition 7.13 Let ν be the greatest fixed point of a monotone operator ⟨ ⟩,

ν =^{def} νR.⟨R⟩ . Then \begin{aligned}ν & = & νR.⟨R⟩ ∪ ν \\ & = & νR.⟨R ∪ ν⟩ \\ & = & νR.⟨R ∪ ν⟩ ∪ ν . \end{aligned}

A useful corollary applies to all the ⟨ ⟩ operators we consider:

Corollary 7.14 Whenever ⟨ ⟩ is monotone and Id ⊆ νR.⟨R⟩ ,

R ⊆ ⟨R ∪ Id⟩ implies R ⊆ νR.⟨R⟩ .

Proof: R ⊆ ⟨R ∪ Id⟩ ⇒ R ⊆ ⟨R ∪ νR.⟨R⟩⟩  , ⟨ ⟩ is monotone

⇒ R ⊆ νR.⟨R ∪ νR.⟨R⟩⟩ , by co-induction
⇒ R ⊆ νR.⟨R⟩  , by proposition 7.13.

Evaluation lemmas

We now prove simulation versions of the evaluation lemmas. The proofs apply hybrid impl simulation and corollary 7.14.

The analogue of lemma evaluation (6.2) is simple to show:

Lemma 7.15 A_{1} ↦ A_{2} implies A_{1} < ∼_{impl} A_{2} .

Proof: Let R = {(A_{1}, A_{2}) | A_{1} ↦ A_{2}}. Use lemma 7.12 and corollary 7.14 and show R ⊆ ⟨R ∪ Id⟩_{impl}^{hybr}, i.e. A_{1} ↦ A_{2} implies A_{1} ⟨R ∪ Id⟩_{impl}^{hybr} A_{2}: (I) A_{1} is not terminated; and (II) whenever A_{2} ↦ B_{2}, also A_{1} ↦^{2} B_{1}, so choose B_{2} = B_{1}.

The determined variant of lemma 7.15 is an example where ⟨ ⟩_{impl}^{hybr} is not applicable:

Lemma 7.16 If A_{1} ↦ A_{2} is the only transition out of A_{1}, then A_{1} is simulation equivalent to A_{2} .

Proof: Given lemma 7.15 and corollary 7.14, it suffices to show R ⊆ ⟨S ∪ Id⟩_{impl} where R = {(A_{2}, A_{1}) | A_{1} ↦ A_{2} is the only transition out of A_{1}} . Whenever A_{1} ↦ A_{2} is the only transition out of A_{1}, show A_{2} ⟨R ∪ Id⟩_{impl} A_{1}, using fact 7.7: (I)(i) follows by definition 3.2 since A_{1} ↦ A_{2} is the only transition out of A_{1}. (I)(ii) and (II) hold because A_{1} cannot be terminated when A_{1} ↦ A_{2}. To show (III), notice that A_{1} ↦ B_{2} implies B_{2} = A_{2}, so let A_{2} ↦^{0} B_{1} = B_{2}.

7.3 Simulation versus contextual testing

Our interest in simulations is as a tool for proving actions contextual preordered. Therefore we have to show that the simulation preorders are included in the contextual preorders. By the basic context lemma (6.10) it suffices to prove that they are included in the experimental preorders. A more standard path, due to Howe [15], is to show the simulation preorders to be precongruences—as in the proof of lemma 5.1—and consequently included in the contextual preorders. Given the basic context lemma, our approach is considerably simpler. (Mason, Smith, and Talcott follow a similar route in [18].)

Lemma 7.17 For closed actions A_{1}, A_{2},

A_{1} < ∼_{may} A_{2} implies  A_{1} < ≈_{may} A_{2} .
A_{1} < ∼_{must} A_{2} implies A_{1} < ≈_{must} A_{2} .

Proof: \underline{m = may:} Show ∀λ<ω. < ∼_{may} ⊆ < ≈_{may}^{λ} by induction on λ. Let λ<ω, assume ∀κ<λ. < ∼_{may} ⊆ < ≈_{may}^{κ}, and show < ∼_{may} ⊆ < ≈_{may}^{λ}: Assume A_{1} < ∼_{may} A_{2}, hence A_{1} ⟨ < ∼_{may} ⟩_{may} A_{2} because < ∼_{may} is a may simulation. If A_{1} is terminated, either A_{1} = fail in which case the result is immediate because fail is the may bottom element (proposition 6.6); or else A_{1}:success and A_{2} ↦^{∗} A_{1}, then conclude by lemma evaluation (6.2). If A_{1} is not terminated, assume E[A_{1}]↓_{may}^{λ} and show E[A_{2}]↓_{may}. E[A_{1}] is not in success since A_{1} is not terminated, therefore E[A_{1}] ↦ B′ and B′ ↓_{may}^{κ} for some κ<λ. By lemma choice of execution point:

Either (i) B′ = E[B_{1}] where A_{1} ↦ B_{1} and A_{2} ↦^{∗} B_{2} such that B_{1} < ∼_{may} B_{2}. By I.H. E[B_{1}]↓_{may}^{κ} ⇒ E[B_{2}]↓_{may}. Conclude by fact 4.2.

Or (ii) B′ = E′[A_{1}] and E[A_{2}] ↦ E′[A_{2}]. The result follows by I.H. and fact 4.2.

Or (iii) E[A_{2}] ↦ B′. Conclude by fact 4.2.

\underline{m = must:} The must case is more complicated. If we try to prove A_{1} < ∼_{must} A_{2} implies A_{1} < ≈_{must}^{λ} A_{2} by induction on λ, as in the may case, we run into a problem: When A_{2} ↦ B_{2} we are not guaranteed that A_{1} ↦^{+} B_{1} such that B_{1} < ∼_{must} B_{2}. We may only have that A_{1} < ∼_{must} B_{2} and then we cannot refer to the induction hypothesis to perform the induction step.

Therefore construct < ∼_{must} as the limit of an increasing sequence,

< ∼_{must} = ⋃_{μ<ω} < ∼_{must}^{μ}

where A_{1} < ∼_{must}^{μ} A_{2} ⇔ A_{1} < ∼_{must} A_{2} ∧ (A_{1} ⇓ ⇒ A_{2} ⇓^{μ}) .

Show ∀λ, μ<ω. < ∼_{must}^{μ} ⊆ < ≈_{must}^{λ} , by well-founded induction on (λ, μ), ordered lexicographically,

(λ_{1}, μ_{1}) ≺ (λ_{2}, μ_{2}) ⇔ λ_{1}<λ_{2} ∨ (λ_{1} =λ_{2} ∧ μ_{1}<μ_{2}) .

Let λ, μ<ω, assume ∀(κ, ν) ≺ (λ, μ). < ∼_{must}^{ν} ⊆ < ≈_{must}^{κ} , and show < ∼_{must}^{μ} ⊆ < ≈_{must}^{λ}: Assume A_{1} < ∼_{must}^{μ} A_{2}. If not A_{1} ⇓, neither E[A_{1}]↓_{must}, hence A_{1} < ≈_{must} A_{2}. Henceforth assume A_{1} ⇓. Since < ∼_{must} is a fixed point for ⟨ ⟩_{must}, A_{1} < ∼_{must}^{μ} A_{2} implies

(I) A_{2} ⇓^{μ}
∧ (II) A_{2}:terminated ⇒ A_{1} ↦^{∗} A_{2}
∧ (III) (∀B_{2} | A_{2} ↦ B_{2})(∃B_{1} | A_{1} ↦^{∗} B_{1}) B_{1} < ∼_{must} B_{2} .

If A_{2} is terminated, conclude by (II) and lemma evaluation (6.2). If A_{2} is not terminated, assume E[A_{1}]↓_{must}^{λ} and show E[A_{2}]↓_{must}. Clearly E[A_{2}] ≠ fail since A_{2} is not terminated. Show E[A_{2}] ↦ B′ implies B′ ↓_{must} by lemma choice of execution point: Either (i) B′ = E[B_{2}] where A_{2} ↦ B_{2} and, according to (III), A_{1} ↦^{∗} B_{1} such

that B_{1} < ∼_{must} B_{2}. Either A_{1} = B_{1} and E[B_{1}] ↓_{must}^{λ}, then use that (I) and A_{2} ↦ B_{2} imply B_{2} ⇓^{ν} for some ν<μ, thus B_{1} < ∼_{must}^{ν} B_{2}. Or else A_{1} ↦^{+} B_{1} and E[B_{1}] ↓_{must}^{κ}, for some κ<λ. In any case, we can apply I.H. to get

E[B_{2}]↓_{must} as required.

Or (ii) B′ = E′[A_{2}] and E[A_{1}] ↦ E′[A_{1}], hence E′[A_{1}] ↓_{must}^{κ}, for some κ<λ. Conclude by I.H.

Or (iii) E[A_{1}] ↦ B′. Conclude by fact 4.2.

7.4 Identity of all characterisations

So far we have shown, for m ∈ {may, must}, < ∼_{m} is included in < ≈_{m} (lemma 7.17) that coincide with ⊏ ∼_{m} (basic context lemma) which is included in ⇀ ∼_{m} (lemma 4.8). Now we will show that for closed basic actions all four pairs of preorders are identical. The missing link in the chain of mutual inclusions is:

Lemma 7.18 For closed actions A_{1}, A_{2},

A_{1} ⇀ ∼_{may} A_{2} implies  A_{1} < ∼_{may} A_{2} .
A_{1} ⇀ ∼_{must} A_{2} implies A_{1} < ∼_{must} A_{2} .

Proof: First show that ⇀ ∼_{may} is a may simulation, ⇀ ∼_{may} ⊆ ⟨ ⇀ ∼_{may} ⟩_{may}, i.e. A_{1} ⇀ ∼_{may} A_{2} implies A_{1} ⟨ ⇀ ∼_{may} ⟩_{may} A_{2}. The latter expands to

(I) A_{1}:success ⇒ A_{2} ↦^{∗} A_{1}
∧ (II) (∀B_{1} | A_{1} ↦ B_{1})(∃B_{2} | A_{2} ↦^{∗} B_{2}) B_{1} ⇀ ∼_{may} B_{2} .

(I) clearly follows from A_{1} ⇀ ∼_{may} A_{2}. Regarding (II), if A_{1} ↦ B_{1}, choose B_{2} = A_{2}; then B_{1} ⇀ ∼_{may} B_{2}: Every successful computation B_{1} ↦^{∗} S extends to a successful computation A_{1} ↦ B_{1} ↦^{∗} S. Since A_{1} ⇀ ∼_{may} A_{2}, there is also a computation A_{2} ↦^{∗} S, i.e. B_{2} ↦^{∗} S.

Correspondingly for must, assume A_{1} ⇀ ∼_{must} A_{2} and show

A_{1} ⇓ ⇒ (I) A_{2} ⇓ ∧ (II) A_{2}:terminated ⇒ A_{1} ↦^{∗} A_{2} ∧ (III) (∀B_{2} | A_{2} ↦ B_{2})(∃B_{1} | A_{1} ↦^{∗} B_{1}) B_{1} ⇀ ∼_{must} B_{2} .

The result is immediate if not A_{1} ⇓, so assume A_{1} ⇓ and hence also (I) since A_{1} ⇀ ∼_{must} A_{2}. The rest is as for the may case above: (II) clearly follows from A_{1} ⇀ ∼_{must} A_{2}. As for (III), when A_{2} ↦ B_{2}, let B_{1} = A_{1}, then B_{1} ⇀ ∼_{must} B_{2} because every successful computation from B_{2} extends to a successful computation from A_{2} and has a corresponding successful computation from A_{1} = B_{1}.

8 (In)equational action theory

This section shows how existing equational action theory respects contextual equivalence. Moreover, Section 8.2 sketches inequational theories for the preorders and demonstrate their expressive power. They enrich action theory by interesting characterisations of the behaviour of actions.

8.1 Equational theory

A number of the equational action laws from Section 2.4 were shown to respect experimental equivalence ‘≈’ in Section 6.1. So by the basic context lemma (6.10), these laws also respect contextual equivalence ‘≃’. We shall now use that simulation equivalence is also included in contextual equivalence (lemma 7.17) to prove the remaining laws from Section 2.4.

Eq.law (9) (A_{1} or A_{2}) or A_{3} ≃ A_{1} or (A_{2} or A_{3}) .

Proof: Every instance of the law is included in S = R ∪ R^{−1}, where

R = {((A_{1} or A_{2}) or A_{3}, A_{1} or (A_{2} or A_{3})) | A_{1}, A_{2}, A_{3}:closed-action} .

S is symmetric and by lemma 7.12 and corollary 7.14 it suffices to show S ⊆ ⟨S ∪ Id⟩_{impl}^{hybr} which is straightforward.

Laws (3), (6), and (11) can be proved analogously.

Half of laws (4) and (7) were shown in corollary 6.5. Of law (4) remains:

Eq.law (4)b A and then complete ≃ A .

Proof: Show that the symmetric relation S = R ∪ R^{−1}, where

R = {(A and then complete, A) | A:closed-action} ,

satisfies S ⊆ ⟨Id⟩_{impl} ∪ ⟨S⟩_{impl}^{hybr}.

R ⊆ ⟨S⟩_{impl}^{hybr} is easy to establish.

Consider R^{−1} next. A ⟨S⟩_{impl}^{hybr} (A and then complete) holds whenever there is a transition out of A. Otherwise show A ⟨Id⟩_{impl} (A and then complete) directly from fact 7.7:

Clearly A ⇓ and (A and then complete) ⇓ when there are no transitions out of A. Only if A is terminated can (A and then complete) perform a transition, (A and then complete) ↦ A, and then conclude since A ↦^{0} A.

The proof of law (7)b is similar.

Laws (10) and (12) require a fact about convergence of or:

Fact 8.1 A_{1} ⇓ ∧ A_{2} ⇓ iff (A_{1} or A_{2})⇓ , for all closed A_{1}, A_{2}.

This is proved by induction on ⇓ . The ‘if’ direction is an instance of a more general fact:

Fact 8.2 E[A]⇓ implies A⇓ , for all evaluation contexts E and closed A.

Eq.law (10) fail or A ≃ A or fail ≃ A .

Proof: Corollary 6.3 and the commutativity of or, eq.law (11), established most of the law. What remains to be shown is A ⊏ ∼_{impl} fail or A. Therefore, show R ⊆ ⟨R ∪ Id⟩_{impl} for R = {(A, fail or A) | A:closed-action}:

Since fail⇓, A⇓ implies (fail or A)⇓. If (fail or A) ↦ B, either B = (fail or A′) and A ↦ A′ and A′RB, or else B = A and conclude since A ↦^{0} A and A Id B.

Eq.law (12) A or A ≃ A .

Proof: Split the proof into (A or A) ⊏ ∼_{impl} A and A ⊏ ∼_{impl} (A or A) .

For the former, R = {(A or A, A) | A:closed-action} is easily shown to satisfy R ⊆ ⟨R⟩_{impl}^{hybr}.

For the latter, show R ⊆ ⟨R ∪ Id⟩_{impl} for R = {(A, A_{1} or A_{2}) | A↦^{∗} A_{1}∧A↦^{∗} A_{2}}, i.e. A ⟨R⟩_{must} (A_{1} or A_{2}) if A↦^{∗} A_{1} ∧ A↦^{∗} A_{2} :

A ⇓ implies A_{i} ⇓, by fact 4.2, which implies (A_{1} or A_{2}) ⇓, by fact 8.1. If (A_{1} or A_{2}) ↦ B, either:

• B = (A′_{1} or A_{2}) and A_{1} ↦A′_{1}, let A↦^{0} A, then ARB since A↦^{∗} A_{1} ↦A′_{1};

• symmetrically, B = (A_{1} or A′_{2}) and A_{2} ↦ A′_{2}; or

• B = A_{i}, let A ↦ A_{i}, then A_{i} Id B.

An interesting fact about law (12) is that it doesn’t respect bisimulation equivalence. E.g., terminate is not bisimilar to A = (terminate or terminate) because A↦^{5} succeed whereas terminate cannot evaluate to an action with the same processing capabilities.

All other equational action laws appear to be included in bisimulation equivalence (as conjectured by Mosses [22, C.4]).

8.2 Inequational theory

Many interesting inequational laws can be expressed in terms of the various semantic preorders.

• The equivalence classes and orderings depicted in Section 4.3 can be expressed as inequational laws.

• Lemma evaluation (6.2) gives an inequational characterisation of the evaluation of actions.

• The action combinators enjoy certain inequational algebraic properties.

• Induction rules characterise unfolding as the least fixed point combinator.

Such laws complement the existing action laws and further characterise the nondeterministic behaviour of actions.

Several of these laws were established in Section 7.2, e.g. fail is the may bottom element:

Ineq.law (i) fail ⊏ ∼_{may} A .

This was proved using the may experimental preorder in proposition 6.6 and using the may simulation preorder in proposition 7.8.

Since ⊏ ∼_{may} is a precongruence (by definition), in particular or is monotone in ⊏ ∼_{may} and the following law is a simple consequence:

Ineq.law (ii) A_{1}, A_{2} ⊏ ∼_{may} (A_{1} or A_{2}) .

Proof:

A_{1} ⊏ ∼_{may} (A_{1} or fail) , fail is unit for or, eq.law (10)
⊏ ∼_{may} (A_{1} or A_{2}) , using ineq.law (i) and or is monotone.

A_{2} ⊏ ∼_{may} (A_{1} or A_{2}) follows by commutativity of or, eq.law (11).

(This law was actually established in the proof of proposition 6.6.)

In conjunction with the idempotency of or we have that or is the may least upper bound operator, ‘⊔_{may}’: it is an upper bound by ineq.law (ii); it is the least such because A_{1}, A_{2} ⊏ ∼_{may} A implies

(A_{1} or A_{2}) ⊏ ∼_{may} (A or A_{2}) , by monotonicity of or
⊏ ∼_{may} (A or A) , by monotonicity of or
≃_{may} A  , by idempotency of or, eq.law (12).

Section 4.3 argues that the ⊕ operator is ⊔_{may}, thus ⊕ coincides with the or combinator may-wise. must-wise, only the inequality (A_{1} ⊕ A_{2}) ⊏ ∼_{must} (A_{1} or A_{2}) holds. The other direction fails because (complete ⊕ fail) ≄_{must} complete but complete ≃ (complete or fail) , by eq.law (10). (Thus the inequational theory of ⊕ and or is the same as that of ⊕ and + in [13].)

As another example of an inequational characterisation of action combinators, we can express an implementation relationship between and, and then:

Ineq.law (iii) A_{1} and A_{2} ⊏ ∼_{impl} A_{1} and then A_{2} .

Proof: R = {(A_{1} and A_{2}, A_{1} and then A_{2}) | A_{1}, A_{2}:closed-action} is easily seen to satisfy R ⊆ ⟨R ∪ Id⟩_{impl}^{hybr}.

Finally, we show an induction rule for the recursive combinator unfolding. It is a least fixed point combinator in both the may and must orderings as expressed by the following recursion induction rule (a.k.a. Park induction):

Rule 8.3 (Recursion induction) For all A, closed B, and m ∈ {may, must},

A@B ⊏ ∼_{m} B ⇒ unfolding A ⊏ ∼_{m} B .

Proof: Assume A@B ⊏ ∼_{m} B. Let U = unfolding A. Notice that U ↦ A@U is the only transition out of U. By lemma 5.1 unfolding A ⊏ ∼_{m} B is equivalent to ∀λ<ω. P (λ), where P (λ) ⇔ ∀ closed F. F [U] ≪_{m}^{λ} F [B], which we show by induction on λ. Let λ<ω, assume ∀κ<λ. P (κ) and show P (λ). I.e. assume F [U]↓_{m} λ and show F [B]↓_{m}. \underline{m = may:} If F [U]:success, then F [U] = F = F [B], hence F [B] ↓_{may}. Otherwise, F [U_{1}] ↦ B′, B′ ↓_{may}^{κ} for some κ<λ. By lemma 3.5:

Either (i) B′ = (E@U)[A@U], F = E@[ ]. Observe B′ = E[A]@U. By I.H. and fact 5.3, B′ ↓_{may}^{κ} implies E[A]@B ↓_{may}, i.e. (E@B)[A@B] ↓_{may}. By assumption A@B ⊏ ∼_{may} B, hence (E@B)[B] ↓_{may}. Conclude since (E@B)[B] =

F [B].

Or (ii) B′ = F′[U] and F [B] ↦ F′[B]. Since F′[U] ↓_{may}^{κ}, F′[B] ↓_{may} by I.H., hence F [B]↓_{may} by fact 4.2.

\underline{m = must:} By lemma 3.4:

Either (i) There exists an evaluation context E s.t. E@[ ] = F. Hence F [U] = (E@U)[U] ↦ (E@U)[A@U] = E[A]@U and E[A]@U ↓_{must}^{κ}, for some κ<λ. By I.H. and fact 5.3, E[A]@B ↓_{must}. E[A]@B = (E@B)[A@B] and by

assumption A@B ⊏ ∼_{must} B, hence (E@B)[B]↓_{must}, i.e. F [B]↓_{must}.

(This covered the case F = [ ]. Hence F [B] = fail only if F [B] = F [U] = F = fail in conflict with the assumption F [U]↓_{must}. What remains to be shown is F [B] ↦ B′ implies B′ ↓_{must}.)

Or (ii) whenever F [B] ↦ B′, there exists F′ s.t. B′ = F′[B] and F [U] ↦ F′[U]. F′[U]↓_{must}^{κ} for some κ<λ, hence by I.H. B′ ↓_{must}. Conclude F [B]↓_{must}.

Normally, see e.g. [13], recursion induction is derived from a stronger induction rule, either Scott induction or an ω-rule. These stronger induction principles do not hold in the presence of countably branching nondeterminism and will therefore not generalise to the functional facet of AN, whereas our direct proof of fixed point induction does carry over (in the must case by means of transfinite induction over all recursive ordinals, see Section 10).

9 Stuck actions

Hitherto we have assumed that closed actions are always well-behaved, that is, they never get stuck and all their closed subterms are well-behaved. In this section we discuss the problems concerned with accounting for stuck actions in our theory. Although ill-behaved actions are arguably of little interest, the problems of dealing with them shed light on the definitions and mutual consistency of the various semantic preorders as well as the definition of the evaluation relation.

Stuck theory

In AN, failure represents controlled error situations during execution, whereas if execution gets stuck it is a pathological error and can thus be viewed as uninteresting. Various syntactic requirements can be used to ensure well-behavedness.

Nonetheless, how would stuck actions fit into our theory as developed above? Clearly all closed stuck actions are indistinguishable and thus equivalent.

stuck= enact false is a representative of this equivalence class. stuck can be plotted into the diagrams of the closed basic orderings as follows:

[figure: succeed = terminate = chaos = ⊤_{may}; complete; escape; diverge = ⊥_{may} = fail = stuck; ⊤_{must} = stuck; complete; fail; escape; complete ; ⊕ fail; succeed; escape ; ⊕ fail; terminate; diverge = ⊥_{must} = chaos]

stuck is the bottom element in the may order—intuitively, stuck can never contribute ‘positively’ to produce a successful outcome and is thus equated with diverge and fail.

In the must order, stuck is the top element, perhaps surprisingly—notice that stuck ↓_{must} and stuck ⇓; examination of the proofs of proposition 4.7 and lemma 4.8 clarifies why stuck = ⊤_{must}.

All the four preorders, ⊏ ∼_{m} , < ≈_{m} , ⇀ ∼_{m} , and < ∼_{m}, still coincide when stuck is taken into account.

Stuck convergence

It doesn’t appear very satisfactory that stuck is the must top element. It seems more appropriate to identify stuck with the bottom element diverge—as in the may ordering. Can this be accomplished?

One reason why stuck is the top element of the four must preorders is that stuck ↓_{must} and stuck ⇓. The ↓_{must} and ⇓ predicates can be redefined such that this is not the case, e.g. modify them to become the least predicates ↓′_{must} and ⇓′ satisfying

A⇓′ ⇔ (A:terminated ∨ ∃B. A ↦ B) ∧ (∀B|A ↦ B)B ⇓′ .
A↓′_{must} ⇔ (A:success ∨ ∃B. A ↦ B) ∧ (∀B|A ↦ B)B ↓′_{must} .

The latter is more conveniently expressed as

A↓′_{must} ⇔ A↓_{may} ∧ (∀B|A ↦ B)B ↓′_{must} .

Replace ↓_{must} and ⇓ by ↓′_{must} and ⇓′ in the definitions of the four must preorders and write the resulting preorders as ⊏ ∼′_{must} , < ≈′_{must} , ⇀ ∼′_{must} , and < ∼′_{must} .

In the modified contextual and experimental preorders, ⊏ ∼′_{must} and < ≈′_{must} , stuck remains a maximal element above fail (think of the context C_{stuck} = [ ] and escape ) but it is no longer the top element. Pictorially, remove the lines from complete and escape to stuck in the above must diagram.

In the ‘simulation-style’ preorders, ⇀ ∼′_{must} , and < ∼′_{must} , stuck becomes the bottom element but the preorders are no longer precongruences (recall C_{stuck}).

C_{stuck} illustrates the problem that makes stuck maximal in ⊏ ∼′_{must} and < ≈′_{must} and makes ⇀ ∼′_{must} , and < ∼′_{must} non-congruent, namely the unfortunate interplay between nondeterminism in the operational semantics and stuck redexes:

Whenever there are more redexes to choose from, a non-stuck redex is chosen. The existence of a stuck redex therefore forces evaluation to choose any alternative redex. Hence stuck subterms may control the execution of a compound action without causing the compound action to get stuck. E.g., (stuck and escape) is indistinguishable from escape .

10 Generalisations to other facets

We have been dealing with four preorders: ⊏ ∼_{m} , < ≈_{m} , < ∼_{m}, and ⇀ ∼_{m} , for m ∈ {may, must}. And we have shown that they are all equivalent for closed basic actions,

⇀ ∼_{m} ⊇^{(1)} ⊏ ∼_{m} =^{(2)} < ≈_{m} ⊇^{(3)} < ∼_{m} ⊇^{(4)} ⇀ ∼_{m} ,

where facts (1), (2), (3), and (4) were established in lemma 4.8, basic context lemma 6.10, lemma 7.17, and lemma 7.18, respectively. Two proof techniques for establishing actions contextual preordered have come out of this:

• Show them experimental ordered by induction on the length of computation using lemma choice of execution point (3.6), conclude by the basic context lemma.

• Exhibit a simulation containing them, conclude by lemma 7.17.

How does all this machinery generalise to other facets of AN?

In general, ⊏ ∼_{m} , < ≈_{m} , and the basic context lemma are straightforward to generalise whereas the other ‘simulation-style’ preorders are more languagespecific.

The functional and declarative facets

When the functional or declarative facet is added, higher-order data flow is introduced.

This adds a complication to the proof of the basic context lemma. The proof technique from the proof of the ‘ciu’ theorem in [14] has to be applied.

⇀ ∼_{m} has to be defined co-inductively (in the style of Ong [28]’s bisimulation preorder for a nondeterministic λ-calculus). The co-inductive definition of < ∼_{m} must be generalised likewise.

All the techniques, results, and laws we have developed for basic actions generalise to these facets.

The functional facet also introduces unbounded, countable nondeterminism. This is easily accommodated in our theory. The only major change is that the inductive definitions of ↓_{must} and ≪_{must}^{λ} must be defined as transfinite limits,

↓_{must} = ⋃_{λ<Ω}↓_{must}^{λ} , ≪_{must} = ⋂_{λ<Ω} ≪_{must}^{λ} ,

where Ω is the least non-recursive ordinal, cf. [2]. All results and proofs in this report have also been carefully phrased so that they carry over. Simply replace all induction arguments in the must case by transfinite induction over all recursive ordinals.

The imperative and communicative facets

The imperative and communicative facets introduce actions with side-effects and interacting with their context.

We have extended the basic context lemma to the imperative facet along the lines of [14]. As for the basic facet, nondeterminism can be handled using a generalisation of lemma choice of execution point (the AN concept of ‘commitment’ [22] has to be incorporated). We still have not considered the communicative facet but we believe that [1] should be readily applicable.

The bisimulation for actions in [22, C.4] indicates how ⇀ ∼_{m} and < ∼_{m} can be generalised. Then lemma 7.18 will cease to hold. Ulidowski [34] explains how < ∼_{m} (his ‘copy+refusal testing’) refines our contextual testing but is weaker than bisimulation. Thus < ∼_{m} becomes strictly stronger than ⊏ ∼_{m} but is a tighter approximation than bisimulation.

All the action laws of Section 8 also hold for these facets. The evaluation lemmas 6.2 and 6.4 only address transitions that can be expressed locally, independent of context. Lemma evaluation (6.2) remains true—when suitably generalised—for transitions performed by ‘interacting’ imperative and communicative actions. Lemma determined evaluation (6.4) doesn’t; this lemma in effect states that, for observing contexts, execution in parallel with the transition being observed adds no discriminative power to observation. This is, in general, false for side-effects.

11 Conclusion

We conclude by recapitulating the technical exposition of this report and by relating our approach to other semantic approaches. Finally, we outline future work.

Overview

We have defined contextual test preorders for actions and developed useful operational proof techniques for establishing them.

Firstly, proofs by induction on the length of computation, based on an alternative characterisation of the preorders in terms of ‘experimental’ preorders. We have extended this proof technique, due to Mason and Talcott, to the nondeterminism in AN.

Secondly, simple simulation proofs. We use divergence sensitive simulations in order to match the contextual preorders. To escape the resulting complexity we employed a ‘hybrid’ simulation technique.

The standard range of test preorders and equivalences allowed us to exhibit an induction rule and inequational and equational laws that give rich characterisations of actions. In particular, we have shown that existing action laws hold for contextual equivalence.

Since basic actions are not very expressive, basic action theory is not very interesting in itself. But we believe that all the theory which we have presented for basic actions generalises to full AN. We have already developed this for the functional, declarative, and imperative facets—we have defined reduction semantics, proved generalisations of the (basic) context lemma (6.10), and proved existing action laws to hold for contextual equivalence. The experimental order proof technique used in the basic facet as well as the evaluation lemma evaluation (6.2) carry over to these other facets too. All the inequational and equational basic action laws in Section 8 remain true when other facets are added.

The simulation proof methods must be adjusted when imperative side-effects enter the picture and the simulation proof methods become incomplete.

Related work

Our operational techniques draw inspiration from a wide range of sources. Most of this literature is concerned with developing special theories for particular languages. Our aspiration is to obtain a useful, general action theory for reasoning about a large class of programming languages. The same objective is pursued by the domain theoretic meta language used in conventional denotational semantics and the associated reasoning techniques. The claim of action semantics is that actions have better pragmatic properties as a semantic meta language, in particular, for descriptions of realistic, complex programming languages. Motivated by these qualities of actions, our work investigates how actions can also provide a useful foundation for program reasoning.

Above we have reworked and strengthened the foundations of the existing action theory in [22] which addresses full AN, based on a nondeterministic structural operational semantics and bisimulation. Alternative semantic foundations for actions exist but none of these appear extensible to a comprehensive theory of full AN. In [7] a categorical semantics is defined for a typed subset of AN and a number of action laws are proven. For a similar subset of AN, Doh and Schmidt [6] define a versatile natural semantics framework for reasoning about (contextual) semantic equivalences (among many other things). Palsberg [30] and Moura [26] define natural semantics for larger AN subsets. Moura defines a ‘functional’ action equivalence but not a full action theory.

Future work

We plan to extend our work to full AN, as sketched in Section 10. Moreover, we are going to explore various applications of the theory. We have two sorts of applications in mind:

First of all, in order to compare action theory to conventional operational and denotational reasoning principles, we want to apply action theory to the pure, well-understood programming languages studied in traditional semantic literature.

Secondly, we would like to exploit the power of action semantics for describing large, complex languages in popular use. Hopefully, a strong action theory will provide means to apply rigourous semantic reasoning to such languages.

Acknowledgements I owe thanks to Peter Mosses for helpful suggestions that improved the presentation of this work, to Peter Ørbæk for discussions of problems encountered in the course of the work, and to Jaap van Oosten for explaining transfinite ordinals to me.

References

[1] G. Agha, I. A. Mason, S. F. Smith, and C. L. Talcott. A foundation for actor computation, Aug. 1994. To appear in Journal of Functional Programming.

[2] K. R. Apt and G. D. Plotkin. Countable nondeterminism and random assignment. J.ACM, 33(4):724–767, 1986.

[3] J. Buhl. Communicative action semantics. M.Sc. dissertation, Computer Science Department, Aarhus University, Nov. 1994.

[4] R. DeNicola and M. Hennessy. Testing equivalences for processes. Theoretical Comput. Sci., 34:83–133, 1984.

[5] K.-G. Doh and D. Schmidt. Action semantics-directed prototyping. Comput. Lang., 19(4):213–233, 1993.

[6] K.-G. Doh and D. Schmidt. The facets of action semantics: Some principles and applications. In Mosses [23], pages 1–15.

[7] S. Even and D. A. Schmidt. Category sorted algebra-based action semantics. Theoretical Comput. Sci., 77:73–96, 1990.

[8] M. Felleisen and D. P. Friedman. Control operators, the SECD-machine, and the λ-calculus. In M. Wirsing, editor, Formal Description of Programming Concepts III. IFIP, 1987.

[9] M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Comput. Sci., 103:235–271, 1992.

[10] A. D. Gordon. A tutorial on co-induction and functional programming. In Glasgow Workshop on Functional Programming, 1994.

[11] A. D. Gordon. Bisimulation as a theory of functional programming. In Proceedings of the 11th Conference of Mathematical Foundations of Programming Semantics, volume 1 of Electronic Notes in Computer Science. Elsevier, 1995.

[12] B. S. Hansen and J. U. Toft. The formal specification of ANDF, an application of action semantics. In Mosses [23], pages 34–42.

[13] M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.

[14] F. Honsell, I. A. Mason, S. F. Smith, and C. L. Talcott. A variable typed logic of effects, 1993. To appear in Information and Computation.

[15] D. J. Howe. Equality in lazy computation systems. In 4th Annual Symposium on logic in computer science. IEEE, 1989.

[16] S. B. Lassen. Design and semantics of action notation. In Mosses [23], pages 16–33.

[17] S. B. Lassen. Reasoning with actions. In U. H. Engberg, K. G. Larsen, and P. D. Mosses, editors, Proc. 6th Nordic Workshop on Programming Theory (Aarhus, 17–19 October, 1994), number NS-94-6 in BRICS Notes Series, pages 251–265, Dept. of Computer Science, Univ. of Aarhus, 1994.

[18] I. A. Mason, S. Smith, and C. L. Talcott. From Operational Semantics to Domain Theory, 1994. Submitted to Information and Computation.

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

[20] R. Milner. Operational and algebraic semantics of concurrent processes. In Handbook of Theoretical Computer Science. Elsevier, Amsterdam, 1990.

[21] P. D. Mosses. Abstract semantic algebras! In D. Bjørner, editor, Formal Description of Programming Concepts II. IFIP, 1983.

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

[23] P. D. Mosses, editor. Proceedings of the First International Workshop on Action Semantics (Edinburgh, Scotland, April 1994), number NS-94-1 in BRICS Notes Series. Dept. of Computer Science, Univ. of Aarhus, 1994.

[24] P. D. Mosses. Unified algebras and abstract syntax. In Recent Trends in Data Type Specification, volume 785 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

[25] P. D. Mosses and D. A. Watt. Pascal action semantics, Version 0.6 , Mar. 1993.

[26] H. Moura. Action Notation Transformations. Ph.D. thesis, University of Glasgow, 1993.

[27] H. Moura and D. Watt. Action transformations in the ACTRESS compiler generator. In CC’94, volume 786 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

[28] C.-H. L. Ong. Non-determinism in a functional setting. In 8th Annual Symposium on logic in computer science. IEEE, 1993.

[29] P. Ørbæk. OASIS: An optimizing action-based compiler generator. In P. Fritzon, editor, Proceedings of the 1994 Conference on Compiler Construction, Edinburgh, volume 786 of LNCS, pages 1–15. Springer-Verlag, April 1994.

[30] J. Palsberg. Provably Correct Compiler Generation. PhD thesis, Dept. of Computer Science, Univ. of Aarhus, 1992.

[31] D. Park. Concurrency and automata on infinite sequences. In Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science, pages 167–183. Springer-Verlag, 1981.

[32] L. C. Paulson. Co-induction and co-recursion in higher-order logic. Tech. report 304, University of Cambridge Computer Laboratory, 1994.

[33] G. D. Plotkin. LCF considered as a programming language. Theoretical Comput. Sci., 5:223–255, 1977.

[34] I. Ulidowski. Equivalences on observable processes. In Seventh Annual Symposium on Logic in Computer Science. IEEE, 1992.

[35] D. J. Walker. Bisimulation and divergence. Information and Computation, 85(2):202–241, 1990.

Index

[ ], 7 Id, 28 ≈, 20 < ≈_{impl}, 20 < ≈′_{must}, 40 < ≈_{m}, 20

<_{@}_{m}, 17

⇀ ∼′_{must}, 40 ⇀ ∼_{m}, 14 ≃, 12 ⊏ ∼_{impl}, 13 ⊏ ∼′_{must}, 40 ⊏ ∼_{m}, 12 ⊥_{m}, 13 < ∼_{impl}, 29 < ∼′_{must}, 40 < ∼_{m}, 28 ⇓, 9 ⇓′, 40 ≪_{m}, 11 ↓_{m}, 11 ↓′_{must}, 40 ↦, 8 ⊕, 14 ⟨ ⟩_{impl}^{hybr}, 31 ⟨ ⟩_{impl}, 29 ⟨ ⟩_{m}, 28 ⊓_{m}, 14 ⊔_{may}, 14 ⊤_{m}, 13 ∘, 16 @, 5 AN, 4 and, 5 and then, 5 AS, 1 ASD, 1

C, 9 C_{stuck}, 40 chaos, 14 check, 4 complete, 4

diverge, 13

E, 8 enact, 4 escape, 4

F, 10 fail, 4

m simulation, 28 may, 11 must, 11

or, 5

stuck, 39 succeed, 13

terminate, 13

trap, 5

unfold, 5 unfolding, 5

Recent Publications in the BRICS Report Series

RS-95-25 S�ren B. Lassen. Basic Action Theory. May 1995. 47 pp.

RS-95-24 Peter �rb�k. Can you Trust your Data? April 1995. 15 pp. Appears in Mosses, Nielsen, and Schwartzbach, editors, Theory and Practice of Software Development. 6th International Joint Conference CAAP/FASE, TAPSOFT ’95 Proceedings, LNCS 915, 1995, pages 575�590.

RS-95-23 Allan Cheng and Mogens Nielsen. Open Maps (at) Work. April 1995. 33 pp.

RS-95-22 Anna Ing� olfsd� ottir. A Semantic Theory for Value�Passing Processes, Late Approach, Part II: A Behavioural Semantics and Full Abstractness. April 1995. 33 pp.

RS-95-21 Jesper G. Henriksen, Ole J. L. Jensen, Michael E. J�rgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders B. Sandholm. MONA: Monadic Second-Order Logic in Practice. May 1995. 17 pp.

RS-95-20 Anders Kock. The Constructive Lift Monad. March 1995. 18 pp.

RS-95-19 Franc�ois Laroussinie and Kim G. Larsen. Compositional Model Checking of Real Time Systems. March 1995. 20 pp.

RS-95-18 Allan Cheng. Complexity Results for Model Checking. February 1995. 18pp.

RS-95-17 Jari Koistinen, Nils Klarlund, and Michael I. Schwartzbach. Design Architectures through Category Constraints. February 1995. 19 pp.

RS-95-16 Dany Breslauer and Ramesh Hariharan. Optimal Parallel Construction of Minimal Suf�x and Factor Automata. February 1995. 9 pp.

RS-95-15 Devdatt P. Dubhashi, Grammati E. Pantziou, Paul G. Spirakis, and Christos D. Zaroliagis. The Fourth Moment in Luby’s Distribution. February 1995. 10 pp. To appear in Theoretical Computer Science.

RS-95-14 Devdatt P. Dubhashi. Inclusion�Exclusion(3) Implies Inclusion�Exclusion(n). February 1995. 6 pp.