Uniform PERs and Comportment Analysis

Alan Mycroft^{1} and Kirsten Lackner Solberg^{2}

1 Computer Laboratory, Cambridge University, New Museums Site, Pembroke Street, Cambridge CB2 3QG, United Kingdom

                        Alan.Mycroft@cl.cam.ac.uk

2 Dept. of Math. and Computer Science, Odense University, Denmark and DAIMI, Aarhus University, Denmark

                             kls@daimi.aau.dk

Abstract. Hunt showed that the notion of PER-based strictness properties subsumed the incomparable notions of ideal- and projection-based properties on non-lifted value spaces. We extend Hunt’s idea so it can encompass other comportment properties (such as totality) by separating the information and fixpoint orderings. We then define a class of uniform PERs (in the sense that they treat non-bottom ground elements, e.g. integers, identically) and then show how these can be hereditarily defined on function spaces. These (or subsets thereof) can be taken as a space of abstract values for abstract interpretation in the style of Nielson.

1 Introduction

Strictness properties are properties of functions between domains; in principle they are intended to capture the notion of how the function reacts to changes in the definedness of its arguments rather than changes between incomparable values of its arguments. A comparison to the notion of partial differentiation may prove fruitful. Since many properties conforming to this notion (e.g. totality) exclude ⊥, we use the word comportment property as coined by Cousot and Cousot [4] to avoid abusing the epithet “strictness property” by allowing it to encompass totality. Here comportment is considered within a denotational formalism.

This work started as an experiment to discover the expressive power of a natural notion of uniform PER as a basis for describing comportment properties. It transpires that the framework of “higher order abstract interpretation” in [4] describes a similar set of comportment properties after being specialised as in the second part of that work. The interest is that PERs in the traditional abstract interpretation framework can express similar properties as simple properties in the higher-order framework. We express no preference between these routes; the aim was to understand better PER-based properties. Moreover we do not discuss implementation complexity.

For many years there were two forms of strictness property, the ideal-based form and the projection-based form [8, 2, 12, 6, 5, 4]. Cousot and Cousot [3] consider a Galois connection view of strictness properties.

Given domains D and E and a continuous function f : D → E (the denotational semantics of a program function) these properties can be summarised as follows.

Let I range over the ideals of D (non-empty Scott-closed sets) and J over those of E. The ideal-based strictness properties are those of the form

W_{I,J}^{ideal}(f) ⇔ f(I) ⊆ J.

Similarly, let α range over projections on D (continuous, idempotent functions such that α(x) ⊑ x) and β over those on E. The projection-based strictness properties are those of the form

W_{α,β}^{proj}(f) ⇔ β ∘ f = β ∘ f ∘ α.

Hunt [6] observed that PER-based properties generalise both the above forms. (Actually Hunt only considered strict and inductive PER-properties which suffice for his generalisation but we relax this so as to be able to encompass as many comportment properties as possible.)

A PER P on D is a relation on D which is symmetric and transitive. It is inductive if it contains limits of chains when seen as a subset of D × D. Such a PER P defines a property W_{P}^{PER} on D given by its diagonal

W_{P}^{PER}(d) ⇔ d ∈ |P | where |P | = {d | dP d}.

Hunt essentially defines the PER-properties of functions in two stages, first defining the basic PER-properties and then the PER-properties as the conjunctive completion (meet completion) of these. Letting P range over (a class of, see below) PERs of D and Q over (a class of) PERs of E, the basic PER-properties appear as

W_{P,Q}^{basic-PER}(f) ⇔ (∀x, y ∈ D)(xP y ⇒ (fx)Q(fy)).

Conjunctions (intersections) of these give PER-properties.

The reader familiar with the presentations of abstract interpretation in the style of Nielson or Burn, Hankin and Abramsky et al. will here note an absence of specifying how the properties at higher-order are related to those at lowerorder (or first-order). Indeed, Cousot and Cousot argue that the framework of abstract interpretation should leave this unspecified; only particular examples instantiating the framework should do this (see e.g. the two parts of [4]). In general the argument is that the framework should allow one to select representations for program properties at each type independently; all that is required is that function properties, ranged over by C, should be in Galois correspondence γ : C → P(D → E) where P(·) is the power-set construct. This yields properties

W_{C}^{Galois}(f) ⇔ f ∈ γ(C).

This paper leans towards the framework propounded by Nielson [9]. Here the framework requires that the properties on higher types are related to those on lower types (albeit possibly in different ways for different uses of a given type). This framework is tighter in that is forbids the parasitic possibility that, e.g., the space of properties for a type depends uncomputably on its type structure. On the other hand the attempt to forbid ‘unreasonable’ interpretations in the framework generally requires the framework to be repeatedly enhanced when desirable interpretations are found not to fit.

One can, perhaps over-simplistically, observe that the former view approach is platonic in that it prescribes a framework and then searches for instances which explain or yield various analyses (these instances appear always to have been decidable). Similarly the effect of the latter approach has generally been constructivist: abstract spaces have been crafted which explain exactly the range of phenomena at hand; abstract spaces for higher types are expected to be derivable from those at lower types (cf. intuitionistic implication). The old arguments transfer beautifully: the Platonist argues that the constructivist is doomed to extend his constructions each time the world demands (and never models it perfectly); the constructivist chides the generality of the Platonist for allowing parasitic solutions which have no application or physical reality.

The present construction of uniform PERs, both at ground type and hereditarily at higher types, is designed to capture as many comportment properties as possible (hopefully all) in a constructive manner. It was developed concurrently with [4] and attempts to capture comportments from the constructive, as opposed to platonic, viewpoint. Interestingly the two approaches differ (ours yields four extra properties at type Int → Int). These are accounted for by the fact that uniform PERs naturally separate the notion of a function being total from it being constant; the application in [4] does not. Certainly, it is possible to imagine a variant of each which models the other.

The range of comportment properties expressible by uniform PERs include not only strictness properties but also totality properties. These latter are also captured by the annotated type system of Solberg et al. [10]. Note also the independent work by Benton [1] and Jensen [7] on expressing strictness properties in logical form.

1.1 Overview

In Section 2 we recall the definition of PERs then define the subset and Egli-Milner orderings on PERs.

Section 3 defines the notion of uniform PER on the integers. These PERs are uniform in the sense that they treat all the integers identically (as in [5]). We observe that some of the uniform PERs on the integers are not strict. Far from being a problem these non-strict PERs describe the property of being a non-bottom value (or at higher types being a total function) in contrast to most work on ideal- or projection-based program analysis (subject to the unsurprising need to use the Egli-Milner ordering on PERs which we define). The empty PER also appears as a uniform PER but is not proscribed because of its possible use to represent some sort of dead code. Next we form following Hunt the PERs on the function space and again we observe that some of these are not strict.

In Section 4 we take a closer look at the uniform PERs on ZZ_{⊥} → ZZ_{⊥}. It appears that we are able to express all the properties that are expressible with ideal-based [5, 8], projection-based [12], and rule-based [1, 10] program analyses. Some new properties also emerge, e.g. the property of being constant on the integers, the property of being non-bottom on the integers, the property of being constant and non-bottom on the integers, the property of being non-bottom on the integers or the bottom-function. These include the comportment properties of [4].

For each property there exists an optimisation that can be applied to the code implementing an expression with that property. So again we can see the advantage of also considering the non-strict PERs. Moreover for each property there exists a function which has that property as the best/most exact description of the expression.

The next step is to define the language in Section 5, its standard semantics, and a non-standard semantics for program analysis. We define the semantics and the program analysis as two different interpretations of the language (as in [6]). Following Hunt’s proof of correctness of the analysis we show that the standard and non-standard semantics of terms satisfy a ternary logical relation which relates pairs of standard values with an abstract value.

The final step is to define the abstract-denotations of the constants, e.g. if, fix, +, such that their standard-denotation is related to the abstract-denotation. The problems here is mostly for fix. Not all the PERs we are dealing with are strict therefore we cannot just follow Hunt using a union operator to form the fixpoint. (Starting with the least PER in the subset ordering (the empty PER) and applying the functional to it would result in the empty PER and hence the fixpoint would be the empty PER.) Following ideas dating from at least [8] we start with the least strict PER and a form of the Egli-Milner ordering which we define on PERs.

2 Formalism

We start by defining the notion of a PER on a set and then consider the possible orderings on PERs when the set has order-structure:

2.1 PERs on domains

Recall that a PER on a set S is a relation on S that is symmetric and transitive. Both the domain and range of the PER is equal to the diagonal-part of P, defined by |P | = {x | (x, x) ∈ P }. For a given set A of PERs, the properties associated with A are the set of diagonals of members of A. PERs can be ordered in at least two different ways: the subset ordering and the Egli-Milner ordering.

Definition 1 The subset ordering The PER P is less than or equal to the PER Q, written P ≤ Q, if P ⊆ Q.

2.2 The Egli-Milner ordering

The subset ordering does not take into account the structure of the domain on which the PERs are built. The least PER in the subset ordering is the empty PER. The result of applying a functional to the empty PER is the empty PER, therefore the fixpoint of a functional is the empty PER. What we want to do is to start with the least, strict, PER. But starting there may not yield a chain under the subset ordering. The obvious choice is to use the Egli-Milner ordering.

Let D be a cpo. We define the Egli-Milner ordering on the space of PERs over D by treating the PERs as subsets of D × D.

Definition 2 The Egli-Milner ordering on PERs over D Let P and Q be PERs over D. We define P ⊑_{EM}^{PER} Q if P ⊑ Q when considered as subsets of D × D, i.e.

(∀p ∈ P ∃q ∈ Q : p ⊑_{D×D} q) ∧ (∀q ∈ Q∃p ∈ P : p ⊑_{D×D} q).
□

We also define a PER P being strict and downwards closed by inheritance from D × D:

Definition 3 Strict and downwards closed PERs A PER P on D is strict if (⊥_{D}, ⊥_{D}) ∈ P; it is downwards closed P if it is downwards closed when seen as a subset of D × D, i.e.

((d_{1}, d_{2}) ⊑ (d_{3}, d_{4}) ∧ (d_{3}, d_{4}) ∈ P) ⇒ (d_{1}, d_{2}) ∈ P
□

For strict PERs (i.e. Hunt’s work) we would expect the subset ordering to coincide with the Egli-Milner ordering:

Lemma 4 Egli-Milner ordering on strict and downwards closed PERs For all strict PERs P on D and for all downwards closed PER Q on D:

P ⊑_{EM}^{PER} Q ⇔ P ≤ Q

Proof We assume P is a strict PER on D and that Q is a downwards closed PER on D. First we assume P ⊑_{EM}^{PER} Q and show P ≤ Q. We assume (x, y) ∈ P then from Definition 2 part one we get that there exits (x′, y′) ∈ Q such that (x, y) ≤ (x′, y′). Since Q is downwards closed it can be the case that x′ = x and y′ = y. Therefore we have that P is a subset of Q. Next assume P ≤ Q and show P ⊑_{EM}^{PER} Q. Since P is a subset of Q then for all (x, y) ∈ P we have (x, y) ∈ Q such that (x, y) ≤ (x, y) which is the first part of Definition 2. We have (⊥_{D}, ⊥_{D}) ∈ P since P is strict. Therefore for all (x, y) ∈ Q we have (⊥_{D}, ⊥_{D}) ≤ (x, y), which is the second part of Definition 2.

3 Uniform PERs on Types

Although the intuition is to define a class of uniform PERs associated with a domain it turns out to be more natural to define the classes of uniform PERs associated with (the standard interpretation of) a type. (For the purposes of abstract interpretation representations of these PERs can be used as abstract values and it is too restrictive to insist that (accidentally) isomorphic domains described by different types should have identical sets of abstract values). We will continue to refer to (e.g.) “the set of uniform PERs on ZZ_{⊥}” when this reads better.

We start with a set Σ, of types, ranged over by σ and τ:

σ ::= Int | σ → σ | σ × σ

For each type σ there is a standard domain D_{σ}^{S}:

DInt^{S} = ZZ_{⊥}  D_{σ→τ}^{S} = D_{σ}^{S} → D_{τ}^{S}  D_{σ×τ}^{S} = D_{σ}^{S} × D_{τ}^{S}

where → is continuous function space. We now define a PER on a type:

Definition 5 Let σ be a type, then P is a PER on σ if P is a PER on D_{σ}^{S}. □

For each type σ we now define a finite set of uniform PERs, U(σ), consisting of certain PERs on σ. A uniform PER on the integers is a PER on the standard domain of the integers which treats all the integers in the same way. The reason for only looking at uniform PERs is that in a comportment analysis we are typically interested in knowing whether an expression evaluates to an integer or undefined value—not about it being any particular integer. The uniform PERs on the integers are:

Definition 6 A PER P on Int is uniform if, whenever π is a permutation on ZZ_{⊥} (= DInt^{S}) leaving ⊥ unchanged, then ∀x, y ∈ ZZ_{⊥} : (x, y) ∈ P ⇔ (πx, πy) ∈ P. □

The set of uniform PERs on the integers, which we call U(Int), thus contains the following 7 elements:

• 1A = ∅
• 2A = {(x, x) | x ∈ ZZ}
• 3A = ZZ × ZZ

• 1B = {(⊥, ⊥)}

• 2B = {(x, x) | x ∈ ZZ_{⊥}}

• 3B = ZZ × ZZ ∪ {(⊥, ⊥)}

• 4 = ZZ_{⊥} × ZZ_{⊥}

and they are related by the subset ordering and the Egli-Milner ordering as in Fig. 1. For the strict PERs {1B, 2B, 3B, 4} we observe that the Egli-Milner ordering coincides with the subset ordering.

Note that U(Int) is intersection and union closed: intersection closedness is desirable for abstract interpretation as it ensures each (standard) value has a best abstract approximation. Union closedness ensures that no more information than necessary is lost on a merge resulting from if then else .

We define the uniform properties UP(σ) associated with σ in the obvious way:

[figure: 1A; 1B; 2A; 2B; 3A; 3B; 4; The subset ordering]

[figure: 1B; 2B; 3B; 4; 2A; 3A; The Egli-Milner ordering]

Fig. 1. The subset ordering and the Egli-Milner ordering on Int

Definition 7 To the set U(σ) of uniform PERs there is associated the set UP(σ) of properties:

UP(σ) = {|P | | P ∈ U(σ)}

□

The uniform properties of Int are as one might expect: UP(Int) = {∅, {⊥}, ZZ, ZZ_{⊥}}. These correspond exactly to the four values in [4], viz. ∅, ⊥, ⊥̸, ⊤. Note further that omitting PERs 2A and 2B from our definition of uniformity leads to the same property space on Int; moreover doing so seems to lead to the Cousots’ comportment property space on Int → Int.

Starting from U(Int) we will define uniform PERs on compound types. First we recall constructions which derive PERs at compound types from PERs of their components:

Definition 8 Given a PER P on σ and a PER Q on τ we can construct a PER P → Q on σ → τ as:

P → Q = {(f, g) ∈ D_{σ→τ}^{S} × D_{σ→τ}^{S} | (∀(a, b) ∈ P)(fa, gb) ∈ Q}

and a PER P × Q on σ × τ as:

P × Q = {((a, c), (b, d)) ∈ D_{σ×τ}^{S} × D_{σ×τ}^{S} | (a, b) ∈ P, (c, d) ∈ Q}

(Note these are particular PERs, not spaces of PERs.) □

Now we define the set of uniform PERs on compound types inductively. Doing so is facilitated by defining them mutually with a set of basic PERs.

Definition 9 The uniform PERs on compound types Given types σ and τ and their associated sets U(σ) and U(τ) of uniform PERs, we define, at type σ → τ, the set of basic PERs, B(σ → τ) as:

B(σ → τ) = {P → Q | P ∈ U(σ), Q ∈ U(τ)}

and the set of uniform PERs, U(σ → τ) as:

U(σ → τ) = {∩S | S ⊆ B(σ → τ)}.

Similarly we define, at type σ × τ, the set of basic PERs, B(σ × τ), as:

B(σ × τ) = {P × Q | P ∈ U(σ), Q ∈ U(τ)}

and the set of uniform PERs, U(σ × τ), as:

U(σ × τ) = {∪S | S ⊆ B(σ × τ)}.
□

In general B(σ → τ) is not intersection closed; hence the definition of U(σ → τ) as its intersection-closure. Note that U(σ → τ) is not union closed. We resist the temptation to form the union-closure at higher types not from any polemic grounds but from a desire to preserve the “abstract function spaces are function spaces on abstract values” property found in [2, 5, 6].

Fact 10 Let σ be a type and A and B be members of U(σ) then: A ∩ B ∈ U(σ) but in general A ∪ B ∉ U(σ). □

Section 4 considers the uniform PERs and properties on Int → Int and the need for intersection closure in some detail.

For Observation 12 below we need the following lemma:

Lemma 11 Intersections and unions For PERs P_{1}, P_{2}, … P_{n} on σ and one PER Q on τ:

(P_{1} ∪ P_{2} ∪ ⋯ ∪ P_{n}) → Q = (P_{1} → Q) ∩ (P_{2} → Q) ∩ ⋯ ∩ (P_{n} → Q)

Proof Let

P_{L} = (P_{1} ∪ P_{2} ∪ ⋯ ∪ P_{n}) → Q

and

P_{R} = (P_{1} → Q) ∩ (P_{2} → Q) ∩ ⋯ ∩ (P_{n} → Q)

We show P_{L} = P_{R} by the following chain of equivalences.

(f, f′) ∈ P_{R} ⇔ ∀i : [(d, d′) ∈ P_{i} ⇒ ((fd, f′d′) ∈ Q)]
⇔ (∀i : (d, d′) ∈ P_{i}) ⇒ ((fd, f′d′) ∈ Q)
⇔ ((d, d′) ∈ ∪P_{i}) ⇒ ((fd, f′d′) ∈ Q)
⇔ (f, f′) ∈ P_{L}

Observation 12 We have

U(σ_{1} × σ_{2} → τ)
= {∩S | S ⊆ B(σ_{1} × σ_{2} → τ)}
= {∩S | S ⊆ {P → Q | P ∈ U(σ_{1} × σ_{2}), Q ∈ U(τ)}}
= {∩S | S ⊆ {P → Q | P ∈ {∪S_{1} | S_{1} ⊆ B(σ_{1} × σ_{2})}, Q ∈ U(τ)}}

Consider the uniform PERs on σ_{1} × σ_{2} → τ but with the restriction that the product PERs involved are basic PERs. That is look at:

{∩S | S ⊆ {P → Q | P ∈ B(σ_{1} × σ_{2}), Q ∈ U(τ)}} = P_{B}

Now since we have B(σ) ⊆ U(σ) we arrive at U(σ_{1} × σ_{2} → τ) ⊇ P_{B}. Showing U(σ_{1} × σ_{2} → τ) ⊆ P_{B} completes the proof, so consider a PER in U(σ_{1} × σ_{2} → τ) in the form:

(P_{11} ⋯ ∪ P_{1n} → Q_{1}) ∩ ⋯ ∩ (P_{k1} ∪ ⋯ ∪ P_{kn} → Q_{k})

where P_{ij} ∈ B(σ_{1} × σ_{2}) and Q_{i} ∈ U(τ). By applying Lemma 11 we get

(P_{11} → Q_{1}) ∩ ⋯ ∩ (P_{1n} → Q_{1}) ∩ ⋯ ∩ (P_{k1} → Q_{k}) ∩ ⋯ ∩ (P_{kn} → Q_{k})

So we have that the PER is in P_{B} and therefore U(σ_{1} × σ_{2} → τ) ⊆ P_{B}. □

Following Observation 12, in this paper we restrict the types to the form

σ ::= Int | σ × ⋯ × σ → σ

(This has the sole effect of forbidding products in function results and is done to avoid arguments concerning appropriate properties for product values.) Indeed, we could have achieved much the same effect by treating such restricted use of product types as shorthand for curried functions. However the present formalism is more natural and enables us to discuss properties of products. Note that because of Observation 12, it suffices to consider B(σ × τ) instead of U(σ × τ) since the restriction means that all products appear to the left of function types.

4 Examples in Int → Int

As an example let us take a look at the basic and uniform on Int → Int. PERs on Int → Int are subsets of the standard domain of (Int → Int) × (Int → Int). Given two uniform PERs P and Q on Int a basic PER on the function space Int → Int can be constructed as:

P → Q = {(f, g) ∈ (ZZ_{⊥} → ZZ_{⊥}) × (ZZ_{⊥} → ZZ_{⊥}) | ∀(a, b) ∈ P ⇒ (fa, gb) ∈ Q}

The set of all basic PERs on the function space Int → Int is:

B(Int → Int) = {P → Q | P, Q ∈ U(Int)}

The set of all uniform PERs on the function space ZZ_{⊥} → ZZ_{⊥} is:

U(Int → Int) = {∩S | S ⊆ B(Int → Int)}

The reason why it is not sufficient only to use the basic PERs is that some expressions lack a least and best PER. Consider the term λx.if x = ⊥ then ⊥ else 42; we have that

(λx.if x = ⊥ then ⊥ else 42) ∈ |1B → 1B|

and

(λx.if x = ⊥ then ⊥ else 42) ∈ |3A → 2A|.

However, the greatest lower bound in the subset ordering of PERs of the form P → Q of the two PERs 1B → 1B and 3A → 2A is the PER 3B → 1A which is empty. One of the missing PERs is the greatest lower bound in the subset ordering of 1B → 1B and 3A → 2A.

The properties, UP(Int → Int), on Int → Int are:

   • empty  = ∅

• strcon  = {f ∈ ZZ_{⊥} → ZZ_{⊥} | (∀a, b ∈ ZZ : fa = fb ∈ ZZ) ∧ (f⊥ = ⊥)}
• ide  = {f ∈ ZZ_{⊥} → ZZ_{⊥} | (∀a ∈ ZZ : fa ∈ ZZ) ∧ (f⊥ = ⊥)}
• div  = {f ∈ ZZ_{⊥} → ZZ_{⊥} | ∀a ∈ ZZ_{⊥} : fa = ⊥}
• strcon|div = {f ∈ ZZ_{⊥} → ZZ_{⊥} | (∀a, b ∈ ZZ : fa = fb ∈ ZZ_{⊥}) ∧ (f⊥ = ⊥)}
• ide|div = {f ∈ ZZ_{⊥} → ZZ_{⊥} | (∀a ∈ ZZ : fa ∈ ZZ) ∧ f⊥ = ⊥} ∪ div
• strict  = {f ∈ ZZ_{⊥} → ZZ_{⊥} | f⊥ = ⊥}
• cgt  = {f ∈ ZZ_{⊥} → ZZ_{⊥} | ∀a, b ∈ ZZ_{⊥} : fa = fb ∈ ZZ}
• totcon  = {f ∈ ZZ_{⊥} → ZZ_{⊥} | ∀a, b ∈ ZZ : fa = fb ∈ ZZ}
• tot  = {f ∈ ZZ_{⊥} → ZZ_{⊥} | ∀a ∈ ZZ : fa ∈ ZZ}
• cgt|div = {f ∈ ZZ_{⊥} → ZZ_{⊥} | ∀a, b ∈ ZZ_{⊥} : fa = fb ∈ ZZ_{⊥}}
• totcon|div = {f ∈ ZZ_{⊥} → ZZ_{⊥} | ∀a, b ∈ ZZ : fa = fb ∈ ZZ_{⊥}}
• tot|div = {f ∈ ZZ_{⊥} → ZZ_{⊥} | ∀a ∈ ZZ : fa ∈ ZZ} ∪ div
• all  = {f ∈ ZZ_{⊥} → ZZ_{⊥}}

          [figure: empty; cgt; strcon^{∗}†; ^{totcon^{∗}}; ^{ide^{†}}; tot; div; cgt|div; strcon|div^{∗}†; ^{totcon|div^{∗}}; ^{ide|div^{†}}; tot|div; strict; all]

Fig. 2. The Subset ordering on UP(Int → Int)

and they are related by the subset ordering as in Fig. 2 and by the Egli-Milner ordering as in Fig. 3.

In the figures, names have been chosen to match [4] except that ‘cgt’ is used for ‘convergent’ leaving ‘con’ to indicate ‘constant’. Annotations: ^{†} indicates a PER added by conjunctive completion;^{∗} indicates a PER not in [4]. For PERs in [4] the ‘|’ character in the name indicates it is added by disjunctive completion. Note that [4] has an error in that ide|div ⊆ tot|div is omitted from the Hasse diagram.

We see that subset ordering coincides with the Egli-Milner ordering for

the strict PERs (div, cgt|div, strcon|div, totcon|div, ide|div, tot|div,

strict, and all). Also note that some of the PER-properties are Egli-Milner equivalent, viz.

                      totcon|div ≡_{EM} cgt|div
                          strict ≡_{EM} ide|div
                             all ≡_{EM} tot|div

This is also left unresolved in [4].

One question to be asked is: “are all these properties useful?”. A property is useful if an optimisation is possible only when it holds (or, indirectly, if it

        [figure: div; strcon|div^{∗}†; empty; totcon|div^{∗},cgt|div; strcon^{∗}†; strict,ide|div^{†}; all,tot|div; ^{totcon^{∗}}; ^{ide^{†}}; cgt; tot]

Fig. 3. The Egli-Milner ordering on UP(Int → Int)

is needed to avoid information loss when calculating such a property—cf. joint strictness). Let f be an expression with property:

empty falsity property—which no function possesses. strcon if the argument, a, is known to be an integer then f0 can be eval-

uated at compile-time and all these calls to f can be replaced by the result and if the argument is known not to terminate, then we can replace such calls with the result ⊥.

ide if the argument is known not to terminate, then we can replace the calls with the result ⊥ and in the case where we know that the argument, a, is an integer then fa can be evaluated at compiletime.

div replace all calls to f by the result ⊥. strcon|div if the argument is known not to terminate, then we can replace the

calls with the result ⊥ and if the argument, a, is known to be an integer then all such calls can be replaced by calls of e.g. f0.

ide|div Egli-Milner equivalent to its convex closure strict compared to

which there do not seem to be additional optimisations.

strict evaluate argument before call. cgt evaluate f⊥ at compile-time and replace all calls to f with that

result which is a terminating value.

totcon if the argument, a, is known to be an integer then f0 can be evaluated at compile-time and all such calls to f can be replaced by the result.

tot if the argument is known to be an integer then we can evaluate the

call at compile-time.

cgt|div replace all calls to f by f⊥; Egli-Milner equivalent to (and a subset

           of) totcon|div.

totcon|div if the argument, a, is known to be an integer then calls fa can be

replaced by calls of e.g. f0.

tot|div there appear no useful optimisations for this property (which is

perhaps unsurprising given that is it Egli-Milner equivalent to all).

all truth property—which all functions possess.

The next question to ask is: “Do there exist terms which have each of these properties?”. The term λx.4 has the property cgt and it does not possess any property less than cgt. The property cgt is the best description of the term. Similarly λx.⊥ has the property div which is the best. Temporarily suppose e′ is the term true⊕false where ⊕ denotes non-deterministic choice; then we can construct a term with the best property cgt|div viz. if e′ then λx.4 else λx.⊥. This argument is more delicate in the absence of such an operator since any such e′ must reduce to true, false or bot. However this fact is not discernible uniformly (for any analysis method there are undetectable tautologies) and hence for any analysis method there is such a term with best property cgt|div. The term fixλf.λx.if x=0 then 1 else f(x-1) has the property strcon as the best one. Now we are able to construct terms for the remainder as we did for the property

cgt|div.

5 Implementation use

We assume a simple typed functional language, whose object types coincide with (and are modelled by) the meta-language types above. Its syntax is

e = x | c | ee′ | λx.e′

where x ranges over variables and c over constants. Its semantics is given in terms of type-indexed semantic functions E_{σ}^{I} by

E_{σ}^{I}[[x]]ρ = ρx
E_{σ}^{I}[[c]]ρ = c^{I}
E_{τ}^{I}[[ee′]]ρ = app_{σ→τ}^{I} (E_{σ→τ}^{I} [[e]]ρ)(E_{σ}^{I}[[e′]]ρ)
E_{σ→τ}^{I} [[λx.e′]]ρ = lam_{σ→τ}^{I} (λd.E_{τ}^{I}[[e′]]ρ[d/x])

where c^{I} (including lam_{σ}^{I} and app_{σ}^{I}) are given by an interpretation which also specifies the interpretation of types as below.

For each type σ we have beside the standard domains D_{σ}^{S} an abstract domain D_{σ}^{A}. We will take D_{σ}^{A} to be the set of names of uniform PERs on σ; e.g. D_{σ}^{A} = N (σ). The names of the uniform PERs are defined as follows:

N (Int) = {1A, 2A, 3A, 1B, 2B, 3B, 4}

N (σ → τ) = {[n_{1}, m_{1}; …; n_{k}, m_{k}] | n_{i} ∈ N (σ), m_{i} ∈ N (τ), k = |N (σ)|}

in one name all the n_{i}’s are distinct N (σ × τ) = {(n, m) | n ∈ N (σ), m ∈ N (τ)}

Names on the function space σ → τ can be seen as a graph of a function from names on σ to names on τ. For each type there is a concretisation function γ_{σ} from the set of names of PERs on the type, N (σ), to the set of uniform PERs on the type, U(σ). (Hunt refers to this type-indexed family of maps as the logical concretisation map.)

γ_{σ} : N (σ) → U(σ)
γInt(1A) = ∅  γInt(1B) = {(⊥, ⊥)}
γInt(2A) = {(x, x) | x ∈ ZZ}  γInt(2B) = {(x, x) | x ∈ ZZ_{⊥}}
γInt(3A) = ZZ × ZZ  γInt(3B) = ZZ × ZZ ∪ {(⊥, ⊥)}
γInt(4) = ZZ_{⊥} × ZZ_{⊥}
γ_{σ→τ} ([n_{1}, m_{1}; …; n_{k}, m_{k}]) = (γ_{σ}n_{1} → γ_{τ} m_{1}) ∩ … ∩ (γ_{σ}n_{k} → γ_{τ} m_{k})
γ_{σ×τ} ((n, m)) = γ_{σ}n × γ_{τ} m

When using this representation (of functions by graphs) it is important to recall Hunt’s observation that the γ are not injective—two (extensionally) different functions between properties may describe the same PER on the function space.

The Egli-Milner ordering on names of uniform PERs is inherited from the Egli-Milner ordering on the uniform PERs:

Definition 13 Let n and m be in N (σ) then n ⊑_{EM}^{N} m if γ_{σ}(n) ⊑_{EM}^{PER} γ_{σ}(m); ⊔_{EM}^{N} is similarly inherited (and well-defined as N (σ) is finite and closed over lubs). □

Standard and PER name-based interpretations are given in Fig. 4. The application and projection functions are monotonic and continuous:

Lemma 14 The two families of functions app_{σ→τ}^{S} and app_{σ→τ}^{A} are monotonic with respect to ordering on the standard domain, ≤, and the Egli-Milner ordering on names of PERs, ⊑_{EM}^{N} , respectively.

Proof From domain theory we know that app_{σ}^{S} is monotonic. We prove that app_{σ}^{A} is monotonic by induction on the type σ. For details see Solberg’s PhD [11].

Lemma 15 The functions π_{1}^{S}, π_{1}^{A}, π_{2}^{S}, and π_{2}^{A} are monotonic with respect to ordering on the standard domain, ≤, and the Egli-Milner ordering on name of PERs, ⊑_{EM}^{N} , respectively.

π_{1}^{S} : D_{σ×τ}^{S} → D_{σ}^{S}
π_{1}^{S}((n, m)) = n
π_{2}^{S} : D_{σ×τ}^{S} → D_{τ}^{S}
π_{2}^{S}((n, m)) = m
app_{σ→τ}^{S} : D_{σ→τ}^{S} → D_{σ}^{S} → D_{τ}^{S}
app_{σ→τ}^{S} fx = fx
lam_{σ→τ}^{S} : (D_{σ}^{S} → D_{τ}^{S}) → D_{σ→τ}^{S}
lam_{σ→τ}^{S} f = f

fix_{σ}^{S} : D_{σ→σ}^{S} → D_{σ}^{S}
fix_{σ}^{S} f = ⊔ {d_{i}}
d_{0} = ⊥D_{σ}^{S}
d_{i+1} = app_{σ→σ}^{S} fd_{i}

π_{1}^{A} : D_{σ×τ}^{A} → D_{σ}^{A}
π_{1}^{A}((n, m)) = n
π_{2}^{A} : D_{σ×τ}^{A} → D_{τ}^{A}
π_{2}^{A}((n, m)) = m

app_{σ→τ}^{A} : D_{σ→τ}^{A} → D_{σ}^{A} → D_{τ}^{A}

app_{σ→τ}^{A} [n_{1}, m_{1}; …; n_{k}, m_{k}]n_{i} = m_{i}

lam_{σ→τ}^{A} : (D_{σ}^{A} → D_{τ}^{A}) → D_{σ→τ}^{A}

lam_{σ→τ}^{A} f = [n_{1}, fn_{1}; …; n_{k}, fn_{k}],

where (n_{i} ∈ D_{σ}^{A}) ∧ (k = |D_{σ}^{A}|)

fix_{σ}^{A} : D_{σ→σ}^{A} → D_{σ}^{A}
fix_{σ}^{A} n = ⊔_{EM}^{N} {d_{i}}

d_{0} = ⊥D_{σ}^{A}^{EMN}

d_{i+1} = app_{σ→σ}^{A} nd_{i}

Fig. 4. Standard and non-standard interpretations for E_{σ}^{I}

Proof From domain theory we know that π_{1}^{S} and π_{2}^{S} are monotonic. We prove that π_{1}^{A} and π_{2}^{A} are monotonic by induction on the type σ × τ. For details see Solberg’s PhD [11].

Lemma 16 The functions app_{σ}^{S}, app_{σ}^{A}, π_{1}^{S}, π_{1}^{A}, π_{2}^{S}, and π_{2}^{A} are continuous with respect to ordering on the standard domain, ≤, and the Egli-Milner ordering on name of PERs, ⊑_{EM}^{N} , respectively.

Proof It is a consequence of Lemma 14 and 15 and by recalling that monotonic functions from a space of finite height are continuous.

5.1 Ternary logical relations

Now we can define the relations by:

(d, d′) ∈ γ_{σ}(a) ⇔ (d, d′)R_{σ}a

Definition 17 Ternary Logical Relations A type-indexed family of relations (R_{σ}) is logical (terminology conventionally abused by writing “R is a logical relation”) if for all σ and τ:

(f, f′)R_{σ→τ} h ⇔ (∀d, d′ ∈ D_{σ}^{S}, ∀a ∈ D_{σ}^{A})

(d, d′)R_{σ}a ⇔ (app_{σ→τ}^{S} fd, app_{σ→τ}^{S} f′d′)R_{τ} (app_{σ→τ}^{A} ha)

(p_{1}, p_{2})R_{σ×τ} p ⇔ (π_{1}^{S}(p_{1}), π_{1}^{S}(p_{2}))R_{σ}π_{1}^{A}(p) ∧ (π_{2}^{S}(p_{1}), π_{2}^{S}(p_{2}))R_{τ} π_{2}^{A}(p)

Proposition 18 The relation R is logical.

Proof We prove that R is a logical relation by induction on the type. For details see Solberg’s PhD [11].

Proposition 19 The relation R is inductive with respect to ordering on the standard domain, ≤, and the Egli-Milner ordering on name of PERs, ⊑_{EM}^{N} , respectively.

Proof We prove that the relation R is inductive by induction on the type. For details see Solberg’s PhD [11].

The standard fixpoint and the abstract fixpoint of related values are related:

Proposition 20 Let (f, f)R_{σ→σ}h then (fix_{σ}^{S}f, fix_{σ}^{S}f)R_{σ}(fix_{σ}^{A}h)

Proof We assume (f, f)R_{σ→σ}h. First we show that (d_{i}^{S}, d_{i}^{S})R_{σ}d_{i}^{A} holds for all i by induction on i. Next from Lemma 14 we know that app^{S} and app^{A} are monotonic therefore are {d_{i}^{S}} and {d_{i}^{A}} chains and since R is inductive (Proposition 19) we have (⊔_{i}{d_{i}^{S}}, ⊔_{i}{d_{i}^{S}})R_{σ}(⊔_{EM}^{N}{d_{i}^{A}}) as required.

Case i = 0: We need to show (⊥D_{σ}^{S}, ⊥D_{σ}^{S})R_{σ}⊥D_{σ}^{A}^{EMN} which is trivially implied

by strictness of γ_{σ}(⊥D_{σ}^{A}^{EMN}).

Case i + 1: Assume (d_{i}^{S}, d_{i}^{S})R_{σ}d_{i}^{A} and show (d_{i+1}^{S}, d_{i+1}^{S})R_{σ}d_{i+1}^{A}: we have d_{i+1}^{S} = app_{σ}^{S} fd_{i}^{S} and d_{i+1}^{A} = app_{σ}^{A} hd_{i}^{A}. Now, since R is logical (Proposition 18),

we have (app_{σ}^{S} fd_{i}^{S}, app_{σ}^{S} fd_{i}^{S})R_{σ}(app_{σ}^{A} hd_{i}^{A}) as required.

Now the soundness and completeness of the analysis is:

Theorem 21 Let ρ be a standard environment and let δ be an abstract environment. Suppose for all constants c of type τ we have (c^{S}, c^{S})R_{τ} c^{A} then for all σ and e we have

(ρ, ρ)Rδ ⇒ (E_{σ}^{S}[[e]]ρ, E_{σ}^{S}[[e]]ρ)R_{σ}(E_{σ}^{S}[[e]]δ)

Proof We prove the Theorem by induction on the type. For details see Solberg’s PhD [11].

Example 22 We calculate

E_{Int→Int}^{A}[[λx.4]]ρ = lam_{Int→Int}^{A} (λd.EInt^{A}[[4 ]]ρ[d/x])
= lam_{Int→Int}^{A} (λd.4^{A})
= lam_{Int→Int}^{A} (λd.2A)
= [1A, 2A; 2A, 2A; 3A, 2A; 1B, 2A; 2B, 2A; 3B, 2A; 4, 2A]

Now

λx.4 ∈ UP(γ_{Int→Int}[1A, 2A; 2A, 2A; 3A, 2A; 1B, 2A; 2B, 2A; 3B, 2A; 4, 2A])

      = cgt

as required. We also have

E_{Int→Int}^{A}[[fix(λx.4)]]ρ =
fix_{Int→Int}^{A}[1A, 1B; 2A, 1B; 3A, 1B; 1B, 1B; 2B, 1B; 3B, 1B; 4, 1B]

and

d_{0} = 1B
d_{1} = app_{Int→Int}^{A} [1A, 2A; 2A, 2A; 3A, 2A; 1B, 2A; 2B, 2A; 3B, 2A; 4, 2A]1B
= 2A
d_{2} = app_{Int→Int}^{A} [1A, 2A; 2A, 2A; 3A, 2A; 1B, 2A; 2B, 2A; 3B, 2A; 4, 2A]2A
= 2A

and hence

E_{Int→Int}^{A}[[fix(λx.4)]]ρ = 2A

We calculate

E_{Int→Int}^{A}[[λx.⊥]]ρ = lam_{Int→Int}^{A} (λd.EInt^{A}[[⊥]]ρ[d/x])
= lam_{Int→Int}^{A} (λd.⊥^{A})
= lam_{Int→Int}^{A} (λd.1B)
= [1A, 1B; 2A, 1B; 3A, 1B; 1B, 1B; 2B, 1B; 3B, 1B; 4, 1B]

and hence

λx.⊥ ∈ UP(γ_{Int→Int}[1A, 1B; 2A, 1B; 3A, 1B; 1B, 1B; 2B, 1B; 3B, 1B; 4, 1B])

      = div

as required. We also have

E_{Int→Int}^{A}[[fix(λx.⊥)]]ρ =
fix_{Int→Int}^{A}[1A, 1B; 2A, 1B; 3A, 1B; 1B, 1B; 2B, 1B; 3B, 1B; 4, 1B]

and

d_{0} = 1B
d_{1} = app_{Int→Int}^{A} [1A, 1B; 2A, 1B; 3A, 1B; 1B, 1B; 2B, 1B; 3B, 1B; 4, 1B]1B
= 1B
d_{2} = app_{Int→Int}^{A} [1A, 1B; 2A, 1B; 3A, 1B; 1B, 1B; 2B, 1B; 3B, 1B; 4, 1B]1B
= 1B

and hence E_{Int→Int}^{A}[[fix(λx.⊥)]]ρ = 1B.

6 Conclusion

We have defined the notion of uniform PERs on the integers and by following the framework of Hunt [6] we have lifted this notion to higher types in one particular way. In the work of Hunt all the PERs were strict. Here we have encountered PERs which are not strict; since they are useful too, we had to handle the fixpoint iteration in another way. We defined the Egli-Milner ordering on PERs and used it for the fixpoint iteration.

More work is need to clarify why our approach yields four extra properties at type Int → Int compared to the approach in [4]. The significance of some of the properties being Egli-Milner equivalent (both in this work and [4]) also needs more fuller investigation.

We now briefly compare this work with related papers. Firstly we show that the strictness properties of Burn, Hankin and Abramsky [2] naturally embed in the uniform PER properties presented here. To be precise, let U′(Int) = {1B = {(⊥, ⊥)}, 4 = ZZ_{⊥} × ZZ_{⊥}} and U′(σ → τ) be defined inductively in the same manner as U(σ → τ). Then for all types σ we have U′(σ) ⊆ U(σ) and moreover U′(σ) is isomorphic to BHA(σ). Here BHA(σ) is the set of strictness properties for type σ defined by Burn, Hankin and Abramsky:

BHA(Int) = 2 = {0, 1}
BHA(σ → τ) = BHA(σ) → BHA(τ)

Note that this embedding can also be seen as selecting uniform PER representatives of the uniform ideals of [5]. It also occurs as an abstraction of the comportment interpretation of [4] which abstracts our uniform PER interpretation.

We also compare with the properties based on annotated types described by Solberg et al. [10]. All the properties of that work can be modelled by the uniform PERs except for two: the property of knowing that a function does not have a WHNF and the property of knowing that a function does have a WHNF. This is not a lack of the uniform PER notion, but due to the fact that we have used non-lifted function spaces in which λx.⊥ = ⊥ and hence WHNF properties are inexpressible.

Acknowledgements

Thanks to Radhia and Patrick Cousot for engaging arguments on the nature of abstract interpretation. Sebastian Hunt explained further about PERs in abstract interpretation. Thanks to Nick Benton, Hanne Riis Nielson, Flemming Nielson and Andrew Pitts for interesting discussions. We wish also to thank the PLILP referees for their comments which have aided the presentation. This work is supported by EU ESPRIT BRA 8130 “LOMAPS” and has been facilitated by Danish support for one author to visit Cambridge and by French support for the other to spend sabbatical leave at Ecole Polytechnique.

References

1. Nick Benton. Strictness Analysis of Functional Programs. PhD thesis, University of Cambridge, 1993. Available as Computer Laboratory Technical Report No. 309.

2. Geoffrey L. Burn, Chris Hankin and Samson Abramsky. Strictness analysis for higher-order functions. Science of Computer Programming, 7:249–278, 1986.

3. Patrick Cousot and Radhia Cousot. Galois connections based abstract interpretation for strictness analysis. In D. Bjørner, M. Broy and I. V. Pottosin, editors, Proceedings of the International Conference on Formal Methods in Programming and their Applications, LNCS 735, pages 98–127, 1993.

[Currently available via http://www.ens.fr/~cousot/]

4. Patrick Cousot and Radhia Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages), invited paper. In Proceedings of the 1994 International Conference on Computer Languages, ICCL’94, pages 95–112, IEEE Computer Society Press, 1994.

[Currently available via http://www.ens.fr/~cousot/]

5. Christine Ernoult and Alan Mycroft. Uniform ideals and strictness analysis. In ICALP 91, LNCS 510, 1991.

[Currently available via http://www.cl.cam.ac.uk/users/am]

6. Sebastian Hunt. Abstract Interpretation of Functional Languages: From Theory to Practice. PhD thesis, Imperial College, London, 1991.

7. Thomas P. Jensen. Abstract Interpretation in Logical Form. PhD thesis, Imperial College, London, 1992.

8. Alan Mycroft. Abstract Interpretation and Optimising Transformation for Applicative programs. PhD thesis, University of Edinburgh, 1981.

9. Flemming Nielson. Two-level semantics and abstract interpretation. Theoretical Computer Science, 69:117–242, 1989.

10. Kirsten Lackner Solberg, Hanne Riis Nielson and Flemming Nielson. Strictness and totality analysis. In Proceedings of Static Analysis Symposium, LNCS 864, 1994.

11. Kirsten Lackner Solberg. Annotated Type Systems for Program Analysis. PhD thesis, Odense University, to appear.

12. Philip Wadler and John Hughes. Projections for strictness analysis. In Proceedings of Functional Programming Languages and Computer Architectures ’87, LNCS 274, 1987.

This article was processed using the LaTEX macro package with LLNCS style