University of Birmingham > Talks@bham > Theoretical computer science seminar > The recursion hierarchy for PCF is strict

## The recursion hierarchy for PCF is strictAdd to your list(s) Download to your calendar using vCal - John Longley (Edinburgh)
- Tuesday 08 September 2015, 11:00-13:00
- CS 217.
If you have a question about this talk, please contact Neel Krishnaswami. Let $\PCF_k$ denote the sublanguage of Plotkin’s $\PCF$ in which fixed point operators $Y_\sigma$ are admitted only for types $\sigma$ of level $\leq k$. We show that the languages $\PCF_k$ form a strict hierarchy, in the sense that for each $k$, there are closed programs of $\PCF_{k+1}$ that are not observationally equivalent to any programs of $\PCF_k$. This answers a question posed by Berger in 1999. Our proof makes substantial use of the theory of \emph{nested sequential procedures} (also called \emph{$\PCF$ B\”ohm trees}). I plan to give the talk in two parts: first, a discussion of the result with a general overview of the method of proof, and then (for any who are interested) a closer look at some of the technical details of the proof. This talk is part of the Theoretical computer science seminar series. ## This talk is included in these lists:- CS 217
- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Theoretical computer science seminar
- computer sience
Note that ex-directory lists are not shown. |
## Other listsMet and Mat Seminar Series Nuclear physics seminars Seminars on Advanced Materials## Other talksAdvancing biomedical photoacoustic imaging using structured light and optical microresonators Order-theoretic fixed point theorems Plasmonic Electronic Paper View fusion vis-à-vis a Bayesian interpretation of Black-Litterman for portfolio allocation [Colloquium:] Aperture Fever: The Extremely Large Telescope Module tensor categories and the Landau-Ginzburg/conformal field theory correspondence |