Towards Operational Semantics of Contexts in Functional Languages

David Sands diku, University of Copenhagen^{∗}

Abstract

We consider operational semantics of contexts (terms with holes) in the setting of lazy functional languages, with the aim of providing a balance between operational and compositional reasoning, and a framework for semantics-based program analysis and manipulation.

Introduction

In this note we initiate a new direction in the semantics of functional programs. The approach is based on operational semantics; our aims are to provide a operational route to high-level semantic issues, such as program analysis and sourceto-source transformation. We investigate the idea of giving a direct operational semantics to program contexts—that is, “incomplete” programs containing a number of holes in the place of some subexpressions.

The idea of providing an operational semantics for contexts has been studied by Larsen (et al) for process algebras [Lar86][LX91]. In that setting, a context is viewed as an action transducer, which consumes actions provided by its internal processes (the holes) and produces externally observable actions. The operational semantics of contexts contains transitions of the form

C \overline{}_{a}^{b} C′

which is interpreted as: by consuming action a, context C can produce action b and change into C′.

We describe some initial steps towards providing an operational semantics for contexts in a functional setting.

Functional Action-Transducers

In the process setting a context is viewed as an action transducer. What is the corresponding notion for a context in the functional setting? In a functional language, the role of an “action” is played by the observables of the language: namely a lazy data constructor— cons, true, “λ”.

∗Universitetsparken 1, 2100 København Ø, DENMARK. e-mail: dave@diku.dk

We take a bold step, and demand that the “actions” should themselves be contexts—but not arbitrary contexts. They should be contexts built from the observables of the language. We will call these observable contexts. Observable contexts will be ranged-over by O, O′, etc. For some context C containing occurrences of a single hole, if we have a transduction of the form:

C \overline{}_{O}^{O′} C′

then we will require that:

C[O] ≃ O′[C′] (∗)

where the notation C[e] denotes context C with e placed “in the hole”, and ≃ denotes the usual operational equivalence, extended to capture-free contexts in the obvious way. This equation does not capture everything we expect from a context semantics. What we expect is that the transduction should be as lazy as possible — ie. we could not have found a smaller “input” O that would have given the same observable “output” O′. If the language is sequential[Ber78] then we expect the semantics to give us the minimal O.

For example, a context of the form if [ ] = 0 then C_{1} else (leaf C_{2}) (containing multiple occurrences of a single hole), where leaf is a constructor, would have a transduction:

         if [ ] = 0 then C_{1} else (leaf C_{2}) leaf ^{[ ]} \overline{} suc ^{[ ]} C_{2} ∘ suc[ ]

where ∘ is context composition, so C_{2} ∘ suc[ ] denotes the context C_{2}[suc[ ]].

Problems Giving a full operational semantics for contexts is difficult because:

• contexts can consume without producing an observable.

For example if [ ] = 0 … can consume a constructor without necessarily being able to produce anything. (Similar situation would arise in Larsen’s work if one did not consider the silent action τ to be observable.)

• The number of occurrences of a given hole may increase under transduction (assuming we use some mechanism like β-reduction in our semantics).

• The number of distinct holes in a context can increase under transduction, in the presence of n-ary constructors.

eg. If C_{1} has a single hole, and C_{1} \overline{} cons^{[ ]}1^{[ ]}2 C_{2} then C_{2} has two distinct

holes.

• How do we treat higher-order functions?

• Contexts can capture variables by means of binding operators

     eg. case e of nil ⇒ e′ cons h t ⇒ C_{2} .

A Simplified Case

As a first step we study only a very simple language. We avoid almost all of the above problems by considering a language with the following features:

• First-order functions

• No binding operators

• Unary constructors and constants (= nullary constructors) as the only values.

The language we consider consists of first-order recursion equations with possible pattern-matching on the first argument (non-nested), based on unary or nullary constructors. Here are some example definitions:

                  add 0 x  = x
                  add (suc y) x = suc (add y x)
                  twice x  = add x x

Notation Let u range over both unary constructors (eg. suc) and constants (eg. 0,true etc.). The observable contexts are then given by

O ::= [ ] | u | u O

For simplicity of presentation, we will only consider contexts with a single hole (occurring zero or more times). (We will consider an expression to be a context with zero occurrences of the hole.) For this restricted language, the extension to handle polyadic contexts (contexts with several distinct holes) is straightforward (eg. borrowing the notations from [LX91]).

In the context transductions, if u is a unary constructor, then we write observable context u [ ] as simply u, and occurrences of the trivial context [ ]

will simply be omitted from the transductions, so we will write C suc \overline{}C′ in

place of C suc^{[ ]} \overline{} [ ] C′. If u is a constant, then u can also be denoted u(). We add

the unit expression () to the language of contexts.

Language Rules

We define the following transductions involving terms of the language:

u C \overline{}^{u} C  (1)

f C⃗ \overline{}e\{x⃗ := C⃗\}  if f x⃗ = e  (2)

\frac{C_{1} \overline{}_{O}^{u} C_{2}}{f C_{1} C⃗ \overline{}_{O} e\{y := C_{2}\}\{x⃗ := C⃗ ∘ O\}} if f (u y) x⃗ = e  (3)

In the last rule, the composition C⃗∘Con′ denotes the vector of contexts obtained by composing each context in C⃗ with Con′. To check that the rule satisfies the desired property (∗), assume that from the antecedent we have

C_{1} ∘ O ≃ u C_{2}

then

(f C_{1} C⃗) ∘ O ≃ f (C_{1} ∘ O) (C⃗ ∘ O)
≃ f (u C_{2}) (C⃗ ∘ O)
≃ e{y := C_{2}}{x⃗ := C⃗ ∘ O}

These rules are straightforward, since they follow the “small-step” semantics of the language (ie. they are non compositional.) We recover the ability to reason compositionally using the following context rules:

Context Rules

[ ] \overline{}_{u}^{u} [ ] (u unary)  (4)

[ ] \overline{}_{u}^{u} () (u constant)  (5)

C \overline{}C  (6)

\frac{C_{1}  \overline{}_{O′_{1}}^{O_{1}} C_{2} C_{2}  \overline{}_{O′_{2}}^{O_{2}} C_{3}}{C_{1} \overline{}_{O′_{1}∘O′_{2}}^{O_{1}∘O_{2}} C_{3}}  (7)

\frac{C_{1}  \overline{}_{O_{2}}^{O_{1}} C′_{1} C_{2}  \overline{}_{O_{3}}^{O_{2}} C′_{2}}{C_{1} ∘ C_{2}  \overline{}_{O_{3}}^{O_{1}} C′_{1} ∘ C′_{2}}  (8)

The last rule is the uniform rule of [Lar89][LX91], and it characterises all the transductions of composed contexts.

Properties

Closed expressions can be viewed as contexts containing zero holes. In this way the rules above can be seen to subsume the usual large-step and smallstep structural operational semantics. Suppose the large step semantics defines an evaluation relation ⇓ (we omit the routine definition), then we have the following:

e ⇓ a ⟺ e \overline{}^{u} e′ ∧ (u e′ ≡ a)

For example, if I is the identity function, then we have the following example proof:

             compose \frac{2 \overline{I (suc 0) \overline{}(suc 0)} 1 \overline{(suc 0) suc \overline{}0}}{I (suc 0) suc \overline{}0}

But this is not the whole story for evaluation of closed expressions. Unlike

the structural operational semantics for ⇓, the proof of e \overline{}^{u} e′ is not unique.

An important point is that by use of the composition rule (8) we can vary the compositionality. This means that when we need to prove a property of a function application f e, we can split this into a context f [ ] and the sub-term e, and derive the transition of the composed system in terms of these components.

As an example, using the functions defined earlier, consider the term twice (I (suc0)). We can prove that

                       7 \frac{2 \overline{twice [ ] → add [ ] [ ]} A}{twice [ ] suc \overline{} suc add [ ] (suc [ ])}

where A is the sub-proof:

      7 \frac{4,1 \frac{[ ] suc \overline{} suc [ ]}{add [ ] [ ] \overline{} suc   suc add [ ] (suc [ ]) suc \overline{}add [ ] (suc [ ])}}{add [ ] [ ] suc \overline{} suc   add [ ] (suc [ ])}

and so using the composition rule we obtain:

            8 \frac{twice [ ] suc \overline{} suc add [ ] (suc [ ])  I (suc 0) suc \overline{}0}{twice (I (suc 0)) suc \overline{}add 0 (suc 0)}

Note that in the example, because of the use of the compositional rule, there is only one sub-proof for the expression I (suc 0), whereas under the standard call by name SOS we would have two sub-proofs.

We conjecture that proofs which always treat function calls compositionally in this way (we need to generalise to n-ary contexts to do this for n-ary functions) have size proportional to the number of evaluation steps required under standard call-by-need computation. This form of proof corresponds to the demand function used in Bjerner and Holmström’s call-by-need time-analysis [BH89].

Further Work

In the remainder of this paper we consider the directions for further development, which mostly concern tackling the problems of richer languages.

Polyadic Contexts

The above semantics is easily extended to handle polyadic contexts, but if we go beyond just unary constructors then the extension quickly becomes notationally complex. The problem is that consuming an observable context may give rise to several new holes, and producing a observable context means that a transduction may result in several contexts. Our proposal for dealing with these problems is to adopt a different kind of transduction. Instead of requiring that a transduction

C \overline{}_{O}^{O′} C′

implies that C ∘ O ≃ O′ ∘ C′, the requirement is that

C ∘ O ≃ O′ ∘ C′ ∘ O

In this way the “type” of the holes in the derived context C′ is the same as in C. The addition of n-ary constructors means that C′ must be a vector of contexts.

With this interpretation of context transductions, the uniform composition rule now has the form:

\frac{C_{1}  \overline{}_{O_{2}}^{O_{1}} C′_{1} C_{2}  \overline{}_{O_{3}}^{O_{2}} C′_{2}}{C_{1} ∘ C_{2}  \overline{}_{O_{3}}^{O_{1}} C′_{1} ∘ O_{2} ∘ C′_{2}}

Higher-Order Functions

If we focus on contexts which cannot capture variables, then higher-order functions can be thought of as introducing an extra hole. We anticipate that to deal with polyadic contexts in their full generality we will need a notation along the lines of Martin-Lö f’s theory of arities, so (X)C will denote a context with a single hole named X. Then a lambda-context could have a transition

(Y⃗)λy.C \overline{}^{λ} (X)(Y⃗)C X ∉ Y⃗ .

Abstract Contexts and Relativised Equivalence

Two natural directions are to consider static analysis problems, and notions of relativised equivalence. We should consider:

• Bisimulation-like characterisations of context-equivalence along the lines of [Abr90][How89].

• Relativised equivalences ≃_{C}:

e ≃_{C} e′ ⟺ C[e] ≃ C[e′]

• Semantics for abstract observable contexts (whose meaning is a set of contexts);

• A notion of environment as a dual to (abstract) observable contexts, thus generalising the demand semantics of [San93].

These points should enable an operational formalisation of context analysis of the form of [Hug87][WH87].

Guarded Contexts

In a somewhat orthogonal study we have considered context semantics for a restricted class of contexts (a form of guarded contexts) for a higher-order language with binding operators and arbitrary lazy constructors. The principle technical problem in this context semantics is to handle holes which occur under bound variables. This operational semantics of contexts finds immediate application to the problem of correct folding in program transformation. It also provides a simple form of “applicative bisimulation up to context” proof technique, a la Sangiorgi [San94].

Acknowlegement An earlier investigation of the subject of this note was undertaken together with Sebastian Hunt a few years ago. Our attempt failed, because we were over-ambitious in trying to give only compositional rules. But a number of ideas crystalised from our attempt, and have influenced the current development. One idea in particular —that the “actions” should themselves be contexts—is due to Sebastian.

References

[Abr90] S. Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65–116. Addison Wesley, 1990.

[Ber78] G. Berry. Stable models of typed lambda calculi. In 5th Coll. on Automata Languages and Programming, LNCS 62. Springer-Verlag, 1978.

[BH89] B. Bjerner and S. Holmström. A compositional approach to time analysis of first order lazy functional programs. In Functional Programming Languages and Computer Architecture, conference proceedings, pages 157–165. ACM press, 1989.

[How89] D. J. Howe. Equality in lazy computation systems. In Fourth annual symposium on Logic In Computer Science, pages 198–203. IEEE, 1989.

[Hug87] R. J. M. Hughes. Backwards analysis of functional programs. Research Report CSC/87/R3, University of Glasgow, March 1987.

[Lar86] K. G. Larsen. Context-Dependent Bisimulation Between Processes. PhD thesis, Department of Computing, University of Edinburgh, 1986.

[Lar89] K. G. Larsen. Compositinal theories based on an operational semantics of contexts. In Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, number 430 in LNCS. Springer-Verlag, 1989.

[LX91] K. G. Larsen and L. Xinxin. Compositinality through an operational semantics of contexts. J. Logic and Computation, 1(6):761–795, 1991.

[San93] D. Sands. A naïve time analysis and its theory of cost equivalence. TOPPS report D-173, DIKU, 1993. To appear: Journal of Logic and Computation, 1995.

[San94] D. Sangiorgi. On the bisimulation proof method. Technical report, University of Edinburgh, 1994.

[WH87] P. Wadler and R. J. M. Hughes. Projections for strictness analysis. In 1987 Conference on Functional Programming and Computer Architecture, pages 385–407, Portland, Oregon, September 1987.