Higher Type Computability: Kleene Recursion in Higher Types

Stan Wainer, University of Leeds. Part of the proofs, constructions and computations seminar series.

Two contrasting notions of computability on higher types will be briefly surveyed, both tracing back to the 1960s, and neither receiving as much attention nowadays as they deserve. The recent book by John Longley and Dag Normann "Higher-Order Computability" (Springer 2015) is an excellent source of up-to-date material.

Lecture 1: Kleene Recursion in Higher Types

The inductive relation {e}(F,f,x) = y. Recursion in a higher-type object, such as 2E. Stage comparison and Gandy Selection. Characterization of \Delta^1_1 as the 1-section of 2E. Grilliot's theorem on effective discontinuity. Kleene/Kreisel countable (or continuous) functionals.

Lecture 2: Platek-Scott-Ershov Computability See next week.

Stan Wainer, University of Leeds