Adventures in Computational Complexity for Higher Types

Photograph of James Royer

James Royer

(New York)

A higher-type functional is a function that takes as input or produces as output another function. Programs for higher type functionals are a standard part of many branches of computing. For instance, the constructions in cryptography that transform a one-way function into a cryptographically strong hash function. Other examples come from learning theory, effective analysis, computational complexity theory, ... and functional programming. In fact, since modules and objects are essentially higher-type notions, higher-types pervade contemporary computing.

Books on algorithms are mostly silent on higher-types. In areas involving particular sorts of higher-type algorithms, their analysis is largely ad hoc, piecemeal, or non-existent. This is because reasoning about time and space complexity is of full of hard subtle conceptual issues --- which make for some very nice problems.

This talk will sketch one path of exploration into the computational complexity of higher-type functions. Our focus will be on higher-type analogues of the polynomial-time computable functions. I will examine the issue of type-level 2 notions of poly-time, where the situation is reasonably well understood, and the analogous issue for type-level 3, where we have only pieces of the picture. In particular, I will discuss work by Irwin, Kapron, and myself that confirms a conjecture by Seth that two seemingly similar notions of ``type-level 3 poly-time'' in fact differ.
Thursday 21st October 2004, 14:00
Robert Recorde Room
Department of Computer Science