A Category-Theoretic Perspective on Higher-Order Approximation Fixpoint Theory

TL;DR

This paper extends Approximation Fixpoint Theory to higher-order logic by employing Category Theory, specifically Cartesian closed categories, enabling the analysis of higher-order definitions within a rigorous algebraic framework.

Contribution

It introduces a formal categorical framework that generalizes AFT to higher-order environments, bridging a gap in the existing algebraic semantics for non-monotonic logics.

Findings

Extends AFT to higher-order logic using category theory

Preserves structures necessary for AFT in higher-order settings

Generalizes previous AFT frameworks to more complex logic environments

Abstract

Approximation Fixpoint Theory (AFT) is an algebraic framework designed to study the semantics of non-monotonic logics. Despite its success, AFT is not readily applicable to higher-order definitions. To solve such an issue, we devise a formal mathematical framework employing concepts drawn from Category Theory. In particular, we make use of the notion of Cartesian closed category to inductively construct higher-order approximation spaces while preserving the structures necessary for the correct application of AFT. We show that this novel theoretical approach extends standard AFT to a higher-order environment, and generalizes the AFT setting of arXiv:1804.08335 . Under consideration in Theory and Practice of Logic Programming (TPLP).