Categorical semantics of type theories are often characterized as structure-preserving functors. This is because in category theory both the syntax and the domain of interpretation are uniformly treated as structured categories, so that we can express interpretations as structure-preserving functors between them. This mathematical characterization of semantics makes it convenient to manipulate and to reason about relationships between interpretations. Motivated by this success of functorial semantics, we address the question of finding a functorial analogue in abstract interpretation, a general framework for comparing semantics, so that we can bring similar benefits of functorial semantics to semantic abstractions used in abstract interpretation. Major differences concern the notion of interpretation that is being considered. Indeed, conventional semantics are value-based whereas abstract interpretation typically deals with more complex properties. In this paper, we propose a functorial approach to abstract interpretation and study associated fundamental concepts therein. In our approach, interpretations are expressed as oplax functors in the category of posets, and abstraction relations between interpretations are expressed as lax natural transformations representing concretizations. We present examples of these formal concepts from monadic semantics of programming languages and discuss soundness.

翻译：类型论的范畴语义通常被刻画为保结构的函子。这是由于在范畴论中，语法和解释域均被统一视为带结构的范畴，从而我们可以将解释表示为它们之间的保结构函子。这种语义的数学刻画使得人们能够便捷地操作和推理解释之间的关系。受这种函子语义成功的启发，我们探讨如何在抽象解释（一种用于比较语义的通用框架）中寻找函子对应物，从而将函子语义的类似优势引入抽象解释中使用的语义抽象。主要差异在于所考虑的解释概念。具体而言，传统语义基于值，而抽象解释通常处理更复杂的性质。本文提出了一种面向抽象解释的函子方法，并研究了其中相关的基础概念。在我们的方法中，解释被表示为偏序集范畴中的反向弱函子，而解释之间的抽象关系则被表示为表示具体化的弱自然变换。我们通过编程语言中的单子语义展示了这些形式概念的实例，并讨论了其可靠性。