Minimal function graphs are not instrumented

Alan Mycroft* & Mads Rosendahl†

* Computer Laboratory, Cambridge University

New Museums Site, Pembroke Street, Cambridge CB2 3QG, United Kingdom

                                     E-mail: Alan.Mycroft@cl.cam.ac.uk

† DIKU, Copenhagen University

Universitetsparken 1, DK-2100 Copenhagen Ø, Denmark

                                                  E-mail: rose@diku.dk

Résumé: The minimal function graph semantics of Jones and Mycroft is a standard denotational semantics modified to include only ‘reachable’ parts of a program. We show that it may be expressed directly in terms of the standard semantics without the need for instrumentation at the expression level and, in doing so, bring out a connection with strictness. This also makes it possible to prove a stronger theorem of correctness for the minimal function graph semantics. Keywords: Minimal function graph, strictness, neededness, abstract interpretation.

Commonly, in abstract interpretation, we start with a standard semantics in denotational style, modify this to make an instrumented semantics which includes further operational detail (for example by adding timing information) and finally abstract this to form a decidable abstract semantics. Much work has gone into the theory of the abstraction process, but relatively little into the instrumentation process. We note that choices (or errors) in the instrumentation can lead to very different conclusions about execution. For example, if we instrument a semantics by replacing values v with pairs (v, n) where n is the number of steps required to reduce an expression e to v then we have possible sensible representations for the instrumented version of subtraction as λ((v, n), (v′, n′)).(v − v′, n + n′ + 1) (sequential) and λ((v, n), (v′, n′)).(v − v′, max(n, n′) + 1) (parallel) together with less reasonable definitions such as λ((v, n), (v′, n′)).(v − v′, 42).

Alan Mycroft & Mads Rosendahl

The minimal function graph semantics was defined by Jones and Mycroft [5] and in part represents a special case of the Cousots’ work [3] on analysing recursive procedures by predicate transformers. It is specified as an instrumented semantics leaving to intuition questions about whether the instrumentation was appropriate. We sidestep this issue by showing that, with a slight modification, the minimal function graph semantics can be defined in terms of the standard semantics. We also show that there are two subtly different MFG semantics according to how the definition of reachability is interpreted — either as strictness or as neededness.

A fuller version of this paper appears as [7].

1. First-order Language

We consider a language of first order recursion equations (of n functions f, each of arity k) with parameters x, constants c, conditional expressions, base functions a (presumed arity k) and defined functions f (also arity k). Expressions e follow a usual first-order syntax. Programs p (also considered as declarations) have the form

f_{1}(x_{1},…, x_{k}) = e_{1};
⋮
f_{n}(x_{1},…, x_{k}) = e_{n}.

The meaning of a program is an n-tuple of functional values. Free (variable) identifiers in e_{i} (1 ≤ i ≤ n) are a subset of {x_{1},…, x_{k}} and free function identifiers a subset of {f_{1},…, f_{n}}.

Standard semantics. This work only considers call-by-value semantics.^{1} A semantics requires a set of ground values V (we assume ⊆ V and ⊆ V and moreover that ⊥ ∉ V so lifting: V → V_{⊥} can be treated as identity). It further requires an interpretation for each constant c_{j}, having as meaning const_{j} ∈ V_{⊥}, and each basic operation a_{j}, having as meaning basic_{j} : V^{k} → V_{⊥}. In examples we will feel free to use other names for constants, basic operations, parameters and functions, particularly ⊥ for an expression whose value is ⊥.

The semantics below assumes a conditional function “· → ·|·” and a function to enforce call-by-value:

strictapp : (V^{k} → V_{⊥}) → (V_{⊥})^{k} → V_{⊥}

Minimal function graphs are not instrumented

strictapp f (v_{1},…, v_{k})\begin{matrix}= f(v_{1},…, v_{k}) & if all v_{i} ≠ ⊥ \\ = ⊥ & otherwise. \end{matrix} Semantic domains and functions

1A companion paper under construction extends this framework to the lazy case.

V  values, as above
ValEnv = V^{k}
FnEnv = (V^{k} → V_{⊥})^{n}

E [[e]] : FnEnv → ValEnv → V_{⊥}
D [[p]] : FnEnv → FnEnv
P [[p]] : FnEnv

Semantic equations

E [[x_{i}]]ηρ  = ρ_{i}
E [[c_{j}]]ηρ  = const_{j}
E [[if e_{1} then e_{2} else e_{3}]]ηρ = E [[e_{1}]]ηρ→E [[e_{2}]]ηρ| E [[e_{3}]]ηρ
E [[a_{j}(e_{1},…, e_{k})]]ηρ  = strictapp basic_{j} (E [[e_{1}]]ηρ,…, E [[e_{k}]]ηρ)
E [[f_{j}(e_{1},…, e_{k})]]ηρ  = strictapp η_{j} (E [[e_{1}]]ηρ,…, E [[e_{k}]]ηρ)

D [[f_{1}(x_{1} … x_{k}) = e_{1}; …; f_{n}(x_{1} … x_{k}) = e_{n}]] = λη.⟨E [[e_{1}]]η,…, E [[e_{n}]]η⟩ P [[p]] = fix D [[p]]

2. Strictness and neededness of a sub-expression

Recall that, in a lazy semantics, an expression e is strict in a (free) variable x if, whenever x is bound to a non-terminating expression then e fails to terminate. Similarly informally e needs x if reduction of e requires reduction of whatever expression x is bound to. In general neededness implies strictness, but the implication is proper — consider an expression such as “⊥” which is strict in all variables but does not need any variable. We now turn to the concepts of strictness and neededness of sub-expressions which are sensible even in call-by-value languages such as ours.

Strictness. We say that an expression e[e′] is strict in the subexpression e′ if, whenever e′ fails to terminate then so does e[e′]. This can be characterised in terms of the standard semantics as E [[e[⊥]]]ηρ = ⊥.

Abusing notation a little, given η ∈ FnEnv = (V^{k} → V_{⊥})^{n} we define updating of one component of η by:

η[(i, v⃗) ↦ w] = ⟨η_{1},…, η_{i−1}, η_{i}[v⃗ ↦ w], η_{i+1},…, η_{n}⟩.

Now, suppose f is a function in a program p, for example

f(x) = if x = 0 then 1 else x ∗ f(x − 1)

and v⃗ = (v_{1},…, v_{k}) is a tuple of argument values. We say e is strict in f(v⃗) if e fails to terminate under the assumption that f(v⃗) fails to terminate. This has two possible meanings according to whether we wish to consider (intensionally) the internal calls, so f(7) is strict in f(7), f(6),…, f(0), or (extensionally) the function as a black box, so f(7) is just strict in itself. In terms of E [[·]] the two choices can be written as

E [[e]](fix λη.((D [[p]]η)[(1, v⃗) ↦ ⊥]))ρ = ⊥ intensional
E [[e]](fix D [[p]])[(1, v⃗) ↦ ⊥]ρ = ⊥  extensional

We select the first, intensional, meaning — this corresponds to the intuitive motivation above and is formalised by the S [[·]] semantic function below.

Neededness. Above we said that an expression e is strict in a subexpression e′ if, whenever e′ is a non-terminating expression, then e fails to terminate. We similarly say that e needs e′ if under the (same) assumed operational semantics, reduction of e requires reduction of e′. For such an operational definition, strictness and neededness only differ subtly — they agree in all circumstances except that an expression which never terminates is always strict in any subexpression but may not need a given subexpression. Barendregt et al. [1] discuss neededness in the λ-calculus in some detail.

When defining neededness formally the problem becomes a little more subtle in that evaluation order which is invisible in the standard semantics may become visible in a neededness semantics.^{2} Typically, however, we wish to abstract from such operational detail and we follow the published version of [5]. It takes the view that the needed semantics consists of those function/argument pairs which are needed by some operational semantics consistent with the prescribed denotational semantics.

3. Formal strictness and neededness

Strict or needed calls are represented as sets of argument tuples associated with each function name. We will use the set C given by

C = P({1,…, n} × V^{k})

2Consider the contrived example \begin{aligned}main() & = h(f(1), g(2)) \\ f(x) & = f(x) \\ g(y) & = g(y) \\ h(x, y) & = x + y \end{aligned}

where given c ∈ C a pair ⟨i, v⃗⟩ ∈ c indicates that the i^{th} function f_{i} will be strict in (respectively need) the argument tuple v⃗.

Strictness semantics, S [[·]]. Recalling the function-update notation from section 2 and given ‘external’ calls c ∈ C, the strict calls in p are

S [[p]]c = ⋃_{⟨j,x⃗⟩∈c}{⟨i, v⃗⟩ | ((fixλη.((D [[p]]η)[(i, v⃗) ↦ ⊥])) ↓ j)(x⃗) = ⊥}

One should note that S is defined from D alone and does not use the actual expressions in function definitions.

Neededness semantics, N [[·]]. We may define a neededness function N which is very similar to S with the intuition

N [[p]]c = {⟨i, v⃗⟩ | ∃⟨j, w⃗⟩ ∈ c. evaluating f_{j}(w⃗) necessitates
the evaluation of f_{i}(v⃗)}

This rather informal definition may also be found in [3]. Due credit is not always given to the Cousots for the idea of neededness. Their language also sidestepped the problem of argument evaluation order apparent in the example in section 2 by requiring the programmer to serialise argument evaluation.

The above informal requirement can be formalised via Jones and Mycroft’s instrumented semantics which replaces values by pairs of values and function calls encountered during their evaluation. For our purposes it is convenient to write a separate semantic function C [[·]] yielding the second component of their pair as an adjunct to defining N [[·]]:

C [[x_{j}]]ηρ  = {}
C [[c_{j}]]ηρ  = {}
C [[if e_{1} then e_{2} else e_{3}]]ηρ = C [[e_{1}]]ηρ ∪ (E [[e_{1}]]ηρ→C [[e_{2}]]ηρ| C [[e_{3}]]ηρ)
C [[a_{j}(e_{1},…, e_{k})]]ηρ  = C [[e_{1}]]ηρ ∪ ⋯ ∪ C [[e_{k}]]ηρ
C [[f_{j}(e_{1},…, e_{k})]]ηρ  = C [[e_{1}]]ηρ ∪ ⋯ ∪ C [[e_{k}]]ηρ ∪
{⟨i, (E [[e_{1}]]ηρ,…, E [[e_{k}]]ηρ)⟩}

N [[p]]c = fix (λb ∈ C.c ∪ ⋃_{⟨i,v⃗⟩∈b} C [[e_{i}]](P [[p]])v⃗)

Minimal neededness. N [[·]] gave a ‘maximal’ neededness interpretation in which a variable is needed if some compatible interpreter needs it. There is also a ‘minimal’ neededness interpretation semantics which helps to identify the difference between S and N via a sandwich construction.

M [[p]]c = ⋃_{⟨j,x⃗⟩∈c}\{⟨i, v⃗⟩ | \begin{matrix}((fixλη.((D [[p]]η)[(i, v⃗) ↦ ⊥])) ↓ j)(x⃗) = ⊥ \\ ∧ (P [[p]] ↓ j)(x⃗) ≠ ⊥\} \end{matrix}

Notice that M [[·]] follows S [[·]] in only using the expressions in a program via their standard denotations.

Sandwich lemma. For all programs p, we have ∀c ∈ C. M [[p]]c ⊆ N [[p]]c ⊆ S [[p]]c.

The program f(x) = f(x) shows that all inclusions may be proper: S [[p]]{42} = V, N [[p]]{42} = {42} and M [[p]]{42} = {}.

4. Minimal function graphs

From either the needed calls N or the strict calls S we may define MFG semantics as semantic functions MFG_{X} (with X ranging over {N, S, M}).

First we need to define a notion of the space of (partial) function graphs G, ranged over by g. This is given by

G = P({1,…, n} × V^{k} × V_{⊥})

Jones and Mycroft used the space G′ given by

G′ = (V^{k} → (V_{⊥})_{⊥})^{n} ≅ {1,…, n} × V^{k} → (V_{⊥})_{⊥}

which has an obvious natural embedding in G. Our semantics only uses values in the embedding of G′ within G.

The three MFG semantics are mappings from ‘initial’ or ‘external world’ calls (in C) to reachable parts of the function graph (in G). It is convenient to define first a function graph semantics

\begin{matrix}FG [[p]] : C → G \\ FG [[p]]c = \{⟨i, v⃗, r⟩ | ⟨i, v⃗⟩ ∈ c ∧ (P [[p]] ↓ i)(v⃗) = r\}. \end{matrix}

The MFG semantics are then simply given by

MFG_{X} [[p]] : C → G
MFG_{X} [[p]]c = FG [[p]](X [[p]]c).

The rest of this section discusses the relationship between the standard semantics P and the minimal function graph semantics MFG_{N} and MFG_{S}.

Correctness. Unlike Jones and Mycroft’s formulation the MFG_{S} semantics is defined directly from the standard semantics. This makes it much easier to verify various connections between these semantics. The proofs may be found in the full version of the paper.

• Any non-⊥ result in an argument-result pair obtained by the minimal function graph interpretation can also be obtained by the standard semantics:

∀c ∈ C.⟨i, v⃗, r⟩ ∈ MFG_{S} [[p]]c ∧ r ≠ ⊥ ⇒ r = (P [[p]] ↓ i)(v⃗)

This is the only proof included in [5]. In this case it follows trivially from the definition of MFG_{S}. A similar result may be proved for the MFG_{N} semantics.

• Any non-⊥ result produced by the standard semantics can also be produced by the minimal function graph interpretation when given the arguments to the call as the specification of initial calls:

(P [[p]] ↓ i)(v⃗) = r ∧ r ≠ ⊥ ⇒ ⟨i, v⃗, r⟩ ∈ MFG_{S} [[p]]{⟨i, v⃗⟩}

This relationship was not stated or proved in [5]. For the MFG_{S} semantics it follows directly from the definition. A similar result may be proved for the MFG_{N} semantics.

• We have claimed that the semantics MFG_{N} is identical to the minimal function graph semantics in [5]. Although this is intuitively quite obvious the proof is not trivial as the needs in [5] are computed from a function environment which only contain information about previously called functions. A proof of this may be based on chaotic iteration sequences [3].

Sandwich theorem (from sandwich lemma).

∀c ∈ C. MFG_{M} [[p]]c ⊆ MFG_{N} [[p]]c ⊆ MFG_{S} [[p]]c.

5. Conclusion

We have shown how the minimum function graph semantics can be defined denotationally which facilitates statements and proofs of correctness. The process links the MFG semantics with the notions of strictness and neededness of subexpressions.

Acknowledgment. This research was supported by UK SERC grant GR/H14465 and by the Danish SNF ‘DART’ grant. We wish to thank Patrick and Radhia Cousot for their comments on a draft version of this paper.

References

[1] H. P Barendregt, J. R Kennaway, J. W Klop and M. R Sleep. Needed Reduction and Spine Strategies for the Lambda Calculus. In Information and Control, vol. 73, 1987.

[2] P Cousot and R Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In 4th POPL, Los Angeles, CA, pp. 238–252, Jan., 1977.

[3] P Cousot and R Cousot. Static determination of dynamic properties of recursive procedures. In Formal Description of Programming Concepts (E. J Neuhold, ed.). North-Holland, 1978.

[4] P Cousot and R Cousot. Inductive definitions, semantics and abstract interpretation In 19th POPL, Jan., 1992.

[5] N. D Jones and A Mycroft. Data Flow Analysis of Applicative Programs using Minimal Function Graphs. In 13th POPL, St. Petersburg, Florida, pp. 296–306, Jan., 1986.

[6] A Mycroft. Abstract Interpretation and Optimising Transformations for Applicative Programs. Ph.D. Thesis. Univ. of Edinburgh, Dec., 1981.

[7] A Mycroft and M Rosendahl. Minimal function graps are not instrumented. Computer Laboratory technical report. Univ. of Cambridge, 1992.