Data types as lattices : retractions, closures and projections

This paper presents the mathematical principles of lattice theory oriented toward the theory of computation, and attempted is a systematic treatment of this lattices theory that involves the definition of data structures.

Abstract

The application of lattice theory to data types définition involves a number of frequently considered notions: retractions, closures, projections and représentations.This paper provides a systematic theory from a rather gênerai point of view, namely by considering monotonie rather than continuous operators.The results are applied to characterize some special lattices.\injective and compactly generated lattices. INTRODUCTION0.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 définitions as fixed point of monotonie (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 formai Systems of X-calculus and combinatory logic it was accepted later as a proper procedure for the définition 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 a mathematical meaning for an operational notion.But it is important to notice that-contrary to the situation for recursive definitions-it is not clear whether the mathematical notion of self-application corresponds to the operational.More recently (see [7]) the lattice approach has been found useful for the définition of data structures.In all these applications a number of constructions appear frequently: retractions, projection, représentations.0.2.We attempt hère a systematic treatment of the lattice theory involving the définition of data structures.We consider monotonie rather than conti-