Data types as lattices: retractions, closures and projections

10.1 This paper considers the mathematical principles of lattice theory oriented toward the theory of computation. This relatively new direction can be traced back to the explanation of recursive definitions as fixed point of monotonic (actually continuous) operators. The usual operational explanation (Kleene's first recursion theorem) is replaced by a pure lattice theoretical existence theorem. Another problem for which the lattice approach provided a significant clarification was the so-called self-application of functions. Introduced first in some formal systems of A-calculus and combinatory logic it was accepted later as a proper procedure for the definition of algorithms in programming languages, the implication being then that there existed a clear operational meaning for such procedure. Again the discovery by Scott of models in which such self-application was available provided