Constructive data refinement in typed lambda calculus

Furio Honsell^{1,2}, John Longley^{1}, Donald Sannella^{1}, and Andrzej Tarlecki^{3,4}

1 Laboratory for Foundations of Computer Science, University of Edinburgh 2 Dipartimento di Matematica e Informatica, Università di Udine 3 Institute of Informatics, Warsaw University 4 Institute of Computer Science, Polish Academy of Sciences

Abstract. A new treatment of data refinement in typed lambda calculus is proposed, phrased in terms of pre-logical relations [HS99] rather than logical relations, and incorporating a constructive element. Constructive data refinement is shown to have desirable properties, and a substantial example of refinement is presented.

1 Introduction

One of the activities involved in developing programs from specifications is the transformation of “abstract programs” involving types of data that are not normally available as primitive in programming languages (graphs, sets, etc.) into “concrete programs” in which a representation of these in terms of simpler types of data is provided. Apart from the change to data representation, such data refinement should have no effect on the results computed by the program: the concrete program should be equivalent to the abstract program in the sense that all computational observations should return the same results in both cases.

The standard treatment of data refinement in the context of typed lambda calculus, originating with Reynolds in [Rey81,Rey83] but described most clearly in [Ten94], cf. Sect. 8.5 of [Mit96], uses logical relations to prove the correctness of refinements. This work has its roots in [Hoa72], which proposes that the correctness of the concrete program be verified using an invariant on the domain of concrete values together with a function mapping concrete values (that satisfy the invariant) to abstract values. In algebraic terms, what is required is a homomorphism from a subalgebra of the concrete algebra to the abstract algebra. A strictly more general method is to take a homomorphic relation (a so-called correspondence [Sch90], cf. [Mil71]) in place of a homomorphism from a subalgebra. Logical relations extend these ideas to deal with higher-order functions.

Proof method ([Ten94 ]). Let A and B be Σ-Henkin models and let OBS, the observable types, be a subset of Types(Σ). To show that B is a refinement of A, find a logical relation R over A and B such that R^{σ} is the identity relation for each σ ∈ OBS. We then say that B is a logical refinement of A and write A ⇝ B, or A ^{R} ⇝ B when we want to make R explicit.

It is well-known that the composition of two logical relations is not in general a logical relation. It follows that, given logical refinements A ^{R} ⇝ B and B ^{S} ⇝ C, the composition S ∘ R cannot in general be used as a witness for the composed refinement A ⇝ C. (In fact, the problem is more serious than it appears at first: sometimes there is no witness for A ⇝ C at all, see Sect. 3.) This is at odds with the stepwise nature of refinement, and the transitivity of the underlying concept of refinement expressed in terms of observational equivalence. It is one source of examples demonstrating the incompleteness of the above proof method; there are other examples that do not involve composition of refinement steps, see e.g. Sect. 5. The proof method is complete in the absence of higher-order term constants [Mit96].

In [HS99], a weakening of the notion of logical relations called pre-logical relations was studied; cf. [PPST00]. Pre-logical relations are closed under composition; in fact, they are the minimal weakening of logical relations with this property. They completely characterize observational equivalence of Henkin models, without restriction to first-order signatures. Replacing logical relations with prelogical relations in the above gives a notion of pre-logical refinement which is in pleasing harmony with stepwise refinement. Indeed, it is equivalent to the underlying concept of refinement, i.e. sound and complete as a proof method.

This is an improvement but pre-logical refinement still does not entirely accord with our intuition concerning data refinement and stepwise development of programs. For one thing, like logical refinement it is a symmetric relation. We will consider a more elaborate notion of data refinement, called constructive pre-logical refinement (Sect. 4). This is a relation between specifications, written SP ^{OBS}_{δ} ∼∼∼∼∼ > SP′, which incorporates a construction in the form of a derived signature morphism δ taking models of SP′ to Henkin models over the signature of SP. Derived signature morphisms define the types and constants in one signature by giving terms over another signature, and this corresponds directly to the code in an ML functor body. It follows that the result of a complete chain of constructive refinements is a Henkin model, corresponding to a modular ML program, which is a solution to the original programming task. We give an extended example of constructive data refinement in the context of exact real number computation, and show that it is not a (constructive) logical refinement (Sect. 5).

Some recent accounts of data refinement in typed lambda calculus have employed variants of logical relations that are related to pre-logical relations, for instance [KOPTT97]. Our inclusion of a constructive element in the relation is new, and our example appears to be the first non-trivial concrete example of data refinement in the lambda calculus literature.

The idea of constructive pre-logical refinement comes from the world of algebraic specifications, where it is called abstractor implementation [ST88] or behavioural implementation [ST97]. This paper is an attempt to explain this idea in lambda calculus terms, since it is a substantial improvement on current accounts of data refinement in that context. One novelty with respect to existing work on abstractor implementations concerns the connection with pre-logical relations, which generalizes Schoett’s characterization of observational equivalence via correspondences and makes a bridge with work on data refinement in lambda calculus based on logical relations. Another novelty concerns the use of derived signature morphisms in the typed lambda calculus for defining constructions. In order for abstractor implementations to compose, constructions are required to preserve observational equivalence, a property known as stability [Sch87]. This requirement is normally imposed as an assumption on the language used for defining constructions, which is left unspecified. Here, stability follows easily from the Basic Lemma of pre-logical relations. Finally, the example in Sect. 5 goes considerably beyond the simple examples of refinement of data representation that have been considered previously.

2 Preliminaries: syntax and semantics

For the sake of simplicity of the exposition we restrict attention to λ^{→}, the simply-typed lambda calculus having → as its only type constructor.

Definition 2.1. The set of types over a set B of base types (or type constants) is given by the grammar σ ::= b | σ → σ where b ranges over B. A signature Σ consists of a set B of type constants and a collection C of typed term constants c : σ. Types(Σ) denotes the set of types over B.

In a Σ-context Γ = x_{1}:σ_{1}, …, x_{n}:σ_{n}, we require that x_{i} ≠ x_{j} for all 1 ≤ i < j ≤ n and σ_{i} ∈ Types(Σ) for all 1 ≤ i ≤ n. Σ-terms are given by the grammar M ::= x | c | λx:σ.M | M M where x ranges over variables and c over term constants. The usual typing rules associate each well-formed term M in context Γ with a type σ ∈ Types(Σ), written Γ ⊳ M : σ (or Γ ⊳_{Σ} M : σ when we need to make Σ explicit). If Γ is empty then we write simply M : σ or ⊳_{Σ}M : σ.

Definition 2.2. A Σ-Henkin model A consists of:

– a carrier set [[σ]]^{A} for each σ ∈ Types(Σ);

– a function App_{A}^{σ,τ} : [[σ → τ]]^{A} → [[σ]]^{A} → [[τ]]^{A} for each σ, τ ∈ Types(Σ);

– an element [[c]]^{A} ∈ [[σ]]^{A} for each term constant c : σ in Σ; and

– elements K_{A}^{σ,τ} ∈ [[σ → (τ → σ)]]^{A} and S_{A}^{ρ,σ,τ} ∈ [[(ρ → σ → τ) → (ρ → σ) → ρ → τ]]^{A} for each ρ, σ, τ ∈ Types(Σ)

such that

– K_{A}^{σ,τ} x y = x and S_{A}^{ρ,σ,τ} x y z = (x z)(y z); and

– (extensionality) if App_{A}^{σ,τ} f x = App_{A}^{σ,τ} g x for every x ∈ [[σ]]^{A}, then f = g.

The class of all Σ-Henkin models is denoted Mod(Σ).

Term constants of functional type are interpreted as total functions. Allowing partial functions does not seem to introduce problems, but we have not checked the details. Moreover, the use of Henkin models in this paper is not essential; the definitions and results in [HS99] that we will need later also apply to nonextensional models, for instance combinatory algebras.

A Γ -environment η on a Henkin model A assigns elements of A to variables, with η(x) ∈ [[σ]]^{A} for x : σ in Γ. A Σ-term Γ ⊳ M : σ is interpreted in A under a Γ -environment η in the usual way with λ-abstraction interpreted via translation to combinators, written [[Γ ⊳ M : σ]]_{η}^{A}, and this is an element of [[σ]]^{A}. If M is closed then we write simply [[M : σ]]^{A}.

We can allow terms to contain the fixed-point combinator Y (viewed as a term constant). To interpret such terms in a Henkin model A, we need to additionally require elements Y_{A}^{σ} ∈ [[(σ → σ) → σ]]^{A} for each σ ∈ Types(Σ) such that f (Y_{A}^{σ} f) = Y_{A}^{σ} f. We will assume that this additional structure is present whenever we consider such terms.

Definition 2.3. A logical relation R over Σ-Henkin models A and B is a family of relations {R^{σ} ⊆ [[σ]]^{A} × [[σ]]^{B}}_{σ∈Types(Σ)} such that:

– R^{σ→τ} (f, g) iff ∀a ∈ [[σ]]^{A}.∀b ∈ [[σ]]^{B}.R^{σ}(a, b) ⇒ R^{τ} (App_{A} f a, App_{B} g b).

– R^{σ}([[c]]^{A}, [[c]]^{B}) for every term constant c : σ in Σ.

Definition 2.4. If Γ ⊳_{Σ} M : σ and Γ ⊳_{Σ} M′ : σ then ∀Γ.M =_{σ} M′ is a Σequation. The subscript σ is omitted when it is obvious. A Σ-Henkin model A satisfies a Σ-equation ∀Γ.M =_{σ} M′ if [[Γ ⊳ M : σ]]_{η}^{A} = [[Γ ⊳ M′ : σ]]_{η}^{A} for all Γ -environments η. It is easy to add connectives and quantifiers, giving sentences of predicate logic with equality. A specification SP consists of a signature Σ and a set Φ of Σ-sentences. Then Sig(SP) = Σ, and Mod(SP) (the models of SP) is the class of all Σ-Henkin models satisfying all the sentences in Φ.

3 Data refinement

We begin with an analysis of the failure of composition of logical relations and its impact on composition of logical refinements.

Example 3.1. Let Σ contain two type constants, b and b′, and no term constants. Consider Σ-Henkin models A, B, C which interpret b and b′ as follows, and interpret function types using full set-theoretic function spaces: [[b]]^{A} = {∗} = [[b′]]^{A}; [[b]]^{B} = {∗} and [[b′]]^{B} = {∘, •}; [[b]]^{C} = {∘, •} = [[b′]]^{C}. Let R be the logical relation over A and B induced by R^{b} = {⟨∗, ∗⟩} and R^{b′} = {⟨∗, ∘⟩, ⟨∗, •⟩} and let S be the logical relation over B and C induced by S^{b} = {⟨∗, ∘⟩, ⟨∗, •⟩} and S^{b′} = {⟨∘, ∘⟩, ⟨•, •⟩}. S ∘ R is not a logical relation because it does not relate the identity function in [[b]]^{A} → [[b′]]^{A} to the identity function in [[b]]^{C} → [[b′]]^{C}. The problem is that the only two functions in [[b]]^{B} → [[b′]]^{B} are {∗ ↦ ∘} and {∗ ↦ •}, and S does not relate these to the identity in C. □

This simple example shows that we may have logical refinements A ^{R} ⇝ B and B ^{S} ⇝ C (where we take OBS = ∅ in both cases), where S ∘ R is not a logical relation and so cannot act as witness to A ⇝ C.

One possible solution might be to construct the relations at higher types from the composite relations at base types. This works if Σ contains only first-order term constants (guaranteeing that the restriction to base types lifts to a logical relation) and if OBS contains only base types (guaranteeing that the resulting logical relation is the identity relation for each σ ∈ OBS). The following example shows how this idea fails in the presence of second-order term constants.

Example 3.2. In the previous example, add a type constant bool and a term constant c : (b → b′) → bool to Σ. Let [[bool]]^{A} = [[bool]]^{B} = [[bool]]^{C} = {true, false} and take R^{bool} and S^{bool} to be the identity. In each model, let the interpretation of c take constant functions to true and all other functions to false. The resulting R and S are logical relations. As before, S ∘ R is not a logical relation but now the restriction of S ∘ R to base types cannot be lifted to a logical relation either: this would relate the identity function in [[b]]^{A} → [[b′]]^{A} (which is a constant function) to every function in [[b]]^{C} → [[b′]]^{C}, but then the constant function in A would be related to non-constant functions in C, and so [[c]]^{A} could not be related to [[c]]^{C}, otherwise true would be related to false. □

These two examples show that certain ways of composing the logical relations witnessing A ⇝ B and B ⇝ C do not yield a logical relation witnessing A ⇝ C. Such a witness may exist, however, and in the above example it does. For OBS = ∅, the full relation suffices; for OBS = {bool}, the full relation on b together with the empty relation on b′ and the identity on bool lifts to a logical relation. But if we add constants b1, b2 : b and b1′, b2′ : b′ with [[b1]]^{A} = [[b2]]^{A} = [[b1′]]^{A} = [[b2′]]^{A} = ∗, [[b1]]^{C} = [[b1′]]^{C} = ∘ and [[b2]]^{C} = [[b2′]]^{C} = • then there is no logical relation over A and C which is the identity on bool so A ⇝̸ C for OBS = {bool}. The following proposition summarizes the situation.

Proposition 3.3. A ⇝ B and B ⇝ C does not in general imply A ⇝ C. □

Ultimately, the justification for the definition of logical refinement lies in the notion of observational equivalence, in terms of which the underlying concept of data refinement is formulated.

Definition 3.4. Let A and B be Σ-Henkin models and let OBS ⊆ Types(Σ). Then A is observationally equivalent to B with respect to OBS, written A ≡_{OBS} B, if for any two closed Σ-terms M, N : σ for σ ∈ OBS, [[M : σ]]^{A} = [[N : σ]]^{A} iff [[M : σ]]^{B} = [[N : σ]]^{B}.

It is usual to take OBS to be the “built-in” types for which equality is decidable, for instance bool and/or nat. Then A and B are observationally equivalent iff it is not possible to distinguish between them by performing computational experiments. Note that OBS ⊆ OBS′ implies ≡_{OBS} ⊇ ≡′_{OBS}.

For OBS = {nat}, the connection between logical refinement and observational equivalence is given by Mitchell’s representation independence theorem.

Theorem 3.5 ([Mit96]). Let Σ be a signature that includes a type constant nat, and let A and B be Σ-Henkin models, with [[nat]]^{A} = [[nat]]^{B} = ℕ. If there is a logical relation R over A and B with R^{nat} the identity relation on natural numbers, then A ≡_{{nat}} B. Conversely, if A ≡_{{nat}} B, Σ provides a closed term for each element of ℕ, and Σ contains only first-order term constants, then there is a logical relation R over A and B with R^{nat} the identity relation. □

The restriction to signatures with first-order term constants in the second part of the theorem is necessary, and this is the key to the incompleteness of logical refinements as a proof method and the problem with composability of logical refinements. If A ⇝ B ⇝ C then A ≡_{OBS} B ≡_{OBS} C, and so A ≡_{OBS} C since ≡_{OBS} is an equivalence relation. But then it follows that A ⇝ C only for signatures without higher-order term constants.

An improved version of the above theorem, without the restriction to firstorder signatures, holds if logical relations are replaced by pre-logical relations.

Definition 3.6 ([HS99]). A pre-logical relation R over Σ-Henkin models A and B is a family of relations {R^{σ} ⊆ [[σ]]^{A} × [[σ]]^{B}}_{σ∈Types(Σ)} such that:

– If R^{σ→τ} (f, g) then ∀a ∈ [[σ]]^{A}.∀b ∈ [[σ]]^{B}.R^{σ}(a, b) ⇒ R^{τ} (App_{A} f a, App_{B} g b).

– R^{σ}([[c]]^{A}, [[c]]^{B}) for every term constant c : σ in Σ.

– R(S_{A}^{ρ,σ,τ} , S_{B}^{ρ,σ,τ}) and R(K_{A}^{σ,τ} , K_{B}^{σ,τ}) for all ρ, σ, τ ∈ Types(Σ).

Theorem 3.7 ([HS99]). Let A and B be Σ-Henkin models and let OBS ⊆ Types(Σ). Then A ≡_{OBS} B iff there exists a pre-logical relation over A and B which is a partial injection on OBS. □

This suggests the following. (We switch to a notation that makes the set of observable types explicit.)

Definition 3.8. Let A and B be Σ-Henkin models and OBS ⊆ Types(Σ). Then B is a pre-logical refinement of A, written A ^{OBS} ∼∼∼∼∼ > B, if there is a pre-logical relation R over A and B such that R^{σ} is a partial injection for each σ ∈ OBS.

We phrase this as a definition, rather than as a proof method for the underlying notion of data refinement, in contrast to logical refinements. As a proof method it is sound and complete, and therefore equivalent to this underlying notion.

Pre-logical relations compose [HS99], so pre-logical refinements compose, and this explains why stepwise refinement is sound. Another explanation goes via Theorem 3.7: A ^{OBS} ∼∼∼∼∼ > B ^{OBS} ∼∼∼∼∼ > C ⇒ A ≡_{OBS} B ≡_{OBS} C ⇒ A ≡_{OBS} C ⇒ A ^{OBS} ∼∼∼∼∼ > C. The set of observable types need not be the same in both steps, as the following result spells out.

Proposition 3.9. If A ^{OBS} ∼∼∼∼∼ > B and B ^{OBS′} ∼∼∼∼∼ > C then A ^{OBS} ∼∼∼∼∼ > C provided OBS ⊆ OBS′. □

The definition of observational equivalence may be extended to allow experiments to include the fixed-point combinator by requiring Henkin models to include elements Y_{A}^{σ} ∈ [[(σ → σ) → σ]]^{A} for each σ ∈ Types(Σ) as indicated above. Theorem 3.7 still holds provided pre-logical relations are required to relate Y_{A}^{σ} with Y_{B}^{σ} for all σ.

4 Constructive data refinement

Pre-logical refinement, like logical refinement, is a symmetric relation. This does not fit the intuition that refinement is about going from an abstract, high-level description of a program to a concrete, more detailed description. There are at least two basic defects of the notion of pre-logical refinement of which the symmetry of the relation is merely a symptom.

First, it is a relation between Henkin models. The intuition behind stepwise refinement suggests that it should be rather a relation between descriptions of Henkin models, i.e. between specifications. The original specification of a problem rarely determines a single permissible behaviour: some of the details of the behaviour are normally left open to the implementor. So at this stage one starts with an assortment of models, corresponding to all the possible choices of behaviours. (Some of these will be isomorphic to one another, given a suitable notion of isomorphism, but if the specification permits more than one externallyvisible behaviour then there will be non-isomorphic models.) The final program, on the other hand, corresponds to a single Henkin model. So the refinement process involves not just replacement of abstract data representations by more concrete ones, but also selection between permitted behaviours.

Definition 4.1. Let SP and SP′ be specifications with Σ = Sig(SP) = Sig(SP′) and OBS ⊆ Types(Σ). Then SP′ is a pre-logical refinement of SP, written SP ^{OBS} ∼∼∼∼∼ > SP′, if for any B ∈ Mod(SP′) there is some A ∈ Mod(SP) with a pre-logical relation R over A and B such that R^{σ} is a partial injection for each σ ∈ OBS.

Second, the idea that refinement is a reduction of one as-yet-unsolved problem to another is not explicit. Intuitively, each refinement step reduces the current problem to a smaller problem, such that any solution to the smaller problem gives rise to a solution to the original problem. In pre-logical refinement of specifications, one models this by having the successive specifications accumulate more and more details arising from successive design decisions. Some parts become fully determined, and remain unchanged as a part of the specification until the final program is obtained. The parts that are not yet fully determined correspond to the unsolved parts of the original problem. (To avoid clutter, we omit the OBS decorations in the following diagrams.)

[figure: SP_{0}; ∼∼∼ >; κ_{1}; SP_{1}; ∼∼∼ >; κ_{1}; κ_{2}; SP_{2}; ∼∼∼ > ⋯ ∼∼∼ >; ^{κ^{1} κ_{2} ⋯ κ_{n}•}]

It is much cleaner to separate the finished parts from the specification, proceeding with the development of the unresolved parts only, giving

[figure: SP_{0}; _{κ_{1}} ∼∼∼ >; SP_{1}; _{κ_{2}} ∼∼∼ >; SP_{2}; _{κ_{3}} ∼∼∼ > ⋯ _{κ_{n}} ∼∼∼ >; ^{• SP_{n} = DONE}]

where DONE is a specification having a ready realisation (e.g. a specification of the built-ins of the programming language in use). The finished parts κ_{1}, …, κ_{n} are constructions extending any solution (model) of a reduced problem (specification) to a solution of the previous problem, and so we will refer to this relation as constructive data refinement. The signatures of successive specifications may be different, in contrast to the earlier refinement relations.

Constructive data refinement will be defined below. As constructions we will take “δ-reducts” of Σ′-Henkin models induced by “derived signature morphisms” δ : Σ → Σ′, where Σ and Σ′ are the signatures before and after refinement, respectively. This amounts to giving an interpretation of the type constants and term constants in Σ as types and terms over Σ′.

Definition 4.2. Let Σ and Σ′ be signatures. A derived signature morphism δ : Σ → Σ′ consists of:

– a mapping from base types in Σ to types over Σ′: for every base type b in Σ, δ(b) ∈ Types(Σ′). This induces a mapping (also called δ) from Types(Σ) to Types(Σ′), using δ(σ → τ) = δ(σ) → δ(τ).

– a type-preserving mapping from term constants in Σ to closed terms over Σ′: for every c : σ in Σ, ⊳_{Σ′}δ(c) : δ(σ).

This induces a mapping (also called δ) from terms over Σ to terms over Σ′, using δ(x) = x, δ(λx:σ.M) = λx:δ(σ).δ(M), δ(M M′) = δ(M) δ(M′), and (if we are using the Y combinator) δ(Y) = Y. Composition is obvious.

Proposition 4.3. If δ : Σ → Σ′ and Γ ⊳_{Σ} M : σ then δ(Γ) ⊳_{Σ′} δ(M) : δ(σ) where δ(x_{1}:σ_{1}, …, x_{n}:σ_{n}) = x_{1}:δ(σ_{1}), …, x_{n}:δ(σ_{n}). □

A derived signature morphism corresponds exactly to a functor in ML terminology, or a parameterised program [Gog84]: the functor parameter is a Σ′-Henkin model, and the functor body contains code which defines the components of Σ using the components of Σ′. If the fixed-point combinator is available then this code may involve recursive functions. (Recursively-defined types are not allowed since we are working in λ^{→}, but see Sect. 6.)

The semantics of these programs as functions on Henkin models is given by the notion of δ-reduct.

Definition 4.4. Let δ : Σ → Σ′ and let A′ be a Σ′-Henkin model. The δ-reduct of A′ is the Σ-Henkin model A′|_{δ} defined as follows:

– [[σ]]^{A′|_{δ}} = [[δ(σ)]]^{A′} for each σ ∈ Types(Σ);

– App_{A′|_{δ}}^{σ,τ} = App_{A′}^{δ(σ),δ(τ)} for each σ, τ ∈ Types(Σ);

– [[c]]^{A′|_{δ}} = [[δ(c)]]^{A′} for each term constant c : σ in Σ; and

– K_{A′|_{δ}}^{σ,τ} = K_{A′}^{δ(σ),δ(τ)}, S_{A′|_{δ}}^{ρ,σ,τ} = S_{A′}^{δ(ρ),δ(σ),δ(τ)} and (if we are using the Y combi-

nator) Y_{A′|_{δ}}^{σ} = Y_{A′}^{δ(σ)}, for each ρ, σ, τ ∈ Types(Σ).

Proposition 4.5. [[Γ ⊳_{Σ} M : σ]]_{η}^{A′|_{δ}} = [[δ(Γ) ⊳_{Σ′} δ(M) : δ(σ)]]_{η}^{A′}. □

Σ-Henkin models and pre-logical relations between such models form a category Mod(Σ). The following property is intimately related to the concept of stability in [Sch87].

Proposition 4.6 (Stability). For any δ : Σ → Σ′, the mapping ·|_{δ} extends to a functor ·|_{δ} : Mod(Σ′) → Mod(Σ). If a pre-logical relation R′ in Mod(Σ′) is a partial injection on OBS′ ⊆ Types(Σ′), then R′|_{δ} is a partial injection on δ^{−1}(OBS′). Thus A′ ≡_{OBS}′ B′ implies A′|_{δ} ≡_{OBS} B′|_{δ} for any OBS ⊆ Types(Σ) such that δ(OBS) ⊆ OBS′.

Proof. Take (R|_{δ})^{σ} = R^{δ(σ)}. It follows from the Basic Lemma for pre-logical relations (see [HS99]) that this yields a pre-logical relation. □

Now we are ready to give a formal definition of constructive data refinement.

Definition 4.7. Let SP and SP′ be specifications, δ : Sig(SP) → Sig(SP′) be a derived signature morphism, and let OBS ⊆ Types(Sig(SP)). Then SP′ is a constructive pre-logical refinement of SP via δ, written SP ^{OBS}_{δ} ∼∼∼∼∼ > SP′, if for any B ∈ Mod(SP′) there is some A ∈ Mod(SP) with a pre-logical relation R over A and B|_{δ} such that R^{σ} is a partial injection for each σ ∈ OBS.

It is easy to modify this definition to give a notion of constructive logical refinement, written _{δ}⇝. The correspondence between derived signature morphisms as defined above and ML functors justifies the use of the word “constructive”. In Sect. 5 below we give an example of constructive pre-logical refinement and show that it is not a constructive logical refinement.

Constructive pre-logical refinements compose via the composition of their underlying derived signature morphisms:

Proposition 4.8. If SP ^{OBS}_{δ} ∼∼∼∼∼ > SP′ and SP′ ^{OBS′}_{δ′} ∼∼∼∼∼ > SP′′ then SP ^{OBS}_{δ′ ∘ δ} ∼∼∼∼∼ > SP′′ provided δ(OBS) ⊆ OBS′. □

The required relationship between OBS and OBS′ is just what one would expect: as refinement progresses, the successive specifications become increasingly less abstract and so the number of non-observable types tends to decrease, while the overall task of implementing SP with observable types OBS remains the same.

As suggested above, a chain of constructive refinements is complete when the original problem has been reduced to a specification DONE with a given (implemented) model D:

SP_{0} ^{OBS^{1}}_{δ_{1}} ∼∼∼∼∼ > SP_{1} ^{OBS^{2}}_{δ_{2}} ∼∼∼∼∼ > ⋯ ^{OBS^{n}}_{δ_{n}} ∼∼∼∼∼ > SP_{n} = DONE

Then, by Prop. 4.8, if the condition on OBS_{1}, …, OBS_{n} is satisfied, DONE is a constructive pre-logical refinement of SP_{0} via δ_{n} ∘ ⋯ ∘ δ_{2} ∘ δ_{1} with respect to OBS_{1}: the Henkin model D|_{δ_{n}∘···∘δ_{2}∘δ_{1}} is observationally equivalent to some model of SP_{0} with respect to OBS_{1}. In other words, δ_{n} ∘⋯∘δ_{2} ∘δ_{1} is a program that is a solution to the original programming task.

5 An example from real number computation

We now present an extended example of constructive data refinement in the context of exact real number computation. The point of this example is that the desired refinement can be expressed in terms of pre-logical relations, but not in terms of logical relations.

We will describe a specification SP involving real numbers and some operations on them, and a specification SP′ which provides a means of implementing SP using higher-type functions. We will then present a constructive pre-logical refinement SP ^{OBS}_{δ} ∼∼∼∼∼ > SP′ that captures this implementation; however, we will show that there is no constructive logical refinement SP _{δ}⇝ SP′.

5.1 A specification for real number operations

The specification SP has an underlying signature Σ consisting of the type constants real and bool and the following term constants:

0, 1 : real  sup_{[0,1]} : (real → real) → real
− : real → real  true, false, ⊥ : bool
+, ∗, max : real → real → real  < : real → real → bool

We declare bool (only) to be an observable type. As usual, we treat +, ∗ and < as infixes. One could of course consider richer signatures (e.g. with division), but the signature above has the technical advantage that all the above operations are total functions in the intended models (see below regarding the interpretation of sup_{[0,1]}).

A class of intended models for SP may be given via some logical axioms, as follows. For 0, 1, −, +, ∗, we take the usual axioms for a field; we also add axioms saying that the type real is totally ordered by ≤, where t ≤ u abbreviates the logical formula ∃z:real.u = t + (z ∗ z). For max and sup_{[0,1]}, we add the axioms

∀x, y:real. (x ≤ y ⇒ max x y = y) ∧ (y ≤ x ⇒ max x y = x)
∀f : real → real. (∃z:real. ∀x:real. 0 ≤ x ∧ x ≤ 1 ⇒ f(x) ≤ z) ⇒

(∀z:real. sup_{[0,1]}f ≤ z ⇔ ∀x:real. 0 ≤ x ∧ x ≤ 1 ⇒ f(x) ≤ z)

An important logical consequence of these axioms (which we shall use later) is the formula sup_{[0,1]}(λx:real. 0) = 0.

The language we have defined is surprisingly expressive. For instance, every algebraic real number is definable by a closed term, and so any model for SP must contain a copy of at least the algebraic reals. In fact, the models we have in mind contain all the computable or recursive reals (though not every computable real is definable by a closed term).

The only purpose of including the type bool in SP is to allow us to make observations on real numbers. In general we do not expect to be able to tell when two real numbers are the same, but we can tell when they are different.

It suffices for our purposes to include the order relation < in our signature. The axioms for < are:

∀x, y:real. (¬y ≤ x) ⇒ x < y = true
∀x, y:real. (¬x ≤ y) ⇒ x < y = false
∀x, y:real. x = y ⇒ x < y = ⊥

This completes the definition of SP.

Some brief remarks on models for SP may be helpful. The full set-theoretic type structure over ℝ gives a model of SP, though we need to assign arbitrary values to the interpretation of sup_{[0,1]} on functions f : ℝ → ℝ which are unbounded on [0, 1]. There are also natural models in which the interpretation of real → real is constrained to include only continuous functions (see e.g. [Nor98]).

5.2 A specification for PCF computations

We now present a specification SP′ corresponding to the familiar functional language PCF [Plo77]. A constructive refinement SP ^{OBS}_{δ} ∼∼∼∼∼ > SP′ for OBS = {bool} then amounts to a way of implementing SP in PCF via a “program” δ.

The signature Σ′ for SP′ will consist of the single type constant nat and:

0 : nat  ifzero : nat → nat → nat → nat
succ, pred : nat → nat  Y^{σ} : (σ → σ) → σ  (σ ∈ Types(Σ′))

This is exactly the language for (a version of) PCF. The intention is that nat stands for the lifted natural numbers, with the term ⊥ ≡ Y^{nat}(λz:nat.z) denoting the bottom element. We freely employ syntactic sugar in PCF terms where the meaning is evident.

We now wish to add axioms to ensure that any model for SP′ is a model of PCF in some reasonable sense. We do not know whether all the axioms below are strictly necessary for our purposes, but they correspond to a well-understood class of models of PCF. Let us write t ↓ as an abbreviation for the formula ifzero t 0 0 = 0 (we may read this as “t terminates”). First we have an axiom saying there is only one non-terminating element of type nat:

∀x:nat. ¬(x ↓) ⇔ x = ⊥

For 0 and succ, we take the usual first-order Peano axioms for the terminating elements. For the remaining constants, we take the axioms

pred 0 = 0  ∀x:nat. pred(succ x) = x
∀y, z:nat. ifzero 0 y z = y  ∀x, y, z:nat. ifzero(succ x) y z = z

∀y, z:nat. ifzero ⊥ y z = ⊥

∀f : σ → σ. Y^{σ}f = f(Y^{σ}f)  ∀f : σ → σ, z:σ. z = f z ⇒ Y^{σ}f ⊑_{σ} z

where t ⊑_{σ} u abbreviates ∀P : σ → nat. (P t ↓) ⇒ (P u ↓).

Note that the full set-theoretic type structure over ℕ_{⊥} is not a model, because not every set-theoretic function ℕ_{⊥} → ℕ_{⊥} has a fixed point. However, the usual Scott model based on CPOs (see [Plo77]) and the game models of e.g. [AJM96] do provide models of SP′, as do their recursive analogues. The extensional closed term model of PCF also provides a model (which in fact is isomorphic to the recursive game models).

5.3 A constructive pre-logical refinement

We now describe a constructive refinement from SP to SP′. The basic idea is that we will represent a real number r by an infinite sequence d = d_{0}d_{1}d_{2} … of natural numbers, which in turn is represented by the function f : ℕ_{⊥} → ℕ_{⊥} given by f(i) = d_{i}. (More generally: in any model B of SP′, including non-standard ones, there will be an inclusion from ℕ_{⊥} to [[nat]]^{B}; for simplicity of notation we take ℕ_{⊥} ⊆ [[nat]]^{B}. Then we represent d by any function f ∈ [[nat → nat]]^{B} such that f(i) = d_{i} for all i ∈ ℕ.) Operations on reals are then represented by higher-type operations on such functions. There are many ways to choose a suitable representation, and the differences between them do not matter much. For definiteness, we will work with sequences d such that d_{i} ≤ 2 for all i ≥ 2; such a sequence will represent the real number d_{0} −d_{1} +∑_{i=2}^{∞} 2^{1−i}(d_{i} −1). We will use the meta-notation IsReal(f) to mean that f ∈ [[nat → nat]]^{B} represents a real number in this way, and write Val(f) to denote the real number it represents. Note that there will be many sequences representing any given real number — this is in fact an essential feature of any representation of reals for which even the most basic arithmetical operations are computable. The above choice is essentially a signed binary representation involving infinite sequences of digits −1, 0, 1 (coded in PCF by 0, 1, 2 respectively).

We can make precise the idea of implementing SP in terms of SP′ by means of a derived signature morphism δ : Σ → Σ′. For the basic types, we take

δ(real) = nat → nat, δ(bool) = nat.

Next, for each term constant c : σ of Σ we need to give a term δ(c) : δ(σ) in Σ′. For the constants 0 and 1, this can be done just by choosing one particular representing sequence for these real numbers, e.g.

δ(0) = λi:nat. 1, δ(1) = λi:nat. ifzero i 2 1.

For the booleans, we take δ(true) = 0, δ(false) = 1 and δ(⊥) = ⊥. It is also straightforward to write PCF programs Minus, Plus, Times, Max, Less for δ(−), δ(+), δ(∗), δ(max) and δ(<) respectively. For example, we may take

Minus = λf : nat → nat, i:nat.

if i = 0 then f(1) else if i = 1 then f(0) else 2 ⌢ f(i)

where ⌢ implements truncated subtraction. In any model B, this satisfies the following condition (which should be understood as a meta-level assertion):

∀f ∈ [[nat → nat]]^{B}. IsReal(f) ⇒
IsReal([[Minus]]^{B}f) ∧ Val([[Minus]]^{B}f) = −Val(f).

Coding details for the other operations are given e.g. in [Plu98]. What is more surprising is that the operation sup_{[0,1]} can be represented in PCF by a thirdorder function Sup, by means of a clever use of higher-type recursion (a detailed account of the algorithm with code is given in [Sim98]).

Proposition 5.1. SP′ is a constructive pre-logical refinement of SP via δ.

Proof sketch. Starting from any B ∈ Mod(SP′), we will obtain a model A ∈ Mod(SP) and a pre-logical relation R.

The correct definition of A is slightly subtle — the whole point is that the obvious definition via a logical relation on B does not work (see below). First, we embed B in its chain completion B̄ via an inclusion ι (we omit the definition). The main purpose of this step is to throw into the model all monotone functions of type nat → nat — this ensures that in B̄ we can represent all the classical reals and not just the computable ones (cf. Section 5.4 below). One can check that if B is a model of SP′ then so is B̄. Next we define partial equivalence relations Ē^{σ} on [[δ(σ)]]B̄ for each σ ∈ Types(Σ). For the base cases, we take

Ē^{real}(f, g) iff IsReal(f) ∧ IsReal(g) ∧ Val(f) = Val(g),
Ē^{bool}(x, y) iff x = y ∧ x ∈ {[[0]]^{B}, [[1]]^{B}, [[⊥]]^{B}}.

(The latter clause means that Ē behaves as a partial injection for observable types.) We lift this to higher types as a binary logical relation on B̄. One can show that for each constant c of Σ we have Ē(ι[[δ(c)]]^{B}, ι[[δ(c)]]^{B}).

We now construct the required model A by taking [[σ]]^{A} to be the set of equivalence classes of Ē^{σ}; one can check that A yields a Henkin model for SP. Finally, we define relations R^{σ} from [[σ]]^{A} to [[δ(σ)]]^{B} by R^{σ}(a, b) iff ι(b) ∈ a; clearly this defines a pre-logical relation R as required. □

5.4 Lack of a constructive logical refinement

We now explain why SP′ is not a constructive logical refinement of SP via δ. Intuitively, the idea is that a logical relation R is completely determined once we have fixed the relation at basic types — we have no freedom of choice for higher types. For certain models B of SP′, this means that we are forced to include in the relation R^{real→real} some highly pathological elements of [[δ(real → real)]]^{B}, and our PCF implementation of sup_{[0,1]} will fail to work for these pathological elements. This leads to a contradiction since we require R([[sup_{[0,1]}]]^{A}, [[Sup]]^{B}) for some model A of SP.

More precisely, let us take B to be some effective model of SP′, such as the effective Scott domain model [Plo77] or the term model for PCF. All that we really require is that the elements of [[nat → nat]]^{B} correspond to just the partial recursive functions ℕ_{⊥} → ℕ_{⊥}. We will show the following:

Theorem 5.2. There is no model A ∈ Mod(SP) admitting a logical relation R over A and B|_{δ} which is a partial injection on bool.

Proof sketch. The proof of the theorem hinges on the existence of a pathological PCF implementation of the constant zero function: that is, a term Funny : (nat → nat) → (nat → nat) such that R^{real→real}([[λx:real. 0]]^{A}, [[Funny]]^{B}), but such that [[Sup Funny]]^{B} = [[Bad]]^{B}, where Bad = λy:nat. if y < 2 then 1 else ⊥. Since SP entails that sup_{[0,1]}(λx:real. 0) = 0, we have R^{real}([[0]]^{A}, [[Bad]]^{B}), which can be shown to be impossible.

The idea behind Funny is based on the Kleene tree, a well-known counterexample from recursion theory (see e.g. [Bee85]). Intuitively, Funny(f) gives 0 whenever f represents a recursive real number but diverges for certain nonrecursive reals. □

Notice how the pre-logical relation ℝ in the proof of Proposition 5.1 avoids this problem: the interpretation of Funny in B̄ is not included in the partial equivalence relation E^{real→real}, since the model contains representations of nonrecursive reals on which Funny diverges.

The above example is robust in the sense that it is not just a feature of the particular implementation Sup we have chosen — it can be shown that there is no PCF program Sup that computes suprema for all relevant functions including Funny. Indeed, we believe that the above theorem should hold for all possible representations of the reals and all choices of the terms δ(c): the only condition on δ we require is that δ(real) = nat → nat.

6 Conclusion

The main purpose of this paper was to introduce the notion of constructive pre-logical refinement and explain how it relates to the usual account of data refinement for typed lambda calculus in terms of logical relations. In a nutshell, the relationship is that for data refinement logical relations work only because they are a special case of pre-logical relations, where the additional requirement imposed by logical relations is more of a hindrance than a help.

There are many directions in which this approach could be developed.

In Sect. 4 we considered linear chains of refinement steps. Decomposition of implementation tasks into separate subtasks can be modelled using constructions that take n-tuples of Henkin models as arguments, giving tree-shaped refinement diagrams. In particular, consider δ : Σ → (Σ′_{1} + … + Σ′_{n}), where Σ′_{1}+…+Σ′_{n} is a coproduct of the signatures Σ′_{1}, …, Σ′_{n}. This induces the reduct ·|_{δ} : Mod(Σ′_{1} + … + Σ′_{n}) → Mod(Σ). However, this does not give an n-ary construction, since Mod(Σ′_{1}+…+Σ′_{n}) and Mod(Σ′_{1})×⋯×Mod(Σ′_{n}) do not coincide even up to isomorphism; in other words, higher-order models do not amalgamate unambiguously. However, they weakly amalgamate: there is a standard (injective) construction that maps Mod(Σ′_{1})×⋯×Mod(Σ′_{n}) into Mod(Σ′_{1} +…+Σ′_{n}) (e.g. by taking full function spaces for extra “mixed” function types). Composing this with ·|_{δ}, we obtain a function from Mod(Σ′_{1}) × ⋯ × Mod(Σ′_{n}) to Mod(Σ) as required. This still ignores one important aspect of development, namely the possibility of mutual dependencies between subtasks. One solution, discussed thoroughly in [SST92], is to use specifications of parametric models in the development process; the same ideas should apply here, but the technical implications of using higher-order models are yet to be worked out.

This paper presents a global view of specifications and their refinement: constructions are required to work on the “whole system” (represented as a model of the implementing specification) and produce a whole system (represented as a model of the implemented specification). Good practice suggests that there should be a way to make the refinement steps “local” — that is, to use only part of the system built so far to implement some remaining parts of the requirements specification, and then add the result to the whole system built so far. Details will be provided in a longer version of the paper.

In this paper we have focused on λ^{→} only. But of course, less elementary type structures are also of great importance in software development using data refinement. One can consider inductive/coinductive datatypes, or more generally recursive types as in ML, or impredicative types as in Girard/Reynold’s System F. For instance exact real numbers as in Sect. 5 are often implemented as streams for efficiency reasons, also in purely functional contexts, and abstract data types can be understood in the context of existential types. Notions of logical relations, appropriate for each of these type disciplines, have been proposed in the literature: see e.g. [Alt98] for inductive/coinductive types and [MM85] for System F. In order to accomodate data refinement involving such datatypes we need to introduce corresponding notions of pre-logical relation. As pointed out in [HS99], there is a standard methodology here: simply require the interpretations of the “relevant” constants in the two structures to be related. Despite its simplicity, this methodology is extremely rewarding, and it allows to harvest seredipitous results also in related areas. A case in point is offered by PER models of System F, where the extra latitude and flexibility given by defining the exponential PER pre-logically allows for a number of possibly novel natural model constructions. Finally, a notion of pre-logical relation for System F would raise the intriguing question of the relationship between this framework and the one in [Han99], where data refinements in the style of [ST88] are translated into System F using existential types.

Acknowledgements: Thanks to Samson Abramsky, Jo Hannay, Peter O’Hearn, Gordon Plotkin, John Power, John Reynolds and Bob Tennent for helpful discussion. This work has been partially supported by EPSRC grants GR/K63795 and GR/L89532, the ESPRIT-funded CoFI working group, the ESPRIT- and INCO-funded CRIT-2 project and MURST’97 and MURST’99 grants.

References

[AJM96] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. To appear in Information and Computation (1996).

[Alt98] T. Altenkirch. Logical relations and inductive/coinductive types. Proc. Computer Science Logic, CSL’98. Springer LNCS 1584, 343–354 (1998).

[Bee85] M. Beeson. Foundations of Constructive Mathematics. Springer (1985).

[Gog84] J. Goguen. Parameterized programming. IEEE Trans. on Software Engineering SE-10(5):528–543 (1984).

[Han99] J. Hannay. Specification refinement with System F. Proc. Computer Science Logic, CSL’99, Madrid. Springer LNCS 1683, 530–545 (1999).

[Hoa72] C.A.R. Hoare. Correctness of data representations. Acta Informatica 1:271–281 (1972).

[HS99] F. Honsell and D. Sannella. Pre-logical relations. Proc. Computer Science Logic, CSL’99, Madrid. Springer LNCS 1683, 546–561 (1999).

[KOPTT97] Y. Kinoshita, P. O’Hearn, J. Power, M. Takeyama and R. Tennent. An axiomatic approach to binary logical relations with applications to data refinement. Proc. TACS’97. Springer LNCS 1281, 191–212 (1997).

[Mil71] R. Milner. An algebraic definition of simulation between programs. Proc. 2nd Intl. Joint Conf. on Artificial Intelligence. British Computer Society, 481–489 (1971).

[Mit96] J. Mitchell. Foundations for Programming Languages. MIT Press (1996).

[MM85] J. Mitchell and A. Meyer. Second-order logical relations. Proc. Logics of Programs, Brooklyn. Springer LNCS 193, 225-236 (1997).

[Nor98] D. Normann. The continuous functionals of finite types over the reals. Technical Report 19, Dept. of Mathematics, University of Oslo (1998).

[Plo77] G. Plotkin. LCF considered as a programming language. Theoretical Computer Science 5:223–255 (1977).

[PPST00] G. Plotkin, J. Power, D. Sannella and R. Tennent. Lax logical relations. Submitted for publication (2000).

[Plu98] D. Plume. A calculator for exact real number computation. B.Sc. project report, Univ. of Edinburgh; available from ftp://ftp.tardis.ed.ac.uk/

users/dbp/report.ps.gz (1998).

[Rey81] J. Reynolds. The Craft of Programming. Prentice Hall (1981).

[Rey83] J. Reynolds. Types, abstraction and parametric polymorphism. Proc. 9th IFIP World Computer Congress, Paris. North Holland, 513–523 (1983).

[SST92] D. Sannella, S. Sokołowski and A. Tarlecki. Toward formal development of programs from algebraic specifications: parameterisation revisited. Acta Informatica 29:689–736 (1992).

[ST88] D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifications: implementations revisited. Acta Informatica 25:233–281 (1988).

[ST97] D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program development. Formal Aspects of Computing 9:229–269 (1997).

[Sch87] O. Schoett. Data Abstraction and the Correctness of Modular Programming. Ph.D. thesis, report CST-42-87, Dept. of Computer Science, Univ. of Edinburgh (1987).

[Sch90] O. Schoett. Behavioural correctness of data representations. Science of Computer Programming 14:43–57 (1990).

[Sim98] A.K. Simpson. Lazy functional algorithms for exact real functionals. Proc. 23rd Intl. Symp. on Mathematical Foundations of Computer Science, Brno. Springer LNCS 1450, 456–464 (1998).

[Ten94] R. Tennent. Correctness of data representations in Algol-like languages. In: A Classical Mind: Essays in Honour of C.A.R. Hoare. Prentice Hall (1994).