Taus Brock-Nannestad
email: taus.brock-nannestad@inria.frngue

Nicolas Guenot

Daniel Gustafsson

Computation in Focused Intuitionistic Logic

Keywords: F.4.1 [Mathematical Logic]: Proof theory, Lambda-calculus and related systems Intuitionistic Logic, Curry-Howard, Lambda-calculus, Focusing, Polarities, Evaluation Strategies, Abstract Machines Γ, x : ↓N, [N ] k [P] Γ, [P] Γ, [P] Γ, x : P, [N ]

We investigate the control of evaluation strategies in a variant of the λ-calculus derived through the Curry-Howard correspondence from LJF, a sequent calculus for intuitionistic logic implementing the focusing technique. The proof theory of focused intuitionistic logic yields a single calculus in which a number of known λ-calculi appear as subsystems obtained by restricting types to a certain fragment of LJF. In particular, standard λ-calculi as well as the call-by-push-value calculus are analysed using this framework, and we relate cut elimination for LJF to a new abstract machine subsuming well-known machines for these different strategies.

Focusing and Computation

Understanding the notion of computation has been a question of great interest to many logicians since the inception of the so-called Curry-Howard correspondence, contributing to the development of the functional paradigm, using expressive type systems, or the introduction of logic programming. The logical perspective on computation is now centered around a couple of results in proof theory, the most important ones being normalisation for natural deduction and focalisation in the sequent calculus. Normalisation provides an operational semantics of languages based on the pure λ-calculus, just as proof search in a focused sequent calculus gives the semantics of a logic programming language [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF].

Over the last decades, the "proofs-as-programs" approach has been extended from its original form in a natural deduction setting to sequent calculus systems [START_REF] Herbelin | A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure[END_REF]. This required a departure from the traditional syntax of the λ-calculus [START_REF] Barendregt | Lambda-terms for natural deduction, sequent calculus and cut elimination[END_REF], and lead to insights on various forms of computation [START_REF] Santo | The λ-calculus and the unity of structural proof theory[END_REF]. On another side, following the "proof-search-as-computation" idea, the advent of focusing [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF] as a technique stemming from the analysis of the sequent calculus through linear logic [START_REF] Girard | Linear logic[END_REF] provided clean logical foundations for logic programming, for linear logic as well as for more standard logics [START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF]. Over time, the scope of focusing has broadened, the role of the associated polarities has been investigated [START_REF] Laurent | Etude de la polarisation en logique[END_REF], and the [Copyright notice will appear here once 'preprint' option is removed.] perception of this result has shifted from a proof search technique to an important normal form in the sequent calculus and in other logical formalisms [START_REF] Brock-Nannestad | Focused natural deduction[END_REF][START_REF] Chaudhuri | The focused calculus of structures[END_REF].

The crucial observation at this point is that the variants of the λ-calculus using the sequent calculus formalism to provide some insights on reduction strategies are focused calculi [START_REF] Dyckhoff | LJQ: a strongly focused calculus for intuitionistic logic[END_REF][START_REF] Herbelin | A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure[END_REF] where a certain form of focusing constrains reduction. In such a calculus, only terms enforcing one particular strategy can be typed, and the corresponding proof system is a fragment of the focused system for intuitionistic logic. Our goal is to give a computational interpretation for (a variant of) the focused system LJF of Liang and Miller [START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF], and show how the resulting λ-calculus provides a means of fine-grained control of the reductions involved in the evaluation of λ-terms. In particular, we show that the λκ-calculus, which we introduce as a language of proof-terms for LJF, contains the standard call-by-name and call-by-value calculi, obtained from the fragments LJT and LJQ. The methodology we follow here has its importance: we wish to interpret LJF as a system entirely justified using proof-theoretical arguments, rather than an ad-hoc system for particular strategies. This approach confirms the two natural representations of the most standard strategies -CBN and CBV -in the focused type system, but it also reveals the tight connection between LJF and call-by-push-value [START_REF] Levy | Call-by-push-value: Decomposing call-by-value and call-by-name[END_REF], in which the two standard strategies can be embedded. The relation between CBPV and focusing was conjectured but still unclear: we establish it in details and discuss their differences.

The ability to control the reduction strategy of a term through dedicated operators, reflected at the level of types by the presence of explicit polarity shifts -the key ingredient in the focalisation result -is a striking example of double discovery. Indeed, the focusing technique was a rather syntactic artifact of linear logic that rose to the status of "éminence grise" in proof theory, while the call-by-push-value language stems from the thorough analysis of the semantics of the two major functional paradigms. Their convergence is a sign of their significance.

Moreover, we study the extraction of an abstract machine from the cut elimination procedure of a given focused proof system, and show how the procedures for the LJT and LJQ fragments of LJF yield essentially the most natural machines implementing CBN and CBV: the KAM [START_REF] Krivine | A call-by-name lambda-calculus machine[END_REF] and the CEK machine [START_REF] Felleisen | Control operators, the SECD-machine and the λ-calculus[END_REF]. Then, we describe an abstract machine implementing cut elimination in the LJF system and show how it relates to the CK-style machine defined in the literature for CBPV [START_REF] Levy | Call-by-push-value: Decomposing call-by-value and call-by-name[END_REF].

Figure 1.

Rules for the sequent calculus LJF and associated terms focused cut elimination procedure. We consider the extracted CBV and CBN machines and their relation to other machines. Then, Section 5 is devoted to the comparison between the λκ-calculus and CBPV, the key contribution being a bijection between the two calculi -this result crucially depends on the particular flavour of the LJF system presented in Section 2. We come there to the conclusion that CBPV corresponds to a specific form of LJF where maximal inversion is not enforced, called a weakly focused system. This correspondence relies on the bidirectional [START_REF] Cittadini | Normal natural deduction proofs (in non-classical logics)[END_REF] variant of the CBPV system, and it involves the introduction of delays to account for the ability to type λ-terms that are not η-long.

Related work. The impact of focalisation on the strategy used to evaluate terms has been mostly studied in the setting of classical logic, after the introduction of the λµ μ-calculus by Curien and Herbelin [START_REF] Curien | The duality of computation[END_REF] and later refined in [START_REF] Curien | The duality of computation under focus[END_REF]. The analysis of polarities in classical logic can be traced back to Girard [START_REF] Girard | A new constructive logic: Classical logic[END_REF], and the LKT and LKQ systems [START_REF] Danos | LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication[END_REF], precursors of the LJT and LJQ systems. Notice that studying directly the intuitionistic focused system LJF allows to clarify the picture, and demonstrates how types for values and computations in the λ-calculus differ in their polarities [START_REF] Zeilberger | On the unity of duality[END_REF]. On the purely logical level, our particular presentation of LJF relates to the structural approach to focalisation [START_REF] Simmons | Structural focalization[END_REF], and the question of polarity assigments in LJF studied in [START_REF] Nigam | Relating focused proofs with different polarity assignments[END_REF].

At the level of the λκ-calculus, the operations involved can be traced to interpretations of LJ [START_REF] Santo | Completing Herbelin's programme[END_REF] or CBPV [START_REF] Levy | Call-by-push-value: Decomposing call-by-value and call-by-name[END_REF]. A relation between sequent calculus systems and abstract machines has been investigated using the λµ μ framework [START_REF] Ariola | Sequent calculi and abstract machines[END_REF], and the connection leading from explicit substitutions -related to "cuts" in natural deduction -to abstract machines has been described from the untyped perspective in [START_REF] Accattoli | Distilling abstract machines[END_REF]. Defining an abstract machine is here presented as a process of extraction of information from a focused cut elimination procedure.

A Computational Interpretation of LJF

In this section we will describe a focused sequent calculus called LJF, with a few differences between our presentation and the original [START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF]. The idea of focusing is that a careful analysis of the properties of inference rules allows to classify them into two categories, one for fully invertible rules, called asynchronous, and one for partially invertible rules, which are called synchronous. It has been observed that these rules can be organised in a particular way inside any given proof -the result originated from linear logic [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF], but it has been generalised to many other logics. For more details about the intuitive interpretation of focusing, we refer the reader to one of the many descriptions available in the literature, see for example [START_REF] Simmons | Structural focalization[END_REF].

There are essentially three differences between the system we use here and the original version of LJF:

1. concerning polarities: in the original presentation of LJF, the syntax of formulas is unpolarised, although the idea of polarity is already present, and used for example in the rules initiating and finishing the synchronous phases -we choose to make it explicit using polarity shifts, which mediate between negative and positive formulas, 2. concerning maximal inversion: the original presentation of LJF enforces not only maximality of synchronous phases, it also has maximal asynchronous phases, using the explicit inversion context, while we drop this restriction to consider the weakly focused version of LJF, although the strongly focused variant is discussed in Section 6 -the computational behaviour of maximal inversion is currently unclear, 3. concerning initial rules: it is customary to have atomic initial rules in a focused calculus -one for negative atoms and one for positive atoms -but we observe that this is not necessary, and in particular one can prove from atomic initial rules the admissibility of the initial rules on shifts.

Remark 2.1. Beyond the question of the computational meaning of maximal inversion, enforcing such a structure in a natural deduction setting [START_REF] Brock-Nannestad | Focused natural deduction[END_REF] is difficult. Directly relating the "strongly" focused LJF to the weakly focused CBPV would be problematic due to the impedance mismatch between these systems.

As mentioned, the syntax of formulas in this variant of LJF is explicitly polarised, based on the following grammar:

P, Q ::= a + | ↓N M , N ::= a -| P ⊃ N | ↑P
and its inference rules are shown above in Figure 1. In the calculus presented there, rules are annotated with terms and sequents take the form of typing judgements, where Γ and ∆ denote sets of labelled formulas. There are three forms of judgements in this system, that we will now simply call LJF:

Γ t : N asynchronous Γ , [N ] k : M left-synchronous Γ p : [P]
right-synchronous

In the synchronous phase, the formula written inside brackets is said to be "under focus". By inspection of the inference rules, it is clear that foci must always be the principal formulas of the conclusions of the rules they appear in. Furthermore, this focus is passed on to the subformulas of the focused formula. In this way, focusing on a given formula ensures that it and its subformulas are decomposed in a maximal chain of inference steps. Conversely, in the asynchronous phase, formulas can be decomposed in any order. Choosing which formulas may be focused and when the synchronous phase ends is made explicit in the rules introducing the polarity shifts ↓ and ↑.

Since we only consider a weakly focused variant of LJF in this paper, the number of cut rules is smaller than in [START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF]. Additionally, we leave out entirely unfocused cuts (the Cut + and Cut -of [START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF]), as they are in fact not needed for the cut elimination proof, and can easily be recovered as corollaries after the fact. Every cut rule in our system thus has the property that the cut formula appears under focus in one of the two premises.

Names of inference rules follow a uniform scheme. For the core cut-free calculus, the first letter indicates whether the principal formula is related to focusing, blurring, or implication. The second letter indicates whether the principal formula is introduced on the left or the right. For the cut rules, we distinguish between the head cuts, where the principal reductions take place, and the focused cuts which handle all the commutative cases. Note that these can be distinguished by whether the conclusion contains a focus or not. Finally, for each of the cut rules, it is the case that the cut formula is focused in exactly one of the two premises. The l or r annotation indicates the premise that is not focused, and thus the premise which will be decomposed during cut reduction.

Judgments are annotated with terms of the λκ-calculus, an extension of the λ-calculus based on the following grammar:

t, u ::= λx.t | x k | p | t k | p to x.t k, m ::= | p :: k | κx.t | k @ m | p to x.k p, q ::= x | t | p to x.q (1)
Note that there is a very tight correspondence between the proof terms and the derivations of LJF. In a sense, the syntax of proof terms was extracted from the calculus by a recipe we will sketch now. The basic observation is the following: the focusing discipline in many cases obviates the need for variable binding in the proof terms. The prototypical example of this would be the il rule from the unfocused LJ:

Γ , f : P ⊃ N t : P Γ , f : P ⊃ N , x : N u : M il - --------------------------------------------------------------------------------------------------------- Γ , f : P ⊃ N let x = f t in u : M

In the focused setting, the second premise must decompose the hypothesis x immediately, and it is therefore not necessary to introduce an explicit binder for x. Consequently, the proof term assignment for this rule in LJF is simply: ----------------------------------------------------------- Γ , [P ⊃ N ] p :: k : M According to this methodology, a binder should only occur when decomposition is not immediately forced. This explains why only bl and ir involve binders, while hcl and fcl do not. The intuitive meaning of the λκ-calculus will be discussed later in this section, but we first concentrate on the basic properties of the LJF system shown in Figure 1. First, when comparing it to the usual, unfocused system LJ for intuitionistic logic, we need to define E(-) to be the following polarity erasure function, mapping a polarised formula to its unpolarised counterpart:

Γ p : [P] Γ , [N ] k : M il -
E(a -) = a E(↑P) = E(P) E(a + ) = a E(↓N ) = E(N ) E(P ⊃ N ) = E(P) ⊃ E(N )
Note that an unpolarised formula may be polarised in many different ways, by choosing the polarity of atoms, or by inserting redundant polarity shifts. In particular, we have E(↑↓N ) = E(N ) and E(↓↑P) = E(P), and this enables a more fine-grained control of the order in which formulas must be decomposed, since phases are controlled by polarity shifts.

The most important property of focusing is that it is sound and complete, regardless of the aforementioned choice of one particular polarisation. Following [START_REF] Simmons | Structural focalization[END_REF], we will state this result in terms of erasure.

Theorem 2.2. Given any negative formula N , the sequent E(N ) is provable in LJ if and only if N is provable in LJF.

Proof. The first direction follows immediately from the fact that the rules of LJF are just more restricted versions of the rules of LJ. To show completeness of LJF, one may show that the all usual unfocused inference rules of LJ are admissible in LJF. This is straightforward once cut rules have been proven admissible in the focused system [START_REF] Simmons | Structural focalization[END_REF]. Alternatively, the result may be established by the "grand tour" strategy, as seen for example in [START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF].

We now turn to the most important result concerning the LJF focused system in this paper, describing the dynamics of proofs. Proof. We proceed by lexicographical induction over the structure of the cut formula and of the premises of the given cut. We assume the two given input derivations to be cut-free, corresponding to a strategy reducing the topmost cuts in the given derivation. Note that because we are working with the focused versions of the cut rule, every cut may be reduced by only considering cases on one of the premises, specifically the premise where the cut formula is not under focus. We show here only a few of the cases of the cut elimination argument -the full proof may be found in the appendix: ---------------------------- Γ p : ↑P E Γ , x : P t : M bl - ---------------------------------------- Γ , [↑P] κx.t : M hcl - ------------------------------------------------------------------------------- Γ p (κx.t) : M Γ p to x.t : M by hcr on (P, D, E).

D Γ p : [P] fr -
• Case hcr: if the second premise ends in fl then it is the principal case for positive shift, and the reduction is: ------------------------------------------------------ Γ , x : ↓ M x k : N hcr - ------------------------------------------------------------------------------------------------------- Γ u to x.(x k) : N

D Γ u : M fr -------------------------------------------- D :: Γ u : [↓ M ] E Γ , x : ↓ M , [M ] k : N bl -
E :: Γ , [M ] u to x.k : N by fcr -on (↓ M , D , E), Γ u ( u to x.k) : N by hcl on (M , D, E ).
and all other cases can be treated in a similar way.

From this cut elimination theorem, we now extract a system of reduction rules on λκ-terms, by considering each case as one rewrite on proof objects: where, in the reductions where p appears we have a proviso that states p should not be a variable. The reason for this is that we wish to avoid the aliasing of names, created when bindings are chained so that a value is pointed to by several names.

(λx.t) (q :: k) → (q to x.t) k q (κx.t) → q to x.t (x k) m → x (k @ m) @ m → m (q :: k) @ m → q :: (k @ m) (κx.t) @ m → κx.(t
Computational interpretation. Such a rewrite system for λκ, extracted from the cut elimination proof, specifies the intuitive meaning to be attributed to each construct of the calculus. The symbols λ and κ as well as the to construction are binding variable names. The calculus obeys the laws of α-conversion, and binders are thus essentially treated as in the pure λ-calculus. An important distinction to be made in λκ is that t denotes a term, having the meaning of a computation, while p denotes a value, which is the result of a computation. Finally, k represents a continuation.

Some of the constructs in λκ are standard operations from the λ-calculus. Others are variations, such as the application (x k), that can be thought of as a continuation k -or context -waiting for a function to be plugged in the place of x. The term k can be seen in most cases as a list of arguments given to the function plugged for x, and after plugging we obtain a proper application t k. Moreover, k @ m represents here the concatenation of two list of arguments, or the composition of two continuations. We can observe how reduction defines the use of a list of arguments, in the rule:

(λx.t) (q :: k) → q to x.(t k) Moreover, values can be bound to names, using the binder to which acts as an explicit substitution of a value p for a variable x. In the minimal system we are considering, values can be variables and are otherwise formed by placing a term in a thunk, that should be seen as delayed computations. The thunks can be forced by applying them to a list of arguments:

u to x.(x k) → u ( u to x.k)
where a copy of u is passed on to the list, which may contain occurrences of x. The two remaining constructs are perhaps the most surprising ones, since they directly affect the control flow of the term. A term p is indeed a computation that has finished, and returns a value, so that it releases control of the computation. The κx.t construction is the continuation that can then take control, binding the result p to the name x and starting computation t, as expressed in the rule: q (κx.t) → q to x.t which already appeared in [START_REF] Santo | Completing Herbelin's programme[END_REF], although its typing there is not controlled by shifts and it requires no return construct to interact with. Note that substitutions are here eagerly decomposed, and propagated. We now turn to the properties of well-typed λκ-terms, the usual ones being simple corollaries of cut elimination.

Corollary 2.4 (Subject Reduction

). If Γ t : N and t → u then we also have Γ u : N .

Proof. Each reduction corresponds to one of the cases of the cut elimination argument, so the result is immediate.

Moreover, cut elimination implies that reduction on well-typed terms is well-behaved, and leads to normal forms, which are terms typeable without the cut rules.

Corollary 2.5 (Normalisation).

For a λκ-term t, if Γ t : N there exists a normal term u such that Γ u : N and t → * u.

As mentioned before, the ways in which a cut might be reduced are limited by the fact that the cut formula must be under focus in either the first or the second premise. This restriction yields cut elimination steps that are highly reminiscent of the steps used in the tq-protocol in [START_REF] Danos | A new deconstructive logic: Linear logic[END_REF]. A slightly more permissive variant of this protocol [START_REF] Santo | Delayed substitutions[END_REF] may be summarised as follows:

1. if the cut formula is not principal in the second premise of the cut we wish to reduce, we permute the cut into this premise, 2. if the cut formula is not principal in the first premise of the cut, then we permute it into the first premise, and 3. if the cut formula is principal in both premises, then we reduce it as a principal cut.

The main difference between these cut elimination procedures is that when the first two cases are reduced in the tq-protocol, the cut must be permuted as far up as possible in one step. In contrast, we describe reductions as small steps, and more importantly we do not consider cases where a cut permutes above some other cut. As we will see in Section 4, it is necessary to introduce such permutations between cuts to construct an abstract machine for LJF, but the proof of normalisation is more challenging. Note that λκ cannot simulate a unique β step separately from other steps, since it is based on the syntax of the sequent calculus. However, we will see how it can implement reduction in other ways, and we observe that its reduction system is confluent, since it is left-linear, and it has no critical pair -under the proviso on variables applicable to the rules shown in [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF]. A particular interest of λκ is that it has two remarkably well-behaved fragments that correspond to the standard strategies used to reduce λ-terms.

Call-by-name and Call-by-value in LJF

In order to illustrate the expressivity of λκ and of the type system obtained from LJF, we consider the two evaluation strategies in the λ-calculus from which the two major lazy and strict paradigms of functional programming are derived. As expected, LJF introduces a uniform treatment of these systems that matches the standard theories developed for these languages.

Call-by-name. The simplest strategy in the λ-calculus is to use β repeatedly until a normal form is reached, disregarding the shape of subterms. This is normally done following an outermost order, and disallows reduction in the argument of an application. This reduction strategy can be enforced by considering the type system shown in Figure 2, based on the LJT system. The resulting λ-calculus allows the application of a term to a list rather than a single argument, based on the grammar:

t, u ::= x k | λx.t | t k | t[u/x] k, m ::= | u :: k | k @ m | k[u/x] ax --------------------------- Γ , [a] : a Γ u : A Γ , [B] k : C il ---------------------------------------------------- Γ , [A ⊃ B] u :: k : C Γ , x : A, [A] k : B foc ----------------------------------------- Γ , x : A x k : B Γ , x : A t : B ir ----------------------------------- Γ λx.t : A ⊃ B Γ t : A Γ , [A] k : B hc --------------------------------------------------- Γ t k : B Γ , [B] k : A Γ , [A] m : C fhc ---------------------------------------------------------------- Γ , [B] k @ m : C Γ u : A Γ , x : A t : B mc ------------------------------------------------------ Γ t[u/x] : B Γ u : A Γ , x : A, [B] k : C fmc ----------------------------------------------------------------- Γ , [B] k[u/x] : C Figure 2.
Rules for the sequent calculus LJT and associated terms

This type system was introduced in [START_REF] Herbelin | A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure[END_REF] as the first λ-calculus isomorphic to a sequent calculus. In LJT, the hc cut represents a β-redex, while reductions of fhc are simply administrative steps. Remaining cuts embody the substitution process. Cut elimination induces the following reductions, known to be call-by-name:

(λx.t) (u :: k) → t[u/x] k (x k) m → x (k @ m) @ m → m (u :: k) @ m → u :: (k @ m) (λz.t)[u/x] → λz.t[u/x] (x k)[u/x] → u k[u/x] ( y k)[u/x] → y k[u/x] [u/x] → (t :: k)[u/x] → t[u/x] :: k[u/x] (3)
The LJT proof system can be seen as a fragment of LJF through a typeability-preserving translation of terms into λκ. The key idea is that the argument of a function needs to be placed into a thunk, to prevent reduction. This is consistent with the fact that u to x.t essentially performs in λκ the substitution of u for x into t. The translation is based on most LJT reductions appearing in LJF. Definition 3.1. The translations T t (•) and T k (•) of λ-terms into λκ-terms are given by the following equations:

T t (x k) = x T k (k) T t (λx.t) = λx.T t (t) T t (t k) = T t (t) T k (k) T t (t[u/x]) = T t (u) to x.T t (t) T k (k[u/x]) = T t (u) to x.T k (k) T k (k @ m) = T k (k) @ T k (m) T k (u :: k) = T t (u) :: T k (k) T k ( ) =
This translation is mostly homomorphic, and it reflects the simplicity of the translation necessary at the type level:

T a = a - T A ⊃ B = ↓T A ⊃ T B
where all formulas are made negative by introduction of a positive shift on the left of implications to account for the positive formula expected in LJF. We can now extend the translation to contexts in the obvious way, translating each formula in a given Γ separately, and prove that the translation preserves typeability.

Theorem 3.2. The translations T t (•) and T k (•) are type-correct:

(i) if Γ t : A then ↓T Γ T t (t) : T A (ii) if Γ , [B] k : A then ↓T Γ , [T B ] T k (k) : T A Proof.
By mutual induction on the derivation. We only show the case for the hcl cut t k, others are treated similarly:

E :: T Γ T t (t) : T N by induction, F :: T Γ , [T N ] T k (k) : T M by induction, T Γ T t (t) T k (k) : T M by hcl on E,F.
Observe that inside of λκ, it is difficult to separate the LJT fragment by looking only at the types of terms. Indeed, a term with a type in the image of our translation might contain a cut on a formula outside of this fragment. We now consider the dynamics of λ and prove that reduction in this calculus is simulated through reduction in λκ, after applying the translation. Theorem 3.3. For any t and u in λ, if t → u then T t (t) → + T t (u).

Proof. By inspection of the reduction rules of λ and of the result of the translation T t (•) -all cases appear in the appendix.

Call-by-value. The second evaluation strategy commonly used in functional programming states that the β rule should only be applied when the argument is a value -a piece of code that has been fully reduced. In practice, this is restricted to weak reduction, where no reduction is performed under an abstraction, so that the term λx.t is considered a value. This implies some form of outermost reduction, but there is a choice between a left-to-right and a right-to-left order of evaluation when a term is applied to several arguments. This strategy has been implemented as a λ-calculus typed with the sequent calculus LJQ, as shown in Figure 3. The key construct here is the generalised application, t[z = x u] similar to the let binding used by Moggi [START_REF] Moggi | Computational λ-calculus and monads[END_REF] and it leads to the representation of CBV in [START_REF] Curien | The duality of computation[END_REF]. This form of application has already been investigated in the context of computational interpretations of LJ [START_REF] Joachimski | Standardization and confluence for a lambda calculus with generalized applications[END_REF]. The grammar of this λq-calculus is:

t, u ::= p | p to x.t | t[z = x p] | t[u/x] p, q ::= x | p to x.q | λx.t
where pto x is an operation allowing the binding of a value, while the substitution of any non-value term is performed by [u/x], representing the strict substitution never pushed until u is turned into some value and a binding is created. In LJQ, the cuts follow the same scheme of head-cuts and mid-cuts as in LJT, but there is no focused mid-cut. Rewritings resulting from cut elimination in LJQ correspond to a fragment of the reduction system of LJF -if we follow the scheme described in Section 2, although the system of [START_REF] Dyckhoff | LJQ: a strongly focused calculus for intuitionistic logic[END_REF] is quite different, in part due to modifications meant to prove a result of strong normalisation for the calculus. Our rules for λq are:

z to x.t → t{z/x} a to x. p → a to x.p a to x.t[z = w p] → (a to x.t)[z = w (a to x.p)] a to x.t[z = x p] → (a to x.t)[(a to x.p) to y.u/z] z to x.p → p{z/x} a to x.x → a a to x.z → z a to x.(λz.t) → λz.(a to x.t) t[ p /x] → p to x.t t[v[z = w p]/x] → t[v/x][z = w p]
where a always denotes the abstraction λ y.u, a proviso reflecting the fact that in LJQ, abstraction is made into a value by placing it inside a thunk. In general, this system is obtained by translation, originated in the embedding of the CBV implication in LJF using polarity shifts. ----------------------------------------------------- Γ t[u/x] : B (no focused mid-cut) Figure 3. Rules for the sequent calculus LJQ and associated terms Key ideas are the use of a continuation binder κ to translate a term under an application, and to place functions in thunks.

ax ----------------------------------- Γ , x : A x : [A] Γ , x : A t : B ir ---------------------------------------- Γ λx.t : [A ⊃ B] Γ p : [A] foc ---------------------- Γ p : A ∆ p : [A] ∆, z : B t : C il ------------------------------------------------------------------------- ∆ = Γ , x : A ⊃ B t[z = x p] : C Γ p : [A] Γ , x : A t : B hc ----------------------------------------------------------- Γ p to x.t : B Γ p : [A] Γ , x : A q : [B] fhc ---------------------------------------------------------------- Γ p to x.q : [B] Γ u : A Γ , x : A t : B mc -
Definition 3.5. The translations Q t (•) and Q v (•) from λq to λκ are given by the equations:

Q t ( p ) = Q v (p) Q t (p to x.t) = Q v (p) to x.Q t (t) Q t (t[u/x]) = Q t (u)(κx.Q t (t)) Q t (t[z = x p]) = x (Q v (p) :: κz.Q t (t)) Q v (p to x.q) = Q v (p) to x.Q v (q) Q v (λx.t) = λx.Q t (t) Q v (x) = x
This translation is slightly more complex than the one for LJT, as it involves the introduction of shifts in two positions when translating an implication at the level of types:

Q a = a + Q A ⊃ B = ↓(Q A ⊃ ↑Q B )
in order to turn subformulas of the original formula into positive formulas. In the case of a sequence of implications, for example in a ⊃ (b ⊃ c), this will introduce a delay on the right of implications, as seen in ↓(a ⊃ ↑↓(b ⊃ ↑c)), and this corresponds to the loss of focus in the premise of the right implication rule, reflecting the forceful integration of λx.t in the grammar of values. We now prove that the translation preserves typeability, as in LJT.

Theorem 3.6. The translations Q t (•) and Q v (•) are type-correct:

(i) if Γ t : A then Q Γ Q t (t) : Q A (ii) if Γ p : [A] then Q Γ Q v (p) : [Q A ]
Proof. By mutual induction on the derivation. We show the case for il, that is t

[z = x p] where k = Q v (p) :: κz.Q t (t) so that we have Q ∆ = Q Γ , x : ↓(Q A ⊃ ↑Q B ))
, and:

E :: Q ∆ Q v (p) : [Q A ] by induction, F :: Q ∆ , z : T B Q t (t) : Q C by induction, F :: Q ∆ [↓Q B ] κz.t : Q C by bl on F, F :: Q ∆ [Q A ⊃ ↓Q B ] k : Q C by il on E,F , Q ∆ x k : Q C by fl on F .
The mc cut in λq is a β-redex, and therefore studying which reduction equations it satisfies, we can learn that this system is call-by-value. The main rule is t[ p /x] → pto x.t which will only apply if the first premise is a value. Reading hc cuts as explicit substitutions, this is the rule that we expect for CBV. Because the first premise of the hc cut is a value, this guarantees that we will only substitute values in a term, and not other terms. Once again, we can prove that λκ simulates reduction in this calculus.

Theorem 3.7. For any t and u in λq

, if t → u then Q t (t) → + Q t (u).
Proof. By inspection of the reduction rules of λq and of the result of the translation Q t (•) -all cases appear in the appendix.

Evaluation Strategies and Abstract Machines

In practice, the functional programming languages using lazy and strict evaluation -based on CBN and CBV respectively -behave differently, and use implementations specific to their evaluation strategies. A detailed account of the operational semantics of a language is specified by its abstract machine: it is the theoretical representation of the code implementing an interpreter. At this level, strategies appear clearly and the transitions of two given machines can be compared intuitively -one could say that the meaning of a strategy is revealed by its abstract machine.

The assumption of this section is that since LJF can shed light on reduction strategies as a type system, it should already contain all the information needed to define an abstract machine for the strategies it can encode. We present here a recipe for building an abstract machine from the cut elimination procedure defined for a focused system.

Focused cuts and evaluation order. Given a focused sequent calculus, there is a simple methodology to follow when designing a cut elimination procedure based on rewrite rules: the reduction of a cut should be driven by the bottom rule in the premise where the cut formula appears unfocused. This uniquely identifies the locus of reduction, as opposed to the situation in an unfocused calculus. This is a requirement for the definition of an abstract machine, which is essentially a fully deterministic procedure for weak normalisation.

Following this idea, we have to consider which cut should be picked first for reduction. A machine takes a term as input and proceeds by decomposition of its structure: it is therefore natural to opt for an outermost reduction, where the bottom cut in a given proof is decomposed -more precisely, an abstract machine will typically implement a weak form of reduction, and thus the last rule in the proof should be a cut for any reduction to happen. In this situation, the order of reduction is deterministically specified by the aforementioned principle. But what should happen if the rule above the targeted premise of this cut is itself a cut? Nowhere in our cut elimination proof have we allowed two cuts to permute, and this would not even be a solution since this could never yield a terminating procedure. Logically, we are forced to consider the two cuts as a block, and by induction we observe that in general, the bottom of a proof during reduction will form a trunk of various cut instances stacked one above the other, and the reductions will happen at one of the leaves of this subtree.

Cut spines. Fortunately, a trunk of cuts need not be described in an abstract machine in an unspecified form: most cuts permute with other cuts and the task of designing the machine thus boils down to the specification of a certain normal form of cut trunks that will be interpreted as a machine architecture. We consider to this end cut spines, sequences of cuts stacked together.

There are two dual notions of cut spines: in a left spine, another smaller left spine appears in the left premise of a cut, whereas in a right spine the smaller spine appears in the right premise. We can describe these as lists of proofs, where the element at a node is either the right or the left premise. The topmost cut in a spine has one premise "outside of the list", and this proof can be viewed as an annotated empty list -we call it the target of a spine. We can then write

F[E n , • • • , E 1 ] and [E 1 , • • • , E n ]
F for left and right spines respectively. For example, we can see the proof: -------------------------------------------------------

G :: Γ L F :: Γ , [L] M --
- Γ M E :: Γ , [M ] N --------------------------------------------------------------------------- Γ N 6 2015/5/28

TJAM (call-by-name machine)

QJAM (call-by-value machine) -------------------------------------------------------------------------------------------Γ , x : P N -------------------------------------------------------------------------------------------Γ N is the right spine [E, F]G. Although one can use other groupings of cuts to organise the cut trunk at the bottom of a proof, these patterns will be the basic bricks for building our machines.

〈 e | λx.t | u[g] • c 〉 → 〈 e, x : u[g] | t | c 〉 〈 e, x : t[g] | x k | c 〉 → 〈 g | t • | k[e, x : t[g]] + c 〉 〈 e | t k | c 〉 → 〈 e | t • | k[e] + c 〉 〈 e | t b | [g] + c 〉 → 〈 e | t | b{c} 〉 〈 e | t b | (u :: k)[g] + c 〉 → 〈 e | t b • u[g] | k[g] + c
terminal configuration: 〈 e | λx.t | • 〉 〈 e | p | x.t[g] • c 〉 → 〈 e | p x.t[g] | c 〉 〈 e | t[z = x p] | c 〉 → 〈 e | p y.u[ f ] | z.t[e] • c 〉 (x : (λ y.u)[ f ] ∈ e) 〈 e | p to x.t | c 〉 → 〈 e | p x.t[e] | c 〉 〈 e | x z.t[g] | c 〉 → 〈 f | λ y.u z.t[g] | c 〉 (x : (λ y.u)[ f ] ∈ e) 〈 e | λx.u z.t[g] | c 〉 → 〈
Stacks and environments. We can make one step further in the definition of the machines by observing different properties of left and right spines. The left premise of intuitionistic cuts has the cut formula in the right-hand side, and therefore they can never permute above any other cut in this premise. As a consequence, the elements of a left spine cannot be exchanged: their order is fixed and they really form a list. Conversely, cuts can permute along their right premise provided there is no actual dependency of a premise on the cut formula, and hence the elements of a right spine can be exchanged under that condition.

This leads us to the definition of two data structures commonly used in abstract machines: stacks and environments. A left spine can be used as a stack, while right spines in which all elements are independent proofs can be seen as an environment. In practice, it is convenient to consider all elements of an environment closed, which corresponds to proofs of sequents with the left-hand side empty. Note that in a right spine, the target proof has access to all cut formulas, each of them being bound to a name if not focused, and present in the left-hand side of the topmost right premise. A term reduced against some stack will thus be the target of a left spine, and the target of a right spine if reduced in an environment -we can easily extend the notion of target so that a term can be viewed on top of both a stack and an environment.

Program and machine syntax. When defining a machine for a λ-calculus with a focused type system, the language of programs is given, it is that of terms in this calculus. However, not all cuts should be included in the language, but rather only head cuts that are used to type a computation. Any other cut has a bureaucratic meaning, appearing as byproduct of elimination of head cuts: the extra cuts are the logical counterpart of the machine architecture, and they translate into particular machine configurations. In LJF, for example, only hcl and hcr are unfocused head cuts, and in LJT and LJQ only hc cuts are. Note that head cuts belong to the syntax of the language but also translate to machine configurations, as they get integrated into the cut trunk during reduction:

machine syntax extra cuts basic rules head cuts program syntax

whereas extra cuts appear by reduction inside the cut trunk and are therefore always part of the representation of the machine architecture -their reduction represents implementation details of the abstract machine.

The protocol to follow in the creation of an abstract machine for a given focused sequent calculus is in the end quite mechanical, as it consists essentially in the identification of a normal form for trunks of cuts, equivalent to the definition of an architecture for the machine, usually based on standard data structures such as environments and stacks. The rest is constrained by the logical system and its cut elimination procedure. We can now turn to the definition of a machine for λκ and its fragments, following these principles to design it on logical grounds.

Data structures for LJF. In the particular situation of this system, environments are built from value bindings and we will consider all elements of an environments to be closed. This can be achieved by associating to each element a local environment to close its free variables. Therefore, the environments we use are a recursive data structure. Moreover, we need lists containing values and continuations that are also closed with local environments. In precise terms, the grammar of lists and environments is:

c, d ::= • | p[e] • c | (x.t[e]) • c e, f , g ::= • | e, x : p[g]
This language is used to describe the architecture of a machine, but all of these constructs have a representation in terms of the λκ-calculus. The translation is the following: where r represents an object that is either t, q or k. Note that in the construction (x.t[e]) • c, the x is not bound in c, so that this translation into λκ does not exploit the full scope of κx. We need to add the following reductions to the rewrite system:

(t m) k → t (m @ k) p to x.(t k) → (p to x.t) (p to x.k) p to x.(q to y.r) → (p to x.q) to y.(p to x.r) (4)
where x ∈ fv(q) and r can be have the shape of either t, p or k, so that some cuts can be permuted without looping. This is necessary to implement on λκ-terms the behaviour of the sequences and environments. These reductions participate in the maintenance of the encoding in λκ of a machine configuration.

Building CBN and CBV machines. Based on ideas described above, we define abstract machines, starting with LJT. The TJAM shown in Figure 4 is created by adding to the λ system the first two rules of (4) and defining machine configurations that support the kind of cuts appearing in LJT. For this, we need to handle a part of context as a difference list, which is just a list denoted by b where an element x is added to the tail -we write b • x for this operation. Moreover, we denote by b{c} the operation producing a list by plugging a list c as the tail of b. We can now describe the two kinds of configurations defining the TJAM architecture.

〈 e | t | c 〉 ( t[e] e ) c c 〈 e | t b | k[g] + c 〉 ( t[e] e ) b{ k[g] e @ c c } c
The first kind of configuration is used to reduce terms, and the second is only necessary to normalise the structure holding lists of arguments. From the transitions in Figure 4, we see that the TJAM is essentially the KAM [START_REF] Krivine | A call-by-name lambda-calculus machine[END_REF], extended to handle lists of arguments and with some explicit mechanism to normalise stacks -it is not needed in the original KAM, since it never pushes more than one argument at a time on the stack. Remark 4.2. The abstract machines we consider here are extremely detailed, and one might wonder if this level of precision is useful. In particular, the bureaucratic reductions maintaining the encoding of configurations could be factored out and made silent. However, it is always possible to make a machine more implicit if it represents all the details, whereas in other direction one would have to recover the precise behaviour of cut elimination that lead to the design of a particular machine. For example, stack normalisation in the TJAM can be made implicit, so that only a single kind of configuration is needed. If we consider the terms encoding pure λ-terms in λ, we observe that the machine transitions are exactly the ones defining the KAM:

〈 e | λx.t | u[g] • c 〉 → 〈 e, x : u[g] | t | c 〉 〈 e, x : t[g] | x | c 〉 → 〈 g | t | c 〉 〈 e | t (u :: ) | c 〉 → 〈 e | t | u[e] • c 〉
〈 e | t | c 〉 c{ t[e] e } c 〈 e | p x.t[g] | c 〉 c{ p[e] e to x. t[g] e } c
This machine is quite different from the TJAM, as it is based on a left spine of mc cuts, representing the stack c of a configuration. It is built as opposite of the TJAM, and although it is slightly more complex, one can observe the similarity to the CEK machine [START_REF] Felleisen | Control operators, the SECD-machine and the λ-calculus[END_REF]. Also, the reduced cut is not at the bottom of the proof anymore, but at the other end of the spine. The principle of its mechanism is that only computed values can be pushed in the environment, leading to a CBV reduction.

Multi-strategy machine. Following the same methodology, we now derive a machine for the full λκ-calculus, based on the cut elimination proof for LJF from Section 2. This machine is slightly more complex that the previous ones, with three configurations.

Definition 4.4 (FJAM). The configurations of the FJAM are:

〈 e | t | c 〉 ( t[e] e ) c c 〈 e | t b | k[g] + c 〉 ( t[e] e ) b{ k[g] e @ c c } c 〈 e | p x.t[g] | c 〉 ( p[e] e to x. t[g] e ) c c
The implementation of this machine is quite similar to that of the TJAM and the QJAM, but it unifies them by having all of their modes of evaluation. The transitions for this machine are shown in Figure 5: we can see that most of the transitions are reminiscent of either one of the previous machines. It is also interesting to see how a transition is represented in the term implementation. Consider for example these reductions:

(λx.t)[e] (p[g] :: k) → (p[g] to x.t[e]) k ( u [e] to z.t[g]) k → t[g, z : u [e]] k
expressed in terms of environments, and corresponding to the second and last transitions respectively. The basic idea of the FJAM is to let the control flow be exchanged by the operators related to a polarity shift. This illustrates how focusing provides explicit mechanisms for influencing the reduction strategy. The TJAM machine can be emulated inside of the FJAM machine, this will be proved by translating TJAM machine configurations into FJAM configurations, in such a way that reduction is preserved by the translation. This works by mapping terms of LJT to terms of LJF and preserving the invariant that all the values in both the context and environment are thunks. The individual components of a TJAM machine will be translated into a FJAM machine component in the following way:

FJAM (multi-strategy machine)

〈 e | p | x.t[g] • c 〉 → 〈 e | p x.t[g] | c 〉 〈 e | λx.t | p[g] • c 〉 → 〈 g | p x.t[e] | c 〉 〈 e, x : t [g] | x k | c 〉 → 〈 g | t • | k[e, x : t [g]] + c 〉 〈 e | t k | c 〉 → 〈 e | t • | k[e] + c 〉 〈 e | p to x.t | c 〉 → 〈 e | p x.t[e] | c 〉 〈 e | t b | [g] + c 〉 → 〈 e | t | b{c} 〉 〈 e | t b | (p :: k)[g] + c 〉 → 〈 e | t c • p[g] | k[g] + c 〉 〈 e | t b | (κx.t)[g] + c 〉 → 〈 e | t | (b • (x.t[g])){c} 〉 〈 e, x : p[ f ] | x z.t[g] | c 〉 → 〈 f | p z.t[g] | c 〉 〈 e | u z.t[g] | c 〉 → 〈 g, z : u [e] | t
T e • = • T e e, x : t[g] = T e e , x : T t (t) [T e g ] T c • = • T c u[g] • c = T t (u) [T e g ] • T c c T c k[e] + c = T k (k)[T e e ] + T c c
Then, a TJAM configuration translates to a configuration of the FJAM by applying the translation to each component, pointwise:

FT 〈 e | t | c 〉 = 〈 T e e | T t (t) | T c c 〉 FT 〈 e | t c | d 〉 = 〈 T e e | T t (t) T c c | T c d 〉 Theorem 4.5 (TJAM in FJAM). Given any two TJAM configurations U and V such that U → V , we have FT U → + FT V .
Proof. By case analysis on the TJAM configurations and on possible reductions -the full proof can be found in the appendix. Moreover, note that translation preserves terminal states. In a similar way, we embed the QJAM inside the FJAM. This translation is also done pointwise, although environments consist of thunks that should be considered as values. The components of the QJAM machine are translated as follows:

Q e • = • Q e e, x : p[g] = Q e e , x : Q v (p)[Q e g ] Q s • = • Q c x.t[g] = x.Q t (t)[Q e g ] Q s c • s = Q c c • Q s s
By applying the translations pointwise, we translate from a QJAM configuration to a FJAM configuration as follows:

FQ 〈 e | t | s 〉 = 〈 Q e e | Q t (t) | Q s s 〉 FQ 〈 e | p c | s 〉 = 〈 Q e e | Q v (p) Q c c | Q s s 〉 Theorem 4.6 (QJAM in FJAM). Given any two QJAM configurations U and V such that U → V , we have FQ U → + FQ V .
Proof. By case analysis on the QJAM configurations and on possible reductions -the full proof can be found in the appendix. Γ p ⇐ P Γ p ⇐ P cp ---------------------- Γ p ⇒ P Figure 6. Rules for bidirectional NJPV with associated terms Remark 4.7. The FJAM supports the use of multiple strategies in the sense that a term can be reduced partly under the CBN order, and partly using CBV. This coexistence of opposite strategies is made possible by the extra syntax in λκ-terms, reflected by polarity shifts at the level of types. This is also the case of the call-by-push-value machine [START_REF] Levy | Call-by-push-value: Decomposing call-by-value and call-by-name[END_REF], as we will see in the next section.

Call-by-push-value and LJF

As we have seen in the previous sections, the LJF system offers a versatile framework for typing λ-terms extended by advanced constructs, providing at least a partial control over the reduction strategies. Of course, the introduction of shifts at the level of types and the encodings given for CBN and CBV are reminiscent of the call-by-push-value language [START_REF] Levy | Call-by-push-value: Decomposing call-by-value and call-by-name[END_REF] in which the markers U and F establish the distinction between value types and computation types. It appears clear that there is a connection here, but this raises the question: are LJF and CBPV describing precisely the same language? This section will show that they are almost the same, but not exactly.

The type system defining CBPV is recalled in Figure 6, although we use a bidirectional presentation that allows to isolate normal forms as proofs not using the coercion rules ct and cp. We name this system NJPV to emphasise that it is a natural deduction calculus. For this reason, we remove the let construct found in CBPV, as it can be implemented as follows: ----------------------------------------------------------------- --------------------------------------------------------------------

Γ p ⇐ [P] Γ , x : P t ⇐ N --
- Γ let p be x.t ⇐ N ≡ Γ p ⇐ P ----------------------------- Γ p ⇐ ↑P ----------------------------- Γ p ⇒ ↑P Γ , x : P t ⇐ N --
- Γ p to x.t ⇐ N
or equivalently by a detour on the implication P ⊃ N . This rule corresponds to a cut in a sequent calculus, leading to a reduction in CBPV reflected as a reduction on the translation. We have adapted the CBPV syntax to fit our general framework, but one can easily see that U is ↓ and F is ↑, making • and • stand for thunk and return respectively, while F denotes the forcing of a value and the CBPV application p't is translated into t p. Formally, we use the following grammar:

t, u ::= λx.t | t p | F p | p | u to x.t p, q ::= x | t
and the terms t p and F p are called synthesised terms, while the others are checked terms, in reference to the form of the typing rules. The operational semantics of this language is specified by an abstract machine [START_REF] Levy | Call-by-push-value: Decomposing call-by-value and call-by-name[END_REF] derived from the CK machine. It has configurations containing just a term and a stack, and transitions involving the full substitution of a term for a variable in one step, as opposed to the machines we used, that performed only local operations. The transitions of the machine are:

〈 u to x.t | s 〉 → 〈 u | (to x.t) • s 〉 〈 p | (to x.t) • s 〉 → 〈 t{p/x} | s 〉 〈 F t | s 〉 → 〈 t | s 〉 〈 t p | s 〉 → 〈 t | p • s 〉 〈 λx.t | p • s 〉 → 〈 t{p/x} | s 〉
in which the stack s contains either values or term continuations, as shown in the typing rules below, found in [START_REF] Levy | Call-by-push-value: Decomposing call-by-value and call-by-name[END_REF], and presented in the style of a focused sequent calculus, as these objects cannot be typed in natural deduction style: -------------------------------------------------------------------- Γ , [↑P] (x.t) • k : M Since the operational semantics of CBPV is given through an abstract machine, it is natural to compare it to the FJAM we defined for LJF. However, the CK machine is not an abstract machine the same sense as the ones we presented here, as it performs actual substitutions on terms instead of maintaining an environment.

axl --------------------------- Γ , [a] • : a Γ p : [P] Γ , [N ] k : M il ------------------------------------------------------------ Γ , [P ⊃ N ] p • k : M Γ , x : P t : N Γ , [N ] k : M bc -
In order to carry out the comparison, we introduce a variant of this CK machine where substitutions are implemented using an environment. Moreover, in order to limit inspection of the term to its surface construct, we use a value-forcing marker F. These changes require us to distinguish between a mode for evaluating terms and another mode to treat values, as in the FJAM machine. The grammar of contexts in this PVAM machine is:

c ::= • | p[e] • c | (x.t[e]) • c | F • c
while environments are value bindings and programs terms of CBPV. Transitions for this machine are shown in Figure 7, and one can observe in particular that the reduction of F t , performed in one step in the CK machine, requires two steps, going through value mode, in the PVAM machine. The syntax of the machine is consistent with our previous framework, so that transitions may be read intuitively as in the FJAM.

Natural deduction and sequent calculi. The machine we just introduced is remarkably similar to the FJAM machine we have previously extracted from LJF. However, they evaluate different kinds of terms, as λκ is based on the sequent syntax of LJF and CBPV on a natural deduction presentation. This is more generally the difference separating the TJAM and QJAM machines from the more standard KAM and CEK machines.

In order to have a clear technical overview of the relation of the FJAM to the CBPV machine, we have defined a bidirectional system that is easier to relate to the sequent calculus. In particular, the coercion rules ct and cp closely correspond to cuts, and the meet rules mt and mp to the identity axiom.

From the perspective of our comparison, we see that CBPV and the λκ-calculus, typed by LJF, are not exactly the same: any term typeable in λκ must be η-long -up to atoms but also shifts, as for example ↓N can be the type of some variable x -while in NJPV this restriction is not enforced. Of course, one could use the η-expansion result of CBPV, valid at non-atomic types, but it would hinder the correspondence between CBPV and λκ. Indeed, if t has type N in CBPV and gets translated to a u of type N in LJF, the η-expansion of t has type N in CBPV but the expansion of u is not always typeable in LJF. To be more precise, the bijection is PVAM (call-by-push-value machine) between well-typed λκ terms and CBPV terms where all subterms of functional type are η-long. This justifies from a computational viewpoint the extension of the identity axiom to ↓N and ↑P: these are the only non-atomic types in LJF that admit η-expansion.

〈 e | u to x.t | c 〉 → 〈 e | u | (x.t[e]) • c 〉 〈 e | p | (x.t[e]) • c 〉 → 〈 e | p (x.t[e]) | c 〉 〈 e | F p | c 〉 → 〈 e | p F • c 〉 〈 e | t p | c 〉 → 〈 e | t | p[e] • c 〉 〈 e | λx.t | p[g] • c 〉 → 〈 g | p (x.t[e]) | c 〉 〈 e, x : p[ f ] | x z.u[g] | c 〉 → 〈 f | p z.u[g] | c 〉 〈 e | t z.u[g] | c 〉 → 〈 g, z : t [e] | u | c 〉 〈 e | t F | c 〉 → 〈 e | t |
Comparing machines. The translation between CBPV and λκ proceeds in two steps: first we encode the implication -⊃of CBPV as ↑↓(-⊃ -) to account for η-long normal forms found in λκ, and this is reflected on terms, as for example:

t p ↑↓ = t ↑↓ to x.(F x) p ↑↓ λx.t ↑↓ = λx. t ↑↓
Next, we translate the resulting terms as well as the machine configurations and observe the simulation of the transitions of these machines. In the following, we assume that CBPV terms are in η-long form. Following the observations made about λ [START_REF] Herbelin | A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure[END_REF] we notice that eliminations in natural deduction correspond to lists in a sequent calculus, involved in an application. Similarly, to relate NJPV to LJF we will translate synthesised terms by building a list and using it as the argument in either a left focus rule or an hcl cut. We can now give the full translation: P c (λx.t) = λx.P c (t)

P c ( p ) = P v (p) P c (u to x.t) = P c (u | κx.P c (t)) P c (t) = P c (t | ) otherwise P c (t p | k) = P c (t | P v (p) :: k) P c (F p | k) = P v (p | k) P c (t | k) = P c (t) k otherwise P v ( t ) = P c (t) P v (x) = x P v (x | k) = x k P v (p | k) = P v (p) to x.x k otherwise
in which the last case, for P v (p | k), is rather uninteresting in the basic setting, where this p can only be t . This would involve more cases in the system extended with positive connectives, such as disjunction. It is then easy to prove that this translation, on pure terms, respects the typing derivations in NJPV and LJF.

Theorem 5.1. The translation from CBPV to λκ is type-correct:

(i) if Γ t ⇐ N then Γ P c (t) : N (ii) if Γ u ⇒ N and Γ , [N ] k : M then Γ P c (u | k) : M (iii) if Γ p ⇐ P then Γ P v (p) : [P] (iv) if Γ q ⇒ a + then Γ P v (q) : [a + ] (v) if Γ q ⇒ ↓N and Γ , [N ] k : M then Γ P v (q | k) : M Proof.
The proof proceeds by mutual induction over derivations, following the structure of the translation.

In order to proceed and translate machine configurations, we will need a notion of applicative context, which is essentially a list of application arguments with a hole for the function to be applied. Such a context will correspond in λκ to a list of values with a hole for the term applied, and it is defined as:

K ::= • | K p
In particular, any synthesised term u can be decomposed into an applicative context composed with either F p or some checked term t. The translation of machine states uses this fact to translate synthesised terms. The environments and stacks are translated pointwise using F e • and F c • respectively, and the terms are translated using P c (•). Note that inside a stack, the continuation construct to x.t[e] is translated to x.P v (t)[F e e ], and a value p closed by an environment e is translated as P v (p)[F e e ]. The full translation of PVAM configurations to FJAM configurations is based on a particular recursive definition meant to handle the applicative contexts of CBPV. It is defined by three equations:

PF 〈 e | K{F q} | s 〉 = PF 〈 e | q F | K[e] • s 〉 PF 〈 e, x : p[g] | x F | s 〉 = PF 〈 g | p | s 〉 PF 〈 e, x : p[g] | x z.u[ f ] | s 〉 = PF 〈 g | p z.u[ f ] | s 〉
where the notation K[e] • s denotes the integration of a context K into the stack s, specified using the equations

• [e] • s = s and K{p}[e] • s = K[e] • (p[e] • s)
. This is a meta-level operation, that helps compute the stack configuration representing a term using an applicative context. The rest of the translation, applicable after all applicative contexts have been handled, is:

PF 〈 e | t | s 〉 = 〈 F e e | P c (t) | F c s 〉 PF 〈 e | t (to x.u[g]) | s 〉 = 〈 F e g, x : t [e] | P c (u) | F c s 〉 PF 〈 e | t F | s 〉 = 〈 F e e | P c (t) | F c s 〉
We can define P c (K{u} | m) to be P c (u | K @ m), where (K @ m) is a notation for the list specified by the equations • @ m = m and K{p} @ m = K @ (P v (p) :: m), reminiscent of the treatment given to applicative contexts in the translation of the PVAM machine. In addition, we can prove the following simple lemma, used in the final simulation result. Lemma 5.2. The FJAM can always perform the following reduction:

〈 F e e | P v (p) F c c | F c s 〉 → * PF 〈 e | p c | s 〉 Proof.
By induction on the structure of the value p and using the definition of P v (•) and PF • in particular.

We finally come to the simulation result stating that the FJAM can reduce terms as the PVAM would. Unlike the results for the TJAM and QJAM machines, the simulation does not guarantee that a step will yield at least one step inside the FJAM, because of the representation of applicative context -as can be observed in the statement of Lemma 5.2.

Theorem 5.3 (PVAM in FJAM)

. Given any two PVAM configurations U and V such that U → V , we have PF U → * PF V .

Proof. By case analysis on the PVAM configurations and on possible reductions. Reductions for the value mode hold immediately. Then, terms can reduce to value mode as shown by Lemma 5.2. In other cases, reduction is simulated with one step in FJAM for one step in the PVAM.

The translation in the other direction is simpler, and it is worth pointing out that both the hcl cut and hcr cut are translated by using a coercion, exhibiting the tight relation between coercion in natural deduction and cut in the sequent calculus.

F t (λx.t) = λx.F t (t) F t (x k) = F k (F x | k) F t ( p ) = F v (p) F t (t k) = F k (F t (t) | k) F t (p to x.t) = (λx.F t (t)) F v (p) F k (t | ) = t F k (t | p :: k) = F k (t F v (p) | k) F k (u | κx.t) = u to x.F t (t) F v (x) = x F v ( t ) = F t (t)
This is once again a translation that preserves the typeability of terms from LJF to the NJPV system.

Theorem 5.4. The translation from λκ to CBPV is type-correct:

(i) if Γ t : N then Γ F t (t) ⇐ N (ii) if Γ t : N and Γ , [N ] k : M then Γ F k (t | k) ⇐ M (iii) if Γ p : [P] then Γ F v (p) ⇐ P
Proof. By mutual induction on the given derivations, based on the translations given above and by inspection of the rules of NJPV and LJF.

A configuration of the FJAM machine will then relate to one in PVAM by a simple translation, that has in this direction no problem related to applicative contexts. Note that there are no list mode configurations in the PVAM: these are mapped the same way as the first configuration exiting the list mode. This is similar to what is done for the value mode in the other translation. The translation is defined as follows:

FP 〈 e | t | c 〉 = 〈 P e e | F t (t) | P c c 〉 FP 〈 e | p c | s 〉 = 〈 P e e | F v (p) P c c | P c s 〉 FP 〈 e | t c | k[g] + s 〉 = 〈 P e e | F t (t) | P c c + k[P e g ] • s 〉
where k[e] • s is a notation specified by the following equations:

[g] • s = P c s (p :: k)[g] • s = F v (p)[g] • (k[g] • s) (κx.t)[g] • s = (x.F t (t)[g]) • P c s
and we can finally state the simulation of the FJAM machine inside its CBPV counterpart. Theorem 5.5 (FJAM in PVAM). Given any two FJAM configurations U and V such that U → V , we have FP U → * FP V .

Proof. By case analysis on the FJAM configurations and on possible reductions.

We can therefore conclude that λκ and CBPV are describing the same language, up to the question of η-expansion. ----------------------------------------------------------------------------------------------------------------- The same analysis as for the basic machine can be conducted here, so that the disjunction in CBPV, generalised into a sum, can be related to these additional operations in the FJAM. A number of other connectives could be added to the system, but for example conjunction being a negative would be simpler that disjunction.

Interpreting Extensions of LJF

Γ p ⇐ Q di 1 ----------------------------------------- Γ inr p ⇐ P ∨ Q Γ p ⇒ P ∨ Q Γ , y : P t ⇐ N Γ , z : Q u ⇐ N de -
Maximal Inversion. One feature of focusing that we explicitly left out in our presentation of LJF is the asynchronous maximality, which not the key feature of focused proofs -in terms of normal forms -but is often adopted, in particular for proof search. As mentioned previously, this is necessary in order to have a calculus that does not enforce η-long normal forms. With this in mind, it is informative to consider whether there is a reasonable interpretation of the added structure coming from the maximal asynchronous phases. Having atomic initial rules enforces the η-long structure, that is driven by the type of the succedent, and thus the context plays no role in determining whether a term is η-long or not.

In a similar way, we can see maximal inversion as an extension of the η-long form to a setting where we consider open terms. In this case, whether a term is η-long in this extended sense is driven by both the succedent and the antecedents. This would lead to another notion of expansion, slightly more complex than η since a term could be expanded along a free variable present in the typing context. This is of particular interest if one intends to reason about programs written in a system such as λκ: normally this is done by considering η-long forms, but analysing the structure of a typed, open λκ-term also requires dealing with free variables in the context. As a general observation, systems based on sequent calculi are more complicated but offer the possibility of handling open terms in a principled way, and focusing provides the necessary structure on sequent calculi.

Conclusion and Future Work

The fundamental idea of this paper is that focusing is not simply an important normal form in pure proof theory, but is also relevant to the computational interpretation of proof systems. We have seen how in this setting, polarities can be related to evaluation strategies in a precise way -this is sometimes viewed as folklore, and has been investigated in particular cases, but never described in a systematic fashion and in the general case.

The fact that LJT and LJQ can be identified as fragments of LJF was first noted in [START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF], albeit only at the level of provability, and not in terms of the dynamics of cut elimination. In part, this is because Liang and Miller do not specify a proof term language for the LJF calculus, and consequently it is difficult to state formally exactly how cut elimination in the three systems are related. As we have shown here, the same tight correspondence exists at the level of the operational semantics given by reduction rules.

We showed how to construct an abstract machine called FJAM for the λκ-calculus by considering "cut trunks" as machine states, and applying the same methodology to LJT and LJQ lead to the TJAM and QJAM machines, variants of the KAM and CEK machines following the principles of sequent-based calculi. This provides a unifying framework in which the FJAM corresponds to the machine given for CBPV and integrates the mechanisms of both paradigms of functional programming, following a purely proof-theoretical methodology. The fact that CBPV subsumes other paradigms [START_REF] Levy | Call-by-push-value: Decomposing call-by-value and call-by-name[END_REF] is therefore explained by the fact that it harnesses the power of polarities, which is exactly what focusing does in proof theory.

An important consequence of building a calculus on a logical foundation is that extension to richer languages becomes an easy task, as shown by the history of the Curry-Howard approach. We used a bare minimum of logical connectives here: just implication, in order to be able to construct an appropriate λ-calculus. In part, this choice is forced by the comparison with LJT and LJQ, since implication is the only connective shared by these systems. We note however that all the results investigated extend to the full range of connectives of LJF, as hinted in Section 6.

The approach to constructing abstract machines outlined in this paper is based on viewing configurations of cuts as machine states, and as observed this results in machines that are somewhat low-level. Another recent approach to abstract machines is that of distillation in the linear substitution calculus [START_REF] Accattoli | Distilling abstract machines[END_REF]. It would be quite interesting to see if these approaches can be either combined or contrasted, and in particular if this can assign a motivation to the LSC methodology in terms of structural proof theory, especially focusing -we have reasons to believe so, given the roots of the LSC in proof-nets for linear logic.

The focused calculus LJF enjoys a special status among calculi for intuitionistic logic because of the added structure enforced therein by the focusing discipline. There are many other focused calculi that admit the same analysis, such as intuitionistic linear logic and its extensions with subexponentials [START_REF] Chaudhuri | Classical and intuitionistic subexponential logics are equally expressive[END_REF] or fixpoints [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF]. These logics enjoy well-behaved focused calculi, and we expect that an abstract machine can be extracted from cut elimination by following our methodology. Another interesting direction would be to apply this approach to the variants of the λ-calculus defined to interpreted classical logic with a stronger form of control.

Theorem 2 . 3 (

 23 Cut elimination). The cut rules hcl, hcr, fcl, fcr + and fcr -are admissible in LJF.

  〉 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Figure 4 .

 4 Figure 4. Transitions for the TJAM and QJAM machines extracted from LJT and LJQ

  r[•] e = r r[e, x : p[g]] e = p[g] e to x. r[e] e • c = p[e] • c c = p[e] e :: c c (x.t[e]) • c c = κx.( t[e] e c c )

Definition 4 . 1 (

 41 TJAM). The configurations of the TJAM are:

Figure 4

 4 Figure 4 also presents the QJAM machine, extracted from the LJQ cut elimination and using two configurations as well.

Definition 4 . 3 (

 43 QJAM). The configurations of the QJAM are:

Figure 5 .

 5 Figure 5. Transitions for the FJAM machine extracted from LJF

Figure 7 .

 7 Figure 7. Transitions for the PVAM machine for CBPV

Figure 8 .

 8 Figure 8. Rules for disjunction in LJF above and NJPV below

The investigation starts with the definition of the λκ-calculus, the computational interpretation of LJF proofs, a discussion of its properties and the relation between reduction rules and cut elimination, in Section 2. The expressivity of LJF is illustrated in Section 3, by considering the fragments LJT and LJQ, and by showing that the general proof-theoretical approach based upon focusing yields the expected results. This is further demonstrated in Section 4 by introducing abstract machines, and we describe a general scheme meant to derive a machine from some given 1 2015/5/28

2015/5/28

• Case hcl: if the first premise ends in ir then this is the principal case for implication, and the reduction is:D Γ , x : P t : N ir --------------------------------------Γ λx.t: P ⊃ N E Γ p : [P] F Γ , [N ] k : M il ------------------------------------------------------------------------Γ , [P ⊃ N ] p :: k : M hcl ------------------------------------------------------------------------------------------------------------- Γ (λx.t) (p :: k) : M D :: Γ p to x.t : N by hcr on (P, E, D), Γ (p to x.t) k : M by hcl on (N , D , F).• Case hcl: if the first premise ends in fr then this is the principal case for negative shift, and the reduction is:

2015/5/28

2015/5/28

Remark 3.4. We are considering a calculus for CBV that is slightly different from the one found in[START_REF] Dyckhoff | LJQ: a strongly focused calculus for intuitionistic logic[END_REF] because that calculus would be overly complicated for the task at hand. Indeed, its rewrite system is specifically tailored to obtain a strong normalisation result, while we are looking for a CBV calculus that fits the general scheme. 5 2015/5/28

2015/5/28

2015/5/28 ax ------------------------------------ Γ , x : P x ⇒ PΓ p ⇐ P ni ----------------------------- Γ p ⇐ ↑P Γ t ⇐ N pi ------------------------------ Γ t ⇐ ↓N Γ t ⇒ P ⊃ N Γ p ⇐ P ie ------------------------------------------------------------ Γ t p ⇒ N Γ , x : P t ⇐ N ii ---------------------------------------- Γ λx.t ⇐ P ⊃ N Γ u ⇒ ↑P Γ , x : P t ⇐ M ne ------------------------------------------------------------------- Γ u to x.t ⇐ M Γ p ⇒ ↓N pe -------------------------- Γ F p ⇒ N . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Γ t ⇒ N N ∈ {a -, ↑P} mt --------------------------------------------------------- Γ t ⇐ N Γ t ⇐ N ct ---------------------- Γ t ⇒ NΓ p ⇒ P P ∈ {a + , ↓N } mp ----------------------------------------------------------

2015/5/28

2015/5/28

We now consider a few of the directions in which the preceding analysis may be extended. The first and most obvious extension would be to add more of the connectives of intuitionistic logic. As an example, the inference rules for disjunction in LJF are shown in Figure8. In terms of the underlying proof theory, this requires a small addition to the cut elimination process, corresponding to the following reduction rules in the λκ calculus:(inl p) to x.x[ y.t | z.u] → p to y.(inl p) to x.t (inr p) to x.x[ y.t | z.u] → p to z.(inr p) to x.u p to x. y[z.t | w.u] → y[z.p to x.t | w.p to x.u] Γ p : [P] dr 0 -----------------------------------------Γ inl p :[P ∨ Q] Γ p : [Q] dr 1 -----------------------------------------Γ inr p :[P ∨ Q] ∆, y : P t : N ∆, z : Q u : N dl ---------------------------------------------------------------------------- ∆ = Γ , x : P ∨ Q x[ y.t | z.u] : N . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Γ p ⇐ P di 0 ----------------------------------------- Γ inl p ⇐ P ∨ Q

2015/5/28

2015/5/28

Acknowledgments

This work is funded by grant 10-092309 of the Danish Council for Strategic Research to Demtech (Guenot and Gustafsson) and by the ERC Advanced Grant ProofCert (Brock-Nannestad).

A. Cut admissibility for LJF

The following theorem establishes cut admissibility for LJF as discussed in Section 2, with details of the cases.

Theorem A.1 (Cut admissibility). The rules hcl, hcr, fcl, fcr + and fcr -are admissible in LJF.

Proof. The proof proceeds by lexicographical induction on the structure of the cut formula and the premises of the cut. Note that this is also a proof of weak normalisation for the reduction rules for LJF proof terms described previously. We assume the given input derivations are cut-free, corresponding to a reduction strategy that reduces the innermost redexes, corresponding to the topmost cuts in the given derivation.

Note that because we are working with focused versions of the cut rule, every cut may be reduced by only considering cases on one of the premises, specifically the premise where the cut formula is not under focus. In addition to this, we also show the cases where the first premise ends in an axiom rule. This is to justify the fact that we eagerly reduce cases that amount to simple variable substitution.

A.1 Cases for hcl

First premise ends in ir (principal case for implication):

First premise ends in fr (principal case for negative shift):

First premise ends in fl (left-commutative case):

A.2 Cases for hcr:

First premise ends in axr: axr ------------------------------------- Γ , x : P x : [P] E Γ , x : P, y : P t : N hcr - -------------------------------------------------------------------------------------------- Γ , x : P x to y.t : N Γ , x : P t{x/ y} : N by renaming substitution.

Second premise ends in fl (principal case for positive shift): ------------------------------------------------------ Γ , x : ↓ M x k : N hcr -------------------------------------------------------------------------------------------------------- Γ u to x.(x k) : N

Second premise ends in fl (right-commutative case): ------------------------------------------------------------------- Γ , x : P, y : ↓ M y k : N hcr - --------------------------------------------------------------------------------------------------- Second premise ends in ir (right-commutative case): -------------------------------------------------- Γ , x : -----------------------------------------------------------------------------------------

Second premise ends in fr (right-commutative case): ----------------------------------------- Γ , x : P q : ↑Q hcr - -------------------------------------------------------------------------------- Γ p to x. q : ↑Q Γ p to x.q : [Q] by fcr + on (P, D, E). Γ p to x.q : ↑Q by fr.

A.3 Cases for fcl:

First premise ends in axl:

First premise ends in il (left-commutative case): ----------------------------------------------------------------------- Γ , ------------------------------------------------------------------------------------------------------ Γ ,

by il on D and E .

First premise ends in bl (left-commutative case): ---------------------------------------------------------------------------------

A.4 Cases for fcr + :

First premise ends in axr: axr ------------------------------------- Γ , x : P x : [P] E Γ , x : P, y : ------------------------------------------------------------------------------------------------- Γ , x : P x to y.p : ------------------------------------------------ Γ , x : P, y : P y : ----------------------------------------------------------------------------------------------------------- Γ , y : P p to x. y :

Second premise ends in axr (principal case): ------------------------------------ Γ , x : P x : -------------------------------------------------------------------------------- Γ p to x.x : [P]

Second premise ends in br (right-commutative case): ------------------------------------------------------------------------------------- Γ p to x. u : [↓N ]

Γ p to x.u : N by hcr on (P, D, E). Γ p to x.u : [↓N ] by br.

A.5 Cases for fcr -:

First premise ends in axr: axr ------------------------------------- Γ , x : P x : --------------------------------------------------------------------------------------------------------- Γ , x : P, [N ] x to y.k : M Γ , x : P, [N ] k{x/ y} : M by renaming substitution.

Second premise ends in axl: ----------------------------------------- Γ , x : P, [N ] : N fcr --------------------------------------------------------------------------------------- Γ , [N ] p to x. : N

Γ , [N ]

: N by axl.

Second premise ends in il: ------------------------------------------------------------------------------------------------- Γ , x : P, [Q ⊃ N ] q :: k : M fcr - ----------------------------------------------------------------------------------------------------------------------- ---------------------------------------------------- Γ , x : P, [↑Q] κ y.t : M fcr - ---------------------------------------------------------------------------------------------

B. λ and λq reductions simulated in λκ

Reductions in λ can be simulated in λκ using the translations T t (•) and T k (•) defined in Section 3.

Theorem B.1. For any t and u in λ, if t → u then T t (t) → + T t (u).

Proof. By inspection of the reduction rules of λ and of the result of the translation T t (•):

Theorem B.2. For any lists k and m in λ, if t → u then T k (t) → + T k (u).

Proof. By inspection of the reduction rules of λ and of the result of the translation T k (•):

Reductions in λq can be simulated in λκ using the translations Q t (•) and Q v (•) defined in Section 3. Proof. By inspection of the reduction rules of λq and of the result of the translation Q t (•), notice that for all t and variables x, y the translation

Theorem B.3. For any t and u in λq

Theorem B.4. For any value p and q in λq, if p → q then

Proof. By inspection of the reduction rules of λq and of the result of the translation Q v (•), notice that for all p and variables x, y the translation

C. TJAM and QJAM simulated inside FJAM

The TJAM machine can be simulated inside FJAM as discussed in Section 4.

Theorem C.1 (TJAM in FJAM). Given any two TJAM configurations U and V such that U → V , we have FT U -→ * FT V .

Proof. By case analysis on the TJAM configurations and on possible reductions, notice that for all b and d the translation

The QJAM machine can be simulated inside FJAM as discussed in Section 4.

Theorem C.2 (QJAM in FJAM). Given any two QJAM configurations U and V such that U → V , we have FQ U -→ + FQ V .

Proof. By case analysis on the QJAM configurations and on possible reductions:


Laurent Bulteau
email: laurent.bulteau@inria.fr

Gustavo Sacomoto
email: gustavo.sacomoto@inria.fr

Blerina Sinaimeri
email: blerina.sinaimeri@inria.fr

Computing an Evolutionary Ordering is Hard 1

Keywords: evolutionary family, ear-decomposition, complexity

A family of sets is evolutionary if it is possible to order its elements such that each set except the first one has an element in the union of the previous sets and also an element not in that union. This definition is inspired by a conjecture of Naddef and Pulleyblank concerning ear decompositions of 1-extendable graphs. Here we consider the problem of determining whether a family of sets is evolutionary. We show that the problem is NP-complete even when every set in the family has at most 3 elements and each element appears at most a constant number of times. In contrast, for families of intervals of integers, we provide a polynomial time algorithm for the problem.

Introduction

A family of sets S, is called evolutionary if there exists an ordering of the sets in S such that except for the first set, every set in the order contains both an element that belongs to the union of the previous sets (an old element) and an element that does not (a new one). The concept of evolutionary families was introduced in [START_REF] Little | Evolutionary families of sets[END_REF] motivated by a result of Carvalho, Lucchesi and Murty [START_REF] Carvalho | Ear Decompositions of Matching Covered Graphs[END_REF] on a question related to the ear-decomposition of 1-extendable graphs, posed by Naddef and Pulleyblank in [START_REF] Naddef | Ear Decompositions of Elementary Graphs and GF2-rank of Perfect Matchings[END_REF].

Let G be a graph and G a subgraph of G. A path P in G of odd length is called an ear of G if V (P ) ∩ V (G ) consists of the two endpoints of P . An n-ear is a set of n vertex-disjoint ears. A graph G is 1-extendable if each one of its edges belongs to a perfect matching of G.

It is well-known that bipartite graphs that are 1-extendable can be constructed simply by adding one ear at a time to smaller graphs of the same type. This property does not hold in general for 1-extendable graphs. In order to guarantee an ear decomposition where each graph in the sequence is also 1-extendable we have to allow to add more ears simultaneously. In [START_REF] Lovász | Matching Theory[END_REF], Lovász and Plummer proved the so called Two Ear Theorem, where they show that in constructing 1-extendable graphs, adding at most two (disjoint) ears in each step will suffice to guarantee that the intermediate graphs in the construction are themselves 1-extendable. Naddef and Pulleyblank [START_REF] Naddef | Ear Decompositions of Elementary Graphs and GF2-rank of Perfect Matchings[END_REF] asked about the smallest number of 2-ear additions necessary in such a decomposition. This question was answered in [START_REF] Carvalho | Ear Decompositions of Matching Covered Graphs[END_REF] and their results inspired Little and Campbell [START_REF] Little | Evolutionary families of sets[END_REF] to introduce the concept of evolutionary families.

Indeed, it was proved in [START_REF] Carvalho | Ear Decompositions of Matching Covered Graphs[END_REF] that the minimum number of 2-ear additions in a ear decomposition of a 1-extendable graph G is dimC(G) -dimA(G), where C(G) and A(G) denote the cycle space and the alternating subspace of G, respectively. Little and Campbell [START_REF] Little | Evolutionary families of sets[END_REF] then observed that the minimum number of 2-ear additions is achieved for a basis of A(G) that, among other properties, is evolutionary. They also gave some sufficient conditions for a family to be evolutionary.

In this paper, we investigate the complexity of deciding whether a given family is evolutionary. More formally, we consider the following problem:

Evolutionary Ordering Problem INSTANCE: A family S of sets. DECIDE: Is S evolutionary? This problem was posed by M. Steel as one of the "Penny Ante" prize questions of the Annual New Zealand Phylogenetics Meeting in 2012 [START_REF] Steel | The "Penny Ante[END_REF]. In this paper we fully answer this question by showing in Section 2 that the problem is NP-complete and remains so even when every set in the family has at most 3 elements and where each element appears a constant number of times. Observe that this result is tight regarding the set cardinalities as for the case when each set has at most two elements the problem can be easily solved in polynomial time as already observed in [START_REF] Little | Evolutionary families of sets[END_REF].

Finally, in Section 3 we show that for sets of intervals of integers the problem is solvable in polynomial time.

Evolutionary ordering is NP-complete

We show in this section that deciding whether a given family is evolutionary is NP-complete. Moreover, it remains so even when each of the sets in the family has cardinality at most 3. The reduction is obtained using a restricted version of the SAT problem defined as follows:

(3, 2)-SAT [START_REF] Tovey | A simplified NP-complete satisfiability problem[END_REF] INSTANCE: A Boolean formula F in conjunctive normal form where each clause has two or three literals and each literal appears in at most 2 clauses. DECIDE: Is there some assignment of true and false value that will make the formula F true?

Theorem 2.1 Evolutionary Ordering is NP-complete.
Proof. It is clear that the Evolutionary Ordering problem is in NP. We show it is also NP-complete. Let Φ be an instance of (3,2)-SAT with n variables and m clauses. For ease of presentation, assume that each literal occurs exactly 2 times, and each clause has exactly 3 literals. Note that 4n = 3m.

We construct an instance of Evolutionary Ordering problem by assigning a set to each variable, literal and clause. The main idea is that every evolutionary ordering of the sets would necessary imply an ordering where the sets corresponding to variables that are assigned true come first, then the sets of the corresponding literals, then all the clauses that contain at least one literal assigned true and hence that appeared before, and finally it must be possible to add the remaining sets corresponding to the variables that are assigned false. Note, that in order to have an assignment we have to guarantee that not both sets corresponding to x i , xi are taken before the clause sets. We proceed now to formally detail the construction.

The universe in which the sets are constructed contains the following 8n + 2m + 1 elements:

• 1 trigger element, denoted τ

• 2n assignment elements, denoted x i and xi for each 1 ≤ i ≤ n

• 2n free elements, denoted f i and fi for each 1 ≤ i ≤ n

• 4n literal elements, denoted 1 i , 2 i and ¯ 1 i , ¯ 2 i for each 1 ≤ i ≤ n • 2m clause elements, denoted c j and c j for each 1 ≤ j ≤ j

We create the following sets:

• A triggering set: T := {τ } • For each 1 ≤ i ≤ n, define two variable sets and a verification set:

L i := {x i , τ, f i , 1 i , 2 i } and Li := {x i , τ, fi , ¯ 1 i , 2 i } V i := {x i , xi , c 1 , c 1 , c 2 , c 2 , . . . c m , c m }
• For each 1 ≤ j ≤ m, where the jth clause uses, say, literals 1 1 , 1 2 , ¯ 1 3 , define two clause sets

C j := { 1 1 , 1 2 , ¯ 1
3 , c j } and C j := {c j , c j } Let S denote this family of sets. We prove that S has an evolutionary ordering if, and only if, Φ is satisfiable.

If. Given a truth assignment, we simply give an evolutionary ordering of the sets. Start with the triggering set {τ }. No condition needs to be satisfied for this set.

For each variable x i add the set L i if x i is assigned true, Li otherwise. For each one of them, τ is old, and f i (or fi ) is new.

For each clause c j , add sets C j and C j . Since the clause is satisfied, some literal h i (or ¯ h i ) must be assigned true, so the corresponding element in L i is old for set C j . Element c j is new for set C j , and then old for set C j . Element c j is new for set C j .

For each variable add the verification set V i . For every i the elements c i , c i are all old for each of those sets. If x i is assigned true (resp. false), then element xi (resp. x i ) is new.

Finally, we add the remaining variable sets. For each variable x i add Li if x i is assigned true, L i otherwise. For each one, τ is old, and f i (or fi ) is new.

Overall, we have an ordering of the sets where each one has an old and a new element: the set is evolutionary.

Only if. Consider an evolutionary ordering of the sets. Observe that every such ordering would put set T = {τ } in the first position. Moreover, all the clauses C j must appear before any V i as C j ⊂ V i . Let us write A for the family of the sets L i and Li that appear before their corresponding verification sets V i . For each variable x i , it is not possible to have both L i ∈ A and Li ∈ A. Otherwise, V i would not have any new element, since V i ⊆ L i ∪ Li ∪ m j=1 C j and each C j is already before V i . Thus, we design a truth assignment such that x i is true if L i ∈ A, and false otherwise. This way, for each L i or Li in A, the corresponding literal (x i or xi ), is assigned true.

It remains to show that the assignment satisfies formula Φ. Consider each regular clause c j . First, C j appears before C j . Indeed, the only sets intersecting C j are C j and each V i . Remember that V i s appear after C j , so either C j is first or C j is before C j . It follows that the old element of C j cannot be c j , hence it is a literal element h i or ¯ h i . So the corresponding variable set L i or Li must be before C j , hence before C j and V i . Overall, for each clause, one of L i or Li corresponding to a literal of the clause is in A, and the literal is satisfied by our assignment.

2

It is possible to modify the gadget used in the previous reduction in such a way that every set in the family has cardinality at most 3 and every element appears at most a constant number of times. Thus, the following stronger result holds. Theorem 2.2 Evolutionary Ordering is NP-complete even if each set in the family has cardinality at most 3 and each element appears at most a constant number of times.

A polynomial algorithm for interval families

In this section we consider the particular case where the sets in S are intervals of integers, i.e. for each S i ∈ S we have that

S i = [a i , b i ] = {k ∈ Z | a i ≤ k ≤ b i }.
We obtain a polynomial algorithm for this case using a dynamic programing approach. Before describing the algorithm, we need some extra definitions. Given a family of intervals S, we define a(S)

= min{a i | [a i , b i ] ∈ S} and b(S) = max{b i | [a i , b i ] ∈ S}. We say S i = [a i , b i ] is the leftmost (resp. rightmost) interval if it is a unique interval with a i = a(S) (resp. b i = b(S)).
In other words, a j > a i (resp. b j < b i ) for all j = i.

An immediate property is that if the union of the sets in S is not an interval (precisely, the interval [a(S), b(S)]), then S cannot be evolutionary. The key observation to obtain an efficient algorithm is given in the next lemma. Lemma 3.1 The last interval in any evolutionary ordering of S is a leftmost or rightmost interval. Moreover, if S has no leftmost nor rightmost intervals then S is not evolutionary.

Proof. Suppose by contradiction that the last interval [x, y] in an evolutionary order of S is not a leftmost or rightmost interval. Write S = S \ {[x, y]}. This implies that a(S ) = a(S) and b(S ) = b(S). On the other hand, [x, y] has a new element z. Thus, there is no evolutionary ordering for S , since this set contains intervals both to the left and to the right of z but none including it.2

As a corollary, we have the following recursive relation: ( ) S is evolutionary iff S has a leftmost interval S l and S \ {S l } is evolutionary, or S has a rightmost interval S r and S \ {S r } is evolutionary. It follows that the number of subproblems of ( ) is bounded by the number of intervals of the form [a i , b j ], which in turn is bounded by |S| 2 . A standard dynamic programming approach based on ( ) gives a polynomial algorithm.

Lemma 3 . 2

 32 Let S , S ⊆ S correspond to subproblems of ( ), if a(S ) = a(S ) and b(S ) = b(S ) then S = S . Proof. At each step of ( ) a leftmost (or rightmost) interval is removed from the current set S, thus strictly increasing a(S) (or decreasing b(S)). This implies that S contains all intervals entirely included in [a(S ), b(S )]. Thus, S = S . 2

 [START_REF] Carvalho | Ear Decompositions of Matching Covered Graphs[END_REF]This work was supported by the European Research Council under the European Community's Seventh Framework Programme (FP7 / 2007-2013) / ERC grant agreement no.

[247073]10 and by the European Union Framework Program 7 "BacHBerry", Project number FP7-613793.