Investigations on relative definability in PCF
Riccardo Pucella · eScholarship@McGill (McGill) · 1996
The focus of this thesis is the study of relative definability of first-order boolean functions with respect to the language PCF, a paradigmatic typed, higher-order language based on the simply-typed $ lambda$-calculus. The basic core language is sequential. We study the effect of adding construct that embody various notions of parallel execution. The resulting set of equivalence classes with respect to relative definability forms a supsemilattice analoguous to the lattice of degrees in recursion theory. Recent results of Bucciarelli show that the lattice of degrees of parallelism has both infinite chains and infinite antichains. By considering a very simple subset of Sieber's sequentiality relations, we identify levels in the lattice and derive inexpressibility results concerning functions on different levels. This allows us to explore further the structure of the lattice of degrees of parallelism and show the existence of new infinite hierarchies. We also identify four subsemilattices of this structure, all characterized by a simple property.