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.

翻译：类型理论的范畴语义常被刻画为保持结构的函子。这是因为在范畴论中，语法与解释域被统一视为带结构范畴，从而可将解释表示为两者间的保持结构函子。这种语义的数学刻画使解释间的关系操纵与推理变得便捷。受函子语义这一成功范例的启发，我们探讨在抽象解释中寻找函子类比的途径——抽象解释是一种比较语义的通用框架，旨在将函子语义的类似优势引入抽象解释所使用的语义抽象中。主要差异涉及所考虑的解释概念：传统语义基于值，而抽象解释通常处理更复杂的性质。本文提出一种面向抽象解释的函子方法，并研究其中的基础概念。在该方法中，解释被表述为偏序集范畴上的op- lax函子，而解释间的抽象关系则被表述为代表具体化的lax自然变换。我们通过编程语言中的单子语义实例展示这些形式化概念，并讨论其可靠性。