Defining the Polynomial Time Functions over N in Nuprl
by Robert L. Constable
I will discuss some of the detail associated with giving a clean inductive definition of the polynomial time computable functions following the methods of Bellantoni and Cook. A number of interesting questions come up about extending the approach to higher order functions.
Some of the seminar will be devoted to discussing these questions and considering the possibility of implementing the Bellantoni and Cook results about their definition.