A Combinatory Algebra for Sequential Functionals of Finite Type
Jaap van Oosten · Cambridge University Press eBooks · 1999
It is shown that the type structure of finite-type functionals associated to a combinatory algebra of partial functions from ℕ to ℕ (in the same way as the type structure of the countable functionals is associated to the partial combinatory algebra of total functions from ℕ to ℕ), is isomorphic to the type structure generated by object N (the flat domain on the natural numbers) in Ehrhard's category of “dI-domains with coherence”, or his “hypercoherences”. Introduction PCF , “Gödel's T with unlimited recursion”, was defined in Plotkin's paper. It is a simply typed λ-calculus with a type o for integers and constants for basic arithmetical operations, definition by cases and fixed point recursion. More important, there is a special reduction relation attached to it which ensures (by Plotkin's “Activity Lemma”) that all PCF -definable higher-type functionals have a sequential, i.e. non-parallel evaluation strategy. In view of this, the obvious model of Scott domains is not faithful, since it contains parallel functions. A search began for “fully abstract” domain-theoretic models for PCF . A proliferation of ever more complicated theories of domains saw the light, inducing the father of domain theory, Dana Scott, to lament that “there are too many proposed categories of domains and […] their study has become too arcane”, a judgement with which it is hard to disagree.