Projecting sequential algorithms on strongly stable functions

Thomas Ehrhard

44 pp. To appear in Annals of Pure and Applied Logic

Abstract:

We relate two sequential models of PCF: the sequential algorithm model due to Berry and Curien and the strongly stable model due to Bucciarelli and the author. More precisely, we show that all the morphisms arising in the strongly stable model of PCF are sequential in the sense that they are the ``extensional projections'' of some sequential algorithms. We define a model of PCF where morphisms are ``extensional'' sequential algorithms and prove that any equation between PCF terms which holds in this model also holds in the strongly stable model.

Comments:
Authors address: Laboratoire de Math'ematiques Discrètes, UPR 9016 du CNRS, 163 avenue de Luminy, case 930, F 13288 MARSEILLE CEDEX 9. ehrhard@lmd.univ-mrs.fr.

BRICS WWW home page