Shin-Ya Katsumata
email: s-katsumata@nii.ac.jp

Xavier Rival
email: rival@di.ens.fr

Jérémy Dubut
email: jeremy.dubut@aist.go.jp

Rival, Dubut Katsumata

A Categorical Framework for Program Semantics and Semantic Abstraction

Keywords: semantics, abstract interpretation, oplax functors, monads

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.

Introduction

In a categorical setting, programs semantics can often be characterized as functors. In this setup, programs are viewed as morphisms and morphism composition describes how programs can be composed. As an example, in the case of typed functional programs, one may let objects be types and morphisms be functions. More precisely, a morphism from object a to object b denotes a function of type a → b. Then, the semantics maps programs to morphisms between objects that interpret input and output elements into a well-chosen semantic domain. This construction is very general and accepts a wide range of semantic domains. This functorial presentation of semantics is prominent in the categorical semantics of type theories and algebraic theories. There, both type theories and semantic categories are treated as categories possessing a common structure, and the semantics itself is presented as a structure-preserving functor. A typical example is the categorical semantics of the simply typed lambda-calculus, commonly studied under the well-known Curry-Howard-Lambek correspondence [START_REF] Lambek | Introduction to Higher-Order Categorical Logic[END_REF]; the calculus modulo βη-equality is presented as a Cartesian closed category, and its semantics in a Cartesian closed category is presented as a functor preserving finite products and exponentials. Another example is the categorical presentation of algebraic theories as a particular kind of categories with finite products (called Lawvere theories [START_REF] Lawvere | Functorial Semantics of Algebraic Theories[END_REF][START_REF] Adámek | Algebraic Theories: A Categorical Introduction to General Algebra[END_REF]), and their models as finite-product preserving functors. These categorical and syntax-free presentations of the calculus and its semantics brought significant convenience and advances to the study of type theories and their semantics. Additionally, monads turned out to be the tool of choice in order to construct semantics for effectful programs [START_REF] Moggi | Notions of computation and monads[END_REF].

Abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] provides a framework to compare program semantics of varying levels of expressiveness, and to derive sound approximations of program semantics, based on a given abstraction relation. It has been used to describe relationships across program semantics [START_REF] Cousot | Constructive design of a hierarchy of semantics of a transition system by abstract interpretation[END_REF], program analysis [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF][START_REF] Distefano | Scaling static analyses at facebook[END_REF], program transformations [START_REF] Cousot | Systematic design of program transformation frameworks by abstract interpretation[END_REF], and more. However, it is usually formalized in order theory since this presentation suffices in many applications. Therefore, it is not immediately compatible with the aforementioned categorical presentation.

Although the notion of Galois connection, which is abundantly used in abstract interpretation works [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Cousot | Abstract interpretation frameworks[END_REF], is adjunctions between posets, few works have studied a more complete description of abstract interpretation frameworks in a categorical setup. Among the works that relied on categorical tools in order to describe some specific semantic abstraction concepts for specific purposes, we can cite, Steffen et al. [START_REF] Steffen | Compositional characterization of observable program properties[END_REF] who integrate both concrete and abstract semantics in a categorical settings in order to examine questions related to soundness and completeness, with respect to a given set of behaviors. Venet [START_REF] Venet | Abstract cofibered domains: Application to the alias analysis of untyped programs[END_REF] uses mathematical tools that stem from category theory in order to construct specific families of abstract domains. More precisely, he applies the Grothendieck construction to generalize constructions such as reduced product and cardinal power [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF]. More recently, Sergey et al. [START_REF] Sergey | Monadic abstract interpreters[END_REF] took advantage of the monadic structure of a semantics of lambda-calculus to derive a static control flow analysis for a small functional language as well as an implementation in Haskell.

In this work, we seek for more comprehensive foundations for classical abstract interpretation techniques into the categorical semantics settings. We start with an interpretation of programs as morphisms in a syntactic category and semantics as functors from programs to the category of posets. We formalize and generalize the notion of collecting semantics typically used in program analysis as a decomposition of such a functor. In this setup, we integrate the notion of abstraction using some form of natural transformations between these functors. More precisely, the approximation inherent in sound, incomplete abstractions are accounted for using lax natural transformations. We show that this construction also enables the abstract interpretation of a basic language.

To achieve these goals, we build upon a categorical interpretation of programs and their semantics. In our categorical formalism, the design of an abstract semantics with respect to a denotational semantics -: L → C proceeds as follows. First, we turn the denotational semantics into a functorial collecting semantics by composingwith a functor C : C → Pos (where Pos denotes the category of posets and monotone functions between them), which we call property functor. This functor plays the role of attaching a notion of property and a direct image operation to the category C. This step is crucial for the design of the analysis, as it fixes the concrete semantics the analysis is built upon. Then, an analysis using abstract domains over the collecting semantics C • -is expressed as an oplax functor A : L → Pos equipped with a lax natural transformation γ : A → C • -representing a concretization of interpretation:

L - * * A * * ⇓γ Pos C C 3 3 (1)
Here, the functor A being oplax means that it only satisfies weakened functor axioms. The lax natural transformations are also weakening of natural transformations, replacing the naturality axiom to an inequality. The use of oplax functors for modeling analysis was initiated by Steffen, Jay and Mendler [START_REF] Steffen | Compositional characterization of observable program properties[END_REF].

We adopt the same approach, and further bring some basic concepts that are not covered in [START_REF] Steffen | Compositional characterization of observable program properties[END_REF] into the oplax functor formalism.

The common approach relies on fixing such an abstraction relation (here described by γ) and seeking for a sound, possibly approximate A that can be implemented efficiently. A natural and important question is how such an (A, γ) pair can be constructed. This can be done by extending the collecting semantics with a family of Galois connections, which are abundantly used in abstract interpretation, or with a family of concretization functions when best abstraction cannot be ensured.

This story naturally extends to the monadic semantics of various effectful programming languages. Indeed, as discussed earlier, the semantics of such programs is often derived using Kleisli categories of monads. Assuming a base category C for values and a monad T for effects, effectful programs are interpreted in the Kleisli category C T , and the semantics takes the form of a functor F : L → C T . We then derive a collecting semantics by composing it with a functor C T → Pos, and its abstraction is given, following the lax natural transformation discussed previously. Therefore, another benefit of our approach is to simplify the design of static analyses for effectful programs, thanks to a better integration of program semantics and abstraction.

To summarize, upon the work by Steffen, Jay and Mendler [START_REF] Steffen | Compositional characterization of observable program properties[END_REF], we formalize abstract interpretation in a functorial semantics framework. The new ingredients from [START_REF] Steffen | Compositional characterization of observable program properties[END_REF] are the following:

(i) We show that interpretations (oplax functors) are closed under the induction operation by Galois connections (Theorem 4.2). This induction also comes with concretizations of interpretations, formulated as lax natural transformations. (ii) We give a categorical formulation of collecting semantics (Section 3), which is the starting point of the development of abstract interpretations. In our formulation, a collecting semantics is an extension of a standard denotational semantics with a property functor, which attaches forward predicate transformers to the model category of the denotational semantics. (iii) We present two examples of developments of abstract interpretations, one for a while language over generic computational effects (Section 3 and Section 4), and the other for the simply typed lambda calculus in Section 5. An additional result that follows from this approach is a strongest postcondition predicate transformer semantics for the while language over general monads and truth value complete lattices (Theorem 3.13). This semantics is a generalization of the strongest postcondition semantics introduced in [START_REF] Zhang | Quantitative strongest post: A calculus for reasoning about the flow of quantitative information[END_REF].

Interpretation as an Oplax Functor

In this section, we set up basic definitions that serve as foundations for our integrated framework in the next sections. At this point, our main goal is to formalize the construction of semantics from programs.

Programs

Before considering semantic interpretations, we need to fix syntactic definitions. In this paper, we make the choice to also integrate programs as categorical entities, so that we can define interpretations as functors. This presentation is natural since programs can be viewed as transformations from inputs to inputs, that can also be composed like morphisms in a category. To do that, we follow a classical idea that lets a category L stand for the syntactic definition of programs and their inputs/outputs; more precisely,

• objects describe elements consumed/produced by programs;

• programs stand for morphisms. As an example, in a functional setup, we may let objects be types (thus describing values) and morphisms be functions mapping values to values.

Definition 2.1 [Programs as morphisms]

In the following, we express a programming language by a category L. Its objects represent types/contexts of programs, and morphisms stand for programs. This approach has been often used to describe functional programs (see e.g. [START_REF] Lambek | Introduction to Higher-Order Categorical Logic[END_REF][START_REF] Crole | Categories for Types[END_REF]). However, it also applies to other families of programs, such as imperative languages, that may not seem, at first, ideally adapted to a categorical approach. We illustrate this in the following examples.

Example 2.2 [A small imperative programming language]

We fix a set of values V and a finite set of variables X. We define the category L w as follows. First, we let expressions be defined by the grammar e := v (where v ∈ V) | x (where x ∈ X) | e ⊕ e (where ⊕ ∈ {+, -, * , ≤, =, . . .}). Second, we let programs be defined by the grammar P := skip | P ; P | x := e | if e {P }else{P } | while e {P }. Intuitively, an expression e is a value, the reading of a variable, or a binary expression, and a program is either the skip program that does nothing, or a sequence, or an assignment, or a condition, or a loop. The sequence construction acts like a composition. To satisfy the properties of morphism composition, we need to equate skip; P and P ; skip with P (identity) and also to let sequential composition act as an associative operation (which boils down to not parenthesizing sequences). Therefore L w simply follows the typical single object category describing a monoid.

As the above example is rather contrived in the sense that it omits any form of scoping, we consider a second, more sophisticated version.

Example 2.3 [Imperative programs with scoped variables] In this example, we extend Example 2.2 with a notion of scope, based on explicit variable creation and destruction operations. We keep the definition of expressions unchanged and extend that of programs with two additional constructions addvar x which adds a new local variable x and stores a default value (that we assume to be 0) into it and delvar x which ends the scope of a local variable x. Note that conventional block-based scoping can be encoded using these two operations.

We revise the construction of L w in Example 2.2 and let objects be finite sets of variables. Intuitively, the object X denotes set of memories storing |X|-many values. To make this explicit, we stratify the set of programs by two sets of variables, that respectively denote the variables in their input and output states. More precisely, we specify the set L wv (X, X ′ ) of programs from X to X ′ . Then, well-formed programs are defined inductively as follows. For any set X, skip ∈ L wv (X, X). Given programs P ∈ L wv (X, X ′ ) and P ′ ∈ L wv (X ′ , X ′′ ) the sequence program P ; P ′ is in the set L wv (X, X ′′ ). Assignment x := e belongs to L wv (X, X) for any X such that x and all variables in e are elements of X. Given two programs P, P ′ ∈ L wv (X, X ′ ), the condition program if e {P }else{P ′ } is in L wv (X, X ′ ) when all variables in e are in X. Similarly, loop (while e {P X,X }) X,X is defined when all variables in e are elements of X (note that the body and the loop program are morphisms from X to itself). Finally, when x ̸ ∈ X, (addvar x) ∈ L wv (X, X ⊎ {x}) and (delvar x) ∈ L wv (X ⊎ {x}, X). We note that the sequence case acts as composition of two morphisms respectively from X to X ′ and from X ′ to X ′′ and that it produces a morphism from X to X ′′ . The resulting category is denoted by L wv .

Semantic Interpretation

Based on the category of programs setup in Section 2.1, we now turn to semantic interpretations. Intuitively, a semantic interpretation should map programs into mathematical objects that describe their behavior in a more abstract manner than just syntax. For instance, the interpretation of a program P may boil down to a function that maps program input states to corresponding output states. Such an interpretation is expected to meet some compositionality property. Therefore, functors appear as the right categorical tool to define semantic interpretations. Before we spell out any definition, we consider a couple of examples.

Example 2.4 [Denotational Semantics] In this first example, we consider the language of Example 2.2. Programs are naturally regarded as actions on memories, namely functions from variables to values. We thus first define M := [X → V] to be the set of memories. Since any memory state is a valid input/output for any program, the construction of Definition 2.1 requires a single object that stands for M. This action will be given as the semantics in the next Example. We observe that not all programs terminate, which entails that one input state may not correspond to exactly one output state. Therefore, following the classical approach to denotational semantics, we interpret the unique object of L into the set M ⊥ ⊥ := M ⊎ {⊥ ⊥} where ⊥ ⊥ stands for non-termination. Then, the interpretation of a program P is the ⊥ ⊥-strict function P from M ⊥ ⊥ into itself. We remark that M ⊥ ⊥ is often interpreted as a poset, where ∀m ∈ M, ⊥ ⊥ ⊑ m and that ⊥ ⊥-strict functions are monotone functions in that set. Such interpretations compose well in the sense that the interpretation of P 0 ; P 1 coincides with the composition of the interpretation of P 1 with that of P 0 . Therefore we may convert it into a functor -: L w → Pos. This is a denotational semantics of L w , interpreting programs as actions on states (including ⊥ ⊥). This type of semantics will be studied in Section 3.1.

This functorial semantics can be extended to the imperative language with variable scoping operators L wv in Example 2.3. In this language, by putting M X := [X → V], program should be viewed a strict continuous function from (M X ) ⊥ ⊥ into (M X ′ ) ⊥ ⊥ for two given finite sets of variables X, X ′ . Note that, in this settings, (addvar x) is well defined since it initializes the new variable x with default value 0, as specified in Example 2.3.

Example 2.5 [Collecting semantics] Another type of semantics is to interpret programs as actions on properties on states. There are various ways to represent them, and one way is by sets of states. Then the semantics of programs are expressed as functions from sets of states into sets of states. Such a semantics is usually called collecting semantics and is one of the fundamental semantics in abstract interpretation. Specifically, we interpret the unique object of L w with the poset (2 M , ⊆) and a program P with a ∪preserving function P c : (2 M , ⊆) → (2 M , ⊆). Typically, P c is defined by induction over the syntax of programs and is compositional in the same sense as P (Example 2.4). It thus determines a functor c : L w → Pos. It can also be derived rather systematically from P -see Section 3.3.

Example 2.6 [Interval analysis] While the semantics shown in Example 2.5 is suitable as a starting point to study static analyzers, it is not computable. Thus, we propose to consider a second interpretation, using abstract properties rather than sets of states [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. We consider here the interval abstraction of [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], assuming values are machine integers. In this setup a set of states is described either with ⊥ (which denotes the empty set) or with a function from variables into intervals with integer bounds (that could be the minimum or maximum representable machine integers). Therefore, an interpretation of a program P may be defined as an abstract semantics P that maps an abstract pre-condition into a sound abstract post-condition: given any abstract state m ♯ and any memory m that satisfies the constraints in m ♯ , all states in P ({m}) are described by P (m ♯ ).

Nevertheless, this construction may not be compositional in the strict sense of denotational semantics. Indeed, the analysis of a composite program may be (and often is) more precise than the composition of the analyses of the sub-programs, in the following sense: we say that an analysis P 0 is more precise than an analysis P 1 when P 0 computes properties that are logically stronger than those computed than P 1 . Indeed, let us consider P 0 be x := 4 * x -2 and P 1 be if x ≤ 0 {x = -x}else{skip}. Moreover, we let m ♯ map x to interval [0, 1]. Then, P 0 (x) = [-2, 2] and P 1 • P 0 (x) = [0, 2]. However, if we consider concrete executions starting with x ∈ [0, 1], only value 2 may be observed as an output, thus a more precise analysis P 0 ; P 1 that maps m ♯ to [x → [START_REF] Aguirre | Weakest preconditions in fibrations[END_REF][START_REF] Aguirre | Weakest preconditions in fibrations[END_REF]] is sound.

The first remark that follows from the last two examples is that Pos provides a natural setup for property-based semantics. Indeed, objects of Pos allow to account for collections of program inputs or outputs, ordered with inclusion, with the usual meaning that smaller elements account for fewer behaviors.

The second remark is that composition may not always be exact when considering static analyses. Indeed, while the concrete semantics of Example 2.4 is compositional, Example 2.6 shows that static analyses may not be. Though, common practice ensures that most analyses satisfy a lax form of compositionality: the analysis of the composition of two programs may be implemented so that it gives somewhat more precise results than that of the composition of the analyses but is not expected to produce worse results. We comment on the limitations of this view in Remark 2.8.

To formalize these remarks, we rely on the order-enrichment on the category Pos of posets and monotone functions. All monotone functions f, g : X → Y in Pos are ordered in a pointwise manner, making Pos an enriched category over Pos itself. Intuitively, the order f ≤ g means that "g is more abstract than f "/"g is coarser than f ". Based on this terminology, we define semantic interpretations: Definition 2.7 [Interpretations] A semantic interpretation (or, for short, interpretation) F consists of an object mapping F : Obj(L) → Obj(Pos) and a morphism mapping F X,Y : L(X, Y ) → Pos(F X, F Y ) such that the following inequalities hold:

F (id) ≤ id, F (f 1 • f 2 ) ≤ F f 1 • F f 2 .
We say that the interpretation is normal if F (id X ) = id X and functorial if it is normal and

F (f 1 • f 2 ) = F f 1 • F f 2 .
Such a weakened form of functor is known as oplax functors. The above definition makes sense when Pos is replaced with some other Pos-enriched category K. In fact, Steffen, Jay and Mendler considered this general definition of interpretation in [START_REF] Steffen | Compositional characterization of observable program properties[END_REF], and their intention is to pick a suitable K for each analysis task. On the other hand, in this paper we fix the codomain of interpretation to Pos.

The semantics studied in Example 2.4 defines a functorial interpretation. The analysis of Example 2.6 defines an interpretation that is normal but not functorial. This latter situation was also commented by Steffen, Jay and Mendler in [START_REF] Steffen | Compositional characterization of observable program properties[END_REF]: indeed, they also introduce an oplax interpretation and remark that strictness analysis is generally not functorial.

Remark 2.8 [Limitations] As stated above, not all semantics satisfy the property of Definition 2.7, and in particular, some static analyses fail to satisfy it. As an example, it is possible to set up a weaker form of interval analysis (Example 2.6) that gives up all precision when applied to programs with updates to more than k variables. If k = 1, P 0 is x = 0 and P 1 is y = 1, although these programs are trivial, P 0 ; P 1 drops all information on x, y whereas P 1 • P 0 is trivially analyzed in a precise manner, thus we do not have

P 0 • P 1 ≤ P 1 • P 0 .
Obviously, this definition is very contrived, and a conventional implementation of interval analysis achieves the oplaxness property stated in Definition 2.7.

We introduce a partial order between interpretations. This order F ≤ G means that F, G agree on the interpretation of objects in L, but F interprets programs with better precision than G.

Definition 2.9 [Partial Order between Interpretations] Given two interpretations

F, G : L → Pos, we write F ≤ G if F (a) = G(a) for any a ∈ L and F (f ) ≤ G(f ) for any f : a → b in L.
This order will be used to compare abstract interpretations derived by Galois connections and its over-approximations (Theorem 4.2,4.3,5.1).

Functorial Collecting Semantics

We have set-up a formulation of abstract semantics as oplax functors. Typically, the development of abstract semantics is initiated from a concrete semantics called collecting semantics. We therefore express collecting semantics in our categorical setting.

The spirit of the collecting semantics is to interpret the behavior of programs as actions on collections of inputs, rather than single inputs. Typically, such a collection is chosen to represent a property on inputs, hence below we use the word property to mean a collection of inputs, or a collection of elements in a set X in general. Properties on X are ordered by the inclusion, forming the poset (2 X , ⊆) (where 2 X denotes the set of subsets of X).

Let us consider a simple example of collecting semantics. We consider a set-theoretic denotational semantics of a deterministic and terminating programming language L. It is defined by a functor -: L → Set mapping a morphism P : a → b in L representing a program into a function P : a → b . Then, the collecting semantics associated to this denotational semantics is the monotone function P c : (2 a , ⊆) → (2 b , ⊆) defined by P c (U ) := { P (x) | x ∈ U }; the right hand side is the direct image of a property U ⊆ a by P . We then regard the collecting semantics as a functorc : L → Pos.

We categorically analyze this definition of collecting semantics as follows. We introduce the covariant powerset functor Q : Set → Pos defined by: Q

(X) := (2 X , ⊆) and Q(f )(U ) := {f (x) | x ∈ U }.
The role of this functor is to assign to each X ∈ Set the poset of properties on X, and to each morphism f in Set the direct image operation associated to f . Then we notice the equality a c = Q( a ) for each object a ∈ L and P c = Q( P ) for each morphism P in L, which amounts to the following functor equality:

-c = L - / / Set Q / / Pos .
This functorial presentation of the collecting semantics suggests us to generalize the middle category to an arbitrary category C instead of Set so that we can define the concept of collecting semantics for general categorical semantics of programming languages. However, we need to replace the covariant powerset functor Q : Set → Pos with something else because it is specific to Set. We therefore need to supply a functor C : C → Pos that plays the same role as Q; it assigns to each object X ∈ C a poset CX of properties on X, whose elements abstractly represent properties on X, and to each f : X → Y a monotone function Cf : CX → CY representing the direct image operation. Based on this observation, we derive the following definition of collecting semantics. Definition 3.1 A functorial collecting semantics of a language L (regarded as a category) consists of a category C and two functors:

L - / / C C / / Pos ,
whereis called a denotational semantics and C is called a property functor (for C). The composite C • -: L → Pos itself is also called the functorial collecting semantics (with respect to -). This definition of functorial collecting semantics reflects our view that concrete semantics for initiating abstract interpretation is synthesized from a denotational semantics -: L → C by composing a property functor C : C → Pos. However, in some situations one may directly construct a collecting semantics without denotational semantics -in this case we simply put C = Id.

Denotational Semantics

In this section, we focus on the first functor and look at several examples of denotational semantics.

Example 3.3 An extreme example of denotational semantics is the identity functor. This means that the semantics of types/contexts and programs are themselves.

A second non-trivial family of examples relates to monadic semantics. Good references to the definitions of monads and Kleisli categories can be found in [START_REF] Maclane | Categories for the Working Mathematician[END_REF] and [START_REF] Moggi | Notions of computation and monads[END_REF]. The Kleisli category of a monad T on C is denoted by C T . We let • denote the composition of morphisms in Kleisli categories. Among examples of monads on Set, we can cite 1) the maybe monad that joins an extra element to a given set, and is defined by M X = X ⊎ { * }, 2) the powerset monad which maps each set to its powerset and is defined by P X = 2 X , and 3) the monad of probability subdistributions defined by D s X = {µ : X → [0, 1] | µ is a countable subdist. on X}. Before we look at monadic semantics, we fix a class of monads that is required to enable a least fixpoint definition of the semantics of while commands. Definition 3.4 A while-monad on Set consists of a monad (T, η, (-) # ) on Set and an ω-cpo (⊑ X , ⊥ ⊥ X ) on each T X. The sup of an ω-chain {x i } i∈N in T X is denoted by x i . 4 We define ⊑ X,Y as the pointwise order on Set T (X, Y ) given by f ⊑ X,Y g ⇐⇒ ∀x ∈ X . f (x) ⊑ Y g(x), and ⊥ ⊥ X,Y as the least function λx . ⊥ ⊥ Y . The data of the while-monad should satisfy:

(i) the Kleisli composition • is monotone and ω-continuous in each argument with respect to ⊑ X,Y , and (ii) additionally, it is strict in the second argument:

f • ⊥ ⊥ X,Y = ⊥ ⊥ X,Z for any f ∈ Set T (Y, Z).
This is a simplification and specialization of the order-enriched monad in [START_REF] Goncharov | A relatively complete generic hoare logic for order-enriched effects[END_REF]. The order ⊑ is to compare the definedness of elements/functions in the sense of domain theory. We later see another order for truth values, and these two orders are independent in general. We do not require • to be strict in the first argument. This is because we may sometimes want to distinguish the divergence after some effect from pure divergence. Consider a program tick; diverge. Then its monadic semantics will be ⊥ ⊥ M,M • tick , which we may want to distinguish from the silent divergence ⊥ ⊥ M,M .

Examples of while-monads on Set include the powerset monad P with the set inclusion order, the maybe monad M with the flat order making ι 2 ( * ) the least element, and the countable subdistribution monad D s with the pointwise mass order.

We now give a generic set-theoretic monadic semantics of the while language in Example 2.2.

Example 3.5 [Monadic Semantics of While Language]

We give a semantics of the while language in Set T . Let (T, η, (-) # , ⊑, ⊥ ⊥) be a while-monad on Set. In this semantics, we allow assignment commands x := e to perform some computational effects. We therefore let the interpretation of the command x := e be the morphism x := e ∈ Set T (M, M). We also assume an interpretation of the boolean expression b as a function b ∈ Set(M, {ff, tt}) into the two-points set. Then, the interpretation of programs is given by

skip T := η M P ; P ′ T := P ′ T • P T x := e T := x := e if b {P 1 }else{P 2 } T := λρ . if b (ρ) = tt then P 1 T (ρ) else P 2 T (ρ)
while e {P } T := µΦ where Φ(f

) := λρ . if b (ρ) = tt then f • P T (ρ) else η Ω M (ρ)
Here µΦ is the least fixpoint of Φ, and η Ω M is a component of the unit natural transformation of the monad T . We regard this interpretation as a functor -T : L w → Set T . When T is the maybe monad M , -M interprets programs as partial functions, while when T is the powerset monad P , -P may be regarded as interpreting programs as binary relations.

Example 3.6 To interpret the while language L wv with variable addition and deletion (Example 2.3), we may adjust the semantics in the previous example as follows. First, we let -T map each object X ∈ L wv , which is a finite set of variables, to the set X T := M X of memories over X (Example 2.4). It is then almost straightforward to modify -T and let it map a program P ∈ L wv (X, X ′ ) to a morphism of type M X → M X ′ in Set T . We interpret two additional commands addvar and delvar by

(addvar x) X,X⊎{x} T (ρ) = η X ⊎{x} (ρ{x → 0}) (delvar x) X⊎{x},X T (ρ) = η X (ρ -x),
where 0 is the presupposed default value for new variables (Example 2.3) and ρ -x is the environment obtained by removing x from the domain of ρ. Overall, we obtain a revised functor -T : L wv → Set T .

Property Functor

We next see some property functors so that we can form functorial collecting semantics of denotational semantics in the previous section.

Example 3.7 An extreme example of a property functor is the identity functor on Pos. This assigns to each poset X the poset of properties consisting of "being less than or equal to x" for each x ∈ X.

Example 3.8 The category Rel of sets and binary relations between them is the host category for various relational semantics of programs. For instance, the relational semantics of the while language interprets a program as an endorelation on M. Recall that each binary relation

f ∈ Rel(X, Y ) determines a ∪- preserving function f S (U ) := {j | i ∈ U ∧ (i, j) ∈ f } : (2 X , ⊆) → (2 Y , ⊆).
We turn this into a functor I P : Rel → CLat ∨ , where CLat ∨ is the subcategory of Pos consisting of complete lattices and joinpreserving functions between them, by I P (X) := (2 X , ⊆) and I P (f ) := f S . Clearly we have the subcategory inclusion ι : CLat ∨ → Pos, so overall we obtain a property functor for Rel as the composite ι•I P : Rel → CLat ∨ → Pos.

Example 3.9 Recall that Rel is isomorphic to the Kleisli category Set P of the powerset monad P . Thus the property functor in the previous example may be seen as the composite ι • I P : Set P → CLat ∨ → Pos.

In this example, we generalize this diagram in two directions: one is to replace P with a Set-monad (T, η, (-) # ), and the other is to adopt complete-lattice valued predicates as properties. We then derive a property functor using the strongest postcondition predicate transformer for Kleisli categories studied in [START_REF] Aguirre | Weakest preconditions in fibrations[END_REF]. We first take a complete lattice (Ω, ≤) for truth values. We use the symbols ⊥, ⊤, ∨, ∧ to mean the least/greatest elements and joins/meets of Ω. We then regard a function ϕ : X → Ω as an Ω-valued property on X. Such properties form a complete lattice Ω X := (Set(X, Ω), ≤ X ), where ≤ X is the pointwise order. The lattice operations on Ω X is written by ∧ X , ∨ X , etc. We note that the mapping X → Ω X extends to a functor of type Set op → CLat (the category of complete lattices and complete lattice homomorphisms).

We next take a T -algebra (or Eilenberg-Moore T -algebra) o : T Ω → Ω (see [24, Section VI.2]), and assume that o is meet-preserving in the following sense: the function λϕ . o • T (ϕ) belongs to CLat ∧ (Ω X , Ω T (X) ), the homset of the category CLat ∧ of complete lattices and meet-preserving functions. Such a T -algebra induces the weakest precondition predicate transformer Corollary 4.6]. The mapping f → wp o (f ) extends to a functor of type Set op T → CLat ∧ , thanks to the Eilenberg-Moore axioms. We then take the left adjoint sp o (f ) ∈ CLat ∨ (Ω X , Ω Y ) of wp o (f ), which we call the strongest postcondition predicate transformer [2, Example 4.11]. We extend the mapping f → sp o (f ) to a functor I o : Set T → CLat ∨ given by I o (X) := Ω X and I o (f ) := sp o (f ). In this way we obtain a property functor

wp o (f ) ∈ CLat ∧ (Ω Y , Ω X ) for each f ∈ Set T (X, Y ). It is given by wp o (f ) := λϕ . o • T ϕ • f [2,
ι • I o : Set T → CLat ∨ → Pos.
We see a few examples of meet-preserving T -algebras where Ω = {⊥ ≤ ⊤}. Now Ω X is the poset of characteristic functions, and we identify it with the poset (2 X , ⊆) of subsets of X.

I o ) satisfies, for f ∈ Set M (X, Y ), sp o (f ) = λϕ . {y ∈ Y | ∃x ∈ X . x ∈ ϕ ∧ f (x) = η Y (y)}.
Example 3.10 Any category C with a functor U : C → Set has a property functor given by the composite Q • U : C → Set → Pos with the covariant powerset functor Q.

For example, let (T, η, (-) # ) be a monad on Set. Its Kleisli category Set T comes with the right adjoint functor K T : Set T → Set given by K T (X) := T (X) and K T (f ) := f # [24, Theorem VI.1]. We then compose this with the covariant powerset functor Q and obtain a property functor

Q • K T : Set T → Set → Pos.
By letting T be the powerset monad P , we obtain the property functor that assigns to a set X the set of hyperproperties over X in the sense of Clarkson and Schneider [START_REF] Clarkson | Hyperproperties[END_REF]. The object part of Q • K T sends a set X to the poset (2 2 X , ⊆) of hyperproperties on X.

Putting Together

We have seen several denotational semantics and property functors. By combining them we obtain functorial collecting semantics.

We consider a functorial collecting semantics of the while language L w with 1) the monadic denotational semantics -T : L w → Set T in Example 3.5, and 2) the property functor ι • I o : Set T → Pos given by the strongest postcondition predicate transformer sp o in Example 3.9. The functorial collecting semantics interprets a program P as P c := ι • I o ( P T ) = sp o ( P T ).

We address the question of whether this collecting semantics can be given inductively. Let (T, η, (-) # , ⊑, ⊥ ⊥) be the while-monad on Set used in the monadic denotational semantics, (Ω, ≤) be the complete lattice, and o : T Ω → Ω be the meet-preserving T -algebra used in the property functor. We remark that these two orders represent two independent notions: ⊑ represents the definedness order of computations in the sense of domain theory, while ≤ represents the strength of truth values in the sense of algebraic logic. As noted in [START_REF] Cousot | Abstract interpretation frameworks[END_REF], we emphasize these two orders may be different in general. We also use different symbols for these two orders: joins for a definedness order is denoted by ⊔.

The following theorem states that the collecting semantics of while-free programs can be inductively given.

Theorem 3.11

The functorial collecting semanticsc satisfies:

skip c = id Ω M P ; P ′ c = P ′ c • P c x := e c = sp o ( x := e ) if b {P 1 }else{P 2 } c = λϕ . P 1 c (ϕ ∧ M [b = tt]) ∨ M P 2 c (ϕ ∧ M [b = ff]).
Here,

[b = v] : M → {⊥ M , ⊤ M } ⊆ Ω M is the function defined by [b = v](ρ) = ⊤ M if and only if b (ρ) = v.
The next question is whether while b {P } c ∈ CLat ∨ (Ω M , Ω M ) can be computed by the least fixpoint of some functional, say Ψ, definable by P and b. Since while b {P } T is the least fixpoint of a functional Φ on Set T (M, M) (see Example 3.5), it suffices to show that 1)

sp o : Set T (M, M) → CLat ∨ (Ω M , Ω M )
is ω-continuous and strict, and 2) Ψ • sp o = sp o • Φ. Regarding 1, it is equivalent to the continuity of o : T Ω → Ω in the following sense. It relates the ω-lub in the definedness order and the ω-lub in the truth value order. Proposition 3.12 The following hold:

(i) sp o ( f i ) = sp o (f i ) holds for any X, Y ∈ Set T and ω-chain f i in hom-ω-cpo (Set T (X, Y ), ⊑ X,Y ) if and only if o( c i ) = (o(c i )) holds for any ω-chain c i in the ω-CPO (T Ω, ⊑ Ω ). (ii) sp o (⊥ ⊥ X,Y ) = λϕ . ⊥ Y if and only if o(⊥ ⊥ Ω ) = ⊤.
Proof We here prove (i); (ii) can be proved similarly. We actually prove that the following are equivalent.

(a) sp o ( f i ) = sp o (f i ) for any X, Y ∈ Set T and ω-chain f i in hom-ω-CPO (Set T (X, Y ), ⊑ X,Y ). (b) wp o ( f i ) = wp o (f i ) for any X, Y ∈ Set T and ω-chain f i in hom-ω-CPO (Set T (X, Y ), ⊑ X,Y ). (c) o ( c i ) = (o(c i )) for any ω-chain c i in the ω-CPO (T Ω, ⊑ Ω ). (a) ⇐⇒ (b) Let f i be an ω-chain in (Set T (X, Y ), ⊑ X,Y ). Then from sp o (f i ) ⊣ wp o (f i ), we obtain: sp o f i = sp o (f i ) ⇐⇒ ∀ϕ, ψ . sp o f i (ϕ) ≤ Y ψ ⇐⇒ sp o (f i )(ϕ) ≤ Y ψ ⇐⇒ ∀ϕ, ψ . ϕ ≤ X wp o f i (ψ) ⇐⇒ ϕ ≤ X wp o (f i )(ψ) ⇐⇒ wp o f i = wp o (f i ). (b) =⇒ (c) Let c i be an ω-chain in (T Ω, ⊑ Ω ). Notice the isomorphism (T Ω, ⊑ Ω ) ∼ = (Set T (1, Ω), ⊑ 1,Ω ). We thus identify c i as an ω-chain in (Set T (1, Ω), ⊑ 1,Ω ). Then o • c i = wp o c i (id Ω ) = wp o (c i )(id Ω ) = o • c i .
(c) =⇒ (b) Let f i be an ω-chain in (Set T (X, Y ), ⊑ X,Y ). Then for any ϕ : Y → Ω and x ∈ X, we have

wp o f i (ϕ)(x) = o • T ϕ • f i (x) = o T ϕ f i (x) = o T ϕ(f i (x)) = o(T ϕ(f i (x))) = (wp o (f i )(ϕ)(x)) = wp o (f i ) (ϕ)(x).
Notice that T ϕ is continuous as T is a while monad. Therefore

wp o ( f i ) = wp o (f i ). 2
We thus say that o makes sp o ω-continuous and strict if it is a strict ω-continuous function of type (T Ω, ⊑ Ω ) op → (Ω, ≤).

(f ) = λϕ . (f • P c (ϕ ∧ M [b = tt])) ∨ Ω M (ϕ ∧ M [b = ff]).
Proof It sufficies to show sp o (µΦ) = µΨ. It is easy to verify that Ψ is a join-preserving endofunction on the pointwise-order complete lattice

CLat ∨ (Ω M , Ω M ). To show that (-) ∧ M [b = v]
: P [0, ∞] → [0, ∞]
is a meet-preserving T -algebra making sp o ω-continuous and strict. The functorial collecting semantics c coincides with the quantitative strongest postcondition in [START_REF] Zhang | Quantitative strongest post: A calculus for reasoning about the flow of quantitative information[END_REF]. By taking the opposite complete lattice ([0, ∞], ≥) for Ω and replacing inf with sup, the functorial collecting semanticsc coincides with the quantitative strongest liberal postcondition in [START_REF] Zhang | Quantitative strongest post: A calculus for reasoning about the flow of quantitative information[END_REF]. (iii) For the maybe while-monad M and Ω = {⊥ ≤ ⊤}, the meet-preserving T -algebra o in Example 3.9 makes sp o ω-continuous and strict.

Example 3.14 We consider a functorial collecting semantics of the while language L w with the monadic denotational semantics -T : L w → Set T in Example 3.5 and the property functor

Q • K T : Set T → Pos in Example 3.10. The interpretation Q•K T ( P T ) : 2 T M → 2 T M of a program P by this functorial collecting semantics satisfies Q • K T ( P T )(U ) = { P # T (c) | c ∈ U }, for any U ∈ 2 T M
, where (-) # is the Kleisli lifting of the monad T . When T is the powerset monad P , this functorial collecting semantics appears in Asaf et al.'s study on hypercollecting semantics [3, Section 4]. The definition of their hypercollecting semantics is partially inductive5 , and is an over-approximation of the above functorial collecting semantics; see the proof of Theorem 1 of their paper.

Semantic Abstraction

After discussing the role of collecting semantics in detail in Section 3, we now consider semantic abstraction and derivation of abstract semantics from a reference (e.g., collecting) semantics.

Abstraction Relations Between Domains and Interpretations

So far, we have studied the definition of program semantics independently from one another and have not considered comparing them quite yet. Abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] is specifically motivated with semantic comparison so as to tie properties that may be proved with one to statements involving another. Therefore, we consider the comparison of program semantics here.

Several forms of abstraction relations have been proposed, including Galois connections [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], concretization functions without assuming the existence of a best abstraction [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF], abstraction functions without assuming the existence of a concretization, or binary relations [START_REF] Cousot | Abstract interpretation frameworks[END_REF][START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF] A concretization of domains from A to C is a family {γ a : A(a) → C(a)} a∈L of monotone functions. We say that it is a concretization of interpretation from

A to C if it satisfies C(f ) • γ a ≤ γ b • A(f ) for any f ∈ L(a, b).
Dually, an abstraction of domains from C to A is a family {α a : C(a) → A(a)} a∈L of monotone functions. We say that it is an abstraction of interpretation from

C to A if it satisfies α b • C(f ) ≤ A(f ) • α a for any f ∈ L(a, b).
A concretization (resp., abstraction) of interpretations is called complete if the above inequality is an equality.

Remark that this definition sets up two notions of concretization (and the same for abstractions): the notion of concretization of domains ties only semantic domains, just like the concretizations in [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] do whereas concretization of interpretation tie not only domains (via a concretization of domains) but also interpretations, thus providing an interpretation soundness statement as typically sought to design a static analysis.

In categorical terminology, a concretization of interpretation is exactly a lax natural transformation from A to C, and an abstraction of interpretation is exactly an oplax natural transformation from C to A. 6Both concretizations and abstractions of interpretation express that one interpretation is more abstract than the other. Moreover, as in [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], we remark that the same abstraction relation may be described simultaneously both by concretization of domains and by an abstraction of domains; this strong correspondence between the two then defines a Galois connection.

We now explain how we develop a sound abstract interpretation of a functorial collecting semantics ( -, C) in our categorical framework. The ultimate goal is to construct an interpretation A together with a concretization of interpretation, as shown in the diagram [START_REF] Adámek | Algebraic Theories: A Categorical Introduction to General Algebra[END_REF]. The development process is broken into the following steps: The delicate part of this process is to find a right combination of A(a), γ a and A(P ) to achieve the soundness, as well as the expressiveness of abstract properties and the effectiveness of the semantics (when implementing it on a computer). In many cases, it is possible to simultaneously carry out the third and fourth steps, and to derive A from the interpretation C • -and the abstraction relation, so as to achieve a sound A.

In the rest of the section we see examples of concretization of interpretation. A bigger example of the development of abstraction is given for the denotational semantics of the lambda calculus (Section 5).

The Case of Galois Connections

As discussed earlier, Galois connections are one of the fundamental constructions that are used in abstract interpretation to describe abstraction relations. In presence of such a strong connection, the semantic induction technique of an interpretation that was mentioned in the previous subsection can be made even more systematic. We now study it in our categorical framework. (i) C G : L → Pos is a (resp. normal) interpretation, which we call the interpretation induced by G.

(ii) γ is a concretization of interpretation from C G to C. Moreover, for any interpretation

A ′ : L → Pos such that A ′ (a) = A(a), if γ is a concretization of interpretation from A ′ to C, then C G ≤ A ′ .
(iii) α is an abstraction of interpretation from C to C G . Moreover, for any interpretation

A ′ : L → Pos such that A ′ (a) = A(a), if α is an abstraction of interpretation from C to A ′ , then C G ≤ A ′ . Proof (i) C G (id a ) ≤ id Ca is immediate by α a • γ a ≤ id Ca .
We show the other inequality:

C G (g • f ) = α c • Cg • Cf • γ a ≤ α c • Cg • γ b • α b • Cf • γ a = C G (g) • C G (f ). (ii) We show γ is a lax natural transformation from C G to C, that is, C(f )•γ a ≤ γ b •C G (f ). This is evident as C(f ) • γ a ≤ γ b • α b • C(f ) • γ a . Next, let A ′ : L → Pos be an interpretation such that A ′ (a) = A(a)
and assume that γ a is a concretization of interpretation from A ′ to Pos. This amounts to C(f

) • γ a ≤ γ b • A ′ (f ) for any f : a → b in L. Since α b is a left adjoint of γ b , this is equivalent to α b • C(f ) • γ a ≤ A ′ (f ), that is, C G (f ) ≤ A ′ (f ). (iii) can be proved similarly. 2
When considering a program f : a → b, the interpretation α b • Cf • γ a is often called best abstract transformer. The above theorem says that C G is the most precise interpretation making γ a concretization of interpretation from C G to C, as well as α an abstraction of interpretation from C to C G .

The induction of abstract semantics by Galois connections is a fundamental operation in abstract interpretation, and our categorical framework of abstract interpretation accommodates it by the above theorem. Employing oplax functors as interpretations (Definition 2.7) is crucial here, because ordinary functors are not closed under the induction operation by Galois connection.

An abstraction of an interpretation in a complete lattice defining a Galois connection.

The semantics induced by a family of Galois connections would not have an inductive characterization due to its oplaxness. The common practice is to derive the best abstract transformers (or approximate ones) for the basic constructs of a language, then extend them to the whole language by induction. We discuss this approach using the functorial collecting semantics of the while language in Section 3.3 using a meet-preserving Eilenberg-Moore T -algebra o : T Ω → Ω and a Galois connection G := α ⊣ γ : A → (Ω M , ≤) with a general complete lattice (A, ∧ A , ∨ A ); later we restrict A so that the abstract interpretation can be computed in a finite means. We apply this Galois connection to the functorial collecting semanticsc in Section 3.3, and induce an abstract interpretation -G c : L w → Pos, which is an oplax functor. It interprets a program P as a monotone function α • P c • γ : A → A, but it does not enjoy an inductive characterization, that is, P G c is not expressible by the interpretation of subprograms in P by -G c . We therefore inductively construct another interpretationthat uses the best abstract transformers at assignment commands:

skip := id A P ; P ′ := P ′ • P x := e := x := e G c (= α • sp o ( x := e ) • γ) if b {P 1 }else{P 2 } := λϕ . P 1 (ϕ ∧ A α([b = tt])) ∨ A P 2 (ϕ ∧ A α([b = ff])) while b {P } := µΘ where Θ(f ) := λϕ . (f • P (ϕ ∧ A α([b = tt]))) ∨ A (ϕ ∧ A α([b = ff]))
Recall that sp o ( x := e ) denotes the strongest postcondition predicate transformer for assignments (Example 3.9), and [b = v] denotes the predicate representing the condition tests (Theorem 3.11). In the interpretation of while, we use the complete lattice structure on the homset Pos(A, A) with the pointwise order.

Theorem 4.3 Suppose that o makes sp ω-continuous and strict (hence Theorem 3.13 holds). The interpretation -: L w → Pos is functorial and -G c ≤ -holds. Proof The functoriality ofis obvious by definition. We show α • P 0 c • γ ≤ P 0 by induction on the structure of P 0 . We omit subscript of ∧, ∨. The cases P 0 = skip, (P ; P ′ ), (x := e) are easy. The case

P 0 = if b {P 1 }else{P 2 } is shown as follows. if b {P 1 }else{P 2 } = λϕ. P 1 (ϕ ∧ α([b = tt])) ∨ P 2 (ϕ ∧ α([b = ff])) {IH} ≥ λϕ.α • P 1 c • γ(ϕ ∧ α([b = tt])) ∨ α • P 2 c • γ(ϕ ∧ α([b = ff])) {γ meet-pres.} = λϕ.α • P 1 c (γ(ϕ) ∧ γ(α([b = tt]))) ∨ α • P 2 c (γ(ϕ) ∧ γ(α([b = ff]))) {unit law and α join-pres.} ≥ λϕ.α( P 1 c (γ(ϕ) ∧ [b = tt]) ∨ P 2 c (γ(ϕ) ∧ [b = ff])) {definition} = α • if b {P 1 }else{P 2 } c • γ
To show the case P 0 = while b {P }, we compare Ψ defined in Theorem 3.13 and Θ used in the definition of while b {P } . We first show α

• Ψ(f ) • γ ≤ Θ(α • f • γ). α • Ψ(f ) • γ = λϕ.α(f ( P c (γ(ϕ) ∧ [b = tt])) ∨ (γ(ϕ) ∧ [b = ff])) {unit law and α join-pres.} ≤ λϕ.(α • f • P c (γ(ϕ) ∧ γ(α([b = tt])))) ∨ α(γ(ϕ) ∧ γ(α([b = ff]))) {γ meet-pres.} = λϕ.(α • f • P c • γ(ϕ ∧ α([b = tt]))) ∨ α(γ(ϕ ∧ α([b = ff]))) {unit and counit law} ≤ λϕ.(α • f • γ • α • P c • γ(ϕ ∧ α([b = tt]))) ∨ (ϕ ∧ α([b = ff])) {IH} ≤ λϕ.(α • f • γ • P (ϕ ∧ α([b = tt]))) ∨ (ϕ ∧ α([b = ff])) = Θ(α • f • γ).
Since α ⊣ γ, the operation α • (-) • γ : (Pos(A, A), ≤) → (Pos(Ω M , Ω M ), ≤) is strict and continuous. Therefore

while b {P } = Θ n (⊥) = Θ n (α • ⊥ • γ) ≥ (α • Ψ n (⊥) • γ) = α • Ψ n (⊥) • γ = α • while b {P } c • γ. 2
This result is generic with respect to monads, the interpretation of (effectful) assignment commands, truth values and Galois connections. This theorem gives a functorial over-approximation of the best abstract interpretation derived from Galois connections. We see a similar story with the simply typed lambda calculus in Section 5. In the following paragraphs, we discuss how Theorem 4.3 paves the way to a computable static analysis.

Evaluation of the abstraction of an interpretation with a finite height domain.

When the abstract domain is a complete lattice with the finite chain property (which asserts that any totally ordered subset of the lattice is finite), Theorem 4.3 provides an algorithm to compute the abstract semantics that it defines [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. Indeed, the complete lattice property and the finite chain property respectively ensure the definition and the termination of the computation of while b {P } . A classical analysis that falls into this case is the analysis with the lattice of constants [START_REF] Kildall | A unified approach to global program optimization[END_REF].

Evaluation of the abstraction of an interpretation using fixpoint over-approximation.

In practice, few abstract domains satisfy the properties that were required in the previous paragraph. First, the complete lattice property often fails to hold. Then, the existence of least upper bounds for any family of abstract elements can then not be guaranteed. Second, even when any family of abstract elements has a least upper bound, the ω-chain generated by while b {P } may not converge after finite iterations, hence its least upper bound may not be computable. As an example, this occurs in the case of the abstract domain of intervals [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]: as it is possible to find an infinite sequence of intervals I 0 ⊂ I 1 ⊂ . . . I n ⊂ I n+1 ⊂ . . ., the definition of while b {P } that was provided earlier does not terminate in general.

Such cases are typically addressed by specific fixpoint approximation abstract operators. The most common instance is widening [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] and consists of a binary operator ▽ that over-approximates concrete unions and ensures termination in the sense that any sequence of applications of widening stabilizes after finitely many iterates. We now detail how our framework accommodates such analyses. We use the same notations as in the previous definition of . and assume a program P , a condition b, and an abstract element ϕ. Then, we define W ϕ n := i=0...n A τ i (ϕ) where τ (x) := P (x ∧ A α([b = tt])). Interpolation operators such as widening produce an over-approximation of all the elements of this sequence in terms of ≤. As an example, in the case of widening, the analysis computes a sequence defined by V ϕ 0 := W ϕ 0 and V ϕ n+1 := V ϕ n ▽ τ (V ϕ n ). This sequence converges to an element that we note V ϕ . Then the analysis produces

while b {P } (ϕ) := V ϕ ∧ A α([b = ff]).

Category of abstractions of interpretations.

We end this section by introducing the category of abstractions of an interpretation. This can be viewed as a categorical understanding of the so-called lattice of abstractions. Fix an interpretation of a category L, that is, an oplax functor C : L → Pos. This interpretation would typically be a functorial collecting semantics as in Section 3. The category of abstractions of C is the category where an object is a concretization of interpretation {γ a : A(a) → C(a)} a∈L from an interpretation A to C, and a morphism from {γ a : A(a) → C(a)} a∈L to {γ ′ a : A ′ (a) → C(a)} a∈L is a concretization of interpretation {δ a : A(a) → A ′ (a)} a∈L such that for any object a of L, γ ′ a • δ a ≥ γ a , saying that γ ′ a • δ a is more abstract than γ a . We will denote it by Abs(C). In words, Abs(C) is the oplax slice category over C of the category of interpretations of L and concretizations between them. Some standard constructions in abstract interpretation can be lifted to categorical structures of Abs(C), provided that C enjoys certain properties. When C factorizes through the category of meet-semilattices and meet-preserving maps, the category Abs(C) has binary products. It is given by the Cartesian product abstract domain (see e.g. [START_REF] Cortesi | A survey on product operators in abstract interpretation[END_REF]). Concretely, given two concretizations {γ a : A(a) → C(a)} a∈L and {γ ′ a : A ′ (a) → C(a)} a∈L , their binary product is given by the interpretation A × A ′ and the concretization {δ a : A(a) × A ′ (a) → C(a)} a∈L where δ a (u, v) = γ a (u) ∧ γ ′ a (v). It remains to be seen what other categorical structures are available on Abs(C).

Abstracting Denotational Semantics of λ-Calculus

In this section, we develop another kind of example to demonstrate the modularity of our theory of abstractions. Examples discussed so far only consist of imperative languages with various semantics and interpretations. Here, we describe interpretations for the simply typed lambda calculus over a higher-order signature, as a larger case study to demonstrate that our theory also copes with functional languages. In this study, we adopt rather simple non-relational abstraction of domains, that is, the abstract domain for product types is the product of abstract domains for component types.

The Language Category: the Free Cartesian Closed Category

Given a set B, we define T yp(B) to be the set of types generated from B with the type constructors for the unit type 1, the binary product type × and the arrow type →. We specify the simply typed lambda calculus by a higher-order signature. It consists of a set B of base types, a set O of constants and a function typ : O → T yp(B) assigning a type to each constant. We do not consider equational axioms on constants. In the rest of Section 5, we let Π be a higher-order signature (B, O, typ).

We write λ(Π) for the free Cartesian closed category (CCC for short) generated from Π [START_REF] Crole | Categories for Types[END_REF]. An object of λ(Π) is a type in T yp(B), and a morphism from τ to τ ′ is a βη-equivalence class of a term-in-context x : τ ⊢ M : τ ′ in the simply typed lambda calculus over Π.

Functorial Collecting Semantics for the Lambda Calculus

We next give a functorial collecting semantics for λ(Π). We first recall the standard functorial semantics of the simply typed lambda calculus in a Cartesian closed category (CCC for short).

:= b 0 , 1 := 1 C , τ 1 × τ 2 := τ 1 × C τ 2 , τ 1 → τ 2 := τ 1 ⇒ C τ 2 .
The Π-structure induces the Cartesian closed functor7 -: λ(Π) → C [START_REF] Crole | Categories for Types[END_REF].

For our functorial collecting semantics, we employ the CCC Set and fix a Π-structure in Set, then take the induced Cartesian closed functoras a denotational semantics. For the property functor, we take the covariant powerset functor Q : Set → Pos from Section 3. To summarize, we take the following functorial collecting semantics: Q • -: λ(Π) → Set → Pos.

Abstracting Collecting Semantics by Galois Connections

Thanks to Theorem 4.2, to construct an abstract semantics of Q( -), it suffices to give a Galois connection of the form α τ ⊣ γ τ : A(τ ) → Q( τ ) for every type τ ∈ T yp(B). We do so by first assuming, for each base type b ∈ B, 1) a poset A 0 (b) of abstract base type properties, and 2) a Galois connection α b ⊣ γ b : A 0 (b) → Q( b ). For instance, when there is a base type nat ∈ B for natural numbers and it is interpreted as the set N of natural numbers, we may take the poset of intervals (including the empty one) over N for A 0 (nat), and take the Galois connection for interval abstraction for α nat ⊣ γ nat : A 0 (nat) → Q(N).

We then inductively extend the mapping A 0 : B → Pos to the one A : T yp(B) → Pos by the Cartesian closed structure of Pos:

A(b) := A 0 (b), A(1) := 1 Pos , A(τ 1 × τ 2 ) := A(τ 1 ) × Pos A(τ 2 ), A(τ 1 → τ 2 ) := A(τ 1 ) ⇒ Pos A(τ 2 ).
We next construct a type-indexed family of Galois connections. Below

α τ i ⊣ γ τ i : A(τ i ) → Q( τ i ) are Galois connections for i = 1, 2. (For α 1 ⊣ γ 1 : 1 Pos → Q( 1 )
we take the unique one.)

A(τ 1 × τ 2 ) Q( τ 1 ) × Pos Q( τ 2 ) ατ 1 ×ατ 2 o o ⊥ / / γτ 1 ×γτ 2 Q( τ 1 × τ 2 ) α × o o ⊥ / / γ × A(τ 1 → τ 2 ) Q( τ 1 ) ⇒ Pos Q( τ 2 ) ατ 2 •_•γτ 1 o o ⊥ / / γτ 2 •_•ατ 1 Q( τ 1 → τ 2 ) α ⇒ o o ⊥ / / γ ⇒
Here, Galois connections α × ⊣ γ × and α ⇒ ⊣ γ ⇒ are given by . The interpretation -G c is normal when the base type Galois connections are Galois insertions: indeed, it can be easily proved by induction on types that α τ • γ τ = id. However, it is not functorial.

To have an inductively defined semantics that over-approximates -G c , we derive a new semantics of the lambda calculus that interprets each constant c by x : 1 ⊢ c : typ(c) G c : 1 Pos → A(typ(c)). Formally, we form a Π-structure (A 0 , { x : 1 ⊢ c : typ(c) G c } c∈O ) in Pos and induce a Cartesian closed functor -: λ(Π) → Pos. This process is a lambda-calculus analogue of the derivation offrom -G c for the while language in Section 4.2; in this example, assignment commands are replaced with constants in Π. The following theorem is in parallel with Theorem 4.3.

Theorem 5.1 -is a Cartesian closed functor, and -G c ≤ -.

Related Works

In this paper, we study the construction of frameworks to describe semantic abstraction using categorical tools which are already used heavily to construct semantics of programming languages. Abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] was proposed as a very general framework to compare program semantics and has found applications in many areas of computer science such as semantics [START_REF] Cousot | Constructive design of a hierarchy of semantics of a transition system by abstract interpretation[END_REF], program analysis and verification [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF][START_REF] Distefano | Scaling static analyses at facebook[END_REF], program transformations [START_REF] Cousot | Systematic design of program transformation frameworks by abstract interpretation[END_REF][START_REF] Rival | Symbolic transfer function-based approaches to certified compilation[END_REF], or security [START_REF] Giacobazzi | Abstract non-interference: parameterizing non-interference by abstract interpretation[END_REF]. It is of very general scope as shown in [START_REF] Cousot | Abstract interpretation frameworks[END_REF], since it can be adapted to various program semantics, styles of abstraction relations (abstraction functions, concretization functions, Galois connections, or basic abstraction relations), abstract domains, and classes of approximation algorithms. Although it was remarked very early that it could also be formalized in category theory, most descriptions use set theory. Steffen et al [START_REF] Steffen | Compositional characterization of observable program properties[END_REF] define both concrete and abstract semantics in a categorical framework in which they express soundness. Before their work, Panangaden and Mishra give a categorical formulation of abstract interpretation based on the concept called quasi-functor [START_REF] Panangaden | A category theoretic formalism for abstract interpretation[END_REF]. We leave the comparision of quasi-functors with oplax functors for future work. Sergey et al. [START_REF] Sergey | Monadic abstract interpreters[END_REF][START_REF] Darais | Galois transformers and modular abstract interpreters: reusable metatheory for program analysis[END_REF] rely on monads to construct a control flow analysis of a small functional language, where various aspects of the program semantics and abstraction are described by monads. Our work uses categorical tools in a different way. First, we use a framework based on oplax functors and lax natural transformations in order to express and compare semantics. This is the right setting for embracing the induction of semantics by Galois connections (Theorem 4.2), which is foundational in abstract interpretation. Second, we build upon a functorial decomposition to generalize the notion of collecting semantics, to expose a property component and a semantic component. According to [START_REF] Cousot | Abstract interpretation frameworks[END_REF] as "the main utilization of the collecting semantics is to provide a sound and relatively complete proof method for the considered class of properties", however this presentation does not give a systematic way to construct one such semantics, thus one of our contributions is to provide a functorial interpretation for this notion. Another of our contributions is to bridge the gap between monadic tools to construct program semantics and their use in abstract interpretation.

This paper focuses on the forward property-based semantics. The other side of the story, namely the backward property-based semantics, has recently been categorically studied [START_REF] Hasuo | Generic weakest precondition semantics from monads enriched with order[END_REF][START_REF] Aguirre | Weakest preconditions in fibrations[END_REF][START_REF] Wolter | Indexed and fibered structures for partial and total correctness assertions[END_REF]. They point out that Dijkstra's weakest precondition predicate transformer (wppt for short), which is a typical backward property-based semantics, corresponds to functors of type L op → Pos (see wp o in Example 3.9). This fact suggests that we may dualize this paper's story to develop abstract interpretations for backward propertybased semantics. There, wppts expressed as functors would play the role of functorial collecting semantics.

Conclusion

We have introduced categorical structures that account for basic concepts and constructions in abstract interpretation. We have demonstrated that it can account for the abstraction of both imperative and functional programs in a unified manner. A future work is to explore various combinations of the data in the diagram [START_REF] Adámek | Algebraic Theories: A Categorical Introduction to General Algebra[END_REF]. For the language category L, it would be interesting to take programming languages other than the while language and the simply typed lambda calculus, such as linear lambda calculus [4], Moggi's monadic metalanguage [START_REF] Moggi | Notions of computation and monads[END_REF], and dependent type theories. For the property functor C, regular fibrations [20, Definition 4.2.1] are a rich source. The construction of (A, γ)-pairs is the central part of the development of abstract interpretation, and it remains to be seen if our categorical formalism provides new construction methods of (A, γ)-pairs.

Remark 3 . 2

 32 The readers who are familiar with fibrational category theory might notice that the property functor C : C → Pos bijectively corresponds to a posetal opfibration (a functor c : E → C from some category E such that c satisfies the opcartesian lifting property; see e.g. [20, Section 9.1]). Therefore C may be replaced by a posetal opfibration c : E → C. In this setting, the functorial collecting semantics interprets a morphism f : a → b in L as the pushforward f * : E a → E b between fibre posets.

  (i) For the powerset monad P , there is only one T -algebra o : P Ω → Ω preserving meets: o(U ) = ⊤ ⇐⇒ ⊥ ̸ ∈ U [2, Example 5.3]. The derived property functor is isomorphic to the one in Example 3.8. (ii) For the maybe monad M , there is only one T -algebra o : M Ω → Ω preserving meets: the one sending ι 2 (⊥ ⊥) to ⊤. The strongest postcondition predicate transformer (hence property functor

Theorem 3 . 13

 313 If o makes sp o ω-continuous and strict, the functorial collecting semanticsc satisfies while b {P } c = µΨ where Ψ

2

 2 preserves joins, we use the fact that [b = v] takes only values in {⊥ M , ⊤ M }. By calculation, we have Ψ • sp o = sp o • Φ. Since sp o is ω-continuous and strict, we obtain sp o (µΦ) = µΨ. We see some examples of meet-preserving T -algebra making sp o ω-continuous and strict. (i) For the powerset while-monad P on Set and Ω = {⊥ ≤ ⊤}, the meet-preserving T -algebra o in Example 3.9 makes sp o ω-continuous and strict. The functorial collecting semanticsc coincides with the standard one in the literature. (ii) For the powerset while-monad P on Set and Ω = ([0, ∞], ≤), the inf-operation inf

  . In categorical terms, a Galois connection α ⊣ γ : A → C is a pair of monotone functions α : C → A and γ : A → C between posets such that the equivalence α(a) ≤ c ⇐⇒ a ≤ γ(c) holds for any a ∈ A, c ∈ C. It is called a Galois insertion if α • γ = id. Definition 4.1 Let A, C : L → Pos be interpretations.

  (i) We give the object part of A; this corresponds to designing a domain of interpretation for each type/context a ∈ L. (ii) We give a concretization of domains {γ a : A(a) → C a }, relating the domain of interpretation of types/contexts and that of the collecting semantics. (iii) We give the morphism part of A; this corresponds to designing how each program P : a → b transfers abstract properties in A(a) to those in A(b). In our categorical framework this should respect the oplax functoriality in Definition 2.7. (iv) We check if the constructed interpretation A satisfies soundness in the following sense: for any program P : a → b in L and an abstract predicate ϕ ∈ A(a), we have C( P )(γ a (ϕ)) ≤ γ b (A(P )(ϕ)). This is equivalent to showing that γ being a concretization of interpretation from A to the functorial collecting semantics C • -.

Theorem 4 . 2

 42 Let C : L → Pos be an (resp. normal) interpretation, {A(a)} a∈L be a family of posets indexed by objects in L, and G := {α a ⊣ γ a : A(a) → C(a)} a∈L be a family of Galois connections (resp. insertions). We define mappings on L-objects and L-morphisms by C G (a) := A(a) and C G (f ) := α b • Cf • γ a (f : a → b).

  Let (C, 1 C , × C , ⇒ C ) be a CCC. A Π-structure in C consists of 1) an assignment -0 : B → C of a C-object to each base type, and 2) an assignment c 0 : 1 C → typ(c) of a C-morphism to each constant c ∈ O; here -: T yp(B) → C is the inductive extension of -0 : B → C by b

α

  × (U ) := (Q(π 1 )(U ), Q(π 2 )(U )) γ × (U, V ) := U × V α ⇒ (F ) := λU . f ∈F Qf (U ) γ ⇒ (g) := {f | ∀U ⊆ τ 1 . Qf (U ) ⊆ g(U )}.This establishes a type-indexed family of Galois connectionsG := {α τ ⊣ γ τ : A(τ ) → Q( τ )} τ ∈T yp(B) .Using the notations of Theorem 4.2, we obtain an abstract interpretation, that is, an oplax functor -G c : λ(Π) → Pos given by τ G c := A(τ ) and x :τ ⊢ P : σ G c := α σ • Q( x : τ ⊢ P : σ ) • γ τ . ByTheorem 4.2, it comes with a concretization of interpretation γ from -G c to Q • -, as well as an abstraction of interpretation α from Q • -to -G c

In this article, the least element of a poset is denoted by ⊥ ⊥ X if it corresponds to non-termination, while it is denoted by ⊥ if it corresponds to the falsity (Example 3.9).

The hypercollecting semantics in[START_REF] Assaf | Hypercollecting semantics and its application to static analysis of information flow[END_REF] Section 4] is not inductive at the interpretation of conditional expressions.

The original definition of (op)lax natural transformation consists of families of 1-cells and 2-cells. In the current context, however, there is at most one choice of 2-cells for (op)lax natural transformations between oplax functors into Pos. Therefore we here treat the concept of (op)lax natural transformation as a property on families of 1-cells.

Here it means a functor strictly preserving finite products and exponentials.

Acknowledgement

The first and third authors were supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST. The third author was also supported by JST, CREST Grant Number JPMJCR22M1. The second author was supported by the French ANR VeriAMOS project. The authors are grateful to James Haydon for his critical reading of the manuscript, and implementation proposals and suggestions of new directions during discussions. The authors are also grateful to Ichiro Hasuo for insightful comments and suggestions.


G Beaugrand
email: gregory.beaugrand@univ-lille.fr^richard.kirby@planktonpundit.org

R Faillettaz

R R Kirby

The recently suggested absence of an internal multidecadal oscillation in the North Atlantic has consequences for anticipating the future of marine ecosystems Opinion Piece Running head: future of North Atlantic marine ecosystems

Abstract

The North Atlantic marine ecosystem was expected to adjust imminently to a negative phase of the Atlantic Multidecadal Oscillation (AMO). Recent results suggest however, that the AMO is not a regular internal source of variability but has been driven by both volcanism and sulphate aerosol emissions that have influenced temperature negatively and a period of greenhouse gas accumulation causing temperatures to be higher than normal. The demise of the AMO removes the expected and imminent cyclical change from the current warm phase to a negative cool phase in the North Atlantic. Here, we discuss the implications of this new finding for the near-future of North Atlantic marine ecosystems in a context of rapid climate warming.

Main text

For centuries, humans have tried to recognise patterns in natural systems and determine their controlling mechanisms, not least in marine ecosystems [START_REF] Cheung | Projecting global marine biodiversity impacts under climate change scenarios[END_REF][START_REF] Rombouts | Potential changes in benthic macrofaunal distributions from the English Channel simulated under climate change scenarios[END_REF][START_REF] Raybaud | Decline in Kelp in West Europe and Climate[END_REF][START_REF] Schickele | Modelling European small pelagic fish distribution: Methodological insights[END_REF] where it helps to enhance predictability and especially, with regard to commercial fisheries, e.g. the European herring Bohuslän periods [START_REF] Alheit | Long-term forcing of European herring and sardine populations[END_REF] or the multidecadal fluctuations of sardines and anchovies in different oceans [START_REF] Chavez | From anchovies to sardines and back: multidecadal change in the Pacific Ocean[END_REF].

Until now, an inherent large-scale oceanic phenomenon called the AMO was thought to explain periodic changes observed in key physical and biological systems in the North Atlantic, with a periodicity of ~60 years [START_REF] Mann | Global interdecadal and century-scale climate oscillations during the past five centuries[END_REF][START_REF] Kerr | A North Atlantic climate pacemaker for the centuries[END_REF][START_REF] Enfield | The Atlantic Multidecadal Oscillation and its relationship to rainfall and river flows in the continental U[END_REF][START_REF] Edwards | Marine ecosystem response to the Atlantic Multidecadal Oscillation[END_REF]. Climate change biologists have documented significant correlations between the cyclical nature of the AMO index and North Atlantic biological systems to try to understand the ecosystem and how it might evolve, even postulating that the next negative AMO phase could alleviate or momentarily reverse the current warming trend [START_REF] Frajka-Williams | Emerging negative Atlantic Multidecadal Oscillation index in spite of warm subtropics[END_REF]. For example, in the English Channel, the Russell Cycle that describes an alternation of periods dominated by cold-water (i.e. herring, Clupea harengus, and the chaetognath Sagitta elegans) and warm-water species (i.e. pilchard, Sardina pilchardus, and the chaetognath S. setosa) has been related to the AMO [START_REF] Russell | Changes in biological conditions in the English Channel off Plymouth during the last half century[END_REF][START_REF] Edwards | Marine ecosystem response to the Atlantic Multidecadal Oscillation[END_REF]. Sardine (and S. setosa) dominates during positive phases and herring (and S. elegans) during negative phases of the AMO. In the North Atlantic, bluefin tuna has been shown to exhibit a long-term, quasi-cyclical, north to south, seesaw-like population movement and changes in abundance driven by climatic variation that correlates with the AMO: when the AMO phase is positive or negative, bluefin tuna are distributed further north or further south, respectively [START_REF] Faillettaz | Atlantic Multidecadal Oscillations drive the basin-scale distribution of Atlantic bluefin tuna[END_REF].

While previous studies attributed the AMO to internal climatic processes, a recent study by [START_REF] Mann | Multidecadal climate oscillations during the past millennium driven by volcanic forcing[END_REF] showed that positive (warm) and negative (cool) phases of the AMO have been due to external forces, such as volcanic activity, sulphate aerosol cooling, and greenhouse-gas-induced warming. The last negative AMO phase was mostly caused by the negative forcing exerted by the increasing sulphate aerosol emission, and the current warm phase by the predominant effect of increasing greenhouse gases at a time of diminishing sulphate aerosol emission [START_REF] Mann | Multidecadal climate oscillations during the past millennium driven by volcanic forcing[END_REF]. The AMO-like pattern has therefore, never been governed fully by internal hydro-climatic variability and this new knowledge is of profound importance for our understanding of the regional climate and marine ecosystems.

To illustrate the strong influence of multidecadal changes in temperature on extratropical North Atlantic marine resources, we have updated a previous Principal Component Analysis (PCA) on Sea Surface Temperature (SST) [START_REF] Beaugrand | Reorganisation of North Atlantic marine copepod biodiversity and climate[END_REF] for the region 20°N-65°N and 100°W-20°E using SST data from the COBE interpolated 1°x1°dataset from 1891 to 2020 [START_REF] Ishii | Objective Analyses of Sea-Surface Temperature and Marine Meteorological Variables for the 20th Century using ICOADS and the Kobe Collection[END_REF]. Expectedly, this analysis shows two cold and two warm phases superimposed on a long-term positive SST trend for most areas of the North Atlantic except for the central and south-western regions (Figure 1a-b). Detrending the first principal component (PC1, 49.8% of the total variance) gives a pattern similar to the classic AMO index, albeit the AMO index is usually based on a larger area than the one we considered here [START_REF] Enfield | The Atlantic Multidecadal Oscillation and its relationship to rainfall and river flows in the continental U[END_REF][START_REF] Mann | Multidecadal climate oscillations during the past millennium driven by volcanic forcing[END_REF][START_REF] Murphy | Investigating the Roles of External Forcing and Ocean Circulation on the Atlantic Multidecadal SST Variability in a Large Ensemble Climate Model Hierarchy[END_REF]).

When we include long-term changes in an index of phytoplankton concentration in the North Sea (Reid et al. 1998) Spring-Spawning herring at the beginning of the 1960s) [START_REF] Lorentzen | The collapse of the Norwegian herring fisheries in the late 1950s and 60s crisis, adaptation, and recovery[END_REF][START_REF] Fromentin | Oceanographic changes and exploitation drive the spatio-temporal dynamics of Atlantic bluefin tuna (Thunnus thynnus)[END_REF][START_REF] Cort | The Fall of the Tuna Traps and the Collapse of the Atlantic Bluefin Tuna, Thunnus thynnus (L.), Fisheries of Northern Europe from the 1960s[END_REF], and because the nature of the phenomenon was cyclical, a reversal of the AMO was soon expected to occur (Frajka-Williams et al. 2017) with its putative consequences for the marine ecosystem and its exploited resources. Results from Mann et al. [START_REF] Mann | Multidecadal climate oscillations during the past millennium driven by volcanic forcing[END_REF] imply that an imminent reversal to a cool period is now unlikely and so we should not expect an imminent shift in the North Atlantic marine ecosystem and provisioning services.

While overfishing has been an important component of the collapse of North-east

Atlantic tuna or Norwegian Spring-Spawning herring and so management actions may have played an important role in the rebuilding of the different stocks [START_REF] Lorentzen | The collapse of the Norwegian herring fisheries in the late 1950s and 60s crisis, adaptation, and recovery[END_REF], Toresen & Østvedt 2008[START_REF] Fromentin | Oceanographic changes and exploitation drive the spatio-temporal dynamics of Atlantic bluefin tuna (Thunnus thynnus)[END_REF][START_REF] Cort | The Fall of the Tuna Traps and the Collapse of the Atlantic Bluefin Tuna, Thunnus thynnus (L.), Fisheries of Northern Europe from the 1960s[END_REF], it often interplayed with changing environmental conditions [START_REF] Beaugrand | Plankton effect on cod recruitment in the North Sea[END_REF][START_REF] Faillettaz | Atlantic Multidecadal Oscillations drive the basin-scale distribution of Atlantic bluefin tuna[END_REF]. A shift in the state of the AMO from positive to negative could have caused another rapid retreat of bluefin tuna southwards as was observed notoriously at the beginning of the 1960s together with another biological shift in the Russel cycle bringing a new period of high productivity to the English Channel. So, while the demise of the AMO does not negate the climatic modulation of North Atlantic biology, it does have significant implications for our understanding of the drivers of change and how ecosystems and provisioning services may change in the future. Consequently, the recent northward shift of bluefin tuna is likely due to greenhouse gas-induced global warming and the well-known Russell Cycle is not necessarily a cycle anymore [START_REF] Mcmanus | Is the Russell Cycle a true cycle? Multidecadal zooplankton and climate trends in the western English Channel[END_REF], and there is now, no a priori reason that the North Atlantic region will return soon to the negative AMO phase that has been anticipated [START_REF] Frajka-Williams | Emerging negative Atlantic Multidecadal Oscillation index in spite of warm subtropics[END_REF][START_REF] Mann | Multidecadal climate oscillations during the past millennium driven by volcanic forcing[END_REF].

The latest IPCC report includes the influence of anthropogenic and volcanic activity The AMV includes the influence of the North Atlantic Oscillation (NAO) that is a natural source of atmospheric variability [START_REF] Hurrell | Decadal trends in the North Atlantic Oscillation: regional temperatures and precipitations[END_REF] and which interacts with the AMOC, although the mechanisms involved and their relative strengths are still unclear (Masson-Delmotte et al. In press). As a result, we also think it is better to replace the AMO by AMV in climate change biology and to therefore recognise that the oscillatory behaviour of Atlantic multidecadal variability observed during the last two centuries may not continue. Consequently, we cannot predict a return to a lower temperature regime with all that entails, i.e. rapid shift in the marine ecosystems with its consequences for exploited resources.

A fundamental question in ecology is, why is what where? [START_REF] Berry | Ecology: where genes and geography meet[END_REF]. Sea surface temperature is a key determinant of the abundance and distribution of marine pelagic species. Of course, knowing that an anticipated and imminent climate reversal in the North Atlantic will not now occur due to the AMO neither invalidates previous environment-driven, cyclical variation seen in species such as bluefin tuna [START_REF] Faillettaz | Atlantic Multidecadal Oscillations drive the basin-scale distribution of Atlantic bluefin tuna[END_REF] nor helps predict the future direction of marine ecosystems, but it does help us focus on those drivers of change that are important. While climatic surprises remain possible (e.g. the slow-down of the Atlantic Meridional Overturning Circulation and its negative influence on North-east Atlantic climate [START_REF] Boers | Observation-based early-warning signals for a collapse of the Atlantic Meridional Overturning Circulation[END_REF][START_REF] Caesar | Current Atlantic Meridional Overturning Circulation weakest in last millennium[END_REF])), if the results of Mann et al. [START_REF] Mann | Absence of internal multidecadal and interdecadal oscillations in climate model simulations[END_REF][START_REF] Mann | Multidecadal climate oscillations during the past millennium driven by volcanic forcing[END_REF] are confirmed, and recent works suggest, at least in part, that they are (Murphy et al. 2021, Masson-Delmotte et al. In press), they have now eliminated the AMO as one variable thereby simplifying a complex world where ecosystem shifts are moving towards a warmer dynamic regime in response to anthropogenic climate change [START_REF] Beaugrand | Reorganisation of North Atlantic marine copepod biodiversity and climate[END_REF].

  , Norwegian spring spawning herring (Toresen & Østvedt 2008) and bluefin tuna distribution in the north-east Atlantic (Faillettaz et al. 2019), we see that changes across three trophic levels in different regions correlate with long-term changes in North Atlantic SST, exhibiting a clear oscillation (Fig. 1ce). High North Sea phytoplankton concentration, high Norwegian Sea herring and north-east Atlantic tuna abundance are observed during a positive (warm) phase of the AMO and inversely. Because the AMO is considered to cause these changes in addition to other factors (e.g. overfishing of North-east Atlantic tuna and Norwegian

on

  Atlantic multidecadal variability (Masson-Delmotte et al. In press). Climatologists now also use the term Atlantic Multidecadal Variability (AMV) instead of the AMO because multidecadal variability in the Atlantic may result from broad, low-frequency signals (Lapointe et al. 2020, Murphy et al. 2021, Masson-Delmotte et al. In press).

Figure legend Figure 1 .

 legend1 Figure legend