A Fixed Point Theorem on Lexicographic Lattice Structures

We introduce the notion of a lexicographic lattice structure, namely a lattice whose elements can be viewed as stratified entities and whose ordering relation compares elements in a lexicographic manner with respect to their strata. These lattices arise naturally in many non-monotonic formalisms, such as normal logic programs, higher-order logic programs with negation, and boolean grammars. We consider functions over such lattices that may overall be non-monotonic, but retain a restricted form of monotonicity inside each stratum. We demonstrate that such functions always have a least fixed point which is also their least pre-fixed point. Moreover, we prove that the sets of pre-fixed and post-fixed points of such functions, are complete lattices. For the special case of a trivial lexicographic lattice structure whose elements essentially consist of a unique stratum, our theorem gives as a special case the well-known Knaster-Tarski fixed point theorem. Moreover, our work considerably simplifies and extends recent results on non-monotonic fixed point theory, providing in this way a useful and convenient tool in the semantic investigation of non-monotonic formalisms.