BRICS RS-96-31 I. Stark: Names, Equations, Relations: Practical Ways to Reason about new

BRICS

Basic Research in Computer Science

Names, Equations, Relations: Practical Ways to Reason about new

Ian Stark

BRICS Report Series RS-96-31 ISSN 0909-0878 September 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

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

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

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

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

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

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

Names, Equations, Relations: Practical Ways to Reason about new

Ian Stark BRICS^{∗}, Department of Computer Science University of Aarhus, Denmark

September 1996

Abstract

The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with state in the form of dynamically-generated names. These names can be created locally, passed around, and compared with one another. Through the interaction between names and functions, the language can capture notions of scope, visibility and sharing. Originally motivated by the study of references in Standard ML, the nu-calculus has connections to other kinds of local declaration, and to the mobile processes of the π-calculus.

This paper introduces a logic of equations and relations which allows one to reason about expressions of the nu-calculus: this uses a simple representation of the private and public scope of names, and allows straightforward proofs of contextual equivalence (also known as observational, or observable, equivalence). The logic is based on earlier operational techniques, providing the same power but in a much more accessible form. In particular it allows intuitive and direct proofs of all contextual equivalences between first-order functions with local names.

∗Basic Research in Computer Science, a centre of the Danish National Research Foundation.

1 Introduction

Many convenient features of programming languages today involve some notion of generativity: the idea that an entity may be freshly created, distinct from all others. This is clearly central to object-oriented programming, with the dynamic creation of new objects as instances of a class, and the issue of object identity. In the study of concurrency, the π-calculus [13] uses dynamically-generated names to describe the behaviour of mobile processes, whose communication topology may change over time. In functional programming, the language Standard ML [14] extends typed lambda-calculus with a number of features, of which mutable reference cells, exceptions and user-declared datatypes are all generative; as are the structures and functors of the module system. More broadly, the concept of lexical scope rests on the idea that local identifiers should always be treated as fresh, distinct from any already declared.

The nu-calculus was devised to explore this common property of generativity, by adding names to the simply-typed lambda-calculus. Names may be created locally, passed around, and compared with one another, but that is all. The language is reviewed in Section 2; a full description is given by Pitts and Stark in [21, 22], with its operational and denotational semantics studied at some length in [25, 26]. Central to the nu-calculus is the use of name abstraction: the expression νn.M represents the creation of a fresh name, which is then bound to n within the body of M. So, for example, the expression

νn.νn′.(n = n′)

generates two new names, bound to n and n′, and compares them, finally returning the answer false. Functions may have local names that remain private and persist from one use of the function to the next; alternatively, names may be passed out of their original scope and can even outlive their creator. It is precisely this mobility of names that allows the nu-calculus to model issues of locality, privacy and non-interference.

Two expressions of the nu-calculus are contextually equivalent^{1} if they can be freely exchanged in any program: there is no way in the language itself to distinguish them. Contextual equivalence is an excellent property in principle, but in practice often hard to work with because of the need to consider all possible programs. As a consequence a number of authors have made considerable effort, in various language settings, to develop convenient methods for demonstrating contextual equivalence.

1The same property is variously known as {operational/observational/observable} {equivalence/congruence}.

Milner’s context lemma [12], Gordon’s ‘experiments’ [4], and the ‘ciu’ theorems of Mason and Talcott [9, 27], provide one such approach. These show that instead of all program contexts, it is sufficient to consider only those in some particular form. For the nu-calculus, a suitable context lemma is indeed available [25, §2.6] and states that one need only consider so-called ‘argument contexts’. However even this reduced collection of contexts is still inconveniently large, a problem arising from the imperative nature of name creation.

Alternatively, one can look for relations that imply contextual equivalence but are easier to work with. One possibility is to define such relations directly from the operational semantics of the language, as with the applicative bisimilarity variously used by Abramsky [1], Howe [7], Gordon [4], and others. Denotational semantics provides another route: if two expressions have equal interpretation in some adequate model, then they are contextually equivalent. For the nu-calculus, such operational methods are developed and refined in [21, 22], while categorical models are presented in [26]. Both approaches are treated at length in [25].

In principle, methods such as these do give techniques for proving contextual equivalences. In practice however, they are often awkward and can require rather detailed mathematical knowledge. The contribution of this paper is to take two existing operational techniques, and extract from them a straightforward logic that allows simple and direct reasoning about contextual equivalence in the nu-calculus.

The first operational technique, applicative equivalence, gives rise to an equational logic with assertions of the form

s, Γ ⊢ M_{1} =_{σ} M_{2} .

If such an assertion can be proved using the rules of the logic, then it is certain that expressions M_{1} and M_{2} are contextually equivalent (here s and Γ list the free names and variables respectively). This equational scheme is simple, but not particularly complete: it is good for reasoning in the presence of names, but not so good at reasoning about names themselves.

The technique of operational logical relations refines this by considering just how different expressions make use of their local names. The corresponding logic is one of relational reasoning, with assertions of the form

Γ ⊢ M_{1} R_{σ} M_{2} .

Here R is a relation between the free names of M_{1} and M_{2} that records information on their privacy and visibility. This logic includes the equational one, and is considerably more powerful: it is sufficient to prove all contextual equivalences between expressions of first-order function type.

It is significant that these schemes both build on existing methods; all the proofs of soundness and completeness work by transferring corresponding properties from the earlier operational techniques. For the completeness results in particular this is a considerable saving in proof effort. Such incremental development continues a form of ‘technology transfer’ from the abstract to the concrete: these same operational techniques were in turn guided by a denotational semantics for the nu-calculus based on categorical monads.

The layout of the paper is as follows: Section 2 reviews the nu-calculus and gives some representative examples of contextual equivalence; Section 3 describes the techniques of applicative equivalence and operational logical relations; Section 4 explains the new logic for equational reasoning; Section 5 extends this to a logic for relational reasoning; and Section 6 concludes.

Related Work

The general issue of adding effects to functional languages has received considerable attention over time, and there is a substantial body of work concerning operational and denotational methods for proving contextual equivalence. A selection of references can be found in [19, 27], for example. However, not so many practical systems have emerged for reasoning about expressions and proving actual examples of contextual equivalence.

Felleisen and Hieb [2] present a calculus for equational reasoning about state and control features. This extends β_{v}-interconvertibility and is similar to the equational reasoning of this paper, in that it is correct and convenient for proving contextual equivalence, but not particularly complete.

Mason and Talcott’s logic for reasoning about destructive update in Lisp [10] is again similar in power to our equational reasoning. Moreover, our underlying operational notion of applicative equivalence corresponds quite closely to Mason’s ‘strong isomorphism’ [8]. Further work [11] adds some particular reasoning principles that resemble aspects of our relational reasoning, but can only be applied to first-order functions; by contrast, our techniques remain valid at all higher function types. In a similar vein, the ‘variable typed logic of effects’ (VTLoE) of Honsell, Mason, Smith and Talcott [6] is an operationally-based scheme for proving certain assertions about functions with state.

The ‘computational metalanguage’ of Moggi [15] provides a general method for equational reasoning about additions to functional languages. Its application to the nu-calculus is discussed in [25, §3.3], where it is shown to correspond closely to applicative equivalence. Related to this is ‘evaluation logic’, a variety of modal logic that can express the possibility or certainty of certain computational effects [16, 20]. Moggi has shown how a variety of program logics, including VTLoE, can be expressed within evaluation logic [17].

Although the nu-calculus may appear simpler than the languages considered in the work cited, the notion of generativity it highlights is still of real significance. Moreover, the relational logic presented here goes beyond all of the above in the variety of contextual equivalences it can prove: we properly capture the subtle interaction between local declarations and higher-order functions.

2 The Nu-Calculus

A full description of the nu-calculus can be found in [25, 26]; this section gives just a brief overview. The language is based on the simply-typed lambdacalculus, with a hierarchy of function types σ → σ′ built over ground types o of booleans and ν of names. Expressions have the form

M ::= x | n | true | false | if M then M else M
| M = M | νn.M | λx:σ.M | MM .

Here x and n are typed variables and names respectively, taken from separate infinite supplies. The expression ‘M = M’ tests for equality between two names. Name abstraction νn.M creates a fresh name bound to n within the body M; during evaluation, names may outlive their creator and escape from their original scope. We implicitly identify expressions which only differ in their choice of bound variables and names (α-conversion). A useful ab-

\overline{s, Γ ⊢ x : σ} (x : σ ∈ Γ) \overline{s, Γ ⊢ n : ν} (n ∈ s) \overline{s, Γ ⊢ b : o} (b = true, false)

\frac{s, Γ ⊢ B : o s, Γ ⊢ M : σ s, Γ ⊢ M′ : σ}{s, Γ ⊢ if B then M else M′ : σ}

\frac{s, Γ ⊢ N : ν  s, Γ ⊢ N′ : ν}{s, Γ ⊢ (N = N′) : o}  \frac{s ⊕ \{n\}, Γ ⊢ M : σ}{s, Γ ⊢ νn.M : σ}

\frac{s, Γ ⊕ \{x : σ\} ⊢ M : σ′}{s, Γ ⊢ λx:σ.M : σ → σ′}  \frac{s, Γ ⊢ F : σ → σ′ s, Γ ⊢ M : σ}{s, Γ ⊢ F M : σ′}

Figure 1: Rules for assigning types to expressions of the nu-calculus

breviation is new for νn.n; this is the expression that generates a new name and then immediately returns it.

Expressions are typed according to the rules in Figure 1. The type assertion

s, Γ ⊢ M : σ

says that in the presence of s and Γ the expression M has type σ. Here s is a finite set of names, Γ is a finite set of typed variables, and M is an expression with free names in s and free variables in Γ. The symbol ⊕ represents disjoint union, here in s ⊕ {n} and Γ ⊕ {x : σ}. We may omit Γ when it is empty.

An expression is in canonical form if it is either a name, a variable, one of the boolean constants true or false, or a function abstraction. These are to be the values of the nu-calculus, and correspond to weak head normal form in the lambda-calculus. An expression is closed if it has no free variables; a closed expression may still have free names. We define the sets

Exp_{σ}(s, Γ) = { M | s, Γ ⊢ M : σ }
Can_{σ}(s, Γ) = { C | C ∈ Exp_{σ}(s, Γ), C canonical }
Exp_{σ}(s) = Exp_{σ}(s, ∅)
Can_{σ}(s) = Can_{σ}(s, ∅)

of expressions and canonical expressions, open and closed.

(CAN)  \overline{s ⊢ C ⇓_{σ} C} C canonical
(COND1)  \frac{s ⊢ B ⇓_{o} (s_{1})true  s ⊕ s_{1} ⊢ M ⇓_{σ} (s_{2})C}{s ⊢ if B then M else M′ ⇓_{σ} (s_{1} ⊕ s_{2})C}
(COND2)  \frac{s ⊢ B ⇓_{o} (s_{1})false  s ⊕ s_{1} ⊢ M′ ⇓_{σ} (s_{2})C′}{s ⊢ if B then M else M′ ⇓_{σ} (s_{1} ⊕ s_{2})C′}
(EQ1)  \frac{s ⊢ N ⇓_{ν} (s_{1})n s ⊕ s_{1} ⊢ N′ ⇓_{ν} (s_{2})n}{s ⊢ (N = N′) ⇓_{o} (s_{1} ⊕ s_{2})true} n ∈ s
(EQ2)  \frac{s ⊢ N ⇓_{ν} (s_{1})n s ⊕ s_{1} ⊢ N′ ⇓_{ν} (s_{2})n′}{s ⊢ (N = N′) ⇓_{o} (s_{1} ⊕ s_{2})false} n, n′ distinct
(LOCAL)  \frac{s ⊕ \{n\} ⊢ M ⇓_{σ} (s_{1})C}{s ⊢ νn.M ⇓_{σ} (\{n\} ⊕ s_{1})C} n ∉ (s ⊕ s_{1})
(APP)  \frac{\begin{matrix}s ⊢ F ⇓_{σ→σ′} (s_{1})λx:σ.M′ s ⊕ s_{1} ⊢ M ⇓_{σ} (s_{2})C \\ s ⊕ s_{1} ⊕ s_{2} ⊢ M′[C/x] ⇓_{σ′} (s_{3})C′ \end{matrix}}{s ⊢ F M ⇓_{σ′} (s_{1} ⊕ s_{2} ⊕ s_{3})C′}

Figure 2: Rules for evaluating expressions of the nu-calculus

The operational semantics of the nu-calculus is specified by the inductively defined evaluation relation given in Figure 2. Elements of the relation take the form

s ⊢ M ⇓_{σ} (s′)C

where s and s′ are disjoint finite sets of names, M ∈ Exp_{σ}(s) and C ∈ Can_{σ}(s ⊕ s′). This is intended to mean that in the presence of the names s, expression M of type σ evaluates to canonical form C and creates fresh names s′. We may omit s or s′ when they are empty.

Evaluation is chosen to be left-to-right and call-by-value, after Standard ML; it can also be shown to be deterministic and terminating [25, Theorem 2.4].

As an example of evaluation, consider the judgement

⊢ (λx:ν.(x = x))(νn.n) ⇓_{o} (n)true .

First the argument νn.n (or new) is evaluated, returning a fresh name bound to n. This is in turn bound to the variable x, and the body of the function compares this name to itself, giving the result true. Compare this with

⊢ (νn′.λx:ν.(x = n′))(νn.n) ⇓_{o} (n′, n)false .

Here the evaluation of the function itself creates a fresh name, bound to n′; the argument provides another fresh name, and the comparison then returns false.

Repeated evaluation of a name abstraction will give different fresh names. Thus the two expressions

νn.λx:o.n and λx:o.νn.n

behave differently: the first evaluates to the function λx:o.n, with every subsequent application returning the private name bound to n; while the second gives a different fresh name as result each time it is applied. The expressions are distinguished by the program

(λf : o → ν . (ftrue = ftrue)) ⟨⟨−⟩⟩

which evaluates to true or false according to how the hole ⟨⟨−⟩⟩ is filled.

This leads us to the notion of program context. A formal definition is given in [25, §2.4]; here we simply note that the form P ⟨⟨−⟩⟩ represents a program P with some number of holes ⟨⟨−⟩⟩, and in P ⟨⟨(x⃗)M⟩⟩ these are filled by an expression M whose free variables are in the list x⃗. There is an arrangement to capture these free variables, and the completed program is a closed expression of boolean type.

Definition 1 (Contextual Equivalence). If M_{1}, M_{2} ∈ Exp_{σ}(s, Γ) then we say that they are contextually equivalent, written

s, Γ ⊢ M_{1} ≈_{σ} M_{2}

if for all closing program contexts P ⟨⟨−⟩⟩ and boolean values b ∈ {true, false},

( ∃s_{1} . s ⊢ P ⟨⟨(x⃗)M_{1}⟩⟩ ⇓_{o} (s_{1})b) ⟺ ( ∃s_{2} . s ⊢ P ⟨⟨(x⃗)M_{2}⟩⟩ ⇓_{o} (s_{2})b).

That is, P ⟨⟨−⟩⟩ always evaluates to the same boolean value, whether the hole is filled by M_{1} or M_{2}. If both s and Γ are empty then we write simply M_{1} ≈_{σ} M_{2}.

This is in many ways the right and proper notion of equivalence between nu-calculus expressions. However the the quantification over all programs makes it inconvenient to demonstrate directly; as discussed in the introduction, the purpose of this paper is to present simple methods for reasoning about contextual equivalence without the need to consider contexts or even evaluation.

Examples.

Up to contextual equivalence, unused names are irrelevant, as is the order in which names are generated:

s, Γ ⊢ νn.M ≈_{σ} M  n ∉ fn(M)  (1)
s, Γ ⊢ νn.νn′.M ≈_{σ} νn′.νn.M .  (2)

Evaluation respects contextual equivalence:

s ⊢ M ⇓_{σ} (s′)C ⟹ s ⊢ M ≈_{σ} νs′.C  (3)

where νs′.C abbreviates multiple name abstractions. Numerous equivalences familiar from the call-by-value lambda-calculus hold, such as Plotkin’s β_{v}- equivalence [23]: if C ∈ Can_{σ}(s, Γ) and M ∈ Exp_{σ′}(s, Γ ⊕ {x : σ}) then

s, Γ ⊢ (λx:σ.M)C ≈_{σ′} M[C/x].  (4)

Names can be used to detect that general β-equivalence fails, as with

(λx:ν.x = x)new ≉_{o} (new = new)  (5)

which evaluate to true and false respectively. More interestingly, distinct expressions may be contextually equivalent if they differ only in their use of ‘private’ names:

νn.λx:ν.(x = n) ≈_{ν→o} λx:ν.false .  (6)

Here the right-hand expression is the function that always returns false; while the left-hand expression evaluates to a function with a persistent local name n, that it compares against any name supplied as an argument. Although these function bodies are quite different, no external context can supply the private name bound to n that would distinguish between them; hence the original expressions are in fact contextually equivalent.

A range of further examples can be found in earlier work on the nucalculus [21, 22, 25, 26].

3 Operational Reasoning

This section describes two operational techniques for demonstrating contextual equivalences in the nu-calculus. Applicative equivalence captures much of the general behaviour of higher-order functions and their evaluation, while the more sophisticated operational logical relations highlight the particular properties of name privacy and visibility. Both are discussed in more detail in [21] and [25], which also give proofs of the results below.

Definition 2 (Applicative Equivalence). We define a pair of relations s ⊢ C_{1} ∼_{σ}^{can} C_{2} for C_{1}, C_{2} ∈ Can_{σ}(s) and s ⊢ M_{1} ∼_{σ}^{exp} M_{2} for M_{1}, M_{2} ∈ Exp_{σ}(s) inductively over the structure of the type σ, according to:

s ⊢ b_{1} ∼_{o}^{can} b_{2} ⟺ b_{1} = b_{2}
s ⊢ n_{1} ∼_{ν}^{can} n_{2} ⟺ n_{1} = n_{2}
s ⊢ λx:σ.M_{1} ∼_{σ→σ′}^{can} λx:σ.M_{2} ⟺ \begin{matrix}∀s′, C ∈ Can_{σ}(s ⊕ s′) . \\ s ⊕ s′ ⊢ M_{1}[C/x] ∼_{σ′}^{exp} M_{2}[C/x] \end{matrix}

s ⊢ M_{1} ∼_{σ}^{exp} M_{2} ⟺ ∃s_{1}, s_{2}, C_{1} ∈ Can_{σ}(s ⊕ s_{1}), C_{2} ∈ Can_{σ}(s ⊕ s_{2}) . s ⊢ M_{1} ⇓_{σ} (s_{1})C_{1} & s ⊢ M_{2} ⇓_{σ} (s_{2})C_{2} & s ⊕ (s_{1} ∪ s_{2}) ⊢ C_{1} ∼_{σ}^{can} C_{2}.

The intuition here is that functions are equivalent if they give equivalent results at possible arguments; while expressions in general are equivalent if they evaluate to equivalent canonical forms.

It is immediate that ∼_{σ}^{exp} coincides with ∼_{σ}^{can} on canonical forms; we write them indiscriminately as ∼_{σ} and call the relation applicative equivalence.^{2} We can extend the relation to open expressions: if M_{1}, M_{2} ∈ Exp_{σ}(s, Γ) then we define

s, Γ ⊢ M_{1} ∼_{σ} M_{2} ⟺ \begin{matrix}∀s′, C_{i} ∈ Can_{σ_{i}}(s ⊕ s′) i = 1, …, n . \\ s ⊕ s′ ⊢ M_{1}[C⃗/x⃗] ∼_{σ} M_{2}[C⃗/x⃗] \end{matrix}

where Γ = {x_{1} : σ_{1}, …, x_{n} : σ_{n}}.

Applicative equivalence is based on similar ‘bisimulation’ relations of Abramsky [1] and Howe [7] for untyped lambda-calculus, and Gordon [5] for typed lambda-calculus. It is well behaved and suffices to prove contextual equivalence:

Theorem 3. Applicative equivalence is an equivalence, a congruence, and implies contextual equivalence.

The proof of this centres on the demonstration that applicative equivalence is a congruence, i.e. it is preserved by all the rules for forming expressions of the nu-calculus. That it implies contextual equivalence follows from this without difficulty; details are in [25, §2.7].

Applicative equivalence verifies examples (1)–(4) above, and numerous others: a range of contextual equivalences familiar from the standard typed lambda-calculus, and all others that make straightforward use of names. What it cannot capture is the notion of privacy that lies behind example (6); where equivalence relies on a particular name remaining secret.

To address the distinction between private and public uses of names, we introduce the idea of a span between name sets. A span R : s_{1} ⇌ s_{2} is an injective partial map from s_{1} to s_{2}; this is equivalent to a pair of injections s_{1} ↢ R ↣ s_{2}, or a relation such that

(n_{1}, n_{2}) ∈ R & (n′_{1}, n′_{2}) ∈ R ⟹ (n_{1} = n′_{1}) ⟺ (n_{2} = n′_{2}) for n_{1}, n′_{1} ∈ s_{1} and n_{2}, n′_{2} ∈ s_{2}. The idea is that for any span R the bijection between dom(R) ⊆ s_{1} and cod(R) ⊆ s_{2} represents matching use of ‘visible’ names, while the remaining elements not in the graph of R are ‘unseen’ names. The identity relation id_{s} : s ⇌ s is clearly a span; and if R : s_{1} ⇌ s_{2} and R′ : s′_{1} ⇌ s′_{2} are spans on distinct name sets, then their disjoint union R ⊕ R′ : s_{1} ⊕ s′_{1} ⇌ s_{2} ⊕ s′_{2} is also a span. Starting from spans, we now build up a collection of relations between expressions of higher types.

2This is a different relation to the applicative equivalence of [21, Definition 13] and [22, Definition 3.4] which (rather unfortunately) turns out not to be an equivalence at all.

Definition 4 (Logical Relations). If R : s_{1} ⇌ s_{2} is a span then we define relations

R_{σ}^{can} ⊆ Can_{σ}(s_{1}) × Can_{σ}(s_{2})
R_{σ}^{exp} ⊆ Exp_{σ}(s_{1}) × Exp_{σ}(s_{2})

by induction over the structure of the type σ, according to:

b_{1} R_{o}^{can} b_{2} ⟺ b_{1} = b_{2}
n_{1} R_{ν}^{can} n_{2} ⟺ n_{1} R n_{2}
(λx:σ.M_{1}) R_{σ→σ′}^{can} (λx:σ.M_{2}) ⟺
∀R′ : s′_{1} ⇌ s′_{2}, C_{1} ∈ Can_{σ}(s_{1} ⊕ s′_{1}), C_{2} ∈ Can_{σ}(s_{2} ⊕ s′_{2}) .
C_{1} (R ⊕ R′)_{σ}^{can} C_{2} ⟹ M_{1}[C_{1}/x] (R ⊕ R′)_{σ′}^{exp} M_{2}[C_{2}/x]
M_{1} R_{σ}^{exp} M_{2} ⟺
∃R′ : s′_{1} ⇌ s′_{2}, C_{1} ∈ Can_{σ}(s_{1} ⊕ s′_{1}), C_{2} ∈ Can_{σ}(s_{2} ⊕ s′_{2}) .
s_{1} ⊢ M_{1} ⇓_{σ} (s′_{1})C_{1} & s_{2} ⊢ M_{2} ⇓_{σ} (s′_{2})C_{2} & C_{1} (R ⊕ R′)_{σ}^{can} C_{2}.

This definition differs somewhat from that for applicative equivalence. Functions are now related if they take related arguments to related results; and expressions in general are related if some span can be found between their respective local names that will relate their canonical forms.

The operational relations R_{σ}^{can} and R_{σ}^{exp} coincide on canonical forms, and we may write them as R_{σ}^{opn} indiscriminately. We can extend the relations to open expressions: if M_{1} ∈ Exp_{σ}(s_{1}, Γ) and M_{2} ∈ Exp_{σ}(s_{2}, Γ) then define

Γ ⊢ M_{1} R_{σ}^{opn} M_{2} ⟺ ∀R′ : s′_{1} ⇌ s′_{2}, C_{ij} ∈ Can_{σ_{j}}(s_{i} ⊕ s′_{i}) i = 1, 2 j = 1, …, n . ( &_{j=1}^{n} . C_{1j} (R ⊕ R′)_{σ_{j}}^{can} C_{2j}) ⟹ M_{1}[C⃗_{1}/x⃗] (R ⊕ R′)_{σ}^{exp} M_{2}[C⃗_{2}/x⃗]

where Γ = {x_{1} : σ_{1}, …, x_{n} : σ_{n}}.

The intuition is that if Γ ⊢ M_{1} R_{σ}^{opn} M_{2} for some R : s_{1} ⇌ s_{2} then the names in s_{1} and s_{2} related by R are public and must be treated similarly by M_{1} and M_{2}, while those names not mentioned in R are private and must remain so.

Theorem 5. For any expressions M_{1}, M_{2} ∈ Exp_{σ}(s, Γ):

Γ ⊢ M_{1} (id_{s})_{σ}^{opn} M_{2} ⟹ s, Γ ⊢ M_{1} ≈_{σ} M_{2}.

If σ is a ground or first-order type of the nu-calculus and Γ is a set of variables of ground type, then the converse also holds:

s, Γ ⊢ M_{1} ≈_{σ} M_{2} ⟹ Γ ⊢ M_{1} (id_{s})_{σ}^{opn} M_{2}.

Proposition 6. Logical relations subsume applicative equivalence: if s, Γ ⊢ M_{1} ∼_{σ} M_{2} then Γ ⊢ M_{1} (id_{s})_{σ}^{opn} M_{2}.

Thus logical relations can be used to demonstrate contextual equivalence, extending and significantly improving on applicative equivalence. They are not quite sufficient to handle all contextual equivalences [25, §4.6], but they are complete up to first-order functions, and in particular they prove all the examples of Section 2 above.

4 Equational Reasoning

Applicative equivalence is generally much simpler to demonstrate than contextual equivalence, and thus it provides a useful proof technique in itself. However, it is still quite fiddly to apply, and at higher types it involves checking that functions agree on an infinite collection of possible arguments. In this section we present an equational logic that is of similar power but much simpler to use in actual proofs.

Assertions in the logic take the form

s, Γ ⊢ M_{1} =_{σ} M_{2}

for open expressions M_{1}, M_{2} ∈ Exp_{σ}(s, Γ). Valid assertions are derived inductively using the rules of Figure 3. To simplify the presentation we use here a notion of non-binding univalent context U⟨−⟩, given by

U⟨−⟩ ::= ⟨−⟩M | F ⟨−⟩ | N = ⟨−⟩ | ⟨−⟩ = N′
| if ⟨−⟩ then M else M′
| if B then ⟨−⟩ else M′ | if B then M else ⟨−⟩.

Equality:

\overline{s, Γ ⊢ M =_{σ} M} \frac{s, Γ ⊢ M_{1} =_{σ} M_{2}}{s, Γ ⊢ M_{2} =_{σ} M_{1}}  \frac{s, Γ ⊢ M_{1} =_{σ} M_{2} s, Γ ⊢ M_{2} =_{σ} M_{3}}{s, Γ ⊢ M_{1} =_{σ} M_{3}}

Congruence:

\frac{s, Γ ⊢ M_{1} =_{σ} M_{2}}{s, Γ ⊢ U⟨M_{1}⟩ =_{σ′} U⟨M_{2}⟩}  \frac{s, Γ ⊕ \{x : σ\} ⊢ M_{1} =_{σ′} M_{2}}{s, Γ ⊢ λx:σ.M_{1} =_{σ→σ′} λx:σ.M_{2}}

Functions:

β_{v} \overline{s, Γ ⊢ (λx:σ.M)C =_{σ′} M[C/x]} C canonical

Booleans: s, Γ ⊢ (if true then M else M′) =_{σ} M s, Γ ⊢ (if false then M else M′) =_{σ} M′

\frac{s, Γ ⊢ M_{1}[true/b] =_{σ} M_{2}[true/b] s, Γ ⊢ M_{1}[false/b] =_{σ} M_{2}[false/b]}{s, Γ ⊕ \{b : o\} ⊢ M_{1} =_{σ} M_{2}}

Names:

\overline{s, Γ ⊢ (n = n) =_{o} true} (n ∈ s) \overline{s, Γ ⊢ (n = n′) =_{o} false} (n, n′ ∈ s distinct)

\frac{s, Γ ⊢ M_{1}[n/x] =_{σ} M_{2}[n/x] each n ∈ s s ⊕ \{n′\}, Γ ⊢M_{1}[n′/x] =_{σ} M_{2}[n′/x] some fresh n′}{s, Γ ⊕ \{x : ν\} ⊢ M_{1} =_{σ} M_{2}}

New names:

\overline{s, Γ ⊢ M =_{σ} νn.M}  \overline{s, Γ ⊢ νn.νn′.M =_{σ} νn′.νn.M}
\frac{s ⊕ \{n\}, Γ ⊢ M_{1} =_{σ} M_{2}}{s, Γ ⊢ νn.M_{1} =_{σ} νn.M_{2}}  \overline{s, Γ ⊢ U⟨νn.M⟩ =_{σ} νn.U⟨M⟩}(n ∉ fn(U⟨−⟩))

Figure 3: Rules for deriving equational assertions.

Thus M is always an immediate subterm of U⟨M⟩, though it may not be the first to be evaluated. This abbreviation appears in the rules for congruence and new names.

The interesting rules of the logic are those concerned with names and name creation. Two expressions with a free variable of type ν are equal if they are equal after instantiation with any existing name, and with a single representative fresh one. Name abstractions νn.(−) can be moved past each other, and through contexts U⟨−⟩, providing that name capture is avoided.

There is no η-rule given for functions; the general rule is not true, and the more restrictive

s, Γ ⊢ C =_{σ→σ′} λx:σ.Cx canonical C ≡ λy:σ.M

follows from the β_{v}-rule, using the fact that the variable ‘x’ counts as a value. Other rules are simplified because evaluation in the nu-calculus is terminating; compare this for example with Riecke’s axiomatisation of callby-value PCF [24].

Proposition 7. This equational theory respects evaluation:

s ⊢ M ⇓_{σ} (s′)C ⟹ s ⊢ M =_{σ} νs′.C .

Proof. It is not hard to demonstrate, using the equational theory, that every rule for evaluation in Figure 2 preserves the property given.

Theorem 8 (Soundness and Completeness). Equational reasoning is sufficient to prove applicative equivalence, and hence also contextual equivalence:

s, Γ ⊢ M_{1} =_{σ} M_{2} ⟹ s, Γ ⊢ M_{1} ∼_{σ} M_{2}
s, Γ ⊢ M_{1} =_{σ} M_{2} ⟹ s, Γ ⊢ M_{1} ≈_{σ} M_{2}.

Moreover, it corresponds exactly to applicative equivalence at first-order types, and to contextual equivalence at ground types:

s, Γ ⊢ M_{1} ∼_{σ} M_{2} ⟹ s, Γ ⊢ M_{1} =_{σ} M_{2}  σ first-order, ground Γ
s ⊢ M_{1} ≈_{σ} M_{2} ⟹  s ⊢ M_{1} =_{σ} M_{2}  σ ∈ {o, ν}.

Proof. Soundness follows from the fact that every rule of Figure 3 for =_{σ} also holds for ∼_{σ}. The converse results on completeness are tedious to prove but not especially difficult; however correct use of the rules for introducing free variables of ground type is important for handling first-order functions.

At higher types applicative equivalence is in principle more powerful than our equational reasoning. However this advantage is illusory: the only way to demonstrate it is to use some more sophisticated technique (such as logical relations) to show that particular functions cannot be expressed in the nucalculus. In practice, the equational logic is much more direct and convenient for reasoning about higher-order functions.

The sample contextual equivalences (1)–(4) from Section 2 are all confirmed immediately by the equational theory. As a slightly more complex example, we prove β-equivalence for univalent function bodies:

s ⊢ (λx:σ.U⟨x⟩)M ≈_{σ′} U⟨M⟩ x ∉ fv(U⟨−⟩).  (7)

By termination and Proposition 7, we have that necessarily s ⊢ M =_{σ} νs′.C for some names s′ and canonical form C. Thus we may reason as follows:

s ⊢ (λx:σ.U⟨x⟩)M = (λx:σ.U⟨x⟩)(νs′.C) congruence
= νs′.((λx:σ.U⟨x⟩)C) pass names through application
= νs′.U⟨C⟩  β_{v}
= U⟨νs′.C⟩  pass names through U⟨−⟩
= U⟨M⟩  congruence.

This is a truly higher-order result: it matters not at all what is the order of the final type σ′.

5 Relational Reasoning

The equational logic presented above is fairly simple, and powerful in that it allows correct reasoning in the presence of an unusual language feature. However it is unable to distinguish between private and public names, and thus cannot prove example (6) of Section 2. The same limitation in the operational technique of applicative equivalence is addressed by a move to logical relations; in this section we introduce a correspondingly refined scheme for relational reasoning about the nu-calculus. As with the equational theory, the aim is to provide all the useful power of operational logical relations in a more accessible form.

Assertions now take the form

Γ ⊢ M_{1} R_{σ} M_{2}

where R : s_{1} ⇌ s_{2} is a span such that M_{1} ∈ Exp_{σ}(s_{1}, Γ) and M_{2} ∈ Exp_{σ}(s_{2}, Γ). To write such assertions, we first need an explicit language to describe spans between sets of names. We build this up using disjoint sum R ⊕ R′ : s_{1} ⊕ s′_{1} ⇌ s_{2} ⊕ s′_{2} over the following basic spans:

\overrightarrow{n} : ∅ ⇌ \{n\}  \overleftarrow{n} : \{n\} ⇌ ∅
∅ : ∅ ⇌ ∅  n_{1} n_{2} : {n_{1}} ⇌ {n_{2}} nonempty.

In particular, we shall use the derived span:

n̂ = n n : {n} ⇌ {n} nonempty.

It is clear that this language is enough to express all finite spans.

The rules for deriving relational assertions are given in Figure 4. The first of these integrates equational results into the logic, so that existing equational reasoning can be reused and we need only consider spans when absolutely necessary. The succeeding rules for congruence and booleans are straightforward, and as before the interesting rules are those concerning names.

To introduce a free variable of type ν requires checking its instantiation with all related pairs of names, and one representative fresh name. This is a weaker constraint than the corresponding rule in the equational logic, where every current name had to be considered; and it is precisely this difference that makes relational reasoning more powerful.

The final three rules handle the name creation operator νn.(−), and capture the notion that local names may be private or public. In combination with the equational rules for new names, they are equivalent to the following general rule:

\frac{Γ ⊢ M_{1} (R ⊕ S)_{σ} M_{2}}{Γ ⊢ (νs_{1}.M_{1}) R_{σ} (νs_{2}.M_{2})} S : s_{1} ⇌ s_{2}.

To apply such rules successfully requires some insight into how an expression uses its local names; which if any are ever revealed to a surrounding program.

Theorem 9 (Soundness). Relational reasoning is sufficient to prove the corresponding operational relations:

Γ ⊢ M_{1} R_{σ} M_{2} ⟹ Γ ⊢ M_{1} R_{σ}^{opn} M_{2} .

By Theorem 5, these in turn can be used to demonstrate contextual equivalence:

Γ ⊢ M_{1} (id_{s})_{σ} M_{2} ⟹ s, Γ ⊢ M_{1} ≈_{σ} M_{2} .

Equational Reasoning:

\frac{Γ ⊢ M_{1} =_{σ} M_{2} Γ ⊢ M_{2} R_{σ} M_{3} Γ ⊢ M_{3} =_{σ} M_{4}}{Γ ⊢ M_{1} R_{σ} M_{4}}

Congruence:

\overline{Γ ⊢ x R_{σ} x} (x : σ ∈ Γ)

Γ ⊢ true R_{o} true

\frac{Γ ⊢ F_{1} R_{σ→σ′} F_{2} Γ ⊢ M_{1} R_{σ} M_{2}}{Γ ⊢ (F_{1}M_{1}) R_{σ′} (F_{2}M_{2})}

Γ ⊢ false R_{o} false
\frac{Γ ⊕ \{x : σ\} ⊢ M_{1} R_{σ′} M_{2}}{Γ ⊢ (λx:σ.M_{1}) R_{σ→σ′} (λx:σ.M_{2})}  \frac{Γ ⊢ N_{1} R_{ν} N_{2} Γ ⊢ N′_{1} R_{ν} N′_{2}}{Γ ⊢ (N_{1} = N′_{1}) R_{o} (N_{2} = N′_{2})}

\frac{Γ ⊢ B_{1} R_{o} B_{2} Γ ⊢ M_{1} R_{σ} M_{2} Γ ⊢ M′_{1} R_{σ} M′_{2}}{Γ ⊢ (if B_{1} then M_{1} else M′_{1}) R_{σ} (if B_{2} then M_{2} else M′_{2})}

Booleans:

\frac{Γ ⊢ (M_{1}[true/b]) R_{σ} (M_{2}[true/b]) Γ ⊢ (M_{1}[false/b]) R_{σ} (M_{2}[false/b])}{Γ ⊕ \{b : o\} ⊢ M_{1} R_{σ} M_{2}}

Names:

\frac{\overline{Γ ⊢ n_{1} R_{ν} n_{2}} ( (n_{1}, n_{2}) ∈ R) Γ ⊢ (M_{1}[n/x]) (R ⊕ n̂)_{σ} (M_{2}[n/x]) some fresh n Γ ⊢ (M_{1}[n_{1}/x]) R_{σ} (M_{2}[n_{2}/x]) each (n_{1}, n_{2}) ∈ R}{Γ ⊕ \{x : ν\} ⊢ M_{1} R_{σ} M_{2}}

Name creation:

\frac{Γ ⊢ M_{1} (R ⊕ \overleftarrow{n_{1}})_{σ} M_{2}}{Γ ⊢ (νn_{1}.M_{1}) R_{σ} M_{2}} \frac{Γ ⊢ M_{1} (R ⊕ \overrightarrow{n_{2}})_{σ} M_{2}}{Γ ⊢ M_{1} R_{σ} (νn_{2}.M_{2})} \frac{Γ ⊢ M_{1} (R ⊕ n_{1} n_{2})_{σ} M_{2}}{Γ ⊢ (νn_{1}.M_{1}) R_{σ} (νn_{2}.M_{2})}

Figure 4: Rules for deriving relational assertions.

Proof. We can show that the operational logical relations R_{σ}^{opn} satisfy all the rules of Figure 4; this in turn depends on Theorem 8, that provable equality =_{σ} implies applicative equivalence ∼_{σ}.

Theorem 10 (Completeness). Relational reasoning corresponds exactly to operational logical relations up to first-order types:

Γ ⊢ M_{1} R_{σ}^{opn} M_{2} ⟹ Γ ⊢ M_{1} R_{σ} M_{2} σ first-order, ground Γ.

By Theorem 5, the same result holds for contextual equivalence:

s, Γ ⊢ M_{1} ≈_{σ} M_{2} ⟹ Γ ⊢ M_{1} (id_{s})_{σ} M_{2} σ first-order, ground Γ.

Proof. By induction on the size of Γ and structure of σ; essentially, we work through the defining clause for logical relations (Definition 4). It is significant here that evaluation is respected by the equational logic (Proposition 7), which is in turn incorporated into the relational theory.

Thus relational reasoning provides a further practical method for reasoning about contextual equivalence. We even have that it can prove all contextual equivalences between expressions of first-order type, thanks to the corresponding (hard) result for operational logical relations. In particular we obtain a demonstration of the final example (6) from Section 2: the crucial closing steps are

x : ν ⊢ (x = n) (\overleftarrow{n})_{o} false
⊢ (λx:ν.(x = n)) (\overleftarrow{n})_{ν→o} (λx:ν.false)
⊢ (νn.λx:ν.(x = n)) ∅_{ν→o} (λx:ν.false)

from which we deduce

νn.λx:ν.(x = n) ≈_{ν→o} λx:ν.false

as required. The span (\overleftarrow{n}) : \{n\} ⇌ ∅ used here captures our intuition that the name bound to n on the left hand side is private, never revealed, and need not be matched in the right hand expression.

6 Conclusions and Further Work

We have looked at the nu-calculus, a language of names and higher-order functions, designed to expose the effect of generativity on program behaviour. Building on operational techniques of applicative equivalence and logical relations, we have derived schemes for equational and relational reasoning; where a collection of inductive rules allow for straightforward proofs of contextual equivalence. We have proved that this approach successfully captures the distinction between private and public names, and is complete up to first-order function types.

One direction for future work is to extend the language from names to the dynamically allocated references of Standard ML, storage cells that allow imperative update and retrieval. For integer references, appropriate denotational and operational techniques are already available [19, 25]. These use relations between sets of states to indicate how equivalent expressions may make different use of local storage cells. The idea then would be to make a similar step in the logic, from name relations to these state relations.

The question of completeness remains open: can these methods be enhanced to prove all contextual equivalences? The operational method of ‘predicated logical relations’ [25, §4.6] does take things a little further, with an even finer analysis of name use; however the theoretical effort involved seems at present to outweigh the practical returns.

Separately from this, it should not be hard to implement the existing relational logic within a generic theorem prover such as Isabelle [18], or even directly in a logic programming language like Prolog. The only difficulty for proof search lies in the choice of relation between local name sets. Human guidance is one solution here, but even a brute force approach would work as there are only finitely many spans R : s_{1} ⇌ s_{2} between any two given name sets. Note that we are not concerned here with an implementation of the proof that the reasoning system itself is correct (Theorem 9); what might benefit from machine assistance is the demonstration that two particular expressions are id_{s}-related, and hence contextually equivalent.

References

[1] S. Abramsky. The lazy lambda calculus. In Research Topics in Functional Programming, pages 65–117. Addison Wesley, 1990.

[2] M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103:235– 271, 1992. Also published as Technical Report 100-89, Rice University.

[3] A. Gordon and A. Pitts, editors. Higher Order Operational Techniques in Semantics. Cambridge University Press, 1997. To appear.

[4] A. D. Gordon. Functional Programming and Input/Output. Cambridge University Press, September 1994.

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

[6] F. Honsell, I. A. Mason, S. Smith, and C. Talcott. A variable typed logic of effects. Information and Computation, 119(1):55–90, May 1995.

[7] D. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2):103–112, February 1996.

[8] I. A. Mason. The Semantics of Destructive Lisp. PhD thesis, Stanford University, 1986. Also published as CSLI Lecture Notes Number 5, Center for the Study of Language and Information, Stanford University.

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

[10] I. A. Mason and C. Talcott. Inferring the equivalence of functional programs that mutate data. Theoretical Computer Science, 105:167– 215, 1992.

[11] I. A. Mason and C. L. Talcott. References, local variables and operational reasoning. In Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pages 186–197. IEEE Computer Society Press, 1992.

[12] R. Milner. Fully abstract models of typed λ-calculi. Theoretical Computer Science, 4:1–22, 1977.

[13] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts I and II. Information and Computation, 100:1–77, 1992.

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

[15] E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, July 1991.

[16] E. Moggi. A general semantics for evaluation logic. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1994.

[17] E. Moggi. Representing program logics in evaluation logic. Unpublished manuscript, available electronically, 1994.

[18] L. C. Paulson. Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science 828. Springer-Verlag, 1994.

[19] A. Pitts and I. Stark. Operational reasoning for functions with local state. In Gordon and Pitts [3]. To appear.

[20] A. M. Pitts. Evaluation logic. In IVth Higher Order Workshop, Banff 1990, pages 162–189. Springer-Verlag, 1991. Also published as Technical Report 198, University of Cambridge Computer Laboratory.

[21] A. M. Pitts and I. Stark. Observable properties of higher order functions that dynamically create local names, or: What’s new? In Mathematical Foundations of Computer Science: Proceedings of the 18th International Symposium, Lecture Notes in Computer Science 711, pages 122–141. Springer-Verlag, 1993.

[22] A. M. Pitts and I. Stark. On the observable properties of higher order functions that dynamically create local names (preliminary report). In Proceedings of the 1993 ACM SIGPLAN Workshop on State in Programming Languages, Yale University Department of Computer Science, Research Report YALEU/DCS/RR-968, pages 31–45, 1993.

[23] G. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.

[24] J. G. Riecke. A complete and decidable proof system for call-by-value equalities. In Automata, Languages and Programming: Proceedings of the 17th International Colloquium, Lecture Notes in Computer Science 443, pages 20–31. Springer-Verlag, 1990.

[25] I. Stark. Names and Higher-Order Functions. PhD thesis, University of Cambridge, December 1994. Also published as Technical Report 363, University of Cambridge Computer Laboratory.

[26] I. Stark. Categorical models for local names. Lisp and Symbolic Computation, 9(1):77–107, February 1996.

[27] C. Talcott. Reasoning about functions with effects. In Gordon and Pitts [3]. To appear.

Recent Publications in the BRICS Report Series

RS-96-31 Ian Stark. Names, Equations, Relations: Practical Ways to Reason about ‘new’. September 1996. ii+22 pp.

RS-96-30 Arne Andersson, Peter Bro Miltersen, and Mikkel Thorup. Fusion Trees can be Implemented with AC^{0} Instructions only. September 1996. 8 pp.

RS-96-29 Lars Arge. The I/O-Complexity of Ordered Binary-Decision Diagram Manipulation. August 1996. 35 pp. An extended abstract version appears in Staples, Eades, Kato, and Moffat, editors, Algorithms and Computation: 6th International Symposium, ISAAC ’95 Proceedings, LNCS 1004, 1995, pages 82�91.

RS-96-28 Lars Arge. The Buffer Tree: A New Technique for Optimal I/O Algorithms. August 1996. 34 pp. This report is a revised and extended version of the BRICS Report RS-94-16. An extended abstract appears in Akl, Dehne, Sack, and Santoro, editors, Algorithms and Data Structures: 4th Workshop, WADS ’95 Proceedings, LNCS 955, 1995, pages 334�345.

RS-96-27 Devdatt Dubhashi, Volker Priebe, and Desh Ranjan. Negative Dependence Through the FKG Inequality. July 1996. 15 pp.

RS-96-26 Nils Klarlund and Theis Rauhe. BDD Algortihms and Cache Misses. July 1996. 15 pp.

RS-96-25 Devdatt Dubhashi and Desh Ranjan. Balls and Bins: A Study in Negative Dependence. July 1996. 27 pp.

RS-96-24 Henrik Ejersbo Jensen, Kim G. Larsen, and Arne Skou. Modelling and Analysis of a Collision Avoidance Protocol using SPIN and UPPAAL. July 1996. 20 pp. Presented at DIMACS Workshop SPIN96 � 2nd International SPIN Veri�cation Workshop on Algorithms, Applications, Tool Use, Theory (Rutgers University, New Jersey, USA, August 5,