page 1  (15 pages)
2to next section

Expanding the text here will generate a large amount of data for your browser to display

On the Observable Properties of

Higher Order Functions that

Dynamically Create Local Names

(preliminary report)

<_author_search_(andrew pitts)>Andrew Pitts1 <_author_search_(ian stark)>Ian Stark2

University of Cambridge Computer Laboratory,
<_author_search_(pembroke street)>Pembroke Street, Cambridge CB2 3QG, England

Tel: +44 223 334629 Fax: +44 223 334678
Email: fAndrew.Pitts,


The research reported in this paper is concerned with the problem of reasoning about properties of higher order functions involving state. It is motivated by the desire to identify what, if any, are the difficulties created purely by locality of state, independent of other properties such as side-effects, exceptional termination and nontermination due to recursion. We consider a simple language (equivalent to a fragment of Standard ML) of typed, higher order functions that can dynamically create fresh names. Names are created with local scope, can be tested for equality and can be passed around via function application, but that is all.

We demonstrate that despite the simplicity of the language and its operational semantics, the observable properties of such functions can be very subtle. Two methods are introduced for analyzing Morris-style observational equivalence between expressions in the language. The first method introduces a notion of `applicative' equivalence incorporating a syntactic version of O'Hearn and Tennent's relationally parametric functors and a version of representation independence for local names. This applicative equivalence is properly contained in the relation of observational equivalence, but coincides with it for first order expressions (and is decidable there). The second method develops a general, categorical framework for computationally adequate models of the language, based on Moggi's monadic approach to denotational semantics. We give examples of models, one of which is fully abstract for first order expressions. No fully abstract (concrete) model of the whole language is known.

1Supported by UK SERC grant GR/G53279 and CEC ESPRIT project CLICS-II
2Supported by UK SERC studentship 91307943 and CEC SCIENCE project PL910296