BRICS RS-97-24 S. B. Lassen: Relational Reasoning about Contexts BRICS

Basic Research in Computer Science

Relational Reasoning about Contexts

Søren B. Lassen BRICS Report Series RS-97-24 ISSN 0909-0878 September 1997 See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

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

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

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

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

This document in subdirectory RS/97/24/

Relational Reasoning about Contexts^{∗}

S. B. Lassen

BRICS^{†}, Department of Computer Science, University of Aarhus

1 Introduction

The syntactic nature of operational reasoning requires techniques to deal with term contexts, especially for reasoning about recursion. In this paper we study applicative bisimulation and a variant of Sands’ improvement theory for a small call-by-value functional language. We explore an indirect, relational approach for reasoning about contexts. It is inspired by Howe’s precise method for proving congruence of simulation orderings and by Pitts’ extension thereof for proving applicative bisimulation up to context. We illustrate this approach with proofs of the unwinding theorem and syntactic continuity and, more importantly, we establish analogues of Sangiorgi’s bisimulation up to context for applicative bisimulation and for improvement. Using these powerful bisimulation up to context techniques, we give concise operational proofs of recursion induction, the improvement theorem, and syntactic minimal invariance. Previous operational proofs of these results involve complex, explicit reasoning about contexts.

Related work

Applicative bisimulation (Abramsky 1990) is an operational theory for higherorder languages, inspired by bisimulation theories for concurrency (Park 1981; Milner 1989). It excels in reasoning about infinite data structures. These exist in every higher-order language but are particularly relevant in lazy functional languages (Gordon 1995; Pitts 1997) and functional object-oriented languages (Gordon and Rees 1996). But applicative bisimulation is not very helpful for reasoning about recursive control structures. There are more ‘intensional’ operational theories (Talcott 1997; Sands 1997b) which address recursion effectively by counting computation steps. But even they are of limited use for proving results such as the validity of the fundamental induction rules for recursion: recursion induction (also known as Park induction), syntactic continuity (ω induction), syntactic minimal invariance (syntactic projections), and the improvement theorem. Existing operational proofs are complex and involve explicit reasoning about term contexts.

Intuitively, a context is a term containing a hole, that may be filled by another term. This is an evocative idea, but for formal arguments contexts are difficult to work with, both technically and notationally. For this reason, Howe deals only indirectly with contexts in his influential congruence proof for applicative bisimilarity (Howe 1989; Howe 1996). Instead the proof is ‘relational’: a larger relation which is closed under contexts is constructed and is shown to coincide with applicative bisimilarity by bisimulation and induction on the evaluation relation. This relational approach yields a formally and notationally very precise proof. Moreover, Howe’s congruence proof applies to many different typed and untyped higher-order languages and operational orderings; see, e.g., Sands (1991, Ong (1992, Ferreira, Hennessy, and Jeffrey (1995, Lassen (1997, Gordon (1997).

∗To appear in Gordon and Pitts (1997).

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

Pitts (1995) extends Howe’s congruence proof for applicative bisimilarity to also establish an up to context rule for applicative bisimulation. The proof is also ‘relational’ and illustrates the versatility of Howe’s implicit, relational approach to reasoning about term contexts. Specifically it shows how to use this proof method to establish applicative bisimulation up to context results. (We present the proof in Section 5.2.) The results we present in this paper stem from the study of this work.

Sangiorgi’s bisimulation up to context is a powerful refined bisimulation proof rule for process calculi (Sangiorgi and Milner 1992; Sangiorgi 1994). Bisimulation up to context allows you to disregard a common term context when relating terms in bisimulation proofs. Unfortunately, his correctness proofs do not carry over to applicative bisimulation for higher-order languages. Gordon (1995) and Sands (1997b) present restricted applicative bisimulation up to context rules. They demonstrate the power of this approach to produce concise proofs of equivalences which are difficult to derive by other operational methods. Both Sangiorgi (1996, 1995) and Sands couple bisimulation up to context with efficiency preorders, called ‘expansion’ and ‘improvement’, respectively. As suggested by Pitts (1995), we also introduce an improvement preorder. The problem which we address in this fashion leads us to adopt an improvement theory based on a different cost measure than that of Sands (1997b).

Overview

Section 2 defines the syntax and operational semantics of the untyped, functional ML fragment which we study below. Section 3 introduces an algebra of relations on terms. This is essential for the calculations with relations in later sections. A substantial example is the proof of the unwinding theorem in Section 4. Applicative (bi)simulation is defined in Section 5. Preliminary applicative simulation up to context results are established and applicative bisimilarity is shown to be a congruence by Howe’s and Pitts’ techniques. A deficiency of applicative simulation up to context is discovered which leads us to introduce an improvement preorder in Section 6. Improvement enjoys a strong up to context rule from which congruence and the improvement theorem follow. Section 7 uses improvement to strengthen the applicative simulation up to context rule from Section 5. Finally, Section 8 concludes. An appendix contains proofs from Sections 6 and 7.

2 A functional ML fragment

We operate with a small call-by-value functional language with lists, an untyped fragment of ML (Milner, Tofte, and Harper 1990).

Syntax

Let f, g, x, y, z range over an infinite set of variables. The syntax of expressions is:

(Exp)  d, e ::= x | fn x => e | nil | e_{1} :: e_{2} | e_{1} e_{2}

                | letfun f x = d in e end | letval x = d in e end
                | (case d ofnil=> e_{1} | x_{1} :: x_{2} => e_{2} | f => e_{3}).

Expressions are identified up to α-renaming of bound variables.

In letval x = d in e end and fn x => e, x is bound in e.

In letfun f x = d in e end, f and x are bound in d, and f is bound in e.

In case d ofnil => e_{1} | x_{1} :: x_{2} => e_{2} | f => e_{3}, x_{1} and x_{2} are bound in e_{2}, and f is bound in e_{3}.

Terms are parsed as in ML. The scope of fn and case extends as far to the right as possible. Application associates to the left and has higher precedence than :: which associates to the right. For instance, the term fn x => x:: y :: x y z parses as fn x => (x:: (y :: ((x y) z))).

The set of values is given by the grammar:

(Val )  u, v, w ::= x | fn x => e | nil | v_{1} :: v_{2}.

Let e{v⃗/x⃗} = e{v^{1}/x_{1}, …, v^{n}/x_{n}} be the result of simultaneous, capture free substitution of values v⃗ = v_{1} … v_{n} for free occurrences of x⃗ = x_{1} … x_{n} in e. (See Stoughton (1988) for a precise definition of simultaneous substitution.) By x⃗ we always mean an ordered list of pairwise distinct variables. We write x ∈ x⃗ to mean variable x occurs in x⃗.

Let Expx⃗ and Val x⃗ be the set of expressions and values, respectively, with free variables contained in x⃗. Notice Val x⃗ ⊆ Expx⃗. We call expressions p, q ∈ Exp_{∅} closed.

A closed value is either the empty list nil, ‘cons’ of two closed values v_{1} :: v_{2}, or a function fn x => e with e ∈ Exp_{x}. The case construct has three corresponding branches. This allows both decomposition of lists and dynamic dispatch on the ‘type’ of values. (The latter would not be well-typed in ML but is common in untyped languages, e.g., Scheme (Clinger and Rees (editors) 1991) has a proc? predicate that tells whether a value is a closure; this feature is necessary for the formulation of syntactic minimal invariance in Proposition 11 but otherwise our results are unaffected by the exact choice of language constructs for accessing values—as long as application is the only means of ‘destructing’ functions.)

We take letval x = d in e end as a language primitive instead of encoding it as (fn x => e) d, because the encoding introduces a function application step. This difference affects the improvement theory of Section 6 and will be important later in the proof of Proposition 11.

We define Ω to be a divergent expression:

                Ω =^{def} letfun f x = f f in f f end.

We write rec f x => d for the recursive function,

          rec f x => d =^{def} fn x => letfun f x = d in d end.

For example, fn x => Ω = rec f x => f f.

A call-by-value fixed point combinator, Yv, can be expressed as:

Yv  =^{def} fn f => (fn g => fn x => f (g g) x) (fn g => fn x => f (g g) x).

So explicit recursion is redundant; later on we prove rec f x => e is semantically equivalent to Yv (fn f => fn x => e).

Evaluation semantics

We define the operational semantics of closed expressions by an evaluation relation ⇓ ⊆ Exp_{∅} × Val_{∅} between expressions and values. An important measure of ‘computational cost’ which we shall use extensively is the number of function applications (‘computation steps’) in evaluations. Therefore we introduce a family of evaluation relations indexed by this measure, ⇓_{N} ⊆ Exp_{∅} × Val_{∅} for N ≥ 0, inductively defined by the rules in Table 1.

‘Plain’ evaluation is just ⇓ =^{def} _{⋃N≥0} ⇓_{N}, i.e., p ⇓ v iff ∃N ≥ 0. p ⇓_{N} v. It is also given inductively by Table 1 with all N subscripts erased from the rules.

Note that v ⇓_{0} v for all v ∈ Val_{∅}. Moreover, evaluation is deterministic:

Proposition 1 (Determinacy) If p ⇓_{N} v and p ⇓_{N′} v′, N = N′ and v = v′.

Examples

1. Let I be the identity function, I =^{def} fn x => x, then

I p ⇓_{N+1} v iff p ⇓_{N} v,

for all p ∈ Exp_{∅}, v ∈ Val_{∅} and N ≥ 0. (Therefore we shall use applications of I as syntactic representations of function application steps in analogy with Sands’ ‘ticks’ (1997b).)

(Eval fn) fn x => e ⇓_{0} fn x => e

(Eval nil) nil ⇓_{0} nil

(Eval cons) \frac{e_{1} ⇓_{N_{1}} v_{1} e_{2} ⇓_{N_{2}} v_{2}}{e_{1} :: e_{2} ⇓_{N_{1}+N_{2}} v_{1} :: v_{2}}
(Eval apply) \frac{e_{1} ⇓_{N_{1}} fn x => e e_{2} ⇓_{N_{2}} v_{2} e\{v^{2}/x\} ⇓_{N_{3}} v}{e_{1} e_{2} ⇓_{N_{1}+N_{2}+N_{3}+1} v}

(Eval let fun) \frac{e\{(rec f x => d)/f\} ⇓_{N} v}{letfun f x = d in e end ⇓_{N} v}
(Eval let val) \frac{d ⇓_{N_{1}} u e\{u/x\} ⇓_{N_{2}} v}{letval x = d in e end ⇓_{N_{1}+N_{2}} v}

(Eval case) \frac{e_{0} ⇓_{N_{1}} v_{0} e ⇓_{N_{2}} v e = \{ \begin{matrix}e_{1} & if v_{0} = nil \\ e_{2}\{v^{1}/x_{1}, v^{2}/x_{2}\} & if v_{0} = v_{1} :: v_{2} \\ e_{3}\{v^{0}/f\} & if v_{0} = fn x => d \end{matrix}}{(\begin{matrix}case e_{0} of & nil=> e_{1} \\ | & x_{1} :: x_{2} => e_{2} \\ | & f => e_{3} \end{matrix}) ⇓_{N_{1}+N_{2}} v}

Table 1: Evaluation relation 2. The divergent expression Ω does not evaluate to anything. Any derivation

Ω ⇓_{N} v would have Ω ⇓_{N−1} v as premise, and this is impossible because of determinacy.

3. Let e^{∞} =^{def} (fn g => fn x => e(g g)x) (fn g => fn x => e(g g)x), so that Yv = fn f => f^{∞}. Then

Yv u ⇓_{2} fn x => u u^{∞} x because u^{∞} ⇓_{1} fn x => u u^{∞} x,

for u ∈ Val_{∅}.

Let an evaluation context, E, be a term with a hole, −, at redex position (Felleisen and Friedman 1987). They are given by the grammar:

(Ev. ctx.)  E ::= − | E :: e | e:: E | E e | e E

                 | letval x = E in e end
                 | (case E ofnil=> e_{1} | x_{1} :: x_{2} => e_{2} | f => e_{3}).

We write E[e] for the term obtained from E by filling in e for the hole −. (We adopt a liberal definition of redex position which does not suggest an evaluation order in ‘cons’ expressions, e_{1} :: e_{2}, and function applications, e_{1} e_{2}. One can indicate a left-to-right evaluation order by excluding evaluation contexts of the form e :: E and e E where e is not a value. But evaluation order is immaterial here as we do not consider small-step reductions of terms and our language has no side effects.)

Evaluation contexts satisfy

E[p] ⇓_{N} v iff ∃M, u. p ⇓_{M} u & E[u] ⇓_{N−M} v.  (2.1)

Combined with the examples above, we see that E[Ω] diverges and

E[I p] ⇓_{N+1} v iff I E[p] ⇓_{N+1} v iff E[p] ⇓_{N} v.  (2.2)

3 Relations

This section introduces our notation for relations and operations on them. Compatible refinement and context closure are of particular importance. Their precise definitions are key to the relational proofs in later sections. The relational algebra given here is quite general and language independent, except that only value substitutions are considered as our language is call-by-value.

Open and closed relations

A binary relation R is a set of pairs. We use infix notation, a R b, to mean (a, b) ∈ R.

Let Rel be the universal relation on closed expressions,

Rel = {(p, p′) | p, p′ ∈ Exp_{∅}}.

We call every R ⊆ Rel a closed relation. For instance, Id = {(p, p) | p ∈ Exp_{∅}} is the closed identity relation.

Moreover, we define

Rel^{∘} = {((x⃗)e, (x⃗)e′) | e, e′ ∈ Expx⃗},

where (x⃗)e is a ‘meta-abstraction’ of e ∈ Expx⃗; the (x⃗) prefix is a binder and x⃗ is subject to α-renaming. We call all R ⊆ Rel^{∘} open relations and write x⃗ ⊢ e R e′ whenever (x⃗)e R (x⃗)e′. By identifying every p ∈ Exp_{∅} with the 0-ary abstraction ()p, we have Rel ⊆ Rel^{∘} and closed relations are special cases of open ones.

We call Rel^{∘} the open extension of Rel. Generally, given any closed relation R, its open extension, R^{∘} ⊆ Rel^{∘}, is given by

\frac{∀v_{1}, …, v_{n} ∈ Val_{∅}. e\{v^{1} … v^{n}/x_{1} … x_{n}\} R e′\{v^{1} … v^{n}/x_{1} … x_{n}\}}{x_{1} … x_{n} ⊢ e R^{∘} e′}

For example, Id^{∘} is the open identity relation.

Both Rel and Rel^{∘} are closed under relation composition, which we write by juxtaposition, a R S b ⇔^{def} ∃c. a R c ∧ c S b. Open extension satisfies

R^{∘} S^{∘} ⊆ (R S)^{∘}.  (3.1)

Relation Substitution

For R, S ⊆ Rel^{∘}, the relation substitution of S into R, written R{S} ⊆ Rel^{∘}, relates expressions obtained by simultaneous substitution of S related values into R related expressions,

x⃗ ⊢ e R e′ y⃗ ⊢ v⃗ S v′
y⃗ ⊢ e{v⃗/x⃗} R{S} e′{^{v′}/x⃗}

where y⃗ ⊢ v⃗ S v′ is shorthand for y⃗ ⊢ v_{i} S v′_{i}, for all i = 1 … n, if v⃗ = v_{1} … v_{n} and v′ = v′_{1} … v′_{n}. Relation substitution is associative. Note that R{S} ⊆ Rel if S ⊆ Rel. As a drill in the notation let us show

R ⊆ S^{∘} iff R{Id} ⊆ S.  (3.2)

For the forward implication, suppose R ⊆ S^{∘} and e{v⃗/x⃗} R{Id} e′{v⃗/x⃗} because x⃗ ⊢ e R e′ and v_{1}, …, v_{n} ∈ Val_{∅}. Then x⃗ ⊢ e S^{∘} e′ and, by definition of open extension, e{v⃗/x⃗} S e′{v⃗/x⃗}. Conversely, if R{Id} ⊆ S and x⃗ ⊢ e R e′ then e{v⃗/x⃗} R{Id} e′{v⃗/x⃗} and e{v⃗/x⃗} S e′{v⃗/x⃗}, for all v_{1}, …, v_{n} ∈ Val_{∅}. From the definition of open extension we get x⃗ ⊢ e S^{∘} e′, as required.

(Comp x) x⃗xy⃗ ⊢ x R̂ x

(Comp fn) \frac{x⃗x ⊢ e R e′}{x⃗ ⊢ fn x => e R̂ fn x => e′}

(Comp nil) x⃗ ⊢ nil R̂ nil

(Comp cons) \frac{x⃗ ⊢ e_{1} R e′_{1} x⃗ ⊢ e_{2} R e′_{2}}{x⃗ ⊢ e_{1} :: e_{2} R̂ e′_{1} :: e′_{2}}

(Comp apply) \frac{x⃗ ⊢ e_{1} R e′_{1} x⃗ ⊢ e_{2} R e′_{2}}{x⃗ ⊢ e_{1} e_{2} R̂ e′_{1} e′_{2}}

(Comp let fun) x⃗fx ⊢ d R d′ x⃗f ⊢ e R e′

              x⃗ ⊢ letfun f x = d in e end R̂ letfun f x = d′ in e′ end

(Comp let val) x⃗ ⊢ d R d′ x⃗x ⊢ e R e′

               x⃗ ⊢ letval x = d in e end R̂ letval x = d′ in e′ end

(Comp case) x⃗ ⊢ d R d′ x⃗ ⊢ e_{1} R e′_{1} x⃗x_{1}x_{2} ⊢ e_{2} R e′_{2} x⃗f ⊢ e_{3} R e′_{3}

          x⃗ ⊢ (\begin{matrix}case d of & nil=> e_{1} \\ | & x_{1} :: x_{2} => e_{2} \\ | & f => e_{3} \end{matrix}) R̂ (\begin{matrix}case d′ of & nil=> e′_{1} \\ | & x_{1} :: x_{2} => e′_{2} \\ | & f => e′_{3} \end{matrix})

Table 2: Compatible refinement

For any open relation R, we say R satisfies weakening if

x⃗y⃗ ⊢ e R e′ ⇒ x⃗xy⃗ ⊢ e R e′, if x ∉ x⃗y⃗.

We call R substitutive if R{R} ⊆ R, and we say that R is closed under substitutions if R{Id^{∘}} ⊆ R. In the latter case R{Id} = R ∩ Rel. Every open extension, R^{∘}, satisfies weakening and is closed under substitutions. Any substitutive and reflexive open relation also satisfies weakening and closure under substitutions. Each of these properties is preserved by relation composition.

Compatible refinement

For every open relation R, its compatible refinement (Gordon 1994) R̂ ⊆ Rel^{∘} relates expressions with identical outermost syntactic constructor and immediate subterms pairwise related by R. Table 2 makes this definition precise for our language. Compatible refinement is monotone, preserves weakening, and commutes with relation composition, R̂ S = R̂ Ŝ.

An open relation R is compatible if R̂ ⊆ R. Every compatible relation is reflexive, as can be shown by structural induction on expressions.

Compatibility can also be expressed in terms of contexts. A context C is an expression with ‘holes’. If C has n holes, C[e_{1}, …, e_{n}] denotes the expression obtained by filling expressions e_{1} … e_{n} into the holes in C, possibly involving capture of free variables of e_{i} if the i’th hole occurs in the scope of binders in C, for i = 1, …, n. A relation R is compatible if whenever e_{i} and e′_{i} are related by R, for i = 1, …, n, so are C[e_{1}, …, e_{n}] and C[e′_{1}, …, e′_{n}], for all contexts C. But a precise formulation of this which accounts for free variables and variable capture becomes complicated. The formalisation above, R̂ ⊆ R, is easier to work with.

Throughout, we exploit compatible refinement as a tractable, indirect notation for contexts.

Lemma 1 Any compatible and transitive relation which is closed under substitutions is substitutive.

Proof Suppose R is compatible, transitive and closed under substitutions. If x⃗ ⊢ e R e′ and y⃗ ⊢ u⃗ R u′, then y⃗ ⊢ e{u⃗/x⃗} Id^{∘}{R} e{^{u′}/x⃗} and y⃗ ⊢ e{^{u′}/x⃗} R{Id^{∘}} e′{^{u′}/x⃗}. Since R is compatible, y⃗ ⊢ e{u⃗/x⃗} R e{^{u′}/x⃗} follows by easy structural induction on e; in general, Id^{∘}{R} ⊆ R for any compatible relation R. Moreover, y⃗ ⊢ e{^{u′}/x⃗} R e′{^{u′}/x⃗} since R is closed under substitutions. By transitivity we conclude y⃗ ⊢ e{u⃗/x⃗} R e′{^{u′}/x⃗}, as required. □

Context closure

For any relation R, its context closure, R^{C} ⊆ Rel^{∘}, relates expressions e, e′ with matching outermost context C,

e = C[d_{1}, …, d_{n}], e′ = C[d′_{1}, …, d′_{n}],

and subterms d_{i}, d′_{i} related by R. This can be defined inductively by means of compatible refinement,

(Ctx R) \frac{y⃗ ⊢ e R e′}{x⃗ ⊢ e R^{C} e′} if y⃗ ⊆ x⃗ (Ctx Comp) \frac{x⃗ ⊢ e R̂^{C} e′}{x⃗ ⊢ e R^{C} e′}

where y⃗ ⊆ x⃗ means that all variables in y⃗ occur in x⃗, in any order. The side condition y⃗ ⊆ x⃗ ensures that R^{C} satisfies weakening, even if R does not. Furthermore, context closure is monotone, idempotent (R^{C})^{C} = R^{C}, and R^{C} is compatible, by (Ctx Comp).

Lemma 2 If R is closed then R^{C} is substitutive.

Proof (Sketch) Whenever x⃗ ⊢ e R^{C} e′ and y⃗ ⊢ v⃗ R^{C} v′, we can prove y⃗ ⊢ e{v⃗/x⃗} R^{C} e′{^{v′}/x⃗} by induction on the derivation of x⃗ ⊢ e R^{C} e′.

Weakening is used as we enter the scope of binders. For example, if x⃗ ⊢ e R^{C} e′ is derived by (Ctx Comp) and (Comp fn), then e = fn z => d, e′ = fn z => d′, and x⃗z ⊢ d R^{C} d′. By weakening, y⃗z ⊢ v⃗ R^{C} v′ holds. Furthermore, y⃗z ⊢ z R^{C} z, by (Comp x) and (Ctx Comp). We calculate

x⃗z ⊢ d R^{C} d′ & y⃗z ⊢ v⃗z R^{C} v′z

⇒ y⃗z ⊢ d{v⃗z/x⃗z} R^{C} d′{^{v′}z/x⃗z}  by induction hypothesis

⇒ y⃗z ⊢ d{v⃗/x⃗} R^{C} d′{^{v′}/x⃗}

⇒ y⃗ ⊢ (fn z => d{v⃗/x⃗}) R̂^{C} (fn z => d′{^{v′}/x⃗}) by (Comp fn)
⇒ y⃗ ⊢ e{v⃗/x⃗} R^{C} e′{^{v′}/x⃗}  by (Ctx Comp).
□

Substitutive context closure, R^{SC}, is a substitutive extension of ordinary context closure, R^{C}. Each R^{SC} relates expressions e, e′ with matching outermost context C,

e = C[d_{1}{v⃗_{1}/x⃗}, …, d_{n}{v⃗_{n}/x⃗}], e′ = C[d′_{1}{^{v⃗_{1}′}/x⃗}, …, d′_{n}{^{v⃗_{n}′}/x⃗}],

subterms d′_{i}, d′_{i} related by R, and substitutions with values v⃗_{i}, v⃗_{i}′ inductively related by R^{SC}. It is important that R^{SC} has a succinct inductive definition,

(SC Subst) \frac{x⃗ ⊢ e R\{R^{SC}\} e′}{x⃗ ⊢ e R^{SC} e′}  (SC Comp) \frac{x⃗ ⊢ e R̂^{SC} e′}{x⃗ ⊢ e R^{SC} e′}

Clearly R^{C} ⊆ R^{SC} and if R is closed they coincide. The advantage of R^{SC} is that it is always substitutive. Substitutive context closure is monotone, idempotent, and R^{SC} is compatible, substitutive, and satisfies weakening. Compatibility is direct from (SC Comp). Weakening and substitutivity follow by induction on derivations. Since R^{SC} is compatible and substitutive, it is also reflexive and closed under substitutions.

Readers familiar with ‘meta-terms’ (Klop, van Oostrom, and van Raamsdonk 1993) will notice that substitutive context closure corresponds to closure under substitution of related meta-abstractions for meta-variables in meta-terms, whereas ordinary context closure is the closure under conventional variable capturing contexts. In fact, Pitts (1994b) advocates meta-terms, called ‘extended expressions’, as a generalised notion of contexts in place of conventional variable capturing contexts because the latter cannot be identified up to α-renaming of bound variables. However, our relational representation of contexts allows us to reason about conventional variable capturing contexts up to α-equivalence.

4 The unwinding theorem

As a first illustration of our relational approach to reasoning about contexts, we give a relational proof of the unwinding theorem. It says that a recursive function in a context converges if and only if one of its finite approximants does. The finite approximants of rec f x => d are given inductively by

rec^{(0)} f x => d =^{def} fn x => Ω,

  rec^{(n+1)} f x => d =^{def} fn x => letval f = (rec^{(n)} f x => d) in d end.

We say p converges iff ∃v. p ⇓ v.

Theorem 1 (Unwinding) For every recursive function rec f x => d and every context C, C[rec f x => d] converges if and only if there exists n ≥ 0 such that C[rec^{(n)} f x => d] converges.

Our proof below shows how the relational notation offers a tractable formulation of a complex syntactic argument. For instance, the proof is not complicated by the fact that we prove the theorem for arbitrary recursive functions, possibly with free variables.

First we construct a family of relations {R_{n}}_{n≥0} with each R_{n} given by

x⃗ ⊢ rec f x => d R_{n} rec^{(n)} f x => d,

  x⃗ ⊢ letfun f x = d in d end R_{n} letval f = (rec^{(n)} f x => d) in d end,

if d ∈ Exp_{x⃗fx}. For each n ≥ 0, we construct a relation U_{n} which satisfies

⊢ C[rec f x => d] U_{n} C[rec^{(n)} f x => d],  (4.1)

for arbitrary contexts C. In the course of the proof of the main lemma below, U_{n} must be preserved by evaluation in an appropriate sense. Therefore we cannot take U_{n} to be the context closure of R_{n}. We are going to strengthen the induction hypothesis by taking U_{n} to be the larger relation

U_{n} =^{def} ( ⋃_{m≥n} R_{m})^{SC} .

By this definition, U_{n} satisfies (4.1), it is substitutive, and U_{n} ⊆ U_{n′} whenever n′ ≤ n. These are key properties for the proof that are easier to formulate precisely in terms of relations rather than contexts. The inductive definition of substitutive context closure is also convenient for formal reasoning. By the construction of U_{n}, whenever x⃗ ⊢ e U_{n} e′, we can argue by cases on the derivation: either x⃗ ⊢ e R_{m}{U_{n}} e′ for some m ≥ n, by (SC Subst), and we can decompose e and e′ into expressions related by R_{m} and substitutions of values related by U_{n}; or x⃗ ⊢ e Û_{n} e′, by (SC Comp), and we may proceed by analysis of the derivation by the rules for compatible refinement in Table 2. For instance, we can deduce, for all values v and v′,

x⃗ ⊢ v U_{n+1} v′ implies x⃗ ⊢ v Û_{n} v′,  (4.2)

since U_{n+1} ⊆ U_{n} and x⃗ ⊢ rec f x => d R̂_{m} rec^{(m+1)} f x => d, for all m.

Lemma 3

(1) If ⊢ p U_{n+N} p′ and p ⇓_{N} v, also p′ ⇓_{N} v′ and ⊢ v U_{n} v′, for some v′.

(2) If ⊢ p U_{0} p′ and p′ ⇓_{N} v′, also p ⇓_{N} v and ⊢ v U_{0} v′, for some v.

Proof In outline, the proof argument for (1) is that any occurrence of rec in p is “unfolded” (evaluated recursively) at most N times in the evaluation p ⇓_{N} v and evaluates in “lock-step” with any rec^{(m+N)} in p′ (m ≥ n). In the end, each residual occurrence of rec in v is matched by some rec^{(m′)} in v′ (m′ ≥ n). The proof of (2) is similar; evaluation of rec^{(m)} in p′ is matched by evaluation of rec in p such that any residual occurrence rec^{(m′)} in v′ is matched by rec in v.

We spell out the proof of (1) in detail as illustration of the relational proof technique explored in this paper. By induction on the derivation of p ⇓_{N} v, we inductively construct a related derivation p′ ⇓_{N} v′. Consider the derivation of ⊢ p U_{n+N} p′. There are two cases:

(SC Subst) ⊢ p R_{m}{U_{n+N}} p′, for some m ≥ n + N, and p = r{u⃗/x⃗}, p′ = r_{m}{^{u′}/x⃗}, where x⃗ ⊢ r R_{m} r_{m} and ⊢ u⃗ U_{n+N} u′.

If r = rec f x => d, r_{m} = rec^{(m)} f x => d, then p, p′ are values, N = 0, v = p, p′ ⇓_{0} v′ = p′, and ⊢ v = p U_{n} p′ = v′.

If r = letfun f x = d in e end, r_{m} = letfun^{(m)} f x = d in e end, then

p ⇓_{N} v must be derived by rule (Eval let fun) from e{u⃗t/x⃗f} ⇓_{N} v, where t = (rec f x => d){u⃗/x⃗}. We let t′ = (rec^{(m)} f x => d){^{u′}/x⃗} and observe that ⊢ t U_{n+N} t′ and ⊢ e{u⃗t/x⃗f} U_{n+N} e{^{u′}t′/x⃗f}. By induction hypothesis e{^{u′}t′/x⃗f} ⇓_{N} v′ with ⊢ v U_{n} v′. And from the definition of r_{m} and by (Eval let val), also p′ ⇓_{N} v′.

(SC Comp) ⊢ p { \atop U_{n+N}} p′. We proceed by analysis of the derivation of p ⇓_{N} v.

Case (Eval apply) p = p_{1} p_{2}, p_{1} ⇓_{N_{1}} v_{1} = fn x => e, p_{2} ⇓_{N_{2}} v_{2}, e{v^{2}/x} ⇓_{N_{3}} v, and N = N_{1} + N_{2} + N_{3} + 1. By (Comp apply), p′ = p′_{1} p′_{2} with ⊢ p_{i} U_{n+N} p′_{i} and by the induction hypothesis p′_{i} ⇓_{N_{i}} v′_{i} with ⊢ v_{i} U_{n+N−N_{i}} v′_{i}. Notice that n + N − N_{i} > n + N_{3} + 1, for i = 1, 2. Therefore ⊢ v_{2} U_{n+N_{3}} v′_{2} and from (4.2) follows v′_{1} = fn x => e′ such that x ⊢ e U_{n+N_{3}} e′. So ⊢ e{v^{2}/x} U_{n+N_{3}} e′{v′_{2}/x}, by substitutivity, and e′{v′_{2}/x} ⇓_{N_{3}} v′ with ⊢ v U_{n} v′, by induction hypothesis. By (Eval apply), we conclude p′ ⇓_{N} v′. Case (Eval let fun) p = letfun f x = e_{1} in e_{2} end and e_{2}{(rec f x => e^{1})/f} ⇓_{N} v. We have p′ = letfun f x = e′_{1} in e′_{2} end, with fx ⊢ e_{1} U_{n+N} e′_{1} and f ⊢ e_{2} U_{n+N} e′_{2}. Then also

⊢ (rec f x => e_{1}) U_{n+N} (rec f x => e′_{1})

and

⊢ e_{2}{(rec f x => e^{1})/f} U_{n+N} e′_{2}{(rec f x => e′_{1})/f}

by compatibility and substitutivity of U_{n+N}. By the induction hypothesis e′_{2}{(rec f x => e′_{1})/f} ⇓_{N} v′ such that ⊢ v U_{n} v′. By (Eval let fun), we conclude p′ ⇓_{N} v′.

Case (Eval case) p = case p_{0} ofnil=> e_{1} | x_{1} :: x_{2} => e_{2} | f => e_{3},

p_{0} ⇓_{N_{1}} u, q ⇓_{N_{2}} v, N = N_{1} + N_{2}, where

q = \{ \begin{matrix}e_{1} & if u = nil \\ e_{2}\{u^{1}/x_{1}, u^{2}/x_{2}\} & if u = u_{1} :: u_{2} \\ e_{3}\{u/f\} & if u = fn x => e. \end{matrix}

By (Comp case), p′ = case p′_{0} ofnil => e′_{1} | x_{1} :: x_{2} => e′_{2} | f => e′_{3}, with ⊢ p_{0} U_{n+N} p′_{0}, ⊢ e_{1} U_{n+N} e′_{1}, x_{1}x_{2} ⊢ e_{2} U_{n+N} e′_{2}, f ⊢ e_{3} U_{n+N} e′_{3}. By induction hypothesis p′_{0} ⇓_{N_{1}} u′ such that ⊢ u U_{n+N_{2}} u′, since n + N = (n+N_{2})+N_{1}. By analysis of the derivation of ⊢ u U_{n+N_{2}} u′ we see that they have matching outermost constructor and, if this is not function abstraction, also ⊢ u { \atop U_{n+N_{2}}} u′. Accordingly, let

q′ = \{ \begin{matrix}e′_{1} & if u = nil = u′ \\ e′_{2}\{u′_{1}/x_{1}, u′_{2}/x_{2}\} & if u = u_{1} :: u_{2}, u′ = u′_{1} :: u′_{2} with ⊢ u_{i} U_{n+N_{2}} u′_{i} \\ e′_{3}\{u′/f\} & if u = fn x => e, u′ = fn x => e′. \end{matrix}

Since N_{2} ≤ N, U_{n+N} ⊆ U_{n+N_{2}} and, by substitutivity of U_{n+N_{2}}, ⊢ q U_{n+N_{2}} q′. By induction hypothesis q′ ⇓_{N_{2}} v′ with ⊢ v U_{n} v′ and we conclude p′ ⇓_{N} v′ by (Eval case).

The remaining cases are simpler. This completes the proof of (1).

The proof of (2) is very similar and proceeds by induction on the derivation of p′ ⇓_{N} v′. The (Eval apply) case exploits that the applied function cannot be rec^{(0)} f x => e as this would diverge. □

Proof of The Unwinding Theorem If C[rec f x => d] ⇓_{N} v, from (4.1) and Lemma 3(1) follows, for all n ≥ N, ∃v′. C[rec^{(n)} f x => d] ⇓_{N} v′. Conversely, if C[rec^{(n)} f x => d] ⇓_{N} v′, also ∃v. C[rec f x => d] ⇓_{N} v, by (4.1) and Lemma 3(2) because U_{n} ⊆ U_{0}. □

The backward direction of the proof can also be derived from the (computationally adequate) theory of applicative bisimulation below, instead of Lemma 3(2).

An important consequence of the unwinding theorem is a ‘syntactic continuity’ property of contextual equivalence (Pitts 1997). In Sections 5.4 and 6.3 we see how Lemma 3 entails syntactic continuity for applicative similarity and improvement. Syntactic continuity is a ‘domain-theoretic’ property that holds in all computationally adequate continuous models; see Pitts (1996a) and Braüner (1996).

There exist a number of operational proofs of these results, both for small-step reduction semantics (Mason, Smith, and Talcott 1996; Sands 1997a) and big-step evaluation semantics like ours (Pitts 1997). But note that our proof holds for open recursive terms r and that Lemma 3 gives very precise information about the operational relationship between r and its finite approximants. Our relational notation makes it feasible to express and reason about the details of contexts and substitutions. A characteristic of such relational proofs is that operational issues are dealt with in one sweeping induction on the derivation of evaluations and syntactic issues are dealt with in terms of the general algebra of relations. No auxiliary lemmas about evaluation and contexts are needed.

In the remainder of the paper we apply the relational technique used in the proof above to the study of operational preorders and equivalences.

5 Similarity

The primary operational relation we study is Abramsky’s applicative bisimulation (Abramsky 1990). It is the basis for a co-inductive generalisation of Milner’s context lemma (Milner 1977) to untyped functional languages. The basic idea is that higher-order functions are infinite data structures, built from the ‘lazy’ function abstraction data constructor, and are related co-inductively by applicative bisimulation in analogy with bisimulation of infinite behaviours in process calculi.

In this section we develop the theory of applicative (bi)simulation for our language, including preliminary simulation up to context results based on Howe’s and Pitts’ congruence proof techniques. This part is mainly a presentation of unpublished work by Pitts (1995) and serves as a basis for our further developments of this idea in Sections 6 and 7. Our aim is to develop techniques for reasoning about recursion. We shall see that simulation up to context is particularly useful for this purpose. In order to complete the discussion of proof rules for recursion we also prove a syntactic continuity property.

We consider an applicative bisimulation preorder, ≲ ⊆ Rel, which we call similarity. Expressions are similar if they evaluate to similar values.

p ≲ p′ iff ∀v. p ⇓ v ⇒ ∃v′. p′ ⇓ v′ & v ≲ v′.  (5.1)

Functions are similar if they are similar on all arguments; by definition of open extension this may be expressed as

fn x => e ≲ fn x => e′ iff x ⊢ e ≲^{∘} e′.  (5.2)

Following Howe (1996) we extend similarity to arbitrary values with matching outermost constructor and immediate subterms pairwise similar.

nil ≲ nil.  (5.3)
v_{1} :: v_{2} ≲ v′_{1} :: v′_{2} iff v_{1} ≲ v′_{1} and v_{2} ≲ v′_{2}.  (5.4)

We regard (5.2)–(5.4) as a definition of similarity on values by structural induction. We formalise this by means of a variant of compatible refinement on values, akin to Gordon’s ‘matching values’ (Gordon 1995). For every open relation R, let \overline{R} relate ‘matching’ values built from identical value constructors and with function

(Match x) x⃗xy⃗ ⊢ x \overline{R} x

(Match fn) \frac{x⃗x ⊢ e R e′}{x⃗ ⊢ fn x => e \overline{R} fn x => e′}

(Match nil) x⃗ ⊢ nil\overline{R} nil

(Match cons) \frac{x⃗ ⊢ v_{1} \overline{R} v′_{1} x⃗ ⊢ v_{2} \overline{R} v′_{2}}{x⃗ ⊢ v_{1} :: v_{2} \overline{R} v′_{1} :: v′_{2}}

Table 3: Matching values

bodies pairwise related by R. This is defined inductively by the rules in Table 3. Now (5.2)–(5.4) can be expressed by

v ≲ v′ iff ⊢ v \overline{≲^{∘}} v′.  (5.5)

We take the mutually recursive equations (5.1) and (5.5) as a co-inductive definition of similarity. To make this definition precise, we define a monotone simulation operator on relations, ⟨ ⟩, which maps any open relation R ⊆ Rel^{∘} to the closed relation ⟨R⟩ ⊆ Rel given by

p ⟨R⟩ p′ ⇔^{def} ∀v. p ⇓ v ⇒ ∃v′. p′ ⇓ v′ & ⊢ v \overline{R} v′.

We define similarity co-inductively as the greatest fixed point of ⟨ ^{∘}⟩,

≲ =^{def} νR.⟨R^{∘}⟩,  (5.6)

and bisimilarity, ∼, as the greatest symmetric fixed point, definable as

∼ =^{def} νR.⟨R^{∘}⟩ ∩ ⟨(R^{∘})^{op}⟩^{op},

where a S^{op} b ⇔^{def} b S a, for every relation S. Closed relations form a complete lattice, ordered by subset inclusion, and ⟨ ^{∘}⟩ and ⟨ ^{∘}⟩ ∩ ⟨( ^{∘})^{op}⟩^{op} are monotone operations with respect to this ordering. The Tarski-Knaster fixed point theorem asserts that their greatest fixed points exist and are also greatest post-fixed points.

Since evaluation is deterministic, ∼ is the largest symmetric relation contained in ≲,

∼ =^{def} ≲ ∩ ≲^{op} .

Therefore it suffices to focus attention on the more primitive relation ≲. In particular, we shall only formulate simulation proof rules for ≲ and omit the obvious analogues for ∼.

Equations (5.1)–(5.4) hold because ≲ is a fixed point, ≲ = ⟨≲^{∘}⟩. An immediate consequence of (5.1) is computational adequacy with respect to termination behaviour,

p ≁ Ω iff ∃v. p ⇓ v.  (5.7)

We shall call R ⊆ Rel a simulation if it is a post-fixed point of ⟨ ^{∘}⟩, that is, R ⊆ ⟨R^{∘}⟩. By the co-inductive definition (5.6), ≲ is the largest simulation, and we have the co-induction simulation rule:

\frac{R ⊆ ⟨R^{∘}⟩}{R ⊆ ≲}

Simulation is a powerful proof technique. To prove two expressions similar, we exhibit a simulation containing them. For example, ≲ is reflexive because the identity relation is a simulation, Id ⊆ ⟨Id^{∘}⟩, and ≲ is transitive because ≲ ≲ is a simulation, ≲ ≲ = ⟨≲^{∘}⟩⟨≲^{∘}⟩ ⊆ ⟨≲^{∘} ≲^{∘}⟩ ⊆ ⟨(≲ ≲)^{∘}⟩, where we use the fact that ⟨ ⟩ satisfies

⟨R⟩⟨S⟩ ⊆ ⟨R S⟩, for all R, S ⊆ Rel^{∘}.  (5.8)

Hence ≲ is a preorder and ∼ is an equivalence relation.

We call expressions p and p′ Kleene equivalent if they both diverge or both evaluate to the same value (because of determinacy, each expression can evaluate to at most one value). Kleene equivalence is easily seen to be a symmetric simulation and hence is included in ∼. An immediate consequence is soundness of evaluation with respect to bisimilarity,

p ⇓ v implies p ∼ v.  (5.9)

Many useful program laws are instances of Kleene equivalence. For instance, beta laws such as

(fn x => e) v ∼ e{v/x}.

            letfun f x = d in e end ∼ e{(rec f x => d)/f}.

These also hold for open expressions and ∼^{∘}, by definition of open extension. From the beta law for recursive function declarations follows a fixed point law for recursive functions,

rec f x => d ∼ fn x => d{(rec f x => d)/f},

by (5.2) and the definition of rec f x => d.

As an example of a co-inductive argument about recursive data, consider

u =^{def} rec f x => f, v =^{def} rec f x => fn y => f.  (5.10)

By definition of recursive functions, u = fn x => p and v = fn x => q, where

          p =^{def} letfun f x = f in f end,
          q =^{def} letfun f x = (fn y => f) in (fn y => f) end.

Observe that p ⇓ u and q ⇓ fn y => v. Both u and v perpetually return a function no matter how many arguments they are applied to. To see that they are bisimilar, we construct the relation R = {(p, q), (p, v)} satisfying u ⟨R^{∘}⟩ v and v ⟨(R^{∘})^{op}⟩ u. Both R and R^{op} are simulations, hence R ⊆ ∼, and u ∼ v follows by definition of ∼ because ⟨ ⟩ is monotone.

Similarity extends to open expressions by open extension, ≲^{∘}. A manipulation of fixed points and monotone operators yields ≲^{∘} = νR.⟨R⟩^{∘}. We call R an open simulation if R ⊆ ⟨R⟩^{∘}, in which case R ⊆ ≲^{∘}, by co-induction.

\frac{R ⊆ ⟨R⟩^{∘}}{R ⊆ ≲^{∘}}  (5.11)

By (3.2), R ⊆ ⟨R⟩^{∘} iff R{Id} ⊆ ⟨R⟩. If R is closed under substitutions then R{Id} = R ∩ Rel and R is an open simulation if R ∩ Rel ⊆ ⟨R⟩.

5.1 Simulation up to context

Often when one wants to prove that a relation R is contained in similarity, R ⊆ ≲, either R is not itself a simulation or it is not possible to show this directly. The solution is to extend R to a larger relation S which is a simulation and thus S ⊆ ≲ and R ⊆ ≲. In fact, this is the co-inductive dual of “strengthening the induction hypothesis” in induction arguments. The proofs of syntactic continuity and precongruence are examples of this. In both cases the constructed relations are tailored to the respective problems. However, often the process of ‘completing’ R follows a common pattern. We shall investigate refined simulation rules which implicitly extend R so as to become a simulation. Gordon (1995) presents a number of such refinements of bisimulation for a typed, call-by-name functional language. One of these is Milner’s bisimulation up to bisimilarity (Milner 1989). For ≲ this says:

Proposition 2 (Simulation up to ≲) \frac{R ⊆ ⟨≲^{∘} R^{∘} ≲^{∘}⟩}{R ⊆ ≲}

Proof If R ⊆ ⟨≲^{∘} R^{∘} ≲^{∘}⟩, then ≲ R ≲ is a simulation:

≲ R ≲ ⊆ ⟨≲^{∘}⟩ ⟨≲^{∘} R^{∘} ≲^{∘}⟩ ⟨≲^{∘}⟩ as ≲ is a fixed point for ⟨ ^{∘}⟩
⊆ ⟨≲^{∘} ≲^{∘} R^{∘} ≲^{∘} ≲^{∘}⟩  by (5.8)
⊆ ⟨≲^{∘} R^{∘} ≲^{∘}⟩  ≲^{∘} is transitive
⊆ ⟨(≲ R ≲)^{∘}⟩  (3.1).

Therefore ≲ R ≲ ⊆ ≲ and, since ≲ is reflexive, R ⊆ ≲. □

It is possible to derive an ‘equational’ simulation rule which does not involve the simulation operator, ⟨ ⟩, nor the evaluation relation.

Proposition 3 \frac{R ⊆ ≲ \overline{R^{∘}} ≲}{R ⊆ ≲}

Proof The inclusion ≲ \overline{R^{∘}} ≲ ⊆ ⟨≲^{∘} R^{∘} ≲^{∘}⟩ follows easily from the definitions of ≲ and ⟨ ⟩, and the rule is an immediate consequence of Proposition 2. □

Recall the example (5.10), where

            u = rec f x => f, v = rec f x => fn y => f.

An ‘equational’ proof of u ∼ v using Proposition 3 looks as follows. Let R = {(u, v), (u, fn y => v)}. By the fixed point law for rec we calculate

           u ∼ fn x => u \overline{R^{∘}} fn x => fn y => v ∼ v,

u ∼ fn x => u \overline{R^{∘}} fn y => v,

hence R ⊆ ≲ and R^{op} ⊆ ≲, by symmetrical applications of Proposition 3. Therefore R ⊆ ∼ and u ∼ v.

Proposition 3 is not a complete proof rule because it can only relate expressions p and p′ where p′ converges: if p ≲ \overline{R^{∘}} ≲ p′, there exist values v and v′ such that p ≲ v \overline{R^{∘}} v′ ≲ p′, and then p′ converges, by (5.1). This prevents us from relating two diverging expressions. We can repair this deficiency as in Gordon (1994), by throwing in the singleton relation {(Ω, Ω)},

\frac{R ⊆ ≲ (\overline{R^{∘}} ∪ \{(Ω, Ω)\}) ≲}{R ⊆ ≲}  (5.12)

Another refinement of bisimulation known from process calculi is Sangiorgi’s powerful bisimulation up to context (Sangiorgi 1994). Here and in ensuing sections we study variants of this proof principle for similarity and improvement.

As a first formulation of simulation up to context we have the following result for closed relations and context closure. The proof is adapted from Pitts (1995).

Proposition 4 (Simulation up to context) \frac{R ⊆ ⟨R^{C}⟩}{R ⊆ ≲}

Proof Assume R ⊆ ⟨R^{C}⟩. We shall prove

R^{C} ∩ Rel ⊆ ⟨R^{C}⟩.  (5.13)

Since R is closed, R^{C} is substitutive, by Lemma 2. As R^{C} is also reflexive, it is closed under substitutions. Therefore (5.13) implies that R^{C} is an open simulation, R^{C} ⊆ ⟨R^{C}⟩^{∘}, and then R^{C} ⊆ ≲^{∘}, by the open simulation rule (5.11). As R ⊆ R^{C}, the result follows.

By definition of ⟨ ⟩, (5.13) means that whenever ⊢ p R^{C} p′ and p ⇓ v, there exists v′ such that p′ ⇓ v′ and ⊢ v \overline{R^{C}} v′. The proof is by induction on the derivation of p ⇓ v.

(Ctx R) If ⊢ p R p′, then p ⟨R^{C}⟩ p′ is immediate from assumption R ⊆ ⟨R^{C}⟩.

(Ctx Comp) Otherwise ⊢ p R̂^{C} p′ and we proceed by analysis of the derivation of p ⇓ v. Each case is as in the proof of Lemma 3, except that we omit the arithmetic on N subscripts exercised there and we observe that the results are matching values. We show three representative cases:

Case (Eval cons) p = p_{1} :: p_{2}, p_{i} ⇓ v_{i}, and v = v_{1} :: v_{2}. Since ⊢ p R̂^{C} p′, we have p′ = p′_{1}:: p′_{2} with ⊢ p_{i} R^{C} p′_{i}. By induction hypothesis p′_{i} ⇓ v′_{i} such that ⊢ v_{i} \overline{R^{C}} v′_{i}, for i = 1, 2, so p′ ⇓ v′_{1} :: v′_{2} and ⊢ v_{1} :: v_{2} \overline{R^{C}} v′_{1} :: v′_{2}, by (Eval cons) and (Match cons).

Case (Eval apply) p = p_{1} p_{2}, p_{1} ⇓ v_{1} = fn x => e, p_{2} ⇓ v_{2}, and e{v^{2}/x} ⇓ v. Since ⊢ p R̂^{C} p′, also p′ = p′_{1} p′_{2} with ⊢ p_{i} R^{C} p′_{i}. By the induction hypothesis p′_{i} ⇓ v′_{i} with ⊢ v_{i} \overline{R^{C}} v′_{i}, for i = 1, 2. Then v′_{1} = fn x => e′ with x ⊢ e R^{C} e′ and, by compatibility, ⊢ v_{2} R^{C} v′_{2}. By substitutivity and induction hypothesis, ⊢ e\{v^{2}/x\} R^{C} e′\{v′_{2}/x\} and e′\{v′_{2}/x\} ⇓ v′ with ⊢ v \overline{R^{C}} v′. We conclude p′ ⇓ v′ by (Eval apply).

Case (Eval case) p = case p_{0} ofnil=> e_{1} | x_{1} :: x_{2} => e_{2} | f => e_{3}, p_{0} ⇓ u and q ⇓ v, where

q = \{ \begin{matrix}e_{1} & if u = nil \\ e_{2}\{u^{1}/x_{1}, u^{2}/x_{2}\} & if u = u_{1} :: u_{2} \\ e_{3}\{u/f\} & if u = fn x => d. \end{matrix}

By (Comp case), p′ = case p′_{0} ofnil => e′_{1} | x_{1} :: x_{2} => e′_{2} | f => e′_{3}, with ⊢ p_{0} R^{C} p′_{0}, ⊢ e_{1} R^{C} e′_{1}, x_{1}x_{2} ⊢ e_{2} R^{C} e′_{2}, f ⊢ e_{3} R^{C} e′_{3}. By induction hypothesis p′_{0} ⇓ u′ such that ⊢ u \overline{R^{C}} u′. By analysis of the derivation of the latter, we construct

q′ = \{ \begin{matrix}e′_{1} & if u = nil = u′ \\ e′_{2}\{u′_{1}/x_{1}, u′_{2}/x_{2}\} & if u = u_{1} :: u_{2}, u′ = u′_{1} :: u′_{2} with ⊢ u_{i} \overline{R^{C}} u′_{i} \\ e′_{3}\{u′/f\} & if u = fn x => d, u′ = fn x => d′, \end{matrix}

where ⊢ q R^{C}\{\overline{R^{C}}\} q′. By compatibility and substitutivity, \overline{R^{C}} ⊆ R^{C} and R^{C}\{\overline{R^{C}}\} ⊆ R^{C}. By induction hypothesis q′ ⇓ v′ with ⊢ v \overline{R^{C}} v′ and we conclude p′ ⇓ v′ by (Eval case).

We conclude (5.13), so R^{C} is an open simulation contained in ≲^{∘}. □

Proposition 4 is not a complete proof rule. For example, fn x => x and fn x => I x are bisimilar but they are not related by any closed relation R such that x ⊢ x R^{C} I x, because x and I x have no common context and R relates only closed expressions.

A more satisfactory and complete rule for simulation up to context would be

\frac{R ⊆ ⟨(R^{∘})^{C}⟩}{R ⊆ ≲}  (5.14)

Unfortunately, our attempts to prove (or refute) this have failed and we leave it as an open problem. A simple calculation, using (3.2), shows that (5.14) is equivalent to the ‘open’ rule:

\frac{R ⊆ ⟨R^{C}⟩^{∘}}{R ⊆ ≲^{∘}}

It differs from Proposition 4 in that R may be open so that R^{C} may capture free variables in expressions related by R. The premise is equivalent to R{Id} ⊆ ⟨R^{C}⟩, by (3.2). In Section 7 we prove a weaker version where we require that the premise holds not only for identical instantiations, R\{Id\}, but also for \overline{R^{C}} related instantiations, R\{\overline{R^{C}}\},

\frac{R\{\overline{R^{C}}\} ∩ Rel ⊆ ⟨R^{C}⟩}{R ⊆ ≲^{∘}}  (5.15)

If R is closed then R\{\overline{R^{C}}\} = R and (5.15) reduces to Proposition 4.

We have found neither simulation up to ≲ nor up to context to be particularly useful in themselves. It seems that their potential is only realised when combined. In connection with the precongruence proof for similarity below, we will show a stronger version of Proposition 4.

Proposition 5 (Simulation up to context and ≲) \frac{R ⊆ ⟨R^{C} ≲^{∘}⟩}{R ⊆ ≲}

This can be used to show that the Yv fixed point combinator enjoys a least pre-fixed point induction rule:

Proposition 6 fn x => e{v/f} ≲ v implies Yv (fn f => fn x => e) ≲ v.

Proof Let u =^{def} fn f => fn x => e, w =^{def} fn x => u u^{∞} x. Recall u^{∞} = (fn f => fn x => u(f f)x) (fn f => fn x => u(f f)x). We have Yv u ⇓_{2} w, u^{∞} ⇓_{1} w, and Yv u ∼ u^{∞}.

Now assume the premise holds. It suffices to show u^{∞} ≲ v. We proceed by simulation up to context and ≲. Let R =^{def} {(u^{∞}, v)}, then R ⊆ ⟨R^{C} ≲^{∘}⟩ holds because u^{∞} ⇓ w = fn x => u u^{∞} x and we have

⊢ fn x => u u^{∞} x \overline{R^{C}} fn x => u v x
\overline{∼^{∘}} fn x => e\{v/f\}
\overline{≲^{∘}} v,

by Kleene equivalence, assumption, and (5.5). Bisimulation up to context and ≲ yields R ⊆ ≲. Hence u^{∞} ≲ v and we conclude Yv u ≲ v, as required. □

For example, by the fixed point law for rec, we get

Yv (fn f => fn x => e) ≲ rec f x => e.  (5.16)

Proposition 5 is still too restrictive for many purposes. For instance, it is not clear how to prove the converse of (5.16) and the least pre-fixed point induction rule for rec. One might expect simulation up to ≲ and simulation up to context to combine as follows:

\frac{R ⊆ ⟨≲^{∘} R^{C} ≲^{∘}⟩}{R ⊆ ≲}  (5.17)

But this fails. As a counterexample (due to Andrew Gordon) take

R =^{def} {(fn x => nil, fn x => Ω)}.  (5.18)

Clearly x ⊢ nil ≴^{∘} Ω and fn x => nil ≴ fn x => Ω. But R ⊆ ⟨∼^{∘} R^{C} ∼^{∘}⟩ because

x ⊢ nil ∼^{∘} (fn x => nil) nil R^{C} (fn x => Ω) nil ∼^{∘} Ω.  (5.19)

This failure corresponds to the situation for process calculi, where a symmetric rule for weak bisimulation up to context and weak bisimulation also fails (Sangiorgi 1996). There the rule is repaired by introducing a more fine-grained efficiency preorder, called expansion. In Section 6 we develop a corresponding improvement relation for our language. Then we repair (5.17) by replacing the left occurrence of similarity in the premise with improvement (Proposition 10).

5.2 Precongruence

A precongruence is a compatible preorder, that is, a preorder which is preserved by all language constructs. Precongruence is an important property of similarity because it allows compositional (in)equational reasoning. Moreover, it shows that bisimilarity coincides with conventional contextual equivalence (an issue which we shall not address in this paper, however). We shall now prove that similarity is a precongruence by means of Howe’s general method for proving congruence of simulation orderings (Howe 1996). We employ an extension of the method, due to Pitts (1995), which also establishes the simulation up to context results of the previous section.

Recall that ≲^{∘} is a preorder. It is a precongruence if it is also compatible, ˆ≲^{∘} ⊆ ≲^{∘}. Howe proves this by simulation but since ˆ≲^{∘} is not itself a simulation he constructs a larger ‘candidate relation’ which is. Pitts parameterises the candidate relation by a closed relation R. For every R ⊆ Rel, the parameterised candidate relation, R^{♯}, is defined inductively by

(Cand R) \frac{p R p′ x⃗ ⊢ p′ ≲^{∘} e′′}{x⃗ ⊢ p R^{♯} e′′}  (Cand Comp) \frac{x⃗ ⊢ e R̂^{♯} e′ x⃗ ⊢ e′ ≲^{∘} e′′}{x⃗ ⊢ e R^{♯} e′′}

Each R^{♯} satisfies all the properties of Howe’s candidate relation:

Lemma 4 (1) R^{♯} is reflexive, compatible, and substitutive.

(2) R^{♯} contains similarity, ≲^{∘} ⊆ R^{♯}.

(3) R^{♯} contains its composition with similarity, R^{♯} ≲^{∘} ⊆ R^{♯}.

Proof Compatibility, R̂^{♯} ⊆ R^{♯}, is immediate from (Cand Comp) because ≲^{∘} is reflexive. Every compatible relation is reflexive, so R^{♯} and R̂^{♯} are reflexive. Again by (Cand Comp) follows (2). Since ≲^{∘} is transitive, (3) is also immediate from the definition of R^{♯}. Weakening,

x⃗y⃗ ⊢ e R^{♯} e′ ⇒ x⃗xy⃗ ⊢ e R^{♯} e′,

can be shown by induction on the derivation of x⃗y⃗ ⊢ e R^{♯} e′, using the fact that ≲^{∘} satisfies weakening, being an open extension. Finally, substitutivity,

x⃗ ⊢ e R^{♯} e′ & y⃗ ⊢ u⃗ R^{♯} u′ ⇒ y⃗ ⊢ e{u⃗/x⃗} R^{♯} e′{^{u′}/x⃗},

is proved by induction on the derivation of x⃗ ⊢ e R^{♯} e′, using (3), weakening, and the fact that ≲^{∘} is closed under substitutions. □

Lemma 5 \frac{R ⊆ ⟨R^{♯}⟩}{R^{♯} ⊆ ≲^{∘}}

Proof As in the proof of Proposition 4, it suffices to prove R^{♯} ∩ Rel ⊆ ⟨R^{♯}⟩, then R^{♯} will be an open simulation and R^{♯} ⊆ ≲^{∘}.

We assume ⊢ p R^{♯} p′′ and p ⇓ v, and we will prove that there exists v′′ such that p′′ ⇓ v′′ and ⊢ v \overline{R^{♯}} v′′. The proof is by induction on the derivation of p ⇓ v.

First consider the derivation of ⊢ p R^{♯} p′′. We see that there exists p′ such that p′ ≲ p′′ and either p R p′ or p R̂^{♯} p′. In either case we argue exactly as in the proof of Proposition 4 to get that p′ ⇓ v′, for some v′ such that ⊢ v \overline{R^{♯}} v′. Then, by definition of ≲, there exists v′′ such that p′′ ⇓ v′′ and ⊢ v′ \overline{≲^{∘}} v′′. Since \overline{R^{♯}} \overline{≲^{∘}} ⊆ \overline{R^{♯} ≲^{∘}} and R^{♯} ≲^{∘} ⊆ R^{♯}, ⊢ v \overline{R^{♯}} v′′ follows, as required. □

Howe’s candidate relation is just ∅^{♯}, for which the premise of the lemma holds trivially and thus establishes ∅^{♯} ⊆ ≲^{∘}. We have the reverse inclusion from above, so ≲^{∘} and ∅^{♯} coincide. Since ∅^{♯} is substitutive and compatible, so is ≲^{∘}. As ≲^{∘} is also a preorder, it is a precongruence.

Proposition 7 ≲^{∘} is substitutive and a precongruence.

Consequently, ∼^{∘} is also substitutive and is a congruence, that is, a compatible equivalence relation.

Lemma 5 also entails Proposition 4: since ≲^{∘} is reflexive we see that R^{C} ⊆ R^{♯}; therefore R ⊆ ⟨R^{C}⟩ implies R ⊆ ⟨R^{♯}⟩ and Lemma 5 gives R^{♯} ⊆ ≲^{∘} and thus R ⊆ ≲. Moreover, since R^{♯} ≲^{∘} ⊆ R^{♯}, also R^{C} ≲^{∘} ⊆ R^{♯}, so Lemma 5 entails Proposition 5 too.

5.3 Equational theory

Let us summarise our results about bisimilarity from above. We supplement some equational laws that follow directly from (5.1)–(5.4) by inspection of evaluations.

Extensionality

v ∼ v′ iff ⊢ v \overline{∼^{∘}} v′ iff ⊢ v ˆ∼^{∘} v′.
x⃗ ⊢ e ∼^{∘} e′ iff ∀u_{1}, …, u_{n} ∈ Val_{∅}. e{u⃗/x⃗} ∼ e′{u⃗/x⃗}.

The latter is just the definition of open extension.

Congruence and substitutivity

p ∼ p.
p ∼ p′ and p′ ∼ p′′ imply p ∼ p′′.
p ∼ p′ implies p′ ∼ p.
⊢ p ˆ∼^{∘} p′ implies p ∼ p′.
x ⊢ e ∼^{∘} e′ and v ∼ v′ imply e{v/x} ∼ e′{v′/x}.

Strachey’s property (Gordon 1994)

either p ∼ Ω or ∃v. p ∼ v.

Functions

(fn x => e) v ∼ e{v/x}.

Combined with the extensionality laws we get:

fn x => e ∼ fn x => e′ iff ∀v. (fn x => e) v ∼ (fn x => e′) v.

Let We have laws corresponding to those of Moggi’s computational lambda calculus (Moggi 1989), here presented as in Talcott (1997).

                  letval x = v in e end ∼ e{v/x}.
                 letval x = p in E[x] end ∼ E[p],

where E is any closed evaluation context.

Actually, these laws follow from the laws for case below because let can be encoded by means of case,

      (\begin{matrix}letval x = p \\ in e end \end{matrix}) ∼ (\begin{matrix}case p of & nil=> e\{nil/x\} \\ | & x_{1} :: x_{2} => e\{x^{1} :: x^{2}/x\} \\ | & f => e\{f/x\} \end{matrix}) .

Case

(\begin{matrix}case v of & nil=> e_{1} \\ | & x_{1} :: x_{2} => e_{2} \\ | & f => e_{3} \end{matrix}) ∼ \{ \begin{matrix}e_{1} & if v = nil \\ e_{2}\{v^{1}/x_{1}, v^{2}/x_{2}\} & if v = v_{1} :: v_{2} \\ e_{3}\{v/f\} & if v = fn x => e. \end{matrix}

(\begin{matrix}case p of & nil=> E[nil] \\ | & x_{1} :: x_{2} => E[x_{1} :: x_{2}] \\ | & f => E[f] \end{matrix}) ∼ E[p].

Fixed point rec is a fixed point operator:

rec f x => d ∼ fn x => d{(rec f x => d)/f}.

Furthermore, rec is rationally open (Braüner 1996):

C[rec f x => d] ∼ Ω iff ∀n ≥ 0. C[rec^{(n)} f x => d] ∼ Ω.

This rule is useful for equational reasoning about divergence, without direct reference to the evaluation relation. Rational openness and the unwinding theorem are easily derived from each other using adequacy (5.7). (Rational openness also follows from syntactic continuity and syntactic bottom below.)

5.4 Inequational theory

We also list some order-theoretic properties of similarity, taken from Pitts (1997), in order to complete our discussion about proof rules for recursion.

Extensionality, precongruence, and substitutivity As for ∼ above, except symmetry.

Syntactic bottom Ω is least with respect to ≲,

Ω ≲ p.

This is direct from (5.1).

Recursion induction rec f x => e is the least pre-fixed point of the functional fn x => e{−/f},

fn x => e{v/f} ≲ v implies rec f x => e ≲ v.

In Section 5.1 we proved this result for the Yv combinator, Proposition 6. The recursion induction rule for rec follows from syntactic continuity below; see Pitts (1997). In the following sections we shall discuss other proofs of recursion induction using improvement and simulation up to context.

Syntactic continuity Every recursive function is the least upper bound of its finite approximants and all language constructs are continuous with respect to this least upper bound,

C[rec f x => e] ≲ q iff ∀n ≥ 0. C[rec^{(n)} f x => e] ≲ q.

Proof We employ Lemma 3 from the proof of the unwinding theorem in Section 4 to give a co-inductive proof. A similar proof is outlined in Pitts (1997). Here we can use the relations from the formulation of Lemma 3 to construct the appropriate simulations. Note that we do not require that rec f x => e is closed.

First consider the backward implication (which is the most interesting). Recall the relations U_{n} from Lemma 3(1). We construct the relation

T =^{def} ⋂_{n≥0}(U_{n} ≲^{∘}).

Observe that ∀n ≥ 0. C[rec^{(n)} f x => e] ≲ q implies ⊢ C[rec f x => e] T q. We show that T is an open simulation, then T ⊆ ≲^{∘} and the result follows. So suppose ⊢ p T p′ and p ⇓_{N} v. By definition of T, for all n ≥ 0, ⊢ p U_{n+1+N} p_{n}, for some p_{n} ≲ p′. From Lemma 3(1) we get p_{n} ⇓_{N} v_{n} with ⊢ v U_{n+1} v_{n}. By the same argument as for (4.2) holds

⊢ u U_{n+1} u′ implies ⊢ u \overline{U_{n}} u′,  (5.20)

so we get ⊢ v \overline{U_{n}} v_{n}. Since p_{n} ≲ p′ also p′ ⇓ v′_{n} with ⊢ v_{n} \overline{≲^{∘}} v′_{n}, hence ⊢ v \overline{U_{n} ≲^{∘}} v′_{n}. Evaluation is deterministic so all v′_{n} are identical. Therefore ⊢ v \overline{U_{n} ≲^{∘}} v′_{0}, for all n ≥ 0, and we conclude ⊢ v \overline{T} v′_{0} and p ⟨T ⟩ p′, hence T is an open simulation as it is closed under substitutions.

The forward implication holds if C[rec^{(n)} f x => e] ≲ C[rec f x => e] for all n. This is derivable from syntactic bottom and precongruence, by induction on n. It also follows from Lemma 3(2). To see this we first extend (5.20) with

⊢ v U_{0}^{op} v′ implies ⊢ v \overline{U_{0}^{op} ∪ ≲^{∘}} v′.  (5.21)

This holds because ⊢ (rec^{(0)} f x => e) \overline{≲^{∘}} (rec f x => e), by syntactic bottom. Lemma 3(2) gives U_{0}^{op} ∩ Rel ⊆ ⟨U_{0}^{op} ∪ ≲^{∘}⟩ and we deduce U_{0}^{op} ∪ ≲^{∘} is an open simulation and U_{0}^{op} ⊆ ≲^{∘}. From (4.1) we get

C[rec^{(n)} f x => e] ≲ C[rec f x => e],

as required. □

Determinacy of evaluation plays a key role in the above proof of syntactic continuity. One can add nondeterminism to the language such that the operational semantics and theory of applicative bisimulation still satisfy the unwinding theorem, rational openness, and recursion induction, but syntactic continuity fails. Braüner (1996) uses this example to illustrate that syntactic continuity is a strictly stronger property than rational openness.

6 Improvement

Following Sands (1997b) we introduce a stricter operational ordering and equivalence that takes computational cost into account, in our case the number of function applications in evaluations. Improvement theory has independent interest as a formal approach to the study of program efficiency but Sands has also demonstrated that it is a powerful tool for reasoning about conventional operational equivalence and recursion. Here we are interested in the latter use of improvement.

We study the theory in some detail as its scope goes far beyond repairing the rule for simulation up to context and ≲ of the previous section. Our relational approach is instrumental in establishing a rule for improvement simulation up to variable capturing contexts. This is interesting in its own right, especially in the absence of a satisfactory counterpart for similarity, and it entails Sands’ improvement theorem.

As motivation for our definition of improvement below, recall that (5.19),

        x ⊢ nil ∼^{∘} (fn x => nil) nil R^{C} (fn x => Ω) nil ∼^{∘} Ω,

was used to prove R ⊆ ⟨≲^{∘} R^{C} ≲^{∘}⟩ and thus invalidated the symmetric up to context and ≲ rule (5.17),

\frac{R ⊆ ⟨≲^{∘} R^{C} ≲^{∘}⟩}{R ⊆ ≲}

Here nil is bisimilar to (fn x => nil) nil but the latter is more “expensive” as it takes one more function application step to compute. So nil is not “improved” by (fn x => nil) nil. This will be the requirement by which we shall repair (5.17) in Section 7.

We measure the number of function applications in evaluations, essentially because applications ‘destruct’ function abstractions. In fact, the counterexample to (5.17) can be constructed with any ‘lazy’ value constructor and associated destructors, but function abstraction and application happen to be the only lazy value constructor and destructor in ML. In general the cost measure must count every destruction of any lazy constructor. We should mention that this is tailored to support reasoning about applicative similarity and it is not meant as a contribution to the discussion of what constitutes a good measure of program effeciency for functional languages (Lawall and Mairson 1996).

We define an improvement preorder, ⊳ ∼, and a cost equivalence relation, {◁▷ \atop ∼}, co-inductively like similarity and bisimilarity but with the additional requirement that p ⊳ ∼ q implies that q evaluates in less function application steps than p. The definitions and the basic theory are quite analogous to those of Section 4.

Let the improvement simulation operator, ⟨ ⟩_{I}, be given by

p ⟨R⟩_{I} p′ ⇔^{def} ∀N.∀v. p ⇓_{N} v ⇒ ∃v′. p′ ⇓_{≤_{N}} v′ & ⊢ v \overline{R} v′,

for R ⊆ Rel^{∘}, p, p′ ∈ Exp_{∅}. Notation p′ ⇓_{≤_{N}} v′ means ∃N′ ≤ N. p′ ⇓_{N′} v′. The compound operator ⟨ ^{∘}⟩_{I} is monotone and we define improvement, ⊳ ∼, as the greatest fixed point

⊳ ∼ =^{def} νR.⟨R^{∘}⟩_{I},  (6.1)

Cost equivalence, {◁▷ \atop ∼}, is the greatest symmetric fixed point and is also the largest symmetric relation contained in improvement,

{◁▷ \atop ∼} = ⊳ ∼ ∩ ⊳ ∼^{op} .

Cost equivalence is computationally adequate, (5.7). But the evaluation relation is not sound, (5.9), with respect to cost equivalence; instead we have a more detailed correspondence between evaluation and cost equivalence:

p ⇓_{N} v implies p {◁▷ \atop ∼} I^{N}v.

Application of the identity function I is used as syntactic representation of function application steps. I^{N}v means N-fold application of I to v.

We call post-fixed points of ⟨ ^{∘}⟩_{I} improvement simulations and we have coinduction improvement simulation rules:

\frac{R ⊆ ⟨R^{∘}⟩_{I}}{R ⊆ ⊳ ∼}  \frac{R ⊆ ⟨R⟩_{I}^{∘}}{R ⊆ ⊳ ∼^{∘}}  (6.2)

We call R an improvement simulation if R ⊆ ⟨R^{∘}⟩_{I} and R is an open improvement simulation if R ⊆ ⟨R⟩_{I}^{∘}.

Improvement refines similarity, ⊳ ∼ ⊆ ≲, because

⟨R⟩_{I} ⊆ ⟨R⟩, for all R ⊆ Rel^{∘},  (6.3)

so every improvement simulation is also an (applicative) simulation.

6.1 Improvement simulation up to context

Refined simulation rules are equally important for improvement as they are for applicative simulation. It turns out that we are able to prove stronger refinements of improvement simulation than was the case for applicative simulation. In the process we will also derive that improvement is a precongruence.

Lemma 6 \frac{R ⊆ ⟨S^{+}⟩_{I}}{S^{+} ⊆ ⊳ ∼^{∘}}, where S =^{def} (R^{∘})^{C} and S^{+} is the transitive closure.

The proof is postponed to Appendix A.

Proposition 8 ⊳ ∼^{∘} is substitutive and a precongruence.

Proof As ⊳ ∼ itself satisfies the premise of the lemma, we get (⊳ ∼^{∘})^{C}^{+} ⊆ ⊳ ∼^{∘}. Therefore ⊳ ∼^{∘} is compatible and transitive, and hence a precongruence. Since ⊳ ∼^{∘} is closed under substitutions, it is also substitutive by Lemma 1. □

Another consequence of Lemma 6 is a full symmetric rule for improvement simulation up to context and improvement.

Proposition 9 (Improvement simulation up to context and ⊳ ∼)

\frac{R ⊆ ⟨⊳ ∼^{∘} (R^{∘})^{C} ⊳ ∼^{∘}⟩_{I}}{R ⊆ ⊳ ∼}

Proof From R ⊆ ⟨⊳ ∼^{∘} (R^{∘})^{C} ⊳ ∼^{∘}⟩_{I} we get that R∪⊳ ∼ ⊆ ⟨((R ∪ ⊳ ∼)^{∘})^{C}^{+}⟩_{I}. Hence ((R ∪ ⊳ ∼)^{∘})^{C}^{+} ⊆ ⊳ ∼^{∘} and R ⊆ ⊳ ∼. □

6.2 Equational theory

The equational theory of cost equivalence is analogous to that of bisimilarity, except for some applications of the identity function, I, to account for computational cost. Since these ‘syntactic computation steps’ can be erased up to bisimilarity, the cost equivalence theory here entails the corresponding theory of bisimilarity in Section 4.

The cost equivalence version of Strachey’s property accounts for the cost of computing a value:

either p {◁▷ \atop ∼} Ω or ∃!N.∃v. p {◁▷ \atop ∼} I^{N}v.

The beta law for function application records the computation step:

(fn x => e) v {◁▷ \atop ∼} I e\{v/x\}.

Notice that letval x = d in e end is one step ‘cheaper’ than the conventional encoding (fn x => e) d. This will be important in the proof of Proposition 11.

The remaining equational laws for bisimilarity in Section 5.3 carry over to cost equivalence unchanged.

The laws can be used to move around syntactic computation steps. For instance, the evaluation context law for case yields

      I (\begin{matrix}case p of & nil=> e_{1} \\ | & x_{1} :: x_{2} => e_{2} \\ | & f => e_{3} \end{matrix}) ∼ case p ofnil=> I e_{1} | x_{1} :: x_{2} => I e_{2} | f => I e_{3},

because (I−) is an evaluation context. A further law of this kind,

E[I p] {◁▷ \atop ∼} I E[p],

moves I across evaluation contexts; it is direct from (2.2). Such laws form a useful ‘tick algebra’ (Sands 1997b) for equational reasoning about computation steps.

Cost equivalence satisfies a unique fixed point rule:

fn x => e\{v/f\} {◁▷ \atop ∼} v implies rec f x => e {◁▷ \atop ∼} v.

This rule follows from recursion induction and co-induction rules below. For illustration, we can use it to prove the following correspondence between explicit recursion and the Yv fixed point combinator.

I^{2} (rec f x => I^{3} e) {◁▷ \atop ∼} Yv u, where u = (fn f => fn x => e),

by calculating Yv u {◁▷ \atop ∼} I^{2} fn x => u u^{∞} x and x ⊢ I^{3} e\{(fn x => u u^{∞} x)/f\} {◁▷ \atop ∼}^{∘} u u^{∞} x. As usual, a corresponding result for bisimilarity, rec f x => e ∼ Yv u, follows as a corollary. This and Proposition 6 constitute a proof of recursion induction for similarity.

6.3 Inequational theory

All the inequational theory for similarity in Section 5.4 also holds for improvement.

The proofs of syntactic bottom and syntactic continuity for improvement are again analogous to those for similarity above. The lemmas from the proof of the unwinding theorem in Section 4 were carefully phrased to also account for computational cost and the syntactic continuity proof for similarity is easily extended with this bookkeeping.

We supplement recursion induction,

fn x => e{v/f} ⊳ ∼ v implies rec f x => e ⊳ ∼ v,

with recursion co-induction,

v ⊳ ∼ fn x => e{v/f} implies v ⊳ ∼ rec f x => e,

which says that recursive functions are also greatest post-fixed points with respect to improvement. We can use improvement simulation up to context and ⊳ ∼ to prove the recursion (co-)induction rules.

Proof of recursion (co-)induction We only prove the first (induction) rule. The second (co-induction) rule follows by a symmetric argument because the improvement simulation up to context and ⊳ ∼ rule, Proposition 9, is symmetric.

Assume fn x => e\{v/f\} ⊳ ∼ v. By extensionality, ⊢ fn x => e\{v/f\} \overline{⊳ ∼^{∘}} v. Let R be the singleton relation, r R v, where r = rec f x => e. Then r is a fixed

point, r {◁▷ \atop ∼} fn x => e\{r/f\}, and ⊢ r \overline{{◁▷ \atop ∼}^{∘}} fn x => e\{r/f\}. Now r ⟨{◁▷ \atop ∼}^{∘} (R^{∘})^{C} ⊳ ∼^{∘}⟩_{I} v

because r ⇓_{0} r, v ⇓_{0} v, and

⊢ r \overline{{◁▷ \atop ∼}^{∘}} fn x => e\{r/f\} \overline{(R^{∘})^{C}} fn x => e\{v/f\} \overline{⊳ ∼^{∘}} v.

Hence R ⊆ ⟨{◁▷ \atop ∼}^{∘} (R^{∘})^{C} ⊳ ∼^{∘}⟩_{I}. By Proposition 9, we conclude R ⊆ ⊳ ∼, i.e., r ⊳ ∼ v. □

Recursion co-induction and the unique fixed point rule are call-by-value versions of Sands’ improvement theorem. This is apparent from the following reformulation, derived by means of equational laws for {◁▷ \atop ∼}.

      x ⊢ letfun f x = d_{0} in d_{0} end ⊳ ∼^{∘} letfun f x = d_{0} in d_{1} end
        ⇒ letfun f x = d_{0} in e end ⊳ ∼ letfun f x = d_{1} in e end,

for d_{0}, d_{1} ∈ Exp_{fx} and e ∈ Exp_{f}. The same holds for {◁▷ \atop ∼}.

It should be noted that a reason why our improvement theory satisfies the improvement theorem is that recursion is bound up with function abstraction in ML, that is, recursive unfoldings require a function application step (cf. the general version of the improvement theorem in Sands (1997a)). Hence our cost measure is actually more fine-grained than Sands’ count of unfoldings of recursion in Sands (1997b). In languages where recursion is not coupled with function abstraction, the two cost measures are incomparable and the two resulting improvement theories will be complementary.

7 Applicative simulation up to improvement

A motivation for introducing improvement is its use in refining applicative simulation. We can extend Proposition 5 as follows.

Proposition 10 (Applicative simulation up to ⊳ ∼ and context and ≲)

\frac{R ⊆ ⟨⊳ ∼^{∘} R^{C} ≲^{∘}⟩}{R ⊆ ≲}

This rule allows us to give a direct proof of recursion induction for similarity, analogous to the proof for improvement above: suppose fn x => e{v/f} ≲ v and let R = {(rec f x => e, v)}, then

rec f x => e {◁▷ \atop ∼} fn x => e\{(rec f x => e)/f\} \overline{R^{C}} fn x => e\{v/f\} ≲ v,

and we deduce R ⊆ ⟨{◁▷ \atop ∼}^{∘} R^{C} ≲^{∘}⟩; hence R ⊆ ≲, by Proposition 10, and rec f x => e ≲ v, as required.

In analogy with Proposition 9 we would like to have a stronger rule:

\frac{R ⊆ ⟨⊳ ∼^{∘} (R^{∘})^{C} ≲^{∘}⟩}{R ⊆ ≲}  (7.1)

But we do not know if this holds. It would entail (5.14) which we left as an open problem. In Appendix A we prove a weaker version:

Lemma 7 \frac{R\{\overline{R^{C}}\} ∩ Rel ⊆ ⟨⊳ ∼^{∘} R^{C} ≲^{∘}⟩}{R ⊆ ≲^{∘}}

It extends the open rule for simulation up to context (5.15) which we discussed in Section 5.1 as an approximation to (5.14).

When R is closed, Lemma 7 reduces to Proposition 10 above. But the utility of the lemma goes beyond that of Proposition 10 as we will now demonstrate by proving a syntactic minimal invariance property and by deriving equational rules for reasoning about open expressions.

7.1 Syntactic minimal invariance

As a non-trivial example, we consider a syntactic version of the domain-theoretic minimal invariance property for our language (Pitts 1994a).

Let π be the recursive function

          π =^{def} rec f x => case x ofnil=> nil | x_{1} :: x_{2} => f x_{1} :: f x_{2} | g => fn y => f(g(f y)).

(This would not be well-typed in ML where one would define a corresponding type-indexed family of functions instead.)

Minimal invariance says that π is the identity function, π ∼ I. We can prove this by means of Lemma 7.

Proposition 11 (Syntactic minimal invariance) π ∼ I.

Proof π ≲ I follows by recursion induction from

            x ⊢ case x ofnil=> nil | x_{1} :: x_{2} => I x_{1} :: I x_{2} | g => fn y => I(g(I y)) ∼^{∘} x,

which is easily verified by case analysis on the value of x.

We invoke Lemma 7 to prove I ≲ π. Let R ⊆ Rel^{∘} be given by

y ⊢ y R π y,

and S = ⊳ ∼^{∘} R^{C} ≲^{∘}. We prove R\{\overline{R^{C}}\} ∩ Rel ⊆ ⟨S⟩, i.e.,

⊢ v \overline{R^{C}} v′ implies π v′ ⇓ v′′ with ⊢ v \overline{S} v′′,

by induction on the derivation of ⊢ v \overline{R^{C}} v′.

(Match nil) v = nil, v′ = nil. Then π v′ ⇓ nil. Clearly ⊢ v \overline{S} nil.

(Match cons) v = v_{1} :: v_{2}, v′ = v′_{1} :: v′_{2}, and ⊢ v_{i} \overline{R^{C}} v′_{i}. By induction hypothesis π v′_{i} ⇓ v′′_{i} with ⊢ v_{i} \overline{S} v′′_{i}. So π v′ ⇓ v′′ = v′′_{1} :: v′′_{2} and ⊢ v \overline{S} v′′.

(Match fn) v = fn y => e, v′ = fn y => e′, and y ⊢ e R^{C} e′. Then π v′ ⇓ v′′ = fn y => π(v′(π y)) and ⊢ v \overline{S} v′′ because

         y ⊢ e {◁▷ \atop ∼}^{∘} letval y = y inletval y = e in y endend
               R^{C} letval y = π y inletval y = e′ in π y endend

∼^{∘} π(v′(π y)),

and {◁▷ \atop ∼}^{∘} R^{C} ∼^{∘} ⊆ S.

We conclude R ⊆ ≲^{∘} by Lemma 7. Therefore v ≲ π v, for all closed values v, and I ≲ π holds by extensionality. □

Simulation up to ⊳ ∼ and context and ≲, Lemma 7, substantially simplifies the proof. Mason, Smith, and Talcott (1996) give a direct operational proof of this result. It is also possible to recast their proof in the relational proof style used throughout this paper.

The finite approximants of π (as defined in Section 4) are ‘syntactic projections’. Syntactic minimal invariance and syntactic continuity entail that their least upper bound is the identity function and thus:

p ≲ q iff ∀n ≥ 0. π_{n} p ≲ q,  (7.2)

where π_{n} is the n’th finite approximant of the recursive function π.

In Milner’s construction of the fully abstract continuous model of PCF (Milner 1977) and in the operational model constructions for a call-by-value language like ours in Mason, Smith, and Talcott (1996), syntactic projections are used to address domain-theoretic notions of finite elements and ω-algebraicity syntactically.

Viewed as a proof rule, (7.2) is a sort of generalised Take Lemma (Bird and Wadler 1987) or higher-order structural induction principle; see Smith (1997). Pitts (1996b, 1994a) has also developed this idea and its domain-theoretic background and he has studied various applications.

7.2 Equational rules

From Lemma 7 we can derive an ‘equational’ version akin to Proposition 3.

Proposition 12 \frac{R ⊆ ⊳ ∼^{∘} \overline{R^{C}} ≲^{∘}}{R ⊆ ≲^{∘}}

Proof If R ⊆ ⊳ ∼^{∘} \overline{R^{C}} ≲^{∘} then

R\{\overline{R^{C}}\} ⊆ (⊳ ∼^{∘} \overline{R^{C}} ≲^{∘})\{\overline{R^{C}}\}
⊆ (⊳ ∼^{∘}\{\overline{Id^{∘}}\})(\overline{R^{C}}\{\overline{R^{C}}\})(≲^{∘}\{\overline{Id^{∘}}\})
⊆ ⊳ ∼^{∘} (\overline{R^{C}}\{\overline{R^{C}}\}) ≲^{∘},  (7.3)

because ⊳ ∼^{∘} and ≲^{∘} are closed under substitutions.

Moreover, we can show \overline{R^{C}}\{\overline{R^{C}}\} ⊆ {◁▷ \atop ∼}^{∘} \overline{R^{C}} {◁▷ \atop ∼}^{∘}, i.e.,

x⃗ ⊢ u \overline{R^{C}} u′ and y⃗ ⊢ v⃗ \overline{R^{C}} v′ imply y⃗ ⊢ u\{v⃗/x⃗\} {◁▷ \atop ∼}^{∘} \overline{R^{C}} {◁▷ \atop ∼}^{∘} u′\{^{v′}/x⃗\},

by induction on the derivation of x⃗ ⊢ u \overline{R^{C}} u′. In the (Match fn) case the substitutions of u and u′ into the function bodies can be replaced by let bindings up to cost equivalence.

Therefore ⊳ ∼^{∘} (\overline{R^{C}}\{\overline{R^{C}}\}) ≲^{∘} ⊆ ⊳ ∼^{∘} \overline{R^{C}} ≲^{∘} and

R\{\overline{R^{C}}\} ∩ Rel ⊆ ⊳ ∼ \overline{R^{C}} ≲  from (7.3)
⊆ ⊳ ∼ ⟨R^{C}⟩ ≲  by definition of ⟨ ⟩
⊆ ⟨⊳ ∼^{∘}⟩⟨R^{C}⟩⟨≲^{∘}⟩ ⊳ ∼ and ≲ are simulations
⊆ ⟨⊳ ∼^{∘} R^{C} ≲^{∘}⟩  by (5.8),

and we conclude R ⊆ ⊳ ∼^{∘}, by Lemma 7. □

Proposition 12 is a useful proof rule in itself—for instance, the proof of recursion induction using Proposition 10 above is more directly an instance of the equational proof rule of Proposition 12. Furthermore, from it we can derive a version of a proof rule by Sands (1997b), called ‘bisimulation up to context and improvement’: let relation ⊳ ⊆ Rel be given by

p ⊳ q iff p ⊳ ∼ I q.
Proposition 13 \frac{R ⊆ ⊳^{∘} R^{C} ≲^{∘}}{R ⊆ ≲^{∘}}

Proof Suppose R ⊆ ⊳^{∘} R^{C} ≲^{∘}. We construct S ⊆ Rel^{∘} by

x⃗ ⊢ (fn z => e) S (fn z => e′),

whenever z ∉ x⃗ and there exist d and d′ such that

x⃗ ⊢ d R d′ and x⃗ ⊢ d ⊳^{∘} e R^{C} e′ ≲^{∘} d′.

Observe that

x⃗ ⊢ d ⊳ ∼^{∘} (fn z => e) nil and x⃗ ⊢ (fn z => e′) nil ≲^{∘} d′.

Therefore R ⊆ ⊳ ∼^{∘} S^{C} ≲^{∘}. We have S ⊆ ⊳ ∼^{∘} \overline{S^{C}} ≲^{∘} because

x⃗ ⊢ (fn z => e) \overline{R^{C}} (fn z => e′),

and

\overline{R^{C}} ⊆ \overline{(⊳ ∼^{∘} S^{C} ≲^{∘})^{C}} ⊆ \overline{(⊳ ∼^{∘})^{C}} \overline{(S^{C})^{C}} \overline{(≲^{∘})^{C}} ⊆ ⊳ ∼^{∘} \overline{S^{C}} ≲^{∘}.

Hence S ⊆ ≲^{∘}, by Proposition 12, and R ⊆ ⊳ ∼^{∘} S^{C} ≲^{∘} implies R ⊆ ≲^{∘}, because ≲^{∘} is a precongruence and contains ⊳ ∼^{∘}. □

Sands (1997b) has demonstrated how (versions of) this rule allows simple calculational proofs of many functional program equivalences from the literature. It is particularly useful for call-by-value languages with inductively defined data types for which conventional applicative simulation is of little use.

For illustration, we solve Exercise 10.20 from Winskel (1993). Let

f =^{def} rec f x => fn y => case x ofnil=> y | x_{1} :: x_{2} => f(append(rx_{1}y)x_{2})(sx_{1}y) | h => Ω,

g =^{def} rec g x => fn y => case x ofnil=> y | x_{1} :: x_{2} => gx_{2}(g(rx_{1}y)(sx_{1}y)) | h => Ω,

where r, s ∈ Val_{∅} (presumably they are functions but we need not require that) and append is the list concatenation function,

    append  =^{def} rec a x => fn y => case x ofnil=> y | x_{1} :: x_{2} => x_{1} :: a x_{2} y | g => Ω.

We will now prove that f and g are bisimilar by means of Sands’ proof rule. As a first attempt, let relation R be given by

x⃗ ⊢ (f u_{0} v) R (g u_{0} v),

whenever u_{0}, v ∈ Val x⃗. By extensionality, f ∼ g if R ⊆ ∼^{∘}.

By means of the equational laws for cost equivalence, we calculate

     x⃗ ⊢ f u_{0} v {◁▷ \atop ∼}^{∘} I^{2} case u_{0} ofnil=> v | x_{1} :: x_{2} => letval x = r x_{1} v inletval y = s x_{1} v in f(append x x_{2}) y end end | h => Ω,

     x⃗ ⊢ g u_{0} v {◁▷ \atop ∼}^{∘} I^{2} case u_{0} ofnil=> v | x_{1} :: x_{2} => letval x = r x_{1} v inletval y = s x_{1} v in g x_{2}(g x y) end end | h => Ω.

The resulting expressions are identical except for the subterms f(append x x_{2}) y and g x_{2}(g x y). We need to extend R to also relate these. Let @(u_{n},..., u_{0}) abbreviate append u_{n}(append u_{n−1}(...(append u_{1} u_{0})...)). Now, let R be given by

x⃗ ⊢ (f @(u_{n},..., u_{0}) v) R (g u_{0}(...(g u_{n} v)...)),

for all n ≥ 0 and u_{0},..., u_{n}, v ∈ Val x⃗. From the calculations above we see that

x⃗ ⊢ (f @(u_{0}) v) = (f u_{0} v) ⊳^{∘} R^{C} ∼^{∘} (g u_{0} v),

because x⃗x_{1}x_{2}xy ⊢ (f(append x x_{2}) y) = (f @(x, x_{2}) y) R (g x_{2}(g x y)). If n ≥ 1 we calculate

x⃗ ⊢ f @(u_{n}, u_{n−1},..., u_{0}) v

{◁▷ \atop ∼}^{∘} I^{2} case u_{n} ofnil=> f @(u_{n−1},..., u_{0}) v | x_{1} :: x_{2} => letval x = r x_{1} v inletval y = s x_{1} v inI^{2} f @(x, x_{2}, u_{n−1},..., u_{0}) y end end | h => Ω,

⊳ ∼^{∘} I^{2} case u_{n} ofnil=> f @(u_{n−1},..., u_{0}) v | x_{1} :: x_{2} => letval x = r x_{1} v inletval y = s x_{1} v in f @(x, x_{2}, u_{n−1},..., u_{0}) y end end | h => Ω,

x⃗ ⊢ g u_{0}(...(g u_{n−1}(g u_{n} v))...)

{◁▷ \atop ∼}^{∘} I^{2} case u_{0} ofnil=> g u_{0}(...(g u_{n−1} v)...) | x_{1} :: x_{2} => letval x = r x_{1} v inletval y = s x_{1} v in g u_{0}(...(g u_{n−1}(g x_{2}(g x y)))...) end end | h => Ω.

Since x⃗x_{1}x_{2}xy ⊢ (f @(x, x_{2}, u_{n−1},..., u_{0}) y) R (g u_{0}(...(g u_{n−1}(g x_{2}(g x y)))...)) and x⃗ ⊢ (f @(u_{n−1},..., u_{0}) v) R (g u_{0}(...(g u_{n−1} v)...)), we get that

x⃗ ⊢ (f @(u_{n}, u_{n−1},..., u_{0}) v) ⊳^{∘} R^{C} ∼^{∘} (g u_{0}(...(g u_{n−1}(g u_{n} v))...)).

Hence R ⊆ ⊳^{∘} R^{C} ∼^{∘} and thus R ⊆ ≲^{∘} by Proposition 13. From the calculations above it is easy to obtain R^{op} ⊆ ⊳^{∘} (R^{op})^{C} ∼^{∘} too, and hence R^{op} ⊆ ≲^{∘}, again by Proposition 13. We conclude that R ⊆ ∼^{∘} and f ∼ g.

The shortcoming of Lemma 7, compared to (7.1), is less apparent in the derived equational rules of Propositions 12 and 13. But note that they work for open relations, in contrast to the ‘closed’ equational rule for simulation up to similarity of Proposition 3. We do not know if stronger, closed versions hold:

(i) \frac{R ⊆ ⊳ ∼ \overline{(R^{∘})^{C}} ≲}{R ⊆ ≲}  (ii) \frac{R ⊆ ⊳ (R^{∘})^{C} ≲}{R ⊆ ≲}  (7.4)

They are consequences of (7.1) because ⊳ ∼ \overline{(R^{∘})^{C}} ≲ ⊆ ⟨⊳ ∼^{∘} (R^{∘})^{C} ≲^{∘}⟩ and (ii) follows from (i) as in the proof of Proposition 13. Propositions 12 and 13 are weaker than (7.4): sometimes reasoning about open terms does not suffice as it may be necessary to argue by cases on the values of the free variables. One such example is syntactic minimal invariance, Proposition 11. It would follow from (7.4)(i), by structural induction on closed values, but not from Proposition 12.

8 Conclusion

The ‘relational’ proof style of Howe (1996) and Pitts (1995) has been used throughout this paper. It is a rather low-level approach but is precise and tractable and applies to a wide range of problems involving term contexts and evaluation. Our proofs of the unfolding theorem and various simulation up to context results substantiate this. The algebra of relations in Section 3 and, in particular, context closure facilitate the construction of relations for this style of proofs. Our results are stated for an untyped ML fragment but should carry over to other typed and untyped higher-order languages.

Simulation up to context is a proof technique with a great practical potential for applicative bisimulation and improvement. This is witnessed by our proofs of recursion induction, the improvement theorem, syntactic minimal invariance, and Exercise 10.20 from Winskel (1993), as well as by the examples of Gordon (1995) and Sands (1997b). But an important problem is left open, namely the validity of (5.14) and (7.1),

\frac{R ⊆ ⟨(R^{∘})^{C}⟩}{R ⊆ ≲}  \frac{R ⊆ ⟨⊳ ∼^{∘} (R^{∘})^{C} ≲^{∘}⟩}{R ⊆ ≲}

The significance of the gap between these and the weaker rule of Lemma 7,

\frac{R\{\overline{R^{C}}\} ∩ Rel ⊆ ⟨⊳ ∼^{∘} R^{C} ≲^{∘}⟩}{R ⊆ ≲^{∘}}

is unclear. In Section 7 we demonstrated how Lemma 7 allows us to prove a range of non-trivial results.

Acknowledgements After some time of fruitless investigations into applicative bisimulation up to context, this work got under way when Andrew Pitts showed me his notes on the subject (Pitts 1995). I am grateful for his encouragement and valuable guidance in this project. I wish to thank David Sands for discussions; his work has been influential in every aspect of this research. Finally, I am indebted to Andrew Gordon, Peter Ørbæk and an anonymous referee for detailed comments and helpful suggestions. I am supported by a grant from the Danish Natural Science Research Council.

A Proofs

This appendix contains the rather delicate proofs of Lemmas 6 and 7. The first of these uses the following lemma.

Lemma 8 Compatibility is preserved by transitive closure.

Proof First observe that compatibility is preserved by relation composition: if R and S are compatible, so is their composition R S,

R̂ S = R̂ Ŝ ⊆ R S.

Next, suppose R is compatible. If x⃗ ⊢ e R̂^{+} e′, each immediate subterm e_{i} of e is related to a corresponding subterm e′_{i} of e′, x⃗y⃗_{i} ⊢ e_{i} R^{+} e′_{i}, for some y⃗_{i}. This means that there exists m_{i} ≥ 1 such that x⃗y⃗_{i} ⊢ e_{i} R^{m_{i}} e′_{i}, where R^{m_{i}} is the m_{i}-fold composition of R with itself. Let m be the greatest of these m_{i}, for all pairs of subterms. Since R is compatible it is also reflexive. Hence x⃗y⃗_{i} ⊢ e_{i} R^{m−m_{i}} e_{i} and then x⃗y⃗_{i} ⊢ e_{i} R^{m} e′_{i}, for all corresponding subterms e_{i} and e′_{i}. Hence x⃗ ⊢ e R̂^{m} e′, by definition of compatible refinement, and then x⃗ ⊢ e R^{m} e′ because compatibility is preserved by relation composition. So x⃗ ⊢ e R^{+} e′ and we conclude that R^{+} is compatible. □

Proof of Lemma 6 \frac{R ⊆ ⟨S^{+}⟩_{I}}{S^{+} ⊆ ⊳ ∼^{∘}}, where S =^{def} (R^{∘})^{C}.

Proof Assume R ⊆ ⟨S^{+}⟩_{I}. We are going to prove that S^{+} is an open improvement simulation,

S^{+} ⊆ ⟨S^{+}⟩_{I}^{∘}.

Then S^{+} ⊆ ⊳ ∼^{∘}, by the improvement simulation rule (6.2).

First we need some properties of S^{+}.

By definition of context closure, S is compatible. Compatibility is preserved by transitive closure, Lemma 8, so S^{+} is also compatible.

Open extension, R^{∘}, is closed under substitutions and so is S because closure under substitutions is preserved by context closure. It is also preserved by relation composition and, consequently, by transitive closure. Therefore S^{+} is closed under substitutions.

By Lemma 1, S^{+} is substitutive because it is compatible, transitive and closed under substitutions.

We proceed to prove S^{+} ⊆ ⟨S^{+}⟩_{I}^{∘}. Since S^{+} is closed under substitutions, it suffices to show S^{+} ∩ Rel ⊆ ⟨S^{+}⟩_{I}. This is equivalent to asserting that predicate P(N), defined by

P(N) ⇔^{def} \begin{matrix}∀p, p′, v. ⊢ p S^{+} p′ & p ⇓_{N} v ⇒ \\ ∃v′. p′ ⇓_{≤N} v′ & ⊢ v \overline{S^{+}} v′, \end{matrix}

holds for all N. The proof is by a series of nested inductions on N, on the derivation of ⊢ p S^{+} p′, and on the derivation of p ⇓_{N} v.

The outer induction hypothesis is

(I.H.1) P(N) for all N < N_{0}.

Then we must show P(N_{0}). This follows if

∀p, p′, v. ⊢ p S p′ & p ⇓_{≤N_{0}} v ⇒ ∃v′. p′ ⇓_{≤N_{0}} v′ & ⊢ v \overline{S^{+}} v′, (A.1)

because, supposing ⊢ p S^{+} p′,

⊢ p = p_{0} S p_{1} S ⋯ S p_{m} = p′,

and p ⇓_{N_{0}} v, by repeatedly applying (A.1) to ⊢ p_{i} S p_{i+1}, we get p′ ⇓_{≤N_{0}} v′ with

⊢ v = v_{0} \overline{S^{+}} ⋯ \overline{S^{+}} v_{m} = v′,

and we can conclude ⊢ v \overline{S^{+}} v′ because \overline{S^{+}} is transitive,

\overline{S^{+}} ⋯ \overline{S^{+}} = \overline{S^{+} ⋯ S^{+}} ⊆ \overline{S^{+}}.

We strengthen (A.1) slightly and prove that predicate Q(p, M, v),

Q(p, M, v) ⇔^{def} \begin{matrix}p ⇓_{M} v & M ≤ N_{0} ⇒ \\ ∀p′. ⊢ p S\{\overline{S^{+}}\} p′ ⇒ \\ ∃v′. p′ ⇓_{≤M} v′ & ⊢ v \overline{S^{+}} v′, \end{matrix}

holds for all p, M, v. This entails (A.1) as ⊢ p S p′ clearly implies ⊢ p S\{\overline{S^{+}}\} p′ with empty substitution of \overline{S^{+}}. Observe also that S\{\overline{S^{+}}\} ⊆ S^{+} because \overline{S^{+}} ⊆ S^{+}, by compatibility, and S{S^{+}} ⊆ S^{+}, since S ⊆ S^{+} and S^{+} is substitutive. In fact, Q(p, M, v) follows from (I.H.1) whenever M < N_{0}.

We prove Q(p, M, v), for all p, M, v, by induction on the derivation of p ⇓_{M} v. For any derivation p_{0} ⇓_{M_{0}} v_{0}, the induction hypothesis is

(I.H.2) Q(p, M, v) for all premises p ⇓_{M} v in the derivation of p_{0} ⇓_{M_{0}} v_{0},

and we must show Q(p_{0}, M_{0}, v_{0}). We assume p_{0} ⇓_{M_{0}} v_{0} and M_{0} ≤ N_{0}, where p_{0} = e\{u⃗/x⃗\}, x⃗ ⊢ e S e′ and ⊢ u⃗ \overline{S^{+}} u′ such that ⊢ e\{u⃗/x⃗\} S\{\overline{S^{+}}\} e′\{^{u′}/x⃗\}. We will show e′\{^{u′}/x⃗\} ⇓_{≤M_{0}} v′_{0}, for some v′_{0} such that ⊢ v_{0} \overline{S^{+}} v′_{0}.

The strategy is to exploit the assumption x⃗ ⊢ e S e′ to build the derivation e′{^{u′}/x⃗} ⇓_{≤M_{0}} v′_{0}. The substitutions of u⃗ and u′ are separated out in the induction on the derivation of e{u⃗/x⃗} ⇓_{M_{0}} v_{0}. If it is derived by means of the (Eval apply) rule, we need to perform these substitutions and we end up with terms related by S^{+} rather than S\{\overline{S^{+}}\}. Then we invoke the stronger induction hypothesis (I.H.1). It applies because the premises of the (Eval apply) rule will all have cost-indexes smaller than M_{0} and N_{0}.

Recall S = (R^{∘})^{C} and consider the derivation of x⃗ ⊢ e S e′. There are two cases.

(Ctx R) Suppose y⃗ ⊢ e R^{∘} e′ with y⃗ ⊆ x⃗. Note that x⃗ ⊢ e Ŝ e because S and Ŝ are reflexive. Therefore ⊢ e\{u⃗/x⃗\} Ŝ\{\overline{S^{+}}\} e\{^{u′}/x⃗\}. From the (Ctx Comp) case below we get e\{^{u′}/x⃗\} ⇓_{≤M_{0}} v′′_{0} with ⊢ v_{0} \overline{S^{+}} v′′_{0}. Moreover, ⊢ e{^{u′}/x⃗} R e′{^{u′}/x⃗}. The assumption R ⊆ ⟨S^{+}⟩_{I} implies e′{^{u′}/x⃗} ⇓_{≤M_{0}} v′_{0} with ⊢ v′′_{0} \overline{S^{+}} v′_{0}. Since \overline{S^{+}} is transitive, we obtain ⊢ v_{0} \overline{S^{+}} v′_{0}, as required.

(Ctx Comp) Suppose x⃗ ⊢ e Ŝ e′. If this is derived by the (Comp x) rule, then e = e′ = x_{i}, for some x_{i} ∈ x⃗, and the result is immediate because e{u⃗/x⃗} ⇓_{0} u_{i}, e′\{^{u′}/x⃗\} ⇓_{0} u′_{i} and, by assumption, ⊢ u_{i} \overline{S^{+}} u′_{i}. Otherwise e and e′ are not variables, and we proceed by analysis of the derivation of e{u⃗/x⃗} ⇓_{M_{0}} v_{0}.

Case (Eval fn) e{u⃗/x⃗} is a function, e{u⃗/x⃗} = v_{0}, and M_{0} = 0. Since e is not a variable, it is itself a function, e = fn y => d for some d ∈ Exp_{x⃗y}. Then x⃗ ⊢ e Ŝ e′ must be derived by (Comp fn) so that e′ = fn y => d′ where x⃗y ⊢ d S d′. Hence e′\{^{u′}/x⃗\} ⇓_{0} e′\{^{u′}/x⃗\} and ⊢ e\{u⃗/x⃗\} \overline{S^{+}} e′\{^{u′}/x⃗\}, by (Eval fn) and (Match fn) because y ⊢ d\{u⃗/x⃗\} S\{\overline{S^{+}}\} d′\{^{u′}/x⃗\} and S\{\overline{S^{+}}\} ⊆ S^{+}.

Case (Eval nil) By reasoning similar to the previous case, we see e and e′ are both nil. Hence e′\{^{u′}/x⃗\} ⇓_{0} e′\{^{u′}/x⃗\} and ⊢ e\{u⃗/x⃗\} \overline{S^{+}} e′\{^{u′}/x⃗\}, by (Eval nil) and (Match nil).

Case (Eval cons) Since e is not a variable, it must be of the form e = e_{1} :: e_{2}, and e_{i}{u⃗/x⃗} ⇓_{M_{i}} v_{i}, for i = 1, 2, such that M_{0} = M_{1} +M_{2} and v_{0} = v_{1} :: v_{2}. Then x⃗ ⊢ e Ŝ e′ implies e′ = e′_{1} :: e′_{2} and x⃗ ⊢ e_{i} S e′_{i}. Observe that M_{i} ≤ N_{0} because M_{i} ≤ M_{0} and M_{0} ≤ N_{0}. Induction hypothesis (I.H.2) and e_{i}\{u⃗/x⃗\} ⇓_{M_{i}} v_{i} imply e′_{i}\{^{u′}/x⃗\} ⇓_{≤M_{i}} v′_{i} with ⊢ v_{i} \overline{S^{+}} v′_{i}. Hence e′\{^{u′}/x⃗\} ⇓_{≤M_{0}} v′_{0} with ⊢ v_{0} = v_{1} :: v_{2} \overline{S^{+}} v′_{1} :: v′_{2}, by (Eval Cons) and (Match Cons).

Case (Eval apply) e = e_{1}e_{2}, e_{1}{u⃗/x⃗} ⇓_{M_{1}} v_{1} = fn y => d, e_{2}{u⃗/x⃗} ⇓_{M_{2}} v_{2}, d{v^{2}/y} ⇓_{M_{3}} v_{0}, and M_{0} = M_{1} + M_{2} + M_{3} + 1. Since x⃗ ⊢ e Ŝ e′, e′ = e′_{1}e′_{2} with x⃗ ⊢ e_{i} S e′_{i}. We observe that M_{i} < N_{0} because M_{i} < M and M ≤ N_{0}, for i = 1, 2, 3. By induction hypothesis (I.H.2), e_{i}{u⃗/x⃗} ⇓_{M_{i}} v_{i} implies e′_{i}\{^{u′}/x⃗\} ⇓_{≤M_{i}} v′_{i} with ⊢ v_{i} \overline{S^{+}} v′_{i}, for i = 1, 2. So v′_{1} = fn y => d′ where y ⊢ d S^{+} d′. Hence ⊢ d{v^{2}/y} S^{+} d′{v′_{2}/y}, because S^{+} is substitutive. Since M_{3} < N_{0}, induction hypothesis (I.H.1) and d{v^{2}/y} ⇓_{M_{3}} v_{0} imply d′\{v′_{2}/y\} ⇓_{≤M_{3}} v′_{0} with ⊢ v_{0} \overline{S^{+}} v′_{0}. By (Eval apply), we conclude e′{^{u′}/x⃗} ⇓_{≤M_{0}} v′_{0}.

Case (Eval let fun) e = letfun f y = e_{1} in e_{2} end, e_{2}{u⃗w/x⃗f} ⇓_{M_{0}} v_{0}, where w = rec f y => e_{1}. Since x⃗ ⊢ e Ŝ e′, e′ = letfun f y=e′_{1} in e′_{2} end with x⃗fy ⊢ e_{1} S e′_{1} and x⃗f ⊢ e_{2} S e′_{2}. Let w′ = rec f y => e′_{1}, then x⃗ ⊢ w \overline{S} w′ because S is compatible. Consequently, x⃗ ⊢ w \overline{S^{+}} w′ and ⊢ e_{2}\{u⃗w/x⃗f\} S\{\overline{S^{+}}\} e′_{2}\{^{u′}w′/x⃗f\}. By induction hypothesis (I.H.2), e_{2}\{u⃗w/x⃗f\} ⇓_{M_{0}} v_{0} implies e′_{2}\{^{u′}w′/x⃗f\} ⇓_{≤M_{0}} v′_{0} with ⊢ v_{0} \overline{S^{+}} v′_{0}. By (Eval let fun), we conclude e′{^{u′}/x⃗} ⇓_{≤M_{0}} v′_{0}.

Case (Eval case) e = case e_{0} ofnil => e_{1} | y_{1} :: y_{2} => e_{2} | f => e_{3}, e_{0}{u⃗/x⃗} ⇓_{M_{1}} v, q ⇓_{M_{2}} v_{0}, and M_{0} = M_{1} + M_{2}, where

q = \{ \begin{matrix}e_{1}\{u⃗/x⃗\} & if v = nil \\ e_{2}\{u⃗v^{1}v^{2}/x⃗y_{1}y_{2}\} & if v = v_{1} :: v_{2} \\ e_{3}\{u⃗v/x⃗f\} & if v = fn y => d. \end{matrix}

Since x⃗ ⊢ e Ŝ e′, e′ = case e′_{0} ofnil => e′_{1} | y_{1} :: y_{2} => e′_{2} | f => e′_{3}, with x⃗ ⊢ e_{0} S e′_{0}, x⃗ ⊢ e_{1} S e′_{1}, x⃗y_{1}y_{2} ⊢ e_{2} S e′_{2}, and x⃗f ⊢ e_{3} S e′_{3}. Observe that M_{i} ≤ N_{0} because M_{i} ≤ M_{0} and M_{0} ≤ N_{0}. Induction hypothesis (I.H.2) and e_{0}\{u⃗/x⃗\} ⇓_{M_{1}} v imply e′_{0}\{^{u′}/x⃗\} ⇓_{≤M_{1}} v′ with ⊢ v \overline{S^{+}} v′. According to the derivation of ⊢ v \overline{S^{+}} v′, let

q′ = \{ \begin{matrix}e′_{1}\{^{u′}/x⃗\} & if v = nil = v′ \\ e′_{2}\{^{u′}v′_{1}v′_{2}/x⃗y_{1}y_{2}\} & if v = v_{1} :: v_{2}, v′ = v′_{1} :: v′_{2}, ⊢ v_{i} \overline{S^{+}} v′_{i} \\ e′_{3}\{^{u′}v′/x⃗f\} & if ⊢ v = fn y => d \overline{S^{+}} fn y => d′ = v′. \end{matrix}

By inspection of the definitions of q and q′, we see that ⊢ q S\{\overline{S^{+}}\} q′. Induction hypothesis (I.H.2) and q ⇓_{M_{2}} v_{0} imply q′ ⇓_{≤M_{2}} v′_{0} with ⊢ v_{0} \overline{S^{+}} v′_{0}. By (Eval case), we conclude e′{^{u′}/x⃗} ⇓_{≤M_{0}} v′_{0}.

Case (Eval let val) Similar to the previous case.

All cases considered, we conclude Q(p_{0}, M_{0}, v_{0}), as required. This completes the induction step for Q and we have Q(p, M, v) for all p, M, v.

Therefore (A.1) and P(N_{0}) hold. This completes the induction step for P, so P(N) holds for all N.

Then S^{+} ∩ Rel ⊆ ⟨S^{+}⟩_{I} and S^{+} is an open improvement simulation, S^{+} ⊆ ⟨S^{+}⟩_{I}^{∘}. The conclusion, S^{+} ⊆ ⊳ ∼^{∘}, follows co-inductively by the improvement simulation rule (6.2). □

Lemma 6 is invalid for similarity (i.e., with ⟨ ⟩ and ≲^{∘} in place of ⟨ ⟩_{I} and ⊳ ∼^{∘}). The proof above uses the improvement aspect of ⟨ ⟩_{I} to assert that p′ ⇓ v′ computes no slower than p ⇓ v when ⊢ p S p′. If there is no bound on the cost of p′ ⇓ v′, the transitivity argument, why (A.1) implies P(N_{0}), breaks down.

The proof of Lemma 6 makes use of the transitive closure of S in two ways.

(i) S^{+} is substitutive. This is used in the (Eval fn) and (Eval apply) cases of the induction step.

(ii) In the (Ctx R) case transitivity is used to avoid substitution of values related by \overline{S^{+}} into expressions related by R^{∘}.

Lemma 7 is essentially a weaker version of Lemma 6 for similarity. The proof is similar to that of Lemma 6 but solves (i) and (ii) without transitive closure.

(i) Substitutions can be replaced by let bindings up to cost equivalence; thereby the compatibility of R^{C} suffices and substitutivity is not necessary.

(ii) The requirement that the premise of Lemma 7 holds for R\{\overline{R^{C}}\} rather than just R circumvents the problem of substitution into expressions related by R.

Proof of Lemma 7 \frac{R\{\overline{R^{C}}\} ∩ Rel ⊆ ⟨⊳ ∼^{∘} R^{C} ≲^{∘}⟩}{R ⊆ ≲^{∘}}

Proof Assume R\{\overline{R^{C}} ∩ Rel\} ⊆ ⟨⊳ ∼^{∘} R^{C} ≲^{∘}⟩. We are going to prove

R^{C}{Id} ⊆ ⟨S⟩, where S = ⊳ ∼^{∘} R^{C} ≲^{∘}.  (A.2)

Observe that S ⊆ ≲^{∘} R^{C}{Id}^{∘} ≲^{∘}, because ⊳ ∼^{∘} ⊆ ≲^{∘} and R^{C} ⊆ R^{C}{Id}^{∘}, by (3.2). By simulation up to similarity, Proposition 2, we get that (A.2) implies R^{C}{Id} ⊆ ≲. Hence R^{C} ⊆ ≲^{∘}, by (3.2), and the conclusion, R ⊆ ≲^{∘}, follows because R ⊆ R^{C},

S is compatible because ⊳ ∼^{∘}, R^{C}, and ≲^{∘} are and compatibility is preserved by relation composition. Therefore S is reflexive and \overline{S} is a reflexive relation on values. Hence R^{C}\{Id\} ⊆ R^{C}\{\overline{S}\}, and (A.2) holds if R^{C}\{\overline{S}\} ⊆ ⟨S⟩. The latter is equivalent to the predicate P(N) holding for all N, where

P(N) ⇔^{def} \begin{matrix}∀p, p′, v. ⊢ p R^{C}\{\overline{S}\} p′ & p ⇓_{N} v ⇒ \\ ∃v′. p′ ⇓ v′ & ⊢ v \overline{S} v′, \end{matrix}

We proceed by induction on N. The induction hypothesis is

(I.H.1) P(N) for all N < N_{0}.

Then we must show P(N_{0}). This follows if Q(p, M, v),

Q(p, M, v) ⇔^{def} \begin{matrix}p ⇓_{M} v & M ≤ N_{0} ⇒ \\ ∀p′. ⊢ p R^{C}\{\overline{S}\} p′ ⇒ \\ ∃v′. p′ ⇓ v′ & ⊢ v \overline{S} v′, \end{matrix}

holds for all p, M, v. We prove Q(p, M, v), for all p, M, v, by induction on the derivation of p ⇓_{M} v. For any derivation p_{0} ⇓_{M_{0}} v_{0}, the induction hypothesis is

(I.H.2) Q(p, M, v) for all premises p ⇓_{M} v in the derivation of p_{0} ⇓_{M_{0}} v_{0},

and we must show Q(p_{0}, M_{0}, v_{0}). We assume p_{0} ⇓_{M_{0}} v_{0} and M_{0} ≤ N_{0}, where p_{0} = e\{u⃗/x⃗\}, x⃗ ⊢ e R^{C} e′ and ⊢ u⃗ \overline{S} u′ such that ⊢ e\{u⃗/x⃗\} R^{C}\{\overline{S}\} e′\{^{u′}/x⃗\}. We will show e′\{^{u′}/x⃗\} ⇓ v′_{0}, for some v′_{0} such that ⊢ v_{0} \overline{S} v′_{0}.

Consider the derivation of x⃗ ⊢ e R^{C} e′. There are two cases.

(Ctx R) Suppose x⃗ ⊢ e R e′. Since ⊢ u⃗ \overline{S} u′, there exist w⃗ and w′ such that ⊢ u⃗ \overline{⊳ ∼^{∘}} w⃗ \overline{R^{C}} w′ \overline{≲^{∘}} u′. As ⊳ ∼^{∘} and ≲^{∘} are precongruences, we get

e\{u⃗/x⃗\} ⊳ ∼ e\{w⃗/x⃗\} R\{\overline{R^{C}}\} e′\{^{w′}/x⃗\} ≲ e′\{^{u′}/x⃗\}

Since e\{u⃗/x⃗\} ⇓ v_{0}, also e\{w⃗/x⃗\} ⇓ v with ⊢ v_{0} \overline{⊳ ∼^{∘}} v. From assumption R\{\overline{R^{C}}\}∩Rel ⊆ ⟨S⟩ follows e′\{^{w′}/x⃗\} ⇓ v′ with ⊢ v \overline{S} v′. Finally, e′\{^{u′}/x⃗\} ⇓ v′_{0} with ⊢ v′ \overline{≲^{∘}} v′_{0}, and ⊢ v_{0} \overline{⊳ ∼^{∘}} v \overline{S} v′ \overline{≲^{∘}} v′_{0} implies ⊢ v_{0} \overline{S} v′_{0} because ⊳ ∼^{∘} S ≲^{∘} ⊆ S by transitivity of ⊳ ∼^{∘} and ≲^{∘}.

(Ctx Comp) If x⃗ ⊢ e R̂^{C} e′, we argue as in the proof of Lemma 6 above (with R^{C} and \overline{S} in place of S and \overline{S^{+}}), except that here we do not keep track of the cost of the evaluation e′{^{u′}/x⃗} ⇓ v′_{0}. Again the result is immediate if e is a variable. Otherwise we proceed by analysis of the derivation of e{u⃗/x⃗} ⇓_{M_{0}} v_{0}. Only the cases when this is derived by (Eval fn) or (Eval apply) are different from those in the proof of Lemma 6.

Case (Eval fn) e{u⃗/x⃗} is a function and e{u⃗/x⃗} = v_{0}. Since e is not a variable, it is itself a function, e = fn y => d for some d ∈ Exp_{x⃗y}. Then x⃗ ⊢ e R̂^{C} e′ must be derived by (Comp fn) so that e′ = fn y => d′ where x⃗y ⊢ d R^{C} d′. Since ⊢ u⃗ \overline{S} u′, there exist w⃗ and w′ such that ⊢ u⃗ \overline{⊳ ∼^{∘}} w⃗ \overline{R^{C}} w′ \overline{≲^{∘}} u′. As ⊳ ∼^{∘}, R^{C}, and ≲^{∘} are compatible, we get

y ⊢ d{u⃗/x⃗} ⊳ ∼^{∘} d{w⃗/x⃗} R^{C}{R^{C}} d′{^{w′}/x⃗} ≲^{∘} d′{^{u′}/x⃗}.

Let (let x⃗ = v⃗ in e) abbreviate a suitable let construction which beta reduces to e{v⃗/x⃗}. Then

y ⊢ d\{w⃗/x⃗\} {◁▷ \atop ∼}^{∘} (let x⃗ = w⃗ in d) R^{C} (let x⃗ = w′ in d′) {◁▷ \atop ∼}^{∘} d′\{^{w′}/x⃗\}.

Since ⊳ ∼ and ≲ contain {◁▷ \atop ∼} and are transitive,

y ⊢ d{u⃗/x⃗} S d′{^{u′}/x⃗},

Hence ⊢ e\{u⃗/x⃗\} \overline{S} e′\{^{u′}/x⃗\}, as required.

Case (Eval apply) e = e_{1}e_{2}, e_{1}{u⃗/x⃗} ⇓_{M_{1}} v_{1} = fn y => d_{1}, e_{2}{u⃗/x⃗} ⇓_{M_{2}} v_{2}, d_{1}{v^{2}/y} ⇓_{M_{3}} v_{0}, and M_{0} = M_{1} + M_{2} + M_{3} + 1. Since x⃗ ⊢ e R̂^{C} e′, e′ = e′_{1}e′_{2} with x⃗ ⊢ e_{i} R^{C} e′_{i}. We observe that M_{i} < N_{0} because M_{i} < M and M ≤ N_{0}, for i = 1, 2, 3. By induction hypothesis (I.H.2), e_{i}{u⃗/x⃗} ⇓_{M_{i}} v_{i} implies e′_{i}\{^{u′}/x⃗\} ⇓ v′_{i} with ⊢ v_{i} \overline{S} v′_{i}, for i = 1, 2. So v′_{1} = fn y => d′_{1} where y ⊢ d_{1} S d′_{1}, that is, there exist d, d′ ∈ Exp_{y} such that y ⊢ d_{1} ⊳ ∼^{∘} d R^{C} d′ ≲^{∘} d′_{1}. Since ⊳ ∼^{∘} and ≲^{∘} are closed under substitutions, d_{1}{v^{2}/y} ⊳ ∼ d{v^{2}/y} and d′{v′_{2}/y} ≲ d′_{1}{v′_{2}/y}. From the former and d_{1}{v^{2}/y} ⇓_{M_{3}} v_{0}, we get d\{v^{2}/y\} ⇓_{≤M_{3}} v with ⊢ v_{0} \overline{⊳ ∼^{∘}} v. As M_{3} < N_{0} and ⊢ d\{v^{2}/y\} R^{C}\{\overline{S}\} d′\{v′_{2}/y\}, induction hypothesis (I.H.1) and d{v^{2}/y} ⇓_{≤M_{3}} v imply d′{v′_{2}/y} ⇓ v′ with ⊢ v \overline{S} v′. Since d′\{v′_{2}/y\} ≲ d′_{1}\{v′_{2}/y\}, d′_{1}\{v′_{2}/y\} ⇓ v′_{0} with ⊢ v′ \overline{≲^{∘}} v′_{0}. Then ⊢ v_{0} \overline{S} v′_{0} because \overline{⊳ ∼^{∘}} \overline{S} \overline{≲^{∘}} = \overline{⊳ ∼^{∘} S ≲^{∘}} and ⊳ ∼^{∘} S ≲^{∘} ⊆ S. By (Eval apply), we conclude e′{^{u′}/x⃗} ⇓ v′_{0}.

This establishes R^{C}\{\overline{S}\} ⊆ ⟨S⟩ and then (A.2) follows, as required. □

References

Abramsky, S. (1990). The lazy lambda calculus. In D. Turner (Ed.), Research topics in functional programming, pp. 65–116. Addison-Wesley.

Bird, R. and P. Wadler (1987). Introduction to Functional Programming. International Series in Computer Science. Prentice-Hall.

Braüner, T. (1996, November). An axiomatic approach to adequacy. Technical Report DS-96-4, BRICS, Department of Computer Science, University of Aarhus. Ph.D. thesis.

Clinger, W. and J. Rees (editors) (1991, July-September). Revised^{4} report on the algorithmic language scheme. LISP Pointers IV(3), 1–55.

Felleisen, M. and D. P. Friedman (1987). Control operators, the SECD-machine, and the λ-calculus. In M. Wirsing (Ed.), Formal Description of Programming Concepts III. IFIP.

Ferreira, W., M. Hennessy, and A. Jeffrey (1995, September). A theory of weak bisimulation for core CML. Technical Report 05/95, COGS, University of Sussex.

Gordon, A. D. (1994). Functional Programming and Input/Output. Cambridge University Press.

Gordon, A. D. (1995, July). Bisimilarity as a theory of functional programming. Mini-course. BRICS Notes Series NS-95-3, BRICS, Department of Computer Science, University of Aarhus.

Gordon, A. D. (1997). Operational equivalences for untyped and polymorphic object calculi. See Gordon and Pitts (1997).

Gordon, A. D. and A. M. Pitts (Eds.) (1997). Higher Order Operational Techniques in Semantics, Publications of the Newton Institute. Cambridge University Press.

Gordon, A. D. and G. D. Rees (1996). Bisimilarity for a first-order calculus of objects with subtyping. In POPL’96 Symposium on Principles of Programming Languages. ACM.

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

Howe, D. J. (1996). Proving congruence of bisimulation in functional programming languages. Information and Computation 124(2), 103–112.

Klop, J. W., V. van Oostrom, and F. van Raamsdonk (1993). Combinatory reduction systems: introduction and survey. Theoretical Computer Science 121, 279–308.

Lassen, S. B. (1997). Action semantics reasoning about functional programs. Mathematical Structures in Computer Science. Special issue dedicated to the Workshop on Logic, Domains, and Programming Languages (Darmstadt, May 1995). To appear.

Lawall, J. L. and H. G. Mairson (1996). Optimality and inefficiency: what isn’t a cost model of the lambda calculus. In ICFP’96 International Conference on Functional Programming, pp. 92–101. ACM.

Mason, I. A., S. F. Smith, and C. L. Talcott (1996). From operational semantics to domain theory. Information and Computation 128(1), 26–47.

Milner, R. (1977). Fully abstract models of typed lambda-calculi. Theoretical Computer Science 4, 1–23.

Milner, R. (1989). Communication and Concurrency. Prentice-Hall.

Milner, R., M. Tofte, and R. Harper (1990). The Definition of Standard ML. Cambridge, Mass.: MIT Press.

Moggi, E. (1989). Computational lambda-calculus and monads. In 4th Annual Symposium on logic in computer science, pp. 14–23. IEEE.

Ong, C.-H. L. (1992, August 7). Concurrent lambda calculus and a general pre-congruence theorem for applicative bisimulation (preliminary version). Unpublished.

Park, D. M. (1981). Concurrency and automata on infinite sequences. In P. Deussen (Ed.), Conference on Theoretical Computer Science, Volume 104 of Lecture Notes in Computer Science, pp. 167–183. Springer-Verlag.

Pitts, A. M. (1994a, November). Inductive and co-inductive techniques in the semantics of functional programs. Course held at BRICS, Department of Computer Science, University of Aarhus.

Pitts, A. M. (1994b, December). Some notes on inductive and co-inductive techniques in the semantics of functional programs (draft version). BRICS Notes Series NS-94-5, BRICS, Department of Computer Science, University of Aarhus.

Pitts, A. M. (1995, March). An extension of Howe’s construction to yield simulation-up-to-context results. Unpublished Manuscript.

Pitts, A. M. (1996a). A note on logical relations between semantics and syntax. Submitted to the Journal of the Interest Group in Pure and Applied Logics, Special Issue for 3rd Workshop on Logic, Language, Information and Computation (WoLLIC’96) May, 1996 Salvador (Bahia), Brazil.

Pitts, A. M. (1996b). Relational properties of domains. Information and Computation 127, 66–90.

Pitts, A. M. (1997). Operationally-based theories of program equivalence. In P. Dybjer and A. M. Pitts (Eds.), Semantics and Logics of Computation. Cambridge University Press.

Sands, D. (1991). Operational theories of improvement in functional languages (extended abstract). In Proceedings of the Fourth Glasgow Workshop on Functional Programming, Workshops in Computing Series, pp. 298–311. Springer-Verlag.

Sands, D. (1997a). From SOS rules to proof principles: An operational metatheory for functional languages. In POPL’97 Symposium on Principles of Programming Languages. ACM.

Sands, D. (1997b). Improvement theory and its applications. See Gordon and Pitts (1997).

Sangiorgi, D. (1994, August). On the bisimulation proof method. Technical Report LFCS-94-299, University of Edinburgh.

Sangiorgi, D. (1995, April). Lazy functions and mobile processes. Technical Report RR-2515, INRIA-Sophia Antipolis.

Sangiorgi, D. (1996). Locality and interleaving semantics in calculi for mobile processes. Theoretical Computer Science 155(1), 39–83.

Sangiorgi, D. and R. Milner (1992). The problem of “weak bisimulation up to”. In W. R. Cleveland (Ed.), CONCUR ’92, Volume 630 of Lecture Notes in Computer Science. Springer-Verlag.

Smith, S. F. (1997). The coverage of operational semantics. See Gordon and Pitts (1997).

Stoughton, A. (1988). Substitution revisited. Theoretical Computer Science 59, 317–325.

Talcott, C. (1997). Reasoning about functions with effects. See Gordon and Pitts (1997).

Winskel, G. (1993). The Formal Semantics of Programming Languages. Cambridge, Mass.: MIT Press.

Recent BRICS Report Series Publications

RS-97-24 Søren B. Lassen. Relational Reasoning about Contexts. September 1997. 45 pp. To appear as a chapter in the book Higher Order Operational Techniques in Semantics, eds. Andrew D. Gordon and Andrew M. Pitts, Cambridge University Press.

RS-97-23 Ulrich Kohlenbach. On the Arithmetical Content of Restricted Forms of Comprehension, Choice and General Uniform Boundedness. August 1997. 35 pp.

RS-97-22 Carsten Butz. Syntax and Semantics of the logic L_{ωω}^{λ}. July 1997. 14 pp.

RS-97-21 Steve Awodey and Carsten Butz. Topological Completeness for Higher-Order Logic. July 1997. 19 pp.

RS-97-20 Carsten Butz and Peter T. Johnstone. Classifying Toposes for First Order Theories. July 1997. 34 pp.

RS-97-19 Andrew D. Gordon, Paul D. Hankin, and Søren B. Lassen. Compilation and Equivalence of Imperative Objects. July 1997. iv+64 pp. Appears also as Technical Report 429, University of Cambridge Computer Laboratory, June 1997. To appear in Foundations of Software Technology and Theoretical Computer Science: 17th Conference, FCT&TCS ’97 Proceedings, LNCS, 1997.

RS-97-18 Robert Pollack. How to Believe a Machine-Checked Proof. July 1997. 18 pp. To appear as a chapter in the book Twenty Five Years of Constructive Type Theory, eds. Smith and Sambin, Oxford University Press.

RS-97-17 Peter Bro Miltersen. Error Correcting Codes, Perfect Hashing Circuits, and Deterministic Dynamic Dictionaries. June 1997. 10 pp.

RS-97-16 Noga Alon, Martin Dietzfelbinger, Peter Bro Miltersen, Erez Petrank, and Gábor Tardos. Linear Hashing. June 1997. 22 pp. A preliminary version appeared with the title Is Linear Hashing Good? in The Twenty-ninth Annual ACM Symposium on Theory of Computing, STOC ’97, pages 465–474.

RS-97-15 Pierre-Louis Curien, Gordon Plotkin, and Glynn Winskel. Bistructures, Bidomains and Linear Logic. June 1997. 41 pp.