Analysing PCF and Kleene computability via sequential procedures

Add to your list(s) Download to your calendar using vCal

• John Longley, University of Edinburgh
• Friday 06 July 2012, 16:00-17:00
• B01 Mechanical Engineering.

If you have a question about this talk, please contact Paul Levy.

Sequential procedures (a.k.a. PCF Böhm trees) offer a model for PCF -style nested sequential computation in a higher order setting, closely related to the various game models for PCF , although more amenable to interpretation in a wide range of other models such as the Scott model. The ideas behind sequential procedures go back to early work of Sazonov; they also played an incidental role in work on game semantics for PCF , but it is only more recently that we have begun to exploit their potential as a model in their own right has begun to be exploited.

In this talk, I shall do three things:

(1) Give a direct and somewhat novel construction of the sequential procedure model via an untyped lambda-algebra, emphasizing in particular that a surprising amount of the theory works without any reference to the type structure of PCF .

(2) Show how combinatorial reasoning on sequential procedures can be used to obtain expressivity results about (sublanguages of) PCF . In particular, by identifying a certain submodel of the sequential procedure model, we obtain a new result: no bar recursion operator is definable in System T plus minimization.

(3) Use sequential procedures to shed new light on Kleene (S1-S9) computability in the world of total functionals, again offering semantic characterizations of some natural expressivity distinctions.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• B01 Mechanical Engineering
• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.