Unique fixpoints in complete lattices with applications to formal languages and semantics

Abstract

Recursive definitions can be modeled either using complete partially ordered sets and applying least-fixpoint theorems or in the context of complete lattices and Tarski's fixpoint theorem which states that all fixpoints of a monotonic operator form a complete lattice, too. Uniqueness is analyzed independently by introducing a metric and looking for contraction properties or by special case analysis depending on application characteristics. We show how Tarski's approach can be extended by characterizing uniqueness. The obtained theorems generalize Arden's lemma related to linear equations of formal languages. Other applications are the uniqueness of equationally defined contextfree languages and of recursive program descriptions.