A Category-Theoretic Perspective on Higher-Order Approximation Fixpoint Theory
Samuele Pollaci, Babis Kostopoulos, Marc Denecker, Bart Bogaerts
TL;DR
This work develops a category-theoretic foundation for higher-order Approximation Fixpoint Theory (AFT) by introducing an approximation category ${\textbf{Approx}}$ and an approximation system that assigns, for each type, a corresponding approximation space and exact elements within a Cartesian closed framework. By proving that standard AFT and the CRS18 higher-order extension sit inside this unified setting, the paper provides a generic method to inductively build higher-order approximation spaces and to apply AFT techniques uniformly across type levels. A key contribution is the explicit notion of exactness for higher-order objects, enabling identification of two-valued models and exact stable models, and the introduction of a new approximator that handles existential quantifiers in rule bodies. The LUcons extension, with its $L\otimes U$ spaces and ILP/IGP conditions, offers a flexible, Cartesian-closed-compatible alternative that resolves previous pathologies and broadens the applicability of AFT to non-monotonic reasoning, abstract argumenation, and related higher-order domains.
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).