{'fraction_non_alphanumeric': 0.05080111554656313, 'fraction_numerical': 0.007218242467326516, 'mean_word_length': 4.19693094629156, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Sound and Complete Typing for lambda-mu

In this paper we define intersection and union type assignment for Parigot's calculus lambda-mu. We show that this notion is complete (i.e. closed under subject-expansion), and show also that it is sound (i.e. closed under subject-reduction). This implies that this notion of intersection-union type assignment is suitable to define a semantics.


Introduction
The Intersection Type Discipline has proven to be an expressive tool for studying termination and semantics for the λ-calculus [12,10]. Intersection type assignment is defined as an extension of the standard, implicative type assignment known as Curry's system [15] (see also [24]), which expresses function composition and application; the extension made consists of relaxing the requirement that a parameter for a function should have a single type, adding the type constructor ∩ next to →. This simple extension allows for a great leap in complexity: not only can a (filter) model be built for the λ-calculus using intersection types, also strong normalisation (termination) can be characterised via assignable types; however, type assignment becomes undecidable. The literature on intersection types is vast; it was first defined by Coppo and Dezani-Ciancaglini in [13] and its development took place over a number of years, culminating in the paper by Barendregt, Coppo, and Dezani-Ciancaglini [11], and has been explored by many people since.
It is natural to ask if these results can be achieved for other calculi (reduction systems) as well, and in previous papers the author investigated (in collaboration) Term Rewriting Systems [6], and Object Oriented Calculi [5]; Maffeis looked at intersection types in the context of the π-calculus [26]. In order to come to a characterisation of strong normalisation for Curien and Herbelin's (untyped) sequent calculus λµμ [14], Dougherty, Ghilezan and Lescanne presented System M ∩∪ [17], that defines a notion of intersection and union typing for that calculus; in a later paper [18], they presented an improved version of their original system.
In [3], the author revisited System M ∩∪ , and showed that that system was neither sound (i.e. closed under reduction), nor complete (i.e. closed under reverse reduction); the same holds for the system presented in [18]. To address completeness, [3] adds ⊤ as the maximal and ⊥ as the minimal type, and extends the set of derivation rules; however, soundness is shown to be impossible to achieve without restricting typeability (effectively making less terms typeable). In [4], the author attempted to solve the same issue, but this time in the context of the sequent calculus X , as defined by Lengrand [25], and later studied by Lescanne and the author [7,8]; X is a sequent calculus in that it enjoys the Curry-Howard isomorphism with respect to the implicative fragment of Gentzen's LK [20]. The advantage of using the sequent approach is that it is now possible to explore the duality of intersection and union fully, through which we can study and explain various anomalies of union type assignment [32,9] and quantification [22,27]. Also for X , the completeness result follows relatively easily, but soundness can only be shown for restricted systems (effectively call-by-name and call-by-value reduction, but it might be possible that other sound restrictions exist as well). The main conclusion of those papers is that, in symmetric calculi (like λµμ and X ) it is inevitable that intersection and union are truly dual, and that the very nature of those calculi makes a sound and complete system unachievable.
In this paper we will continue on this path and bring intersection types to the context of classical logic, by presenting a notion of intersection and union type assignment for the (untyped) calculus λµ, that was first defined by Parigot in [31], and was later extensively studied by various authors.
Intersection and union types have also been studied in the context of the λ-calculus in [9]; also for the system defined in that paper soundness is lost, which can only be recovered by limiting to parallel reduction, i.e. all residuals of a redex need to be contracted in parallel. The problem of loss of soundness also appears in other contexts, such as that of ML with side-effects [22,33,27], and that of using intersection and union types in an operational setting [16,19]. As here, also there the cause of the problem is that the type-assignment rules are not fully logical, making the context calls (which form part of the reduction in X ) unsafe; this has, in part, already been observed in [23] in the context of Curien and Herbelin's calculus λµμ [14]. This also explains why, for ML with side-effects, quantification is no longer sound [22,27]: also the (∀I) and (∀E) rules of ML are not logical.
In the view of those failures, the result presented here comes as a surprise. We will define a notion of type assignment for λµ that uses intersection and union types, and show that it is both sound and complete. The system presented is a natural extension of the strict intersection type assignment system as defined in [2]; this implies that intersection models the distribution of arguments in a parameter call. But it is also a natural extension of the system for λµ, and in order to achieve completeness for structural reduction, as in the papers mentioned above, union types are added. However, the union types are no longer dual to intersection types; union types play only a marginal role, as was also the intention of [18]. Contrary to that paper, however, we do not see union as negated intersection, but see a union type as a strict type; in particular, we do not allow the normal (∪I) and (∪E) rules as used in [9], which we know create the same soundness problem. Moreover, although one can link intersection types with the logical connector and, the union types we use here have no relation with or; one could argue that therefore perhaps union is not the right name to use for this type constructor, but we will stick with it nonetheless.
The limited view of union types is mirrored by λµ's limited (with respect to λµμ and X ) notion of context 1 . In λµ, we distinguish control structures as those terms that start with a context switch µα.
[β]M, followed by a number of arguments; since union types allow us to express that the various continuations (all called α) need not have the same type, we use a different formulation for rule (→E), which has an implicit use of union elimination (see Definition 3.2). The type system defined here will be shown to be the natural one, in that intersection and union play their expected roles for completeness. Because the use of intersection and union is limited in that a context variable cannot have an intersection type, and although we allow union types for term variables, we do not have the normal union elimination rule; thanks to these two restrictions, we can show soundness as well.

The calculus λµ
Parigot's λµ-calculus [29] is a proof-term syntax for classical logic, expressed in Natural Deduction, defined as an extension of the Curry type assignment system for the λ-calculus. We quickly revise some basic notions: 2. Curry-type assignment is defined by the following natural deduction system.
With λµ Parigot created a multi-conclusion typing system which corresponds to classical logic; the derivable statements have the shape Γ ⊢ λµ M : A | ∆, where A is the main conclusion of the statement, expressed as the active conclusion, and ∆ contains the alternative conclusions, consisting of pairs of Greek characters and types; the left-hand context Γ, as usual, contains pairs of Roman characters and types, and represents the types of the free term variables of M. As with Implicative Intuitionistic Logic, the reduction rules for the terms that represent the proofs correspond to proof contractions; the difference is that the reduction rules for the λ-calculus are the logical reductions, i.e. deal with the elimination of a type construct that has been introduced directly above. In addition to these, Parigot expresses also the structural rules, where elimination takes place for a type constructor that appears in one of the alternative conclusions (the Greek variable is the name given to a subterm): he therefore needs to express that the focus of the derivation (proof) changes, and this is achieved by extending the syntax with two new constructs [α]M and µα.M that act as witness to deactivation and activation, which together move the focus of the derivation.
We will now present the variant of λµ we consider in this paper, as considered by Parigot in [30]; for convenience, we split terms into two categories: we define terms, and control structure: The λµ-terms we consider are: We also define control structure as a subset of terms: To shorten proofs and notation, we will treat µα.M as a term as well, whenever convenient.
As usual, λx.M binds x in M, and µα.
[β]M binds α in M, and the notions of free and bound variables are defined accordingly; the notion of α-conversion extends naturally to bound names, and we assume Barendregt's convention on free and bound variables.
In We define formally how to preform the µ-substitution; this is convenient in later proofs. Definition 1. 4 We define M[N·γ/α] by induction over the structure of terms by: We have the following rules of computation in λµ: Parigot defines a number of reduction rules: two computational rules as well as the simplification rules: which are added mainly to simplify the presentation of his results 2 . Reduction on λµ-terms is defined as the compatible closure of these rules.
It is possible to define more reduction rules, but Parigot refrained from that since he aimed at defining a confluent reduction system. The intuition behind the structural rule is given by de Groote [21]: "in a λµ-term µα.M of type A→B, only the subterms named by α are really of type A→B (. . . ); hence, when such a µ-abstraction is applied to an argument, this argument must be passed over to the sub-terms named by α." In this paper, we will only deal with the logical, structural and renaming rule; this is also the restriction made by de Groote in [21].
Type assignment for λµ is defined by the following natural deduction system; there is a main, or active, conclusion, labelled by a term of this calculus, and the alternative conclusions are labelled by the set of Greek variables α, β, etc. Definition 1.6 (TYPING RULES FOR λµ) Our types are those of Definition 1.2, extended with the type constant ⊥ that is essentially added to express negation, i.e.: The type assignment rules are: We can think of [α]M as storing the type of M amongst the alternative conclusions by giving it the name α -the set of Greek variables is called the set of context variables (or names).
As an example illustrating the fact that this system is more powerful than the system for the λ-calculus, here is a proof of Peirce's Law (due to Ong and Steward [28]): Notice that ⊥ plays no part in this proof. Indeed, we can define the set of types without ⊥; the underlying logic of such a system then corresponds to minimal classical logic [1].
Since we allow ⊥ as a proper type, we can even express negation (of course, it is also implicitly present in the right-hand type environment), and can give a derivation for ¬¬A→A, so can express double negation elimination; so in λµ we can represent full Classical Logic.
Notice that this term is not closed, since β is free, albeit of type ⊥.
De Groote [21] considers a variant of λµ which separates the naming and µ-binding features 3 . This gives a considerable different system, that allows for ¬¬A→A to be inhabited via (the closed term) λy.µα.y(λx. For the moment, we will deal with Parigot's original system only; we aim to extend our results to de Groote's variant in future work.

The Strict Intersection Type Assignment System for the λ-calculus
The remainder of this paper will be dedicated a notion of intersection/union typing on λµ. This will be defined as a natural extension of the Strict Intersection System [2] for the λ-calculus. Before we come to that, we will briefly summarise the latter.

Definition 2.1 (STRICT TYPES)
1. Let ϕ range over an infinite, enumerable set of type variables. The set T s of strict types, ranged over by A, B, etc is defined through the grammar: The set T of intersection types is defined as the union of {⊤} and the closure of T s under intersection; we will use A, B, etc for intersection types as well, and mention which set they belong to when necessary. 2. A statement is an expression of the form M : A, with M ∈ Λ and A ∈ T . M is the subject and A the predicate of M : A. 3. A type-environment Γ is a partial mapping from term variables to intersection types, and we write So if we write a type as A→B, then B ∈ T s , and A ∈ T . In the notation of types, as usual, right-most outer-most parentheses in arrow types will be omitted, and we assume ∩ to bind stronger than →. From hereon, we will write n for the set {1, . . . , n}.
We will consider a pre-order on types which takes into account the idem-potence, commutativity and associativity of the intersection type constructor, and defines ⊤ to be the maximal element.

Definition 2.2
1. The relation '≤' is defined as the least pre-order on T such that: T will be considered modulo ∼; then ≤ becomes a partial order. It is easy to show that both (A∩B)∩C ∼ A∩(B∩C) and A∩B ∼ B∩ A, so the type constructor ∩ is associative and commutative, and we will write ∩ n A i for A 1 ∩· · ·∩ A n , and consider ⊤ to be the empty intersection: ⊤ = ∩ 0 A i . Moreover, we will assume, unless stated explicitly otherwise, that in ∩ n A i each A i is strict.

Definition 2.3
The strict type assignment is defined by the following natural deduction system (where all types mentioned are strict, with the exception of A in rule (→I) and (→E)): We will write Γ ⊢ M : A for statements that are derived using these rules.
Notice that Γ ⊢ M : ⊤ for all Γ, M by rule (∩I). Properties of this system have been studied in [2].

Intersection and union type assignment for λµ
We will now define a notion of type assignment for λµ that uses intersection and union types. We see the context variables α as names for possible continuations that in the philosophy of intersection types need not all be typed with the same type; we therefore allow multiple types for a context variable in the environment ∆, grouped using a new type constructor, which we call union.
Binding a context variable then generates a context switch µα.
[β]M, which naturally has a union type ∪ n A i ; reduction of the term (µα. [β]M)N will bring the operand N to each of the pseudo subterms in M of the shape [α]Q ('named' with α), where Q has type A i ; since N gets placed behind Q, this implies that A i = C i →B i and that therefore the type for α should be ∪ n (C i →B i ); this then also implies that N should have all the types C i (∀i ∈ n); rule (→E) as below expresses exactly that. The only 'functionality' we need for union types therefore is the ability to choose a collection of types for α amongst those stored in ∆; this is represented by rule (∪E).

Definition 3.1 (THE SYSTEM ⊢ ∩∪
λµ ) 1. The set of strict types we consider for the intersection-union type assignment is: As above, we call A 1 ∩· · ·∩ A n (with n ≥ 0) an intersection type, and call B 1 ∪· · ·∪B m (with m ≥ 0) a union type; we use ⊤ for the empty intersection type, and ⊥ for the empty union type. 2. The relation ≤ of Definition 2.2 is extended to intersection-union types by: Notice that we consider union types to be strict as well; this implies that we allow an intersection of union types, a union of union types, but not a union of intersection types.
Definition 3.2 (THE SYSTEM ⊢ ∩∪ λµ ) Intersection-union type assignment for λµ is defined via: We write Γ ⊢ ∩∪ λµ M : A | ∆ if this statement is derivable using these rules.
We will normally not distinguish between the two variants of (∪E). Notice that the traditional (→E) of Definition 2.3 is obtained by taking n = 1. Moreover, all A i can be intersection types, so each can be ⊤; this is why that rule is not formulated using Γ ⊢ ∩∪ λµ N : ∩ n A i | ∆. If x:∪ m B j ∈ Γ, then we can only derive Γ ⊢ ∩∪ λµ x : ∪ m B j | ∆, i.e. we have no way of eliminating a union assigned to a term variable. Moreover, we have no traditional rules (∪I) and (∪E) on terms, which would be formulated (as in [9]), via (∪I) : These create the subject-reduction problem dealt with in that paper by limiting to parallel reduction.
Notice that both the strict system for the λ-calculus and the system for λµ are true subsystems; the first by not allowing union types, or alternative conclusions, the second by limiting to Curry types.
Proof. By easy induction.  .[δ]x) : A→B | , since the two occurrences of [δ] need to be typed differently, but with related types. This is comparable to both A and A→B to be needed as assumption for x to type λx.xx.
We can show that a general (∩E) (for all terms) is admissible.
The following result is standard.
Proof. By easy induction.
As a consequence, the following rules are admissible: (T ) :

Subject reduction and expansion
We will now show our main results, by showing that our notion of type assignment is sound and complete. We start by showing two variants of the substitution lemma.
Then by induction, there are C 1 , C 1 2 , . . . , C r 2 such that: • Γ, x: Because of Lemma 3.4, we can extend the above results also to the case that A is an intersection type; notice that this is implicitly used in the third case, where D j can be an intersection type.
Dually, we have: Proof. We only show the interesting cases. ⇒ : Let C = ∪ r C j , with r ≥ 1. Then, by Lemma 3.3, there exists D j ∈ T (∀j ∈ r) such that  such that, without loss of generality, ∪ r (E l →D l ) ∪ ∪ n−r B i = ∪ n B i , and the derivation is shaped like (notice that we can assume γ, β ∈ fv (N)): Then, by induction, there exist A i (∀i ∈ n−r) such that Γ ⊢ ∩∪ λµ M : B n | α:∪ n−r (A i →B i ), β:C, ∆ and, for all i ∈ n−r, Γ ⊢ ∩∪ λµ N : A i | ∆, and we can construct:   [β]M)N : A | ∆, then by Lemma 3.3 there exist A i (∀i ∈ n) and C i (∀i ∈ n) such that A = ∪ n A i , and Γ ⊢ ∩∪ λµ µα.