Full abstraction for the second order subset of an ALGOL-like language (preliminary report)

Abstract

The search for fully abstract models of block structured languages with local variables began in the mid 80s. A series of observationalcongruences in [MeyerS88] revealed the shortcomings of existing models and served as test cases for new ones. The most recently developed models in [OHearnT93, Sieber93] could prove all these test equivalences, but it was not known whether they are fully abstract. In this paper we show that (a slight variant of) the model in [Sieber93] IS fully abstract for the second order subset of an ALGOL-like language (which subsumes all the test equivalences). The general technique for constructing our model is still the same as in [MeyerS88], namely we use `relationally structured locally complete partial orders` with `relation preserving locally continuous functions`. The particular model differs from the one in [MeyerS88] by having the `finest possible relation structure`, an idea which we have developed in [Sieber92] for constructing a fully abstract model for the second order subset of sequential PCF. The full abstraction proof also uses some ideas from [Sieber92], but for its main part we had to develop new techniques in order to cope with the more complicated (in comparison with PCF) setting of an ALGOL-like language.