Semantic and Syntactic Approaches to Simulation Relations^{⋆}

Jo Hannay^{1}, Shin-ya Katsumata^{2}, and Donald Sannella^{2}

1 Department of Software Engineering, Simula Research Laboratory 2 Laboratory for Foundations of Computer Science, University of Edinburgh

Abstract. Simulation relations are tools for establishing the correctness of data refinement steps. In the simply-typed lambda calculus, logical relations are the standard choice for simulation relations, but they suffer from certain shortcomings; these are resolved by use of the weaker notion of pre-logical relations instead. Developed from a syntactic setting, abstraction barrier-observing simulation relations serve the same purpose, and also handle polymorphic operations. Meanwhile, second-order prelogical relations directly generalise pre-logical relations to polymorphic lambda calculus (System F). We compile the main refinement-pertinent results of these various notions of simulation relation, and try to raise some issues for aiding their comparison and reconciliation.

1 Introduction

One of the central activities involved in stepwise development of programs 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 (integers, arrays, etc.) 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 usual way of establishing this property, known as observational equivalence, is by exhibiting a simulation relation that gives a correspondence between the data values involved in the two programs that is respected by the functions they implement. The details depend on the nature of the language in which the programs are written. In the simple case of a language with only first-order functions, it is usually enough to use an invariant on the domain of concrete values together with a function mapping concrete values (that satisfy the invariant) to abstract values [Hoa72], but a strictly more general method is to use a homomorphic relation [Mil71], [Sch90], [ST97]. If non-determinism is present in the language then some kind of bisimulation relation is required.

⋆ This research was partly supported by the MRG project (IST-2001-33149) which is funded by the EC under the FET proactive initiative on Global Computing. SK was supported by an LFCS studentship.

When the language in question is the simply-typed lambda calculus, the standard choice of simulation relation — which originates with Reynolds in [Rey81,Rey83] but is described most clearly in [Ten94], cf. [Mit96] — is to use a logical relation, a type-indexed family of relations that respects not just function application (like homomorphisms) but also lambda abstraction. Logical relations are used extensively in the study of typed lambda calculus and have applications outside lambda calculus. A problem with the use of logical relations, in connection with data refinement and other applications, is the fact that they lack some convenient algebraic properties; in particular, the composition of two logical relations is not in general a logical relation. This calls into question their application to data refinement at least, where one might expect composition to account for the correctness of stepwise refinement.

An alternative is to use instead a pre-logical relation [HS02], a weaker form of logical relations that nevertheless has many of the features that make logical relations so useful as well as being composable. This yields a proof method for establishing observational equivalence that is not just sound, as with logical relations, but is also complete. The use of pre-logical relations in data refinement is studied in [HLST00].

The situation is more complicated when we consider polymorphically typed lambda calculi such as System F [Gir71,Rey74]. Pre-logical relations can be extended to this context, see [Lei01], but then they do not compose in general although they remain sound and complete for observational equivalence. At the same time, the power of System F opens the possibility of taking a syntactic approach, placing the concept of simulation relation in a logical setting and using existential type quantification for data abstraction [MP88]. This line of development has been investigated in a string of papers on abstraction barrierobserving simulation relations by Hannay [Han99,Han00,Han01,Han03] based on a logic for parametric polymorphism due to Plotkin and Abadi [PA93]. A clear advantage of such an approach is that it is amenable to computer-aided reasoning but there are certain compromises forced by the syntactic nature of the framework.

We present this background in Sects. 2–4 and then make a number of remarks aiming at some kind of reconciliation in Sect. 5. There are more questions than answers but some possible lines of enquiry are suggested.

2 Pre-Logical Relations

Our journey begins with λ^{→}, 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.

Σ-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 a Σ-context Γ = x_{1}:σ_{1}, …, x_{n}:σ_{n} with a type σ ∈ Types^{→}(Σ), written Γ ⊳ M : σ. If Γ is empty then we write simply M : σ.

Definition 2.2. A Σ-combinatory algebra 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

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

such that K_{A}^{σ,τ} x y = x (i.e. App_{A}^{τ,σ} (App_{A}^{σ,τ→σ} K_{A}^{σ,τ} x) y = x) and S_{A}^{ρ,σ,τ} x y z = (x z)(y z) (ditto).

A Γ -environment η on a combinatory algebra 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}.

A signature Σ models the interface (type names and function names) of a functional program, with Σ-combinatory algebras modelling programs that match interface Σ. Observational equivalence of two Σ-combinatory algebras is then fundamental to the notion of data refinement.

Definition 2.3. Let A and B be Σ-combinatory algebras and let OBS, the observable types, be a subset of 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}.

Logical relations are structure-preserving relations on combinatory algebras.

Definition 2.4. A logical relation R over Σ-combinatory algebras 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 Σ.

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

Theorem 2.5 (Representation Independence [Mit96]). Let Σ be a signature that includes a type constant nat, and let A and B be Σ-combinatory algebras^{3} with [[nat]]^{A} = [[nat]]^{B} = ℕ. If there is a logical relation R over A and

3 Actually Henkin models, which are extensional combinatory algebras; however extensionality is not a necessary condition for this theorem.

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. □

This theorem corresponds directly to the following method for establishing the correctness of data refinement steps.

Proof method ([Ten94]). Let A and B be Σ-combinatory algebras and let OBS ⊆ 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.

A well-known problem with logical relations is the fact that they are not closed under composition. 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.) This is at odds with the stepwise nature of refinement, and the transitivity of the underlying notion 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 [HLST00].

The restriction to signatures with first-order term constants in the second part of Theorem 2.5 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.

In [HS02], a weakening of the notion of logical relations called pre-logical relations was studied; see [PPST00] for a categorical formulation.

Definition 2.6 ([HS02]). An algebraic relation R over Σ-combinatory algebras A, 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 Σ.

A pre-logical relation R is an algebraic relation such that:

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

The idea of this definition is to replace the reverse implication in the definition of logical relations with a requirement that the relation contains the S and K combinators. Since these suffice to express all lambda terms, this amounts to requiring the reverse implication to hold only for pairs of functions that are expressible by the same lambda term. It is easy to see that any logical relation is a pre-logical relation.

Example 2.7. A Σ-homomorphism h : A → B is a type-indexed family of functions {h^{σ} : [[σ]]^{A} → [[σ]]^{B}}_{σ∈Types^{→}(Σ)} such that for any term constant c : σ in Σ, h^{σ}([[c]]^{A}) = [[c]]^{B}, h^{τ} (App_{A}^{σ,τ} f a) = App_{B}^{σ,τ} h^{σ→τ} (f) h^{σ}(a) and h^{σ→τ} ([[Γ ⊳ λx:σ.M : σ → τ]]_{η_{A}}^{A}) = [[Γ ⊳ λx:σ.M : σ → τ]]_{h∘η_{A}}^{B}. Any Σhomomorphism is a pre-logical relation but is not in general a logical relation.

The binary case of pre-logical relations over A and B is derived from the unary case of pre-logical predicates for the product structure A × B. Similarly for n-ary relations for n > 2.

Definition 2.8 ([HS02]). A pre-logical predicate P over a Σ-combinatory algebra A is a family of predicates {P^{σ} ⊆ [[σ]]^{A}}_{σ∈Types^{→}(Σ)} such that:

– If P^{σ→τ} (f) then ∀a ∈ [[σ]]^{A}.P^{σ}(a) ⇒ P^{τ} (App_{A} f a).

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

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

Example 2.9. For any signature Σ and combinatory algebra A, the family

P^{σ}(v) ⇔ v is the value of a closed Σ-term M : σ

is a pre-logical predicate over A. (In fact, P is the least such — see Prop. 2.17 below.) Now, consider the signature Σ containing the type constant nat and term constants 0 : nat and succ : nat → nat and let A be the combinatory algebra over ℕ where 0 and succ have their usual interpretations and [[σ → τ]]^{A} = [[σ]]^{A} → [[τ]]^{A} for every σ, τ ∈ Types^{→}(Σ) with App_{A}^{σ,τ} f x = f(x). Then P is not a logical predicate over A: any function f ∈ [[nat → nat]]^{A}, including functions that are not lambda definable, takes values in P to values in P and so must itself be in P.

An improved version of Theorem 2.5, without the restriction to first-order signatures, holds if pre-logical relations are used in place of logical relations.

Theorem 2.10 (Representation Independence for Pre-Logical Relations [HS02]). Let A and B be Σ-combinatory algebras 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 2.11 ([HLST00]). Let A and B be Σ-combinatory algebras 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 — in fact, for extensional models they are the minimal weakening of logical relations with this property (see [HS02] for details).

Proposition 2.12 ([HS02]). The composition S ∘ R of pre-logical relations R over A, B and S over B, C is a pre-logical relation over A, C. □

So pre-logical refinements compose, and this explains why stepwise refinement is sound. Another explanation goes via Theorem 2.10: 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 2.13. If A ^{OBS} ∼∼∼∼∼ > B ^{OBS′} ∼∼∼∼∼ > C and OBS ⊆ OBS′ then A ^{OBS} ∼∼∼∼∼ > C. □

The key to many of the applications of logical relations, including Theorem 2.5, is the Basic Lemma, which says that any logical relation over A and B relates the interpretation of each lambda term in A to its interpretation in B.

Lemma 2.14 (Basic Lemma for Logical Relations). Let R be a logical relation over A and B. Then for all Γ -environments η_{A}, η_{B} such that R^{Γ} (η_{A}, η_{B}) and every term Γ ⊳ M : σ, R^{σ}([[Γ ⊳ M : σ]]_{η_{A}}^{A}, [[Γ ⊳ M : σ]]_{η_{B}}^{B}). □

(Here, R^{Γ} (η_{A}, η_{B}) refers to the obvious extension of R to environments.) For pre-logical relations, we get a two-way implication. This says that pre-logical relations are the most liberal weakening of logical relations that give the Basic Lemma. (The reverse implication fails for logical relations.)

Lemma 2.15 (Basic Lemma for Pre-Logical Relations [HS02]). Let R = {R^{σ} ⊆ [[σ]]^{A} × [[σ]]^{B}}_{σ∈Types^{→}(Σ)} be a family of relations over A and B. Then R is a pre-logical relation iff for all Γ -environments η_{A}, η_{B} such that R^{Γ} (η_{A}, η_{B}) and every Σ-term Γ ⊳ M : σ, R^{σ}([[Γ ⊳ M : σ]]_{η_{A}}^{A}, [[Γ ⊳ M : σ]]_{η_{B}}^{B}). □

Composability of pre-logical relations (Prop. 2.12) is an easy consequence of this.

Pre-logical relations enjoy a number of useful algebraic properties apart from closure under composition. For instance:

Proposition 2.16 ([HS02]). Pre-logical relations are closed under intersection, product, projection, permutation and ∀. Logical relations are closed under product, permutation and ∀ but not under intersection or projection. □

A consequence of closure under intersection is that given a property P of relations that is preserved under intersection, there is always a least pre-logical relation satisfying P. We then have the following lambda-definability result (recall Example 2.9 above):

Proposition 2.17 ([HS02]). The least pre-logical predicate over a given combinatory algebra contains exactly those elements that are the values of closed Σ-terms. □

In a signature with no term constants, a logical relation may be constructed by defining a relation R on base types and using the definition to “lift” R inductively to higher types. The situation is different for pre-logical relations: there are in general many pre-logical liftings of a given R, one being of course its lifting to a logical relation. But since the property of lifting a given R is preserved under intersection, the least pre-logical lifting of R is also a well-defined relation. Similarly, the least pre-logical extension of a given family of relations is well-defined for any signature. Lifting R to a logical relation is not possible in general for signatures containing higher-order term constants. Extension is also problematic: the cartesian product A × A is a logical relation that trivially extends any binary relation on A, but this is uninteresting.

3 Pre-Logical Relations for System F

The simply-typed lambda calculus λ^{→} considered in the last section is a very simple language. Extending it with other type constructors, for example sum and product types, is unproblematic, see [HS02]. Much more challenging is the addition of parametric polymorphism as found in functional programming languages, which yields System F [Gir71,Rey74]. A hint of the power this adds, apart from the obvious ability to define functions that work uniformly over a family of types, is the fact that it is possible to encode inductive types, including the natural numbers, booleans, lists and products, in pure System F [BB85].

Our interest is in data refinement over System F viewed as a programming language, as a means of applying the ideas in the previous section to languages like Standard ML. The key concept underlying data refinement, as we have seen, is that of observational equivalence, and thus understanding the notion of observational equivalence between models of System F is the main theme. Towards this goal, we extend the semantic approach described in Sect. 2 to System F. This involves extending pre-logical relations to System F, and characterising observational equivalence by pre-logical relations. Leiß [Lei01] has developed a formulation of pre-logical relations and studied their properties in F_{ω}, the extension of System F by type constructors. In the context of this paper we restrict attention to plain System F, even though the further extension to F_{ω} presents no additional difficulties.

Definition 3.1. The set of types for System F over a set B of base types is given by the grammar σ ::= b | α | σ → σ | ∀α . σ, where α ranges over type variables. A signature Σ consists of a set B of type constants and a collection C of typed term constants c : σ where σ is closed. Types_{→∀}(Σ) denotes the set of types over B.

The set of Σ-terms for System F is given by the grammar M ::= x | c | λx : σ . M | MM | Λα . M | Mσ.

For simplicity, we obey Barendregt’s variable convention: bound variables are chosen to differ in name from free variables in any type or term. A Σ-type context (ranged over by Δ) is a list of distinct type variables. A Σ-context (ranged over by Γ) is a list of pairs of variables and types in Types_{→∀}(Σ), where variables are distinct from each other. We often omit Σ if it is clear from the context. For the type system and representation of data types, see e.g. [GTL90]. By Δ ⊳ τ, Δ ⊳ Γ and Δ | Γ ⊳ M : τ we mean to declare a type, a context and a term which are well-formed.

First we introduce the underlying model theory of System F in the style of Bruce, Mitchell and Meyer [BMM90].

Definition 3.2. A Σ-BMM interpretation (abbreviated BMMI) A consists of

– a set T_{A} and a family [T_{A}^{n} → T_{A}] ⊆ T_{A}^{n} → T_{A} for each n ∈ N satisfying certain conditions,^{4}

– an element [[b]]^{A} ∈ T_{A} for each b ∈ B of Σ,

– functions ⇒_{A}: T_{A} × T_{A} → T_{A} and ∀_{A} : [T_{A} → T_{A}] → T_{A},

– a T_{A}-indexed family of sets A,

– a function App_{A}^{t⇒u} : A^{t⇒_{A}u} → (A^{t} → A^{u}) for each t, u ∈ T_{A},

– a function App_{A}^{∀f} : A^{∀_{A}f} → ∏_{t∈A} A^{f(t)} for each f ∈ [T_{A} → T_{A}].

Here we introduce two terminologies. A Δ-environment is a mapping from type variables in Δ to T_{A}. We write T_{A}^{Δ} for the set of Δ-environments. For a context Δ⊳Γ, a Γ -environment is a mapping which maps a variable in Γ to an element in A^{[[Γ (x)]]_{χ}^{A}}, where χ is a Δ-environment. We write A^{[[Γ]]_{χ}^{A}} for Γ -environments. We continue the definition:

– a meaning function for types [[−]]^{A}, which maps a type Δ ⊳ σ and χ ∈ T_{A}^{Δ} to [[σ]]_{χ}^{A} ∈ T_{A} (for details, see [Has91]),

– an element [[c]]^{A} ∈ A^{[[σ]]^{A}} for each c : σ in Σ,

– a meaning function for terms [[−]]^{A} (we use the same symbol), which maps a term Δ | Γ ⊢ M : σ and environments χ ∈ T_{A}^{Δ}, η ∈ R^{[[Γ]]_{χ}^{A}} to a value [[M]]_{χ;η}^{A} ∈ R^{[[σ]]_{χ}^{A}} (for details, see [Has91]).

Given Σ-BMMIs A and B, we can define the product Σ-BMMI A × B in the obvious componentwise fashion.

Definition 3.3. Let A be a Σ-BMMI. A predicate R over A (written R ⊆ A) consists of a subset T_{R} ⊆ T_{A} and T_{R}-indexed family of subsets R^{t} ⊆ A^{t}. For t, u ∈ T_{A} and f ∈ [T_{A} → T_{A}] such that f(t) ∈ T_{R} for any t ∈ T_{R}, we define

R^{t} → R^{u} = {x ∈ A^{t⇒_{A}u} | ∀y ∈ R^{t} . App_{A}^{t⇒u}(x)(y) ∈ R^{u}}
∀x ∈ T_{R} . R^{f} = {x ∈ A^{∀_{A}f} | ∀t ∈ T_{R} . π_{t}(App_{A}^{∀f}(x)) ∈ R^{f(t)}}

Binary relations for Σ-BMMIs are just predicates over product interpretations. Now a predicate R ⊆ A is

– pre-logical for types if it satisfies the following:

• [[b]]^{A} ∈ T_{R},

• t, u ∈ T_{R} implies t ⇒_{A} u ∈ T_{R},

4 [T_{A}^{n} → T_{A}] includes projections and is closed under composition, ⇒_{A} and ∀_{A}. See [Has91] for a detailed account.

• for all types Δ, α ⊳ σ with χ ∈ T_{R}^{Δ}, if [[σ]]_{χ{α↦t}}^{A} ∈ T_{R} holds for all

t ∈ T_{R}, then [[∀α . σ]]_{χ}^{A} ∈ T_{R},

– algebraic if it is pre-logical for types and • [[c]]^{A} ∈ R^{[[σ]]^{A}} for all c : σ in Σ,

• for all t, u ∈ T_{R}, R^{t⇒_{A}u} ⊆ R^{t} → R^{u},

• for all types Δ, α ⊳ σ with χ ∈ T_{R}^{Δ}, R^{∀_{A}f} ⊆ ∀x ∈ T_{R} . R^{f} holds, where

f(t) = [[σ]]_{χ{α↦t}}^{A},^{5}

– pre-logical if it is algebraic and

• for all terms Δ | Γ, x : σ ⊳ M : σ′ with χ ∈ T_{R}^{Δ} and η ∈ R^{[[Γ]]_{χ}^{A}}, if [[M]]_{χ;η{x↦v}}^{A} ∈ R^{[[σ′]]_{χ}^{A}} holds for all v ∈ R^{[[σ]]_{χ}^{A}}, then [[λx : σ . M]]_{χ;η}^{A} ∈

R^{[[σ]]_{χ}^{A}⇒_{A}[[σ′]]_{χ}^{A}},

• for all terms Δ, α | Γ ⊳ M : σ with χ ∈ T_{R}^{Δ} and η ∈ R^{[[Γ]]_{χ}^{A}}, if [[M]]_{χ{α↦t};η}^{A} ∈ R^{ft} holds for all t ∈ T_{R}, then [[Λα . M]]_{χ;η}^{A} ∈ R^{∀_{A}f}, where f(t) = [[σ]]_{χ{α↦t}}^{A}.

– logical if it is pre-logical for types and conditions of algebraic relations hold by equality.

Alternatively, we can extend the definition of pre-logical relations (Definition 2.6) in terms of algebraic relations relating additional combinators for System F [BMM90].

We have the following main theorem of pre-logical predicates:

Theorem 3.4 (Basic Lemma for Pre-Logical Predicates [Lei01]). Let A be a Σ-BMMI and R ⊆ A be a predicate.

1. R is pre-logical for types iff for all types Δ ⊳ σ with χ ∈ T_{R}^{Δ}, [[σ]]_{χ}^{A} ∈ T_{R} holds.

2. R is pre-logical iff for all terms Δ | Γ ⊳ M : σ with χ ∈ T_{R}^{Δ} and η ∈ R^{[[Γ]]_{χ}^{A}}, [[M]]_{χ;η}^{A} ∈ R^{[[σ]]_{χ}^{A}} holds. ⊓ ⊔

Corollary 3.5 ([Lei01]). Logical predicates over Σ-BMMIs are pre-logical. ⊓ ⊔

Proposition 3.6 ([Lei01]). Let A be a Σ-BMMI. We define the definability predicate D by T_{D} = {[[∅ ⊳ σ]]^{A}} and D^{[[∅⊳σ]]^{A}} = {[[∅ | ∅ ⊳ M : σ]]^{A}}. Then D is the least pre-logical predicate over A. ⊓ ⊔

It is easy to see that pre-logical predicates for System F are closed under product, permutation and arbitrary intersection. On the other hand, they are not closed under composition (nor under projection). This is pointed out by Leiß in the setting of F ω [Lei01]. The composition R∘S of two relations R ⊆ A×B, S ⊆ B×C is given as follows:

T_{R∘S} = T_{R} ∘ T_{S}, R ∘ S^{t,u} = {R^{t,r} ∘ S^{r,u} | ∃r.(t, r) ∈ T_{R}, (r, s) ∈ T_{S}}

5 At this point we know that f(t) ∈ T_{R} for any t ∈ T_{R} by the first part of Theorem 3.4. Thus ∀x ∈ T_{R} . R^{f} is defined.

Proposition 3.7. Binary pre-logical relations between Σ-BMMIs do not compose in general.

Proof. Let Σ_{c} = ({b}, {c : b}) be a signature and A be a Σ_{c}-BMMI where [[b]]^{A} contains at least two elements, namely {⊤, ⊥}. Any non-trivial BMMI for the empty signature can be used for this purpose. We interpret the constant by [[c]]^{A} = ⊤. We use λx . ⊥ as shorthand for [[λx : b . y]]_{∅;{y↦⊥}}^{A} ∈ A^{[[b]]^{A}⇒_{A}[[b]]^{A}}.

Let θ = [b/α] and θ′ = [b ⇒ b/α] be type substitutions. We define relation T_{R} by T_{R} = {([[σθ]]^{A}, [[σθ′]]^{B}) | α ⊢ σ}. It is easy to show that this is pre-logical for types. Next we define R^{[[σθ]]_{χ}^{A},[[σθ′]]_{χ}^{B}} for all Δ, α ⊳ σ and χ ∈ T_{R}^{Δ} by induction:

R^{[[bθ]]_{χ}^{A},[[bθ′]]_{χ}^{B}} = {(⊤, ⊤)}

R^{[[αθ]]_{χ}^{A},[[αθ′]]_{χ}^{B}} = {(⊥, λx . ⊥)}

R^{[[βθ]]_{χ}^{A},[[βθ′]]_{χ}^{B}} = R^{χ(β)}

R^{[[(σ⇒σ′)θ]]_{χ}^{A},[[(σ⇒σ′)θ′]]_{χ}^{B}} = R^{[[σθ]]_{χ}^{A},[[σθ′]]_{χ}^{B}} → R^{[[σ′θ]]_{χ}^{A},[[σ′θ′]]_{χ}^{B}}

R^{[[(∀β.σ)θ]]_{χ}^{A},[[(∀β.σ)θ′]]_{χ}^{B}} = ∀x ∈ T_{R} . R^{f} (f(t, u) = ([[σθ]]_{χ{β↦t}}^{A}, [[σθ′]]_{χ{β↦u}}^{B}))

We can show that R = (T_{R}, R) is pre-logical. However the relation R^{−1} ∘ R relates (λx . ⊥, λx . ⊥) but not (⊥, ⊥). This contradicts algebraicity. ⊓ ⊔

One natural question is when the composition of two pre-logical relations is pre-logical, and Leiß showed a sufficient condition [Lei01].

We give a characterisation of observational equivalence by pre-logical relations, as in Theorem 2.10. We can reuse Definition 2.3 for observational equivalence between Σ-BMMIs with respect to closed observable types.

Theorem 3.8 ([Lei01]). Let A and B be Σ-BMMIs and let OBS be a set of closed types of System F. Then A ≡_{OBS} B iff there exists a pre-logical relation over A and B which is a partial injection on OBS.

4 Expressing Simulation Relations Syntactically

Our journey now moves into the syntactic realm, placing the concepts of simulation relation and representation independence in a logical setting. The main incentive is that computer-aided reasoning requires syntactic expressibility.

One reasonable choice for syntactic formalism is the polymorphic lambda calculus, together with a second-order logic, with the lambda calculus being the object programming language. The decision in this section to make use of polymorphism is motivated primarily by expressibility, since semantic notions may then be internalised in syntax. At the outset, we use this expressive power to express the simply-typed notions of Sect. 2. However, in Sect. 4.4, polymorphism in data types is also handled. Nevertheless, in Sect. 4.6 we suggest that the appropriate setting for describing polymorphic data types is actually F_{3}.

Our choice here of formalism influences the way we regard the failure of standard simulation relations, i.e., logical relations, at higher order. It turns out that a natural trail of development gives a solution that is conceptually different from that of pre-logical relations, although it should be evident that the concepts are strongly related. The syntactic approach here is developed directly from syntactic abstraction barriers inherent in polymorphic types. This gives a notion of abstraction barrier-observing (abo) simulation relation.

4.1 Internalisation into Syntax

To start, we consider System F, cf. Sect. 3. Here we wish to be formalistic, so we use pure System F without constants. Self-iterating inductive types can be encoded [BB85], e.g., nat =^{def} ∀α.α → (α → α) → α, bool =^{def} ∀α.α→α→α, and list_{σ} =^{def} ∀α.α → (σ → α → α) → α, with programmable constructors, destructors and conditionals. Products encode as σ × τ =^{def} ∀α.(σ → τ → α) → α with constructor pair_{σ,τ} and destructors proj_{1}_{σ,τ} and proj_{2}_{σ,τ}.

We use the logic for parametric polymorphism due to [PA93], a second-order logic over System F augmented with relation symbols, relation definition, and the axiomatic assertion of relational parametricity. See also [Mai91,Tak98]. Formulae now include relational statements as basic predicates and quantifiables,

ϕ ::= (M =_{σ} N) | M ξ N | ⋯ | ∀ξ ⊂σ×τ . ϕ | ∃ξ ⊂σ×τ . ϕ

where ξ ranges over relation variables. Relation definition is given by the syntax

Γ ⊳ (x:σ, y:τ) . ϕ ⊂ σ×τ

where ϕ is a formula. For example eq_{σ} =^{def} (x:σ, y:σ) . (x =_{σ} y).

We write U[X] to indicate possible occurrences of variable X in type, term or formula U, and write U[A] for the capture-correct substitution U[A/X].

Complex relations may be built from simpler ones. We get the arrow-type relation R→R′ ⊂ (σ →σ′)×(τ →τ′) from R ⊂ σ×τ and R′ ⊂ σ′×τ′ by

(R→R′) =^{def} (f:σ →σ′, g:τ →τ′) . (∀x:σ.∀y:τ . (x R y ⇒ (fx) R′ (gy)))

The universal-type relation ∀(α, β, ξ ⊂ α×β)R[ξ] ⊂ (∀α.σ[α])×(∀β.τ[β]) is defined from R[ξ] ⊂ σ[α] × τ[β], where α, β and ξ ⊂ α × β are free, by

∀(α, β, ξ ⊂ α×β)R[ξ] =^{def} (y:∀α.σ[α], z:∀β.τ[β]) . (∀α.∀β.∀ξ . (yα)R[ξ](zβ))

For n-ary α, σ, τ, R, where R_{i} ⊂σ_{i}×τ_{i}, we get ρ[R]⊂ρ[σ]×ρ[τ], the action of type ρ[α] on R, by substituting relations for type variables:

\begin{matrix}ρ[α] = α_{i} : & ρ[R] = R_{i} \\ ρ[α] = ρ′[α]→ρ′′[α] : & ρ[R] = ρ′[R]→ρ′′[R] \\ ρ[α] = ∀α′.ρ′[α, α′] : & ρ[R] = ∀(β, γ, ξ ⊂β×γ)ρ′[R, ξ] \end{matrix}

Here, R may be seen as base relations from which one uniquely defines relations according to type construction. This is logical lifting and gives the mechanism for logical relations in our syntactic setting.

The proof system is intuitionistic natural deduction, augmented with inference rules for relation symbols in the obvious way. There are standard axioms for equational reasoning implying extensionality for arrow and universal types.

Parametric polymorphism requires all instances of a polymorphic functional to exhibit a uniform behaviour [Str67,BFSS90,Rey83]. We adopt relational parametricity [Rey83,MR91]: A polymorphic functional instantiated at two related domains should give related instances. This is asserted by the schema

Param : ∀γ.∀f:(∀α.σ[α, γ]) . f (∀α.σ[α, eq_{γ}]) f

The logic with Param is sound; we have, e.g., the parametric per-model of [BFSS90] and the syntactic models of [Has91]. In order to prove the existence of a model, one has to show that Param holds for all closed f. If one then expands the statement, one obtains a syntactic analogue of the Basic Lemma for logical relations, but here involving universal types.

Lemma 4.1 (Basic Lemma Param [PA93]). For all closed f : ∀α.σ[α], we derive without Param, f (∀α.σ[α]) f. □

Constructs such as products, sums, initial and final (co-)algebras are encodable in System F. With Param, these become provably universal constructions. Relational parametricity also yields the fundamental

Lemma 4.2 (Identity Extension Param [PA93]). With Param, we derive

∀γ.∀u, v:σ[γ] . (u σ[eq_{γ}] v ⇔ (u =_{σ[γ]} v)) □

For data types, we use the following notation: A data type over a signature T consists of a data representation A and an implementation of a set of operations 𝔞:T [A]. Encapsulation is provided in the style of [MP88] by the following encoding of existential (abstract) types and pack and unpack combinators:

∃α.T [α] =^{def} ∀β.(∀α.(T [α]→β)→β), β not free in σ

pack_{T} (A)(𝔞) =^{def} Λβ.λf:∀α.(T [α]→β).f(A)(𝔞)

unpack_{T} (package)(τ)(f) =^{def} package(τ)(f)

Operationally, pack packages a data representation and an implementation of operations on that data representation to give a data type of the existential type. The resulting package is a polymorphic functional, that given a client computation and its result domain, instantiates the client with the particular elements of the package. The unpack combinator is merely the application operator for pack. An abstract type for stacks of natural numbers could be

∃α.(α × (nat →α→α) × (α→α) × (α→nat))

A data type of this type is, e.g., (pack list_{nat} 𝔩), where

(proj_{1} 𝔩) = nil, (proj_{2} 𝔩) = cons,
(proj_{3} 𝔩) = λl:list_{nat} . (cond list_{nat} (isnil l) nil (cdr l)),
(proj_{4} 𝔩) = λl:list_{nat} . (cond nat (isnil l) 0 (car l)).

For convenience we use a labelled product notation,

∃α.T_{Stack_{nat}} [α]

where T_{Stack_{nat}} [α] =^{def} (empty : α, push : nat → α → α, pop : α → α, top : α → nat). Each f_{i} : T_{i}[α] is a profile in T [α]. The analogy to Sect. 2 is that f_{i} is a term constant in the signature T, and models are internalised as packages (packA𝔞).

Consider now the issue of when two packages are interchangeable in a program. To each refinement stage, a set OBS of observable types is associated, assumed to contain closed inductive types, such as bool or nat, and also any parameters. Two data types are interchangeable if their observable properties are the same, i.e., packages should be observationally equivalent if it makes no difference which one is used in computations with observable result types. Thus:

Definition 4.3 (Observational Equivalence). Observational equivalence of (packA𝔞), (packB𝔟) with respect to OBS is expressed by

⋀_{ι∈OBS} ∀f:∀α.(T [α]→ι).(fA 𝔞) =_{ι} (fB 𝔟)

For example, an observable computation on natural-number stacks could be Λα.λ𝔵:T_{Stack_{nat}} [α] . 𝔵.top(𝔵.push n 𝔵.empty).

Observational equivalence is the conceptual description of interchangeability, and simulation relations is a means for showing observational equivalence. In the logic one uses the action of types on relations to define logical relations. Two data types are related by a simulation relation if there exists a relation on their data representations that is preserved by their corresponding operations.

Definition 4.4 (Simulation Relation). The existence of a simulation relation between (packA𝔞) and (packB𝔟) is expressed by ∃ξ ⊂A×B . 𝔞(T [ξ, eq_{γ}])𝔟.

We want the two notions to be equivalent. For data types with first-order operations, this equivalence is a fact under relational parametricity. At higher-order this is not the case. Also, the composability of simulation relations fails at higher order, compromising the constructive composition of refinement steps.

Consider the assumption that T [α] has only first-order function profiles:

FDT_{OBS}^{T}: Every profile T_{i}[α] = T_{i}_{1}[α] → ⋯ → T_{n_{i}}[α] → T_{c_{i}}[α] of T [α] is first order, and such that T_{c_{i}}[α] is either α or some ι ∈ OBS.

Theorem 4.5 (Composability [Han99]). Assuming FDT_{OBS}^{T}, with Param we get

\begin{matrix}∀A, B, C, ξ ⊂A×B, ζ ⊂B×C, 𝔞:T [A], 𝔟:T [B], 𝔠:T [C]. \\ 𝔞 T [ξ, eq_{γ}] 𝔟 ∧ 𝔟 T [ζ, eq_{γ}] 𝔠 ⇒ 𝔞 T [ξ ∘ ζ, eq_{γ}] 𝔠 □ \end{matrix}

Theorem 4.6 (Representation Independence [Han99]). Assuming FDT_{OBS}^{T}, we get with Param, for A, B, 𝔞:T [A], 𝔟:T [B] and OBS,

∃ξ ⊂A×B . 𝔞 T [ξ, eq_{γ}] 𝔟 ⇔ ⋀_{ι∈OBS} ∀f:∀α.(T [α]→ι) . (fA 𝔞) =_{ι} (fB 𝔟)

□ For Theorem 4.6, consider how to derive ⇒. In Sect. 2, we would use the Basic Lemma in this situation. Here, we apply Param; f (∀α.T [α, eq_{γ}] → ι) f. As mentioned before, Param for closed f is essentially the Basic Lemma for logical relations. In the semantic setting one can talk about closed terms. This is not immediately possible syntactically, and note that the definition of observational equivalence here says nothing about f being closed. To compensate for this, we use a extended ‘Basic Lemma’, namely relational parametricity.

For the opposite direction, one must construct a relation ξ. Analogous to the case in the semantic setting, we use definability, but since closedness is intangible for us, we can only exhibit ξ =^{def} (a:A, b:B) . (Dfnbl(a, b)), where

Dfnbl =^{def} (x:A, y:B) . (∃f_{α}:∀α.T [α]→α . f_{α}A𝔞 = x ∧ f_{α}B𝔟 = y)

This works since observational equivalence is defined ‘open’ as well. For example, if there is a profile g: α → α in T, then we show 𝔞.g (Dfnbl → Dfnbl) 𝔟.g which follows easily by giving f =^{def} Λα.λ𝔵: α.𝔵.g(f_{α}α𝔵), where f_{α} is postulated by the antecedentary Dfnbl. If g : α → ι, then f : ∀α.T [α] → ι, and by observational equivalence we have fA𝔞 =_{ι} fB𝔟, which gives fA𝔞 ι fB𝔟 by Param.

This particular proof fails if T [α] has higher-order profiles. Consider

T [α] =^{def} (p:(α→α)→nat, s:α→α)

We must derive ∀x: A → A, y: B → B . x(Dfnbl → Dfnbl)y ⇒ 𝔞.px =_{nat} 𝔟.py. However, x(Dfnbl → Dfnbl)y does not give us an f_{α→α}: ∀α.T [α] → (α → α) such that f_{α→α}A𝔞 = x ∧ f_{α→α}B𝔟 = y, so we cannot construct our f: ∀α.T [α] → nat to complete the proof.

This negative result involving Dfnbl generalises. At higher order, there might not exist any simulation relation in the presence of observational equivalence [Han01]. To exemplify with T [α] above, any candidate R ⊂ A × B has to satisfy ∀x: A → A, y: B → B . x (R → R) y ⇒ 𝔞.px =_{nat} 𝔟.py, and this includes x and y that do not belong to, or are not expressible by, operations in the respective data types. This, one might argue, is unreasonable.

In fact, it is. Consider a computation f = Λα.λ𝔵 : T [α].M[α, 𝔵]. A crucial observation is now embodied in the following obvious statement.

Abs-Bar : A computation Λα.λ𝔵:T [α].M[α, 𝔵] cannot have free variables of types involving the virtual data representation α.

This has a direct bearing on how data type operations may be used. For example, x: A → A and y: B → B above cannot be arbitrary, but must be expressible by respective data type operations; in this case, the only possible candidate for x is 𝔞.g, and 𝔟.g for y.

4.2 abo-Simulation Relations with Special Parametricity

An obvious solution is now to define a notion of simulation relation where arrowtype relations are weakened by definability clauses for arguments [Han00,Han01]. For example, write 𝔞.s (R→R)^{ℷ} 𝔟.s, for ℷ =^{def} ⟨A, B⟩⟨𝔞, 𝔟⟩, meaning

∀x:A, y:B . x R y ∧ Dfnbl_{α}^{ℷ}(x, y) ⇒ 𝔞.sx R 𝔟.sy

where Dfnbl_{α}^{ℷ}(x, y) =^{def} (x:A, y:B) . (∃f_{α}:∀α.T [α]→α . f_{α}A𝔞 = x ∧ f_{α}B𝔟 = y).

In general, definability clauses are inserted recursively in arrow types, bottoming out at base relations, i.e., R^{ℷ} =^{def} R. The full definition is in [Han01], and includes the formulation at universal type as well. With a slight abuse of notation, Definition 4.7 (abo-Simulation Relation). For any A, B and R ⊂ A × B,

T [R, eq_{γ}]^{ℷ} =^{def} (𝔞:T [A, γ], 𝔟:T [B, γ]) . (∧_{1≤i≤k} 𝔞.g_{i} (T_{i}[R, eq_{γ}]^{ℷ}) 𝔟.g_{i})

Observable types such as nat are universal types and appear in ℷ-variants inside T [ξ]. Therefore, it is important that nat^{ℷ} is eq_{nat}. This holds for closed inductive types using Param. However, we do not get desired relational properties at product type, hence the formulation in Definition 4.7.

We are still working under the assumption of relational parametricity. However, notice that we cannot apply Param, e.g., when using T [ξ, eq_{γ}]^{ℷ}. One can recover the needed proof power by asserting the missing piece of relational parametricity. Write f (∀α.T [α, eq_{γ}]^{ε} →σ[α, eq_{γ}]^{ε}) f, meaning

\begin{matrix}∀A, B, ξ ⊂A×B.∀𝔞:T [A, γ], 𝔟:T [B, γ] . \\ 𝔞(T [ξ, eq_{γ}]^{ℷ})𝔟 ⇒ (fA 𝔞)(σ[ξ, eq_{γ}]^{ℷ})(fB 𝔟) \end{matrix}

where ℷ = A, B, 𝔞, 𝔟. We assume the following: HDT_{OBS}^{T}: Every profile T_{i}[α] = T_{i}_{1}[α]→⋯→T_{n_{i}}[α]→T_{c_{i}}[α] of T [α] is such that

T_{i}_{j}[α] has no occurrences of universal types other than those in OBS, and T_{c_{i}}[α] is either α or some ι ∈ OBS.

Definition 4.8 (Special abo-Parametricity (SpParam)). For HDT_{OBS}^{T}, for σ[α, γ] having no occurrences of universal types other than those in OBS, and whose only free variables are among α and γ,

SpParam: ∀f:∀α.(T [α, γ]→σ[α, γ]) . f (∀α.T [α, eq_{γ}]^{ε} →σ[α, eq_{γ}]^{ε}) f

Lemma 4.9 (Basic Lemma SpParam [Han01]). For HDT_{OBS}^{T}, for σ[α] having no occurrences of universal types other than those in OBS, and for closed f:∀α.(T [α]→σ[α]), we derive f (∀α.T [α]^{ε} →σ[α]^{ε}) f. □

Lemma 4.9 entails soundness for the logic with Param and SpParam with respect to the closed type and term model and the parametric minimal model due to [Has91]. Theorem 4.10 (Composability [Han00]). Assuming HDT_{OBS}^{T}, we get using SpParam, for ℷ = ⟨A, B⟩⟨𝔞, 𝔟⟩, ℷ′ = ⟨B, C⟩⟨𝔟, 𝔠⟩, and ℷ′′ = ⟨A, C⟩⟨𝔞, 𝔠⟩,

\begin{matrix}∀A, B, C, ξ ⊂A×B, ζ ⊂B×C, 𝔞:T [A], 𝔟:T [B], 𝔠:T [C]. \\ 𝔞 T [ξ, eq_{γ}]^{ℷ} 𝔟 ∧ 𝔟 T [ζ, eq_{γ}]^{ℷ′} 𝔠 ⇒ 𝔞 T [ζ ∘ ξ, eq_{γ}]^{ℷ′′} 𝔠 □ \end{matrix}

Theorem 4.11 (Representation Independence [Han00]). With the assumption HDT_{OBS}^{T}, we get with SpParam, for A, B, 𝔞 : T [A], 𝔟 : T [B], OBS, and ℷ = ⟨A, B⟩⟨𝔞, 𝔟⟩,

∃ξ ⊂A×B . 𝔞 T [ξ, eq_{γ}]^{ℷ} 𝔟 ⇔ ⋀_{ι∈OBS} ∀f:∀α.(T [α]→ι) . (fA 𝔞) =_{ι} (fB 𝔟)

□ 4.3 abo-Simulation Relations with Closed Special Parametricity

If we can express closedness in the logic, then we can relate to non-syntactic models as well. Closedness is inherently intractable, but we can approximate to a certain degree. We add a basic predicate Closed to the syntax together with a pre-defined semantics. The effect of this is, for example, that the interpretation in any model of ∀f:∀α.(T [α, γ]→ι) . Closed_{OBS}(f) ⇒ ϕ(f) restricts attention in ϕ to those interpretations of all f:∀α.(T [α]→ι) that are denotable by terms whose only free variables are of types in OBS.

The semantics for the predicate Closed is not stable under term formation, so we cannot make axioms for Closed in order to derive the closedness of a term from its subterms. We can however add a second symbol ClosedS with a pre-defined semantics that does allow the derivation of closedness, but ClosedS will then not satisfy substitutivity. This is resolved by giving a separate nonsubstitutive calculus for deriving closedness, together with rules for importing the needed results into the main logic. Details are in [Han01]. We now get:

Definition 4.12 (Observational Equivalence by Closed Computation). Observational equivalence by closed computation of (packA𝔞) and (packB𝔟) with respect to OBS is expressed as

⋀_{ι∈OBS} ∀f:∀α.(T [α]→ι) . Closed_{OBS}(f) ⇒ (fA 𝔞) =_{ι} (fB 𝔟)

Also we write for example, 𝔞.s (R→R)_{C}^{ℷ} 𝔟.s, for ℷ =^{def} ⟨A, B⟩⟨𝔞, 𝔟⟩, meaning

∀x:A, y:B . x R y ∧ DfnblC_{α}^{ℷ}(x, y) ⇒ 𝔞.sx R 𝔟.sy

where DfnblC_{α}^{ℷ}(x, y) =^{def} (x:A, y:B) . (∃f_{α}:∀α.T [α]→α . Closed_{OBS}(f) ∧ f_{α}A𝔞 = x ∧ f_{α}B𝔟 = y)

Again, with a slight abuse of notation:

Definition 4.13 (abo-Simulation Relation by Closed Computation). For any A, B and R ⊂ A × B,

T [R, eq_{γ}]_{C}^{ℷ} =^{def} (𝔞:T [A, γ], 𝔟:T [B, γ]) . (∧_{1≤i≤k} 𝔞.g_{i} (T_{i}[R, eq_{γ}]_{C}^{ℷ}) 𝔟.g_{i})

Definition 4.14 (Special Closed abo-Parametricity (spParamC)). For HDT_{OBS}^{T}, for σ[α, γ] having no occurrences of universal types other than those in OBS, and whose only free variables are among α and γ,

spParamC: ∀f:∀α.(T [α, γ]→σ[α, γ]) . Closed_{OBS}(f) ⇒ f (∀α.T [α, eq_{γ}]_{C}^{ε} →σ[α, eq_{γ}]_{C}^{ε}) f

Using this, we get analogous results to the previous section. The corresponding Basic Lemma entails the soundness of the logic with Param and spParamC with respect to any relational parametric model.

4.4 abo-Relational Parametricity

The previous two subsections augmented relational parametricity with special instances of what one could call abo-relational parametricity. Now we replace relational parametricity altogether with full-fledged abo-relational parametricity. This gives a much simpler treatment than the previous approaches, but at a price: we now need infinite conjunctions in the logic. These are however well-behaved in the sense that proofs only need pointwise treatment. Moreover, refinement proofs need not be concerned with infinite conjunctions.

Abs-Bar says that function arguments in computations are bounded by formal parameters, e.g., in the computation f =^{def} Λα.λx: α.λs: α → α.t[x, s], s will only be applied to arguments built from formal parameters x and s. This transfers to instances fσ and fτ. So even at the basic level of universal types, one could for R ⊂σ×τ say that e.g., s_{σ} (R →R) s_{τ} should reflect this, in that only those x, y are considered for the antecedent x R y that are admissible in the computations. Thence, f (∀α.α→(α→α)→α)^{abo} g is the relation given by

\begin{matrix}∀γ, δ, ξ ⊂ γ × δ . ∀a:γ, b:δ, s:γ →γ, s′:δ →δ . \\ a ξ b ⇒ s (ξ →ξ)^{ℸ} s′ ⇒ fγas ξ gδbs′ \end{matrix}

where s (ξ →ξ)^{ℸ} s′ for ℸ = ⟨γ, δ⟩⟨a, b⟩⟨s, s′⟩ is

∀x:γ, y:δ . x ξ y ∧ Dfnbl_{γ}^{ℸ}(x, y) ⇒ sx ξ s′y

where Dfnbl_{γ}^{ℸ}(x, y) =^{def} (x:γ, y:δ) . (∃f_{α}:∀α.T [α]→α . f_{α}γas = x ∧ f_{α}γbs′ = y).

In general, Dfnbl clauses are inserted recursively in arrow types, bottoming out at base relations. The notion of abo-relation in [Han03] formalises the idea. Universal types play two rôles. Consider (∀α.α→(α→α)→(∀β.(α→β)→β)→α)^{abo}, and a term of this type, e.g., Λα.λx:α, s:α→α, p:∀β.(α→β)→β . s(pαs). The abo-relation treats the outer universal type as the type of a computation, and sets up the Dfnbl clauses according to formal parameters x, s, p. Then, the inner universal type must be treated as a polymorphic parameter, and it is necessary to capture that instances pσ may only vary in α. This is where infinite conjunctions enters the scene, but this discernability for universal types is what enable abo-simulation relations to handle polymorphism in data types, see below.

The abstraction barrier-observing formulation of relational parametricity is now given by the following axiom schema.

Definition 4.15 (abo-Parametricity).

abo-Param : ∀γ.∀f:(∀α.σ[α, γ]) . f (∀α.σ[α, eq_{γ}])^{abo} f

The abo-version of the identity extension lemma does not follow from abo-Param, because we can no longer use extensionality. Nevertheless, in the spirit of observing abstraction barriers, we argue that in virtual computations, it suffices to consider extensionality only with respect to function arguments that will actually occur. The simplest way to capture this is in fact by asserting identity extension.

Definition 4.16 (abo-Identity Extension for Universal Types).

abo-Iel : ∀γ.∀u, v:(∀α.σ[α, γ]) . u (∀α.σ[α, eq_{γ}])^{abo} v ⇔ u = v

Both abo-Param and abo-Iel hold in the abo-parametric per-model [Han03]. We can also formulate a basic lemma for abo-Param, if we allow infinite derivations. Regular parametricity, Param, will not hold in this model; in fact any logic containing both Param and abo-Param is inconsistent. Note that abo-Iel implies abo-Param. Nevertheless, we choose to display both. With abo-Param and abo-Iel, we regain universal properties, for example for products:

∀σ, τ.∀z:σ×τ . pair(proj_{1}z)(proj_{2}z) = z

∀u, v:σ × τ . u (σ[eq_{γ}]×τ[eq_{γ}])^{abo} v ⇔ (proj_{1}u) σ[eq_{γ}]^{abo} (proj_{1}v) ∧ (proj_{2}u) τ[eq_{γ}]^{abo} (proj_{2}v)

Theorem 4.17 (Representation Independence [Han03]). Under the assumption HDT_{OBS}^{T}, we get with abo-Param and abo-Iel,

∀A, B.∀𝔞:T [A], 𝔟:T [B] .

∃ξ ⊂A×B . 𝔞 T [ξ, eq_{γ}]^{⟨A,B⟩⟨𝔞,𝔟⟩} 𝔟 ⇔ ⋀_{ι∈OBS} ∀f:∀α.(T [α]→ι) . (fA 𝔞) =_{ι} (fB 𝔟) □

Theorem 4.18 (Composability [Han03]). Assuming HDT_{OBS}^{T}, we get with abo-Param and abo-Iel,

∀A, B, C, ξ ⊂A×B, ζ ⊂B×C, 𝔞:T [A], 𝔟:T [B], 𝔠:T [C].

𝔞(T [ξ, eq_{γ}]^{⟨A,B⟩⟨𝔞,𝔟⟩})𝔟 ∧ 𝔟(T [ζ, eq_{γ}]^{⟨B,C⟩⟨𝔟,𝔠⟩})𝔠 ⇒ 𝔞(T [ζ ∘ ξ, eq_{γ}]^{⟨A,C⟩⟨𝔞,𝔠⟩})𝔠 □

If we allow infinite derivations, we get representation independence and composability for data types with polymorphic operations, under one requirement: In the sense of Sects. 2 and 3, all type constants must either be observable or hidden, if they are the result type of any operation. Here, type constants correspond to closed types, and since we have polymorphism, type instantiation requires added caution. For example, if OBS = {bool}, then T [α] may not have a profile g : α → (∀β.β → β), since ∀β.β → β is not observable, nor any profile g : α → (∀β.α → β), since gx can then be instantiated by a non-observable closed type yielding a derived profile gx(∀β.β → β) : α → (∀β.β → β). Thus, the requirement takes the form

DT_{OBS}^{T}: Every profile T_{i}[α] = T_{i}_{1}[α] → ⋯ → T_{n_{i}}[α] → T_{c_{i}}[α] of T [α] is such that if T_{c_{i}}[α] has a deepest rightmost universal type ∀β.V, then this subtype is not closed, nor is the deepest rightmost subtype of ∀β.V the quantified β.

Then, Theorem 4.17 and Theorem 4.18 hold under DT_{OBS}^{T}.

In closing, we mention that for this section, HDT_{OBS}^{T} can in any case be relaxed by dropping the restriction on T_{i}_{j}.

4.5 pl-Relational Parametricity

It is possible to define algebraic relations in the logic. We do this from basic principles, just as we do for abo-relations. Consider again for example the universal type ∀α.α →(α →α)→α. In a sense, universal types determine signatures with function profiles. This inductive type has a profile for ‘zero’, and a profile for ‘successor’. Relative to the ‘signature’ consisting of these profiles, one can then define algebraic relations in a finite way. Here this can be done for any σ and τ, by giving a relation R_{α} ⊂ σ ×τ, taking the rôle of a base type relation, and then giving a relation R_{α→α} ⊂ (σ →σ) × (τ →τ) that we insist satisfies algebraicity: R_{α→α}(s, s′) ⇒ s (R_{α} → R_{α}) s′. In this manner, the universal type induces a family of relations, namely R_{α} and R_{α→α}, over the ‘signature’ of the universal type. Thus, we write e.g., f (∀α.α→(α→α)→α)^{pl} g for the relation

\begin{matrix}∀γ, δ, ξ_{α} ⊂ γ × δ, ξ_{α→α} ⊂ γ →γ × δ →δ . pl_{α→α}(ξ_{α→α}; ξ_{α}) ⇒ \\ ∀a:γ, b:δ, s:γ →γ, s′:δ →δ . R_{α}(a, b) ∧ R_{α→α}(s, s′) ⇒ R_{α}(fγas, gδbs′) \end{matrix}

where pl_{α→α}(ξ_{α→α}; ξ_{α}) asserts algebraicity of ξ_{α→α} relative to ξ_{α}. In general, one completes the finite family of relations with all so-called free subtypes, in order to ensure well-definedness of the algebraicity conditions. Also, the full definition of algebraic relations in this manner must reflect the two levels of polymorphism mentioned in the previous section.

To get pre-logical relations (pl-relations), one must additionally ensure closure over abstraction. This spoils finiteness, since for a combinatorial approach, we must assert relatedness of an infinite set of combinators. Again this infinite conjunction is well-behaved, since it ranges over all types only varying over the data representations.

We may soundly assert pl-relational parametricity and using this, we get similar results to those in the previous section.

It might be possible to get away with a finite number of combinators. The rationale behind this is that one may proceed with only a finite family of algebraic relations. If relations of higher order than those in the family are needed, then these can be constructed by logical lifting. This is relevant for polymorphic instantiation. Based on this, it may suffice to have an upper bound on the type complexity of combinators needed. This is under investigation.

4.6 Polymorphic Data Types in F_{3}

Polymorphism within data types is dealt with in a somewhat general manner in the two previous sections. However, it is hard to find natural examples of data types with polymorphic operations that are expressible in System F. Instead, F_{3} is appropriate, and then one could give e.g., polymorphic stacks as follows.

∃𝔛:∗→∗.T_{polyStack}[𝔛],

T_{polyStack}[𝔛] = (\begin{matrix}empty :∀γ . 𝔛γ, push :∀γ . γ →𝔛γ →𝔛γ, \\ pop :∀γ . 𝔛γ →𝔛γ, top :∀γ . 𝔛γ →γ →γ, \\ map :∀γ, γ′ . (γ →γ′)→𝔛γ →𝔛γ′ ) \end{matrix}

This provides polymorphic stack operations. The data representation is a type constructor 𝔛 to be instantiated by the relevant stack element type.

One can treat this kind of shallow polymorphism in a pointwise fashion in F_{2} [Han01], so that one essentially reduces the problem to non-polymorphic signatures. Then it is not necessary that F_{2} technology deals with polymorphic signatures, neither in one way or another. Alternatively, one could devise appropriate notions of relational parametricity for F_{3}.

5 Reconciliation

In comparison with the neat and tidy story of pre-logical relations in the simplytyped lambda calculus told in Sect. 2, both the semantic account of pre-logical relations in System F in Sect. 3 and the syntactic approach of abstraction barrier-observing simulation relations in Sect. 4 exhibit certain shortcomings. Our present feeling is that true enlightenment on this subject will require some bridge between the two. The following subsections suggest some possible lines of enquiry that seem promising to us.

5.1 Internalisation of Semantic Notions into Syntax

Sects. 2 and 3 deal with semantic simulation relations between models for lambda calculi. Sect. 4, on the other hand, internalises models and simulation relations into syntax. Models (data types) then become terms of an existential type of the form ∃α.T [α] =^{def} ∀β.(∀β.T [α] → β) → β, for some ‘signature’ T [α], and computations or programs using data types are f : ∀α.T [α] → σ. Thus, polymorphism is used to internalise semantic notions. This use of polymorphism is at a level external to data types (models); as in the outermost universal type in computations f:∀α.T [α]→σ, in contrast to polymorphism within models arising from any polymorphic profiles in T [α].

Relationally, this two-leveled aspect gives rise to certain difficulties. For logical relations it suffices to give a uniform relational definition for universal types, but for abo-relations which use definability relative to data type signatures, it is necessary to reflect the two levels in the relational definitions. This gives a nonuniform relational treatment at universal type. Note that the semantic approach in Sect. 3 does not work on internalised structures in the syntax, and the notion of relational parametricity is there cleaner.

Internalising models as, e.g., inhabitants of existential type, gives syntactic control, especially in the context of refining abstract specifications to executable programs. However, we think that the benefits of this to mechanised reasoning should be weighed against a possible scenario without internalisation, but perhaps with sound derived proofs rules for data refinement. This would be a more domain-specific calculus, but might provide a simpler formalism, perhaps more in style with semantic reasoning.

5.2 Equivalence of Models Versus Equivalence of Values in a Model

As a consequence of the internalisation of semantic notions discussed above, the term “observational equivalence” has been applied at two different levels to achieve similar aims. In Sects. 2 and 3, observational equivalence is a relation between two models over the same signature, representing programs. In Sect. 4, it is a relation on encapsulated data types within a single model; such a relation is sometimes referred to as indistinguishability, written ≈. In both of the latter two sections, the power of System F would allow the opposite approach to be taken. Then the question of the relationship between the resulting definitions arises. This question has been investigated in a number of simpler frameworks in [BHW95,HS96,Kat03], where the connection is given by a factorisability result of the form A ≡ B iff A/≈ ≅ B/≈. It is likely that the same applies in the context of System F, and this might in turn help to shed light on the relationship between the semantic and syntactic worlds.

5.3 Finiteness

Pre-logical relations are defined in terms of definable elements. In logic it is hard to deal with definability in a term-specific way. In Sect. 4.3 we approximated by introducing a new predicate Closed, and in Sect. 4.2 we explicitly related to syntactic models. In both Sect. 4.4 and Sect. 4.5, we basically end up with infinitary logic, albeit in a tractable manner. It may also be feasible to combine elements, for example to use the Closed predicate together with pl-relations.

From a purist point of view, all these approaches are slightly unsatisfactory, although for practical purposes they provide methods for proving refinement, since the infinitary issues are basic and of no concern when doing refinement proofs. In fact this is true a fortiori for abo-simulation relations, since these are in fact finite, unlike pre-logical relations.

5.4 Pre-Logical Relations and abo-Relations

Both pre-logical relations (pl-relations in the logic) and abo-relations solve the same problems for refinement. The question is then what else they have in common. To make a comparison easier, one can do two things. First, one can transpose the syntactic idea of abo-relation into the semantic setting around e.g., combinatory algebras. It is then probably natural to interpret the Dfnbl clauses as term-definability. In that case when considering data types, it is evident that abo-simulation relations specialise to a finitary version of the minimal pre-logical relation, which is not surprising. The general relationship is however unclear.

Conversely, one might transpose the idea of pre-logical relation into syntax with internalised data types. This is mentioned in Sect. 4.5. Then, the connection is not so clear, since the Dfnbl clause says nothing about term-definability, unless we use the Closed predicate of Sect. 4.3. Any comparison would probably depend on the model of choice for the logic.

Furthermore, at a more fundamental level, one gets various concepts of relational parametricity. We have the ones in the syntactic setting where data types are internalised, but we also have the external semantic concept in connection to the scenario in Sect. 3. Characterising these in terms of one another is left as an interesting challenge, the start of which is described in the next section.

5.5 Connection with Pre-Logical Relations and Relational Interpretation of System F

We can regard a binary relation over a BMM interpretation as an interpretation of types by relations. The origin of this viewpoint, the relational interpretation of System F, goes back to Reynolds [Rey83] in his attempt to obtain a set-theoretic model of System F. This relational viewpoint enables him to capture the nature of polymorphism in terms of relational parametricity.

A semantic account of this viewpoint is given in [MR91,Has91,RR94,BAC95]. Roughly speaking, a relational interpretation of System F consists of two components: a reflexive graph (a graph with an identity edge at each node), which gives a skeleton of binary relations; and an underlying interpretation of System F together with binary relations over it. The interpretation ties nodes and edges of the reflexive graph to the carrier sets of the underlying interpretation and binary relations. This mapping respects identity, i.e. identity edges are mapped to identity relations.

We can find a correspondence between pre-logical relations and the relational interpretation of System F. Reflexive graphs are a generalisation of reflexive relations. Thus a pair consisting of a BMM interpretation A and a relation R ⊆ A×A such that T_{R} is reflexive and R^{t,t} = id_{A^{t}} form a relational interpretation of System F. Conversely, any relational interpretation whose reflexive graph is just a reflexive relation can be regarded as a relation over its underlying interpretation of System F. Moreover we often assume that the mapping from edges to relations respects the interpretation of types. This situation is called natural in [Has91], and under the above correspondence, this means that the corresponding relation is logical.

This correspondence suggests that we can bring back our notion of pre-logical relations to consider a class of relational interpretations of System F. We expect that this new class includes interpretations which satisfy Reynolds’ abstraction theorem. The question is how do we understand the notion of relational parametricity in this new class. Parametricity states that relations at universal types include identity relations, but the identity relation itself is a logical notion (in extensional models). One negative consequence of this mismatch is that the Identity Extension Lemma does not hold. On the other hand, modifying parametricity is a good idea for achieving a finer characterisation of observational equivalence. This is exactly achieved on the syntactic side in Sect. 4. We expect that this modification and relevant results developed in the syntactic approach will provide interesting feedback to the relational interpretation of System F.

References

[BFSS90] E. Bainbridge, P. Freyd, A. Scedrov, and P. Scott. Functorial polymorphism. Theoretical Computer Science 70:35–64 (1990).

[BAC95] R. Bellucci, M. Abadi, and P.-L. Curien. A model for formal parametric polymorphism: a PER interpretation for system R. Proc. 2nd Intl. Conf. on Typed Lambda Calculi and Applications, TLCA’95, Edinburgh. Springer LNCS 902, 32–46 (1995).

[BHW95] M. Bidoit, R. Hennicker and M. Wirsing. Behavioural and abstractor specifications. Science of Computer and Programming, 25:149–186 (1995).

[BB85] C. Böhm and A. Berarducci. Automatic synthesis of typed λ-programs on term algebras. Theoretical Computer Science 39:135–154 (1985).

[BMM90] K. Bruce, A. Meyer, and J. Mitchell. The semantics of the second-order lambda calculus. Information and Computation 85(1):76–134 (1990).

[Gir71] J.-Y. Girard. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. Proc. 2nd Scandinavian Logic Symp., Oslo. Studies in Logic and the Foundations of Mathematics, Vol. 63, 63–92. North-Holland (1971).

[GTL90] J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge University Press (1990).

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

[Han00] J. Hannay. A higher-order simulation relation for System F. Proc. 3rd Intl. Conf. on Foundations of Software Science and Computation Structures. ETAPS 2000, Berlin. Springer LNCS 1784, 130–145 (2000).

[Han01] J. Hannay. Abstraction Barriers and Refinement in the Polymorphic Lambda Calculus. PhD thesis, Laboratory for Foundations of Computer Science (LFCS), University of Edinburgh (2001).

[Han03] J. Hannay. Abstraction barrier-observing relational parametricity. Proc. 6th Intl. Conf. on Typed Lambda Calculi and Applications, TLCA 2003, Valencia. Springer LNCS 2701 (2003).

[Has91] R. Hasegawa. Parametricity of extensionally collapsed term models of polymorphism and their categorical properties. Proc. Intl. Conf. on Theoretical Aspects of Computer Software, TACS’91, Sendai. Springer LNCS 526, 495–512 (1991).

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

[HS96] M. Hofmann and D. Sannella. On behavioural abstraction and behavioural satisfaction in higher-order logic. Theoretical Computer Science 167:3–45 (1996).

[HLST00] F. Honsell, J. Longley, D. Sannella and A. Tarlecki. Constructive data refinement in typed lambda calculus. Proc. 3rd Intl. Conf. on Foundations of Software Science and Computation Structures. ETAPS 2000, Berlin. Springer LNCS 1784, 161–176 (2000).

[HS02] F. Honsell and D. Sannella. Prelogical relations. Information and Computation 178:23–43 (2002). Short version in Proc. Computer Science Logic, CSL’99, Madrid. Springer LNCS 1683, 546–561 (1999).

[Kat03] S. Katsumata. Behavioural equivalence and indistinguishability in higherorder typed languages. Selected papers from the 16th Intl. Workshop on Algebraic Development Techniques, Frauenchiemsee. Springer LNCS, to appear (2003).

[Lei01] H. Leiß. Second-order pre-logical relations and representation independence. Proc. 5th Intl. Conf. on Typed Lambda Calculi and Applications, TLCA’01, Cracow. Springer LNCS 2044, 298–314 (2001).

[MR91] Q. Ma and J. Reynolds. Types, abstraction and parametric polymorphism, part 2. Proc. 7th Intl. Conf. on Mathematical Foundations of Programming Semantics, MFPS, Pittsburgh. Springer LNCS 598, 1–40 (1991).

[Mai91] H. Mairson. Outline of a proof theory of parametricity. Proc. 5th ACM Conf. on Functional Programming and Computer Architecture, Cambridge, MA. Springer LNCS 523, 313–327 (1991).

[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).

[MP88] J. Mitchell and G. Plotkin. Abstract types have existential type. ACM Trans. on Programming Languages and Systems 10(3):470–502 (1988).

[PA93] G. Plotkin and M. Abadi. A logic for parametric polymorphism. Proc. Intl. Conf. Typed Lambda Calculi and Applications, TLCA’93, Utrecht. Springer LNCS 664, 361–375 (1993).

[PPST00] G. Plotkin, J. Power, D. Sannella and R. Tennent. Lax logical relations. Proc. 27th Int. Colloq. on Automata, Languages and Programming, Geneva. Springer LNCS 1853, 85–102 (2000).

[Rey74] J. Reynolds. Towards a theory of type structures. Programming Symposium (Colloque sur la Programmation), Paris, Springer LNCS 19, 408–425 (1974).

[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).

[RR94] E. Robinson and G. Rosolini. Reflexive graphs and parametric polymorphism. Proc., Ninth Annual IEEE Symposium on Logic in Computer Science, Paris, 364–371. IEEE Computer Society Press (1994).

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

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

[Str67] C. Strachey. Fundamental concepts in programming languages. Lecture notes from the Intl. Summer School in Programming Languages, Copenhagen (1967).

[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).

[Tak98] I. Takeuti. An axiomatic system of parametricity. Fundamenta Informaticae, 33(4):397–432 (1998).