![]() |
![]() |
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
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:
Note that ex-directory lists are not shown. |
Other listsSERENE Seminars Physics and Astronomy Colloquia Molecular and Medical Physics Seminar SeriesOther talksQuantum simulations using ultra cold ytterbium Modelling uncertainty in image analysis. Sensing and metrology activities at NPL, India Provably Convergent Plug-and-Play Quasi-Newton Methods for Imaging Inverse Problems Hodge Theory: Connecting Algebra and Analysis TBC |