Normal functors, power series and \(\lambda\)-calculus (Q1103618)

The origin of this paper was in \(\Pi^ 1_ 2\)-logic: cf. \textit{J.-Y. Girard}, Proof-theory and logical complexity, Volume I (1987; Zbl 0635.03052); its ultimate outcome is the author's ``linear logic'' that might very well revolutionize the way we look at and understand programs - and which is closely related to relevant logic. It looks at ``continuous functionals'' from a functorial - instead of a topological - point of view. These are also considered in Computer Science for models of some \(\lambda\)-calculi. Here ``continuous functionals'' mean ``functors preserving direct limits, infinite pull-backs and kernels''. They are called ``normal functors'', since they have a normal form, and are expressible (up to isomorphism) by power series. The normal functors from \(Set^ A\) to \(Set^ B\) are the objects of a category \(Set^{Int(A).B}\). The usual operations and constructs (e.g., \(\lambda\)- abstraction, the \(\lambda\)-calculus, the Gödel-system \({\mathcal T}\), probabilistic algorithms, etc.) are seen to be interpretable in this setting. The appendix A discusses qualitative domains - the simplified analogue of Scott domains, while Appendix B studies sums of types.