Recursion on the partial continuous functionals
Helmut Schwichtenberg · Cambridge University Press eBooks · 2007
Introduction. We describe a constructive theory of computable functionals, based on the partial continuous functionals as their intendend domain. Such a task had long ago been started by Dana Scott [30], under the well-known abbreviation LCF. However, the prime example of such a theory, Per Martin-Löf's type theory [23] in its present form deals with total (structural recursive) functionals only. An early attempt of Martin-Löf [24] to give a domain theoretic interpretation of his type theory has not even been published, probably because it was felt that a more general approach — such as formal topology [13] — would be more appropriate. Here we try to make a fresh start, and do full justice to the fundamental notion of computability in finite types, with the partial continuous functionals as underlying domains. The total ones then appear as a dense subset [20, 15, 7, 31, 27, 21], and seem to be best treated in this way.