Projecting sequential algorithms on strongly stable functions
44 pp. To appear in Annals of Pure and Applied Logic
Available as PostScript,
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.
Authors address: Laboratoire de Math'ematiques
Discrètes, UPR 9016 du CNRS, 163 avenue de Luminy, case 930, F 13288
MARSEILLE CEDEX 9. firstname.lastname@example.org.
BRICS WWW home page