Ian Stark

On the Observable Properties of Higher Order Functions
that Dynamically Create Local Names (Preliminary Report)

Andrew Pitts and Ian Stark

In Proceedings of the ACM SIGPLAN Workshop on State in Programming Languages, Copenhagen, Denmark, June 12, 1993. Research Report YALEU/DCS/RR-968, pages 31–45. Yale University Department of Computer Science, 1993.

Fetch a preprint of the paper (PDF, 179k). Go to other papers, talks or my home page.


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 non-termination 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.

  author =       {Andrew M. Pitts and Ian Stark},
  title =        {On the Observable Properties of Higher Order Functions
                  that Dynamically Create Local Names (Preliminary
  booktitle =    {Proceedings of the ACM SIGPLAN Workshop on State in
                  Programming Languages},
  pages =        {31--45},
  series =       {Research Report},
  number =       {YALEU/DCS/RR-968},
  publisher =    {Yale University Department of Computer Science},
  year =         1993,
  url =          {http://www.inf.ed.ac.uk/~stark/obspho-sipl.html},
  pdf =          {http://www.inf.ed.ac.uk/~stark/obspho-sipl.pdf}

This research was supported by: UK SERC grant GR/G53279; CEC ESPRIT project CLICS-II; UK SERC studentship 91307943; and CEC SCIENCE project PL910296.

Page last modified: Thursday 27 November 2008