Vincent Danos

Russ Harmer

Ricardo Honorato-Zimmer

Thermodynamic graph-rewriting

We develop a new 'thermodynamic' approach to stochastic graph-rewriting. The ingredients are a finite set of reversible graphrewriting rules G (called generating rules), a finite set of connected graphs P (called energy patterns), and an energy cost function ǫ : P → R. The idea is that G defines the qualitative dynamics by showing which transformations are possible, while P and ǫ specify the long-term probability π of any graph reachable under G. Given G, P, we construct a finite set of rules GP which (i) has the same qualitative transition system as G, and (ii) when equipped with suitable rates, defines a continuous-time Markov chain of which π is the unique fixed point. The construction relies on the use of site graphs and a technique of 'growth policy' for quantitative rule refinement which is of independent interest. The 'division of labour' between the qualitative and the long-term quantitative aspects of the dynamics leads to intuitive and concise descriptions for realistic models (see the example in §4). It also guarantees thermodynamical consistency (aka detailed balance), otherwise known to be undecidable, which is important for some applications. Finally, it leads to parsimonious parameterizations of models, again an important point in some applications.

Introduction

Along with Petri nets, communicating finite state machines, and process algebras, models of concurrent systems based on graphs and graph transformations (GTS) have long been investigated as means to describe, verify and synthesize distributed systems [START_REF] Ehrig | Handbook of graph grammars and computing by graph transformation: Applications, Languages and Tools[END_REF]. Beyond their visual aspect, which is useful in modelling situations, there is a lot to like about GTSs: there are category-theoretic frameworks to express them and encapsulate their syntax; and the existence of a strong meta-theory [START_REF] Lack | Adhesive categories[END_REF] is a reassurance that methodologies developed in specific cases can be 'ported' to other variants.

Graph-rewriting rules are convenient for writing compact models and modifying them [START_REF] Danos | Agile modelling of cellular signalling[END_REF], and lend themselves naturally to probabilistic extensions [START_REF] Heckel | Dpo transformation with open maps[END_REF][START_REF] Krivine | Stochastic bigraphs[END_REF]. However, for all their flexibility, even rules can only do so much. We ask in this paper "what if we did not have to write the rules?". This is where we take a page from the book of classical statistical mechanics. In such models, which often involve graph-like structures as in the Ising model, the dynamics is not described upfront. Instead, the system of interest is equipped with an 'energy lansdcape' which specifies its long run behaviour, be it deterministic as in classical mechanics, or probabilistic in statistical physics. The dynamics just follows from the energy data. In the eye of a computer scientist, this use of energy looks like a latent syntax. (This is especially true in the application of these ideas to molecular dynamics.)

The broad aim of this paper is to make this syntax explicit by introducing energy patterns and costs from which the total energy of a state of the system can be computed; and to define a procedure whereby, indeed, the dynamics described as probabilistic graph-rewriting rules can be derived from these energy data. Descriptively, this takes us to an entirely new level of conciseness (as in the example §4). It also guarantees thermodynamical consistency, otherwise known to be undecidable [START_REF] Danos | Equilibrium and termination[END_REF], which is important for some applications. But perhaps the nicest byproduct of this approach is the fact that the methodology leads to parsimonious parameterizations. The parameter space which usually scales as the number of rules (which in turn has at best a logarithmic impact on the cost of a simulation event [START_REF] Danos | Scalable simulation of cellular signaling networks[END_REF]), will now scale as the number of energy patterns provided in the specification.

The particular kind of GTSs we consider forms a reversible subset of the Kappa site-graph stochastic rewriting language. Kappa is used for the simulation and analysis of combinatorial dynamical systems as typically found in cellular signalling networks [START_REF] Carlos F Lopez | Programming biological models in python using pysb[END_REF][START_REF] Tiger | A framework for mapping, visualisation and automatic model creation of signal-transduction networks[END_REF] and has been predicted to "become one of the mainstream modelling tools of systems biology within the coming decade" [START_REF] John | New approaches to modeling complex biochemistry[END_REF]. Similar graph formalisms where nodes have a controlled valence/degree have been considered e.g. the BNG language [START_REF] Faeder | Rule-based modeling of biochemical systems with BioNetGen[END_REF][START_REF] Hlavacek | Rules for modeling signal-transduction systems[END_REF], Kissinger and Dixon's quantum proof language [START_REF] Dixon | Open graphs and monoidal theories[END_REF], and Kirchner et al. chemical calculi [START_REF] Bournez | A rule-based approach for automated generation of kinetic chemical mechanisms[END_REF]. Site-graph rewriting has found recently a 'home' both in the single-pushout GTS tradition [START_REF] Danos | Constraining rule-based dynamics with types[END_REF] and the double-pushout one [START_REF] Hayman | Pattern graphs and rule-based models: The semantics of kappa[END_REF]. This makes one hopeful that the thermodynamic methodology we propose can crossover to other fields where quantitative GTSs can be used, e.g. in the modelling of adaptive networks [START_REF] Gross | Adaptive networks[END_REF]. While our scalable energy-based parameterization is particularly important in biological applications where parameters often need to be inferred, one can imagine it to be useful in other modelling situations with uncertainty.

Outline: We start with the definition and relevant properties of the specific GTS we use, namely a simple reversible fragment of Kappa. Next, we introduce growth policies (adapted from Ref. [START_REF] Murphy | Rule-based modelling and model resolution[END_REF]), a tool which allows one to replace a rule with an orthogonal set of refined rules while preserving the quantitative semantics. We use this tool with a specific policy which refines a rule into finitely many rules, each of which has a definite energy balance with respect to a given set of energy patterns. This leads to our main theorem which guarantees that the stochastic dynamics of the obtained refined rule set converges to an equilibrium distribution parametrized by the cost of each energy pattern. Throughout, the presentation is set in category-theoretic terms and mostly self-contained. A substantial example concludes the paper. (For lack of space, and following the advice of the referees, proofs were omitted in this extended abstract; these will be presented in a longer version.)

2 Site graph rewriting

Site graphs and homomorphisms

A site graph G consists of a finite sets of agents and sites, A G and S G , a partial function σ G : S G ⇀ A G , and a symmetric edge relation E G on S G . The pair A G , E G form an undirected graph; sites not in the domain of E G are said to be free. The role of the additional map σ G is to assign sites to agents; sites not in the domain of σ G are said to be dangling, and will be used to represent half-edges (see below). Usually one also endows agents and/or sites with states (see §4); the construction we will give in §3 carries over trivially to these.

One says G is realizable iff (i) no site has an edge to itself; (ii) sites have at most one incident edge; (iii) no dangling site is free; and, (iv) edges have at most one dangling site.

S G h S G G σ G ≤ S G ′ σ G ′ A G h A G G A G ′ A homomorphism h : G → G ′ of site graphs is a pair of functions, h S : S G → S G ′ and h A : A G → A G ′ , such that (i) when- ever h A (σ G (s)) is defined, so is σ G ′ (h S (s)) and they are equal; and (ii) if s E G s ′ then h S (s) E G ′ h S (s ′ ). A homomorphism h : G → G ′ is an embed- ding iff (i) h A and h S are injective; and (ii) if s is free in G, so is h S (s) in G ′ . If h : G → G ′ is an embedding and G ′ is realizable then G is also realizable.
Site graphs and homomorphisms form a category SG with the natural 'tiered' composition; embeddings form a subcategory; if in addition, we restrict objects to be realizable, we get the subcategory rSGe of realizable site graphs and embeddings.

The category of site graphs over C

A homomorphism h : G → C is a contact map over C iff (i) G is realizable, (ii) σ C is total and (iii) whenever h S (s 1 ) = h S (s 2 ) and σ G (s 1 ) = σ G (s 2 ), then s 1 = s 2 . The third condition of local injectivity means that every agent of G has at most one copy of each site of its corresponding agent in C; C is called the contact graph.

G h 0 0 ψ G G G ′ h ′ Ð Ð C
Hereafter, we work in the (comma) category rSGe C whose objects are contact maps over C, and arrows are embeddings such that the associated triangle commute in SG. We write Υ (h, h ′ ) for the set of such embeddings between h, h ′ contact maps over C; we also write | | for the domain functor from rSGe C to rSGe which forgets types. In particular, if h : G → C is a contact map, we write |h| for its source G.

The contact graph C is fixed and plays the role of a type: it specifies the kinds of agents that exist, the sites that they may possess, and which of the |S C | 2 possible edge types are actually valid. It also gives canonical names to the types of agents and their sites. In examples, we write agent and sites names directly.

In rSGe, a dangling site s in G can be mapped to any site of G ′ by an embedding h : G → G ′ ; as such, it can be used as an any site wild card when matching G. In rSGe C , the contact map c : G → C tells us which agent A in C the site s belongs to because σ C is total, and this must be respected by h; we call this a binding type wild card since it typically allows us to express the property of being bound to the site s of some occurrence of the agent A.

The category SG has all pull-backs, constructed from those in Set; it is easy to see that they restrict to rSGe C . The category SG also has sums, but these do not restrict to rSGe C . (Just like sums in Set do not restrict to the subcategory of injective maps.)

h 1 θ1 G G γ1 1 1 s i ∃!m h 2 θ2 o o γ2 h
However, rSGe C has multi-sums: meaning for all pairs of site graphs of type C, h 1 : G 1 → C and h 2 : G 2 → C, there exists a family of co-spans θ i 1 : h 1 → s i ← h 2 : θ i 2 , such that any co-span γ 1 : h 1 → h ← h 2 : γ 2 factors through exactly one of the family and does so uniquely. The idea is that the pairs θ i 1 , θ i 2 enumerate all minimal ways in which one can glue h 1 and h 2 , that is to say all the minimal glueings of G 1 and G 2 that respect C. There are finitely many which all factor through the standard sum in the larger slice category SG C .

The notion of multi-sum dates back to Ref. [START_REF] Diers | Familles universelles de morphismes[END_REF]; we will call them minimal glueings in rSGe according to their intuition in this concrete context, and use them in §3.2 to construct balanced rules.

Rules

L r L 0 0 I A ,I S G G R r R Ð Ð C A rule r over C is a pair of contact maps r L : L → C, r R : R → C which differ only in their edge structures, i.e. A L = A R , S L = S R , σ L = σ R , r LA = r RA , and r LS = r RS . A contact map m : M → C is a mixture iff σ M is total (no dangling edge) and, for all a ∈ A M , σ -1 M (a) ∼ = σ -1 C (m A (a)), i.
e. m S is locally surjective. In words, a mixture is a fully-specified site graph with respect to the type C.

r L G G ψ r R ψ ⋆ m G G m ⋆ (1)
An embedding ψ : r L → m induces a rewrite of a mixture m by modifying the edge structure of the image of ψ, i.e. an instance of L in M , to that of R; the result of rewriting is a new mixture m ⋆ , where |m ⋆ | has the same agents and sites as M = |m|, and an embedding ψ ⋆ : r R → m ⋆ . This can be formalized using double push-out rewriting [START_REF] Danos | Constraining rule-based dynamics with types[END_REF] (since all the required push-outs do exist in rSGe C ). But with the simple rules considered here, there is no need.

We also write Υ (r, m) for the set of all embeddings ψ : r L → m. The inverse of r, defined as r ⋆ := (r R , r L ) is also a valid rule; by rewriting m ⋆ with r ⋆ via ψ ⋆ , we recover m and ψ.

Given a finite set of rules G over C, we define a labelled transition system L G on mixtures over C: a transition from a mixture m is a rewriting step determined and labelled by an 'event' (r, ψ) as in diagram (1); with r in G, and ψ in Υ (r, m).

We suppose hereafter that G is closed under rule inversion, i.e. G = G ⋆ . Hence, every (r, ψ)-transition has an inverse (r ⋆ , ψ ⋆ ), and L G is symmetric. Hence, given a rate map k from G to R + , we can equip L G with the structure of an irreducible continuous-time Markov chain (CTMC), simply by assigning rate k(r) to an event of the form (r, ψ).

CTMC semantics

We write L k G for the obtained CTMC. We need here to record a definition for later use: a finite CTMC M has detailed balance for a probability distribution π on M's state space, if for all states x and y, π(x) • q(x, y) = π(y) • q(y, x) where q(x, y) is M's transition rate from x to y. This implies that, assuming M is irreducible, π is the unique fixed point of the action of M, to which the probabilistic state of M converge, regardless of the initial state.

Extensions and rule refinement

Epis of rSGe C can be characterized as follows [START_REF] Murphy | Rule-based modelling and model resolution[END_REF]: suppose s : G → C and s ′ : G ′ → C are contact maps then φ : s → s ′ of rSGe C is an epi iff every connected component of G ′ contains at least one agent in the image of φ A .

s φ 1 1 φ ′ s ′′ s ′ θ j j θ ′ t t =
(2) We refer to an epi φ : s → s ′ as an extension of s. The category of extensions of s is a pre-order, i.e. there is at most one arrow between any two objects: if

φ ′ = θφ = θ ′ φ then θ = θ ′ because φ is an epi. We write φ ≤ φ ′ for this specialization order. If φ ≤ φ ′ and φ ′ ≤ φ then we write φ ∼ =s φ ′ .
A family of epis φ i : s → t i uniquely decomposes s iff, for all mixtures m and embeddings h : s → m, there exists a unique i and ψ such that h = ψφ i . This is the basic requirement for a reasonable notion of rule refinement: it guarantees that the LHS s of a given rule splits into a non-overlapping collection of more specific cases t i .

In the next Section, we will be constructing specific such decompositions in order to produce families of sub-rules which are compatible with energy patterns.

First, we recall the growth policy method to find such unique decompositions which works by detailing which agents and sites should be added to s.

Specifically, a growth policy Γ for s is a family of functions Γ φ , indexed by extensions φ : s → t, where Γ φ maps u ∈ A |t| to a subset Γ φ (u) of σ -1 C (t A (u)), i.e. each agent in |t| is allocated a subset of the sites its sites can map to in C. An agent in |t| may cover some, or all, of these sites or even completely extraneous sites: if the former, i.e. for all u in A |t| , t S (σ -1 |t| (u)) ⊆ Γ φ (u), we say that φ is immature; if for all us, the inclusion is an equality, we say that φ is mature; otherwise φ is said to be overgrown. The functions Γ φ must satisfy, for all extensions φ and φ ′ ≥ φ, the faithfulness property, Γ φ = Γ φ ′ ψ A , where ψ is the epi witnessing φ ≤ φ ′ ; so a site requested by φ must be requested by any further extension. If φ is not overgrown then no φ ′ ≤ φ is overgrown either. Also, note that the union of two growth policies is itself a growth policy.

Given an s and a growth policy Γ for s, we define Γ (s) by choosing one representative per ∼ =s-isomorphism class of the set of all extensions of s which are mature according to Γ .

Theorem 1 If Γ is a growth policy for s, then Γ (s) uniquely decomposes s.

The theorem (adjusted from Ref. [START_REF] Murphy | Rule-based modelling and model resolution[END_REF]) guarantees that factorizations through Γ (s) are unique, but not that they always exist. In the next section, we will construct a growth policy for which this propoerty of exhaustivity of the decomposition can be proved by hand.

Given a rule r and an extension φ of r L , r φ denotes the 'refined' rule associated to φ. If Γ is a growth policy for r L , the refinement of r by Γ is the set of rules, Γ (r), the elements of which are of the form r φ , for φ in Γ (r L ) a mature extension.

It is easy to see that due to the simple nature of our rules, the category of extensions of r L and r R are isomorphic; if φ is an extension of r L , we will write φ ⋆ for the corresponding extension of r R .

An example of growth policy is the ground policy which assigns all possible sites to all agents. In which case: Γ (s) is simply the set, possibly infinite, of epis of s into mixtures, considered up to ∼ =s; and Γ (r), the ground refinement of r, contains all refinements of r along these epis, which therefore directly manipulate mixtures.

Rule generation

We fix a finite set G of generator rules; and a finite set P of connected contact maps in rSGe C ; these are our energy patterns.

The goal is now to refine G into a new rule set G P where each refined rule is P-balanced, which means that, however applied, it consumes or produces a fixed amount of each pattern c in P. The construction proceeds in two steps: first, we characterize balanced refinements; second, we define a growth policy with balanced mature extensions, and apply Th. 1. Note that ground extensions of g are trivially balanced but, in general, the ground refinement is impractically large or even infinite; ours will always be finite.

P-balanced extensions

c γ ′ G G γ 1 1 t r L ψ ′ o o ψ m
Consider c in P, and a rule r. For an r-event ψ to consume an instance γ of c in a mixture m, the cospan (γ S , ψ S ) must have images which intersect on at least one edge modified by r. This is the case iff the associated minimal glueing (γ ′ , ψ ′ ) -obtained by restricting the cospan to the union of its images in m-has the same property. Likewise, for an r-event to produce an instance of c, the associated minimal glueing between c and r R must have a modified intersection. We call such minimal glueings relevant; they are the ones which underlie events that can affect the set of instances of c.

g

L φ c γ 0 0 t θ ≃ ũ (3)
Pick g in G and φ : g L t an extension of g L . One says that φ is P-left-balanced iff, for all relevant minimal glueings γ : c → u ← t : θ with c ∈ P, θ is an isomorphism. This means that the image of c under γ is contained in t. Symmetrically, one says that φ is P-rightbalanced iff φ ⋆ is a P-left-balanced extension of r ⋆ .

An extension φ is P-balanced iff it is P-left-and P-right-balanced; we say that φ is prime iff it is minimal P-balanced in the specialization order ≤.

If φ is a P-balanced extension of g, the refined rule g φ has a balance vector in Z P , written ∆φ, where ∆φ(c), for c ∈ P, is the amount of c produced by any g φevent leading from m to m ⋆ , or equivalently the difference between the number of embeddings of c in the RHS and the LHS of g φ . Indeed, as φ is balanced,

|Υ (c, m ⋆ )| -|Υ (c, m)| = |Υ (c, g φ,R )| -|Υ (c, g φ,L )|.
Conversely, a non-P-balanced extension will incur different ∆φ(c) for wellchosen applications of g φ , if c in P violates the condition of diagram (3). Thus, the notion of balanced extension characterizes the property that we want. (This would no longer be the case if one were to relativize the construction to a superset of reachables; e.g. in order to reduce the size of the generated rule set.)

Add-by-glueing

We now define a growth policy, which uses minimal glueings on non-P-balanced extensions φ to add further required sites into φ's codomain; this corresponds in diagram (3) to the case where θ is not an isomorphism. Some care is needed to ensure faithfulness, i.e. Γ φ = Γ φ ′ φ φ ′ A , since relevant minimal glueings on φ can disappear along a further extension φ ′ and, consequently, a site that was 'requested' at φ may no longer be so after at φ ′ φ. To address this, we add site requests from all relevant minimal glueings in the past of an extension.

g L φ1 φ $ $ c γ 4 4 t 1 ∋ u 1 θ y y φ2 9 9 t ′ t ∋ u (4
) Given g ∈ G we define a growth policy Γ L for g L . Suppose φ : g L → t is an extension of g L . We set Γ L (φ) to request a site s in σ -1 C (t A (u)) at agent u ∈ A |t| iff either (i) u = φ A (u 0 ) and s = φ S (s 0 ) for some u 0 in A |g L | , s 0 in S |g L | ; or (ii) φ factorizes as φ 2 φ 1 , where φ 1 : s → t 1 , and there is a relevant minimal glueing γ :

c → t ′ ← t 1 : θ, u 1 in A |t1| , and a site s ′ 1 in σ -1 |t ′ | (θ A (u 1 )
) such that u = φ 2,A (u 1 ), and s = t ′ S (s ′ 1 ). The first clause simply ensures that all sites already covered in g L are asked for; the second one adds in sites which appear by glueing at some point between g L and t. We refer to φ 2 : t 1 → t as a rewind of φ.

Symmetrically, we define a growth policy Γ R for g R by applying the same definition to the reverse generator g ⋆ . Since extensions of g L and g R are isomorphic, we can, with a slight abuse of notation, define Γ P := Γ L ∪ Γ R .

Theorem 2

The above Γ P is indeed a growth policy for g L ; the induced refined rule set Γ P (g) is non-empty, balanced, exhaustive and finite.

Therefore, given G and P, we obtain a finite P-balanced rule set which refines G exhaustively, by setting G P := ∪g∈G Γ P (g) (disjoint sum). To every refinement g φ , corresponds an inverse refinement g ⋆ φ ⋆ ; hence, G P = G ⋆ P is closed under inversion like G.

Rates

To equip G P with rates, we suppose given a P-indexed real-valued vector of energy costs ǫ, and a rate map k : G P → R + such that, for all g φ in G P :

log k(g ⋆ φ ⋆ ) -log k(g φ ) = ǫ • ∆φ (5)
with ∆φ in Z P , the balance vector of the refined rule g φ with respect to P, a well-defined quantity by Th. 2. We write P(x) for the P-indexed vector which maps c to |Υ (c, x)|, and define the energy E(x) of x as ǫ • P(x). We also write L G (x) for the finite (strongly) connected component of x in L G , and define a probability distribution (in Boltzmann format) on L G (x) by:

π x (y) := e -ǫ•P(y) / y∈L G (x) e -ǫ•P(y) (6)
Theorem 3 Let G, P, G P , k, and π x be as above; L G P and L G are isomorphic as symmetric LTSs; and, for any mixture x, the irreducible continuous-time Markov chain L k G P has detailed balance for, and converges to π x , on L G P (x) = L G (x) the finite strongly connected component of x.

Note that the subset of the state space which is reachable from x in L G , namely L G (x) is finite; hence, the partition function Z(x) = y∈L G (x) e -E(y) is finite. With rules which increase the number of agents, components L G (x) can be infinite, and Z(x) may diverge. For (mass action stochastic) Petri nets, convergence is guaranteed if detailed balance holds, but it is not true in general for Kappa [START_REF] Danos | Equilibrium and termination[END_REF][START_REF] Danos | Equilibrium and termination II: the case of Petri Nets[END_REF].

Another point worth making is that the result holds symbolically-regardless of the energy cost ǫ. So ǫ can be seen as a set of parameters, an ideal support for machine learning techniques if one were contemplating fitting a model to data.

A linear kinetic model

So, the reader will ask, what of the actual rates of L k G P ? Among all possible choices which accord with [START_REF] Danos | Constraining rule-based dynamics with types[END_REF], it is possible to delineate a tractable subset the size of which grows quadratically in |P|. This is a useful log-linear heuristics, which is common in machine learning but has no claim to validity.

We keep the same notations as in Th. 3. Suppose we have, for every generating rule g in G, a constant c g ∈ R, and a matrix A g of dimension |P| × |P|. Subject to the constraints that c g ⋆ = c g , and A g ⋆ + A g = I, we can define a log-affine rate map which satisfies (5) by:

log(k(g φ )) := c g -A g (ǫ) • ∆φ (7)
The kinetic model expressed in [START_REF] Danos | Agile modelling of cellular signalling[END_REF] requires of the order of |P| 2 × |G| parameters. In practice, one needs even fewer parameters, as only those energy patterns that are relevant to a given g, i.e. have a non-zero balance for at least one rule in Γ P (g), need to be considered when building A g . Typically, for larger models, this will be a far smaller number than |P|. This relative parsimony is compounded by the fact that the number of independent parameters will be often lower, because the ∆φ family has often low rank. It is to be compared with the total number of choices possible which is far greater as it is of the order of the number of refinements, that is to say g∈G |Γ P (g)|.

If we set c g ⋆ = c g = 0, A g ⋆ = 0, A g = I, we get: k(g φ ) = e -ǫ•∆φ , k(g ⋆ φ ⋆ ) = 1. As ǫ • ∆φ is the difference of energy between the target and source in any application g φ , this choice amounts to being exponentially reluctant to climb up the energy gradient. This is a continuous-time version of the celebrated Metropolis algorithm [START_REF] Metropolis | Equation of state calculations by fast computing machines[END_REF].

Allosteric ring

We can put our energy-based modelling methodology to use on a realistic example of a bacterial flagellar engine. In this section, we will prefer the traditional syntax of Kappa to denote site graphs: namely subscripts for states and shared superscripts for edges between sites, e.g. A(x 1 0 ), B(y 1 ). Differently from the mathematical definitions of §2, agent and site types are indicated as explicit labels.

We use KaSim (https://github.com/jkrivine/KaSim), the standard Kappa engine, for the simulation shown below.

The engine can rotate clockwise or anti-clockwise at high angular velocities, and this will decide whether the bacterium tumbles or swims forward. One can build a simple model of the switch between the two modes [START_REF] Bai | Conformational spread as a mechanism for cooperativity in the bacterial flagellar switch[END_REF]. The engine is seen as a ring of n identical components, P , with two possible conformations, 0 and 1. (In reality, each of the n = 34 component protomers is itself a tiny complex made of different subcomponents, but the model ignores this.) A ring homogeneously in state 0 (1) rotates (anti-) clockwise and induces tumbling (straight motion). Importantly, neighbouring P s on the ring prefer to have matching conformations. States of the ring with many mismatches thus incur high penalties. In the absence of any Y molecule binding a P , its favoured conformation is 0; conversely, in the presence of a Y, P favours 1. (Y stands for a small diffusible protein named CheY.) To bind, Y has to be activated by an external signal. Hence the switch can be triggered by a sudden activation of Y which then binds the ring and induces a change of regime. The sharper the transition between the two regimes the better.

As each of the P s can be in four states, the ring has on the order of 10 20 nonisomorphic configurations which precludes any reaction-based (e.g. Petri nets) approach to the dynamics where each global state is considered as one chemical species. At this stage, we could apply the rule-based approach, or, better, we can obtain the rules indirectly by applying the methodology of §3. This is what we do now informally.

First, we define our contact graph with two agent types: P (x, y, f 0,1 , s) with domains x, y to form the ring, s to bind its signal Y , and f a placeholder for P 's conformation; Y(s u,p ) with two internal states to represent activity.

Motif

Cost

P (f i , x 1 ), P (y 1 , f j ) ǫ P P ij P (f i ) ǫ P i P (f i , s 1 ), Y (s 1 ) ǫ P Y i
Second, we capture the informal statements in the discussion above by defining the energy patterns and associated costs. Note that the various motifs overlap. Following §3, we associate to each ring configuration x the occurrence vector P(x) and total energy ǫ • P(x). For example, a ring of size n uniformly in state 0 and with no bound Y s has total energy n(ǫ P P 00 + ǫ P 0 ). This, in turn, defines the equilibrium distribution of the ring, namely x has probability proportional to exp(-ǫ • P(x)). (The convention is that the lower the energy, the likelier the state.) ǫ P P 00 , ǫ P P 11 < ǫ P P 10 , ǫ P P 01 (8)

ǫ P 0 < ǫ P 1 ( 9
)
ǫ P Y 0 > ǫ P Y 1 (10)
In order to complete our energy landscape, we need to pick energy costs which reward or penalize local configurations as discussed above: the role of ( 8) is to align the internal states of neighbours on the ring -an Ising penalty term for mismatching neighbours which will "spread conformation"; (9) makes 0 the favoured state, while [START_REF] Dixon | Open graphs and monoidal theories[END_REF], which kicks in only in the presence of Y, makes 1 the favoured state. has a ∆E which is ambiguous as it will be either ǫ P Y 0 or ǫ P Y 1 depending on its instances; hence, we have no hope of assigning rates to this rule that satisfy detailed balance-unless ǫ P Y 0 = ǫ P Y 1 , which contradicts [START_REF] Dixon | Open graphs and monoidal theories[END_REF]. To get a definite balance, one needs to refine this rule:

b 0 := P (f 0 , s), Y (s p ) ↔ P (f 0 , s 1 ), Y (s 1 p ) b 1 := P (f 1 , s), Y (s p ) ↔ P (f 1 , s 1 ), Y (s 1 p )
Now each rule b i specifies enough of the context in which it applies to have a definite energy balance ǫ P Y i . Following the same intuition of revealing (just) enough context, we obtain a balanced rule set for conformational changes:

f ij := P (f i , y 1 ), P (x 1 , f 0 , y 2 , s), P (x 2 , f j ) ↔ P (f i , y 1 ), P (x 1 , f 1 , y 2 , s), P (x 2 , f j ) f ′ ij := P (f i , y 1 ), P (x 1 , f 0 , y 2 , s ), P (x 2 , f j ) ↔ P (f i , y 1 ), P (x 1 , f 1 , y 2 , s ), P (x 2 , f j )

The first (second) group of rules represents the changes in the absence (presence) of a Y bound to the middle P undergoing a change of conformation. (The fact that P 's site s is bound is indicated by the underscore exponent.) These f -rules have respective balance:

ǫ P P i1 + ǫ P P 1j -ǫ P P i0 -ǫ P P 0j + ǫ P 1 -ǫ P 0 ǫ P P i1 + ǫ P P 1j -ǫ P P i0 -

ǫ P P 0j + ǫ P 1 -ǫ P 0 + ǫ P Y 1 -ǫ P Y 0
As we have ten reversible rules, and only eight energy patterns, there must be linear dependencies between the various balances. Indeed, in this case, it is easy to see that the family of vector balances has rank six. Thermodynamic consistency induces relationships between rates; a well-established fact in the case of reaction networks (e.g. see Ref. [START_REF] Danos | Equilibrium and termination II: the case of Petri Nets[END_REF]).

With the rules in place, the final step is to choose rates which satisfy detailed balance. This guarantees that the obtained rule set converges to the equilibrium specified by the choice of the energy cost vector. Convergence will happen whatever ǫ is, ie symbolically. If, in addition, ǫ follows (8-10), one can see in Fig. 1 that the ring 1) undergoes sharp transitions when active Y is stepped up and down again, and 2) has at all times very few mismatches.

:= P (s), Y (s p ) ↔ P (s 1 ), Y (s 1 p ) f := P (f 0 ) ↔ P (f 1 )
Note that there is a design choice here. In effect, we are saying that we are not interested in forming/breaking the bonds between the P s in the ring. If we wanted to incorporate also the ring assembly in the model, we would have to add P (x), P (y) ↔ P (x 1 ), P (y 1 ) among our generator set G. This would generate many more refined rules, as we will see. Recall that our patterns fall in three subgroups: P (f i , x 1 ), P (y 1 , f j ); P (f i ); and P (f i , s 1 ), Y (s 1 ).

Consider the extensions of b: clearly only the last pattern can glue relevantly on it; the corresponding (unique) site request is for P to reveal f and its internal state. This gives the first two rules b 0 , b 1 .

Consider now the more interesting extensions of f : the second pattern type glues relevantly but does not generate any site request; the third one asks P to reveal its site s, resulting in two possible extensions (s means that s is bound):

P (f 0 , s) ↔ P (f 1 , s) P (f 0 , s ) ↔ P (f 1 , s )
These extensions are not mature yet, as one can glue relevantly patterns of the first type on both sides of P , inducing a further request for revealing P 's sites x and y. If we are in the component of an initial state where P s are arranged in a ring, then we know that the neighbours on both sides exist and are P s; this gives the final refinement of the above into the rules f ij , f ′ ij described earlier. If, on the other hand, we do not know that, we also have to add several rules where one or both of x, y are free, corresponding to open P -chains. This demonstrates the sensitivity of the obtained rule set to the initial choice of generators. Hence, the rule set above does accord with our general refinement strategy of §3. We can visualize the obtained simulations by extracting snapshots before, after and during the injection of active Y s, as in Fig. 2. Again we see few mismatches in both regime because of the Ising interaction expressed by the ǫ P P energy costs. The full model is available on-line at http://www.rulebase.org/ models/ising-ring. The choice of rates made in Ref. [START_REF] Bai | Conformational spread as a mechanism for cooperativity in the bacterial flagellar switch[END_REF] for the f -generator is a particular symmetric case of our model [START_REF] Danos | Agile modelling of cellular signalling[END_REF], namely A f ⋆ = A f = I/2.

Conclusion

We have presented a new 'energy-oriented' methodology for the development of site graph rewriting models based on a set P of energy patterns; these patterns use a graphical syntax which allows us to specify the energy landscape. Rewrite rules are implicitly defined by P and generator rules G. The resulting rule set G P is guaranteed to be thermodynamically correct and to eventually converge to the probability distribution described by the energy landscape given suitable rates. The construction is entirely parametric in the energy costs ǫ, and modular in G. This means that in a modelling context, one can sweep over various values for ǫ without having to rebuild the model, and compositionally add new rule components to G. Both features are clearly useful.

We expect our construction to provide a broad and uniform language to describe and analyse models of interacting biomolecules and similar systems of a quantitative fine-grained and distributed nature.

There are no specific conditions bearing on this construction other than that energy patterns should be local. It would be interesting to investigate whether, suitable constraints on patterns and generator rules can obtain optimized generated rule sets. Another interesting extension would be to deal with non-local forms of energies expressing long-range interactions, where the metric is read off the graph itself. In practice, there will be many more rules generated, and beyond the descriptive aspects, simulations will need new ideas to be feasible. A ray of hope comes from the log-affine kinetic model (presented in the last subsection), as rules can be partitioned by energy balances for faster selection.

Finally, as said in the introduction, there is a growing body of literature which turns a theoretical eye to site graph rewriting [START_REF] Hayman | Pattern graphs and rule-based models: The semantics of kappa[END_REF][START_REF] Dixon | Open graphs and monoidal theories[END_REF][START_REF] Heckel | DPO transformation with open maps[END_REF][START_REF] Danos | Constraining rule-based dynamics with types[END_REF], and it is tempting to ask whether our derivation can be replayed in more abstract settings; in particular, it would be very interesting to investigate its integration with the abstract framework for rule-based modelling developed in [START_REF] Lynch | A logical characterization of individual-based models[END_REF].

  It is not difficult to see that for any rule r, |Υ (r, m)| ≤ |A |m| | d(r) where d(r) is the number of connected components in r L . Hence, L G has finite out-degree, bounded by |G| • |A |m| | d for some d. Also, as agents are preserved by rules, the (strongly) connected components of L G are finite.

  The next step is to create the dynamics. The naive rule b for PY binding: b := P (s), Y (s p ) ↔ P (s 1 ), Y (s 1 p )

4. 1

 1 How to generate the rules Our set of balanced rules for the ring dynamics was based on two generators, b for binding, f for flipping: b

Fig. 1 .

 1 Fig. 1. The simulation steps up the amount of active Y at t = 100, and down again at t = 200; this sends the entire ring into an homogeneously 1 conformation, and back to 0. The number of mismatches (lowest curve) stays low, even during transitions.

Fig. 2 .

 2 Fig. 2. Snapshots of the ring configuration are taken at time 500, 1500, and 2500. Solid (green) circles indicate conformation 1, hollow ones conformation 0; a dot in the centre indicates a bound (hence active) Y . At times 500, 2500, no Y is bound (because they are all inactive) and the ring is globally in state 0, up to tiny fluctuations; at time 1500, it is globally in state 1 as a consequence of the binding of Y s.

Acknowledgments We would like to thank Peter Swain, Andrea Weisse, Julien Ollivier, Nicolas Oury, Finlo Boyde and Eric Deeds for many useful and fascinating conversations concerning the subject of this paper.


P Clairambault

Andrzej S Murawski

Böhm Trees as Higher-Order Recursive Schemes

Keywords: Subject Classification F.3.3, F.4.1 Lambda calculus, Böhm trees, Recursion Schemes 1

Higher-order recursive schemes (HORS) are schematic representations of functional programs. They generate possibly infinite ranked labelled trees and, in that respect, are known to be equivalent to a restricted fragment of the λY -calculus consisting of ground-type terms whose free variables have types of the form o → ⋯ → o (with o being a special case).

In this paper, we show that any λY -term (with no restrictions on term type or the types of free variables) can actually be represented by a HORS. More precisely, for any λY -term M , there exists a HORS generating a tree that faithfully represents M 's (η-long) Böhm tree. In particular, the HORS captures higher-order binding information contained in the Böhm tree. An analogous result holds for finitary PCF.

As a consequence, we can reduce a variety of problems related to the λY -calculus or finitary PCF to problems concerning higher-order recursive schemes. For instance, Böhm tree equivalence can be reduced to the equivalence problem for HORS. Our results also enable MSO modelchecking of Böhm trees, despite the general undecidability of the problem.

Introduction

Higher-order recursive schemes (HORS) are a class of programming schemes introduced to account for recursive procedures with higher-order parameters [START_REF] Damm | The IO-and OI-hierarchies[END_REF]. They can be viewed as grammars describing a potentially infinite tree. As tree generating devices, HORS can be identified with a limited fragment of the λY -calculus [START_REF] Statman | On the lambdaY-calculus[END_REF] consisting of ground-type terms whose free variables have types of order at most 1. The free variables play the role of tree constructors. HORS have recently been intensively investigated in connection with program verification. Notably, Ong [START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF] showed that monadic second-order logic (MSO) is decidable over trees generated by HORS and Kobayashi [START_REF] Kobayashi | Types and higher-order recursion schemes for verification of higher-order programs[END_REF] took advantage of the result to propose a novel approach to the verification of higher-order functional programs.

As already mentioned, HORS are naturally viewed as a fairly small fragment of the λYcalculus: they generate potentially infinite trees, whereas normal forms of arbitrary λY -terms additionally contain variable bindings. This binding information cannot be represented in HORS explicitly. In fact, it turns out that MSO becomes undecidable over Böhm trees of λY -terms, if the binding relation is included in the signature. Nevertheless, as we show in the paper, HORS still allow one to generate faithful representations of (η-long) Böhm trees of λY -terms, where binding is encoded indirectly via De Bruijn levels [START_REF] De Bruijn | Lambda calculus notation with nameless dummies[END_REF]. We also prove an analogous representation theorem for the finitary (finite datatypes) variant PCF f of PCF [START_REF] Plotkin | LCF considered as a programming language[END_REF].

Our results make it possible to recast a variety of problems related to the λY -calculus or finitary PCF as problems concerning higher-order recursive schemes. For example, we obtain a reduction of Böhm tree equivalence in the λY -calculus or PCF f to the (tree) equivalence problem for HORS. Unfortunately, the latter is currently not known to be decidable and is closely related to the equivalence problem for deterministic collapsible pushdown automata [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]. The Böhm tree equivalence problem for PCF f also has semantic significance, because PCF Böhm trees [START_REF] Abramsky | Full abstraction for PCF[END_REF] are concrete representations of the strategies representing the terms in game semantics, and therefore characterize contextual equivalence in PCF with respect to contexts featuring state and control effects.

Other consequences, in the form of decidability results, can be derived by applying Ong's decidability result to representations of Böhm trees obtained through our theorems. In this way, one can show that numerous problems for λY or PCF f are decidable. Examples include normalizability, finiteness, solvability or having a Böhm tree prefixed by a given finite term. Some of the results are already known, while others appear new.

Thus far, higher-order verification based on HORS focussed on model-checking trees extracted from programs. Our contribution opens the perspective of applying model-checking to terms with binding and arbitrary free variables, such as higher-order components of closed programs.

2

λY -calculus

Böhm trees of λY -terms

We work with simple types built from a single atom o using the arrow type constructor. They are defined by the grammar given below.

θ ∶∶= o θ → θ
The order of a type is defined as follows.

ord(o) = 0 ord(θ 1 → θ 2 ) = max(ord(θ 1 ) + 1, ord(θ 2 ))
Terms are considered up to α-equivalence, and equipped with β-reduction and η-expansion (respectively written → β and → η ). We write ≃ βη for the symmetric reflexive and transitive closure of → β and → η . We shall consider several extensions of the simply-typed λ-calculus over the types introduced above.

The λ -calculus additionally contains a constant o ∶ o. More generally, we shall write θ for terms specified as follows.

θ = o θ ≡ o λx θ1 . θ2 θ ≡ θ 1 → θ 2
For λ -terms, let us define a partial order ⊑ (relating only terms with equal types) by

M ⊑ M o ⊑ M M 1 ⊑ M 2 λx.M 1 ⊑ λx.M 2 M 1 ⊑ M ′ 1 M 2 ⊑ M ′ 2 M 1 M 2 ⊑ M ′ 2 M ′ 2 .
We will also consider the extension of the λ -calculus to infinite terms, which we refer to as the λ ∞ -calculus. The partial order ⊑ can be extended to λ ∞ -terms to yield an ω-cpo.

The λY -calculus contains a family of fixed-point operators Y θ ∶ (θ → θ) → θ, where θ ranges over arbitrary types, equipped with the reduction rule

Y θ M → Y M (Y θ M ). ▸ Definition 1. Given a λY -term M and n ∈ N, the nth approximant of M , written M ↾ n, is a λ -term defined by x ↾ n = x λx.M ↾ n = λx.(M ↾ n) M N ↾ n = (M ↾ n) (N ↾ n) Y θ ↾ n = λf θ→θ .f n ( θ ).
▸ Definition 2. The η-long Böhm tree of a λ -term Γ ⊢ M ∶ θ, written BT(M ), is its β-normal η-long form. For a λY -term Γ ⊢ M , the η-long Böhm tree, also denoted by BT(M ), is defined to be ⊔ n BT(M ↾ n).

Being η-long, these infinite normal forms might be more adequately called Nakajima trees [START_REF] Nakajima | Infinite normal forms for the λ-calculus[END_REF]. However, their PCF counterparts are generally called PCF Böhm trees [START_REF] Curien | Abstract Böhm trees[END_REF]. So, for consistency, we call them η-long Böhm trees, and for conciseness we will often omit η-long.

▸ Definition 3. λY -terms satisfying Γ ⊢ M ∶ o are called ground. Given n ≥ 0, we shall say that a ground term Γ ⊢ M ∶ o is of level n if, for all (x ∶ θ) ∈ Γ, we have ord(θ) < n.

Note that the free variables in a ground term of level 2 can have types of order 0 or 1, i.e. they are of the form o → ⋯ → o, where o has at least one occurrence. Thus, Böhm trees of such terms are (possibly infinite) trees.

The restrictions on types of free variables in ground terms of level 2 are analogous to the restriction concerning types of terminal symbols in higher-order recursion schemes [START_REF] Damm | The IO-and OI-hierarchies[END_REF]. In fact, it can be shown that the Böhm trees of level-2 ground terms coincide with trees generated by higher-order recursive schemes [START_REF] Salvati | Recursive schemes, Krivine machines, and collapsible pushdown automata[END_REF], and therefore have a decidable MSO theory.

In this paper, we are interested in the study of the Böhm trees of arbitrary λY -terms. Unlike in the case of level-2 ground terms, Böhm trees of arbitrary λY -terms involve binders, as illustrated by the following example.

▸ Example 4. Consider G = Y o→(o→o)→o (λf o→(o→o)→o .λy o .λx o→o . b (x y) (f (x y))) a, which has type (o → o) → o in context a ∶ o, b ∶ o → ((o → o) → o) → o. Its Böhm tree is λx 1 . b (x 1 ~a) (λx 2 . b (x 2 c c (x 1 y y a)) (λx 3 . b (x 3 { { (x 2 w w (x 1 j j a))) (λx 4 . . . .
where the arrows indicate binding information: for each variable occurrence, the arrow indicates the location of the associated binder. Note that because all bound variables are used infinitely often, countably many variable names are required to represent binding.

This binding information is far from innocent: in fact, we prove in the next section that it makes MSO undecidable. In particular, the term G above has an undecidable MSO theory.

Undecidability of MSO with binders

φ ∶∶= X x x λ → y x n → y ¬φ φ ∨ φ φ ∧ φ ∃x. φ ∀x. φ ∃X. φ ∀X. φ
We write the first-order variables x, y in a different font to distinguish them from the variable names of the λ-calculus. The validity of an MSO formula φ on a binding structure B, written B ⊧ φ, is defined as usual.

g 1,3 R / / U O O g 2,3 R / / U O O g 3,3 U O O g 1,2 R / / U O O g 2,2 U O O g 1,1 U O O (b) The half-grid in BT(G)
Figure 1 Construction of the half-grid ▸ Theorem 6. MSO is undecidable on binding structures corresponding to Böhm trees of λY -terms.

Proof. We reduce the well-known undecidable problem of deciding MSO on the infinite half-grid to MSO over binding structures generated by λY -terms. In particular, we will show that the binding structure B(BT(G)) contains an MSO-definable half-grid. The nodes of the half-grid will be occurrences of bound variables in BT(G), which are definable by the formula grid(x) ≜ ∃y. x λ → y. We say that a bound variable occurrence x i is at layer j if it occurs after j applications of b. Then for any 1 ≤ i ≤ j, there is a unique occurrence of the bound variable x i at layer j, we denote it by g i,j . The g i,j 's will be the nodes of the half-grid; in Figure 1a we describe the intended correspondence between occurrences of bound variables in BT(G) and the half-grid. The following two relations correspond respectively to moving right and up inside the grid.

x

R → y ≜ y 0 → x x U → y ≜ ∃z. z 0 * → x ∧ z 10 * → y ∧ ∃x ′ . x λ → x ′ ∧ y λ → x ′
1 ≤ i ≤ j and 1 ≤ i ′ ≤ j ′ we have g i,j R → g i ′ ,j ′ iff i ′ = i + 1 and j ′ = j, and g i,j U → g i ′ ,j ′ iff i ′ = i and j ′ = j + 1.
Consequently, the half-grid is MSO-definable within BT(G) and, thus, the latter must have an undecidable MSO theory. ◂

De Bruijn representations of binders

Theorem 6 exhibits a difference in expressivity between HORS and the λY -calculus. Nonetheless, in the following, we shall show how to construct HORS that faithfully capture Böhm trees generated by λY -terms. To that end, we shall use binder-free representations. As a consequence, we will be able to recast problems concerning the λY -calculus in the setting of HORS. In particular, we will retain the decidability of MSO model-checking such representations, which will provide us with a technique to verify a variety of properties of λY -terms in spite of Theorem 6.

Our binder-free representation scheme will rely on De Bruijn levels [START_REF] De Bruijn | Lambda calculus notation with nameless dummies[END_REF]: each bound variable x is given an index i, where i is the sum of a starting index and the number of lambdas enclosing the binding location (De Bruijn levels should not be confused with De Bruijn indices, which associate numbers to variable uses and not their points of introduction, and can associate different numbers to different occurrences of the same variable).

▸ Example 7. Consider the term M = λf (o→o)→o .Y o (λy o .f (λx o .b x y)), of type ((o → o) → o) → o in context b ∶ o → o → o.
The Böhm tree of M , annotated with De Bruijn levels, has the shape λx 1 .x 1 (λx 2 .x 0 x 2 (x 1 (λx 3 .x 0 x 3 (x 1 (λx 4 . . . . , where b ∶ o → o → o is given an index of 0. Note that each variable introduction and use are now labelled with a natural number. This representation is unique, in the sense that, for a fixed choice of indices for free variables and a choice of a starting index, two α-equivalent terms must have the same representation.

With De Bruijn levels, λ -terms can be represented as level-2 ground terms, typable in a special context defined below.

▸ Definition 8. Let Γ rep be the following context.

{ z ∶ o, succ ∶ o → o, var ∶ o → o, app ∶ o → o → o, lam ∶ o → o → o }
Given n ∈ N, we write n for the term succ n (z).

In particular, the terms n will be used to represent binding information as De Bruijn levels.

▸ Definition 9. Let Γ ⊢ M ∶ θ be a λ -term and let ν ∶ Γ → N be an injection. We define another λ -term Γ rep ⊢ rep ν (M, n) ∶ o by rep ν ( , n) = rep ν (λx.M, n) = lam n rep ν⊕{x↦n} (M, n + 1) rep ν (x, n) = var ν(x) rep ν (M N, n) = app rep ν (M, n) rep ν (N, n).
Note that, as long as n > max (x∶θ)∈Γ ν(x), rep ν (M, n) faithfully represents the syntactic structure of

M . Given Γ ⊢ M ∶ θ, where Γ = {x 1 ∶ θ 1 , ⋯, x k ∶ θ k }, let ν ∶ Γ → N be defined by ν(x i ) = i -1. We define rep(M ) to be rep ν (M, k).
For any finite λ -term M , rep(M ) gives a binder-free representation of M as a ground λ -term in context Γ rep . Being monotonic, the function rep preserves ω-chains, and therefore can be used to represent the Böhm tree of any λY -term as a ground infinite λ ∞ -term in context Γ rep . This invites the question whether this infinite λ ∞ -term can always be obtained as the Böhm tree of a level-2 ground λY -term.

T (n) = app (var 1) (lam n (app (app (var 0) (var n) T (n + 1))))
More precisely, we have

⊔ n rep(BT(M ↾ n)) = M ∞ . In this case, it is easy to extract a λY -term Γ rep ⊢ M rep ∶ o such that BT(M rep ) = M ∞ from the definition of M ∞ .
This can be done by expressing the coinductive definition of M ∞ inside the λY -calculus as

M rep = lam 1 (Y o→o M step 2)
, where

M step = λT o→o . λn o .app (var 1) (lam n (app (app (var 0) (var n)) (T (succ n)))).
Consequently, the Böhm tree of M rep is a binder-free representation of the Böhm tree of M .

In our paper, we show how to obtain such representations in a systematic way.

▸ Theorem 11. Let Γ ⊢ M ∶ θ be a λY -term. There exists a level-2 λY -term

Γ rep ⊢ M rep ∶ o such that BT(M rep ) = ⊔ n rep(BT(M ↾ n)).
Next we describe the construction underlying our proof of Theorem 11. In this section we only provide the necessary definitions, delegating the proof and a methodological discussion to Section 3. The construction uses normalization by evaluation [START_REF] Dybjer | Normalization and partial evaluation[END_REF] and, in particular, the observation that the technique can be internalized within the λY -calculus in our case.

Consider

Γ ⊢ M ∶ θ with Γ = {x 1 ∶ θ 1 , ⋯, x k ∶ θ k }.
First we apply a simple transformation on type annotations inside M and substitute o → o for o: let M * be defined as

M [o → o o].
The substitution is meant to be applied to types θ occurring in λ-abstractions (λx θ .M ) and fixed-point combinators (Y θ ). Observe that

x 1 ∶ θ * 1 , ⋯, x k ∶ θ * k ⊢ M * ∶ θ * ,
where

o * = o → o, (θ ′ → θ ′′ ) * = (θ ′ ) * → (θ ′′ ) * .
Next we define by mutual recursion two families of λ-terms {↓ θ }, {↑ θ }, subject to the following conditions:

Γ rep ⊢ ↓ θ ∶ θ * → o → o and Γ rep ⊢ ↑ θ ∶ (o → o) → θ * .
We write λ.M for λz o .M , where z does not occur in M .

↓ o = λx o→o .x ↓ θ ′ →θ ′′ = λx (θ ′ →θ ′′ ) * . λv o . lam v (↓ θ ′′ ( x (↑ θ ′ λ.(var v)) ) (succ v) ) ↑ o = λx o→o .x ↑ θ ′ →θ ′′ = λe o→o . λa (θ ′ ) * . ↑ θ ′′ ( λv o . app (e v) (↓ θ ′ a v) )
Now, with all the definitions in place, it turns out that one can take M rep to be

↓ θ M * [ ↑ θ1 λ.(var 0) x 1 , ⋯ , ↑ θ k λ.(var k -1) x k ] k.
In the next section we shall prove that M rep indeed represents the Böhm tree of M in the sense of Theorem 11. Before that, we illustrate the outcome of the construction on an example.

▸ Example 12. Let us revisit the term M from Example 7. We have

M * = λf ((o→o)→(o→o))→(o→o) .Y o→o (λy o→o .f (λx o→o .b x y))
and, thus,

M rep =↓ ((o→o)→o)→o M * [↑ o→o→o λ.(var 0) b] 1.
By unfolding the definitions of ↓ θ , ↑ θ and applying β-reduction the term can be rewritten. In fact, taking advantage of the β-equivalences

↑ o→o→o ≃ β λe o→o 1 .λa o→o 1 .λa o→o 2 .λv o 2 . app (app (e 1 v 2 ) (a 1 v 2 )) (a 2 v 2 ) ↓ ((o→o)→o)→o ≃ β λx (((o→o)→o)→o) * .λv o 1 . lam v 1 (x M aux (succ v 1 )),
where

M aux = λa (o→o) * .λv o 2 . app (var v 1 ) (lam v 2 (a (λ.var v 2 ) (succ v 2 ))), one can show that M rep is β-equivalent to

Internalized normalization by evaluation

In this section, we present the mathematical development that led to the term transformation of the previous section. As already mentioned, the main idea comes from normalization by evaluation (NBE). NBE is a general method used to construct normal forms for terms through their denotational semantics; the reader is referred to [START_REF] Dybjer | Normalization and partial evaluation[END_REF] for an introduction. The basic idea is to interpret terms in a suitable semantic universe. By soundness, the interpretation will be invariant under syntactic reduction. Moreover, if one uses a class of domains expressive enough to encode representations of normal forms, then one can attempt to extract a representation of the normal form of a term from the semantics. Notably, the extraction can be performed by evaluating the interpretation map on well-chosen elements of the domain, which yields an entirely semantic normalization procedure. NBE has been described for a variety of languages, including the simply-typed λ-calculus [START_REF] Berger | An inverse of the evaluation functional for typed lambdacalculus[END_REF] as well as richer languages with coproducts [START_REF] Altenkirch | Normalization by evaluation for typed lambda calculus with coproducts[END_REF], or type theory [START_REF] Abel | Normalization by evaluation for Martin-Löf type theory with typed equality judgements[END_REF]. Our presentation of NBE follows along the lines of [START_REF] Dybjer | Normalization and partial evaluation[END_REF]. The main novelty is the internalization of the process within the λY -calculus itself, which ultimately allows us to present NBE as a term transformation.

Semantic NBE for the λY -calculus

We first describe a domain semantics for the λY -calculus that will be exploited to obtain an NBE procedure. We assume the basic vocabulary of domain theory, e.g. [START_REF] Winskel | The Formal Semantics of Programming Languages[END_REF]. Let us recall that an ω-cpo is a partial order where each ω-chain (of the form x 1 ≤ x 2 ≤ . . . ) has a supremum. We will interpret types as pointed ω-cpos, i.e., ω-cpos with a bottom element written . A function f ∶ A → B is continuous if it preserves suprema of ω-chains. The set of continuous functions from A to B, ordered pointwise, is itself a pointed ω-cpo, denoted by A → B.

Our NBE procedure will generate representations of Böhm trees of λY -terms as elements of the pointed ω-cpo of λ ∞ -terms of ground type in context Γ rep , henceforth referred to as E. Representations based on De Bruijn levels lack compositionality: the indices present in a subterm depend on the number of variables abstracted in the context in which the subterm occurs. In order to overcome the difficulty, instead of constructing directly De Bruijn terms in E, we will construct term families [START_REF] Dybjer | Normalization and partial evaluation[END_REF], intuitively functions N → E, which -unlike De Bruijn terms -can be manipulated compositionally.

We now describe our semantic NBE for λY . In our case, E will also be used to represent natural numbers, so term families will be interpreted as elements of the pointed ω-cpo Ê = E → E, where the first E plays the role of N. For the sake of clarity, we will sometimes write N instead of E to highlight subterms representing natural numbers. This should not create any confusion.

Our NBE relies on the standard interpretation of the λY -calculus with o = Ê. Note that we write λ, rather than λ, to stress that the semantic operation of function abstraction (on continuous functions between pointed ω-cpos) is meant.

o = Ê x ρ = ρ(x) ρ = λx θ .M ρ = λa θ . M ρ⊕{x↦a} θ 1 → θ 2 = θ 1 → θ 2 M N ρ = M ρ ( N ρ ) Y θ ρ = ⊔ n λf θ → θ .f n ( )
We claimed above that unlike raw De Bruijn terms, term families can be constructed compositionally. This is done with the help of the following continuous functions, which generalize term constructors of E to Ê.

var = λv N .λn N .var v ∶ N → Ê app = λe Ê 1 .λe Ê 2 .λn N .app (e 1 (n)) (e 2 (n)) ∶ Ê → Ê → Ê lam = λf N → Ê .λn N .lam n (f (n)(succ n)) ∶ (N → Ê) → Ê
Using these extended constructors, one can define families of continuous functions, traditionally called reification (⇓ θ ∶ θ → Ê) and reflection (⇑ θ ∶ Ê → θ ).

⇓ o x = x ⇓ θ1→θ2 x = lam(λn N . ⇓ θ2 (x(⇑ θ1 ( var(n))))) ⇑ o e = e ⇑ θ1→θ2 e = λx θ1 . ⇑ θ2 ( app(e)(⇓ θ2 (x)))
For closed terms ⊢ M ∶ θ, the normalization-by-evaluation function can now be defined by setting nbe(M ) = ⇓ θ ( M )(0). In order to apply the same method to open terms Γ ⊢ M ∶ θ, where Γ = {x 1 ∶ θ 1 , . . . , x k ∶ θ k }, we need to build a canonical inhabitant of Γ by defining the canonical semantic environment ρ Γ ∶ Π xi∈Γ θ i , associating ⇑ θi (λ_ N .var (i -1)) ∈ θ i to any x i . This leads to a generalized variant of the normalization function, defined by:

nbe(M ) = ⇓ θ ( M ρ Γ )(k). ▸ Proposition 13. For any λ -term Γ ⊢ M in β-normal η-long form, nbe(M ) = rep(M ). For any λY -term Γ ⊢ M ∶ θ, nbe(M ) = ⊔ n rep(BT(M ↾ n)).
Proof. The first part is proved by induction on M . For the second part, we reason equationally as follows: nbe(M )

= ⇓ θ ( M ρ Γ )(k) (1)
= ⇓ θ (⊔ n M ↾ n ρ Γ )(k) (2)
= ⊔ n ⇓ θ ( M ↾ n ρ Γ )(k) (3)
=

⊔ n ⇓ θ ( BT(M ↾ n) ρ Γ )(k) (5)
= ⊔ n rep(BT(M ↾ n)) where (1) is by definition of NBE, (2)
is by induction on M from the definition of interpretation, (3) is by continuity of ⇓ θ and application. Since M ↾ n is a simply-typed λ -term, it has a normal form BT(M ↾ n) such that M ↾ n ≃ βη BT(M ↾ n). By soundness of the domain semantics, this implies that M ↾ n ρ = BT(M ↾ n) ρ and ( 4) is true. Finally, (5) follows from the first part. ◂

Internalization

Following Section 2, for any λY -term Γ ⊢ M ∶ θ, we define the syntactic NBE by snbe(M ) =↓ θ M * [↑ θi λ.(var i -1) x i ] k so that Γ rep ⊢ snbe(M ) ∶ o (↓ θ and ↑ θ are the terms defined in Section 2). In the remainder of this section we show the correctness of snbe, namely BT(snbe(M )) = ⊔ n rep(BT(M ↾ n)), by noting that snbe amounts to an internalization of the NBE procedure inside the λY -calculus, i.e., that the following triangle commutes.

λY snbe(-) nbe(-) ! ! λY BT(-)
/ / E To carry out the argument, below we introduce another interpretation of terms Γ rep , Γ ⊢ θ, written -, which will treat variables from Γ rep as constants. Accordingly, the sequents will be interpreted by a continuous function from Γ to θ , with Γ rep omitted. Similarly, the semantic environment for a context Γ rep , x 1 ∶ θ 1 , . . . , x k ∶ θ k is simply ρ ∶ Π xi∈Γ θ i . In the same vein, whenever we write Γ ⊢ M ∶ θ from now on, we will assume that none of the variables from Γ rep occurs in Γ (this does not affect the generality of our results, as free variables of a λY -term can be renamed to avoid clashes with Γ rep ). Below we let z range over the variables from Γ rep .

o = E x ρ = ρ(x) var ρ = λn E .var n θ → θ ′ = θ → θ ′ M N ρ = M ρ ( N ρ ) app ρ = λe E 1 .λe E 2 .app e 1 e 2 λx θ .M ρ = λa θ . M ρ⊕{x↦a} lam ρ = λn E .λe E .lam n e z ρ = z Y θ ρ = ⊔ n λf θ → θ .f n ( ) succ ρ = λn E .succ n
The interpretationsandare related by the following lemma, which is easily proved by induction. We applyto M ⋆ on the understanding that Γ ⊢ M ∶ θ implies Γ rep , Γ ⋆ ⊢ M ⋆ ∶ θ ⋆ and that Γ = Γ rep , Γ ⋆ . ▸ Lemma 14. For any type θ, θ = θ ⋆ . For any λY -term Γ ⊢ M ∶ θ and any semantic environment ρ ∈ Γ , we have M ρ = M ⋆ ρ . On the other hand,is related to Böhm trees by the following lemma. Proof. From the following calculations. BT(snbe(M ))

= snbe(M )

(2)

= ↓ θ M * [ ↑ θi λ.(var i -1) x i ] k (3) = ↓ θ ( M * xi↦ ↑ θ i λ.(var i-1) )( k ) (4)
= ⇓ θ ( M xi↦⇑ θ i (λ.(var i-1)) )(k)

= nbe(M ) We conclude this section with a discussion on the effect of the M ↦ snbe(M ) transformation on the order of terms (the order of a λY -term, written ord(M ), is the maximal order of the types of its subterms). We note that, given Γ ⊢ M ∶ θ, the term snbe(M ) is of order at most ord(M ) + 2, because it contains ↓ θ , which has type θ * → (o → o) of order ord(θ) + 2. However, as in Example 12, snbe(M ) can be simplified by one size-decreasing β-reduction step to M ′ of order ord(M ) + 1. Furthermore, if one is interested in obtaining an equivalent HORS then M ′ can be transformed into a HORS of order ord(M ) [START_REF] Salvati | Recursive schemes, Krivine machines, and collapsible pushdown automata[END_REF].

Generalization to PCF

Here we show that the methodology of the previous section can be applied to PCF [START_REF] Plotkin | LCF considered as a programming language[END_REF]. This brings us closer to realistic programs, which can branch on data values. PCF extends the λY -calculus in that the ground type o is replaced with the type of natural numbers, basic arithmetic and zero testing. It was designed to be Turing-complete, so in order to avoid obvious undecidability we focus on its finitary variants. In what follows we consider boolean PCF 2 in which o is the type of booleans, but it should be clear that the techniques extend to any finite ground type.

▸ Theorem 18. For any

PCF 2 term Γ ⊢ M ∶ θ, there is a level-2 λY -term Γ pcf ⊢ M rep ∶ o such that BT(M rep ) = ⊔ n rep(BT(M ↾ n)).
To construct M rep from M , we first apply the following syntactic transformation translating types and terms of PCF 2 to λY -terms, combining the operation (-) * on λY -terms defined in Section 2 with an elimination of booleans based on Church encodings.

B * = (o → o) → (o → o) → (o → o) tt * = λa o→o .λb o→o .a (θ ′ → θ ′′ ) * = (θ ′ ) * → (θ ′′ ) * ff * = λa o→o .λb o→o .b (if M then N 1 else N 2 ) * = λ → x → θ * .λa o→o .λb o→o .M * (N * 1 → x a b) (N * 2 → x a b)
where, in the last equation, N 1 and N 2 have type → θ → B. The translation (-) * can be extended to all the other term constructors in the obvious way. Note that, since this translation gives us a λY -term, we can already apply the transformation of Section 2 and obtain a λY -term generating the Böhm tree of M * . To get the PCF Böhm tree of M instead one can modify the ↓ θ , ↑ θ terms as follows.

↓ B = λx B * .x (λ.tt) (λ.ff ) ↑ B = λe o→o .λa o→o .λb o→o .λn o .if (e n) (a n) (b n) ↓ θ ′ →θ ′′ = λx (θ ′ →θ ′′ ) * . λv o . lam v (↓ θ ′′ ( x (↑ θ ′ λ.(var v)) ) (succ v) ) ↑ θ ′ →θ ′′ = λe o→o . λa (θ ′ ) * . ↑ θ ′′ ( λv o . app (e v) (↓ θ ′ a v) ) Assuming Γ = x 1 ∶ θ 1 , . . . , x k ∶ θ k , we can then set M rep =↓ θ M * [↑ θi λ.var i -1 x i ] k.
The notion of order on types and terms is generalised to PCF 2 by setting ord(B) = 0. As for λY , M rep can be simplified by one β-reduction step to M ′ of order ord(M ) + 2. M ′ can then be transformed into a HORS of order ord(M ) + 1 [START_REF] Salvati | Recursive schemes, Krivine machines, and collapsible pushdown automata[END_REF].

Conclusion

We have shown that faithful representations of η-long Böhm trees of arbitrary λY -terms and PCF Böhm trees of PCF 2 -terms can be generated by higher-order recursion schemes. We can use the result to reduce various decision problems related to the λY -calculus or PCF 2 to problems for higher-order recursive schemes.

The first class of problems to which the reduction technique can be applied are equivalence problems.

▸ Corollary 19. The following problems are recursively equivalent: HORS equivalence, Böhm tree equivalence in the λY -calculus, PCF Böhm tree equivalence in PCF 2 .

The decidability status of these problems is currently unknown, but they are known to be related to two other interesting problems: the equivalence problem for deterministic collapsible pushdown automata [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF] and contextual equivalence for PCF 2 -terms with respect to contexts with state and control effects (contextual equivalence for PCF 2 -terms with respect to purely functional contexts is undecidable, even without Y [START_REF] Loader | Finitary PCF is not decidable[END_REF]).

In a different direction, we can exploit the decidability result for MSO on trees generated by HORS [START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF] to decide a variety of properties of Böhm trees. Here the undecidability result for binders places a limit on the kind of binding-related information that can be captured by MSO on our representations. However, many interesting problems on Böhm trees still fall within the range of our representation.

▸ Corollary 20. The following problems are decidable for λY -and PCF 2 -terms: normalizability (is a given term equivalent to a Y -free term?), finiteness (is the Böhm tree/PCF Böhm tree finite, i.e. a λ /PCF 2, -term?), solvability (is the Böhm tree/PCF Böhm tree non-empty after leading abstractions?), prefix (does the Böhm tree/PCF Böhm tree have a given finite prefix?).

The results follow from the fact that all the relevant properties are expressible in MSO. Normalizability and solvability for the λY -calculus were already known to be decidable [START_REF] Statman | On the lambdaY-calculus[END_REF]. To the best of our knowledge, the other consequences are new. In future work, we would like to understand the exact complexity of these problems and see whether our results yield optimal bounds.

  Let us first make formal what we mean by MSO on Böhm trees with binders. ▸ Definition 5. A binding structure B = (S, →) is a labelled transistion system, namely a set of states S and a relation →⊆ S × L × S, where L is the set of labels L = N ∪ {λ}. For l ∈ L, we write a l → b for (a, l, b) ∈→. Every λ ∞ -term M defines a binding structure B(M ) in which the states are nodes in the syntax tree of M , a n → b holds if b is the n-th child of a and a λ → b expresses the fact that b is a binder-node λx and a an occurrence of x. The MSO formulas over binding structures are given as follows.

→

  are respectively the relational composition of e1 → and e2 → and the transitive closure of e →, both MSO-definable. The relations define the half-grid in the sense that for any

▸ Example 10 .

 10 Consider again the term M of Example 7. The binder-free representation of M 's Böhm tree can be captured as an open (infinite) term in context Γ rep , namely, M ∞ = lam 1 T (2), where

lam 1 (

 1 Y (λy. λv.app (var 1) (lam v (app (app (var 0) (var v)) (y (succ v))))) 2), the manually constructed term from Example 10.

▸ Lemma 15 .▸ Theorem 16 .

 1516 For any λY -term Γ rep ⊢ M ∶ o, we have M = BT(M ). Proof. Suppose first that Γ rep ⊢ M ∶ o is a λ -term in β-normal η-long form, i.e. M = BT(M ). Then M must be an applicative term built from , z, succ, var, lam and app. By induction on M it follows that M = M and, thus, M = BT(M ). Now consider arbitrary Γ rep ⊢ M ∶ o, and n ∈ N. By construction, M ↾ n is a λ -term. By normalization of the simply-typed λ-calculus, M ↾ n has a Böhm tree BT(M ↾ n) such that M ↾ n ≃ βη BT(M ↾ n). By soundness of the denotational model, it follows that M ↾ n = BT(M ↾ n) . By the first part above, we can deduce M ↾ n = BT(M ↾ n). The lemma then follows by continuity. ◂ Putting all the lemmas together, we arrive at our main result. For any λY -term Γ ⊢ M ∶ θ, BT(snbe(M )) = ⊔ n rep(BT(M ↾ n)).

( 6 )

 6 = ⊔ n rep(BT(M ↾ n)). (1) follows from Lemma 15, (2) and (3) from the definitions of snbe andrespectively, (4) is a consequence of ↓ θ =⇓ θ , ↑ θ =⇑ θ and Lemma 14. Finally, (5) follows from the definition of nbe and (6) from Proposition 13. ◂

Böhm Trees as Higher-Order Recursive Schemes 4.1 PCF 2 and PCF 2 Böhm trees PCF 2 types are defined by the grammar θ ∶∶= B θ → θ and terms are given by M, N ∶∶= tt ff if M then N 1 else N 2 x λx θ .M M N Y θ M . The following typing rules apply. Γ ⊢ tt ∶ B Γ ⊢ ff ∶ B

Acknowledgment. We would like to thank Sylvain Salvati for pointing out to us the undecidability argument for MSO on trees with binding. This research was conducted while the first author was in Cambridge, supported by the Advanced Grant ECSYM. The second author gratefully acknowledges the support of the EPSRC (EP/J019577/1).

For PCF 2 , the canonical forms that we wish to generate are PCF Böhm trees: they are (potentially infinite) trees generated by the rules displayed below.

Such trees were first introduced along with the game semantics for PCF [START_REF] Hyland | On Full Abstraction for PCF[END_REF][START_REF] Abramsky | Full abstraction for PCF[END_REF], serving as a syntactic counterpart to strategies. Later developments in game semantics [START_REF] Abramsky | Linearity, sharing and state[END_REF][START_REF] Laird | Full abstraction for functional languages with control[END_REF] showed that two terms of PCF have the same strategy, i.e. the same PCF Böhm tree, if and only if they are indistinguishable by evaluation contexts having access to computational effects such as state and control operators. This makes PCF Böhm trees a natural candidate for a representation of higher-order programs to be used for verification purposes, since purely functional programs are eventually executed in runtime environments that have access to such effects. We also consider the variant PCF 2, consisting of Y -free terms of PCF 2 , extended with a constant ∶ B. They are partially ordered by the obvious adaptation of the partial order ⊑ on λ -terms, still written ⊑. As before, this partial order extends to an ω-cpo on infinite terms of PCF 2, , referred to as PCF ∞ 2, . The operational semantics for PCF 2 for which PCF Böhm trees can be taken to be canonical representatives is obtained by adding the rules listed below to β, η and Y . For brevity, if M then N 1 else N 2 is written as if(M, N 1 , N 2 ). The rules are restricted to the cases where both sides typecheck.

We write ≃ PCF for the corresponding equational theory. For PCF 2, we also add the rule if( , N 1 , N 2 ) → . The following property can then be established by standard means.

To define Böhm trees of arbitrary PCF 2 -terms Γ ⊢ M ∶ θ, we define the nth approximant of M , written M ↾ n, by replacing fixpoint combinators Y θ with λf θ .f n ( θ ), yielding a term of PCF 2, . In the general case, the PCF Böhm tree is then defined by BT(M ) = ⊔ n BT(M ↾ n).

Representability

We would like to represent PCF Böhm trees of PCF