School of Computer Science

Seminar details - Finite Sequential Procedures with observational ordering

Finite Sequential Procedures with observational ordering

( Theory (old) Series )

Dag Normann, Department of Mathematics, The University of Oslo, Blindern, N-0316 Oslo, Norway

Date and time: Tuesday 5th May 2009 at 14:00
Location: LG33, Learning Centre
Host: Martin Escardo

The sequential functionals of finite types with the observational ordering serve as a fully abstract model for PCF. They can be viewed as objects in Milner's fully abstract model based on Domain Theory, but have over the last 10-15 years been characterized in other ways as well. For many years it was an open problem if the sequential functionals forms directed complete partial orderings, which would mean that all objects in Milner's model are sequential, but in 2004 Normann showed that this is not the case. This result led Sazonov to conjecture that there are sequential functionals that are compact in Milner's model, but not if we restrict the attention to the sequential objects, and that not all sequential functionals commute with least upper bounds within the sequential functionals. In this lecture, I will introduce the Finite Sequential Procedures and construct the sequential functionals as standard parts of Hyperfinite Sequential Procedures. I will show that Sazonov's conjectures hold and discuss the frequency of the phenomena suggested by the conjectures. We will, for instance, see that even for non-pure types at level 2 the sequential functionals do not form dcpo's.

The technical results are joint with Vladimir Sazonov at the University of Liverpool.