Browse Theses

This dissertation studies the abstract characterization of sequential computation. The goal is to be able to develop a theory of sequential computation to answer questions such as "Is a given function f sequential__ __" Often presented as the full abstraction problem for the language PCF, the characterization of sequential computation, and especially higher-order sequential computation over function spaces, has been an open problem for a long time, and has attracted considerable research and interest.

Why would sequential computation prove more difficult to formalize semantically than non-sequential computation__ __ The problem is that sequentiality does not quite make sense as a property of a set-theoretic function, and some structure is necessary for expressing the sequentiality of computation--for instance, one might need to talk about argument positions and order of evaluation. But it is not clear how this structure should be represented abstractly, especially for higher-order sequential computation over arrow types.

This work proposes to formalize sequential computation using a notion of index structures. Indices represent atomic computational steps in an incremental demand-driven computation over a domain of values, acting as queries about the value being computed. By restricting our attention to functions that compute using only valid indices--these are the continuous functions with respect to a certain generalized topology--the problem may be reduced to a search for suitable index structures. We present constructions of index structures that capture some aspects of sequential computation, and outline further considerations and refinements necessary for a satisfactory formalization of higher-order sequential computation.