Towards a Unifying View on Monotone Constructive Definitions

Constructive definitions, including inductive and recursive definitions, are ubiquitous in mathematical texts and occur in a wide variety of computer science fields and Knowledge Representation applications. While in different areas there is a high level of familiarity with certain types of constructive definitions, fairly little interaction between different areas seems to exist, resulting in a lack of deep understanding of principles and their applications. This paper aims to fill this void by laying the foundations for a single unifying framework, bringing together a wide variety of definitions. First, we recall the principle of (monotone) inductive definition and its formalization in fixpoint theory. We discuss the constructive and the non-constructive interpretation of inductive definitions and the induction process. We then analyze examples, including but not limited to (co)inductive and (co)recursive definitions, found in a wide range of areas through the lens of our proposed framework.