Non-constructive proof of a fixed point theorem on lexicographic lattice structures

In this thesis, we develop a novel, non-constructive proof of the fixed point theorem proposed by A. Charalambidis, G. Chatziagapis and P. Rondogiannis (LICS20). This theorem proves the existence of a least fixed point of functions that possess a restricted form of monotonicity, and are defined over some specially structured partially ordered sets, which we will call lexicographic lattice structures. Our results give as a special case the well-known Knaster-Tarski theorem when restricted to monotonic functions.

The initial proof of the theorem, as presented at LICS 2020, is constructive. Our novel proof is simpler and it gives an alternative intuition and a deeper understanding of the theorem. Furthermore, we prove that the sets of pre-fixed, post-fixed and fixed points of function over those structures form a complete lattice. Our proofs have been verified through the Coq proof assistant. Our results have direct applications in fields of Computer Science where non-monotonic formalisms are being used, such as Artificial Intelligence, Logic Programming and Formal Language Theory.