A relational framework for abstract interpretation^{1}

Alan Mycroft

Computer Laboratory Corn Exchange Street Cambridge CB2 3QG England Neil D. Jones DIKU Sigurdsgade 41 DK-2200 Copenhagen N Denmark

Abstract

Abstract interpretation is a very general framework for proving certain properties of programs. This is done by interpreting the symbols of the program, or the symbols of a denotational metalanguage translation, in two different ways (the standard interpretation and the abstract interpretation) and relating them. We set up a new framework for abstract interpretation based on relations (with the intent of inclusive or logical relations). This avoids problems with power domains and enables certain higher-order frameworks to be proved correct. As an example we show how the Hindley/Milner type system can be viewed as a special case of our system and is thus automatically correct.

1 Introduction

This work collects together several ideas from the literature and uses them as a new framework for abstract interpretation including higher types and gives associated examples. The prime importance of this work is this framework and indeed parts of the theory of the examples are well discussed in the literature. Much work remains to be done and we would expect the final shape of these ideas to differ from this preliminary form.

The development uses relations defined inductively on types instead of power domains and adjoined functions of previous works. One argument for using relations instead of functions for abstraction is to consider the example of determining types in a language with a monotyped (Pascal-like) type system. We might want to associate a value (or set of values) with a type by means of a function. However, it is clear by considering the value λx.x that it should be related to the types (int → int) and (bool → bool), but that these do not have a least upper bound type in this system. Relations naturally encode this many-many property. Another technical reason for using relations is concerned with higher-order objects as discussed in section 3.

In fact, in a sense which we will make more precise later on, the Hindley/Milner polymorphic type discipline is up to a representation function a sublattice of the power set of such types in which λx.x is related by means of a function to the set of types of the form (t → t) as t ranges over monotypes. This corresponds to the notion of a principal type.

As we might expect from this, many abstraction relations are induced from abstraction functions. We discuss this in section 6.

Finally, we feel that the abstraction functions involved in abstract interpretation and the homomorphisms occurring in universal algebra are special cases of a more general concept — see the discussion in section 3.

1A preliminary version of this paper was presented at the Workshop on Abstract Interpretation at Kent University, Canterbury in August 1985.

1.1 What questions do we wish to ask?

One particularly crucial task in program analysis is deciding what questions we wish to have answers to, or more formally, which theorems we wish to prove.

One can separate two cases, the second more general than the first:

• We wish to know the answers to questions pertaining to a form of ‘global’ correctness – for example that the result of running a program analysed to have a certain type actually yields a value of that type. (Note that correctness here may not have anything to do with termination.) Also, supposing we have a program consisting of a set of recursion equations, we may wish to know certain properties of the individual denotations of the functions (e.g. whether they are strict at a certain argument position). Most analyses of functional programs using abstract interpretation have used such a framework – as far as we know the only exception is [7] discussed below.

• We wish to know the answers to questions of ‘local’ behaviour – for example that only certain variable-value environments may obtain at a given program point (= label). The seminal Cousot paper on abstract interpretation considers such a circumstance, although it is clear that this is not a generalisation of the case above. A recent paper by Jones and Mycroft [7] discusses a framework of abstract interpretation based on ‘minimal function graphs’ (mfg) in which (for the case of first-order recursion equations) we can model the values of arguments the functions are actually called with. Moreover, the standard interpretation is an abstraction of this mfg interpretation and by transitivity so is every ‘global’ problem as defined above which can be characterised as an abstact interpretation in the ‘global’ sense above.

One resolution of this dichotomy is to follow Nielson[15] and analyse the meta-language of a denotational definition (to be viewed as a translation of object- to meta-language terms). However, Nielson’s work has several problems (see chapter 6 in the above reference) the main ones being the absence of any treatment of higher order objects and the hardwired treatment of the least fixpoint operator which seems to preclude the mfg analysis above.

For reasons of concreteness (and the clarity of exposition gained in this case) this work deals with constructing a framework (for the special case of the λ-calculus) which may be used to answer questions of the former kind and which deals with higher-order functions. Because of the fixed denotational schema we cannot expect it to be able to express all questions of the latter kind. We would anticipate that it would generalise easily to a framework like Nielson’s.

1.2 Related work

The classical paper on abstract interpretation is the Cousots’ seminal work[3], which set up a general framework for static program analysis and showed how many apparently ad hoc techniques were special cases. Donzeau-Gouge[5] developed the Cousots’ framework for denotational semantics parameterising it on certain key domains. Mycroft [13] and later with Nielson [14] extended such techniques for the analysis of functional programs including termination. Unfortunately, the last-mentioned work used a framework using a rather special power-domain construction which only seems to work for the first-order case. Nielson’s thesis[15] mentioned above used a similar idea to logical relations (q.v.) to relate the standard semantics to the collecting semantics via a relation sim_{t}. However, its most fundamental contribution seems to be the formalisation of the notion of abstract interpretation of a meta-language term.

Recently, Jones and Mycroft [7] developed a theory of abstract interpretation for collecting the arguments with which functions may be called. This included a definition of abstraction as a semi-homomorphic property which lifted in the manner of logical relations to second-order objects. Abramsky[1] has applied (and further developed) the framework described here for strictness analysis of the typed λ-calculus thus simplifying the notation of [2] who gave the first satisfying account of strictness analysis for higher-order functions.

Finally (see also the discussion on the (α → β) relation in section 3) we must mention Dybjer’s[6] work on “domain algebras”. It is not yet clear as to how relevant this work is to abstract interpretation.

1.3 Organisation

Sections 2 and 3 explain our notation and develop the theory of abstraction relations. Section 4 shows how a language can be given a scheme of denotational meanings parameterised on certain key domains and (function) values. As examples we develop interpretations corresponding to call-by-name, call-by-value, the Hindley/Milner type checking algorithm and strictness analysis. This is followed by section 5 which uses abstraction relations to develop a general theory of relationship between interpretions. This framework can then be used to prove correct analyses based on such related interpretations. As an example the Hindley/Milner type system is proved correct. Section 6 shows how relations can be induced in different ways from a function between interpretations. Section 7 compares this work with the previous framework of power objects and adjoined functions. This is followed by section 8 which gives some category-theoretic thoughts. Finally, we end with some concluding remarks.

2 Notation, definitions

For any sets A, B we write A → B to denote the space of functions from A to B and A × B to denote their cartesian product. We write A + B for their disjoint union with associated injection functions in_{1} : A → (A + B) and in_{2} : B → (A + B). Similarly, R(A, B) will denote their set of relations {r ⊆ A × B}.

A cpo is a partial order with a least element and limits of all directed sets. The word domain will be used interchangeably.

We use these same symbols for the corresponding operations on cpo’s: → will then yield the space of continuous functions, × the cartesian product and + the separated sum. The cpo operations will be extended to act on partial orders (e.g. a set with equality) provided the result is a cpo. The set of relations R(A, B) between cpo’s A, B is just the set of relations on their underlying sets (note that we do not put a domain structure on R(A, B)).

3 Inclusive predicates

In this section we will consider what objects might be used to relate usefully two different meanings of a given program. Similar objects occurring in the literature (although used for different purposes) are:

• Inclusive predicates which were independently developed by Milne (see [19] for more details) and Reynolds (e.g. [17]) who calls them directed complete relations. Both definitions really are that of admissible predicate up to the difference between “directed set complete” and “chain complete”. However, both Milne and Reynolds then proceed to use these words with the extra understanding that the inclusive predicates or directed complete relations used are actually logically defined in the sense of Plotkin below and may also be used on recursive domain definitions. So much so that the words “inclusive predicate” often seem to take the additional meaning of “possibly self-referential” as we see in Mulmulmey’s work[11] which discusses these objects and their existence at some length. Gordon[8] uses similar techniques.

• Logical relations were introduced by Plotkin [16] to refer to the related concept of relations defined inductively over (non-recursive) type structure, in the manner explained below.

Nielson[15] uses similar ideas in the definition of his sim_{t} predicate for relating the standard and collecting interpretation but does not explain how his definitions are related to the above.

We turn to summarising the ideas involved. Let A, A′, B, B′ be sets. Given functions α : A → A′ and β : B → B′ it is easy to induce functions (α + β) : (A + B) → (A′ + B′) and (α × β) : (A × B) → (A′ × B′) in a natural manner. However, it is not possible in general to induce a function (α → β) : (A → B) → (A′ → B′) since, considering (α → β) as the natural relation ∈ R(A → B, A′ → B′) defined by

f(α → β)f′ ⇔ (∀a ∈ A)(f′(α(a)) = β(f(a)))

turns out not to necessarily be a function.^{2} (Consider A = A′ = B = B′ = {0, 1} with α(x) = β(x) = 0 then any two functions f, f′ with f(0) = f′(0) = 0 are related).

However, Dybjer[6] considers a category of domain algebras in which this relationship is functional, but it is unclear whether his work can be applied to abstract interpretation. The exposition and references of his work are also useful.

This motivates Milne and Reynolds’ use (and our adoption) of relations since, using Reynolds’ notation, given R ∈ R(A, A′), S ∈ R(B, B′) we can define

R + S ∈ R(A + B, A′ + B′)
R × S ∈ R(A × B, A′ × B′)
R → S ∈ R(A → B, A′ → B′)

by

\begin{matrix}x(R + S)x′ ⇔ & \begin{matrix}(x = in_{1}(a) ∧ x′ = in_{1}(a′) ∧ aRa′) ∨ \\ (x = in_{2}(b) ∧ x′ = in_{2}(b′) ∧ bSb′) \end{matrix} \\ (a, b)(R × S)(a′, b′) ⇔ & aRa′ ∧ bSb′ \\ x(R → S)x′ ⇔ & (∀a ∈ A, a′ ∈ A′)(aRa′ ⇒ x(a)Sx′(a′)) \end{matrix}

One may check that if R and S are relations representing functions then the first two constructions embody the suggested definitions earlier.

2Universal algebraists note that this is just a special case of an algebra and shows that homomorphisms as we know them do not naturally appear in higher-order algebra.

Now let us suppose that A, A′, B, B′ are domains. The definitions of R × S and R → S go through unchanged, with pleasant properties such as

\begin{matrix}=_{A} × =_{B} = & =_{A×B} & =_{A} → =_{B} = & =_{A→B} \\ ⊑_{A} × ⊑_{B} = & ⊑_{A×B} & ⊑_{A} → ⊑_{B} = & ⊑_{A→B} \end{matrix}

However, for R + S ∈ R(A + B, A′ + B′) there are three distinct natural choices, viz:

x(R +^{L} S)x′ ⇔ x = ⊥ ∨ x(R +^{X} S)x′
x(R +^{M} S)x′ ⇔ (x = ⊥ ∧ x′ = ⊥) ∨ x(R +^{X} S)x′
x(R +^{U} S)x′ ⇔ x′ = ⊥ ∨ x(R +^{X} S)x′

where

x(R +^{X} S)x′ ⇔ \begin{matrix}(x = in_{1}(a) ∧ x′ = in_{1}(a′) ∧ aRa′) ∨ \\ (x = in_{2}(b) ∧ x′ = in_{2}(b′) ∧ bSb′) \end{matrix}

The second one corresponds to Nielson’s sim_{t} definition, but there are strong reasons for believing that +^{L} and +^{U} (read lower and upper) are relevant to dataflow analysis. For example if we are deriving computable abstract meanings to the semantics of a program, then given undecidability, we must inevitably confuse certain looping programs with certain halting programs.^{3} See section 6.1. The existence of this choice seems to stem from the fact that the separated sum operation is not a domain co-product. The above definitions have the feature that the following equivalences hold, but in general no others hold:

⊑_{A} +^{L} ⊑_{B} = ⊑_{A+B}  =_{A} +^{M} =_{B} = =_{A+B}  ⊒_{A} +^{U} ⊒_{B} = ⊒_{A+B}

The next problem to face, and the one with which Milne, Reynolds and Mulmuley above concerned themselves, is the following. Suppose D = F_{A}(D) is a recursive domain definition of a domain D parameterised on a domain A and D′ = F_{A′}(D′) is a similar definition of D′. Now suppose that we have a relation R ∈ R(A, A′). Can we lift this to a relation in R(D, D′) in a manner similar to the above treatment (and which could immediately be used if F (D) did not depend on D). We consider a special case of this in section 6.1. Warning: Note that since there is no domain structure on the set of relations it is possible to write recursive ‘definitions’ of such relations which are plausible only at first sight. Mulmuley[11] discusses this in some detail, including (essentially) the following example: given a domain D = (D → D) then there is no predicate P (in this context the real analogy is a relation ∈ R(D, {·}) for some one point set) such that

P (d) ⇔ (∀d′ ∈ D)(P (d′) ⇒ d(d′) = λx.x)

In this paper we do not need to insist that all the relations we consider are admissible since we do not consider a fixpoint operator. The use of admissibility is to ensure that relations behave properly at limits implied by the standard fixpoint operator.

For our purposes, that of relating two different semantics of a programming language, this notation becomes rather clumsy, and we follow Nielson in adopting a variant of Plotkin’s notation for logical relations[16].

3This implies that computable interpretations are liable to identify certain convex sets of values in the manner of the Egli-Milner ordering, but this property is not built into the notion of abstraction as it has been previously.

Let ι_{1}, …, ι_{n} be symbols (to be interpreted as A, A′ etc.) representing base types. The set of meta-language types is the closure of ι_{1}, …, ι_{n} under the binary syntactic operations +, ×, →. Given any spaces (sets or domains) A = (A_{1}, …, A_{n}) we can interpret any type σ as a space [σ]A by the definition

[ι_{i}]A = A_{i}  [σ + τ]A = [σ]A + [τ]A
[σ × τ]A = [σ]A × [τ]A  [σ → τ]A = [σ]A → [τ]A

Note that here, and below, the left-hand side use of +, ×, → represents syntax and the righthand side a function.

Suppose we have two such interpreting spaces A, A′ and a family of relations indexed by types R_{σ} ∈ R([σ]A, [σ]A′) then we say that (R_{σ}) is a logical relation if

R_{σ+τ} = R_{σ} + R_{τ}  R_{σ×τ} = R_{σ} × R_{τ}  R_{σ→τ} = R_{σ} → R_{τ}

Clearly we can induce a logical relation from its subfamily (R_{ι_{i}}).

This notation enables us to treat the type as a subscript indicating which relation to choose and this naturally puts the emphasis on the relation rather than its construction from base relations. Moreover, rather than writing (e.g.) R_{ι_{1}→ι_{2}} we will often write R_{A_{1}→A_{2}} to stand for the relation ∈ R(A_{1} → A_{2}, A′_{1} → A′_{2}) We will further abuse this notation by omitting the subscript entirely when it is clear from context.

From now on no further mention will be made of meta-language types to avoid confusion with the types we give to the language Exp in section 4.3.

4 The lambda calculus and its semantics

We give a class of denotational semantics (parameterised on certain domains and operators) to the untyped λ-calculus in the following form (we choose the λ-calculus as being the simplest programming language with higher-order objects). Let x range over a set Var of variables, then the class Exp of expressions (ranged over by e) conforms to the syntax:

e ::= x | λx.e | e e′

For this treatment constants are presumed to be pre-bound variables.

Definition

An interpretation I is a triple (D_{I}, lam_{I}, app_{I}) where D is a cpo and lam : (D → D) → D and app : (D × D) → D are continuous functions. (We drop the subscripts when the context is clear.) Given an interpretation (D, lam, app) we can define the notion of environment (over D) by

Env_{D} = Var → D

We use the letter ρ to range over environments. Such an interpretation, I, naturally defines an associated semantics

E_{I} : Exp → Env_{D} → D

in the following manner:

E[[x]]ρ = ρ(x)
E[[λx.e]]ρ = lam(λd ∈ D. E[[e]]ρ[d/x])
E[[e e′]]ρ = app(E[[e]]ρ, E[[e′]]ρ)

When considering static program analysis we can consider D as a set of data desciptions, then lam encodes the natural view of a lambda term (as a function from input descriptions to output descriptions) in terms of a description itself. app reverses this process.

4.1 Example

The standard interpretation, CBN, of the (call-by-name) untyped λ-calculus with (integer) constants is given by (V, lam, app) where V is the solution of the recursive domain equation

V = Z + (V → V)

where Z is the set of integers and + denotes the separated sum with associated injection functions

in_{Z} : Z → V, in_{F} : (V → V) → V

lam and app are then defined by

\begin{matrix}lam(f) = in_{F} (f) \\ app(d, d′) = case d of \begin{matrix}⊥ ⇒ ⊥ \\ in_{Z}(n) ⇒ ⊥ \\ in_{F} (f) ⇒ f(d′) \end{matrix} \end{matrix}

For the purposes of showing the correctness of type checking (more precisely to show that omission of run-time type tags implied by the separated sum above is valid) it is useful to have a related interpretation CBN* in which type errors lead immediately to an error stop. We define, following Milner, CBN* = (V, lam, app) where V is now the solution of the recursive domain equation

V = Z + (V → V) + {wrong}

and + denotes the ternary separated sum with associated injection functions

in_{Z} : Z → V, in_{F} : (V → V) → V, in_{W} : {wrong} → V

lam and app are similarly defined by

\begin{matrix}lam(f) = in_{F} (f) \\ app(d, d′) = case d of \begin{matrix}⊥ ⇒ ⊥ \\ in_{W} (wrong) ⇒ in_{W} (wrong) \\ in_{Z}(n) ⇒ in_{W} (wrong) \\ in_{F} (f) ⇒ f(d′) \end{matrix} \end{matrix}

Note that we could have easily defined call-by-value interpretations CBV and CBV*, the latter by changing f(d′) in CBN* to

case d′ of \begin{matrix}⊥ ⇒ ⊥ \\ in_{W} (wrong) ⇒ in_{W} (wrong) \\ in_{Z}(n′) ⇒ f(d′) \\ in_{F} (f′) ⇒ f(d′) \end{matrix}

and similarly for CBV from CBN.

4.2 Remarks

Given Γ a subset of {α, β, η} we say that an interpretation I is a Γ-model of the λ-calculus if, for all γ ∈ Γ and for all e, e′ ∈ Exp such that e and e′ are 1-step γ-convertible we have that E_{I}[[e]] = E_{I}[[e′]].

The definition of the semantics in terms of such an interpretation guarantees that all interpretations are α-models. However, as we might expect for the λ-calculus with constants many interpretations such as CBN are not η−models. Moreover, interpretations such as CBV and HM discussed below are not β-models. (The latter corresponds to the difference in type checking rules for let x = e in e′ and (λx.e′)e in [10].) The interpretations CBN and CBN* are αβ-models.

An interpretation will, in general, preserve β-convertibility only if

app(lam(f), x) = f(x)

Similarly, η-convertibility will only be preserved in general if

lam(λx.app(d, x)) = d

[As an aside, if we write \overline{app} for the curried version λd.λd′.app(d, d′) of app then the above sufficiency conditions reduce to

\overline{app} ∘ lam = 1_{(D→D)} and lam ∘ \overline{app} = 1_{D},

the classical isomorphisms in D = (D → D). The above conditions are not necessary due at least to the possibility that elements of D which are not used as interpretations of λ-terms cause them to fail.]

4.3 The Hindley/Milner polymorphic interpretation

Hindley[9], for the case of combinatory logic, and Milner[10] (also together with Damas[4]), for a programming language based on the λ-calculus, give a method of ascribing a certain type scheme to expressions. (For full details of the usual framework of this work the reader is referred to the above references.) These type schemes are principal in that they subsume all other types which may be inferred for a given expression. To make this possible, we have to introduce a set of type variables ranged over by α, β, … and then introduce a class of types and type schemes (ranged over by τ, σ respectively). These satisfy the syntax:

\begin{matrix}τ : type ::= α | int | τ → τ′ \\ σ : typescheme ::= τ | ∀α.σ \end{matrix}

Note that → above is used as a constructor function (another name for a cartesian product) and not as a function space. For this reason many logic texts use F instead.

We call a type or type scheme closed if it contains no free type variables. We often use the conventional wording that a monotype is a closed type. We say τ is a (generic) instance of σ, written τ ≤ σ, if τ may be obtained from σ by substituting types for quantified type variables subject to the usual rules about name clashes.

A type environment or type assumption ranged over by η is simply a map Var → typescheme. It is closed if it maps each variable into a closed type scheme. Inference rules are now given (for atomic statements of the form η ⊢ e : σ meaning under assumptions η we can ascribe type scheme σ to e). In the simple case we consider they may be written:

η ⊢ e : σ ; \overline{η ⊢ e : τ} if τ ≤ σ  (type specialisation)

η ⊢ e : σ ; \overline{η ⊢ e : (∀α.σ)} if α is not free in η (type generalisation)

\overline{η ⊢ x : σ} if σ = η(x)  (variable)

\underline{η ⊢ e : (τ′ → τ) η ⊢ e′ : τ′} ; η ⊢ (e e′) : τ  (application or → elimination)

η[τ/x] ⊢ e : τ′ ; \overline{η ⊢ (λx.e) : (τ → τ′)}  (λ-abstraction or → introduction)

The first two rules merely concern how polymorphic types behave and the last three are defined structurally on λ-terms. We would like to express this type system as an interpretation. In doing this we find that the particular (finitary) representation of type schemes using type variables and quantification tends to get in the way, and we choose an alternative representation using sets of monotypes. This also has the advantage that we could compare the expressiveness of various type systems by representing them both within the same framework.

Let M be the set of monotypes above. Let S = P(M) be the powerset of the set of monotypes. S is to be ordered by reverse inclusion (⊑=⊇) and as such is a cpo. In our framework members of M play the role of types and members of S play the role of type schemes. Observe that there is a natural injection of the set of closed type schemes into S which maps a type onto its set of closed generic instances. We refer to this map as Ground.

We make S into an interpretation by defining functions lam and app in the following manner:

\begin{matrix}lam(f) = \{(t → t′) | t ∈ M ∧ t′ ∈ f(\{t\})\} \\ app(s, s′) = \{t ∈ M | (∃t′ ∈ M)((t′ → t) ∈ s ∧ t′ ∈ s′)\} \end{matrix}

We use HM to refer to this interpretation.

Remarks

The definitions of lam and app in HM are essentially transcribed from the Hindley/Milner inference rules above, with the translation of the type-deduction relation as a map into the powerset S and the use of singleton sets (in lam) to represent the special treatment of λ-bound variables as types rather than type schemes (the generic/non-generic distinction).

Further, we really do reconstruct the Hindley/Milner type system: in practice, one only ever uses the above inference rules to deduce η ⊢ e : σ in the situation where η is closed and σ is most general. Now most general types infered from a closed type environment are themselves closed. So, supposing η is a closed type environment and letting σ temporarily range over closed type schemes, then we have

E_{HM}[[e]](Ground ∘ η) = ⋃{Ground(σ) | η ⊢ e : σ}

Proof

It suffices to show that

E_{HM}[[e]](Ground ∘ η) = {τ | η ⊢ e : τ, τ a monotype}

as we can end each deduction of η ⊢ e : σ with the type specialisation rule to yield η ⊢ e : τ for any τ ∈ Ground(σ). This we show by

1. For all τ ∈ E[[e]](Ground ∘ η) we have η ⊢ e : τ, by structural induction on e.

2. For all deductions η ⊢ e : τ we have that τ ∈ E[[e]](Ground ∘ η). This is due to the fact that any derivation of η ⊢ e : τ can be transformed into a ground derivation (i.e. one where every τ′ encountered in a consequent η′ ⊢ e′ : τ′ is also ground, excepting the variable rule). We now merely show inductively (over the deduction tree) that at each stage τ′ ∈ E[[e′]](Ground ∘ η′).

Corollary

As a rather trivial but illuminating corollary based on the property of most-general types we have that if σ is the most general type for e under η then

E_{HM}[[e]](Ground ∘ η) = Ground(σ).

4.4 Example: strictness analysis

We can define an interpretation corresponding to strictness analysis for higher-order functions in this scheme by using the domain

H = {⊤} + (H → H)

where + as before is the separated sum with injections in_{1}, in_{2}. H can be made into an interpretation SA = (H, lam, app) by defining

\begin{matrix}lam(f) = in_{2}(f) \\ app(h, h′) = case h of \begin{matrix}⊥ ⇒ ⊥ \\ in_{1}(⊤) ⇒ in_{1}(⊤) \\ in_{2}(f) ⇒ f(h′) \end{matrix} \end{matrix}

[If we wish to make the natural identification for stictness analysis of ⊤ and λx.⊤ then it is natural to use the domain H′ = (H′ → H′)_{⊥} instead of H above (and of course modifying lam, app appropriately).]

5 Abstraction

We say that an interpretation I′ = (D′, lam′, app′) is an ABS-abstraction^{4} of I = (D, lam, app), written I ⊳_{ABS} I′ if the following conditions hold

1. ABS ∈ R(D, D′). We often write ABS as ABS_{D}.

4Compare the notion of “homomorphic image”.

2. lam ABS_{(D→D)→D} lam′

3. app ABS_{(D×D)→D} app′

In the following we also assume that ABS is extended to the equality relation in R(Var, Var) and write this as ABS_{Var}.

The essential thing about abstraction is that it is a local property of interpretations which lifts to a property of the induced semantics and hence of all programs that can be written in Exp:

Proposition (correctness of abstraction)

(∀e ∈ Exp)(∀ρ ∈ Env_{D}, ρ′ ∈ Env_{D′})(ρ ABS_{Var→D} ρ′ ⇒ E_{I}[[e]]ρ ABS_{D} E_{I′}[[e]]ρ′)

or, more succinctly,

(∀e ∈ Exp)E_{I}[[e]] ABS_{Env_{D}→D} E_{I′}[[e]]

Proof

By structural induction on e. The base case of e = x is true a fortiori due to the assumption on ρ and ρ′. So inductively assume the proposition is true for all ρ, ρ′ (satisfying ρABSρ′) and all e subterms. We have d ABS_{D} d′ ⇒ ρ[d/x] ABS_{ENV_{D}} ρ′[d′/x] and hence

(λd ∈ D. E[[e]]ρ[d/x]) ABS_{D→D} (λd′ ∈ D′. E[[e]]ρ′[d′/x])

Now, by the assumption lamABSlam′ the result holds for λx.e. The case for e e′ is similar.

Remarks

The proof of this proposition can be better seen as an induction over meta-language terms together with the homomorphic (structural) definition of E[[.]]. As such the induction duplicates [16, proposition 1]. A similar theorem occurs within [15, theorem 3.3:14].

Unfortunately, in this framework there seems to be no a priori reason why the composition of abstraction relations should itself be one. I.e. given I ⊳_{ABS} I′ ⊳_{ABS′} I′′ then in general it is unclear whether there is any systematic manner of obtaining ABS′′ such that I ⊳_{ABS′′} I′′. Certainly, there is no reason why (ABS ∘ ABS′)_{D→D} should equal ABS_{D→D} ∘ ABS′_{D→D}.

This proposition (in various guises) appears again and again in program analysis. Special cases are the safety criterion in dataflow analysis and also the requirement of semantic soundness of Milner[10], to which we now turn.

5.1 HM abstracts CBN*

Let us assume that CBN* = (V, lam, app) and HM = (S, lam′, app′), and that S = P(M) as in section 4.3. We define a map (following Milner [10]) Ideal : M → P(V), the power set of V, by

\begin{matrix}Ideal(int) = \{⊥\} ∪ \{in_{Z}(n) | n ∈ Z\} \\ Ideal(t → t′) = \{⊥\} ∪ \{in_{F} (f) | f ∈ (V → V) ∧ f(Ideal(t)) ⊂ Ideal(t′)\} \end{matrix}

This now lifts to a map Ideal : S → P(V) by defining Ideal(S) = ⋂_{M∈S} Ideal(M) = ⨆_{M∈S} Ideal(M). Note that if S is empty we accordingly take Ideal(S) = V, i.e. that an ill-typed program can return any value, including in_{W} {wrong}. Ideal(s) is the ideal corresponding to type scheme s.

We now can define ABS by

v ABS s ⇔ v ∈ Ideal(s)

Specialising the “correctness of abstraction” proposition above leads to

(∀e ∈ Exp) \begin{matrix}(∀ρ ∈ (Var → V), η ∈ (Var → S)) \\ (((∀x ∈ Var)ρ(x) ∈ Ideal(η(x))) ⇒ E_{CBN*}[[e]]ρ ∈ Ideal(E_{HM}[[e]]η)) \end{matrix}

which is essentially Milner’s semantic soundness condition relating type-checking to evaluation.

5.2 Relationship of CBN and CBV

As in the above we find that CBN, CBV are related by CBN ⊳_{⊒} CBV where ⊒ is the (inverse) ordering on D_{CBN} = D_{CBV}. This result is just the statement that call-by-name (normal order) evaluation yields a more defined result than call-by-value (applicative order) evaluation. It is simply shown by observing that lam_{CBN} = lam_{CBV} and that app_{CBN} ⊒ app_{CBV}.

6 Inducing ABS-relations from functions

Many abstraction relations, as in the two examples above, are indeed induced from functions. Here we do not mean the “usual” abstraction functions ∈ P(D) → D′ but the direct ones ∈ D → D′. For the relationship with the former kind see section 7. We show there is a choice of ways in which this can be done. Firstly, let us say a relation R is LU-closed if y ⊑ x R x′ ⊑ y′ ⇒ y R y′. Similarly we say it is UL-closed if y ⊒ x R x′ ⊒ y′ ⇒ y R y′. It is convenient to think of LU- and UL-closed relations as generalised orderings.

Suppose that we have a (continuous) function abs : D → D′. We can induce relations abs^{L}, abs^{M}, abs^{U} ∈ R(D, D′) by defining

d abs^{L} d′ ⇔ abs(d) ⊑ d′  d abs^{M} d′ ⇔ abs(d) = d′  d abs^{U} d′ ⇔ abs(d) ⊒ d′

Then abs^{L} is LU-closed and abs^{U} is UL-closed. Moreover, this process is invertible in that the relations each determine the function. Defining an abstraction relation to be principal if it is induced as abs^{L} or abs^{U} from a function abs then generalises the notion of the principal type (amongst all types) of a value.

For example, given ABS above ∈ R(D_{CBN*}, D_{HM}) define abs : D_{CBN*} → D_{HM} by abs(d) = ⋃{s | d ABS s} then ABS = abs^{L}. Similarly ABS ∈ R(D_{CBN}, D_{CBV}) of the previous section is r^{U} induced from the retraction function r : D_{CBN} → D_{CBV} (note D_{CBN} = D_{CBV}) defined by

r(d) = case d of \begin{matrix}⊥ ⇒ ⊥ \\ in_{Z}(n) ⇒ in_{Z}(n) \\ in_{F} (f) ⇒ in_{F} (λd′ ∈ D_{CBV} .d′ = ⊥ → ⊥, r(fd′)) \end{matrix}

CBN* can be related to CBN by a similar retraction unstar : D_{CBN*} → D_{CBN} given by

unstar(d) = case d of \begin{matrix}⊥ ⇒ ⊥ \\ in_{W} (wrong) ⇒ ⊥ \\ in_{Z}(n) ⇒ in_{Z}(n) \\ in_{F} (f) ⇒ in_{F} (λd′ ∈ D_{CBN}.unstar(fd′)) \end{matrix}

Then CBN* ⊳_{unstar^{U}} CBN. A similar relationship holds for CBV* and CBV.

6.1 Inducing relations on recursive domains – strictness analysis

Certain interpretatations, e.g. the strictness analysis, SA and call-by-name CBN,CBN* interpretations presented above, have the property that their underlying domains are closely related. If we have two interpretations I = (D, lam, app) and I′ = (D′, lam′, app′) with

D = A + (D → D) D′ = A′ + (D′ → D′)

and an abstraction relation R ∈ R(A, A′) then we would like to lift R to a relation R^{∗} ∈ R(D, D′). The question is therefore as to whether there exists such an R^{∗} such that R^{∗} = R + (R^{∗} → R^{∗}) and, if so, whether it is unique. Formally we should require R^{∗} = Φ ∘ (R + (R^{∗} → R^{∗})) ∘ Φ^{−1} where Φ is the relation corresponding the the pair of isomorphisms ϕ : A+(D → D) → D and ϕ′ : A′ +(D′ → D′) → D′. Of course, as we mentioned in section 3, there are three choices for the + symbol in the above. So let us try to find relations

R^{♯} = R +^{L} (R^{♯} → R^{♯}) R^{♭} = R +^{U} (R^{♭} → R^{♭})

These, if they exist, would correspond to the ♯ and ♭ strictness analysis interpretations of [12] (part of [13]) provided merely that R is the universal relation in R(Z, {⊤}) corresponding to the function λn.⊤. Note how the difference between the interpretations is determined by the choice of + construction rather than by R.

The natural way to construct R^{♯}, R^{♭} is by essentially the inverse limit construction. Let R^{∗} stand for R^{♯} or R^{♭} and + for +^{L} or +^{U} respectively. Suppose D^{n}, D′^{n} are the nth iterates of the above recursive domain equation (with D^{0} = D′^{0} = {⊥}). Elements of D can now be considered to be certain members of ∏_{i} D^{i}. We can lift a relation R^{n} ∈ R(D^{n}, D′^{n}) to R^{n+1} by the usual logical relation definition, i.e. R^{n+1} = R_{A+(D→D)}^{n}, with R^{0} = {(⊥, ⊥)}. One can now consider R^{n} as a restriction of R^{n+1} via the retraction (this is a non-trivial lemma to be proved) and take the limit R^{∗} determined by (d_{0}, …)R^{∗}(d′_{0}, …) ⇔ (∀i)d_{i}R^{i}d′_{i}. Now we need to show that R^{∗} satisfies the equation for R^{♯} or R^{♭} above.

At the time of writing this proof of existence and uniqueness of R^{♯}, R^{♭} has not been done. It seems that the best way to treat this generally would be to generalise Mulmuley’s

“predicate domains” to “relation domains” (D, D′, R) where D, D′ are domains and R ∈ R(D, D′) and then define continuous operations +^{L}, +^{M}, +^{U}, ×, → (corresponding to his predictors) on them.

Abramsky[1] considers in much more detail the issue of strictness analysis in the framework of the typed λ-calculus.

7 Comparison with the power object and adjoined function framework

We first consider the conventional framework for abstract interpretation. (In this section most of the definitions are taken from [15] as representing the most up-to-date and most general treatment.)

We have two domains of standard values V_{1}, V_{2} and two domains L_{1}, L_{2} of abstract values. These domains interpret two sort symbols either as standard or abstract domains. Similarly, we have functions f : V_{1} → V_{2} and g : L_{1} → L_{2} representing standard and abstract interpretations of some function symbol. Moreover, we require some form of power object construction P(·) on V_{1} and V_{2} together with an associated map P(f) : P(V_{1}) → P(V_{2}). (This merely says that the power construction is a functor.) The domains P(V_{i}) and the function P(f) are refered to as the collecting interpretation although this is at some variance with the Cousots’ use of the term.

Additionally, we require that the P(V_{i}) and L_{i} each possess two orders (⊆, ⊑) with respect to which P(f) and g are monotonic. Typically a power object construction automatically provides ⊆ and ⊑, the latter by the Egli-Milner ordering since the V_{i} are domains. (We can recover the Cousot-style (termination ignoring) framework by taking P(·) to be the Hoare power domain in which ⊆=⊑ and L to be any complete lattice with ⊆ defined to be ⊑.)

Following [15, p. 258] we require that there are abstraction and concretisation functions

abs_{i} : P(V_{i}) → L_{i}, conc_{i} : L_{i} → P(V_{i})

which are both to be ⊑- and ⊆-monotonic and to further satisfy (for all s ∈ P(V_{i}), l ∈ L_{i})

(abs_{i} ∘ conc_{i})(l) ⊆ l and (conc_{i} ∘ abs_{i})(s) ⊇ s

Now, given the above set up, we say that f is abstracted by g if, for all l ∈ L_{1}, we have (conc_{2} ∘ g)(l) ⊇ (P(f) ∘ conc_{1})(l). This is [15, p. 253] and corresponds to safety in dataflow analysis. It is useful because it is preserved by composition and the taking of least fixpoints (modulo some conditions on the behaviour of ⊆ at ⊑-limits).

To show how this idea forms a special case of our framework we define relations ABS_{i} ∈ R(V_{i}, L_{i}) by

v ABS_{i} l ⇔ v ∈ conc_{i}(l)

(One should be a little careful with v ∈ conc_{i}(l) above — it is really just a shorthand for {v} ⊆ conc_{i}(l).)

The benefit is that the second-order relation “f is abstracted by g” above is now merely equivalent to f ABS_{1→2} g, the natural logically induced relation on functions spaces, defined by

f ABS_{1→2} g ⇔ (∀v ∈ V_{1}, l ∈ L_{1})(v ABS_{1} l ⇒ f(v) ABS_{2} g(l))

Proof:

(∀l ∈ L_{1})(conc_{2} ∘ g)(l) ⊇ (P(f) ∘ conc_{1})(l)
⇔ (∀l ∈ L_{1})(conc_{2} ∘ g)(l) ⊇ {f(v) | v ∈ V_{1} ∧ v ABS_{1} l}
⇔ (∀l ∈ L_{1})(∀v ∈ V_{1})(v ABS_{1} l ⇒ f(v) ∈ (conc_{2} ∘ g)(l))
⇔ (∀l ∈ L_{1})(∀v ∈ V_{1})(v ABS_{1} l ⇒ f(v) ABS_{2} g(l))

as required.

Note how the relational framework does not require power objects (the problem of defining suitable power objects has so far precluded general use of abstract interpretation when higher order objects are involved). Moreover, the homologue of the collecting interpretation is now the standard interpretation, which is in itself pleasing.

8 The view from Categoria

The fly in the ointment here is that logical relations do not necessarily compose (we are grateful to Samson Abramsky for warning of this particular pitfall). This seems to destroy the intuitive idea from abstract interpretation that abstracting an abstraction yields another abstraction. Perhaps a suitable restriction upon the abstraction relations we consider would recover this property without losing too many interpretations from the general framework.

There seem to be two categorical views which we would otherwise like to put upon all of this. The first is the conventional one that we are dealing with a category whose objects are interpretations and whose arrows are abstractions.

The other view, which probably ought to be investigated further, is that we are dealing with (cartesian closed) categories, certain subcategories of which are interpretations (having sets (with structure) for objects and functions for morphisms) and relating them together using abstraction relations as generalised functors.

9 Conclusions and further work

This work grew out of our increasing dissatisfaction with the complexity and mathematical (foundational) difficulty of the power domain and adjoined function approach to abstract interpretation. This idea was originally developed by one of the authors[13] and further developed with Nielson[14, 15]. However, we suspect that this (power domain) development may not endure.

The work presented here is a first attempt to both simplify the theory and to present a plausible theory of abstract interpretation for higher order objects. This is done by the use of relations instead of functions and power objects.

There are still many unanswered questions, such as

• There is a symmetrical treatment of the ABS relation. Surely there should be some characterisation as to which of two interpretations is ‘more concrete’. Surjectivity appears not to work. Similarly, the problem of composing abstraction relations needs to be tackled.

• The theory needs to be developed into a general framework for relating two different (but of the same ‘shape’) denotatational semantics of the same programming language possibly along the lines of [15].

• Can the theory presented here be generalised so that it includes classical notions such as (traditional or continuous) algebraic interpretation and homomorphism as a special case?

Acknowledgements

We would like to thank Samson Abramsky and Mike Gordon for their comments on an earlier version of this paper presented at the workshop on abstract interpretation at Kent University, Canterbury in August 1985 organised by Samson Abramsky, Chris Hankin and Richard Sykes. Thanks also to Harrald Ganzinger for helping to organise the Copenhagen workshop. Financial support for the two workshops was provided by the British Science and Engineering Research Council and by the Danish Natural Research Council.

References

[1] Abramsky, S. Strictness analysis based on logical relations. Unpublished manuscript, 1985.

[2] Burn, G., Hankin, C. and Abramsky, S. The theory and practice of strictness analysis for higher order functions. Imperial college report DoC 85/6, 1985. To appear in Science of Computer Programming.

[3] Cousot, P. and Cousot, R. Abstract interpretation: a unified lattice model for static analysis of programs by construction and approximation of fixpoints. Proc. ACM symp. on Principles of Programming Languages, 1977.

[4] Damas, L. and Milner, R. Principal type schemes for functional programs. Proc. ACM symp. on Principles of Programming Languages, 1980.

[5] Donzeau-Gouge, V. Utilisation de la sémantique dénotationelle pour l’étude d’interprétations non-standard. INRIA rapport 273, 1978.

[6] Dybjer, P. Domain Algebras. Lecture Notes in Computer Science: Proc. 11th ICALP, vol. 172, Springer-Verlag, 1984.

[7] Jones, N.D. and Mycroft, A. Dataflow of applicative programs using minimal function graphs. Proc. ACM symp. on Principles of Programming Languages, 1986.

[8] Gordon, M. Models of pure LISP. Ph.D. thesis, Dept. of Artificial Intelligence, Edinburgh University, 1973.

[9] Hindley, J.R. The principal type scheme of an object in combinatory logic. Transactions of the Amer. Math. Soc., vol 146, pp 29-60, 1969.

[10] Milner, R. A theory of type polymorphism in programming. JCSS 1978.

[11] Mulmuley, K. A mechanisible theory for existence proofs of inclusive predicates. CMU computer science report CMU-CS-85-149, 1985.

[12] Mycroft, A. The theory and practice of transforming call-by-need into call-by-value. Lecture Notes in Computer Science: Proc. 4th intl. symp. on programming, vol. 83, Springer-Verlag, 1980.

[13] Mycroft, A. Abstract Interpretation and Optimising Transformations of Applicative Programs. Ph.D. thesis, Edinburgh University, 1981. Available as computer science report CST-15-81.

[14] Mycroft, A. and Nielson, F. Strong abstract interpretation using power domains. Lecture Notes in Computer Science: Proc. 10th ICALP, vol. 154, Springer-Verlag, 1983.

[15] Nielson, F. Abstract interpretation using domain theory. Ph.D. thesis, Edinburgh University, 1984. Available as computer science report CST-31-84.

[16] Plotkin, G. Lambda definability in the full type hierarchy. In [18].

[17] Reynolds, J.C. Types, abstraction and parametric polymorphism. IFIP 83, (ed) R.E.A. Mason, North-Holland, 1983.

[18] Seldin, J.P., and Hindley, J.R. To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism. Academic Press, 1980.

[19] Stoy, J. Denotational semantics: the Scott-Strachey approach to programming language theory. MIT press, 1977.