Jirka Maršík

Maxime Amblard

Philippe De Groote

Introducing λ , a λ-calculus for effectful computation

Keywords: side effects, monads, λ-calculus, handlers, CRS, IDTS

come

1 Introduction λ-calculus is a widely used tool for semantic analysis of natural language [START_REF] Partee | The development of formal semantics in linguistic theory[END_REF]. λ terms serve as higher order logic formulas that give the truth conditions of sentences and they also describe how the meanings of the individual constituents compose together using abstraction and function application. The numerous linguistic phenomena in play lend themselves to analyses using computational side effects and monads [START_REF] Shan | Monads for natural language semantics[END_REF][START_REF] Shan | Linguistic side effects[END_REF][START_REF] Shan | Linguistic side effects[END_REF][START_REF] Charlow | On the semantics of exceptional scope[END_REF]. The idea of treating linguistic expressions as effectful actions or programs is also very relevant to dynamic semantics, which treats the meanings of sentences as instructions to update some common ground or other linguistic context [START_REF] Kamp | From discourse to logic: Introduction to modeltheoretic semantics of natural language, formal logic and discourse representation theory[END_REF][START_REF] Groenendijk | Dynamic predicate logic[END_REF]. In order to study a fragment of natural language that encompasses several of the effectful phenomena, we need a framework that would help us manage the increasing complexity of the λ-terms involved. In this paper, we present an extension to the simply-typed λ-calculus for that exact purpose.

Taking stock of the different monadic structures of linguistic side effects, we can examine existing approaches that try to combine side effects to find a formalism that can talk about all the aspects of language at the same time. One such theoretical framework are effects and handlers. In this framework, programs are interpreted as sequences of instructions (or more generally as decision trees). 1 The instructions are symbols called operations, which stand for the different effects, the different ways that programs can interact with their contexts. The process of calculating the semantic representation of a linguistic expression is then expressed as a program using these operations. This is when handlers come into play. A handler is an interpreter that gives a definition to the operation symbols in a program. Handlers can be made modular2 so that the interpreter for our vocabulary of context interactions can be defined as the composition of several smaller handlers, each treating a different aspect of language (dynamicity, implicatures, deixis. . . ).

When using effects and handlers, we therefore start by enumerating the set of interactions that programs can have with their contexts. We then write handlers which implement these instructions and produce a suitable semantic representation. This approach thus closely follows the mantra given by Lewis: In order to say what a meaning is, we may first ask what a meaning does and then find something that does that. General Semantics, David Lewis [START_REF] Lewis | General semantics[END_REF] We can trace the origins of effects and handlers to two strands of work. One is Cartwright and Felleisen's work on Extensible Denotational Language Specifications [START_REF] Cartwright | Extensible denotational language specifications[END_REF], in which a technique for building semantics is developed such that when a (programming) language is being extended with new constructions (and new side effects), the existing denotations remain compatible and can be reused.

The other precursor is Hyland, Plotkin and Power's work on algebraic effects [START_REF] Hyland | Combining effects: Sum and tensor[END_REF], a categorical technique for studying effectful computations, which was later extended by Plotkin and Pretnar to include handlers [START_REF] Plotkin | Handlers of algebraic effects[END_REF][START_REF] Pretnar | Logic and handling of algebraic effects[END_REF][START_REF] Plotkin | Handling algebraic effects[END_REF]. The reader can refer to [START_REF] Plotkin | Computational effects and operations: An overview[END_REF][START_REF] Pretnar | An introduction to algebraic effects and handlers[END_REF] for an overview of computational effects. This was further developed in [START_REF] Hillerström | Shallow effect handlers[END_REF][START_REF] Biernacki | Abstracting algebraic effects[END_REF].

The technique has gained in popularity in recent years (2012 and onward). It finds applications both in the encoding of effects in pure functional programming languages [START_REF] Kiselyov | Extensible effects: an alternative to monad transformers[END_REF][START_REF] Kiselyov | Freer monads, more extensible effects[END_REF][START_REF] Kammar | Handlers in action[END_REF][START_REF] Brady | Programming and reasoning with algebraic effects and dependent types[END_REF] and in the design of programming languages [START_REF] Bauer | Programming with algebraic effects and handlers[END_REF][START_REF] Lindley | Do be do be do[END_REF][START_REF] Dolan | Effective concurrency through algebraic effects[END_REF][START_REF] Kiselyov | Eff directly in ocaml[END_REF][START_REF] Hillerström | Compiling links effect handlers to the ocaml backend[END_REF], and also inspired extensions of other programming languages in Java [START_REF] Brachthäuser | Effect handlers for the masses[END_REF] and in C [START_REF] Leijen | Implementing algebraic effects in c[END_REF].

Algebraic effects provide a strong and deep foundation for a theory of computation side effects. Their mathematical development is rooted in Lawvere theories [START_REF] Hyland | The category theoretic understanding of universal algebra: Lawvere theories and monads[END_REF][START_REF] Lawvere | Algebraic theories, algebraic categories, and algebraic functors[END_REF], with new generalizations [START_REF] Bonchi | Functorial semantics for relational theories[END_REF] and extensions [START_REF] Baez | Enriched lawvere theories for operational semantics[END_REF] of the context still being discovered. The use of algebraic theories to describe computation also lends itself to other fruitful applications, e.g. connecting the theories with algebraic specifications of programs.

The problem of the specification and verification of programs with algebraic effects has seen a lot of progress recently [START_REF] Letan | Modular verification of programs with effects and effects handlers[END_REF][START_REF] De Vilhena | A separation logic for effect handlers[END_REF][START_REF] Kiselyov | Not by equations alone: Reasoning with extensible effects[END_REF][START_REF] Luksic | Local algebraic effect theories[END_REF][START_REF] Swierstra | A predicate transformer semantics for effects (functional pearl)[END_REF][START_REF] Biernacki | Handle with care: relational interpretation of algebraic effects and handlers[END_REF][START_REF] Matache | A sound and complete logic for algebraic effects[END_REF]. Other interesting developments include the introduction of dependent types [START_REF] Ahman | Handling fibred algebraic effects[END_REF], a generalization from monads to applicative functors and arrows [START_REF] Pieters | Generalized monoidal effects and handlers[END_REF], new mechanisms for abstracting effects [START_REF] Biernacki | Abstracting algebraic effects[END_REF] and novel implementation techniques [START_REF] Hillerström | Effect handlers via generalised continuations[END_REF][START_REF] Kawahara | One-shot algebraic effects as coroutines[END_REF]. Algebraic effects and effect handlers provide a modular abstraction for effectful programming. They support user-defined effects, as in Haskell [START_REF] Jones | Haskell 98 language and libraries: the revised report[END_REF], in conjunction with direct-style effectful programming, as in ML [START_REF] Gordon | A metalanguage for interactive proof in lcf[END_REF][START_REF] Milner | Implementation and applications of scott's logic for computable functions[END_REF]. They also present a structured interface to programming with delimited continuations [START_REF] Hillerström | Continuation passing style for effect handlers[END_REF].

In this article, we will focus on defining a suitable calculus based on STLC which implement effects and handlers: λ .

We will be adding a new type constructor, F, into our language. The type F(α) will correspond to effectful computations that produce values of type α. The idea comes from the programming language Haskell and its use of monads [START_REF] Moggi | Notions of computation and monads[END_REF][START_REF] Wadler | The essence of functional programming[END_REF]. Our type constructor F will also stand in for a monad, one that has been already encoded in Haskell in several ways [START_REF] Kiselyov | Extensible effects: an alternative to monad transformers[END_REF][START_REF] Kammar | Handlers in action[END_REF]. The motivation behind λ is to build a minimal language which directly gives us the primitive operations for working with this particular monad. This way, we end up with a language that:

• is smaller than Haskell (and thus more mananageable to analyse),

• is closer to the STLC (favored by semanticists),

• and which makes more evident the features that our proposal relies on.

The distinction between the type α and the type F(α) will, in different analyses, align with dichotomies such as reference/sense or static/dynamic meaning.

The question then is, what form should our general F type constructor take? We want to have a construction that can combine all the existing ones. One can do the combining at the level of monads with the use of monad transformers, a technique pioneered by Moggi and very well-established in the Haskell programming community [START_REF] Moggi | Notions of computation and monads[END_REF]. Simon Charlow has made the case that this technique can be exploited to great benefit in natural language semantics as well [START_REF] Charlow | On the semantics of exceptional scope[END_REF].

However, a competing technique has emerged in recent years. The technique goes by many names, "algebraic effects and handlers" and "extensible effects" being the most commonly used ones. This is in part due to the fact that it lies at the confluence of several research programs. This fact will allow us to present the theory from two different perspectives.

Algebraic Effects and Handlers

Hyland, Power and Plotkin have studied the problem of deriving denotational semantics of programming languages that combine different side effects [START_REF] Hyland | Combining effects: Sum and tensor[END_REF]. In their approach, rather then modeling the individual effects using monads and combining the monads, every effect is expressed in terms of operators on computations. Computations thus become algebraic expressions with effects as operations and values as part of the generator set. Let us take the example of nondeterminism. In the monadic framework, this effect is analyzed by shifting the type of denotations from α to the powerset P(α). In the algebraic framework, a binary operator + is introduced and is given meaning through a set of equations. In this case, these are the equations of a semilattice (stating the operator's associativity, commutativity and idempotence).

When the time comes to combine two effects, their signatures are summed together and their theories are combined through either a sum or a tensor (tensor differs from sum in that it adds commutativity laws for operators coming from the two different effects).

In order to fit exception handlers into their theory, Plotkin and Pretnar enriched the theory with a general notion of a handler [START_REF] Plotkin | Handling algebraic effects[END_REF]. A handler's purpose is to replace occurrences of an operator within a computation by another expression. This notion was shown to be very useful. Since using a handler on a computation is similar to interpreting its algebraic expression in a particular algebra, in many practical applications, the use of handlers has replaced equational theories altogether [START_REF] Bauer | Programming with algebraic effects and handlers[END_REF][START_REF] Kammar | Handlers in action[END_REF][START_REF] Brady | Programming and reasoning with algebraic effects and dependent types[END_REF].

Extensible Effects

In the early 90's, Cartwright and Felleisen were working on the following problem. Imagine you have a simple programming language along with some denotational semantics or some other interpretation. In your simple language, numerical expressions might be interpreted as numbers. In that case, the literal number 3 would denote the number 3 and the application of the sum operator to two numerical expressions would denote the sum of their interpretations. Now imagine that you want to add mutable variables to your language. Numerical expressions no longer denote specific numbers, but rather functions from states of the variable store to both a number and an updated variable store (since expressions can now both read from and write to variables). The number 3 is thus no longer interpreted as the number 3 but as a combination of a constant function yielding the number 3 and an identity function. The addition operator now has to take care to thread the state of the memory through the evaluation of both of its arguments. In short, we are forced to give new interpretations for the entire language.

Cartwright and Felleisen proposed a solution to this problem [START_REF] Felleisen | Abstract continuations: a mathematical semantics for handling full jumps[END_REF][START_REF] Cartwright | Extensible denotational language specifications[END_REF]. In their system, an expression can either yield a value or produce an effect. If it produces an effect, the effect percolates through the program all the way to the top, with the context that the effect projected from stored as a continuation. The effect and the continuation are then passed to an external "authority" that handles the effect, often by producing some output and passing it back to the continuation. When a new feature is added to the language, it often suffices to add a new kind of effect and introduce a new clause into the central "authority". The central authority then ends up being a collection of small modular interpreters for the various effect types. Denotation-wise, every expression can thus have a stable denotation which is either a pure value or an effect request coupled with a continuation.

Later on, this project was picked up by Kiselyov, Sabry and Swords, who, following Plotkin and Pretnar's work on handlers, proposed to break down the "authority" into the smaller constituent interpreters and have them be part of the language themselves [START_REF] Kiselyov | Extensible effects: an alternative to monad transformers[END_REF].

Synthesis

In our language, values of type F(α) can be seen either as algebraic expressions or as programs. Under the algebraic perspective, an expression is either a variable or an operator applied to some other expressions, whereas under the "extensible effects" perspective, a program is either a value or a request for an effect followed by some other programs (the continuation).

Our calculus will also have a special form for defining handlers. In the "algebraic effects and handlers" frame of mind, these can be thought of as algebras that interpret the operations within an algebraic expression. On the other hand, with "extensible effects", the intuition is more similar to that of an exception handler which intercepts requests of a certain type and decides how the computation should continue.

There is a way to avoid lifting when working with monad transformers. We characterize every monad transformer by some capabilities/operations it gives us and then we write abstract polymorphic terms which can be interpreted in different monads provided that they have enough structure to interpret the capability/operation. This is the method presented in [START_REF] Liang | Monad transformers and modular interpreters[END_REF][START_REF] Jones | Functional programming with overloading and higher-order polymorphism[END_REF] and used in (Haskell) libraries implementing monad transformers [START_REF]mtl: Monad classes, using functional dependencies[END_REF]. However, formalizing this method already leads us half of the way towards effect and handlers (we write computations using abstract operations and the type of the computation indicates the operations that must be interpreted).

Article structure

The article is organised as follows: Section 2 gives the fundamental definitions of λ and Section 3 shows some derivable rules. With all the equipment in place, we can now go deeper into the properties of the calculus. We start in Section 4 with type soundness, which includes subject reduction and progress. Then we discuss the algebraic properties in Section 5, confluence in Section 6 and termination in Section 7.

Definitions

We start with the formal definitions of all the essential components of λ , starting with the syntax of terms, then the syntax of types. We then continue with the judgments that relate types to terms and the reduction semantics.

Terms

Let X be a set of variables, Σ a typed signature and E a set of operation symbols. The expressions of our language are comprised of the following: The first four constructions -variables, constants, abstractions and applications -come directly from STLC with constants.

The next four deal with the algebraic expressions used to encode computations. Let us sketch the behaviors of these four kinds of expressions under the two readings outlined above.

Algebraic Expressions -The Denotational View

The set of algebraic expressions is generated by closing some generator set over the operations of the algebra. The η function serves to inject values from the generator set into the set of algebraic expressions. It is the constructor for the atomic algebraic expressions.

Next, for every symbol op in E, we have a corresponding constructor op in our calculus. op is a constructor for algebraic expressions whose topmost operation is op. The op constructor takes as argument a function that provides its operands, which are further algebraic expressions.

The banana brackets op 1 : M 1 , . . . , op n : M n , η: M η contain algebras: interpretations of operators and constants. These components are combined into a catamorphism that can interpret algebraic expressions (hence the use of banana brackets [START_REF] Meijer | Functional programming with bananas, lenses, envelopes and barbed wire[END_REF]). 3The extraction function -• , pronounced "cherry", takes an atomic algebraic expression (the kind produced by η) and projects out the element of the generator set.

Effectful Computations -The Operational View

We will now explain these constructions from the computational point of view. The η function "returns" a given value. The result of applying it to a value x is a computation that immediately terminates and produces the value x.

The symbols from E become something like system calls. A computation can interrupt its execution and throw an exception with a request to perform a system-level operation. For every symbol op in E, there is a constructor op that produces a computation which issues a request to perform the operation op. This constructor takes as an argument a continuation which yields the computation that should be pursued after the system-level operation op has been performed.

The banana brackets op 1 : M 1 , . . . , op n : M n , η: M η describe handlers: they contain clauses for different kinds of interrupts (operation requests) and for successful computations (clause η). They behave very much like handlers in languages with resumable exceptions such as Common Lisp or Dylan.

Finally, the cherry function -• can take a computation that is guaranteed to be free of side effects and run it to capture its result.

The 9th construction in our calculus is the C operator. C serves as a link between the function type discussed by STLC (constructions 1-4) and the computation type introduced in our calculus (constructions 5-8). C is a (partial) function that takes a computation that produces a function and returns a function that yields computations. In a way, C makes abstracting over a variable and performing an operation commute together. 4We will see the utility of C later on. The idea came to us from a paper by Philippe de Groote [START_REF] De Groote | On logical relations and conservativity[END_REF] which tried to solve a similar problem. The name comes from the C combinator, which reorders the order of abstractions in a λ-term.

Types and Typing Rules

We now give a syntax for the types of λ alongside with a typing relation. In the grammar below, ν ranges over atomic types from a set T .

The types of our language consist of: function α → β, where α and β are types atom ν, where ν is an atomic type from T computation F E (α), where α is a type and E is an effect signature (defined next)

The only novelty here is the F E (α) computation5 type. This type will be inhabited by effectful computations that have permission to perform the effects described in E and yield values of type α. The representation will be that of an algebraic expression with operators taken from the signature E and generators of type α.

In giving the typing rules, we will rely on the standard notion of a context. For us, specifically, a context is a partial mapping from the variables in X to the types defined above. We commonly write Γ, x : α for a context that assigns to x the type α and to other variables y the type Γ(y). We also write x : α ∈ Γ to say that the context maps x to α. Note, however, that for ∆ = Γ, x : α, x : β, we have x : β ∈ ∆ while x : α / ∈ ∆. Effect signatures are very much like contexts. They are partial mappings from the set of operation symbols E to pairs of types. We will write the elements of effect signatures the following way: op : α β ∈ E means that E maps op to the pair of types α and β. 6 When dealing with effect signatures, we will often make use of the disjoint union operator . The term E 1 E 2 serves as a constraint demanding that the domains of E 1 and E 2 be disjoint and at the same time it denotes the effect signature that is the union of E 1 and E 2 .

The last kind of dictionary used by the type system is a standard higher-order signature for the constants (a map from names of constants to types). For those, we adopt the same conventions.

x : α ∈ Γ [var] Γ x : α c : α ∈ Σ [const] Γ c : α Γ, x : α M : β [abs] Γ λx. M : α → β Γ M : α → β Γ N : α [app] Γ M N : β Γ M : α [η] Γ η M : F E (α) Γ M p : α Γ, x : β M c : F E (γ) op : α β ∈ E [op] Γ op M p (λx. M c ) : F E (γ) Γ M : F ∅ (α) [ -• ] Γ -• M : α E = {op i : α i β i } i∈I E f E = E E f [Γ M i : α i → (β i → F E (δ)) → F E (δ)] i∈I Γ M η : γ → F E (δ) Γ N : F E (γ) [ ] Γ (op i : M i ) i∈I , η: M η N : F E (δ) Γ M : α → F E (β) [C] Γ C M : F E (α → β)
Figure 1: The typing rules for λ .

In our typing judgments, contexts will appear to the left of the turnstile and they will hold information about the statically (lexically) bound variables, as in STLC. Effect signatures will appear as indices of computation types and they will hold information about the operations that are dynamically bound by handlers. Finally, there will be a single higher-order signature that will globally characterize all the available constants.

The typing judgments are presented in Figure 1. Metavariables M , N . . . stand for expressions, α, β, γ. . . stand for types, Γ, ∆. . . stand for contexts, op, op i stand for operation symbols and E, E . . . stand for effect signatures. Σ refers to the higher-order signature giving types to constants.

The typing rules mirror the syntax of expressions. Again, the first four rules come from STLC. The next four deal with introducing pure computations, enriching them with effectful operations, handling those operations away and finally eliminating pure computations. The C rule lets us start to see what we meant by saying that the C operator lets the function type and the computation type commute.

Let us ponder the types of the new constructions so as to get a grip on the interface that the calculus provides us for dealing with computations.

[η]

First off, we have the η operator. It takes a value of type α and injects it into the type F E (α). The metavariable E is free, meaning η can take values of type α to type F E (α) for any E. The algebraic intuition would say that elements of the generator set are valid algebraic expressions independent of the choice of signature. Computationally, returning a value is always an option, independently of the available permissions.

[op]

More complicated computations can be built up by extending existing computations using the operation construction. Let us have an effect signature E such that op : α β ∈ E. To use op, we first apply it to a value of the input type α and to a continuation. The continuation is a function of type β → F E (γ) that accepts a value of the output type β (the result of performing the operation) and chooses in return a computation that should be pursued next. The return type of our new computation will thus be the return type γ of the computation provided by the continuation. The continuation's computation and the new extended computation will also share the same effect signature E. This means that all uses of the operation op within the created computation have the same input and output types. 7There is a parallel between the [var] rule and the [op] rule. The [var] rule lets us use a symbol x with type α provided x : α ∈ Γ. The [op] rule lets us use a symbol op with type α →

(β → F E (γ)) → F E (γ) provided op : α β ∈ E.
The crucial difference is that contexts (Γ) are components of judgments whereas effect signatures (E) are components of types. The meaning of a variable is determined by inspecting the expression in which it occurs and finding the λ that binds it (this is known as lexical or static binding). On the other hand, the meaning of an operation in a computation is determined by evaluating the term in which the computation appears until the computation becomes the argument of a handler. This handler will then give meaning to the operation symbol by substituting it with a suitable interpretation (this kind of late binding is known as dynamic binding).

We have now seen how to construct pure computations using η and extend them by adding operations. However, before we go on and start talking about handlers, we would like to give the algebraic intuition behind [op], as the algebraic point of view makes explaining the handler rule [ ] easier.

We can see the effect signature as an algebraic signature. For every op : α β ∈ E, we have an α-indexed family of operators of arity β. Let's unpack this statement.

• First, there is the matter of having an indexed family of operators. A common example of these is the case of scalar multiplication in the algebra of a vector space. A single-sorted algebraic signature is a set of operation symbols, each of which is given an arity (a natural number). For vector addition, the arity is 2, since vector addition acts on two vectors (two elements of the domain). Scalar multiplication acts on one scalar and one vector. However, neither arity 1 nor arity 2 adequately express this. We can get around the limitations of a single-sorted signature by introducing for every scalar k an operation of arity 1 that corresponds to multiplying the vector by k. Scalar multiplication is therefore not a single operator but a scalar-indexed family of operators.

The very same strategy is applied here as well. A single operation symbol doesn't need to map to a single operator but can instead map to (possibly infinitely) many operators indexed by values of some type α. For example, writing messages to the program's output (print : string 1) can be seen as a string-indexed family of unary operators on computations. For every string s, we get an operator that maps computations c to computations that first print s and then continue as c.

• Next, we were speaking about operators of arity β. The use of a type in place of a numerical arity is due to a certain generalization. In set theory, natural numbers become sets that have the same cardinality as the number they represent (|N | = N ). We can therefore conservatively generalize the idea of arity to a set by saying that an operator of arity X takes one operand per each element of the set X. It's a short step from there to using types as arities, wherein an operator of arity β takes one operand per possible value of type β.

This will come in very handy in our system. We want our operator op to have as many operands as there are possible values in the output type β. Therefore, we simply say that the operator has arity β.

How do we write down the application of an operator of arity β to its operands? We can no longer just list out all the operands, since types in λ may have an unbounded number of inhabitants. We will organize operands in operand clusters,8 arity-indexed families of operands. We will write them down as functions, using λ-abstraction, from the arity type β to some operand type, e.g., F E (γ).

Now we can understand what it means to say that op : α β ∈ E gives rise to an α-indexed family of operators of arity β. We apply to op an index of type α to get an operator and then we apply that operator to an operand cluster of type β → F E (γ) to get a new expression of type F E (γ).

We suggest visualizing these algebraic expressions as trees (see Section 2 of [START_REF] Lindley | Algebraic effects and effect handlers for idioms and arrows[END_REF] for the original idea). Trees of type F E (α) consist of leafs containing values of type α and internal nodes labelled with operations and their parameters. Every internal node is labelled with some op : α β ∈ E and with a parameter of type α and it has a cluster of children indexed by β.

[ ]

Now we are ready to explain the handler rule. The typing rule for is repeated in Figure 2. To illustrate the constraints on the types of the components, M i and M η , of a handler, we will examine its semantics. The handler processes the algebraic expression N by recursive induction. Depending on the shape of the expression, one of the following will happen:

E = {op i : α i β i } i∈I E f E = E E f [Γ M i : α i → (β i → F E (δ)) → F E (δ)] i∈I Γ M η : γ → F E (δ) Γ N : F E (γ) [ ] Γ (op i : M i ) i∈I , η: M η N : F E (δ)
• If N = η N , then N is of type γ. This is where the M η function comes in. It must take a value of type γ and produce a new tree of type F E (δ), hence the fourth hypothesis of the rule.

• If N = op i N p (λx. N c ) for some i ∈ I, then N p must be of type α i . Furthermore, for every x : β i , we have an operand N c : F E (γ). We know this since N is of type F E (γ) and the first hypothesis tells us that op i :

α i β i ∈ E.
We will recursively apply our handler to the cluster of operands, changing their type from F E (γ) to F E (δ). We now need something which takes N p , whose type is α i , and the cluster of processed operands, type β i → F E (δ), which is exactly the function M i in the third hypothesis of the rule.

• If N = op N p (λx. N c ) and op : α β ∈ E f for some α and β, then we will ignore the node and process only its children. This means that the resulting expression will contain the operation symbol op from E f , 9 . In order for such an expression to be of the desired type F E (δ), E f must be included in E , which is what the second hypothesis of the rule guarantees.

We have covered the whole rule, except for the presence of the effect signature E . It serves two roles.

• First of all, it acts as a "free" variable over effect signatures. This means that we can give any effect signature E to the type F E (δ) of the resulting computation N as long as E contains E f (E represents the relative complement of E f in E ). This is in analogy to the free effect variable E in the [η] and [op] rules. This freedom of effect variables is a way of implementing the idea that a computation of type F E1 (α) can be used anywhere that a computation of type F E2 (α) is needed given that E 1 ⊆ E 2 .

• In the previous paragraph, why did we put the word "free" in quotation marks? Because the effect variable E is not actually free. It is the complement of E f in E and E is constrained by the types of M i and M η in the third and fourth hypotheses, respectively. The handler's clauses might themselves introduce new effects, which will in turn translate into constraints on E and E . This happens when a handler interprets an operation by making an appeal to some other operation (e.g. a handler could interpret computations using n-ary choice into computations using binary choice).

As the simplest example, we can take a handler that replaces one operation symbol with another, old: (λpc. new p (λy. c y)), η: (λx. η x) . The type scheme corresponding to the term is

F {old:α β} E f (γ) → F {new:α β} E + E f (γ).
In this scheme, α, β and γ are free meta-variables ranging over types and E f and E + range over effect signatures. The E of the rule corresponds to {new : α β} E + (i.e. E is not free, it must contain new). The handler has eliminated the old effect but it has also introduced the new effect. This concludes our exploration of the rule. We have explained it in terms of algebraic expressions and trees, using the denotational intution. We will develop the operational intuition, which talks about handlers in terms of computations and continuations, in Section 2.3, where we will give the semantics of our language using reduction rules. [cherry] Next up is the cherry operator, -• . Its type is F ∅ (α) → α and it serves as a kind of dual to the η opertator, an elimination for the F type.

M = λ op 1 (M 1 ) op 2 (M 2 ) B 2 B 1 op 1 (M 1 ) op 2 (M 2 ) A 2 A 1 C M = op 1 (M 1 ) op 2 (M 2 ) λ A 2 B 2 λ A 1 B 1
The type F ∅ (α) demands that the effect signature be empty. In such a case, the tree has no internal nodes and is composed of just a leaf containing a value of the type α. The -• operator serves to extract that value.

Another way to look at it is to say that a computation of type F ∅ (α) cannot perform any "unsafe" operations and it is therefore always safe to execute it and get the resulting value of type α.

[C]

Finally, we take a look at the C operator. The type of the operator is

(α → F E (β)) → F E (α → β).
Its input is an α-indexed family of computations and its output is a computation of α-indexed families. The operator applies only in the case when all the computations in the family share the same internal structure. By sharing the same internal structure, we mean that the trees can only differ in their leaves. What the C operator then does is to push the λ-binder down this common internal structure into the leaves. This way, we can evaluate/handle the common operations without commiting to a specific value of type α.

The action of the C operator is illustrated in Figure 3. Here, M is a function of some two-value type. It maps one value to the left subtree of λ (with leaves A i ) and the other value to the right subtree (leaves B i ). Both subtrees correspond to computations, in which a box is an operation and a circle is an atomic expression (i.e. a return value). Furthermore, op 1 has a two-value output type (arity 2) and op 2 has a one-value output type (arity 1).

Since the operations op 1 and op 2 and their arguments M 1 and M 2 are the same in both subtrees, and thus independent of the value passed to the λ, we can apply the C operator. The C pulls this common structure out of the λ and gives us a computation that produces a function.

We can also explain the action of C in operational terms. As in call-by-push-value [START_REF] Levy | Call-by-push-value: A subsuming paradigm[END_REF], we can think of abstraction over α as some effectful operation that tries to pop a value x : α off a stack. The input of C can then be seen as a continuation waiting for this x and wanting to perform some further operations. C assumes that the continuation performs operations independently of x10 and it can thus postpone popping x off the stack until after the operations dictated by the continuation have been evaluated. C is therefore a kind of commutativity law for operations and abstractions (the popping of a value off the operand stack): as long as one does not depend on the other, it does not matter whether we first perform an operation and then abstract over an argument or whether we do so the other way around. 11

Reduction Rules

We will now finally give a semantics to λ . The semantics will be given in the form of a reduction relation on terms. Even though the point of the calculus is to talk about effects, the reduction semantics will have no notion of order of evaluation; any reducible subexpression can be reduced in any context.

Before we dive into the reduction rules proper, we will first have to handle some formal paperwork, most of it due to the fact that we use variables and binders in our calculus. In order to quotient out the irrelevant distinction between terms that are the same up to variable names, we will introduce a series of definitions leading up to a notion of α-equivalence. Definition 2.1. Evaluation contexts are terms with a hole (written as []) inside. They are formally defined by the following grammar.

C ::= [] | λx. C | C N | M C | op C (λx. M c ) | op M p (λx. C) | η C | op 1 : M 1 , . . . , op n : M n , η: M η C | op 1 : M 1 , . . . , op i : C, . . . , op n : M n , η: M η N | op 1 : M 1 , . . . , op i : M i , . . . , op n : M n , η: C N | -• C | C C Definition 2.2.
Let ∼ be a binary relation on the terms of λ . We define the relation [∼], called the context closure of ∼, as the smallest relation that contains ∼ and satisfies the following closure property for any evaluation context C:

• if M [∼] M , then C[M ] [∼] C[M ]
We will be defining relations on the terms of λ that will correspond to different transformations (such as swap and the reduction rules). The notion of context closure will allow us to say that a term can be transformed by transforming any of its parts.

We are now at a point where we can easily lay down the reduction rules for λ . A reduction rule ξ will be a relation on terms. Most of the time, we will deal with their context closures, [ξ], for which we will also adopt the notation → ξ . We will also use the notation → ξ1,...,ξn for the composition → ξn • • • • • → ξ1 . The reduction relation → of λ is the union of the → ξ relations for every reduction rule ξ. We will also use the symbols and to stand for the reflexive-transitive and reflexive-symmetric-transitive closures of →, respectively. If M N , we will also say that M and N are convertible. A term which is not reducible to some other term is said to be in normal form.

We will now go through the reduction rules of λ , presented in Figure 4, one by one.

First off, we have the β and η rules. By no coincidence, they are the same rules as the ones found in STLC.

Next we have the three rules that govern the behavior of handlers. We recognize the three different rules as the three different cases in the informal denotational semantics given in Section 2.2.

• When the expression is just an atom (i.e. η N ), rule η applies the clause M η to the value N contained within.

• When the expression is an operation op j N p (λx. N c (x)) with j ∈ I, we first recursively apply the handler to every child N c (x). We then pass the parameter N p stored in the node along with the cluster of the processed children to the clause M j .

• When the expression is an operation op j N p (λx. N c (x)) but where j / ∈ I, we leave the node as it is and just recurse down on to the subexpressions (effectively using op j as the handler clause for op j ).

(λx. M ) N → rule β M [x := N ] λx. M x → rule η M where x / ∈ FV(M ) (op i : M i ) i∈I , η: M η (η N ) → rule η M η N (op i : M i ) i∈I , η: M η (op j N p (λx. N c )) → rule op M j N p (λx. (op i : M i ) i∈I , η: M η N c )
where j ∈ I and x / ∈ FV((M i ) i∈I , M η )

(op i : M i ) i∈I , η: M η (op j N p (λx. N c )) → rule op op j N p (λx. (op i : M i ) i∈I , η: M η N c ) where j / ∈ I and x / ∈ FV((M i ) i∈I , M η ) -• (η M ) → rule -• M C (λx. η M ) → rule C η η (λx. M ) C (λx. op M p (λy. M c )) → rule C op op M p (λy. C (λx. M c ))
where x / ∈ FV(M p ) By looking at these rules, we also notice that all they do is just traverse the continuations (N c ) and replace η with M η and op i with M i . This justifies thinking of η and the operation symbols as special variables which are bound to a value when being passed through a handler. This substitutability is already hinted at by the types of M η and M i in the typing rule and their correspondence with the typing rules [η] and [op], respectively.

The next rule talks about the cherry operator. It does what we would expect it to do. 12 It expects its argument to always be an atomic algebraic expression, a pure computation, and it extracts the argument that was passed to the η constructor.

Finally, we have the two rules defining the behavior of C. We remind ourselves that the goal of C is to make computations and abstractions commute by pushing λ below operation symbols and η.

• Rule C η treats the base case where the computation that we try to push λ through is a pure computation.

In that case, we just reorder the λ binder and the η operator.

• Rule C op deals with the case of the λ meeting an operation symbol. The solution is to push the C operator down through the continuation. The operation C (λx. . . . ) is applied recursively to every child M c (y). However, this strategy is sound only when M p has no free occurrence of x (which would have been bound by the λ in the redex but would become unbound in the contractum). We therefore have a constraint saying that x must not occur free in M p . Unlike the other freshness constraints, this one cannot be fixed by a simple renaming of variables. If this constraint is not met, the C will not be able to reduce.

When talking about the C operator in Section 2.2, we talked about how it applies only to families of computations that share the same internal structure (i.e. functions of x where the internal structure does not depend on x). This is reflected in the reduction rules in two ways:

-Firstly, in order for C op to kick in, the body of the function must have already reduced to something of the form op M p M c . This means that the next operation to be performed has already been determined to be op without needing to wait for the value of x.

-Secondly, the reduction can only proceed if M p does not contain a free occurrence of x. This means that M p is independent of x.

Common Combinators

Here we will introduce a collection of useful syntactic shortcuts and combinators for our calculus.

Composing Functions and Computations

First of all, to save some space and write functions in a terse "point-free" style, we introduce the composition operator (known as the B combinator in combinatory logic).

_ • _ : (β → γ) → (α → β) → (α → γ) f • g = λx. f (g x)
We will also "functionalize" our term constructors (i.e. we will write η as a shortcut for (λx. η x)). Our motive in not defining our symbols directly as function constants in the core calculus is due to the proofs of confluence and termination. A complete list of functionalized symbols is given below. 13η :

α → F E (α) π 1 : (α × β) → α η = λx. η x π 1 = λP. π 1 P op : α → (β → F E (γ)) → F E (γ) π 2 : (α × β) → β op = λpc. op p (λx. c x) π 2 = λP. π 2 P (op i : M i ) i∈I , η: M η : F E (γ) → F E (δ) inl : α → (α + β) (op i : M i ) i∈I , η: M η = λx. (op i : M i ) i∈I , η: M η x inl = λx. inl x -• : F ∅ (α) → α inr : β → (α + β) -• = λx. -• x inr = λx. inr x C : (α → F E (β)) → F E (α → β) C = λf. C f
Later on, in Section 5, we will see that our F E is a functor which, combined with some other elements, forms a monad, or equivalently, a Kleisli triple. We use a star to denote the extension of a function from values to computations, as in [START_REF] Moggi | Notions of computation and monads[END_REF], and we use = to denote the bind of a monad, as in Haskell.14

_ * : (α → F E (β)) → (F E (α) → F E (β)) f * = η: f _ = _ : F E (α) → (α → F E (β)) → F E (β) M = N = N * M
Finally, we will define a notation for applying infix operators to arguments wrapped inside computations. Let _ _ be an infix operator of type α → β → γ. Then we define the following:

_ _ : F E (α) → β → F E (γ) X y = X = (λx. η (x y)) _ _ : α → F E (β) → F E (γ) x Y = Y = (λy. η (x y)) _ _ : F E (α) → F E (β) → F E (γ) X Y = X = (λx. Y = (λy. η (x y)))
In particular, we will be using this notation for the function application operator:

_ • _ : (α → β) → α → β f • x = f x
which will yield the following combinators:

_ • _ : F E (α → β) → α → F E (β) F • x = F = (λf. η (f x)) _ • _ : (α → β) → F E (α) → F E (β) f • X = X = (λx. η (f x)) _ • _ : F E (α → β) → F E (α) → F E (β) F • X = F = (λf. X = (λx. η (f x)))
The first of the three, •, is the inverse function to C. The second, • , is the morphism component of the F E functor (which we will demonstrate in Section 5). F E is also an applicative functor [START_REF] Mcbride | Applicative programming with effects[END_REF] and the third operator in the list above, • , is the operator for application within the functor.

We also need to introduce some shortcuts to allow us to proceed faster and at a higher level of abstraction. For exemple a regular pattern is a sequences of = and * . We note η. = this rule.

Operations and Handlers

Now we will look at syntactic sugar specific to λ . In 2.4.1, we have seen the bind operator = and other ways of composing computations. Since we now have a practical way to compose computations, we can simplify the way we write effectful operations.

op! = λp. op p (λx. η x)
The exclamation mark partially applies an operation by giving it the trivial continuation η. However, we can still recover op from op! using =:

op! p = k = (λp. op p (λx. η x)) p = k → β op p (λx. η x) = k = k * (op p (λx. η x)) = η: k (op p (λx. η x)) → op op p (λx. η: k (η x)) → η op p (λx. k x)
The exclamation mark streamlines the typing rule for operations, as it is presented on the pair of rules below:

op : α β ∈ E [op] Γ op : α → (β → F E (γ)) → F E (γ) op : α β ∈ E [op!] Γ op! : α → F E (β)
We can also see that the arrow used in effect signatures gives rise to a Kleisli arrow since F E is a monad.

Handlers In Section 2.3, we have seen how the reduction rules treat unknown operation symbols: by leaving them intact. With some syntactic sugar, we can extend this behavior to the η operator as well. We will sometimes write a handler and omit giving the η clause. In that case, the η clause is presumed to be just η. 15 Schematically, we can define this piece of new syntax in the following way:

(op i : M i ) i∈I = (op i : M i ) i∈I , η: η
Finally, we will introduce a special syntax for closed handlers [START_REF] Kammar | Handlers in action[END_REF]. A closed handler is a handler that interprets the entire computation that is given as its input (it must have a clause for every operator that appears within). Since all effects are handled and none are forwarded, the codomain of the handler can be something else than a computation. However, trying to write handlers that want to exploit this possibility, implies that there is a lot of translating between α types and F ∅ (α) types that needs to be done and that clouds the inherent simplicity of a closed handler. We introduce syntax for closed handlers which takes care of this problem.

(op i : M i ) i∈I , η: M η N = -• ( (op i : (λxk. η (M i x ( -• • k)))) i∈I , η: (λx. η (M η x)) N )
As we can see, the only material added by the closed handler brackets are the functions η and -• , 16 which simply translate between the types α and F ∅ (α). Rather than closely studying the definition and scrutinizing the etas and the cherries, the idea of a closed handler is better conveyed by giving its typing rule. The following rule will be proven sound in 3.3:

E = {op i : α i β i } i∈I [Γ M i : α i → (β i → δ) → δ] i∈I Γ M η : γ → δ Γ N : F E (γ) [ ] Γ (op i : M i ) i∈I , η: M η N : δ
The lack of multiple effect signatures to implement effect forwarding makes the rule simpler than the one of :

• M η gives δ-typed interpretations to the terminal values of type γ

• M i maps the parameter of type α i and the δ-typed interpretations of the β i -indexed family of children to a δ-typed interpretation of an internal node

The η clause in a closed handler is optional. Similarly to open handlers, we will assume that γ = δ and that M η is the identity function. This is the same as saying that a closed handler without an η clause is translated into an open handler without an η clause.

(op i : M i ) i∈I N = -• ( (op i : (λxk. η (M i x ( -• • k)))) i∈I N ) = -• ( (op i : (λxk. η (M i x ( -• • k)))) i∈I , η: (λx. η x) N ) = -• ( (op i : (λxk. η (M i x ( -• • k)))) i∈I , η: (λx. η ((λx. x) x)) N ) = (op i : M i ) i∈I , η: (λx. x) N 3 Derived Rules
At the end of Section 2, in 2.4, we have introduced some new syntax for λ terms and we have translated that syntax into terms of the core λ calculus. In this section, we will give typing rules and reduction rules to these new constructions and prove their correctness.

Function Composition (•)

The first piece of syntactic sugar we have introduced was an infix symbol for function composition.

f • g = λx. f (g x)
In order to type terms containing this symbol, it will be useful to have a typing rule.

Proposition 3.1. The following typing rule is derivable in λ :

Γ M : β → γ Γ N : α → β [•] Γ M • N : α → γ Proof. Since M • N = λx. M (N x)
, we can prove the validity of this rule with the typing rule below:

Γ, x : α M : β → γ Γ, x : α N : α → β Γ, x : α x : α [app] Γ, x : α N x : β [app] Γ, x : α M (N x) : γ [abs] Γ λx. M (N x) : α → γ
x is presumed to be fresh for M and N and so we can equate Γ, x : α M : β → γ with Γ M : β → γ and the same for N .

The result of function composition is another function and functions can be applied to arguments. We can derive a reduction rule for this kind of function.

Proposition 3.2. The following reduction is derivable in λ :

(M 1 • M 2 ) N → • M 1 (M 2 N ) Proof. (M 1 • M 2 ) N = (λx. M 1 (M 2 x)) N → β M 1 (M 2 N ) 3.2 Monadic Bind ( =)
As a reminder, we give the definition of = from 2.4.1.

M = N = N * M = η: N M
First, we will prove the correct typing for =.

Proposition 3.3. The following typing rule is derivable in λ :

Γ M : F E (α) Γ N : α → F E (β) [ =] Γ M = N : F E (β)
Proof. We note that M = N = η: N M and construct the following typing derivation in λ :

Γ N : α → F E (β) [ ] Γ η: N : F E (α) → F E (β) Γ M : F E (α) [app] Γ η: N M : F E (β)
Next, we will prove the validity of two reduction rules for =.

Proposition 3.4. The following reductions are derivable in λ :

η M = N → η. = N M op M p (λx. M c ) = N → op. = op M p (λx. M c = N ) Proof. η M = N = η: N (η M ) → η N M op M p (λx. M c ) = N = η: N (op M p (λx. M c )) → op op M p (λx. η: N M c ) = op M p (λx. M c = N )

Closed Handlers

In 2.4.2, we introduced a notation for closed handlers. Even though we define closed handlers in terms of (open) handlers, their typing and reduction rules are actually simpler, since they do not have to go out of their way to support openness (i.e. passing through uninterpreted operations).

(op i : M i ) i∈I , η: M η N = -• ( (op i : (λxk. η (M i x ( -• • k)))) i∈I , η: (λx. η (M η x)) N )
We will first go through the typing rule.

Proposition 3.5. The following typing rule is derivable in λ :

E = {op i : α i β i } i∈I [Γ M i : α i → (β i → δ) → δ] i∈I Γ M η : γ → δ Γ N : F E (γ) [ ] Γ (op i : M i ) i∈I , η: M η N : δ Proof. We have (op i : M i ) i∈I , η: M η N = -• ( (op i : (λxk. η (M i x ( -• • k)))) i∈I , η: (λx. η (M η x)) N
) and we will proceed by building a typing derivation for this term.

Γ M i : α i → (β i → δ) → δ Γ, x : α i x : α i [app] Γ, x : α i M i x : (β i → δ) → δ Γ -• : F ∅ (δ) → δ Γ, k : β i → F ∅ (δ) k : β i → F ∅ (δ) [•] Γ, k : β i → F ∅ (δ) -• • k : β i → δ [app] Γ, x : α i , k : β i → F ∅ (δ) M i x ( -• • k) : δ [η] Γ, x : α i , k : β i → F ∅ (δ) η (M i x ( -• • k)) : F ∅ (δ) [abs] Γ, x : α i λk. η (M i x ( -• • k)) : (β i → F ∅ (δ)) → F ∅ (δ) [abs] Γ λxk. η (M i x ( -• • k)) : α i → (β i → F ∅ (δ)) → F ∅ (δ)
x and k are assumed to be fresh for M i .

Γ, x : γ M η : γ → δ Γ, x : γ x : γ [app] Γ, x : γ M η x : δ [η] Γ, x : γ η (M η x) : F ∅ (δ) [abs] Γ λx. η (M η x) : γ → F ∅ (δ)
x is assumed to be fresh for M η .

We can also have reduction rules for closed handlers, which work exactly the same way as the open handler reduction rules (only they do not include cases for uninterpreted operations).

Proposition 3.6. The following reductions are derivable in λ :

(op i : M i ) i∈I , η: M η (η N ) → η M η N (op i : M i ) i∈I , η: M η (op i N p (λx. N c )) → op M i N p (λx. (op i : M i ) i∈I , η: M η N c )
Proof.

(op i : M i ) i∈I , η: M η (η N ) = -• ( (op i : (λxk. η (M i x ( -• • k)))) i∈I , η: (λx. η (M η x)) (η N )) → η -• ((λx. η (M η x)) N ) → β -• (η (M η N )) → -• M η N (op i : M i ) i∈I , η: M η (op i N p (λx. N c )) = -• ( (op i : (λxk. η (M i x ( -• • k)))) i∈I , η: (λx. η (M η x)) (op i N p (λx. N c ))) → op -• ((λxk. η (M i x ( -• • k))) N p (λx. . . . N c )) → β -• ((λk. η (M i N p ( -• • k))) (λx. . . . N c )) → β -• (η (M i N p ( -• • (λx. . . . N c )))) → -• M i N p ( -• • (λx. . . . N c )) = M i N p (λx. -• ((λx. . . . N c ) x)) → β M i N p (λx. -• ( . . . N c )) = M i N p (λx. (op i : M i ) i∈I , η: M η N c )
In the above, . . . is taken to be a shortcut for (op i : (λxk. η

(M i x ( -• • k)))) i∈I , η: (λx. η (M η x)) .

Type Soundness

In Section 2, we have introduced both a type system and a reduction semantics for λ . Now we will give more substance to these two definitions by proving properties which outline the relationship between them. Types can give us two guarantees: typed terms do not get stuck and typed terms always terminate. The former property is known as progress and, in Subsection 4.2, we will show that it holds for λ as long as we abstain from using the partial function C. The latter is known as termination and its proof is more involved, so we will delay it until section 7. For both of these properties to hold, it will be essential to prove that a typed term stays typed after performing a reduction. This will be the object of the next subsection.

Subject Reduction

We now turn our attention to the subject reduction property. We can summarize subject reduction with the slogan "reduction preserves types". The rest of this section will consider a formal proof of this property for λ , but before we begin, we present a the definition of substitution and a lemma.

(M K)[x := N ] = (M [x := N ]) (K[x := N ]) x[x := N ] = N y[x := N ] = y given that x = y 19 c[x := N ] = c (op M p (λy. M c ))[x := N ] = op (M p [x := N ]) (λy. M c [x := N ]) assuming that y = x and y is fresh for N (η M )[x := N ] = η (M [x := N ]) ( (op i : M i ) i∈I , η: M η N )[x := N ] = (op i : (M i [x := N ])) i∈I , η: (M η [x := N ]) (N [x := N ]) ( -• M )[x := N ] = -• (M [x := N ]) (C M )[x := N ] = C (M [x := N ])
We are now at a point where we can easily lay down the reduction rules for λ . A reduction rule ξ will be a relation on terms. Most of the time, we will deal with their context closures, [ξ], for which we will also adopt the notation → ξ . We will also use the notation → ξ1,...,ξn for the composition

→ ξn • • • • • → ξ1 .
The reduction relation → of λ is the union of the → ξ relations for every reduction rule ξ. We will also use the symbols and to stand for the reflexive-transitive and reflexive-symmetric-transitive closures of →, respectively. If M N , we will also say that M and N are convertible. A term which is not reducible to some other term is said to be in normal form. • All the other cases end up being trivial. We follow the definition of substitution (Definition 4.1) which just applies substitution to all of the subterms. For every such subterm, we make appeal to the induction hypothesis and construct the new typing derivation.

We apply Lemma 4.2 to Γ, x : α M : τ and Γ M : α to get a typing derivation for Γ M [x := M ] : τ .

• M → η N We have M = λx. M x with x fresh for M , N = M and τ = τ 1 → τ 2 . Since Γ M : τ , we have the following:

Γ, x : τ 1 M : τ 1 → τ 2 Γ, x : τ 1 x : τ 1 [app] Γ, x : τ 1 M x : τ 2 [abs] Γ λx. M x : τ 1 → τ 2
From the inferred judgments, we can build a typing derivation for the redex.

Γ M p : α Γ, x : β M c : F E (γ) . . . [ ] Γ, x : β (op i : M i ) i∈I , η: M η M c : F E (δ) op : α β ∈ E [op] Γ op M p (λx. (op i : M i ) i∈I , η: M η M c ) : F E (δ) • M → -• N In this case, M = -• (η M ) and N = M . Γ M : τ [η] Γ η M : F ∅ (τ ) [ -• ] Γ -• (η M ) : τ
We immediately get Γ M : τ , which is the sought after typing derivation of the redex.

• M → Cη N M = C (λx. η M ), N = η (λx. M ) and τ = F E (γ → δ). Γ, x : γ M : δ [η] Γ, x : γ η M : F E (δ) [abs] Γ λx. η M : γ → F E (δ) [C] Γ C (λx. η M ) : F E (γ → δ)
From these judgments, we build a type for the redex.

Γ, x : γ M : δ [abs] Γ λx. M : γ → δ [η] Γ η (λx. M ) : F E (γ → δ) • M → Cop N M = C (λx. op M p (λy. M c )), N = op M p (λy. C (λx. M c )) and τ = F E (γ → δ). Γ, x : γ M p : α Γ, x : γ, y : β M c : F E (δ) op : α β ∈ E [op] Γ, x : γ op M p (λy. M c ) : F E (δ) [abs] Γ λx. op M p (λy. M c ) : γ → F E (δ) [C] Γ C (λx. op M p (λy. M c )) : F E (γ → δ)
With the judgments above, we build the derivation below.

Γ M p : α Γ, y : β, x : γ M c : F E (δ) [abs] Γ, y : β λx. M c : γ → F E (δ) [C] Γ, y : β C (λx. M c ) : F E (γ → δ) op : α β ∈ E [op] Γ op M p (λy. C (λx. M c )) : F E (γ → δ)
In the above we get Γ M p : α from Γ, x : γ M p : α and the rule's condition that x / ∈ FV(M p ).

•

C[M ] → C[N ]
The reduction relation of λ is defined as the context closure of the individual reduction rules. We have covered the rules themselves, we now address the context closure. By induction hypothesis, we know that the reduction from M → N preserves types, i.e. for any ∆ and α such that ∆ M : α, we have ∆ N : α. We observe that the typing rules of λ (Figure 1) are compositional, meaning that the type of a term depends only on the types of its subterms, not on their syntactic form. We can check this easily by looking at the premises of all of the typing rules. For every immediate subterm T , there is a premise ∆ T : α where T is a metavariable. We can therefore replace T and its typing derivation by some other T with ∆ T : α. Since the typing rules of λ are compositional, we can replace the ∆ M : α in Γ C[M ] : τ by ∆ N : α and get Γ C[N ] : τ .

We have proven subject reduction for core λ . The syntax, semantics and types that we have introduced for sums and products are standard. Their proofs of subject reduction carry over into our setting as well.

Progress

Progress means that typed terms are never stuck. Among the terms of λ , we will have to identify terms which are acceptable stopping points for reduction. Progress will mean that if a term is not in one of these acceptable positions, then there must be a way to continue reducing. The term we will use for these acceptable results is value. Definition 4.4. A λ term is a value if it can be generated by the following grammar:

V ::= λx. M | op V (λx. M ) | η V
where M ranges over λ terms.

The above definition reflects the intuition that λ consists of functions and computations, where functions are built using λ and computations using op and η. The other syntactic constructions (application, , -• and C) all have rules which are supposed to eventually replace them with other terms. As with subject reduction, before we proceed to the main property, we start with a lemma. Lemma 4.5. Value classification Let V be a closed well-typed value (i.e. ∅ V : τ ). Then the following hold:

• if τ = α → β, then V = λx. M • if τ = F E (α), then either V = op V p (λx. M c ) or V = η V Proof. • Assume τ = α → β. If V = op V p (λx. M c ) or V = η V , then τ must be a computation type F E (γ),
which is a contradiction. The only remaining possibility is therefore V = λx. M .

• Assume τ = F E (α). If V = λx. M , then τ must be a function type β → γ, which is a contradiction. The only remaining possibilities are therefore

V = op V p (λx. M c ) or V = η V .
Property 4.6. Progress Every closed well-typed term M from λ without C and constants20 is either a value or is reducible to some other term.

Proof. We will proceed by induction on M .

• M = λx. M Then M is already a value.

• M = x Impossible, since M must be a closed term.

• M = M 1 M 2 By induction hypothesis, M 1 and M 2 are either values or reducible terms. If either one is reducible, then our term is reducible as well and we are done. If neither is reducible, then they are both values. Since M is a closed well-typed term (i.e. ∅ M : τ ), then M 1 : α → τ for some α. Thanks to Lemma 4.5, we have that M 1 = λx. M 1 . This means that M = (λx. M 1 ) M 2 and M is therefore reducible with β.

• M = op M p (λx. M c ) By induction hypothesis, M p is either reducible or a value. If M p is reducible, then so is M . If it is a value, then so is M as well.

• M = η N The same argument as for op. By induction hypothesis N is reducible or a value and therefore the same holds for M .

• M = (op i : M i ) i∈I , η: M η N By induction hypothesis, N is either a value or it is itself reducible. If it is reducible, then so is M . If it is not, then it must be a (closed) value. The type of N is a computation type F E (α) and so by Lemma 4.5, it must either be op

V p (λx. M c ) or η V . If N = op V p (λx. M c ), then (op i : M i ) i∈I , η: M η (op V p (λx. M c )
) is reducible by op or op (depending on whether or not

op ∈ {op i } i∈I ). Otherwise, if N = η V , then (op i : M i ) i∈I , η: M η (η V ) is reducible by η . • M = -•
N By induction hypothesis, N is either reducible or a value. As before, we only have to focus on the case when N is a value. From Lemma 4.5, we know that N = op V p (λx. M c ) or N = η V . However, we can rule out the former since we know that ∅ N : F ∅ (α), meaning that op is not in the empty effect signature ∅. We therefore end up with -• (η V ), which is reducible by -• .

We have shown progress for λ without C. It is easy to see that we cannot do better, as the C operator can violate progress and get us stuck quite easily. Observation 4.7. There exists a closed well-typed term M from λ without constants that is neither a value nor reducible to some other term.

Proof. The most trivial example is C (λx. x). The computation that is performed by the body of the function λx. x is entirely determined by the parameter x. It is therefore not possible to pull out this structure outside of the function. Therefore, applying the C operator to this function is undefined and evaluation gets stuck.

Algebraic Properties

In this section, we will clarify what we mean when we say that the F E (α) computation types form a functor/applicative functor/monad and we will prove that the constructions in λ conform to the laws of these algebraic structures. The object on which we will build these mathematical structures will be the meanings of λ terms. We will therefore start by building an interpretation for λ , a denotational semantics. Then we will be in measure to define the algebraic structures mentioned above and verify that their laws are satisfied.

Denotational Semantics

We start by identifying the domains of interpretation. For each type, we designate a set such that all terms having that type will be interpreted in that set. Before we do so, we introduce some notation on sets. Notation 5.1. Let A and B be sets. Then:

• A B is the set of functions from B to A • A × B is the cartesian product of A and B • A B is the disjoint union of A and B 21
• A ⊥ is the disjoint union of A and {⊥} Definition 5.2. Given a set A ν for every atomic type ν, the interpretation of a type τ is a set τ defined inductively by:

ν = (A ν ) ⊥ α → β = ( α → β ) ⊥ F E (γ) = ( γ op:α β∈E α × F E (γ) β ) ⊥
Note that F E (γ) is recursively defined not only by induction on the type itself but also by its use of F E (γ) on the right hand side. Formally, we take F E (γ) to be the least fixed point of the monotone functional F (X) = ( γ op:α β∈E α × X β ) ⊥ , whose existence is guaranteed by the Knaster-Tarski theorem [START_REF] Knaster | Un théoreme sur les fonctions d'ensembles[END_REF][START_REF] Tarski | A lattice-theoretical fixpoint theorem and its applications[END_REF].

Notation 5.3. We will use λ notation to write down elements of α → β :

• λx. F (x) ∈ α → β when F (x) ∈ β for every x ∈ α • ⊥ ∈ α → β
We will use the following syntax to write down elements of F E (γ) :

• η(x) ∈ F E (γ) with x ∈ γ • op(p, c) ∈ F E (γ) with op : α β ∈ E, p ∈ α and c ∈ F E (γ) β • ⊥ ∈ F E (γ)
The definition of τ follows the definition of a value (Definition 4.4): function types denote functions and computation types either denote atomic algebraic expressions (η) or applications of algebraic operations (op). In the denotational semantics, we also take care of the fact that terms can get stuck and fail to yield the expected value. We represent this by adding the element ⊥ to the interpretation of every type. Definition 5.4. We define the interpretation of a typing context Γ as the set Γ of functions that map every x : α ∈ Γ to an element of α .

We will call these functions valuations. We will use the notation e[x := f ] to stand for the extension of e with x → f . The domain of the extension is dom(e) ∪ x. The extension maps x to f and every other variable in its domain to e(x).

(op i : M i ) i∈I , η: M η N (e) = (op i : M i ) i∈I , η: M η (e)( N (e)) -• M (e) = x, if M (e) = η(x) ⊥, otherwise C M (e) = C ( M (e))
Definition 5.6. The interpretation of a handler (op i : M i ) i∈I , η: M η within a valuation e (also written as (op i : M i ) i∈I , η: M η (e)) is the function h defined inductively by:

h(η(x)) = M η (e)(x), if M η (e) is a function ⊥, otherwise h(op j (p, c)) =      M j (e)(p)(λx. h(c(x))
), if j ∈ I, and M j (e) and M j (e)(p) are both functions

op j (p, λx. h(c(x))), if j / ∈ I ⊥, otherwise h(⊥) = ⊥
The equations defining h use h on the right-hand side. Nevertheless, h is well-defined since we can rely on induction. There is a well-founded ordering on the elements of F E (γ) , where ∀x. op(p, c) > c(x). The monotonic functional

F (X) = ( γ op:α β∈E α ×X β ) ⊥ used in defining F E (γ) (Definition 5.
2) is also Scott-continuous (i.e. it is both monotonic and it preserves suprema). By Kleene fixed-point theorem [START_REF] Kleene | Introduction to metamathematics[END_REF], we have that the least fixed point of F is the supremum of the series ∅ ⊆ F (∅) ⊆ F (F (∅)) ⊆ . . .. Let the rank of x be the smallest n such that x ∈ F n (∅). The ordering < r , defined as x < r y whenever rank(x) < rank(y), is a well-founded ordering. It is also the inductive ordering that we were looking for. Whenever rank(op(p, c)) = n, then c is a function whose codomain is F n-1 (∅) and therefore ∀x. op(p, c) > r c(x).

Definition 5.7. The interpretation of the C operator is a function g defined inductively by:

g(f ) =      η(h), if f is a function and ∃h. ∀x. f (x) = η(h(x)) op(p, λy. g(λx. c(x)(y))), if f is a function and ∃op, p, c. ∀x. f (x) = op(p, c(x)) ⊥, otherwise
As with Definition 5.6, we have to show that this is actually a valid definition since we are using g on the right-hand side of an equation defining g. This time around, the arguments to g are functions whose codomain is the interpretation of some computation type F E (β). We can extend a well-founded ordering on the set F E (β) to a well-founded ordering on α → F E (β) by stating that f < g whenever f and g are both functions (not ⊥) and ∀x ∈ α . f (x) < g(x).

We have to show that the recursive call to g in the definition above is performed on an argument which is smaller than the original function. Let f = λx. c(x)(y) be the function to which we recursively apply g. We have that f (x) = op(p, c(x)) and f (x) = c(x)(y). We know that ∀y. op(p, c(x)) > c(x)(y), since that is the property of the well-founded ordering on the elements of F E (γ) established above. Therefore, we have that ∀x ∈ α . f (x) > f (x) and so f > f . This was the entire definition of our denotational semantics. 23 We will now compare it to the reduction semantics introduced in 2.3. Proof. The property relies on two facts: that our denotational semantics is compositional, which means that the context closure of reduction rules preserves denotations, and that every individual reduction preserves denotations. To prove so for the β rule is a matter of proving a lemma stating that M (e[x := N (e)]) = M [x := N ] (e), which follows from the compositionality of the denotational semantics. For all the other rules, it suffices to use the definition of interpretation (Definition 5.5) to calculate the denotation of both the left-hand side and the right-hand side and verify that they are the same object.

We see that equalities from the reduction semantics are carried over to the denotational semantics. The converse, however, is not the case. Observation 5.9. Incompleteness of reduction w.r

.t. denotations

There exist terms M and N in λ such that M = N but M and N are not convertible.

Proof. Consider a stuck term such as M = C (λx. x) and another term N = M = (C (λx. x)). Neither one of these two terms is reducible and neither one is a value. They are stuck and the denotational semantics assigns the value ⊥ to both of them, therefore M = N . However, as a consequence of confluence (coming up in section 6), a pair of different normal terms is never convertible, and therefore M and N are not convertible.

And this concludes the definition of the denotational semantics of λ . Throughout most of the article, we will be using the reduction semantics introduced in 2.3, even though it is incomplete, since it allows us to simplify terms in a mechanical and transparent step-by-step manner. However, the denotational semantics will be useful to us in the rest of this section since it will let us access extra equalities needed to prove some general laws.

Category

We aim to show that the computation types in λ form a monad. All these terms are defined w.r.t. some category and so we will start by introducing the category underlying λ .

We will be working with a particular category, which we will call λ . The λ category consists of:

objects: the types of the λ calculus arrows: for any two types α and β, the arrows from α to β are the functions from α to β composition: composition of arrows is defined as composition of functions identities: for every type α, we define id α as the identity function with domain α

Since the arrows in our category are functions, the three laws of a category (associativity, left identity and right identity) fall out of the same properties for functions. Since the arrows in our category are functions, the three laws of a category (associativity (??), left identity (??) and right identity (??)) fall out of the same properties for functions.

The Three Laws

Monads form a subset of applicative functors which in turn is a subset of functors. Instead of incrementally building up from a functor all the way to a monad, it will end up being more practical to first prove the monad laws and then illustrate how they let us verify the functor and applicative functor laws. Therefore, we first define our monadic bind operator and prove the three monad laws. Definition 5.10. Let X be from F E (α) and f be a function from α to F E (β) . We define X = f inductively on the structure of X:

op(p, c) = f = op(p, λx. c(x) = f ) η(x) = f = f (x) ⊥ = f = ⊥ Note that X = f is equivalent to x = y ([x → X, y → f ]).
Law 5.11. (Associativity of =) Let X be from F E (α) , f be a function from α to F E (β) and g be a function from β to F E (γ) . Then the following equation holds:

(X = f ) = g = X = (λx. f (x) = g) Proof.
Proof by induction on the well-founded structure of X:

• X = ⊥ (⊥ = f ) = g = ⊥ = g = ⊥ = ⊥ = (λx. f (x) = g) • X = η(x) (η(x) = f ) = g = f (x) = g = (λx. f (x) = g)(x) = η(x) = (λx. f (x) = g) • X = op(p, c) (op(p, c) = f ) = g = op(p, λy. c(y) = f ) = g = op(p, λy. (c(y) = f ) = g) = op(p, λy. c(y) = (λx. (f (x) = g)))
= op(p, c) = (λx. f (x) = g) Law 5.12. (Left identity for =) Let η(x) be from F E (α) and f be a function from α to F E (β) . Then the following holds:

η(x) = f = f (x)
Proof. Follows immediately from the definition of = (Definition 5.10).

Law 5.13. (Right identity for =) Let X be from F E (α) . Then the following holds:

X = (λx. η(x)) = X
Proof. By induction on the structure of X:

• X = ⊥ ⊥ = (λx. η(x)) = ⊥ • X = η(x) η(x) = (λx. η(x)) = (λx. η(x))(x) = η(x) • X = op(p, c) op(p, c) = (λx. η(x)) = op(p,
F (α) → (α → F (β)) → F (β)
, polymorphic in α and β. These objects must also satisfy the following laws:

(X = f ) = g = X = (λx. f (x) = g) (Associativity) (1)
η(x) = f = f (x) (Left identity) (2)
X = η = X (Right identity) (3)
To understand why the laws look the way they do, we will consider functions of type α → F (β). These are the kinds of functions one might use to model call-by-value [START_REF] Moggi | Notions of computation and monads[END_REF][START_REF] Moggi | An abstract view of programming languages[END_REF]: we take a value α and then yield some computation F (β). Now assume we would use this type of functions to model procedures of input type α and output type β and we would want these procedures to form a category. For every type α, we would like an identity procedure with input type and output type α, therefore a function of type α → F (α). The polymorphic η combinator will be this identity procedure. We would also like to be able to compose a procedure from α to β with a procedure from β to γ, i.e. compose functions of types α → F (β) and β → F (γ). When composing f : α → F (β) with g : β → F (γ), we run into the problem of having some f (x) : F (β) and g : β → F (γ) that we cannot compose. This is where = comes in and composes these two values for us. Let f >= > g = λx. f (x) = g be the resulting composition operator. In order for this structure to be a category, it needs to satisfy the following:

(f >= > g) >= > h = f >= > (g >= > h) η >= > f = f f >= > η = f
By taking f to be the constant function that returns X, we end up with the laws of the monad. Conversely, with the principle of extensionality [START_REF] Balat | Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums[END_REF], we can derive these laws from the monad laws. Therefore F, η, = forms a monad whenever the derived >= > and η form a category. This kind of category is called a Kleisli category and the particular presentation of a monad that we have given here is known as a Kleisli triple. To prove that F E is a monad will be trivial: we have already done so! The η combinator is of course our η and = is our =. The three laws that we need to verify are three laws that we have introduced in 5.3 and have been using throughout this section. Monads have been introduced to natural language semantics by Chung-chieh Shan in 2002 [START_REF] Shan | Monads for natural language semantics[END_REF]. Since then, they have seen occasional use, mostly to handle dynamics without burdening the semantics with context/continuation passing [START_REF] Unger | Dynamic semantics as monadic computation[END_REF][START_REF] Champollion | Back to events: More on the logic of verbal modification[END_REF], but also other phenomena such as conventional implicature/opacity [START_REF] Giorgolo | Multidimensional semantics with unidimensional glue logic[END_REF][START_REF] Giorgolo | Monads for conventional implicatures[END_REF][START_REF] Giorgolo | Monads as a solution for generalized opacity[END_REF]. The challenge of combining different phenomena which rely on different monads has been tackled from two angles: using distributive laws for monads [START_REF] Giorgolo | Natural language semantics with enriched meanings[END_REF] and using monad transformers [START_REF] Charlow | On the semantics of exceptional scope[END_REF][START_REF] Barker | Monads for natural language[END_REF]. In the λ calculus, the monadic operations η and = are available as the η constructor and the = combinator introduced in 2.4.1.

Confluence

The object of our study during this section will be the proof of the confluence property of λ . Informally, it means that a single term cannot reduce to two or more different results. Together with the termination from Section 7, this will give us the property that every term yields exactly one result and does so in a finite amount of steps (a property known as strong normalization). Confluence also gives us a strong tool to prove an inequality on terms. If two terms reduce to different normal forms, confluence guarantees us that they are not convertible. Proofs of this property are often mechanical and follow the same pattern. Our strategy will be to reuse a general result which applies one such proof for a general class of rewriting systems. Our rewriting system is a system of reductions on terms and the reductions have side conditions concerning the binding of free variables. A good fit for this kind of system are the Combinatory Reduction Systems (CRSs) of Klop [START_REF] Klop | Combinatory reduction systems: introduction and survey[END_REF].

The main result about CRSs that we will make use of is the following (Corollary 13.6 in [START_REF] Klop | Combinatory reduction systems: introduction and survey[END_REF]). Theorem 6.2. Confluence of orthogonal CRSs Every orthogonal CRS is confluent.

We will model λ as a CRS. However, η-reduction will deny us orthogonality. We will therefore first prove confluence of λ without η-reduction and then we will manually show that confluence is preserved on adding η-reduction back. Notation 6.3. The intensional λ calculus λ -η is the λ calculus without the η-reduction rule.

The rest of this section will go like this:

• CRS: a formalism for higher-order rewriting (6.1)

• λ is a CRS (6.2)

• Klop et al [93]: Every orthogonal CRS is confluent (6.3)

λ -η is an orthogonal CRS ⇒ λ -η is confluent (Lemma 6.12) η is an orthogonal CRS ⇒ η is confluent (Lemma 6.13)

• λ -η + η is confluent (6.4, Theorem 6.18) -because λ -η and η commute (Lemma 6.17)

Combinatory Reduction Systems

A Combinatory Reduction System is defined by an alphabet and a set of rewriting rules. We will first cover the alphabet. Definition 6.4. A CRS alphabet consists of:

• a set Var of variables (written lower-case as x, y, z,. . . )

• a set MVar of metavariables (written upper-case as M , N , . . . ), each with is own arity • a set of function symbols, each with its own arity Let us sketch the difference between the variables in Var and the metavariables in MVar. The variables in Var are the variables of the object-level terms, in our case it will be the variables of λ . The variables in MVar are the metavariables that will occur in our reduction rules and which we will have to instantiate in order to derive specific application of those rules. In other words, the variables in Var are there to express the binding structure within the terms being reduced and the metavariables in MVar are there to stand in for specific terms when applying a reduction rule. Definition 6.5. The metaterms of a CRS are given inductively:

• variables are metaterms • if t is a metaterm and x a variable, then [x]t is a metaterm called abstraction • if F is an n-ary function symbol and t 1 ,. . . ,t n are metaterms, then F (t 1 , . . . , t n ) is a metaterm

• if M is an n-ary metavariable and t 1 ,. . . ,t n are metaterms, then M (t 1 , . . . , t n ) is a metaterm Definition 6.6. The terms of a CRS are its metaterms which do not contain any metavariables.

To finish the formal introduction of CRSs, we give the definition of a CRS reduction rule. Definition 6.7. A CRS reduction rule is a pair of metaterms s → t such that:

• s and t are both closed, i.e. all variables are bound using the [_]_ abstraction binder • s is of the form F (t 1 , . . . , t n )

• all the metavariables that occur in t also occur in s

• any metavariable M that occurs in s only occurs in the form M (x 1 , . . . , x k ), where x i are pairwise distinct variables Definition 6.8. A Combinatory Reduction System (CRS) is a pair of a CRS alphabet and a set of CRS reduction rules.

We will only sketch the way that a CRS gives rise to a reduction relation and we will direct curious readers to Sections 11 and 12 of [START_REF] Klop | Combinatory reduction systems: introduction and survey[END_REF]. When we instantiate the metavariables in a CRS rule, we use a valuation that assigns to every n-ary metavariable a term with holes labelled from 1 to n. The instantiation of M (t 1 , . . . , t n ) then replaces the metavariable M using the valuation and then fills the holes labelled 1, . . . , n with the terms t 1 , . . . , t n respectively. The crucial detail is that in a particular context, a metavariable can only be instantiated with terms M that do not contain any free variables bound in that context. This means that for the instantiation of M to contain a variable bound in its context, M must explicitly take that variable as an argument. All other variables not explicitly declared can therefore be safely assumed to not occur freely within M . Consider the following examples of β and η-reduction.

(λx. M (x)) N → M (N ) λx. N x → N
More formally written as:

@(λ([x]M (x)), N ) → M (N ) λ([x]@(N, x)) → N
where λ is a unary function symbol and @ is a binary function symbol. In both of the versions, M is a unary metavariable and N is a nullary metavariable. In the rule for β-reduction, we can observe how the idea of instantiating metavariables by terms with holes lets us express the same idea for which we had to introduce the meta-level operation of substitution. In the rule for η-reduction, we see that N appears in a context where x is bound but it does not have x as one of its arguments. Therefore, it will be impossible to instantiate N in such a way that it contains a free occurrence of x. In both of those rules, we were able to get rid of meta-level operations (substitution) and conditions (x / ∈ F V (N )) and have them both implemented by the formalism itself.

6.2

λ as a CRS We will now see how to rephrase the reduction rules of λ in order to fit in to the CRS framework. We have already seen how to translate the β and η rules in the previous subsection. The next rules to address are the rules defining the semantics of the handlers. We will repeat the rules for handlers to make the issue at hand clear.

(op i : M i ) i∈I , η: M η (η N ) → rule η M η N (op i : M i ) i∈I , η: M η (op j N p (λx. N c )) → rule op M j N p (λx. (op i : M i ) i∈I , η: M η N c )
where j ∈ I and x / ∈ FV((M i ) i∈I , M η )

(op i : M i ) i∈I , η: M η (op j N p (λx. N c )) → rule op op j N p (λx. (op i : M i ) i∈I , η: M η N c ) where j / ∈ I and x / ∈ FV((M i ) i∈I , M η )
The syntax of CRSs does not allow us to use the (op i : M i ) i∈I notation nor capture the j ∈ I or j / ∈ I conditions. The symbols op i are problematic as well, since technically, they are not concrete λ syntax but metavariables standing in for operation symbols. We do away with all of the above problems by expanding these meta-notations and adding a separate rule for every possible instantiation of the schema. This means that for each sequence of distinct operation symbols op 1 ,. . . ,op n , we end up with: • for every op ∈ E \ {op i 1 ≤ i ≤ n}, a special rewriting rule

op 1 : M 1 , . . . , op n : M n , η: M η (op N p (λx. N c (x))) → op N p (λx. op 1 : M 1 , . . . , op n : M n , η: M η N c (x))
The rule for the cherry -• extraction operator is already in CRS form, so all we have to do is address the rules for the C operator. We present them side-by-side in their original form and in CRS-style. Original:

C (λx. η M ) → η (λx. M ) C (λx. op M p (λy. M c )) → op M p (λy. C (λx. M c )) where x / ∈ FV(M p )
CRS-style:

C (λx. η (M (x))) → η (λx. M (x)) C (λx. op M p (λy. M c (x, y))) → op M p (λy. C (λx. M c (x, y)))
We can see that the only difference is to replace "simple" metavariables M , M p and M c with their higher-order versions: the unary M , nullary M p and binary M c . We see that every CRS metavariable is applied to the variables in its scope, except for M p , which thus loses access to the variable x. This way, the condition that x must not appear free in M p is now encoded directly in the reduction rule itself. In 6.1, we have said that a CRS is formed by a set of reduction rules and by an alphabet. We have already seen all of the rules of our CRS (β and η were given at the end of 6.1 and the -• rule is the same as the original one in 2.3). In order to have a complete definition, all that remains is to identify the alphabet. The set of variables V ar is exactly the set of variables X used in the definition of λ . The set of metavariables M V ar consists of the unary M , nullary N , nullary N p , unary N c , nullary M p , binary M c , nullary M i and nullary M η . The set of function symbols is composed of the following:

• the binary symbol @ for function application In giving the CRS-style reduction rules above, we have used the "native" syntax of λ instead of writing out everything in terms of function symbols. For clarity, we give the rules governing the relationship of the two. We write:

• @(t, u) as t u

• λ([x]t) as λx. t • η(t) as η t • op(t p , [x]t c ) as op t p (λx. t c ) 24
• ( op 1 : _, . . . , op n : _, η: _ _)(t 1 , . . . , t n , t η , u) as op 1 : t 1 , . . . , op n : t n , η: t η u

• -• (t) as -• t • C(t) as C t
We have connected the terms of λ with CRS terms and we have also expressed all of our reduction rules in terms of CRS reduction rules. As in λ , CRS then proceeds to take a context closure of this redex-contractum relation. Our translation from λ to a CRS also preserves subterms 25 and so we end up constructing the same reduction relation.

Orthogonal CRSs

In order to use Theorem 6.2, we need to show that our CRS is orthogonal, so let us start us by looking at what "orthogonal" means in the context of CRSs. Definition 6.9. A CRS is orthogonal if it is non-overlapping and left-linear.

We will need to satisfy two criteria: no overlaps and left linearity. We will start with the latter. Definition 6.10. A CRS is left-linear if the left-hand sides of all its reduction rules are linear. A CRS metaterm is linear if no metavariable occurs twice within it.

By going through the rules we have given in 6.2, we can see at a glance that no rule uses the same metavariable twice in its left-hand side and so our CRS is indeed left-linear. Definition 6.11. A CRS is non-overlapping if:

• Let r = s → t be some reduction rule of the CRS and let M 1 ,. . . ,M n be all the metavariables occurring in the left-hand side s. Whenever we can instantiate the metavariables in s such that the resulting term contains a redex for some other rule r , then said redex must be contained in the instantiation of one of the metavariables M i .

• Similarly, whenever we can instantiate the metavariables in s such that the resulting term properly contains a redex for the same rule r, then that redex as well must be contained in the instantiation of one of the metavariables M i .

In simpler words, no left-hand side of any rule can contain bits which look like the top of the left-hand side of some other rule. Let us try and verify this property in λ :

• The rules have no overlaps with any of the other rules. Their left-hand sides are constructed only of the symbols and the op and η constructors. Since there is no reduction rule headed by op and η, they have no overlap with any of the other rules. Furthermore, the three rules are mutually exclusive, so there is no overlap between themselves.

• The -• rule does not overlap with any of the other neither, since the left-hand side contains only -• and η, and there is no reduction rule headed by η.

• The C rules are both mutually exclusives, so there is no overlap between the two. However, their lefthand sides are built not only out of C, op and η, but also of λ, for which there is the η-reduction rule. Fortunately, in this case, the C rules only apply when the λ-abstraction's body is an η expression or an op expression, whereas the η rule applies only when the body is an application expression. 26 Therefore, there is no overlap.

We have established that all the reduction rules in our system are pairwise non-overlapping except for β and η. However, these two have a notorious overlap. We can instantiate the metavariables in the left-hand side of the β rule to get a term which contains an η-redex which shares the λ-abstraction with the β-redex.

(λx. y x) z

We can also instantiate the metavariables in the left-hand side of the η rule to create a β-redex which shares the application with the η-redex. λx. (λz. z) x

Because of these overlaps, the λ CRS is therefore not orthogonal. However, we can still make good use of Theorem 6.2. Lemma 6.12. Confluence of λ -η The λ reduction system without the η rule is confluent.

Proof. If we exclude the η rule, we have a CRS which is left-linear and also non-overlapping. 27 Therefore, it is orthogonal and thanks to Theorem 6.2, also confluent. Lemma 6.13. Confluence of η-reduction The reduction system on λ terms containing only the ηreduction rule is confluent. 28Proof. We have seen that η is a valid left-linear CRS rule. It also does not overlap itself since its left-hand side does not contain any λ subexpression. The CRS consisting of just the η rule is therefore orthogonal and confluent.

Putting η Back in λ

We have shown that both λ -η and η are confluent. The reduction relation of the complete λ calculus is the union of these two reduction relations. Using the Lemma of Hindley-Rosen (1.0.8.( 2) in [START_REF] Klop | Term rewriting systems[END_REF]), we can show that this union is confluent by showing that the two reduction relations commute together. Definition 6.14. Let → 1 and → 2 be two reduction relations on the same set of terms A. → 1 and → 2 commute if for every a, b, c ∈ A such that a 1 b and a 2 c, there exists a d ∈ A such that b 2 d and c 1 d. Lemma 6.15. Lemma of Hindley-Rosen [START_REF] Klop | Term rewriting systems[END_REF] Let → 1 and → 2 be two confluent reduction relations on the same set of terms. If → 1 and → 2 commute, then the reduction relation → 1 ∪ → 2 is confluent.

We will not be proving the commutativity directly from the definition. Instead, we will use a lemma due to Hindley (1.0.8.( 3) in [START_REF] Klop | Term rewriting systems[END_REF]). Lemma 6.16. Let → 1 and → 2 be two reduction relations on the same set of terms A. Suppose that whenever there are a, b, c ∈ A such that a → 1 b and a → 2 c, there is also some

d ∈ A such that b 2 d and c → = 1 d (meaning c → 1 d or c = d).
In that case, → 1 commutes with → 2 . [START_REF] Klop | Term rewriting systems[END_REF] We can use this to prove that λ -η commutes with the η-reduction rule. Lemma 6.17. Commutativity of η and λ -η The reduction relations induced by η and by the rest of the λ rules commute.

Proof. We will prove this lemma by an appeal to Lemma 6.16. Let → η be the reduction relation induced by the rule η and → λ -η the reduction relation induced by all the other reduction rules in λ . We need to prove that for all terms a, b and c where a → λ -η b and a → η c, we have a term d such that b η d and c → = λ -η d. This will turn out to be a routine proof by induction on the structure of the term a. The base cases are trivial since terms without any proper subterms happen to have no redexes in λ and therefore trivially satisfy the criterion. In the inductive step, we will proceed by analyzing the relative positions of the redexes which led to the reductions a → λ -η b and a → η c. • If the redex in a → λ -η b is the entire term a, but the redex in a → η c is a proper subterm of a: We will solve this by case analysis on the form of a:

-If a is an application: Since a is an application and also a λ -If a is any other kind of term: Let l → r be the rule used in a → λ -η b. Not counting β, which only acts on applications and which we dealt with just above, the rules of λ -η do not overlap with the η rule. This means the η-redex which led to c must lie entirely inside a part of l which corresponds to a metavariable. Let M be that metavariable, then we will decompose l into L(M ) • If the redex in a → η c is the entire term a, but the redex in a → λ -η b is a proper subterm of a: In this case, a must be an abstraction that matches the left-hand side of the η rule, i.e. a = λx. N x. Also, we have c = N .

-As before, we will first deal with the case when the λ -η -redex is contained completely within • If a is the redex for both reductions a → λ -η b and a → η c, then a must match the left-hand side of a λ -η rule and the η rule. However, this is impossible since the left-hand side of the η rule is headed by abstraction, which is the case for none of the rules of λ -η .

Equipped with this lemma, we can go on to prove our main result, Theorem 6.18, the confluence of λ .

Theorem 6.18. Confluence of λ

The reduction relation → on the set of λ terms, defined by the reduction rules in 2.3, is confluent.

Proof. From Lemma 6.12, we know that the λ -η system is confluent and from Lemma 6.13, we know that the η-reduction rule is confluent as well. Lemma 6.17 tells us that these two reduction systems commute and therefore, by Lemma 6.15, their union, which is the λ reduction system, commutes as well.

7 Termination Definition 7.1. A reduction relation is terminating if there is no infinite chain M 1 → M 2 → . . ..

In this section, we will prove termination with a similar strategy as the one we employed for confluence. λ is an extension of the λ-calculus with computation types and some operations on computations. Our computations can be thought of as algebraic expressions, i.e. they have a tree-like inductive structure. The reason that all computations in λ terminate is that the operations defined on computations rely on wellfounded recursion. However, it is quite tricky to go from this intuition to a formal proof of termination. Fortunately, we can rely on existing results. Blanqui, Jouannaud and Okada have introduced Inductive Data Type Systems (IDTSs) [START_REF] Blanqui | Inductive-data-type systems[END_REF][START_REF] Blanqui | Termination and confluence of higher-order rewrite systems[END_REF]. Like CRSs, IDTSs are a class of rewriting systems for which we can prove certain interesting general results. In this section, we will start by examining the definition of an IDTS and fitting λ into that definition. The theory of IDTSs comes with a sufficient condition for termination known as the General Schema. λ will not satisfy this condition and so we will first transform it using Hamana's technique of higher-order semantic labelling [START_REF] Hamana | Higher-order semantic labelling for inductive datatype systems[END_REF]. As with our proof of confluence, we will first consider the case of λ without η-reduction and then add η manually while preserving termination. The plan will look like this:

• IDTS = Typed CRS (7.1)

• The λ τ IDTS (7.2) 29 Since our rules are left-linear, M is guaranteed to appear in L(M ) at most once. Therefore, if a →η a in one step, then also L(a ) →η L(a ) in one step as well. 30 a can occur multiple times in R(a ) when the rule l → r is duplicating (which is actually the case for the op rules). However, we are able to go from R(a ) to R(a ) in multiple steps. NB: This is why we use Lemma 6.16 instead of trying to prove commutativity directly.

The definition of an IDTS rewrite rule is almost identical to the one for CRS reduction rules. The only difference is the extra condition stating that the redex and contractum must have identical types. Definition 7.7. An IDTS rewrite rule is a pair of metaterms s → t such that:

• s and t are both closed, i.e. all variables are bound using the [_]_ abstraction binder • s is of the form F (t 1 , . . . , t n )

• all the metavariables that occur in t also occur in s

• any metavariable M that occurs in s only occurs in the form M (x 1 , . . . , x k ), where x i are pairwise distinct variables

• s and t are both of the same type

As stated above, an IDTS is just an alphabet along with a set of rewrite rules. An IDTS induces a rewriting relation in exactly the same way as a CRS does, see [START_REF] Blanqui | Termination and confluence of higher-order rewrite systems[END_REF] for more details.

7.2

λ as an IDTS Now we will link λ to the IDTS framework in order to benefit from its general termination results. The biggest obstacle will be that IDTS assigns a fixed type to every symbol. In λ , symbols are polymorphic: the η constructor can produce expressions like η : F E (1) or η (λx. x) : F E (α → α) and that for any choice of E. We would therefore like to replace function symbols such as η with specialized symbols η F E (α) . For a given type α and effect signature E, the symbol η F E (α) would have the type α → F E (α), i.e. it would belong to F α,F E (α) . We will call this calculus with specialized symbols λ τ . There will not be a bijection between λ and λ τ since a single term in λ will generally correspond to a multitude of specialized versions in λ τ (think of λx. x in λ versus λx ι . x ι , λx o . x o . . . in λ τ ). Therefore, the results we prove for λ τ will not automatically transfer to λ . In the rest of this subsection, we will elaborate the definition of λ τ and show why termination carries over from λ τ to λ -η . 317.2.1 Defining λ τ λ τ will be defined as an IDTS. This means we need to first identify the alphabet. The base types B of λ τ will be the set of types of λ . 32 Note that both λ and IDTS have a notion of function type, but the notation is different. Contrary to common practice, in our exposition of IDTS we use α ⇒ β for the IDTS function type. This allows us to keep using the α → β notation for λ types, as we do in the rest of the article. Next, we will introduce function symbols for all the syntactic constructions of λ , except for abstraction, which is handled by the [_]_ binder construct already found in IDTSs:

• ap α,β ∈ F α→β,α,β (i.e. for every pair of types α and β, there will be a function symbol ap α,β of type

(α → β) ⇒ α ⇒ β in our alphabet) • λ α,β ∈ F α⇒β,α→β • c ∈ F α for any constant c : α ∈ Σ • η α,E ∈ F α,F E (α) • op γ,E ∈ F α,β⇒F E (γ),F E (γ)
for any operation symbol op from E and any E such that op :

α β ∈ E • -• α ∈ F F ∅ (α),α • op 1 ,...,op n ,γ,δ,E,E ∈ F α1→(β1→F E (δ)),...,αn→(βn→F E (δ)),γ→F E (δ),F E (γ),F E (δ)
where:

-

op 1 : α 1 β 1 ∈ E, . . . , op n : α n β n ∈ E -E \ {op 1 , . . . , op n } ⊆ E • C α,β,E ∈ F α→F E (β),F E (α→β)
The list above is based on the typing rules of λ found on Figure 1. We convert the typing rules of λ into the typed function symbols of λ τ with the following process:

• We take a typing rule of λ , other than [var] (since variables are already present in the language of IDTS terms).

• We identify all the type-level metavariables. That is, metavariables α, β, γ . . . ranging over types, metavariables E, E . . . ranging over effect signatures and metavariables op ranging over operation symbols.

• We strip these metavariables down to a minimal non-redundant set (e.g. in the [op] rule, we have that op : α β ∈ E, therefore E and op determine α and β and α and β are redundant).

• We introduce a family of symbols: for every possible instantiation of the metavariables mentioned above, we will have a different symbol. The arity of the symbol will correspond to the number of typing judgments that serve as hypotheses to the typing rule. The types of the arguments and of the result will be derived from the types of the judgments of the hypotheses and the conclusion respectively. If a variable of type α is bound in a premise of type β, then that will correspond to the IDTS function type α ⇒ β.

-Example: In the [η] rule, we have two metavariables: α standing in for a type and E standing in for an effect signature. The rule has one typing judgment hypothesis. For every type α and every effect signature E, we will therefore have a unary symbol η α,E of type α ⇒ F E (α) (i.e. belonging to F α,F E (α) ).

A specifically-typed symbol in λ τ then corresponds to an instantiation of the type metavariables in a λ typing rule. We can follow this correspondence further and see that λ τ IDTS terms, written using the above function symbols, correspond to typing derivations in λ . Our alphabet now has types and function symbols. We also need to specify the sets of variables and metavariables and so we will take some arbitrary sets with x τ , y τ , . . . ∈ X τ and M α1,...,αn,β , N α1,...,αn,β , . . . ∈ Z α1,...,αn,β . To complete our IDTS, we have to give the rewrite rules. The rules for λ τ are given in Figure 5. An important property of an IDTS rewrite rule is that both its left-hand and right-hand side are well-typed and that they have the same type. In order to facilitate the reader's verification that this is indeed the case, we have used a different labelling scheme for function symbols. When we write f α1,...,αn,β , we are referring to the instance of symbol f which has the type α 1 ⇒ . . . ⇒ α n ⇒ β (i.e. belongs to F α1,...,αn,β ). This way, instead of using a symbol name like η α,E , forcing to look up its type α ⇒ F E (α), we will refer to this symbol directly as η α,F E (α) . In Figure 5 presents the rewrite rules with all the subscripts removed. This allows to get a high-level look at the term without any of the type annotation noise. By removing the type indices from the λ τ IDTS rewrite rules, we get the λ CRS-reduction rules of Section 6 (modulo the renaming of @ to ap). When describing the rewrite rules for handlers, we introduce a shortcut

(op i ) i∈I F E (γ),F E (δ) (N F E (γ)
), which stands for partially applied to the clauses M i and M η . We then reuse this shortcut in all of the rules.

Connecting λ τ to λ

We have given a complete formal definition of λ τ . This will let us find a proof of termination for λ τ using the theory of IDTSs. However, in order to carry over this result to our original calculus, we will need to formalize the relationship between the two. Definition 7.8. Term is a (partial) function from λ τ terms to λ terms which removes any type annotations (the subscripts on function symbols, variables and metavariables) and translates λ τ syntax to λ syntax using the following equations:

ap(λ([x]M (x)), N ) → rules β α,γ M (N ) ap α→γ,α,γ (λ α⇒γ,α→γ ([x α ]M α,γ (x α )), N α ) → M α,γ (N α ) let (op i ) i∈I F E (γ),F E (δ) (N F E (γ) ) = (op i ) i∈I (αi→(βi→F E (δ))→F E (δ)) i∈I ,γ→F E (δ),F E (γ),F E (δ) ((M i αi→(βi→F E (δ))→F E (δ) ) i∈I , M η γ→F E (δ) , N F E (γ) ) (op i ) i∈I (η(N )) → rules η (op i ) i∈I F E (γ),F E (δ) ap(M η , N ) (op i ) i∈I F E (γ),F E (δ) (η γ,F E (γ) (N γ )) → ap γ→F E (δ),γ,F E (δ) (M η γ→F E (δ) , N γ ) (op i ) i∈I (op j (N p , [y]N c (y))) → rules op (op i ) i∈I F E (γ),F E (δ) ap(ap(M j , N p ), λ([y] (op i ) i∈I (N c (y))))
where j ∈ I

(op i ) i∈I F E (γ),F E (δ) (op jα,β⇒F E (γ),F E (γ) (N p α , [y β ]N c β,F E (γ) (y β ))) → ap (β→F E (δ))→F E (δ),β→F E (δ),F E (δ) (ap α→(β→F E (δ))→F E (δ),α,(β→F E (δ))→F E (δ) (M j α→(β→F E (δ))→F E (δ) , N p α ), λ β⇒F E (δ),β→F E (δ) ([y β ] (op i ) i∈I F E (γ),F E (δ) (N c β,F E (γ) (y β )))) (op i ) i∈I (op j (N p , [y]N c (y))) → rules op (op i ) i∈I F E (γ),F E (δ) op j (N p , [y] (op i ) i∈I (N c (y)))
where j / ∈ I

(op i ) i∈I F E (γ),F E (δ) (op jα,β⇒F E (γ),F E (γ) (N p α , [y β ]N c β,F E (γ) (y β ))) → op jα,β⇒F E (δ),F E (δ) (N p α , [y β ] (op i ) i∈I F E (γ),F E (δ) (N c β,F E (γ) (y β ))) -• (η(N )) → rules -• α N -• F ∅ (α),α (η α,F ∅ (α) (N α )) → N α C(λ([x]η(M (x)))) → rules C η α,β,E η(λ([x]M (x))) C α→F E (β),F E (α→β) (λ α⇒F E (β),α→F E (β) ([x α ]η β,F E (β) (M α,β (x α )))) → η (α→β),F E (α→β) (λ α⇒β,α→β ([x α ]M α,β (x α ))) C(λ([x]op(M p , [y]M c (x, y)))) → rules C op α,β,E op(M p , [y]C(λ([x]M c (x, y)))) C α→F E (β),F E (α→β) (λ α⇒F E (β),α→F E (β) ([x α ]op γ,δ⇒F E (β),F E (β) (M p γ , [y δ ]M c α,δ,F E (β) (x α , y δ )))) → op γ,δ⇒F E (α→β),F E (α→β) (M p γ , [y δ ]C α→F E (β),F E (α→β) (λ α⇒F E (β),α→F E (β) ([x α ]M c α,δ,F E (β) (x α , y δ ))))
Figure 5: The IDTS rewrite rules for λ τ , shown in parallel with the CRS rules for λ .

Term(x) = x Term(λ([x]M )) = λx. Term(M ) Term(ap(M, N )) = (Term(M )) (Term(N )) Term(c) = c Term(η(M )) = η (Term(M )) Term(op(M p , [x]M c )) = op (Term(M p )) (λx. Term(M c )) Term( -• (M )) = -• (Term(M )) Term( op 1 ,...,op n (M 1 , . . . , M n , M η , N )) = op 1 : Term(M 1 ), op n : Term(M n ), η: Term(M η ) (Term(N )) Term(C(M )) = C (Term(M ))
Definition 7.9. Types is a function from λ terms to sets of λ τ terms, defined by the equation below.

Types(M ) = {m | Term(m) = M } Lemma 7.
10. Let M and N be λ terms. Then,

M → λ -η N ⇒ ∀m ∈ Types(M ). ∃n ∈ Types(N ). m → n
In the above, upper-case letters stand for λ terms, while lower-case letters stand for λ τ terms.

Proof. This property is essentially a stronger kind of subject reduction for λ -η . In proofs of subject reduction, we examine every reduction rule and we show how a typing derivation of the redex can be transformed into a typing derivation of the contractum. We can think of λ τ terms as λ typing derivations. The reduction rules in Figure 5 are the rules which tell us how to take a typing of the redex and transform it into a typing of the contractum.

In order to prove this property, we will need to check the following:

• The redexes and contracta in Figure 5 are well-formed (i.e. well-typed). For that reason, we have included the type of every variable, metavariable and function symbol as a subscript.

• Applying Term to the left-hand and right-hand sides of the λ τ rules yields the left-hand and righthand sides of all the λ -η rules (and therefore the left-hand and right-hand sides of λ τ rules belong to the Types image of the left-hand and right-hand sides of the λ -η rules). Since in Figure 5, we have included the terms with their type annotations removed, we can see at a glance that the stripped rules align with the CRS formulation of λ .

• Finally, we have to check whether the rewriting rules in Figure 5 actually apply to all the m ∈ Types(M ).

In other words, we need to check whether the type annotation scheme used for the left-hand sides is the most general and covers all possible typings of the left-hand side. This is the case because we have followed the typing rule constraints and given the most general type annotations.

Given a reduction in λ -η from M to N , we can find the untyped reduction rule used in Figure 5. We know that if m ∈ Types(M ), then m then matches the left-hand side of the corresponding typed rule. We also know that the right-hand side of the typed rule belongs to Types(N ) and therefore, the property holds. Furthermore, if we were to formalize the correspondence between λ typing derivations and λ τ terms, we would get another proof of subject reduction for λ -η . Lemma 7.11. If the reduction relation of λ τ is terminating, then so is the λ -η reduction relation on well-typed terms.

Proof. Consider the contrapositive: if there exists an infinite λ -η chain of well-typed λ terms, we can use Lemma 7.10 to translate it, link by link, to an infinite λ τ chain. However, infinite λ τ reduction chains do not exist since λ τ is terminating.

Termination for IDTSs

So far, we have introduced an IDTS and have shown that if this IDTS is terminating, then so is λ -η . We will now look at a general result for IDTSs that we will make use of.

Theorem 7.12. Strong normalization [START_REF] Blanqui | Termination and confluence of higher-order rewrite systems[END_REF] Let I = (A, R) be a β-IDTS satisfying the assumptions (A). If all the rules of R satisfy the General Schema, then → I is terminating.

The theorem was lifted verbatim33 from [START_REF] Blanqui | Termination and confluence of higher-order rewrite systems[END_REF] and parts of it deserve explaining:

• What is a β-IDTS?

• What are the assumptions (A)?

• What is the General Schema?

We will deal with these in order. A β-IDTS is an IDTS which, for every two types α and β, has a function symbol @ α,β ∈ F α⇒β,α,β and a rule @ α,β ([x α ]M α,β (x α ), N α ) → M α,β (N α ). Furthermore, there must be no other rules whose left-hand side is headed by @. We can turn our IDTS from 7.2 into a β-IDTS by extending it with these function symbols and reduction rules. 34 Termination in a larger system will still imply termination in our system.

Checking Off the Assumptions

Next, we will deal with the assumptions (A).

Definition 7.13. The Assumptions (A) are defined as the following four conditions:

1. every constructor is positive 2. no left-hand side of rule is headed by a constructor 3. both > B and > F are well-founded 4. stat f = stat g whenever f = F g For these to make sense to us, we will need to identify some more structure on top of our IDTS: the notion of a constructor and the > B and > F relations. We will need to designate for every base type γ a set C γ ⊆ ∪ p≥0,α1,...,αp∈T (B) F α1,...,αp,γ (i.e. a set of function symbols with result type γ). We will call the elements of these sets constructors of γ. The base types of our IDTS consist of atomic types, function types and computation types. We will have no constructors for atomic types. On the other hand, every function type α → β will have a constructor λ α,β (∈ F α⇒β,α→β ) and every computation type F E (γ) will have constructors η γ,E (∈ F γ,F E (γ) ) and op γ,E (∈ F α,β⇒F E (γ),F E (γ) ) for every op : α β ∈ E. We can now check assumption (A.2). Since the only constructors in our IDTS are η, op and λ, we validate this assumption. 35 Our choice of constructors induces a binary relation on the base types.

Definition 7.14. The base type α depends on the base type β if there is a constructor c ∈ C α such that β occurs in the type of one of the arguments of c.

We will use ≥ B to mean the reflexive-transitive closure of this relation. Furthermore, we will use = B and > B to mean the associated equivalence and strict ordering, respectively.

Observation 7.15. If τ 1 ≤ B τ 2 , then τ 1 is a subterm of τ 2 .
Proof. We will prove this by induction on the structure of the base type τ 2 . If τ 2 is an atomic type, then τ 2 has no constructors, so it does not depend on any other type. If we look at the reflexive-transitive closure of that, ≥ B , then the only type α such that τ 2 ≥ B α is, by reflexivity, τ 2 itself, which is a subterm of τ 2 .

If τ 2 is the computation type F E (γ), then we will have several constructors. We have η γ,E with a single argument of type γ. We thus know that F E (γ) depends on γ. For every op : α β ∈ E, we have a constructor op γ,E with arguments of types α and β ⇒ F E (γ). This tells us that F E (γ) also depends on α, β and F E (γ). F E (γ) does not have any more constructors, so those are all the types it depends on. The ≥ B relation, which is the subject of this observation, is the reflexive-transitive closure of the dependency relation between base types. This means that τ 2 ≥ B τ 1 if either τ 2 = τ 1 or τ 2 depends on some τ 2 = τ 2 such that τ 2 ≥ B τ 1 .

• If τ 2 = τ 1 , then trivially τ 1 is a subterm of τ 2 and we are done.

• If τ 2 depends on some τ 2 = τ 2 , then τ 2 must be either γ or one of the α or β from E since τ 2 = F E (γ).

In all these cases, we can apply the induction hypothesis for τ 2 . We know that τ 2 ≥ B τ 1 and by the induction hypothesis, we now know that τ 1 is a subterm of τ 2 . Since τ 2 is a subterm of τ 2 , we have that τ 1 is a subterm of τ 2 .

Corollary 7. [START_REF] Plotkin | Handling algebraic effects[END_REF].

If τ 1 = B τ 2 , then τ 1 = τ 2 .
Corollary 7.17. If τ 1 < B τ 2 , then τ 1 is a proper subterm of τ 2 .

We can now check assumption (A.3). Since the proper subterm relation is well-founded (i.e. has no infinite descending chains) and > B is a subset of the proper subterm relation, then > B must be well-founded as well. We can also check assumption (A.1) once we explain what a strictly positive type is. β ∈ E, op γ,E is a constructor of F E (γ); the type of its second argument is β ⇒ F E (γ). This occurrence is positive and so we validate assumption (A.1). To validate the second half of (A.3), we will need to introduce the > F relation. As > B was induced by the structure of constructors, > F will be induced by the structure of the rewriting rules R of our IDTS. Definition 7.20. A function symbol f depends on a function symbol g if there is a rule defining f (i.e. whose left-hand side is headed by f ) and in the right-hand side of which g occurs. We will use ≥ F as the name for the reflexive-transitive closure of this relation. We will also write = F and > F for the associated equivalence and strict ordering, respectively.

If we scan the rules of λ , we will see that the symbols depend on op (for when there is no handler and the op is copied), ap (for applying the handler clauses to their arguments), λ (for the continuation) and on (for recursion). The C symbols depend on op (when passing the λ through an op), η (when switching the λ with the η), λ (for the argument) and C (for recursion). There is no other dependency in our IDTS. This means we can check off the second part of assumption (A.3) since > F is well-founded (it contains only

> F op, > F ap, > F λ, C > F op, C > F η and C > F λ). Assumption (A.4
) is trivial in our case since, within our IDTS, f = F g only when f = g. This assumption comes into play only in the general theory of IDTSs when one exploits mutual recursion with functions of multiple arguments. The stat f values mentioned in the assumption (A.4) describe the way in which a function's arguments should be ordered to guarantee that recursive calls are always made to smaller arguments. In the case of mutual recursion, both functions must agree on the order according to which they will decrease their arguments. Since we do not deal with mutual recursion in λ , we will not go into any more detail into this.

General Schema

There is one last obstacle in our way towards proving termination of λ τ . We will need to verify that the rewrite rules that we have given in Figure 5 follow the General Schema. Definition 7.21. A rewrite rule f (l 1 , . . . , l n ) → r follows the General Schema if r ∈ CC f (l 1 , . . . , l n ).

CC f (l 1 , . . . , l n ) refers to the so-called computable closure of the left-hand side f (l 1 , . . . , l n ). The idea behind the computable closure is that the left-hand side of a rewrite rule can tell us what are all the possible right-hand sides that still lead to a correct proof of termination. 36 A formal definition of computable closure is given in [77, p. 8]. Informally, r ∈ CC f (l 1 , . . . , l n ) if:

• Every metavariable used in r is accessible in one of l 1 , . . . , l n .

• Recursive function calls (i.e. uses of function symbols g = F f ) are made to arguments smaller than the arguments l 1 , . . . , l n .

A metavariable is accessible in a term if it appears at the top of the term or under abstractions or constructors. If a metavariable occurs inside an argument of a function symbol which is not a constructor, then there are some technical constraints on whether it is accessible. However, in every rewrite rule of our IDTS, the arguments of the function symbol being defined contain only constructors as function symbols. Finally, we will need to show that the arguments being recursively passed to and C are smaller than the original arguments and therefore the recursion is well-founded and terminating. However, the General Schema presented in [START_REF] Blanqui | Termination and confluence of higher-order rewrite systems[END_REF] uses a notion of "smaller than" which is not sufficient to capture the decrease of our arguments. On the other hand, when we were defining a denotational semantics for λ , we gave a well-founded ordering showing that the successive arguments to these operations are in fact decreasing. We will therefore make use of a technique which will allows us to incorporate this semantic insight into the IDTS so that the General Schema will be able to recognize the decreasing nature of the arguments.

Higher-Order Semantic Labelling

We will make use of the higher-order semantic labelling technique presented by Makoto Hamana in [START_REF] Hamana | Higher-order semantic labelling for inductive datatype systems[END_REF]. The idea behind the semantic labelling technique is to label function symbols with the denotations of their arguments. Whereas before, a function symbol was rewritten to the same function symbol on a smaller argument, in the labelled IDTS, a labelled symbol will be rewritten to a different smaller symbol (i.e. one with a smaller label). The theory in [START_REF] Hamana | Higher-order semantic labelling for inductive datatype systems[END_REF] is expressed in terms of category theory. This results in a very elegant and concise formulation of the theorems and their proofs. In this article, we only care about the applications of the theory and so we will try to introduce the technique without presupposing the reader's familiarity with category theory.

Presheaves and Binding Algebras

We will nevertheless introduce a few terms from category theory. When dealing with binding and types, it is usually not so useful to consider a mixed set of terms or denotations of different types. It is much more pertinent to speak of families of terms having the same type in the same typing context, i.e. T τ (Γ) = {t | Γ t : τ }. In this example, T is a family of sets, indexed first by type and second by context. We can therefore say that T ∈ (Set F↓B ) B , where B is the set of base types of our IDTS (i.e. the set of λ types) and F ↓ B is the set of λ typing contexts (functions from finite sets to B). The category-theoretical presentation of abstract syntax and binding originating in [START_REF] Fiore | Abstract syntax and variable binding[END_REF] relies on a similar notion known as presheaf. Presheaf can be seen as a synonym for functor, usually going from some kind of "index category" to some other category. In the above example, B, F ↓ B and Set can be seen as categories:

• B has base types as objects and no arrows besides the mandatory identities • F ↓ B has typing contexts as objects and renamings of contexts (exchanges, weakenings, contractions) as arrows

• Set is the standard category with sets as objects and functions as arrows

Set F↓B is the category of functors from F ↓ B to Set. The object component of such a functor maps contexts to sets (usually sets of objects having some type within the given context). The arrow component translates the renamings of contexts into renamings of variables in these objects. The functors in the category (Set F↓B ) B map types to the objects of Set F↓B ; their arrow component is trivial since B has only trivial arrows. We will call the objects of (Set F↓B ) B presheaves (sometimes, we will also call the objects in Set F↓B presheaves). In our presentation, we will care only about the object level, meaning that we will identify a presheaf with a family of sets. We will now consider some presheaves that will come into play:

• The key presheaf will be the presheaf T of λ terms, T τ,Γ = {M | Γ M : τ }. Every element of T τ,Γ is a well-typed λ term.

• Another useful presheaf is the presheaf V of variables where V τ,Γ = {x | x : τ ∈ Γ}.

• Z is the presheaf of the IDTS metavariables from Z, Z τ,(x1:α1,...,xn:αn) = {M | M ∈ Z α1,...,αn,τ }.

• T Σ V is the presheaf of IDTS terms with alphabet Σ.

• M Σ Z is the presheaf of IDTS metaterms with alphabet Σ and typed metavariables Z. Now we will define some endofunctors on the category of presheaves. As before, we will ignore the arrow component and give only a mapping from one family to another.

• First, we introduce an endofunctor on the category of presheaves in Set F↓B . For every base type τ , we have a functor δ τ : Set F↓B → Set F↓B . For A ∈ Set F↓B , we define (δ τ A)(Γ) = A(Γ + τ ) where Γ + τ is the extension of context Γ by a variable of type τ . 37 The idea behind this operation is to model binders, i.e. the arrow type ⇒ of IDTS. If the presheaf A β ∈ Set F↓B models the type β, then the presheaf δ α A β models the type α ⇒ β.

• The alphabet of our IDTS, Σ, induces an endofunctor on the category (Set F↓B ) B mapping presheaves

A to presheaves ΣA. (ΣA) γ = f ∈F α 1 ⇒β 1 ,..., α l ⇒β l ,γ 1≤i≤l δ αi A βi
In the above, we use the vector notation α ⇒ β for α 1 ⇒ . . . ⇒ α n ⇒ β and δ α for δ α1 • . . . • δ αn . Note that the above definition assumes that α i , β i and γ are all base types. Since in our encoding of λ , we use a function constructor → on the level of base types, this is the case.

We are now ready to define the notion of a Σ-binding algebra.

Definition 7.22. A Σ-(binding) algebra A is a pair of a presheaf A and a natural transformation38 α : ΣA → A. The presheaf is the carrier and the natural transformation interprets the operations. Since ΣA is a coproduct over all the f ∈ F, we can also see α as the copair [f A ] f ∈F , where f A is the interpretation in algebra A of operation f .

We will need to construct a (V + Σ)-algebra in order to proceed, where (V + Σ)(A) is defined as V + Σ(A). Our algebra will be a term algebra, the carrier will be the presheaf T . We will need to give an interpretation to variables and to every function symbol defined in the alphabet Σ. This interpretation must be given as an α : V + ΣT → T , meaning that the interpretation of every function symbol must be compositional. A value from (ΣT ) γ,Γ is composed of some function symbol f of result type γ together with the interpretation of all of the symbol's arguments. If the i-th argument of the function symbol f has type β i and binds variables α i , then the interpretation of the argument in our term model will be a λ term whose type in the context Γ+ α i is β i . The translation Term from λ τ terms to λ terms that we have given in 7.2 gives us the operations of the term model algebra. For example, the line defining the translation of the expression op(M p , [x]M c ) can be transformed into an interpretation for the function symbol op the following way:

Term(op(M p , [x]M c )) = op (Term(M p )) (λx. Term(M c )) op Γ (M p , M c ) = op (Term(M p )) (λx n+1 . Term(M c ))
where n = |Γ|. Therefore, the Term translation function from 7.2 gives us a (V + Σ)-algebra T with carrier T .

Building a Quasi-Model

We will now deal with presheaves equipped with partial orders.

Definition 7.23. A presheaf equipped with a partial order is a pair of a presheaf A and a family of partial orders ≥ A such that ≥ Aτ,Γ is a partial order on the set A τ,Γ .

Definition 7.24. An arrow f :

A 1 × • • • × A n → B in Set F↓B is weakly monotonic if for all Γ and a 1 , b 1 ∈ A 1 Γ , . . . , a n , b n ∈ A n Γ with a k ≥ A k,Γ b k for some k and a j = b j for all j = k, we have that f (Γ)(a 1 , . . . , a n ) ≥ BΓ f (Γ)(b 1 , . . . , b n ).
Definition 7.25. A weakly monotonic (V +Σ)-algebra is a (V +Σ)-algebra A whose carrier A is equipped with a partial order ≥ A such that every operation of A is weakly monotonic.

We want to equip our (V + Σ)-algebra T with the order. However, while we know that is by definition a preorder, reflexive and transitive, we do not know whether it is antisymmetric and therefore whether it forms a partial order. Because of this, we will build a partial order on top of the preorder.

Definition 7.26. We say that terms M and N are interreducible, M N , if M N and N M .

The interreducibility relation defined above is an equivalence relation and we can use it to quotient sets of terms. We define the T / presheaf as the presheaf with T N . This preorder is antisymmetric and the relation on interreducibility classes therefore forms a partial order. This means that (T / , ) is a presheaf equipped with a partial order. We can verify that is a congruence on the (V + Σ)-algebra T . All of the operations in the algebra T construct new λ terms with the operands as subterms of the constructed term. Let f be an operation of T and M 1 , . . . , M k , and N 1 , . . . , N k be λ terms such that ∀i. M i N i . Then we have f

(M 1 , . . . , M k ) f (N 1 , . . . , N k ) because ∀i. M i N i and f (N 1 , . . . , N k ) f (M 1 , . . . , M k ) because ∀i. N i M i . Therefore, we have f (M 1 , . . . , M k ) f (N 1 , . . . , N k ).

Since

is a congruence on (V + Σ)-algebra, we can quotient it and get a (V + Σ)-algebra T / whose carrier is the T / presheaf. We now have a (V + Σ)-algebra, T / , whose carrier is equipped with a partial order, . Because the reduction relation of λ is closed on contexts, the operations of T / are weakly monotonic: if we replace one of the arguments

M i in f (M 1 , . . . , M n ) with an M i such that M i M i , then we will also have f (M 1 , . . . , M i , . . . , M n ) f (M 1 , . . . , M i , . . . , M n ).
Therefore, we have a weakly monotonic (V + Σ)-algebra T / . Definition 7.27. For a given (V +Σ)-algebra A, a term-generated assignment φ is an arrow in (Set F↓B ) B from the presheaf Z to the presheaf A such that φ = ! •θ, where:

• θ is an IDTS valuation,39 i.e. an arrow from Z to T Σ V .

• ! is the unique homomorphism from the initial (V + Σ)-algebra T Σ V to A. 40To clarify the nomenclature: valuations replace metavariables with terms, assignments replace metavariables with interpretations in some algebra and term-generated assignments are assignments that can only assign an interpretation x if x can be computed as the interpretation of some term. Definition 7.28. A weakly monotonic (V + Σ)-algebra (A, ≥ A ) satisfies an IDTS rewrite rule l → r, with l and r of type τ , if for all term-generated assignments φ of the free metavariables Z in l and r, we have:

! θ * τ,Γ (l) ≥ Aτ,Γ ! θ * τ,Γ (r
) where φ = ! •θ, θ * is the extension of the valuation θ to meta-terms and Γ is the context regrouping all the free variables exposed by θ. Definition 7.29. A weakly monotonic (V + Σ)-algebra (A, ≥ A ) is a quasi-model for the IDTS (Σ, R) if (A, ≥ A ) satisfies every rule in R.

Our weakly monotonic algebra (T / , ) is a quasi-model for the IDTS λ τ . The expressions L = ! θ * τ,Γ (l) and R = ! θ * τ,Γ (r) are instances of the left-hand and right-hand side, respectively, of the λ reduction rule l → r. Therefore, we always have L R.

Labelling Our System

We will now decide how to label the and C symbols. The labels we will choose will be the λ denotations introduced in 5.1. We will build up some orders on the denotations that will become crucial later.

Definition 7.30. For each λ type τ , we define a well-founded strict partial order > τ on the set of denotations τ by induction on τ .

• τ is an atomic type Then > τ is the empty relation.

• τ = α → β f > τ g if and only if f and g are both functions (i.e. not ⊥) and ∀x ∈ α . f (x) > β g(x).

The new order is well-founded: any hypothetical descending chain f 1 > τ f 2 > τ . . . could be projected to a descending chain f 1 (x) > β f 2 (x) > β . . ., which is well-founded by induction hypothesis.

• τ = F E (γ) Let E = {op i : α i β i } i∈I .
The order > τ is the smallest transitive relation satisfying the following:

-∀i ∈ I, ∀p ∈ α i , ∀c ∈ F E (γ) βi , ∀x ∈ β i . op i (p, c) > τ c(x)
The proof of the well-foundedness of this relation was given in the definition of the interpretation of a handler (Definition 5.6). It relies on the fact that F E (γ) is defined as a union of an increasing sequence of sets where c(x) always belongs to a set preceding the one in which op i (p, c) appears for the first time.

As our labels, we will use denotations of (possibly open) λ terms. These objects are functions from Γ to τ for some typing context Γ and type τ . We will need to compare denotations of two objects having the same type but not necessarily occurring in the same typing context. We introduce some notation to deal with context and valuation extensions. Notation 7.31. Let Γ and ∆ be typing contexts. The typing context Γ, ∆, the extension of Γ with ∆, is defined by: 7.32. Let e and d be valuations 41 for the typing contexts Γ and ∆, respectively. The valuation e + d for the context Γ, ∆, called the extension of e with d, is defined by:

(Γ, ∆)(x) = ∆(x), if ∆(x) is defined Γ(x), otherwise Notation
(e + d)(x) = d(x), if x ∈ dom(d) e(x), otherwise
• For every symbol f ∈ F α1,...,αn,β and for every label p in S f , we will have f p ∈ F α1,...,αn,β .

To complete our new IDTS, we will also have to transform the rules, so we will need a way to label metaterms. Definition 7.36. Let φ : Z → T / be a term-generated assignment with φ = ! •θ. The labelling map φ L : M Σ Z → M Σ Z is the arrow in (Set F↓B ) B defined by:

φ L τ,Γ (x) = x φ L τ,Γ (Z α1,...,αn,β (t 1 , . . . , t n )) = Z(φ L α1,Γ (t 1 ), . . . , φ L αn,Γ (t n )) φ L τ,Γ (f ([ x 1 ]t 1 , . . . , [ x n ]t n )) = f ! θ * (t1),...,! θ * (tn) f Γ ([ x 1 ]φ L βi,(Γ, x1: α1) (t 1 ), . . . , [ x n ]φ L βn,(Γ, xn: αn) (t n ))
where f ∈ F α1⇒β1,..., αn⇒βn,τ .

The labelling map traverses an IDTS metaterm and replaces unlabelled function symbols from F with labelled ones from F. Note that the term-generated assignment is not used to rewrite the metavariables: the assignment has values in the carrier presheaf of our (V + Σ)-algebra and it can therefore be something completely different than an IDTS term. The term-generated assignment φ = ! •θ is only used when labelling a function symbol. The IDTS valuation θ is used to replace the metavariables in all of the arguments with some specific terms and the resulting IDTS terms are then interpreted in our algebra T / using ! (which turns them into interreducibility classes of λ terms). These interpretations are then given as arguments to the semantic label mapf , which chooses a label from the label set. Note also that there is no case for bare abstraction ([x]t). In the theory of higher-order semantic labelling presented in [START_REF] Hamana | Higher-order semantic labelling for inductive datatype systems[END_REF], the IDTS is assumed to not contain any bare abstractions: abstractions should always be arguments to function symbols. This is the case in our IDTS λ τ . Knowing how to label metaterms, we can now label the rules of an IDTS. Definition 7.37. Given an IDTS (Σ, R), a (V + Σ)-algebra M and a choice of semantic label sets S f and mapsf , we define the rules of the labelled IDTS (Σ, R) with:

• R = {φ L τ,∅ (l) → φ L τ,∅ | l → r : τ ∈ R, term-generated assignment φ : Z → M }
The labelled IDTS will multiply the number of rules. For every possible IDTS valuation of the free metavariables of a rule, there will be a new rule in which the function symbols have been labelled using the interpretations of their arguments. As we have done in 7.2, we will have to show that termination of this new labelled system gives us termination of the unlabelled one. This is the object of the principal result in [START_REF] Hamana | Higher-order semantic labelling for inductive datatype systems[END_REF] (Theorem 3.7): Theorem 7.38. Higher-order semantic labelling Let M be a quasi-model for an IDTS (Σ, R) and (Σ, R) the labelled IDTS with respect to M . Then (Σ, R) is terminating if and only if (Σ, R ∪ Decr) is terminating. Definition 7.39. Given a labelled IDTS alphabet Σ with semantic label sets S f , the rules of the IDTS (Σ, Decr) (called decreasing rules) consist of:

f p ([ x 1 ]t 1 , . . . , [ x n ]t n ) -→ f q ([ x 1 ]t 1 , . . . , [ x n ]t n )
where f ∈ F α1⇒β1,..., αn⇒βn,γ and p > S f q.

The decreasing rules allow us to freely adjust the labels on function symbols to fit rewrite rules as long as we do not increase them.

Verifying the General Schema

Now we will retrace the steps we have carried out in 7.3, this time with our semantically labelled system λ τ .

1. every constructor is positive 2. no left-hand side of rule is headed by a constructor 3. both > B and > F are well-founded 4. stat f = stat g whenever f = F g First we have to check off the assumptions (A.1) through (A.4), repeated above. The constructors of λ τ are the same as the ones in λ τ and so we validate assumption (A.2). It also means that the induced ordering > B is the same as before and it is therefore still well-founded, so we have the first half of assumption (A.3). Since > B is still the same, then so is = B , which is used in the definition of positive constructors (Definition 7.18). The constructors are therefore still positive as well and we get assumption (A.1). To verify the second half of assumption (A.3) and assumption (A.4), we will need to investigate the ordering on function symbols > F and it is here that we will reap the benefits of our labelling. We need to give a well-founded partial order ≥ F on the function symbols such that whenever we have a rule f (l 1 , . . . , l n ) → r, then f ≥ F g for all function symbols g occurring in r. We propose the following relation:42

• p op 1 ,...,op n ,γ,δ,E,E > F q op 1 ,...,op n ,γ,δ,E,E if p > S q • op 1 ,...,op n > F op i • > F ap • > F λ • C p α,β,E > F C q α,β,E if p > S C q • C > F op • C > F η • C > F λ
Whenever we elide indices in the above (for labels, types or the operations in a handler), we assume that they are universally quantified over. This relation is indeed a well-founded strict partial order: ap, op, η and -• are minimal elements and decreasing chains of or C symbols are all finite since the underlying semantic label set orderings > S f are well-founded. This means that our > F ordering validates the second half of assumption (A.3). We also let ≥ F be the reflexive closure of > F and then we validate assumption (A.4) because f = F g only if f = g. We have checked off all of the assumptions and so now we need to check whether the rewrite rules of our labelled IDTS λ τ all follow the General Schema. This boils down to checking whether the ≥ F order correctly describes the recursive behavior of our function definitions. Whenever we use a function symbol g in the right-hand side r of a rule f (l 1 , . . . , l n ) → r, we need to show that f ≥ F g. Furthermore, if f = F g, we need to show that the arguments passed to g are smaller than the arguments l 1 , . . . , l n passed to f . However, thanks to the semantic labelling, we will be able to show that for every rule f (l 1 , . . . , l n ) → r, f > F g for any function symbol g occurring in r. We first check the rules in Decr. These work out because > F contains the label ordering for both labelled function symbols, and C (i.e. p > F q and C p > F C q whenever p > q).

p (M i . . . , M η , N ) → q (M i . . . , M η , N ) C p (M ) → C q (M ) whenever p > q
Then we check the rules that correspond to reductions in λ , looking at either the original formulation on Figure 4 or the CRS/IDTS versions on Figure 5. For most of the rules, it is just a matter of checking that only certain symbols appear in the right-hand sides of certain rules. However, in rules op , op and C op , we have the same (unlabelled) symbol on both the left-hand side and the right-hand side of the rule. In these cases, we will need to prove that the label on the right-hand side occurrence is strictly smaller than the label on the left-hand side occurrence. We will start with the rules op and op .

(op i : M i ) i∈I , η: M η p (op j N p (λx. N c )) → M j N p (λx. (op i : M i ) i∈I , η: M η q N c ) where j ∈ I (op i : M i ) i∈I , η: M η p (op j N p (λx. N c )) → op j N p (λx. (op i : M i ) i∈I , η: M η q N c )
where j / ∈ I

In both cases, the on the left-hand side is applied to Γ op j N p (λx. N c ) : F E (γ) whereas the on the right-hand side is applied to Γ, x : β j N c : F E (γ) where op j : α j β j ∈ E. The label p of the left will be the denotation op j N p (λx. N c ) whereas the label q of the right will be the denotation N c . The ordering on these labels is the > D(F E (γ)) ordering. For the first to be greater than the second, we will need to prove for all e ∈ Γ and all d ∈ β j that op j N p (λx. N c ) (e) > F E (γ) N c (e[x := d]). C p (λx. op M p (λy. M c )) → op M p (λy. C q (λx. M c ))

On the left-hand side, C is applied to Γ λx. op M p (λy. M c ) : γ → F E (δ), and on the right-hand side, it is applied to Γ, y : β λx. M c : γ → F E (δ) where op : α β ∈ E. The label p of the left C is the denotation λx. op M p (λy. M c ) while the label q of the right-hand side C is λx. M c . These labels are ordered by the > D(γ→F E (δ)) ordering under which p > q if for all e ∈ Γ and all d ∈ β , we have p(e) > γ→F E (δ) q(e[y := d]). Then to show that p(e) > γ→F E (δ) q(e[y := d]), we will need to show that they are both functions and that for all c ∈ γ , we have p(e)(c) > F E (δ) q(e[y := d])(c). The reduction relation of λ without η-reduction is terminating.

Proof. By Corollary 7.41 and Lemma 7.11.

Putting η Back in λ

We have shown termination for λ -η . We know that the η-reduction on λ is terminating: it decreases the number of λ-abstractions in the term by one in each step. We would now like to show that the combination of λ -η and η is terminating as well. Note that we could not have used the General Schema to prove that λ with η is terminating. The General Schema does not admit η-reduction. The left-hand side of every rule needs to be headed by a function symbol which is not a contructor. If we tried declaring that λ is not a Finally, we note that Eff is a general-purpose programming language which includes general recursion (let rec) and therefore it is not terminating, contrary to λ .

• λ eff

The λ eff calculus [START_REF] Kammar | Handlers in action[END_REF] is a call-by-push-value λ-calculus [START_REF] Levy | Call-by-push-value: A subsuming paradigm[END_REF] with operations and handlers. Call-bypush-value is special in introducing two kinds of terms: computations and values. The intuition behind the two is that computations do, whereas values are. Two of the crucial things that computations do are to pop values from a stack (that is what abstractions do) and to push values to the stack (that is what applications do). Therefore, applications and abstractions are considered as computations. Furthermore, the function in an application term must be a computation term (which is expected to, among other things, pop a value from the stack), whereas the argument, which is the value to be pushed to the stack, must be a value term. This might make it look like that call-by-push-value is like call-by-value since all the arguments passed to functions are values. However, in true call-by-value, we can use complex expressions as arguments and we expect that the reduction system will evaluate the arguments down to values before passing them to the function. To do this in call-by-push-value, we have to implement this manually by evaluating the argument computation down to a value x and then passing the value x to the function in question (i.e. in λ eff syntax let x ← M in F x). In λ , this amounts to the term M = F , where M : F E (α) and F : α → F E (β). To implement call-by-name, computations can be mapped to values by wrapping them in thunks, which are primitive constructs in call-by-push-value (in λ eff syntax F {M }, where M is a computation and the thunk {M } is a value). In λ , the corresponding term is F M , where M : F E (α) and F : F E (α) → F E (β).

λ eff presents an intriguing alternative to λ . The call-by-push-value calculus is flexible enough to accommodate both call-by-name and call-by-value. λ-abstractions and operations are both treated as effects, which might make the definition of the C operator, which permutes λ with operations, more intuitive. 47 λ eff also has a well-developed metatheory, developed in [START_REF] Kammar | Handlers in action[END_REF]: it is both confluent (due to its reduction relation being deterministic) and terminating (thanks to its effect type system).

λ eff served as an inspiration to the design of λ ; notably, λ 's effect system is based on that of λ eff . However, λ diverges from λ eff in that it is a proper extension of the simply-typed λ-calculus (STLC): every term, type, typing judgment or reduction in STLC is also a term, type, typing judgment or reduction in λ . For example, the STLC term λx. x is not a λ eff term. Its closest counterparts in λ eff would be either ∅ λx. return x : A → F (A), where A is a value type, or E λx. x! : U E (C) → C, where C is a computation type (a function or an effectful computation). On the other hand, in λ , λx. x : α → α is a valid term for any α, be it an atomic type such as o, a function type such as ι → o or a computation type such as F E (o).

The fact that λ is an extension of STLC motivates its use for two reasons. First, STLC is the lingua franca of formal semantics. λ already introduces a lot of new notation and the use of effects in natural language semantics is not yet ubiquitous. By basing λ on STLC, we narrow the gap between the common practice of formal semantics and our use of effects and monads, hopefully making the technique more approachable to researchers in the field. Second, the purpose of the calculus is to write down computations that produce logical representations. By having STLC as a subpart of λ , terms of Church's simple theory of types (i.e. formulas of higher-order logic) are already included in our calculus and we can reuse the same notions of λ-abstraction and variables. In λ eff , we would either need to add constructors for logic formulas (i.e. having some logic as an object language over the terms of which the meta language λ eff would calculate) or use call-by-push-value computations in our logical representations.

• Extensible Effects of Kiselyov et al [START_REF] Kiselyov | Extensible effects: an alternative to monad transformers[END_REF] and other implementations of effect systems in pure functional programming languages (Haskell, Idris . . . ) 47 The extra typing rule for the C construction in λ eff would look like this:

Γ E M : A → C Γ E C M : F (U ∅ (A → C))
Our adoption of a free monad and effect handlers was motivated by the paper of Kiselyov, Sabry and Swords on extensible effects [START_REF] Kiselyov | Extensible effects: an alternative to monad transformers[END_REF]. The paper presented a Haskell library for encoding effectful computations, combining computations with diverse effects and interpreting them by composing a series of modular interpreters. The library used a free monad (in the style of [START_REF] Swierstra | Data types à la carte[END_REF]): a computation is either a pure value (η in λ ) or a request to perform some kind of effect (an operation in λ ). These requests are then handled by interpreters which behave similarly to effect handlers (the authors of [START_REF] Kiselyov | Extensible effects: an alternative to monad transformers[END_REF] also relate handlers to the technique of "extensible denotational language specifications" published in 1994 by Cartwright and Felleisen [START_REF] Cartwright | Extensible denotational language specifications[END_REF]). The paper demonstrated that the approach is more flexible when it comes to combining interacting effects than the existing state-of-the-art technique of using monad transformers. A more refined version of the approach was published in [START_REF] Kiselyov | Freer monads, more extensible effects[END_REF] and similar implementations of effects and handlers exist also in other pure functional programming languages such as Idris [START_REF] Brady | Programming and reasoning with algebraic effects and dependent types[END_REF].

The extensible effects discipline provides the tools that we would like to use to build a modular semantics of natural language. However, we do not want our formal semantics to depend on the semantics of a large programming language such as Haskell 48 or Idris. We created λ to reap the benefits of extensible effects without incurring the complexity of using a language like Haskell as our meta language. λ extends STLC only with computation types, two constructors (η and operations), two destructors (handlers and -• ) and the C operator. Unlike Haskell, our extension of STLC preserves strong normalization.

We have introduced λ , a formal calculus that extends the simply-typed λ-calculus (STLC) with effects and handlers. The definition of λ is given in Section 2. λ introduces a new family of types into STLC, the computation types, and new terms, which are built out of computation constructors and destructors. We gave a type system to the calculus which extends that of STLC and a reduction semantics which combines the STLC β and η reductions with definitions of the new function symbols. In our exposition of the calculus, we have given two perspectives on the intended meaning of the terms: computations can be seen as programs that interact with a system through a selected set of "system calls" (operations) or they can be seen as algebraic expressions built upon an infinitary algebraic signature.

We then devoted most of the article to the development of the metatheory of λ . In Section 3, concepts which are primitive in some other languages (closed handlers and the = operator) were defined within λ and their typing rules and reduction rules were derived from those of λ . In Section 5, we connected the calculus to the theory of monads by identifying a monad in the category in which we interpret λ with our denotational semantics. In Section 4, we proved subject reduction of λ . This result gives a basic coherence between the type system of λ and the reduction semantics, guaranteeing that types are preserved under reduction. This is complemented by a proof of progress, which states that terms which do not use any of the partial operators and which can no longer be reduced must have a very specific shape.

We followed this with another fundamental property: strong normalization. Its proof was split into two parts: confluence (proved in Section 6) and termination (proved in Section 7). The proofs of both confluence and termination proceed by similar strategies: prove the property for the calculus without η-reduction by applying a general result and then extend the property to the complete calculus. In the case of confluence, the general result is the confluence of orthogonal Combinatory Reduction Systems [START_REF] Klop | Combinatory reduction systems: introduction and survey[END_REF]. In the case of termination, we rely on two techniques: the termination of the reduction relation of Inductive Data Type Systems that validate the General Schema [START_REF] Blanqui | Termination and confluence of higher-order rewrite systems[END_REF] and Higher-Order Semantic Labelling [START_REF] Hamana | Higher-order semantic labelling for inductive datatype systems[END_REF], which lets us use our denotational semantics to label the terms of our calculus so that it validates the General Schema.

Finally we briefly discuss the comparison of λ with other existing frameworks. Andrej Bauer made the analogy that effects and handlers are to delimited continuations what while loops or if-then-else statements are to gotos [START_REF] Bauer | Lambda the ultimate -programming with algebraic effects and handlers, personal Communication[END_REF], continuations themselves having proven to be a useful tool in natural language semantics [START_REF] De Groote | Type raising, continuations, and classical logic[END_REF][START_REF] Barker | Continuations and the nature of quantification[END_REF][START_REF] Shan | Linguistic side effects[END_REF][START_REF] De Groote | Towards a montagovian account of dynamics[END_REF][START_REF] Barker | Continuations in natural language[END_REF][START_REF] Barker | Continuations and natural language[END_REF].

  variable x, where x is a variable from X constant c, where c is a constant from Σ abstraction λx. M , where x is a variable from X and M is an expression application M N , where M and N are expressions injection η M , where M is an expression operation op M p (λx. M c ), where op is an operator from E, x is a variable from X and M p and M c are expressions handler op 1 : M 1 , . . . , op n : M n , η: M η where op i are operators from E and M i and M η are expressions extraction -• exchange C

Figure 2 :

 2 Figure 2: The typing rule for the handler construction.

Figure 3 :

 3 Figure 3: Example of applying the C operator to a term.

Figure 4 :

 4 Figure 4: The reduction rules of λ .

Definition 4 . 1 .

 41 Let M and N be terms and x a variable. We define the (capture-resolving) substitution of N for x in M , written as M [x := N ], 17 using the following equations:(λy. M )[x := N ] = λy. (M [x := N ]) assuming that y = x and y is fresh for N18

Lemma 4 . 2 .

 42 Substitution and typesWhenever we have Γ, x : α M : τ and Γ N : α, we also have Γ M [x := N ] : τ (i.e. we can substitute in M while preserving the type).Proof. The proof is carried out by induction on the structure of M (or rather the structure of the type derivation Γ M : τ ). • M = y -If y = x, then M [x := N ] = N and α = τ . We immediately have Γ M [x := N ] : τ from the assumption that Γ N : α. -If y = x, then M [x := N ] = x and we get Γ M [x := N ] : τ from the assumption that Γ, x : α M : τ and the fact that x / ∈ FV(M ).

Definition 5 . 5 .

 55 Assume given I(c) ∈ α for every constant c : α ∈ Σ. For a well-typed term M with Γ M : τ , we define the interpretation of term M as a function M from Γ to τ . The definition proceeds by induction on M : 22 λx. M (e) = λX. ( M (e[x := X])) x (e) = e(x) M N (e) = M (e)( N (e)), if M (e) is a function ⊥, if M (e) is ⊥ c (e) = I(c) op M p (λx. M c ) (e) = op( M p (e), λX. ( M c (e[x := X]))) η M (e) = η( M (e))

Property 5 . 8 .

 58 Soundness of reduction w.r.t. denotations Whenever M → N in λ , then M = N .

  λy. c(y) = (λx. η(x))) = op(p, λy. c(y)) = op(p, c) 5.4 Monad Definition 5.14. A monad is a functor F and two combinators, η : α → F (α) and = :

Definition 6 . 1 .

 61 A reduction relution → on a set A is said to be confluent whenever for each a, b, c ∈ A such that a → b and a → c there is a d ∈ A such that b d and c d.

• a special rewriting rule op 1 :

 1 M 1 , . . . , op n : M n , η: M η (η N ) → M η N • for every 1 ≤ i ≤ n, a special rewriting rule op 1 : M 1 , . . . , op n : M n , η: M η (op i N p (λx. N c (x))) → M i N p (λx. op 1 : M 1 , . . . , op n : M n , η: M η N c (x))

•

  the unary symbol λ for function abstraction • a nullary symbol for every constant in the signature Σ • the unary symbol η for the injection operator • a binary symbol op for every op ∈ E • a (n+2)-ary symbol ( op 1 : _, . . . , op n : _, η: _ _) for every sequence op 1 , . . . , op n of distinct symbols from E of length n • the unary symbol -• for the extraction operator • the unary symbol C for the C operator

•

  If both reductions occurred within a common subterm of a, i.e. a = C[a ], b = C[b ] and c = C[c ] while at the same time a → λ -η b and a → η c , we can use the induction hypothesis for a . This gives us a d such that b η d and c → = λ -η d and therefore we also have d = C[d ] with b η d and c → = λ -η d. • If both reductions occurred within non-overlapping subterms of a, i.e. a = C[a 1 , a 2 ], b = C[b , a 2 ] and c = C[a 1 , c ] with a → λ -η b and a → η c: We can take d = C[b , c ] since we have b η d in one step and c → = λ -η d in one step too.

  -η -redex, it must match the left-hand side of the β rule, (λx. M (x)) N , and b must be M (N ). * We will first deal with the case when the η-redex which lead to c originated in M (x). In that case M (x) → η M (x) and c = (λx. M (x)) N . Our sought-after d is then M (N ), since c → = λ -η d via β in one step and b = M (N ) η d = M (N ). * Now we get to one of the two interesting cases which necessitated this whole lemma: the overlap between β and η, with β on the top. If the η-redex did not originate in M (x), then the η-redex must be λx. M (x). Therefore, M = T x and a = (λx. T x) N . Performing the η-reduction yields c = T N . In this case, both b and c are equal to T N and so we can choose T N as our d.

  and r into R(M ). We have a = L(a ) for some a , b = R(a ) and c = L(a ) 29 . Our d will be R(a ) and we have b = R(a ) η d = R(a ) in several steps 30 and c = L(a ) → = λ -η d = R(a ) in one step of l → r.

  N . Then N → λ -η N and b = λx. N x. The common reduct d is N since b η d in one step and c = N → = λ -η d = N as established before. -Now this is where we deal with the second overlap between β and η in our reduction system, the one with η on top. The λ -η -redex in a must be N x and the reduction rule in question must therefore be β. Therefore, N = λy. T (y) and a = λx. (λy. T (y)) x. Performing the β-reduction gives us b = λx. T (x) which is, however, equal to c = N = λy. T (y). So we can choose d = b and we are done.

Definition 7 .

 7 18. A constructor c ∈ C β is positive if every base type α = B β occurs only at positive positions in the types of the arguments of c. Definition 7.19. The base types occurring in positive positions (Pos) and the base types occurring in negative positions (Neg) within a type are defined by the following mutually recursive equations: Pos(α ⇒ β) = Neg(α) ∪ Pos(β) Neg(α ⇒ β) = Pos(α) ∪ Neg(β) Pos(ν) = {ν} with ν an atomic type Neg(ν) = ∅ with ν an atomic type In our IDTS, α = B β is true only when α = β. The only time a base type occurs in the type of one of its constructor's arguments is in the case of the op constructors. Given op : α

  = {{N | M N } | Γ M : τ }, i.e. T / is the quotient of the T presheaf w.r.t. the interreducibility relation. The elements of T / τ,Γ are interreducibility classes of terms having the type τ in the typing context Γ. We will use the metavariables M and N for these equivalence classes. The preorder on λ terms can be extended to interreducibility classes of λ terms. Formally, we have M N if there exists M ∈ M and N ∈ N such that M

  op j N p (λx. N c ) (e) = op j ( N p (e), λX. ( N c (e[x := X]))) From the definition of > F E (γ) (Definition 7.30), we know that for all d ∈ β j , op j ( N p (e), (λX. N c (e[x := X]))) > F E (γ) N c (e[x := d]) which is exactly what we wanted to show. Now we look at the C op rule.

  λx. op M p (λy. M c ) (e)(c) = (λX. ( op M p (λy. M c ) (e[x := X])))(c) = op M p (λy. M c ) (e[x := c]) = op( M p (e[x := c]), λY. ( M c (e[x := c, y := Y ]))) λx. M c (e[y := d])(c) = (λX. ( M c (e[y := d, x := X])))(c) = M c (e[y := d, x := c]) = M c (e[x := c, y := d]) We elaborate both of the expressions. The last step in rewriting λx. M c (e[y := d])(c) is due to e[x := X, y := Y ] = e[y := Y, x := X] for distinct variables x and y. From the definition of > F E (δ) (Definition 7.30), we get that for all d ∈ β , op( M p (e[x := c]), λY. ( M c (e[x := c, y := Y ]))) > ( M c )(e[x := c, y := d]), which is exactly what we need. Having shown that the function symbols that head the left-hand sides of rules are strictly larger (in a well-founded poset) than the function symbols that occur in the right-hand sides gives us termination for the labelled IDTS λ τ via Theorem 7.12. Theorem 7.40. (Termination of λ τ ) The reduction relation induced by the labelled IDTS λ τ is terminating. 43 Proof. Proof given above by the application of the General Schema presented in [77]. Corollary 7.41. (Termination of λ τ ) The reduction relation induced by the IDTS λ τ is terminating. Proof. By Theorem 7.40 and Theorem 7.38. Corollary 7.42. (Termination of λ -η )

More precisely, we are interpreting programs in a free monad[START_REF] Swierstra | Data types à la carte[END_REF].

In a similar way that monads can be turned into monad transformers (monad morphisms) and then composed[START_REF] Liang | Monad transformers and modular interpreters[END_REF][START_REF] Shan | Monads for natural language semantics[END_REF][START_REF] Wu | Transformers, handlers in disguise, haskell eXchange[END_REF].

Since the banana brackets can contain an arbitrary number of operator clauses, we adopt the syntax of named parameters/records used in languages such as Ruby, Python or JavaScript.

This is very reminiscent of the idea behind Paul Blain Levy's call-by-push-value calculus[START_REF] Levy | Call-by-push-value: A subsuming paradigm[END_REF], which treats abstracting over a variable as an effectful operation of popping a value from a stack. Using call-by-push-value could prove to be a rewarding way to refine our approach.

Throughout this article, we will be using the term computation to mean values of type F E (α). Programs written in λ are simply called terms and their normal forms are called values. To break it down, in λ , terms evaluate to values, some of which can be computations (those of an F type).

The two types α and β are to be seen as the operation's input and output types, respectively.

In general, the same operation symbol can be used with different input and output types, in computations whose types are indexed by different effect signatures.

Our use of the word cluster is synonymous with the mathematical term family. We will be using the term cluster for families of computations passed to operations and handlers.

The f in E f stands for forwarded effects since it refers to effects that the handler will not interpret but instead forward to some other interpreter. The notation comes from a similar rule in the λ eff calculus[START_REF] Kammar | Handlers in action[END_REF].

Violating this assumption will yield terms which get stuck during evaluation (we will see the partial reduction rules in Section 2.3). Sam Lindley presented a refined type system for a similar calculus to track the use of variables[START_REF] Lindley | Algebraic effects and effect handlers for idioms and arrows[END_REF]. A similar refinement should be possible in our case as well but it would obscure the already dense type notation.

The other direction, typed F E (α → β) → (α → F E (β)), is already possible without introducing a special operator since F E is a functor.

Based on what we said about it in Section 2.2, not on its name.

The type and effect signature metavariables that appear in the types are bound by the typing constraints of the terms on the right-hand side.

In the types of the operators given below, we use the same effect signature E everywhere. Technically, a more general type could be derived for these terms given our system. However, we will rarely need this extra flexibility and so we stick with these simpler types.

This is not a part of the core calculus as this is only sound when the type of the handler is of the shape F E (γ) → F E (γ) (i.e. when the handler preserves the type γ of values returned by the computation).

Composing the -•operator with a handler is an identifying characteristic of closed handlers: a closed handler is a banana with a cherry on the top.

E = {op i : α i β i } i∈I [Γ λxk. η (M i x ( -• • k)) : α i → (β i → F ∅ (δ)) → F ∅ (δ)] i∈I Γ λx. η (M η x) : γ → F ∅ (δ) Γ N : F E (γ) [ ] Γ (op i : (λxk. η (M i x ( -• • k)))) i∈I , η: (λx. η (M η x)) N : F ∅ (δ) [ -• ] Γ -• ( (op i : (λxk. η (M i x ( -• • k)))) i∈I , η: (λx. η (M η x)) N ) : δWe still need to prove both Γ λxk. η(M i x ( -• • k)) : α i → (β i → F ∅ (δ)) → F ∅ (δ)for every i ∈ I and Γ λx. η (M η x) : γ → F ∅ (δ).

From now on, this notation will be used for capture-resolving substitution only.

Property 4.3. Subject reduction If Γ M : τ and M → N , then Γ N : τ . Proof. We prove this by induction on the reduction rule used in M → N . • M → β N It must be the case that M = (λx. M ) M and N = M [x := M ]. Since, Γ M : τ , we must have the following typing derivation:Γ, x : α M : τ [abs] Γ λx. M : α → τ Γ M : α [app] Γ (λx. M ) M : τ[START_REF] Pretnar | An introduction to algebraic effects and handlers[END_REF] Here, y is a bound variable and we can simply assume that it is different from x and proceed. . .[START_REF] Hillerström | Shallow effect handlers[END_REF] . . . whereas here, y is a free variable and therefore, we have to examine whether it is different from x or not.

From the above derivation, we can extract Γ, x : τ 1 M : τ 1 → τ 2 . However, since x is fresh for M , we can strengthen this to Γ M : τ 1 → τ 2 , which is what we wanted to prove.• M → η N We have M = (op i : M i ) i∈I , η: M η (η M ), N = M η M , τ = F E (δ)and the following typing derivation for M :Γ M η : γ → F E (δ) Γ M : γ Γ η M : F E (γ) . . . [ ] Γ (op i : M i ) i∈I , η: M η (η M ) : F E (δ)From the inferred typing judgments for M η and M , we can build the typing derivation for M η M .Γ M η : γ → F E (δ) Γ M : γ [app] Γ M η M : F E (δ) • M → op N We have M = (op i : M i ) i∈I , η: M η (op j M p (λx. M c )), N = M j M p (λx. (op i : M i ) i∈I , η: M η M c ) and τ = F E (δ). Γ M j : α j → (β j → F E (δ)) → F E (δ) Γ M p : α j Γ, x : β j M c : F E (γ) op j : α j β j ∈ E [op] Γ op j M p (λx. M c ) : F E (γ) . . . [ ] Γ (op i : M i ) i∈I , η: M η (op j M p (λx. M c )) : F E (δ)From the types of M p , M c and M j , we can calculate the type of our redex, M j M p (λx. (op i :M i ) i∈I , η: M η M c ). Γ M j : α j → (β j → F E (δ)) → F E (δ) Γ M p : α j [app] Γ M j M p : (β j → F E (δ)) → F E (δ) Γ, x : β j M c : F E (γ) . . . [ ] Γ, x : β j (op i : M i ) i∈I , η: M η M c : F E (δ) [abs] Γ λx. (op i : M i ) i∈I , η: M η M c : β j → F E (δ) [app] Γ M j M p (λx. (op i : M i ) i∈I , η: M η M c ) : F E (δ) • M → op N We have M = (op i : M i ) i∈I , η: M η (op M p (λx. M c )), N = op M p (λx. (op i : M i ) i∈I , η: M η M c ) and τ = F E (δ). Γ M p : α Γ, x : β M c : F E (γ) op : α β ∈ E [op] Γ op M p (λx. M c ) : F E (γ) op : α β ∈ E . . . [ ] Γ (op i : M i ) i∈I , η: M η (op M p (λx. M c )) : F E (δ)

Constants are assumed to be reduced away by some external rule. In our case, this will be the application of an ACG lexicon (??).

Note that this disjoint union operator is different from the one from Section 2. A B is defined as{(x, 0) | x ∈ A} ∪ {(x, 1) | x ∈ B}.

In the definition, we make use of (op i : M i ) i∈I , η: Mη (e) and C . This notation is introduced right after this definition.

We could also extend this interpretation to sums and products. The types would be interpreted by α × β = ( α × β ) ⊥ and α + β = ( α β ) ⊥ . The term level definitions would be the standard definitions one would expect for pairs and variants (modulo the treatment of ⊥).

Note that with this translation, op tp (λx. tc) does not contain λx. tc as a subterm. This is the same as in λ , where the notion of evaluation context (see 2.3) does not identify λx. tc, but rather tc, as a subterm of op tp (λx. tc). This becomes important in our discussion of confluence since it makes it impossible to make the λ disappear by something like η-reduction.

More precisely, if a is a subterm of b in λ then the CRS version of a is a subterm of the CRS version of b. In the other direction, whenever a is a variable or a function-headed term which is a subterm of b in the CRS version of λ , then the corresponding a in λ is a subterm of the corresponding b.

This is not so much a fortunate conincidence but rather a deliberate choice in the design of the calculus. For example, it is one of the reasons why, in λ , η x is not decomposed as an application of the built-in function η to x, but is treated as a special form.

We know that β does not overlap any of the other rules. Neither does it overlap itself since its left-hand side does not have an application subexpression.

This also holds for λ with sums and products since their rules are left-linear and do not overlap with the λ rules.

In the sequel, we will ignore the η-reduction and use IDTSs to prove the termination of λ without η-reduction, λ -η .

Note that throughout this section, we will make a distinction between two notions of "basic" types: atomic types and base types. Atomic types are the basic types of λ . Base types are the basic types of IDTSs. In our particular IDTS, the base types consist of all the types of λ , i.e. the atomic types, the λ function types α → β and the computation types. This means that, from the point of view of the IDTS, λ function types and computation types are just another base type.

In fact, the actual Theorem in[START_REF] Blanqui | Termination and confluence of higher-order rewrite systems[END_REF] states that the system is strongly normalizing. However, by strongly normalizing they mean that every term is computable, i.e. that there is no infinite reduction chain.

These β rules and application operators are different from the ones already in our IDTS. ap is defined for the α → β function type from λ whereas @ serves the α ⇒ β type of IDTS.

This is why we have to prove termination with η reduction separately

Theorem 7.12 is proven using Tait's method of computability predicates[START_REF] Tait | Intensional interpretations of functionals of finite type i[END_REF]. The term computable closure comes from the fact that the admissible right-hand sides are the metavariables of the left-hand side closed on operations that preserve computability.

When we extend a context, we usually extend it with a pair of a variable name and a type, e.g. Γ, x : τ . However, the theory of binding algebras uses Bruijn levels[START_REF] De Bruijn | Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem[END_REF], where the names of variables in a context are always integers from 1 to some n. Extending a context x 1 : α 1 , . . . , xn : αn with a type τ then yields a context x 1 : α 1 , . . . , xn : αn, x n+1 : τ .

Natural transformation is the name for an arrow between two functors (presheaves). In our particular setting, naturality boils down to Aγ being a function of (ΣA)γ for every γ.

Same as the CRS valuations introduced in 6.1, but typed.

Homomorphisms between Σ-algebras are defined in the same way as homomorphisms for first-order algebras. The term algebra T Σ V is called an initial algebra because we can find a (unique) homomorphism from T Σ V to any other algebra A that works by interpreting terms from T Σ V using the operations of A.

Not IDTS valuations, but the valuations used by the denotational semantics in 5.1.

In Subsection 7.3, we said that the ordering ≥ F is induced by the form of the rewrite rules. Actually, we are free to define ≥ F ourselves as long as it validates the assumptions and the General Schema.

This result can be extended to λ with sums and products. The pair construction -, -and the injections inl and inr will be the constructors for α × β and α + β, respectively, with α < B α × β, β < B α × β, α < B α + β and β < B α + β. All of the rules defining case analysis and projections π 1 and π 2 satisfy the General Schema.

Rules like η can delete metavariables (n = 0 for the metavariable Mη), while others, like , can copy them (n = 2 for the variable M j )

The case of D = [] is not considered, because it is covered by the case where the contractum of the first reduction containts the redex of the second reduction.

An inductive type is a recursive type with positive constructors. In 7.3, we have seen that a computation type F E (α) has positive constructors η and op for every op ∈ E.

The implementations of extensible effects in Haskell make use of a wealth of language extensions which are not even part of the Haskell standard.

if λ τ terminates, then λ -η terminates (Lemma 7.11)

• Blanqui [START_REF] Blanqui | Termination and confluence of higher-order rewrite systems[END_REF]: General Schema ⇒ termination (7.3) • Hamana [START_REF] Hamana | Higher-order semantic labelling for inductive datatype systems[END_REF]: IDTS R terminates iff the labelled IDTS R terminates (7.4) -Theorem 7.40: λ τ terminates (via Blanqui [START_REF] Blanqui | Termination and confluence of higher-order rewrite systems[END_REF]) -Corollary 7.41: λ τ terminates (via Hamana [START_REF] Hamana | Higher-order semantic labelling for inductive datatype systems[END_REF]) -Corollary 7.42: λ -η terminates (via Lemma 7.11) • λ -η + η terminates (7.5,Theorem 7.46) because λ -η and η are exchangeable (Lemma 7.44)

and therefore λ is strongly normalizing (Theorem7.47)

Inductive Data Type Systems

We will go by the revised definition of Inductive Data Type Systems that figures in [START_REF] Blanqui | Termination and confluence of higher-order rewrite systems[END_REF] and [START_REF] Hamana | Higher-order semantic labelling for inductive datatype systems[END_REF]. This formulation extends IDTSs to higher-order rewriting and does so using the CRS formalism that we introduced earlier.

Definition 7.2. An Inductive Data Type System (IDTS) is a pair of an IDTS alphabet and a set of IDTS rewrite rules.

Just like a CRS, an IDTS is an alphabet coupled with some rewrite rules. Let us first look at the alphabet and the rules for building terms out of the elements of the alphabet; the rewrite rules will follow. The distinction between a CRS-alphabet and an IDTS alphabet is that the IDTS alphabet comes equipped with a set of types. Furthermore, all the other symbols in the alphabet are indexed by types, so we end up with typed variables, typed function symbols and typed metavariables. When we consider IDTS metaterms, we admit only well-typed terms. The definition of IDTS metaterms refines the definition of CRS metaterms by restraining term formation in accordance with the types. Definition 7.5. The typed metaterms of an IDTS are given inductively:

• variables from X τ are metaterms of type τ • f > D(τ ) g if and only if:

We will use the notation ≥ D(τ ) for the reflexive closure of > D(τ ) .

For every symbol f to label, we will now choose a non-empty well-founded poset (S f , ≥ S f ), called the semantic label set. In our application of the technique, we will always choose the set of possible denotations of the argument that is being recursively decreased by the function. For the symbols that we do not care to label, we will assume that their semantic label set is the singleton set 1.

, we take as the semantic label set the poset

, we take as the semantic label set the poset

Having fixed the semantic label sets, we will now choose the semantic label maps. For each symbol f ∈ F α1⇒β1,..., αn⇒βn,γ to be labelled, we define a weakly monotonic arrowf in Set F↓B :

This semantic label map has access to the interpretations of all of the function symbol's arguments and needs to map them to an element of the semantic label set. In our model, the carrier containing the interpretations is the presheaf T / of interreducibility classes of λ terms. However, the interreducibility relation will be a congruence for all of the semantic label maps that we will define and so we will define them directly on terms instead of interreducibility classes. This means that for every op 1 ,...,op n ,γ,δ,E,E ∈ F α1→(β1→F E (δ)),...,αn→(βn→F E (δ)),γ→F E (δ),F E (γ),F E (δ) , we need to give:

We do so by projecting the last argument, which is a λ term of type F E (γ) in the context Γ, and finding its denotation using -.

We will do the same for the C symbols. For every

, we give a:

by: M C Γ = M We can check that interreducibility is indeed a congruence for these semantic label maps: denotations are preserved under reduction (Property 5.8), and therefore all the terms in an interreducibility class have the same denotation. This means that we can extend these semantic label maps to T / , the carrier of our quasimodel (T / , ). The semantic label maps must also be weakly monotonic. That is a condition that our maps satisfy: whenever we have M N , then by Property 5.8, the denotations M and N for M ∈ M and N ∈ N will be equal and therefore so will be the labels M and N . Since, M = N , we have M ≥ N . We have now built up enough structure to correctly label our IDTS with denotations. Let us start with the alphabet. Definition 7. [START_REF] Baez | Enriched lawvere theories for operational semantics[END_REF]. Let Σ = (B, X , F, Z) be the alphabet of an IDTS (Σ, R) and S f the chosen semantic label sets. The alphabet of the labelled IDTS (Σ, R) is the IDTS alphabet Σ = (B, X , F, Z) where: constructor, we would run into problems with the notion of accessibility. When accessing the metavariables of the left-hand side of a rule, we can access all of the arguments of a constructor but we can only access the arguments of a non-constructor symbol that has a basic type. The type of the argument of λ α,β is α ⇒ β and so we could not access the arguments of λ in our rules (which would break the β rule, η rule and the C rules). Termination is generally not a modular property of higher-order rewriting systems [START_REF] Appel | Higher-order (non-) modularity[END_REF]. Our plan will be to show that η-reduction does not interfere with the rewrite rules of λ -η . Then we will be able to take any reduction chain in λ and pull out from it a chain which only uses rules from λ -η . Since this chain must be finite due to the termination of λ -η , we will have a proof of finiteness for the reduction chain in λ .

Definition 7.43. An n-ary evaluation context C n is a λ term in which n disjoint subterms have been replaced with the symbol []. We write C n [M ] for the term in which all of the occurrences of the symbol [] have been replaced with M . Lemma 7.44. Exchanging η with λ -η For every well-typed reduction chain s → η t → λ -η u, there exists a well-typed reduction chain s → + λ -η t → * η u.

Proof. We will consider all the possible relative positions of the contractum of the first reduction and the redex for the second reduction within t.

• Assume the two are disjoint, i.e.

Then we can easily reorder the two reductions, producing the chain

• Assume that the contractum of the first reduction contains the redex for the second reduction, i.e.

• Assume that the redex for the second reduction contains the contractum of the first reduction, i.e.

We will now distinguish two scenarios:

-The occurrence of M in D[M ] is matched by a metavariable in the left-hand side of rule R.

The R-redex N of D[M ] will be a term E n [M , . . . , M ] where E n is an n-ary context for some n which depends on the rule R and the metavariable that was matched. 44 Furthermore, we can replace M with any other term of the same type and the reduction will still go through, e.g. notably

-The occurrence of M in D[M ] is not matched by a metavariable.

M is an η-contractum and must therefore have a function type. If we investigate the left-hand sides of all the rewriting rules in λ -η and search for terms that have a function type, we end up with:

We note that in all of these rules, the symbol which replaces [] must be a λ-abstraction. Therefore, if

We can replace this step by a β-reduction: M = λx. (λx. M ) x → β λx. M = M . The β rule is a part of λ -η and so we can now build the chain

Lemma 7.45. Pulling a λ -η link from a λ chain Let t 1 → t 2 → . . . be an infinite reduction chain in λ . Then there exists another infinite reduction chain u 1 → u 2 → . . . in λ and t 1 → λ -η u 1 .

Proof. The goal of this lemma is to show that we can find an λ -η link in every infinite λ and move it to the beginning of the chain. An infinite chain in λ must use a rule from λ -η , otherwise it would be an η chain and those cannot be infinite since η is terminating.

Let t k → t k+1 be the first link in the chain that uses a rule from λ -η . We will prove this lemma by induction on k.

If k = 1, then we can use the chain t 2 → t 3 → . . . which also uses rules from λ -η infinitely often and which satisfies t 1 → λ -η t 2 .

If k > 1, then we replace the segment t k-1 → η t k → λ -η t k+1 with the segment t k-1 → + λ -η t k → * η t k+1 using Lemma 7.44. By induction hypothesis, the chain t 1 → . . . → t k-1 → + λ -η t k → * η t k+1 → t k+2 → . . . gives us the necessary chain u 1 → u 2 → . . . with t 1 → λ -η u 1 .

Theorem 7.46. Termination of λ

The reduction relation → on λ terms given by the rules in Figure 4 is terminating.

Proof. We will prove this theorem by contradiction. Let t 1 → t 2 → . . . be an infinite reduction chain in λ . Since we have an infinite chain in λ , we can iterate Lemma 7.45 to get an infinite sequence of chains such that the first element of every chain reduces via λ -η to the first element of the next chain in the sequence.

The first elements of these chains form an infinite reduction chain λ -η , which is in contradiction with the termination of λ -η .

Theorem 7.47. Strong normalization of λ There are no infinite reduction chains in λ and all maximal reduction chains originating in a λ term M terminate in the same term, the normal form of M .

Proof. The lack of infinite reduction chains is due to termination of λ (Theorem 7.46) and the fact that all maximal reduction chains lead to the same term is entailed by confluence of λ (Theorem 6.18).

Comparison with Existing Work and Conclusion

Calculus

λ can be compared to several existing calculi and implementations of effects and handlers:

• System F (i.e. the polymorphic λ-calculus or the second-order λ-calculus) λ extends the simply-typed λ-calculus with computation types F E (α). Computations are algebraic expressions and as such can be expressed as inductive data types. 46 In λ , a computation of type F E (α) can also be given the type F E E (α), where E E is an extension of E. However, in the direct encoding of λ into System F, for every effect signature E E that we would like to ascribe to a computation, we would end up with a different term. On the other hand, in λ we can keep using the same term. This lets us give a semantics to lexical items that does not have to change when new effects are introduced into the theory.

• Eff

The Eff language [START_REF] Bauer | Programming with algebraic effects and handlers[END_REF] is an ML-like programming language with effects and handlers. Like in ML, effects can be freely used within any expression, without any term encoding (we say that the calculus is direct-style). For this to work correctly, the calculus has a fixed evaluation order, which, following ML, is call-by-value.

We have used Eff in our first explorations of effects and handlers in natural language semantics [START_REF] Maršík | Algebraic effects and handlers in natural language interpretation[END_REF], benefiting from the existing implementation. However, we have found that besides call-by-value, callby-name evaluation is also common, notably on the boundaries of lexical items. Call-by-name can be simulated in call-by-value by passing around thunks (functions of type 1 → α for some α). However, in the presence of both call-by-name and call-by-value, we have opted for an indirect presentation of effects using monads which favors neither call-by-value nor call-by-name and that lets us manipulate the order of execution using =.