Untyped strictness analysis

Christine Ernoult^{1} and Alan Mycroft

Computer Laboratory, Cambridge University

New Museums Site, Pembroke Street

Cambridge CB2 3QG United Kingdom

        E-mail: ernoult@info.emn.fr, Alan.Mycroft@cl.cam.ac.uk

Abstract

We re-express Hudak and Young’s higher-order strictness analysis for the untyped λ-calculus in a conceptually simpler and more semantically-based manner. We show our analysis to be a sound abstraction of Hudak and Young’s which is also complete in a sense we make precise.

1 Background

Untyped strictness analysis is currently a little out of vogue. There are two reasons for this. One is that the standard reference [3] is presentationally hard to read and, as we show, is complicated by spurious domain elements. The other is that most of the functional programming world uses some form of typed (typically simple polymorphic) λ-calculus. Strictness analysis for such languages benefits from the simple exposition of the Imperial College stable and various finiteness properties seemingly associated by the decidability of type inference.

However, some properties of (e.g.) the second-order polymorphic λ-calculus are best proved by appeal to untyped results and, as yet, we know of no polymorphic invariance properties which allow lifting of results for simple types.

It is with this interest in such strictness analysis that we give a more fundamental explanation of the ideas in the untyped λ-calculus which both better explains the theory and encourages its use as a basis for such extended analyses.

We discuss the treatment of domain errors which influence strictness. In particular, it is common to wish errors to give non-⊥ values (exceptions) in an untyped language, but when we see the untyped language used as an underlying implementation of a typed language such as the second-order λ-calculus then (unobtainable) domain errors should be treated as ⊥ to ease strictness analysis.

2 Introduction

Strictness analysis was originated by Mycroft [8] for the first-order case over flat domains, using a formalism based on abstraction and concretisation functions.

1Current address: Ecole des Mines de Nantes, 3, rue Marcel Sembat, 44 100 Nantes, France

Temporarily, suppose that D is a flat cpo. Let 2 stand for the the set {0, 1} ordered by 0 < 1. Recall that f : D^{n} → D is strict in its k-th argument if (∀\overline{x} ∈ D^{n})f(x_{1}, …, x_{k−1}, ⊥, x_{k+1}, …, x_{n}) = ⊥. Mycroft developed a strictness theory for first order functions on flat domains which gave a standard interpretation of a program user-defined function symbol (say f) as a function f as above and also non-standard interpretation f^{♯} : 2^{n} → 2. Such f^{♯} satisfy a correctness property with respect to f along the lines of f^{♯}(1, …, 1, 0, 1, …, 1) = 0 ⇒ f is strict in its k-th argument. This property is respected by composition and fixpoint extraction and so lifts from base functions to user-defined functions.

Burn, Hankin and Abramsky [1] showed that the Hoare (or relational) powerdomain could be used to generate a theory of strictness analysis for the simply typed λ-calculus. (Their system abstracts functions between concrete domains with functions between abstract domains).

Around the same time Hudak and Young [3] gave a definition of strictness pairs which enabled them to analyse the untyped λ-calculus. They observed that an expression has not only a “direct strictness” (the set of variables which are evaluated when it is), but also a “delayed strictness” (the set of variables which are evaluated when the expression is applied). They suggested that the strictness property should perhaps be captured by an object, the domain of strictness pairs Sp defined by:

Sp = P(V) × (Sp → Sp)

where V is the set of variable names and P(V) is ordered by reverse inclusion ⊇. With every expression e in a strictness environment senv, they associated a strictness pair that provides properties of e both as an ‘isolated value’ and as a ‘function to be applied’:

S[[e]]senv = ⟨sv, sf ⟩

Their work was less semantically based than Burn, Hankin and Abramsky’s because its use of power-sets of variable names in the ‘strictness pair’ domain introduced syntactic objects into a semantic construction. In retrospect, it was both oversyntactic and unnecessary in the sense that P(V) can be replaced by 2 with no loss of expressive power as we show in section 3.1, where we use the notation E_{HY} [[ · ]] instead of S[[ ·]].

This work is structured in the following manner. Section 3 explains notation and the syntax and standard semantics for the untyped λ-calculus. It also describes the problem of domain error. Section 4 gives strictness interpretations which formalise Hudak and Young’s and also our improvement. Section 5 sets up the relationship between the standard semantics, Hudak and Young’s strictness and ours. Section 6 shows the correctness and completeness of our strictness interpretation relative to Hudak and Young’s.

3 Notation and λ-calculus

Here we use the word domain to mean complete (pointed) partial order as usual. Let 2 stand for the domain {0, 1} ordered by 0 < 1. Recursive domain definitions are as usual and +, ⊕, ×, → will mean respectively separated sum, coalesced sum, cartesian product and continuous function space.

3.1 Untyped λ-calculus

We consider the untyped λ-calculus with constants. Let C and V be sets of constants (including primitive functions) and variables ranged over by c and x respectively (z will also be used to range over integer constants). For the purposes of this paper we will assume C contains ZZ and Turing-sufficient arithmetic constants {plus, minus, cond}. (The first argument of cond is required to be an integer which is tested for zero/non-zero as in the ‘C’ programming language). A natural alternative would be to use the register-machine primitives of {succ, pred, cond} acting over IN.

The set Λ of λ-calculus terms is then:

e ∈ Λ ::= c | x | λx.e | e e′

The standard domain of interpretation is:

U = ZZ + (U → U) + {wrong} [≡ ZZ_{⊥} ⊕ (U → U)_{⊥} ⊕ {wrong}_{⊥}]

treating · + · + · as a ternary separated sum. Injections into this sum will be written in_{z}(·), in_{f}(·) and in_{w}(·). We use typewriter font for syntactic objects and italic font for mathematical (meta-language) objects.

In the untyped world we need to inject functions (in U → U) into U to represent them as values and outject them from U to U → U to apply them. This can be summarised by two functions lam and app respectively such as:

lam x = in_{f}(x)
app x y = case x of in_{f}(f) ⇒ f(y) else err.

Here ‘err’ typically represents ⊥ or in_{w}(wrong), see below. Hudak and Young use the symbol ‘error’ to represent such domain errors for constants—their treatment of these (and also for app) suggests they mean our in_{w}(wrong). Milner [7] used a similar ‘wrong’ value to handle domain errors.

3.2 Definition of an interpretation

An interpretation I is a tuple (D_{I}; lam_{I}, app_{I}, num_{I}, plus_{I}, minus_{I}, cond_{I}, err_{I}) where D_{I} is a cpo and lam_{I} : (D → D) → D and app_{I} : D → (D → D) are continuous functions; num_{I} : ZZ → D is a function and plus_{I}, minus_{I}, cond_{I}, err_{I} ∈ D. (We drop the subscripts when the context is clear.)

Given such an interpretation, I, we can define the notion of environment (over I) by

Env_{I} = V → D_{I}

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

E_{I} : Λ → Env_{I} → D_{I}

in the following manner:

E_{I}[[x]]ρ = ρ(x)
E_{I}[[c]]ρ = K_{I}[[c]]
E_{I}[[λx.e]]ρ = lam_{I}(λd ∈ D_{I}.E_{I}[[e]]ρ[d/x])
E_{I}[[e e′]]ρ = app_{I}(E_{I}[[e]]ρ)(E_{I}[[e′]]ρ)

Here we use K_{I} for the meaning of constants—it is simply given by

K_{I}[[z]] = num_{I}(z)
K_{I}[[plus]] = plus_{I}
K_{I}[[minus]] = minus_{I}
K_{I}[[cond]] = cond_{I}.

We write STD to refer to the standard interpretation given by U as domain and the constants as given below. Arithmetic constants have the usual meanings for arguments within ZZ in STD (including num z = in_{z}z)—we now consider their definition over the larger space D. The otherwise unused err_{STD} provides a convenient way of varying the error value in plus, app etc. used in the semantics for constants. (This is important as strictness depends on it.) Although this is rather an abuse of notation, given an interpretation, say STD above, we will write STD[⊥/err] or STD[in_{w}(wrong)/err] to represent an interpretation in which the error value and all parts of the interpretation which use it are altered.

3.3 Semantics of constants

3.3.1 Treatment of domain errors

We use the phrase “domain errors” to refer to situations such as plus(λx.x)3 or 3(2) in which an inappropriate value is used for an operand. To clarify this, let us consider an example, the function F defined by

                          F = λx.λy.plusxy

Is F strict in y? In the standard interpretation we obviously have

plus(in_{z}(m))(in_{z}(n)) = in_{z}(m + n)

but this does not define the other cases of plus(in_{f}(f)) and plus(in_{z}(m))(in_{f}(g)). If we define

plus(in_{f}(f)) = ⊥

then F is strict in y, but if we define

plus(in_{f}(f))y = in_{w}(wrong)

then F is non-strict in y. Similarly app(in_{z}(z))x and app(in_{w}(wrong))x provide similar choices which affect strictness.

As Mishra noted in [5] some very specific choices are made in the denotational semantics regarding such issues as: domain errors due to primitive functions or whether all looping terms should be regarded as denoting the same value.

3.3.2 Subtlety of partial applications

Note that, even for a fixed choice of domain error value there is still a non-trivial choice for semantics of partially applied constants. Clarifying Hudak and Young’s remark, there is a non-trivial choice of semantics of the (strict, curried) constants due to the lifting which occurs as a consequence of the above separated sum. (The problem arises from the non-isomorphism of (A × B → C)_{⊥} and (A → (B → C)_{⊥})_{⊥} which causes η-equivalence to fail). For example, in the standard interpretation we can give

K[[plus]] = in_{f}λx.in_{f}λy.case (x, y) of (in_{z}(i), in_{z}(j)) ⇒ in_{z}(i + j) else err
K[[cond]] = in_{f}λx.in_{f}λy.in_{f}λz.case x of in_{z}(n) ⇒ (n ≠ 0 → y, z) else err

or we can give the following versions (which are more strict in the case of err = ⊥)

K[[plus]] = in_{f}λx.case x of in_{z}(i) ⇒ in_{f}λy.case y of in_{z}(j) ⇒ in_{z}(i + j) else err else err

K[[cond]] = in_{f}λx.case x of in_{z}(n) ⇒ (n ≠ 0 → (in_{f}λy.in_{f}λz.y), (in_{f}λy.in_{f}λz.z)) else err

Such differences are important for the precise details of the abstract strictness interpretation given in section 4.

To reproduce as closely as possible Hudak and Young’s world, we adopt the former definitions and err_{STD} = in_{w}(wrong).

4 Untyped strictness

In this section we give a simpler and more semantically oriented framework for the strictness analysis of Hudak and Young [3]. Section 3 gave the syntax and standard interpretation of our λ-calculus which yields the standard value domain U, given in section 3.1 as

U = ZZ + (U → U) + {wrong} [≡ ZZ_{⊥} ⊕ (U → U)_{⊥} ⊕ {wrong}_{⊥}].

Now, since the abstract domain for ZZ_{⊥} is to be 2 as in the first order case, it might appear that the cpo

S = {1} + (S → S)

is a suitable domain of strictness properties (the separated sum adds a ⊥ element corresponding to 0. However, the untyped nature of functions like λx.condx 7 (λy.42+ y) means that we need more least upper bounds to exist—in particular any uncertainty of the value of x requires the λ-body to be described as the least upper bound of an integer and a function. The reasoning is identical to that whereby a non-deterministic amb operator may require the least upper bound of two differing integers leading to a power-domain. (In abstract interpretation the uncertainty induced by imprecise knowledge behaves very much like non-determinism.) Recalling the natural isomorphism of P(A+B) and P(A)×P(B) leads us to complete S with least upper bounds by using

S = 2 × (S → S)

which can now be viewed as a simpler formulation of Hudak and Young’s strictness pairs.^{2} We adopt the name strictness pairs and their notation: elements s ∈ S are written ⟨v, f⟩ with s_{v}, s_{f} standing for the components of s.

4.1 Strictness in the presence of domain errors

Note that the treatment of domain errors affects strictness. In the STD[in_{w}(wrong)/err] interpretation above, we have that λx.cond (λy.y) x x is not strict in x and hence neither is λx.λy.condyxx. Sometimes it is simplistically said that “strictness analysis is invalid in the presence of non-⊥ error values”. A more correct view (which we adopt here) is that strictness functions need to correspond to standard semantic functions—hence they must reflect the treatment of err as ⊥ or in_{w}(wrong). A minor error in Hudak and Young’s original strictness interpretation causes the above functions to be incorrectly analysed as strict.

4.2 Strictness semantic interpretation

We take

S = 2 × (S → S)

as above for the domain part of the interpretation. The function part is given by:

lam x = ⟨1, x⟩

app x y \begin{matrix}= ⟨x_{v} ⊓ (x_{f}y)_{v}, (x_{f}y)_{f}⟩ \\ = ⟨x_{v}, ⊤_{S→S}⟩ ⊓ (x_{f}y) \end{matrix}

err = ⟨1, λs.err⟩

= ⊤_{S} (the unique fixpoint) num z = ⟨1, λs.err⟩

plus = minus = ⟨1, λx.⟨1, λy.⟨x_{v} ⊓ y_{v}, λs.err⟩⟩⟩
cond \begin{matrix}= ⟨1, λx.⟨1, λy.⟨1, λz.⟨x_{v} ⊓ (y_{v} ⊔ z_{v}), y_{f} ⊔ z_{f}⟩⟩⟩⟩ \\ = ⟨1, λx.⟨1, λy.⟨1, λz.⟨x_{v}, ⊤_{S→S}⟩ ⊓ (y ⊔ z)⟩⟩⟩ \end{matrix}

2Later, Young suggested this domain in his Ph.D. dissertation [11] but they did not carry through with it in the analysis.

The strictness interpretation of cond above is for the first choice (i.e. Hudak and Young’s) of standard semantics of plus and cond given in section 3.3.2, i.e. when cond ⊥ ≠ ⊥. For the case of cond ⊥ = ⊥ we would have the better (enabling more strictness inferences) interpretation as

plus = ⟨1, λx.⟨x_{v}, λy.⟨x_{v} ⊓ y_{v}, λs.err⟩⟩⟩
cond = ⟨1, λx.⟨x_{v}, (x_{v} = 0)→λs.err, λy.⟨1, λz.(y ⊔ z)⟩⟩⟩.

We will refer to this interpretation as EM and use ‘EM’ subscripts on its components when the context requires.

4.3 Hudak and Young’s strictness interpretation

Let us call HY-strictness the strictness interpretation HY defined by

(S_{HY}; lam_{HY} , app_{HY} , num_{HY} , plus_{HY} , minus_{HY} , cond_{HY} , err_{HY})

satisfying the definitions below. These are taken from the strictness semantics of Hudak and Young, save that we use the ⊔ symbol to denote the least upper bound on S_{HY} → S_{HY} but inexplicably they use ⊓ “for clarity”. Similarly, to make the semantic basis clearer, we have used the ⊔ symbol instead of the synonymous ∩ on (P(V), ⊇) and similarly ⊓ for ∪.) We also have no need for “hatted” variables x̂ to range over sets of variables which they used because of their mix of syntax and semantics. HY is given, dropping subscripts, by:

S = (P(V), ⊇) × (S → S)

lam x = ⟨{}, x⟩

app x y \begin{matrix}= ⟨x_{v} ⊓ (x_{f}y)_{v}, (x_{f}y)_{f}⟩ \\ = ⟨x_{v}, ⊤_{S→S}⟩ ⊓ (x_{f}y) \end{matrix}

err \begin{matrix}= ⟨\{\}, λs.err⟩ \\ = ⊤_{S} \end{matrix}

num z = ⟨{}, λs.err⟩

plus = minus = ⟨{}, λx.⟨{}, λy.⟨x_{v} ⊓ y_{v}, λs.err⟩⟩⟩

cond \begin{matrix}= ⟨\{\}, λx.⟨\{\}, λy.⟨\{\}, λz.⟨x_{v} ⊓ (y_{v} ⊔ z_{v}), y_{f} ⊔ z_{f}⟩⟩⟩⟩ \\ = ⟨\{\}, λx.⟨\{\}, λy.⟨\{\}, λz.⟨x_{v}, ⊤_{S→S}⟩ ⊓ (y ⊔ z)⟩⟩⟩ \end{matrix}

It appears that merely re-phrasing Hudak and Young’s formulation as an interpretation helps to separate syntax and semantics.

4.3.1 Warning

As we noted in section 4.1 the definition of cond_{HY} is only correct with respect to err_{STD} = ⊥ not err_{ST D} = in_{w}(wrong). Accordingly, to ensure the correctness of the following theorem from now on we take

K_{ST D}[[cond]] = in_{f}λx.in_{f}λy.in_{f}λz.case x of \begin{matrix}in_{z}(n) ⇒ (n ≠ 0 → y, z) \\ else ⊥ \end{matrix}

instead of that given in section 3.3.2.

5 Relationship between various interpretations

We claim the following results.

1. (From Hudak and Young) HY (= HY [⊤_{S_{HY}} /err]) is a correct abstraction of STD (= STD[in_{w}(wrong)/err])

2. HY[⊥/err] is a correct abstraction of STD[⊥/err]

3. EM is a correct abstraction of HY

4. EM is complete for HY

5. EM[⊥/err] is a correct abstraction of HY[⊥/err]

6. EM[⊥/err] is complete for HY[⊥/err]

The correctness relations between STD and EM hold by transitivity.

The next section sets about proving that results 3 and 4, i.e. that EM is a correct abstraction of HY which is also complete.

6 Relationship to Hudak and Young’s strictness

We now set up a relationship between between HY-strictness HY and EM-strictness EM from sections 4.2 and 4.3. This relationship is then shown to induce an abstraction of HY-strictness into EM-strictness. Moreover, the abstraction is complete in that all properties exploited by Hudak and Young are derivable via our strictness interpretation.

For notational reasons in this section we will use A for S_{EM} and B for S_{HY}. Both A and B are given as recursive function spaces, viz

A = 2 × (A → A)
B = (P(V), ⊇) × (B → B)

Let us define γ_{1} : 2 → P(V) by

γ_{1}(0) = V
γ_{1}(1) = {}.

Now, the relation we seek to define should satisfy

∼ ⊆ A × B
(x, f) ∼ (y, g) ⇔ \begin{matrix}y = γ_{1}(x) ∧ \\ (∀a ∈ A, b ∈ B) a ∼ b ⇒ f(a) ∼ g(b) \end{matrix}

but it is unclear whether this is well-defined. To prove the unique existence and various properties of ∼ we define it simultaneously with the inverse limit construction for A and B.

Recall that domain equations like that for A above are solved by the inverse limit construction—we put A_{0} = {⊥}, the trivial domain, and then put A_{k+1} = 2×(A_{k} → A_{k}). There are embedding i_{k} : A_{k} → A_{k+1} and projection p_{k} : A_{k+1} → A_{k} maps between A_{k} and A_{k+1}. A is obtained as the limit

A_{∞} = {(a_{0}, a_{1}, …) ∈ ∏_{k} A_{k} | a_{k} = p_{k}(a_{k+1})}

The isomorphism of A and 2 × (A → A) is obtained pointwise from the p_{k} and i_{k}. The construction for B is identical.

We can define approximants of ∼ in the following manner

∼_{k} ⊆ A_{k} × B_{k}
a ∼_{0} b ⇔^{Δ} true
(x, f) ∼_{k+1} (y, g) ⇔^{Δ} \begin{matrix}y = γ_{1}(x) ∧ \\ (∀a ∈ A_{k}, b ∈ B_{k}) a ∼_{k} b ⇒ f(a) ∼_{k} g(b) \end{matrix}

and hence properly define

∼ ⊆ A × B
(a_{0}, a_{1}, …) ∼ (b_{0}, b_{1}, …) ⇔ (∀k) a_{k} ∼_{k} b_{k}.

It is convenient to write

∼^{1} ⊆ 2 × P(V)
∼^{2}_{k+1} ⊆ (A_{k} → A_{k}) × (B_{k} → B_{k})
x ∼^{1} y ⇔^{Δ} y = γ_{1}(x)
f ∼^{2}_{k+1} g ⇔^{Δ} (∀a ∈ A_{k}, b ∈ B_{k}) a ∼_{k} b ⇒ f(a) ∼_{k} g(b)

so that

(x, f) ∼_{k+1} (y, g) ⇔ x ∼^{1} y ∧ f ∼^{2}_{k+1} g.

It is also convenient to define here the type-induced (‘logical’) relations from ∼. Allowing t to range over meta-language types given by t ::= D | t → t we define

a ∼^{D} b ⇔ a ∼ b
f ∼^{t→t′} g ⇔ ((∀x, y) x ∼^{t} y ⇒ fx ∼^{t′} gy)

The limit relation ∼^{2} now coincides with ∼^{D→D}

We now have distributivity lemma for ∼: Lemma: ∼ preserves arbitrary LUBs and GLBs (including ⊥ and ⊤) in that, given possible empty sequences a^{i} ∈ A, b^{i} ∈ B, we have

((∀i) a^{i} ∼ b^{i}) ⇒ (⨆_{i} a^{i} ∼ ⨆_{i} b^{i} ∧ ⊓_{i}a^{i} ∼ ⊓_{i}b^{i})

6.1 Proposition: relatedness

For all λ-terms e ∈ Λ we have that

(∀η ∈ Env_{EM}, ρ ∈ Env_{HY}) η ∼ ρ ⇒ E_{EM}[[e]]η ∼ E_{HY} [[e]]ρ

where η ∼ ρ ⇔ (∀x ∈ V) η(x) ∼ ρ(x). It turns out that this abstraction relation is both correct and complete and we study these aspects after a proof sketch.

6.2 Proof

We the above proposition by structural induction on the (object) term e. But first we need some lemmas, viz

• app_{EM} ∼^{D→(D→D)} app_{HY}

• lam_{EM} ∼^{(D→D)→D} lam_{HY}.

• (∀z ∈ ZZ)num_{EM}(z) ∼ num_{HY} (z)

• plus_{EM} ∼ plus_{HY}

• minus_{EM} ∼ minus_{HY}

• cond_{EM} ∼ cond_{HY}

• err_{EM} ∼ err_{HY} Given these lemmas, proved below, the theorem is a trivial structural induction.

We give two cases:

• case e = x: trivial.

• case e = λx.e′: By inductive hypothesis, supposing also a ∼ b then E_{EM}[[e′]]η[a/x] ∼

E_{HY} [[e′]]ρ[b/x]. Hence by the lemma lam_{EM}λa.E_{EM}[[e′]]η[a/x] ∼ lam_{EM}λb.E_{HY} [[e′]]ρ[b/x]. Proof of lemmas We give the representative cases for app and cond.

• app_{EM} ∼^{D→(D→D)} app_{HY}: Assume a ∼ b and a′ ∼ b′ then, expanding the

definitions of app_{HY} and app_{EM}, it is equivalent to prove

⟨a_{v}, ⊤_{A→A}⟩ ⊓ (a_{f}a′) ∼ ⟨b_{v}, ⊤_{B→B}⟩ ⊓ (b_{f}b′). This holds since a ∼ b ⇔ a_{v} ∼^{1} b_{v} ∧ a_{f} ∼^{2} b_{f} and the lemma for ∼-preservation of ⊔ and ⊓.

• cond_{HY} ∼ cond_{EM}: We need to prove

⟨1, λa.⟨1, λa′.⟨1, λa′′.⟨a_{v}, ⊤_{A→A}⟩ ⊓ (a′ ⊔ a′′)⟩⟩⟩ ∼
⟨{}, λb.⟨{}, λb′.⟨{}, λb′′.⟨b_{v}, ⊤_{B→B}⟩ ⊓ (b′ ⊔ b′′)⟩⟩⟩.

Assume a ∼ b, a′ ∼ b′ and a′′ ∼ b′′ then, using the recursive definition of ∼ and recalling that 1 = ⊤_{A} and {} = ⊤_{B}, this is equivalent to

⊤_{A} ∼^{1} ⊤_{B} ∧ ⟨a_{v}, ⊤_{A→A}⟩ ⊓ (a′ ⊔ a′′) ∼ ⟨b_{v}, ⊤_{B→B}⟩ ⊓ (b′ ⊔ b′′).

The first conjunct holds by definition and by the lemma for ∼-preservation of ⊔ and ⊓ it suffices to show

⟨a_{v}, ⊤_{A→A}⟩ ∼ ⟨b_{v}, ⊤_{B→B}⟩.

This holds since a ∼ b ⇒ a_{v} ∼^{1} b_{v} and

⊤_{A→A} = λx ∈ A.⊤_{A} ∼^{2} λy ∈ B.⊤_{B} = ⊤_{B→B}.

6.3 Proposition: soundness

The relation ∼ restricts to a embedding-closure pair (an abstraction of B = S_{HY} by A = S_{EM}). The concretisation and abstraction maps respectively are γ : A → B and α : B → A given by

γ(a) = ⨆{b ∈ B|a ∼ b}
α(b) = ⊓{a ∈ A|a ∼ b} = ⊓{a ∈ A | γ(b) ⊑ a}

The α and γ form a galois connection as usual and correctness of the remainder of the interpretation interpretation (i.e. lam, app, plus etc.) with respect to (α, γ) follows from that the base lemmas above.

6.4 Proposition: completeness

Since the trivial abstract interpretation would be sound with respect to HY-strictness, we now show that EM-strictness can provide all the information that HY-strictness can. This is a completeness argument. Note that we cannot expect to have a natural completeness result of the form “EM-strictness of expressions determines their HY-strictness”. Consider the term λx.x: this has HY-strictness of ({}, λx ∈ S_{HY} .x) and EM-strictness of (0, λx ∈ S_{EM}.x). It is unreasonable to expect some function of the latter, coarser-grained, interpretation to yield the former, finer, one. (The general question of completeness in abstract interpretation is addressed in [10].)

Accordingly, our completeness result relies on the observation that Hudak and Young’s analysis makes strictness optimisations only on the basis of limited predicates (actually whether the first component of S_{HY} is empty or non-empty). The rest of the internal structure is non-observable. Accordingly, we wish to assert that our simpler internal structure gives rise to the precisely the same observable properties.

The key notion is that both the EM and HY interpretations are only used for strictness optimisations, i.e. early evaluation of an expression. Although it is rarely clearly stated, we implicitly have a predicate whose result tells us when an abstract value permits strictness optimisations. Here, this predicate (subset of S_{HY} or S_{EM}) is given by

p(v, f) ⇔ v = ⊥.

This is a sound predictor of when the standard interpretation gives ⊥ for some prescribed assignments of values to free variables. We abuse notation by using p as a predicate both on S_{HY} and S_{EM}.

Our completeness result is that, for all meta-terms e,

(∀η ∈ Env_{EM}, ρ ∈ Env_{HY}) η ∼ ρ ⇒ (p(E_{EM}[[e]]η) ⇔ p(E_{HY} [[e]]ρ))

Thus all optimisations permitted by the HY interpretation are also permitted by the EM interpretation. This forms the basis of our claim that the HY domain had spurious elements.

7 Problem of infinite chains

Hudak and Young mentioned in [3] that their higher-order analysis is not guaranteed to terminate. Indeed, this is the case when a strictness pair needs to be applied an infinite number of times. They gave the following example, f = λx.fxx which leads to EM-strictness

s = ⟨1, λx.⟨s_{v} ⊓ (s_{f}x)_{v} ⊓ ((s_{v}x)_{f}x)_{v}, ((s_{f}x)_{f}x)_{f}⟩⟩

or HY-strictness

s = ⟨{}, λx.⟨s_{v} ∪ (s_{f}x)_{v} ∪ ((s_{v}x)_{f}x)_{v}, ((s_{f}x)_{f}x)_{f}⟩⟩

There is a circularity which Hudak and Young suggest is due to the fact that “early” elements of P(V) in the nested pairs depend on “deeper” S_{HY} → S_{HY} elements. Note that, because HY- (and EM-) strictness inherits undecidability from the pure λ-calculus part of the standard interpretation, limiting such infinite chains is undecidable and not merely an algorithmic problem. Hudak and Young make the suggestion that, to avoid such chains, we may be able “to impose a weak type discipline”. The next paragraph shows how this could work for the simply typed λ-calculus and, although this is clearly not the best way to handle the simply typed λ-calculus, it points to how one might treat the second-order λ-calculus.

Further work

It would be desirable to consider whether certain finite-height lattices could represent strictness properties for the untyped λ-calculus instead of the infinite chains present in Hudak and Young. For example, if the given program in Λ can be corresponds to a (type-stripped) program in the simply typed λ-calculus (with (object) types ranged over by t) then we can use ∑ T_{ZZ_{⊥}}[[t]] for the value domain (a retract of D = ZZ + (D → D)) and hence ∑ T_{2}[[t]] for the strictness domain (a retract of S = 2 × (S → S)) where

\begin{matrix}T_{X}[[int]] = X \\ T_{X}[[t → t′]] = T_{X}[[t]] → T_{X}[[t′]]. \end{matrix}

This exhibits [1] within our model and the key point is that ∑ T_{2}[[t]] has no infinite ascending chains. The key question is to whether there exists finite height models for another subset of Λ, those programs corresponding to second-order polymorphically typable terms—this would enable us to conclude Hudak and Young’s suggestion of modelling list operators as λ-terms and thereby inheriting a sensible strictness theory.

Acknowledgments

Thanks to Andy Pitts for explaining subtleties of recursive function spaces. We are indebted to the referees for their careful reading and apposite comments of the draft version of [2] which included sketched versions of these results. This research was supported by SERC grant GR/H14465.

References

[1] Burn, G., Hankin, C. and Abramsky, S. The theory and practice of strictness analysis for higher order functions. In [4].

[2] Ernoult, C. and Mycroft A. Uniform ideals and strictness analysis. Proc. 18th ICALP, Springer-Verlag Lecture Notes in Computer Science, vol. 510, 1991.

[3] Hudak, P. and Young, J. Higher order strictness analysis in untyped lambda calculus. Proc. 13th ACM symp. on Principles of Programming Languages, 1986.

[4] Jones, N.D. and Ganzinger, H. (eds.) Programs as Data Objects: Proc. of a Workshop, Copenhagen, Springer-Verlag Lecture Notes in Computer Science, vol. 215, 1985.

[5] Kuo, T.-M. and Mishra, P. Strictness analysis: a new perspective based on type inference. Proc. of the functional programming and computer architecture conference, ACM-IFIP, 1989.

[6] MacQueen, D., Plotkin, G.D. and Sethi, R. An ideal model for recursive polymorphic types. Proc. 11th ACM symp. on Principles of Programming Languages, 1984.

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

[8] Mycroft, A. Abstract interpretation and optimising transformations of applicative programs. Ph.D. thesis, Edinburgh University, 1981. Available as computer science report CST-15-81.

[9] Mycroft, A. and Jones, N.D. A relational framework for abstract interpretation. In [4].

[10] Mycroft, A. Completeness and predicate-based abstract interpretation. Proc. ACM conf. on Partial Evaluation and Program Manipulation, 1993.

[11] Young, J. The Theory and the Practice Semantic Program Analysis for Higher-Order Functional Programming Languages. Ph.D. thesis, Department of Computer Science, Yale University, May 1989. Available as research Report YALEDU/DCS/RR-669.