Jacques Darn

Co-induced actions for topological and filtered groups

Co-induced actions for topological and filtered groups

Introduction

The present paper deals with the study of actions in some categories of topological and filtered groups. The author's main motivation is the study of strongly central filtrations on groups (also called N-series). These occur in several contexts. For instance:

• On the Torelli subgroup of the automorphisms of free groups, there are two such filtrations defined in a canonical way ; the Andreadakis problem, still very much opened, asks the question of the difference between them.

• On the Torelli subgroup of the mapping class groups of a surface, the Johnson filtration is a N-series. The difference between this filtration and the lower central series is linked to invariants of 3-manifolds, such as the Casson invariant.

• On the pure braid groups or the pure welded braid groups, such filtrations appear in the study of Milnor invariants and Vassiliev invariants.

Considering strongly central filtrations as a category has led to a better understanding of phenomena appearing in these various contexts, in particular the role of Johnson morphisms, or semi-direct product decompositions of certain associated Lie algebras.

At the heart of this work lies the study of actions in this category. Our main result here is a further step in that direction:

Theorem 2.1. The category of strongly central filtrations admits co-induction functors along any morphism α : E * → B * , that is, a right adjoint to the restriction of B *actions along α, for all α.

Moreover, our methods can be adapted to the case of topological groups, to show:

Theorem 3.1. In the category of topological groups, there are co-induction functors along any morphism between locally compact groups.

If we restrict our attention to a convenient category of topological spaces, then more is true: Theorem 3.2. A convenient category of topological groups admits co-induction functors along all morphisms.

This last result can also be seen as an enriched version of the existence of coinduction in the category of groups, obtained from Kan extensions.

Strongly central filtrations and actions

Strongly central filtrations

We recall the definition of the category

SCF introduced in [Dar18]. Definition 0.1. A strongly central filtration G * is a nested sequence of groups G 1 ⊇ G 2 ⊇ G 3 • • • such that [G i , G j ] ⊆ G i+j
for all i, j 1. These filtrations are the objects of a category SCF , where morphisms from G * to H * are those group morphisms from

G 1 to H 1 sending each G i into H i .
Recall from [Dar18] that this category is complete, cocomplete, and homological, but not semi-abelian. It is also action-representative.

Actions

In a protomodular category C, an action of an object B on an object X is a given isomorphism between X and the kernel of a split epimorphism with a given section Y B . Objects of C endowed with a B-action form a category, where morphisms are the obvious ones. This category of B-objects is the same as the category of split epimorphisms onto B with given sections, also called points over B, and is denoted by P t B (C).

For example, an action in the category of groups is a group action of a group on another, by automorphism (see for instance [START_REF] Borceux | Internal object actions[END_REF]). The equivalence between B-groups (in the last sense) and B-points is given by:

B G -→ B ⋊ G B .
The same construction allows us to identify the category of B-points in topological groups with the category of topological groups G endowed with a topological B-action, i.e. a group action such that

B × G → G is continuous. Recall from [Dar18, Prop. 1.20] that in SCF , an action of B * on G * is the data of a group action of B 1 on G 1 such that [B i , G j ] ⊆ G i+j for all i, j
1, where the commutator is taken in the semi-direct product

B 1 ⋉ G 1 , that is: [b, g] = (b • g)g -1 .

Restriction and induction functors

Suppose that our protomodular category C admits finite limits and colimits. Let α : E → B be a morphism in C. We can restrict a B-action along α by pulling back (in C) the corresponding epimorphism. This defines a restriction functor (also called base-change functor ):

α * : P t B -→ P t E .

If we are given a E-action, we can define the induced B-action by pushing out (in C) the corresponding section. This defines an induction functor α * , which is left adjoint to α * . A question then arises naturally: is there a co-induction functor ? That is, when does the restriction functor α * also have a right adjoint ? When all α have this property, the category is called Locally Algebraically Cartesian Closed (LACC). This is a rather strong condition, implying for instance algebraic coherence [CGV15, Th. 4.5]. This condition has been studied for example in [START_REF] James | Algebraic exponentiation in general categories[END_REF][START_REF] Bourn | Aspects of algebraic exponentiation[END_REF].

Acknowledgements: The author thanks Tim Van der Linden for asking the question which became the starting point of this work, and for inviting him in Louvain-la-Neuve, where we had the most interesting and helpful discussions. He also thanks Alan Cigoli for taking part in these discussions and making some very interesting remarks. 1 Co-induction in the category of groups

Our aim is to show that the category SCF is LACC, that is, that it admits co-induced actions. We first review the case of groups, that will be the starting point of our construction.

The construction of co-induced group actions follows easily from the following fact: if B is a group, the category P t B (Grps) of B-groups identifies with the functor category Fct(B, Grps), where B is considered as a category with one object. Then the restriction functor α * along a group morphism α : E → B is given by precomposition by α (interpreted as a functor between the corresponding small categories). Since Grps is complete and co-complete, this functor has both a left and a right adjoint, given by left and right Kan extensions along α.

Let us describe the right adjoint of α * in this context. If ϕ : C → D is a functor between small categories, recall that the right Kan extension of F : C → T along ϕ is given by the end formula:

Ran ϕ (F ) = c∈C hom(D(-, ϕ(c)), F (c)),
where hom denote the co-tensor over Sets: if T is a set, and T ∈ T , then hom(X, T ) = T X is the product of X copies of T .

In our situation (ϕ = α, and 2 Co-induction in the category SCF The construction described above in the category of groups seems to be very specific, as it relies on an identification between the categories of points and functor categories. Such an identification does not hold in the case of strongly central filtrations. However, we will be able to compare the categories of points with functor categories. This will allow us to use Kan extensions for constructing co-induction.

F = Y is a B-group),

Categories of points and functor categories

When dealing with a strongly central filtration G * , we will often omit the subscript 1, for short, denoting the underlying group G 1 by G.

Let B * be a strongly central filtration. There is an obvious forgetful functor, recalling only that B acts by automorphisms preserving the filtration:

ω : P t B * (SCF ) -→ Fct(B, SCF ).
Since the compatibility conditions it forgets are only conditions on objects, not on morphisms, this functor is fully faithful. Let α : E * → B * be a morphism in SCF . The restriction functor α * 1 between the corresponding functor categories fits into a commutative diagram:

P t B * (SCF ) Fct(B, SCF ) P t E * (SCF ) Fct(E, SCF ). ω α * α * 1 ω
Moreover, since SCF is complete, α * 1 has a right adjoint, given by the right Kan extension (α 1 ) ! . It follows from the description of limits in SCF [Dar18, Prop. 1.10] and from the construction of Section 1 that (α 1 ) ! (Y * ) is hom E (B, Y * ), that is, the filtration defined pointwise on hom E (B, Y ) (which is obviouly strongly central).

If we construct a right adjoint t to the forgetful functor ω (for any B * ), then by composing adjunctions, t • (α 1 ) ! will be right adjoint to α * 1 • ω, and t • (α 1 ) ! • ω will be right adjoint to α * , because ω is fully faithful:

Hom (α * (X * ), Y * ) = Hom (ω • α * (X * ), ω(Y * )) = Hom (α * 1 • ω(X * ), ω(Y * )) = Hom (X * , t • (α 1 ) ! • ω(Y * )) .
We will construct this functor t = t ∞ (B * , -) in the next section. This will finish the proof of our first main theorem: Theorem 2.1. There are co-induction functors in SCF . Explicitly, co-induction along α : E * → B * is given by:

Y * -→ α ! (Y * ) = t ∞ (B * , hom E (B, Y * )),
which is the largest strongly central filtration smaller than hom E (B, Y * ) on which B * acts.

Maximal B * -filtration

Since the forgetful functor ω : P t B * (SCF ) → Fct(B, SCF ) is fully faithful, if it admits a right adjoint t, then the counit ωt(G * ) → G * has to be a monomorphism. Thus, if G * is a strongly central filtration on which B acts by automorphisms preserving the filtration, we need to construct the maximum sub-object of G * such that the restricted action of B satisfies the conditions defining a B * -action. We will do so through a limit process, restricting to smaller and smaller subgroups endowed with smaller and smaller filtrations. Corollary 2.3. The forgetful functor ω : P t B * (SCF ) → Fct(B, SCF ) has a left adjoint t, the filtration t(G * ) being the greatest filtration constructed in the above proposition.

Proof. Suppose that B * acts on K * , that the group B acts on G * (by filtrationpreserving automorphisms), and that f : K * → G * is a B-equivariant morphism. Then B * acts on f (K * ) ⊆ G * . As a consequence, f (K * ) ⊆ t(G * ), so that f is in fact a morphism from K * to t(G * ).

Lemma 2.4. Under the hypothesis of the proposition, the filtration defined by:

t i (B * , G * ) := { g ∈ G j | ∀j, [B j , g] ⊆ G i+j }
is strongly central, and stable under the action of B.

Proof. For short, denote t * (B * , G * ) by t * . These are subgroups of G because of the normality of G i+j and the formula [b,

gg ′ ] = [b, g] • ( g [b, g ′ ]). The three subgroups lemma applied in B⋊G tells us that [B k , [t i , t j ]] is contained in the normal closure of [[B k , t i ], t j ] and [[B k , t j ], t i ]. These are both inside G i+j+k , which is normal in B ⋊ G because it is normal in G and B-stable. Thus [B k , [t i , t j ]] ⊆ G i+j+k ,
which means exactly that [t i , t j ] ⊆ t i+j . Each t i is also stable under the action of B, since if b ∈ B, using that the B j and the G k are B-stable, we have that [B j , t

b i ] = [ b B j , t i ] b ⊆ [B j , t i ] b ⊆ G b i+j ⊆ G i+j , thus t b i ⊆ t i . Proof of
∀i, j, l, [B j , t ∞ i (G * )] ⊆ [B j , t l+1 i (G * )] ⊆ t l i+j (G * ),
so that by taking the intersection on l,

∀i, j, [B j , t ∞ i (G * )] ⊆ t ∞ i+j (G * ).
Secondly

Co-induction for topological groups

Our argument for strongly central filtrations can be adapted to the case of topological groups. The first part, about Kan extension, is exactly the same. The comparison between the category of points and functors categories, however, does only work with some restrictions : we need either the acting group to be locally compact, or the category of topological spaces to be a convenient one, for example the category of compactly generated weakly Hausdorff spaces. The main idea behind the construction is the same as before: restricting to smaller and smaller subgroups, and refining more and more the topology.

Categories of points and functor categories

A topological group is the data of a group G and a topology τ on it, with the usual compatibility requirements [Bou71, Chap. 3] ; it can be seen as a group object in the category of topological spaces. We will denote such an object by (G, τ ), or only by G or by τ , whenever the rest of the data is clear from the context. Also, in any topological group G and any point g ∈ G, we will denote by V G (g) the set of neigbourhoods of g in G. Note that the only topologies we will consider are the ones compatible with group structures ; expressions such as "the finest topology satisfying..." have to be understood with this requirement in mind. Topological groups, together with continuous morphisms, form a category T opGrp, which is complete, cocomplete, and homological.

If B is a topological group, the obvious forgetful functor ω from P t B (T opGrp) to Fct(B, T opGrp) is fully faithful. If α : E → B is a continuous morphism, then restriction along α is defined in the usual way, between the category of points and between the categories of functors. The picture is exactly the same as in the case of strongly central filtrations, and the right Kan extension along α is defined in the same way: α ! (Y ) = hom E (B, Y ) ⊆ Y B , endowed with the topology inherited from the product topology on Y B . We will show below (Proposition 3.3) that the forgetful functor admits a right adjoint for any locally compact B. Thus we will have proved: Theorem 3.1. There are co-induction functors along morphisms between locally compact groups in T opGrp. Explicitly, co-induction along α : E → B is given by:

Y -→ α ! (Y ) = t ∞ (B, hom E (B, Y )),
which is the largest topological group endowed with an monomorphism into hom E (B, Y ), on which B acts continuously.

We want to define the coarsest topology on G 1 making a : B × G 1 → G continuous. Such a topology exists, as it is the coarsest topology making ā : G 1 → C(B, G) continuous, which is exactly the subspace topology on G 1 ⊆ C(B, G). We denote it by τ 1 . Remark that τ 1 is finer than the subgroup topology on G 1 ⊆ G, because a(1, -) is exactly the inclusion G 1 ֒→ G, that has to be continuous when G 1 is endowed with τ 1 .

Lemma 3.6. The group B acts on C(B, G), whence also on (G 1 , τ 1 ), by continuous automorphisms.

Proof. The action of b ∈ B on C(B, G) is given by pre-composition by (-) • b, which is continuous. By functoriality of C(-, G), it is continuous. Moreover, since the group law is defined pointwise on the target, it acts via an automorphism: b

• (uv) = uv(-• b) = u(-• b)v(-• b) = (b • u)(b • v).
Lemma 3.7. Let B act topologically on a topological group X, and f : X → G be a continuous B-equivariant map. Then f (X) ⊆ G 1 and f :

X → (G 1 , τ 1 ) is continuous. Proof. The map (b, x) → f (b•x) is the composite B ×X → X f → G, so it is continuous. Its adjoint x → f (-• x)
is also continuous and, since it coincides with x → (-) • f (x), it factorizes as a set map through G 1 , which means that f takes values in G 1 . Moreover, f is a continuous map from X to the subspace G 1 of C(B, G).

Proof of Proposition 3.3. Let (G, τ ) be a topological group on which B acts by continuous automorphisms. We iterate the construction t : G → (G 1 , τ 1 ) described above. This is possible thanks to Lemmas 3.5 and 3.6. We denote by (G l , τ l ) the l-th iterate t l (G), and we define t ∞ (G) as the intersection G ∞ of the G l , endowed with the reunion τ ∞ of the τ l | G∞ . That is, G ∞ is the (topological) projective limit of the G l .

We first show that the action of B on G ∞ is topological, that is, that B ×G ∞ → G ∞ is continuous. This is equivalent to the map B × G ∞ → G l being continuous for every l. But this last map can be seen as the composite B ×G ∞ → B ×G l+1 → G l , and these maps are continuous by construction, so the action of B on G ∞ is indeed topological. Now suppose that B acts topologically on X, and f : X → G is a continuous Bequivariant map. Then, thanks to Lemma 3.7, f : X → (G 1 , τ 1 ) is again a continuous B-equivariant map, and by iterating the construction, we see that f : X → t l (G) is, for all l. Thus f takes values in G ∞ and is continuous with respect to τ ∞ . Since any continuous B-equivariant map f : X → t ∞ (G) comes uniquely from such an f (which is continuous because the injection of G ∞ into G is, since it is a G∞ (1, -)), we have showed that t ∞ is the right adjoint we were looking for.

Restricting to a convenient category of spaces

If B is any topological group acting on another topological group G, there does not seem to be a coarsest topology τ 1 on G 1 making B ×G 1 → G continuous, so our construction fails to produce an adjoint to the corresponding forgetful functor. However, we can change that by restricting to a convenient category of topological spaces. We need this category T to satisfy the following four hypotheses:

• T is a full subcategory of topological spaces containing the one-point space.

• T admits (small) limits.

• T is cartesian closed.

• If a subset X of an object T ∈ T is given, there should be a topology τ on X such that (X, τ ) is in T , the injection (X, τ ) ֒→ T is continuous, and every f : The point, being final in T , is the unit of the cartesian monoidal structure. Thus the forgetful functor to sets is T ( * , -). In particular, if we denote by C(B, -) the right adjoint to B × (-), the underlying set of C(B, X) is the set of continuous maps from B to X:

Y → T in T such that f (Y ) ⊆ X defines a continuous map f : Y → (X, τ ).
T ( * , C(B, X)) = T (B × * , X) = T (B, X).
Moreover, the underlying set of a limit is the limit of the underlying diagram to sets. Indeed, if D is a small category and F : D → T is a diagram, then :

T ( * , lim F ) = lim T ( * , F ).

The reader can check that the constructions of the previous paragraph work well under these hypotheses, replacing the category T opGrp by the category T Grp of group objects in T . Precisely, the topology τ 1 has to be the T -subspace topology on G 1 ⊆ C(B, X), and G ∞ has to be the limit of the G l in T . Thus we can state: Proposition 3.9. For any topological group B ∈ T Grp, the forgetful functor from P t B (T Grp) to Fct(B, T Grp) has a right adjoint.

Remark that this proposition, together with the following fact, suggest that T Grp is a nice category to work with. Thus the same construction as in ordinary groups (Section 1) works here, replacing Kan extensions by enriched Kan extensions. This uses the fact that T Grp is Tcomplete (that is, it is complete and co-tensored over T ).

This gives an alternative proof of Theorem 3.2. However, neither Theorem 3.1 nor Theorem 2.1 fits in this machinery. Moreover, Proposition 3.9 is still meaningful in this context: it provides a right adjoint to the forgetful functor from the category Fct T (B, T Grp) of enriched functors to the category Fct(B, T Grp) of non-enriched ones.

Contents1

  Co-induction in the category of groups 3 2 Co-induction in the category SCF 4 2.1 Categories of points and functor categories . . . . . . . . . . . . . . . . 4 2.2 Maximal B * -filtration . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3 Co-induction for topological groups 6 3.1 Categories of points and functor categories . . . . . . . . . . . . . . . . 6 3.2 Maximal B-topology . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.3 Restricting to a convenient category of spaces . . . . . . . . . . . . . . 8

  the coend is taken over the one object * of E. Moreover, hom(B( * , α( * )), Y ( * )) is the group of applications from B to Y (whose product is defined pointwise), and the coend is the subgroup of applications u satisfying u(α(e)b) = e • u(b) for all e ∈ E and b ∈ B, that is, the subgroup of E-equivariant applications hom E (B, Y ). The action of B on hom E (B, Y ) is given by (b • u)(-) = u(-• b). Thus, we recover: Proposition 1.1. [Gra12, Th. 6.11]. In the category of groups, co-induction along a morphism α : E → B is given by Y -→ hom E (B, Y ), where hom E (B, Y ) is the group of E-equivariant applications from B to Y (with multiplication defined pointwise), on which B acts by (b • u)(-) = u(-• b).

  Proposition 2.2. Let B * and G * be strongly central filtrations, and let B = B 1 act on G = G 1 by group automorphisms preserving the filtration G * . Then there exists a greatest one among those strongly central filtrations H * ⊆ G * such that the action of B on G induces and action of B * on H * .

Fact 3. 10 .

 10 The category T Grp is also action-representative: a representant of actions on G is the set of continuous automorphisms Aut(G) ⊂ C(G, G), endowed with the T -subspace topology.A remark on T -denriched categoriesTheorem 3.2 can be obtained directly, in a fashion similar to the construction of coinduction for groups. To do that, we use the language of T -enriched categories [Kel05]. The category T Grp is T -enriched ; moreover, every T -group B can be considered as a T -category with one object, and there is an obvious equivalence: P t B (T Grp) ≃ Fct T (B, T Grp).

  , if B * acts on H * ⊆ G * , then by we show that H * ⊆ t l

* (G * ) for all l: by definition, H * ⊆ G * = t 0 * (G * ), and if H * ⊆ t l * (G * ) for some l, then: ∀i, j, [B i , H j ] ⊆ H i+j ⊆ t l i+j (G * ), proving that H * ⊆ t * (B * , t l * (G * )) = t l+1 * (G * ), and our claim.

  Such a topology is called the T -subspace topology on X. Fact 3.8. [Str09, Prop. 2.12, Lem. 2.28 and Prop. 2.30]. These hypotheses are satisfied if T = CGW H is the category of compactly generated Hausdorff spaces.

Note that it is not the largest topological subgroup, as largest here also mean: endowed with the coarsest possible topology.

If we restrict our category of topological spaces (for example to compactly generated weakly Hausdorff spaces), then we will show (Proposition 3.9) that our construction works for all group object B. Theorem 3.2. There are co-induction functors in the category of topological groups (that is, it is LACC) when the base category of topological spaces is the category CGW H of compactly generated weakly Hausdorff spaces, or any convenient category of topological spaces, is a sense made precise below.

Maximal B-topology

Suppose that B is locally compact (note that we do not imply that it is locally Hausdorff). We now construct the right adjoint to the forgetful functor, in a series of lemmas leading to the proof of: Proposition 3.3. For any locally compact topological group B, the forgetful functor from P t B (T opGrp) to Fct(B, T opGrp) has a right adjoint.

We will make use of the classical : Consider G an element of Fct(B, T opGrp). This means that G is a topological group endowed with an action of the discrete group B via continuous automorphisms. If H G is a subgroup, consider the map:

obtained by restriction of the action of B on G. How can we endow H with a new topology such that a H is continuous ? In order to do this, we first need to restrict to a subgroup of G. Indeed, if a H is continuous (for any topology on H), then for any g ∈ H, the map a H (-, g) = (-) • g : B → G has to be continuous. Thus we are led to the definition:


Y Jannot

A Degiovanni

M Camus

Extension of the thermal porosimetry method to high gas pressure for nanoporosimetry estimation

Keywords: Insulating material, nano-porosimetry, pore size distribution, thermal conductivity, pressure, vacuum

Standard pore size determination methods like mercury porosimetry, nitrogen sorption, microscopy or X-ray tomography are not suited to highly porous, low density and thus very fragile materials. For this kind of materials, a method based on thermal characterization has been developed in a previous study. This method has been used with air pressure varying from 10 -1 to 10 5 Pa for materials having a thermal conductivity less than 0.05 W m K at atmospheric pressure. It enables the estimation of pore size distribution between 100 nm and 1 mm. In this paper, we present a new experimental device enabling thermal conductivity measurement under gas pressure up to 10 6 Pa, enabling the estimation of the volume fraction of pores having a 10 nm diameter. It is also demonstrated that the main thermal conductivity models (Parallel, Series, Maxwell, Bruggeman, Self-consistent) lead to the same estimation of the pore size distribution as the extended parallel model (EPM) presented in this paper and then used to process the experimental data. Three materials with thermal conductivities at atmospheric pressure ranging from 0.014 W m K to 0.04 W m K are studied. The thermal conductivity measurements results obtained with the three materials are presented and the corresponding pore size distributions between 10 nm and 1 mm are presented and discussed.

Introduction

Thermal porosimetry is a method developed for the estimation of pore size distribution in a porous medium. This method takes place as a complement to other classical methods such as mercury porosimetry [START_REF] Washburn | Note on a method of determining the distribution of pore sizes in a porous material[END_REF][START_REF] Pirard | Characterization of porous texture of hyperporous materials by mercury porosimetry using densification equation[END_REF][START_REF] Rigby | Characterization of porous solids using integrated nitrogen sorption and mercury porosimetry[END_REF] , gas sorption [START_REF] Saleh | Caractérisation et analyse des poudres -Propriétés physiques des solides divisés[END_REF][START_REF] Barrett | The determination of pore volume and area distributions in porous substances. I. Computations from nitrogen isotherms[END_REF][START_REF] Rouquerol | Texture des matériaux pulvérulents ou poreux[END_REF] or imagery [START_REF] Lux | Comportement thermique macroscopique de milieux fibreux réels anisotropes : étude basée sur l'analyse d'images tridimensionnelles[END_REF][START_REF] Kaemmerlen | Transfert de chaleur à travers les isolants thermiques du bâtiment[END_REF] . It is based on the processing of thermal conductivity measurements performed on a sample set in an enclosure with variable air pressure. For highly porous and insulating materials, the thermal conductivity of the sample is sensitive to the thermal conductivity of the air and thus to the size of the containing pore [START_REF] Collishaw | An assessment of expressions for the apparent thermal conductivity of cellular materials[END_REF] . O.J. Lee et al. [START_REF] Lee | Determination of mesopore size of aerogels from thermal conductivity measurements[END_REF] already used this sensitivity to deduce information about the pores size from thermal conductivity measurements under various air pressure values. Felix et al. [START_REF] Félix | Thermoporosimetry: a new method to estimate pore size distribution in highly porous insulating materials[END_REF] develop a method to estimate pore size distribution between 100 nm and 1 mm by processing thermal conductivity measurements realized under gas pressures varying from 1 to 10 5 Pa. They also validate the method with materials having a thermal conductivity lower than 0.05 W m K .

In this paper we present a new experimental device enabling the measurement of the thermal conductivity of a porous medium under a gas pressure up to 10 6 Pa, extending the estimation of the pore size distribution between 10 nm and 1 mm. Then the results obtained with three materials with thermal conductivities ranging from = 0.014 W m K to 0.04 W m K under normal gas pressure are given. Finally the pore size distributions of each material between 10 nm and 1 mm are presented.

Theoretical background

Thermal conductivity of the air

A highly porous material is mainly composed of air which thermal conductivity is a function of both its pressure and the size of its containing cavity. Indeed, if the mean free path of gaseous molecules is high related to the mean distance between the cavity walls, those molecules only interact with the walls, so that the heat conduction property is governed by the pore size, this is called the Knudsen effect. As a consequence, pore size is an important parameter in the equation of the thermal conductivity of the air that is confined into a pore. For spherical pores, that equation comes under the form [START_REF] Collishaw | An assessment of expressions for the apparent thermal conductivity of cellular materials[END_REF] :

, = ,! (1)
With: " Thermal conductivity of the air at atmospheric pressure (0.026 W.m -1 .K -1 ) Constant, = 1.5 for air [START_REF] Collishaw | An assessment of expressions for the apparent thermal conductivity of cellular materials[END_REF] The Knudsen number #$ , is calculated by:

#$ , = % ! (2)
With:

Pore diameter (m) Mean free path, its value for air is 12 : = 2.27 × 10 ) * (3) + Temperature (K) Air pressure (Pa) Fig. 1 shows that the thermal conductivity of the air does not vary in the same pressure range for different values of . It also shows that thermal conductivity of air in the pores with a 10 nm diameter varies significantly only for gas pressure values between 10 5 Pa and 10 6 Pa.

Thermal conductivity of porous media

The material is considered as a heterogeneous porous medium which global porosity ratio is , = 1 -, . , composed of a solid phase characterized by its thermal conductivity . and / fluid phases (air). Each fluid phase correspond to a class of pore diameter with thermal conductivity , and volume fraction , , . Several models can be used to predict the thermal conductivity of the equivalent homogeneous medium 01! = 23, . , . , , , , , 4. According to Felix et al [START_REF] Félix | Thermoporosimetry: a new method to estimate pore size distribution in highly porous insulating materials[END_REF] , the most suited ones for low density thermal insulators are the parallel model (PM) and a combined serial/parallel (CSP) model developed by these authors [START_REF] Félix | Thermoporosimetry: a new method to estimate pore size distribution in highly porous insulating materials[END_REF] . The later one was developed to represent the thermal conductivity of materials which thermal conductivity verifies:

5 60 -7 " 89 0: > , . . (4)
In this case, the parallel model can no longer represent the thermal conductivity on all the pressure range.

In fact, to estimate the pores size distribution, one only needs the form of the curve = 2 , the amplitude enabling the estimation of the thermal conductivity of the solid phase.

It is thus possible to process only the reduced thermal conductivities curves defined as:

* = =>? @ ( 5
)
Where A is the thermal conductivity for → ∞ and " is the thermal conductivity for → 0.

We will show that for low density porous materials (, > 0,80), all the main thermal conductivity models leads to similar curves for * . It is the reason why the thermal porosity method is a robust method, leading to the same estimation of the pore size distribution whatever the model used. On the contrary, the estimated value of the solid phase thermal conductivity highly depends on the model used.

We have thus chosen the model closer to the physics of the considered materials, i.e. the parallel model, hence:

* = =>? @ = ∥ ∥ @∥ ∥ (6)
Thus:

01! = ∥ ∥ @∥ ∥ A -" + " (7)
With for the parallel model: ∥ = , . . + ∑ ,

And: "∥ = , . .

Thus:

01! = A -" / A∥ -"∥ ∑ , + " (10)
The model used for the estimation called the extended parallel model (EPM) can then be expressed as:

01! = ∑ , + " (11)
Where and " are two unknown parameters to be identified. The figures represent the simulated thermal conductivities and their reduced values as a function of the gas pressure for 8 models and for 3 types of products representing the products that will be further studied and a cellular concrete.

The models are: -The Maxwell model 13 : (1) -The parallel model: (

-The series model: (3) -The Bruggeman models 14 : (4), ( 5) and ( 6), the last one being the average of ( 4) and ( 5) -The self-consistent model 15 (7) -The combined series-parallel model CSP [START_REF] Félix | Thermoporosimetry: a new method to estimate pore size distribution in highly porous insulating materials[END_REF] .

The expressions of the thermal conductivity given by these models are presented in the Appendix.

For the comparison, the considered typical porous materials have two pores sizes, which are described in Table 1. To be more realistic, we have used the properties that have been estimated from experimental curves. The figures 2 to 4 show that the thermal conductivities simulated with the different models are quite different but that the reduced ones are rather the same for three first materials having high porosities: Nano-T, super-insulator and Pavapor.

Figure 2: Thermal conductivity (and reduced one * ) of Nano-T, simulated by different models

One can wonder if the method could be extended to lower porosity materials such as cellular concrete (with 0.65 porosity) which characteristics are given in Table 1. The eight models have been tested on this material. Figure 5 shows that in this case even the reduced thermal conductivity curves obtained with the different models cannot be assimilated to a unique curve. Thus, the estimated pore size distribution will depends on the thermal conductivity model used for the estimation. The thermal porosimetry technique is thus only suited to high porosity insulating materials with a porosity greater than 0.80. The presented models only take into account the conduction heat transfer. Nevertheless, radiation heat transfer may be significant especially in low density porous media. In fact, since all the experiments are carried out at the same temperature and radiation is independent on gas

λ (Wm -1 K -1 ) (1) (2) (3) (4) (5) (6) (7) (8)
λ (Wm -1 K -1 ) (1) (2) (3) (4) (5) (6) (7) (8) -1 0 1 2 3
λ (Wm -1 K -1 ) (1) (2) (3) (4) (5) (6) (7) (8)
λ (Wm -1 K -1 ) (1) (2) (3) (4) (5) (6) (7) (8)
λ* (1) (2) (3) (4) (5) (6) (7) (8)
pressure, the contribution of the radiation heat transfer is included in the estimated parameter independent on the gas pressure, i.e. the thermal conductivity of the solid phase. Particularly, when the equivalent thermal conductivity is extrapolated for a null gas pressure, the obtained value takes into account both the conduction in the solid phase and the radiation.

Materials and methods

Materials and devices

This study has been carried out on insulating materials for which density and global porosity have been measured using a helium pycnometer device [START_REF] Bal | Water content dependence of the porosity, density and thermal capacity of laterite based bricks with millet waste additive[END_REF] : -A super-insulating material with a density N = 116.8 kg m H and a global porosity , = 0.901.

-"Nano-T" commercialized by Final Materials that is an insulating material design for high temperature applications with a density N = 247.7 kg m H and a global porosity , = 0.877.

-"Pavapor" that is a fibrous wood-based material commercialized by Pavatex with a density N = 152.9 kg m H and a global porosity , = 0.896.

Thermal conductivity measurements have been done using the centered hot plate method [START_REF] Jannot | A centered hot plate method for measurement of thermal properties of thin insulating materials[END_REF] with 100 × 100 mm 2 cross section samples. The measurement device (see figure 6) has been placed inside a chamber in which pressure is controlled between 10 -1 and 10 6 Pa. Fig. 1 shows that the thermal conductivity of the air stops decreasing under 10 -1 Pa if the pores size is lower than 1 mm. Apparently, the considered materials have not any pore greater than 1 mm, so measuring conductivities at lower pressures than 10 -1 Pa would not bring any useful information.

Estimation method

The first step is to measure the thermal conductivity of the materials under different pressures varying between 10 -1 and 10 6 four different pressures for each pressure decade, such as represented on figure 7 giving an example of a measurement set.

Figure 7: Example of thermal conductivity measurements used for the estimation of pore size

The inversion process is built on the principle of minimization of the sum of the quadratic differences, given by relation (12), and the modeled values 01! using the Levenberg-Marquardt algorithm. The estimate 8 parameters: " , followings:

min ∑ 3 01!, -UVW, 4 X Y5 0 Z , , Z 1 ∑ , , [ 5 1 -, .

Standard deviations of the estimated parameters

Thermal conductivity measurements using the hot plate method are deduced from the expression: Two kinds of errors can be done on th -A systematic error on each experimental value of the thermal conductivity which depends on the knowledge of the thickness According to their conclusions, the value / 6 was chosen with the following mean diameter values of the pores: 10 nm, 100 nm, 1µm, 10 µm, 100 µm and 1 mm. The first step is to measure the thermal conductivity of the materials under different pressures [START_REF] Rouquerol | Texture des matériaux pulvérulents ou poreux[END_REF] Pa. Typically, the thermal conductivity is measured for four different pressures for each pressure decade, such as represented on figure 7 giving an example of a measurement set.

Figure 7: Example of thermal conductivity measurements used for the estimation of pore size distribution

The inversion process is built on the principle of minimization of the sum of the quadratic given by relation (12), between the thermal conductivity experimental data 01!, calculated using relation (11). The minimization is achieved Marquardt algorithm. The thermal conductivity EPM and six values of , . The minimization constraints are the 4

Standard deviations of the estimated parameters

conductivity measurements using the hot plate method are deduced from the thickness (m) Electrical resistance of the heating element (Ω) Current intensity passing through the heating element (A) Surface of the heating element (m 2 ) Temperature difference between the heated surface of the sample and the constant temperature surface (°C) Two kinds of errors can be done on these measurements: error on each experimental value of the thermal conductivity which depends on the knowledge of the thickness b (± 1%) and of the surface f (± 2%), which introduce a 8 was chosen with the following m and 1 mm.

The first step is to measure the thermal conductivity of the materials under different pressures Pa. Typically, the thermal conductivity is measured for at least four different pressures for each pressure decade, such as represented on figure 7 giving an The inversion process is built on the principle of minimization of the sum of the quadratic experimental data UVW, minimization is achieved EPM model requires to . The minimization constraints are the (12) (13) (14) conductivity measurements using the hot plate method are deduced from the (15) Temperature difference between the heated surface of the sample and the constant error on each experimental value of the thermal conductivity which depends on 2%), which introduce a constant deviation equal to ± 3% on the measured values. -A random error, different for each point due to the accuracy of the current e measuring device (± 1%) and of the temperature acquisition chain which is evaluated at 0.1 °C for a Δ+ of 10 °C representing a ± 1% deviation. The total random deviation is so estimated at ± 2% of the measured value. The error on the global porosity ratio using the Helium pycnometer [START_REF] Bal | Water content dependence of the porosity, density and thermal capacity of laterite based bricks with millet waste additive[END_REF] has been considered constant and equal to ± 2%. Finally, the uncertainty on pressure measurements has been evaluated at ± 5% of the measured value. Standard deviations of the estimated parameters ( " , , , , ) have been calculated by a statistical method. Modeled thermal conductivities 01! have first been computed taking the estimated parameters as nominal values and considering the biased value , . + , . of the solid volume fraction , . (so that the uncertainty on the global porosity ratio , is considered); Then, the obtained values of the thermal conductivities and the experimental pressure values are noised # times as describes by relations ( 16) and ( 17):

h,Y = Y + i h,Y (16)
h,Y = 01! + + i′ h,Y ′ (17)
Where: 1 < l < # and: Random number (uniform density of probability between -1 and +1) Maximum value of the systematic error on due to the errors on b and f ′ Uncertainty due to random error on e and Δ+ Uncertainty due to random error on

The # noised curves h have been considered as 'numerical' experiments and a set of optimal parameters ( " , , , , ) has been estimated for each curve. Finally the mean values and the standard deviations of the # estimated values for each parameter have been calculated. To have a good statistic representation, # has been set to 1000.

Results and discussion

The results obtained by processing the thermal conductivity measurements of the three studied materials are presented in this part. Measurements have then been processed considering the global porosity ratio as a known parameter measured by Helium pycnometry.

Figure 8 representing the thermal conductivity vs gas pressure shows a very good fitting of the experimental points by the EPM model, with very low residues centered on the null value. Figure 9 representing the volume fraction for each pore size class shows that a porous material must contain a high percentage of nanopores to be super-insulating. The estimated pores size distribution for Pavapor (wooden wool) in the range 10 to 100 µm is in agreement with the pore size of wood which mean value is around 40 µm. It could also be noticed that the low volume fraction of pore with diameter in the range 100 µm -1 mm for super insulator materials could be interpreted by the existence of point defects inside the material or at the contact between the material and the heating resistance on one hand, and between the material and the thermostated blocks on the other hand. Nevertheless, the corresponding volume fraction is quite low in each case.

Conclusion

We showed that it is possible to determine the distribution of the open pores sizes of a low density porous material by a thermal method.

Working under gaseous pressure up to 10 bars makes it possible to detect pore sizes as low as 10 nm, so that the pore size characterization of super-insulators becomes possible.

The main advantages of this method are the followings:

-with regard to the classical methods, such as the mercury porosimetry or the nitrogen sorption, it enables to obtain directly the size of pores and not the size of the opening of pores. -there is no mechanical constraint applied on the sample during the measurement, so that it may be used for fragile materials with very high porosities (up to 99%). -the method is robust, since it is independent from the model. Its main disadvantages are the followings:

-it requires a great number of thermal conductivity measurements (around 20) so that it may take a long time. -it is only suited to materials having a high porosity (greater than 0.8).

Figure 1 :

 1 Figure 1: Thermal conductivity of air vs gas pressure for different pore diameters 0.000

  ), (P in Pa)

Figure 3 :Figure 4 :Figure 5 :

 345 Figure 3: Thermal conductivity (and reduced one * ) of super-insulator, simulated by different models

Figure 6 :

 6 Figure 6: View of the measurement device

  Current intensity passing through the f Surface of the heating element (m Δ+ Temperature difference between the heated surface of the sample and the constant temperature surface (°C)

Figure 7 :

 7 Figure 7: Example of thermal conductivity measurements used for the estimation of pore size

Figure 8 :Figure 9 :

 89 Figure 8: Thermal conductivities (experiment, model and residues) vs gas pressure

Table 1 :

 1 Characteristics of the typical materials considered for the simulations

	Nano-T Super-insulator Pavapor Cellular concrete 10 H 10 I 10 J 10 J 10 I 10 K 10 ) 10 I , . 0.123 0.1 0.104 0.35 , 0.03 0.45 0.566 0.5 0.844 0.45 0.33 0.15 , . 0.2 0.33 0.26 0.4 L 0.964 0.958 0.896 0.99989 M 0.599 0.4 0.544 0.96388

Appendix

Expressions of the thermal conductivity 01! given by different models for a porous media with global porosity ratio , 1 -, . , composed of a solid phase characterized by its thermal conductivity . and its volume fraction , . , and / fluid phases (air). Each fluid phase correspond to a class of pore diameter with thermal conductivity , and volume fraction , , .

Parallel model (2):

Serial model (3):

Combined serial/parallel model (CSP), (8):

With: zW = up q q v{p r r p q p r 9 | up q v p q (A4)

And: z = u p q q v {p r r p q p r 9 | u p q v p q (A5)

Maxwell (1):

p q p r }~r 9~q•~r p q p r }~9 9~q•~9 p q p r }~q 9~q•~r p q p r }~q 9~q•~9 (A6) Self-consistent (7):

Bruggemann( 4), ( 5) and ( 6):

01! J = . , .


Luigi Liquori
email: luigi.liquori@inria.fr

Claude Stolze
email: claude.stolze]@inria.fr

THE ∆-CALCULUS: SYNTAX AND TYPES

Keywords: 1998 ACM Subject Classification: F.3.2 Semantics of Programming Languages, F.4.1 Mathematical logic ad hoc polymorphism, Logic and λ-calculus, intersection types, subtyping

published or not. The documents may come

Introduction

Intersection type theories T were first introduced as a form of ad hoc polymorphism in (pure) λ-calculi à la Curry. The paper by Barendregt,Coppo,and Dezani [BCDC83] is a classic reference, while [START_REF] Henk | Lambda calculus with types[END_REF] is a definitive reference. Intersection type assignment systems λ T ∩ have been well-known in the literature for almost 40 years for many reasons: among them, characterization of strongly normalizing λ-terms [START_REF] Henk | Lambda calculus with types[END_REF], λ-models [START_REF] Alessi | Intersection types and lambda models[END_REF], automatic type inference [START_REF] Assaf | Principality and type inference for intersection types using expansion variables[END_REF], type inhabitation [Urz99, RU12], type unification [START_REF] Dudenhefner | The algebraic intersection type unification problem[END_REF]. As intersection had its classical development for type assignment systems, many papers tried to find an explicitly typed λ-calculus à la Church corresponding to the original intersection type assignment systems à la Curry. The programming language Forsythe, by Reynolds [START_REF] Reynolds | Preliminary design of the programming language Forsythe[END_REF], is probably the first reference, while Pierce's Ph.D. thesis [START_REF] Pierce | Programming with intersection types, union types, and bounded polymorphism[END_REF] combines also unions, intersections and bounded polymorphism. In [START_REF] Wells | A calculus with polymorphic and polyvariant flow types[END_REF] intersection types were used as a foundation for typed intermediate languages for optimizing compilers for higher-order polymorphic programming languages; implementations of typed programming language featuring intersection (and union) types can be found in SML-CIDRE [START_REF] Davies | Practical Refinement-Type Checking[END_REF] and in StardustML [START_REF] Dunfield | Refined typechecking with stardust[END_REF][START_REF] Dunfield | Elaborating intersection and union types[END_REF]. Annotating pure λ-terms with intersection types is not simple: a classical example is the difficulty to decorate the bound variable of the explicitly typed polymorphic identity λx:?.x such that the type of the identity is (σ → σ) ∩ (τ → τ ): previous attempts showed that the full power of the intersection type discipline can be easily lost.

In this paper, we define and prove the main properties of the ∆-calculus, a generic intersection typed system for an explicitly typed λ-calculus à la Church enriched with strong pairs, denoted by ∆ 1 , ∆ 2 , projections, denoted by pr i ∆, and type coercions, denoted by ∆ σ . A strong pair ∆ 1 , ∆ 2 is a special kind of cartesian product such that the two parts of a pair satisfies a given property R on their "essence", that is ∆ 1 R ∆ 2 . An essence ∆ of a ∆-term is a pure λ-term obtained by erasing type decorations, projections and choosing one of the two elements inside a strong pair. As examples, λx:σ ∩ τ.pr 2 x , λx:σ ∩ τ.pr 1 x = λx.x λx:(σ → τ ) ∩ σ.(pr 1 x)(pr 2 x) = λx.x x λx:σ ∩ (τ ∩ ρ). pr 1 x , pr 2 pr 1 x , pr 2 pr 2 x = λx.x and so on. Therefore, the essence of a ∆-term is its untyped skeleton: a strong pair ∆ 1 , ∆ 2 can be typechecked if and only if ∆ 1 R ∆ 2 is verified, otherwise the strong pair will be ill-typed. The essence also gives the exact mapping between a term and its typing à la Church and its corresponding term and type assignment à la Curry. Changing the parameters T and R results in defining a totally different intersection typed system. For the purpose of this paper, we study the four well-known intersection type theories T , namely Coppo-Dezani T CD [START_REF] Coppo | An extension of the basic functionality theory for the λ-calculus[END_REF], Coppo-Dezani-Sallé T CDS [START_REF] Coppo | Functional characterization of some semantic equalities inside λ-calculus[END_REF], Coppo-Dezani-Venneri T CDV [START_REF] Coppo | Functional characters of solvable terms[END_REF] and Barendregt-Coppo-Dezani T BCD [START_REF] Barendregt | A filter lambda model and the completeness of type assignment[END_REF]. We will inspect the above type theories using three equivalence relations R on pure λ-terms, namely ≡, = β and = βη . The combination of the above T and R allows to define ten meaningful typed systems for the ∆-calculus that can be pictorially displayed in a "∆-chair" (see Definition 2.9). Following the same style as in the Barendrengt et al. book [START_REF] Henk | Lambda calculus with types[END_REF], the edges in the chair represent an inclusion relation over the set of derivable judgments. A type coercion ∆ τ is a term of type τ whose type-decoration denotes an application of a subsumption rule to the term ∆ of type σ such that σ T τ : if we omit type coercions, then we lose the uniqueness of type property.

Section 3 shows a number of typable examples in the systems presented in the ∆-chair: each example is provided with a corresponding type assignment derivation of its essence.

Some historical examples of Pottinger [START_REF] Pottinger | A type assignment for the strongly normalizable λ-terms[END_REF], Hindley [START_REF] Hindley | The simple semantics for Coppo-Dezani-Sallé types[END_REF] and Ben-Yelles [START_REF] Ben-Yelles | Type assignment in the lambda-calculus: syntax and semantics[END_REF] are essentially re-decorated and inhabited (when possible) in the ∆-calculus. The aims of this section is both to make the reader comfortable with the different intersection typed systems, and to give a first intuition of the correspondence between Church-style and Curry-style calculi.

Section 4 proves the metatheory for all the systems in the ∆-chair: Church-Rosser, unicity of type, subject reduction, strong normalization, decidability of type checking and type reconstruction.

Section 5 studies the relations between intersection type assignment systems à la Curry and the corresponding intersection typed systems à la Church. Notions of soundness, completeness and isomorphism will relate type assignment and typed systems. We also show how to get rid of type coercions ∆ τ defining a translation function, denoted by , inspired by the one of Tannen et al. [START_REF] Tannen | Inheritance as implicit coercion[END_REF]: the intuition of the translation is that if ∆ has type σ and σ T τ , then σ T τ is a ∆-term of type σ → τ , ( σ T τ ∆ ) has type τ and σ T τ is the identity λx.x.

→ σ → σ) ∩ (τ → τ → τ ).
Pierce [START_REF] Pierce | Programming with intersection types, union types, and polymorphism[END_REF] improves Forsythe by using a for construct to build ad hoc polymorphic typing, as in for α ∈ {σ, τ }.λx:α, λy:α.x. However, we cannot type a typed term, whose type erasure is λx.λy.λz.(x y , x z), with the type

((σ → ρ) ∩ (τ → ρ ) → σ → τ → ρ × ρ ) ∩ ((σ → σ) ∩ (σ → σ) → σ → σ → σ × σ).
Freeman and Pfenning [START_REF] Freeman | Refinement types for ML[END_REF] introduced refinement types, that is types that allow ad hoc polymorphism for ML constructors. Intuitively, refinement types can be seen as subtypes of a standard type: the user first defines a type and then the refinement types of this type. The main motivation for these refinement types is to allow non-exhaustive pattern matching, which becomes exhaustive for a given refinement of the type of the argument. As an example, we can define a type boolexp for boolean expressions, with constructors True, And, Not and Var, and a refinement type ground for boolean expressions without variables, with the same constructors except Var: then, the constructor True has type boolexp∩ground, the constructor And has type (boolexp * boolexp → boolexp) ∩ (ground * ground → ground) and so on. However, intersection is meaningful only when using constructors.

Wells et al. [START_REF] Wells | A calculus with polymorphic and polyvariant flow types[END_REF] introduced λ CIL , a typed intermediate λ-calculus for optimizing compilers for higher-order programming languages. The calculus features intersection, union and flow types, the latter being useful to optimize data representation. λ CIL can faithfully encode an intersection type assignment derivation by introducing the concept of virtual tuple, i.e. a special kind of pair whose type erasure leads to exactly the same untyped λterm. A parallel context and parallel substitution, similar to the notion of [START_REF] Liquori | Towards an intersection typed system à la Church[END_REF][START_REF] Liquori | Intersection typed system à la Church[END_REF], is defined to reduce expressions in parallel inside a virtual tuple. Subtyping is defined only on flow types and not on intersection types: this system can encode the λ CD ∩ type assignment system. [START_REF] Wells | Branching types[END_REF] introduced λ B , a more compact typed calculus encoding of λ CIL : in fact, by comparing Fig. 1 and Fig. 2 of [START_REF] Wells | Branching types[END_REF] we can see that the set of typable terms with intersection types of λ CIL and λ B are the same. In that paper, virtual tuples are removed by introducing branching terms, typable with branching types, the latter representing intersection type schemes. Two operations on types and terms are defined, namely expand, expanding the branching shape of type annotations when a term is substituted into a new context, and select, to choose the correct branch in terms and types. As there are no virtual tuples, reductions do not need to be done in parallel. As in [START_REF] Wells | A calculus with polymorphic and polyvariant flow types[END_REF], the λ CD ∩ type assignment system can be encoded.

Wells and Haak

Frisch et al. [START_REF] Frisch | Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types[END_REF] designed a typed system with intersection, union, negation and recursive types whose semantics are loosely the corresponding set-theoretical constructs. The authors inherit the usual problem of having a domain space D that contains all the terms and, at the same time, all the functions from D to D. They prevent this by forbidding nested arrows, and by having an auxiliary domain space which is the disjoint union of D 2 and P(D 2 ). The subtyping relation is a relation on the set-theoretical interpretation of the types. For instance, the problem σ ∩ τ σ will be interpreted as σ ∩ τ ⊆ σ , where ∩ becomes the set intersection operator, and the decision program actually decides whether ( σ ∩ τ ) ∩ σ is the empty set.

Bono et al. [START_REF] Bono | A typed lambda calculus with intersection types[END_REF] introduced a relevant and strict parallel term constructor to build inhabitants of intersections and a simple call-by-value parallel reduction strategy. An infinite number of constants c σ⇒τ is applied to typed variables x σ such that c σ⇒τ x σ is upcasted to type τ . It also uses an unusual local renaming typing rule, which changes type decoration in λ-abstractions, as well as coercions. Term synchronicity in the tuples is guaranteed by the typing rules. The calculus uses van Bakel's strict version [START_REF] Van Bakel | Cut-elimination in the strict intersection type assignment system is strongly normalizing[END_REF] of the T CD intersection type theory. 1.2. Logics for intersection types. Proof-functional (or strong) logical connectives, introduced by Pottinger [Pot80], take into account the shape of logical proofs, thus allowing for polymorphic features of proofs to be made explicit in formulae. This differs from classical or intuitionistic connectives where the meaning of a compound formula is only dependent on the truth value or the provability of its subformulae. Pottinger was the first to consider the intersection ∩ as a proof-functional connective. He contrasted it to the intuitionistic connective ∧ as follows: "The intuitive meaning of ∩ can be explained by saying that to assert A ∩ B is to assert that one has a reason for asserting A which is also a reason for asserting B, while to assert A ∧ B is to assert that one has a pair of reasons, the first of which is a reason for asserting A and the second of which is a reason for asserting B". A simple example of a logical theorem involving intuitionistic conjunction which does not hold for proof-functional conjunction is (A ⊃ A) ∧ (A ⊃ B ⊃ A). Otherwise there would exist a term which behaves both as I and as K. Later, Lopez-Escobar [START_REF] Edgar | Proof functional connectives[END_REF] and Mints [START_REF] Mints | The completeness of provable realizability[END_REF] investigated extensively logics featuring both proof-functional and intuitionistic connectives especially in the context of realizability interpretations. It is not immediate to extend the judgments-as-types Curry-Howard paradigm to logics supporting proof-functional connectives. These connectives need to compare the shapes of derivations and do not just take into account their provability, i.e. the inhabitation of the corresponding type. There are many proposals to find a suitable logics to fit intersection types; among them we cite [Ven94, RR01, Miq01, CLV01, BVB08, PRR12], and previous papers by the authors [START_REF] Daniel | A realizability interpretation for intersection and union types[END_REF][START_REF] Liquori | A decidable subtyping logic for intersection and union types[END_REF][START_REF] Stolze | Towards a Logical Framework with Intersection and Union Types[END_REF]. All logical aspects of the ∆-calculus will be treated in a companion paper [START_REF] Liquori | The ∆-calculus: logics[END_REF]. 1.3. Raising the ∆-calculus to a ∆-framework. In the future, we plan to extend the generic typed system for the ∆-calculus with union types, relevant arrow types and dependent types: some preliminary results can be found in [DdLS16, LS17, SLHS17] by the authors. In a nutshell:

Minimal type theory min

(refl) σ σ (incl) σ ∩ τ σ, σ ∩ τ τ (glb) ρ σ, ρ τ ⇒ ρ σ ∩ τ (trans) σ τ, τ ρ ⇒ σ ρ Axiom schemes (U top ) σ U (U → ) U σ → U (→∩) (σ → τ ) ∩ (σ → ρ) σ → (τ ∩ ρ) Rule scheme (→) σ 2 σ 1 , τ 1 τ 2 ⇒ σ 1 → τ 1 σ 2 → τ 2
Strong disjunction is a proof-functional connective that can be interpreted as the union type ∪ [DdLS16, SLHS17]: it contrasts with the intuitionistic connective ∨. As Pottinger did for intersection, we could say that asserting (A ∪ B) ⊃ C is to assert that one has a reason for (A ∪ B) ⊃ C, which is also a reason to assert A ⊃ C and B ⊃ C. A simple example of a logical theorem involving intuitionistic disjunction which does not hold for strong disjunction is ((

A ⊃ B) ∪ B) ⊃ A ⊃ B.
Otherwise there would exist a term which behaves both as I and as K.

Strong (relevant) implication is yet another proof-functional connective that was interpreted in [START_REF] Barbanera | Proof-functional connectives and realizability[END_REF] as a relevant arrow type → r . As explained in [START_REF] Barbanera | Proof-functional connectives and realizability[END_REF], it can be viewed as a special case of implication whose related function space is the simplest one, namely the one containing only the identity function. Because the operators ⊃ and → r differ, A → r B → r A is not derivable. Dependent types, as introduced in the Edinburgh Logical Framework [HHP93] by Harper et al., allows considering proofs as first-class citizens albeit differently with respect to proof-functional logics. The interaction of both dependent and proof-functional operators is intriguing: the former mentions proofs explicitly, while the latter mentions proofs implicitly. Their combination therefore opens up new possibilities of formal reasoning on proof-theoretic semantics.

Syntax, Reduction and Types

Definition 2.1 (Type atoms, type syntax, type theories and type assignment systems).

We briefly review some basic definition from Subsection 13.1 of [START_REF] Henk | Lambda calculus with types[END_REF], in order to define type assignment systems. The set of atoms, intersection types, intersection type theories and intersection type assignment systems are defined as follows:

(1) (Atoms). Let A denote a set of symbols which we will call type atoms, and let U be a special type atom denoting the universal type. In particular, we will use

A ∞ = {a i | i ∈ N} with a i being different from U and A U ∞ = A ∞ ∪ {U}. x:σ ∈ B B T ∩ x : σ (ax) B, x:σ T ∩ M : τ B T ∩ λx.M : σ → τ (→I) B T ∩ M : σ B T ∩ M : τ B T ∩ M : σ ∩ τ (∩I) B T ∩ M : σ → τ B T ∩ N : σ B T ∩ M N : τ (→E) B T ∩ M : σ ∩ τ B T ∩ M : σ (∩E 1 ) B T ∩ M : σ ∩ τ B T ∩ M : τ (∩E 2 ) U ∈ A B T ∩ M : U (top) B T ∩ M : σ σ T τ B T ∩ M : τ ( T )
Figure 2: Generic intersection type assignment system λ T ∩ (see Figure 13.8 of [START_REF] Henk | Lambda calculus with types[END_REF]) (2) (Syntax). The syntax of intersection types, parametrized by A, is:

λ T ∩ T A min plus ref. λ CD ∩ T CD A ∞ - [CDC80] λ CDS ∩ T CDS A U ∞ (U top ) [CDCS79] λ CDV ∩ T CDV A ∞ (→), (→∩) [CDCV81] λ BCD ∩ T BCD A U ∞ (→), (→∩), (U top ), (U→) [BCDC83]
σ ::= A | σ → σ | σ ∩ σ
(3) (Intersection type theories T ). An intersection type theory T is a set of sentences of the form σ τ satisfying at least the axioms and rules of the minimal type theory min defined in Figure 1. The type theories T CD , T CDV , T CDS , and T BCD are the smallest type theories over A satisfying the axioms and rules given in Figure 3. We write T 1 T 2 if, for all σ, τ such that σ T 1 τ , we have that σ T 2 τ . In particular T CD T CDV T BCD and T CD T CDS T BCD . We will sometime note, for instance, BCD instead of T BCD . (4) (Intersection type assignment systems λ T ∩ ). We define in Figure 2 § an infinite collection of type assignment systems parametrized by a set of atoms A and a type theory T . We name four particular type assignment systems in the table below, which is an excerpt from Figure 13.4 of [START_REF] Henk | Lambda calculus with types[END_REF]. B T ∩ M : σ denotes a derivable type assignment judgment in the type assignment system λ T ∩ . Type checking is not decidable for λ CD ∩ , λ CDV ∩ , λ CDS ∩ , and λ BCD ∩ .

2.1. The ∆-calculi. Intersection type assignment systems and ∆-calculi have in common their type syntax and intersection type theories. The generic syntax of the ∆-calculus is defined as follows. § Although rules (∩Ei) are derivable with min, we add them for clarity.

Definition 2.2 (Generic ∆-calculus syntax).

∆ ::= u ∆ | x | λx:σ.∆ | ∆ ∆ | ∆ , ∆ | pr i ∆ | ∆ σ i ∈ {1, 2}
u ∆ denotes an infinite set of constants, indexed with a particular untyped ∆-term. ∆ σ denotes an explicit coercion of ∆ to type σ. The expression ∆ , ∆ denotes a pair that, following the Lopez-Escobar jargon [START_REF] Edgar | Proof functional connectives[END_REF], we call "strong pair" with respective projections pr 1 and pr 2 . The essence function is an erasing function mapping typed ∆-terms into pure λ-terms. It is defined as follows.

Definition 2.3 (Essence function).

x def = x ∆ σ def = ∆ λx:σ.∆ def = λx. ∆ ∆ 1 ∆ 2 def = ∆ 1 ∆ 2 ∆ 1 , ∆ 2 def = ∆ 1 pr i ∆ def = ∆ i ∈ {1, 2} u ∆ def = ∆
One could argue that the choice of ∆ 1 , ∆ 2 def = ∆ 1 is arbitrary and could have been

replaced with ∆ 1 , ∆ 2 def = ∆ 2 .
However, the typing rules will ensure that, if ∆ 1 , ∆ 2 is typable, then, for some suitable equivalence relation R, we have that ∆ 1 R ∆ 2 . Thus, strong pairs can be viewed as constrained cartesian products. The generic reduction semantics reduces terms of the ∆-calculus as follows.

Definition 2.4 (Generic reduction semantics). Syntactical equality is denoted by ≡.

(1) (Substitution) Substitution on ∆-terms is defined as usual, with the additional rules:

u ∆ 1 [∆ 2 /x] def = u (∆ 1 [∆ 2 /x]) ∆ σ 1 [∆ 2 /x] def = (∆ 1 [∆ 2 /x]) σ
(2) (One-step reduction). We define three notions of reduction:

(λx:σ.∆ 1 ) ∆ 2 -→ ∆ 1 [∆ 2 /x] (β) pr i ∆ 1 , ∆ 2 -→ ∆ i i ∈ {1, 2} (pr i ) λx:σ.∆ x -→ ∆ x ∈ FV(∆) (η)
Observe that (λx:σ.∆ 1 ) σ ∆ 2 is not a redex, because the λ-abstraction is coerced. The contextual closure is defined as usual except for reductions inside the index of u ∆ that are forbidden (even though substitutions are propagated). We write -→ βpr i for the contextual closure of the (β) and (pr i ) notions of reduction, -→ η for the contextual closure of (η). We also define a synchronous contextual closure, which is like the usual contextual closure except for the strong pairs, as defined in point (3). Synchronous contextual closure of the notions of reduction generates the reduction relations -→ βpr i and -→ η .

U ∈ A B T R u ∆ : U (top) x:σ ∈ B B T R x : σ (ax) B, x:σ T R ∆ : τ B T R λx:σ.∆ : σ → τ (→I) B T R ∆ 1 : σ B T R ∆ 2 : τ ∆ 1 R ∆ 2 B T R ∆ 1 , ∆ 2 : σ ∩ τ (∩I) B T R ∆ 1 : σ → τ B T R ∆ 2 : σ B T R ∆ 1 ∆ 2 : τ (→E) B T R ∆ : σ ∩ τ B T R pr 1 ∆ : σ (∩E 1 ) B T R ∆ : σ ∩ τ B T R pr 2 ∆ : τ (∩E 2 ) B T R ∆ : σ σ T τ B T R ∆ τ : τ ( T )
Figure 4: Generic intersection typed system ∆ T R

(3) (Synchronous closure of -→ ). Synchronous closure is defined on the strong pairs with the following constraint:

∆ 1 -→ ∆ 1 ∆ 2 -→ ∆ 2 ∆ 1 ≡ ∆ 2 ∆ 1 , ∆ 2 -→ ∆ 1 , ∆ 2 (Clos )
Note that we reduce in the two components of the strong pair; (4) (Multistep reduction). We write -→ -→ βpr i (resp. -→ -→ βpr i ) as the reflexive and transitive closure of -→ βpr i (resp. -→ βpr i );

(5) (Congruence). We write = βpr i as the symmetric, reflexive, transitive closure of -→ -→ βpr i . We mostly consider βpr i -reductions, thus to ease the notation we omit the subscript in βpr i -reductions.

The next definition introduces a notion of synchronization inside strong pairs.

Definition 2.5 (Synchronization).

A ∆-term is synchronous if and only if, for all its subterms of the shape ∆ 1 , ∆ 2 , we have that ∆ 1 ≡ ∆ 2 .

It is easy to verify that -→ preserves synchronization, while it is not the case for -→. The next definition introduces a generic intersection typed system for the ∆-calculus that is parametrizable by suitable equivalence relations on pure λ-terms R and type theories T as follows.

Definition 2.6 (Generic intersection typed system). The generic intersection typed system is defined in Figure 4. We denote by ∆ T R a particular typed system with the type theory T and under an equivalence relation R and by B T R ∆ : σ a corresponding typing judgment.

The typing rules are mostly intuitive for a calculus à la Church except rules (∩I), (top) and ( T ). The typing rule for a strong pair (∩I) is similar to the typing rule for a cartesian product, except for the side-condition ∆ 1 R ∆ 2 , forcing the two parts of the strong pair to have essences compatible under R, thus making a strong pair a special case of a cartesian pair. For instance, λx:σ.λy:τ.x , λx:σ.x is not typable in ∆ T ≡ ; (λx:σ.x) y , y is not typable in ∆ T ≡ but it is in ∆ T = β ; x , λy:σ.((λz:τ.z) x) y is not typable in ∆ T ≡ nor ∆ T = β but it is in ∆ T = βη . In the typing rule (top), the subscript ∆ in u ∆ is not necessarily typable so u ∆ can easily be any arbitrary λ-term.

The typing rule ( T ) allows to change the type of a ∆-term from σ to τ if σ T τ : the term in the conclusion must record this change with an explicit type coercion τ , producing the new term ∆ τ : explicit type coercions are important to keep the unicity of typing derivations. The next definition introduces a partial order over equivalence relations on pure λ-terms and an inclusion over typed systems as follows.

Definition 2.7 (R and ).

(

1) Let R ∈ {≡, = β , = βη }. R 1 R 2 if, for all pure λ-terms M, N such that M R 1 N , we have that M R 2 N ; (2) if B T 1 R 1 ∆ : σ and ∆ T 1 R 1 ∆ T 2 R 2 , then B T 2 R 2 ∆ : σ. Fact 2.8. (1) ∆ CD R ∆ CDS R ∆ BCD R and ∆ CD R ∆ CDV R ∆ BCD R ; (2) ∆ T 1 R 1 ∆ T 2 R 2 if T 1 T 2 and R 1 R 2 .
2.2. The ∆-chair. The next definition classifies ten typed systems for the ∆-calculus: some of them already appeared (sometime with a different notation) in the literature by the present authors. Definition 2.9 (∆-chair). Ten typed systems ∆ T R can be drawn pictorially in a ∆-chair, where the arrows represent an inclusion relation. [START_REF] Liquori | Towards an intersection typed system à la Church[END_REF][START_REF] Liquori | Intersection typed system à la Church[END_REF] (in the expression M @∆, M is the essence of ∆) and in its intersection part to [START_REF] Stolze | Towards a Logical Framework with Intersection and Union Types[END_REF]; ∆ CDS ≡ corresponds roughly in its intersection part to [START_REF] Daniel | Logic and computation in a lambda calculus with intersection and union types[END_REF], ∆ BCD ≡ corresponds in its intersection part to [START_REF] Liquori | A decidable subtyping logic for intersection and union types[END_REF], ∆ CD = βη corresponds in its intersection part to [START_REF] Daniel | A realizability interpretation for intersection and union types[END_REF]. The other typed systems are basically new. The main properties of these systems are:

∆ CD ≡ ∆ CD = β ∆ CDV ≡ ∆ CDV = β ∆ CDS ≡ ∆ CDS = β ∆ BCD ≡ ∆ BCD = β ∆ CDV = βη ∆ BCD = βη ∆ CD ≡ corresponds roughly to
(1) All the ∆ T ≡ systems enjoys the synchronous subject reduction property, the other systems also enjoy ordinary subject reduction (Theorem 4.12);

(2) All the systems strongly normalize (Theorem 4.17);

(3) Type checking and type reconstruction are decidable for all the systems, except ∆ CDS = β , ∆ BCD = β , and ∆ BCD = βη (Theorem 5.4); (4) All the systems correspond to the to original type assignment systems except ∆ CDV = βη and ∆ BCD = βη (Theorem 5.2).

Examples

This section shows suitable examples of typed derivations ∆ T R and highlights the corresponding pure type assignment judgment in λ T ∩ they correspond to, in the sense that we have a derivation B T R ∆ : σ and another derivation B T ∩ ∆ : σ. The correspondence between intersection typed systems ∆ T R and intersection type assignment λ T ∩ will be clearly defined in Subsection 5.1.

Example 3.1 (Polymorphic identity).

In all of the intersection type assignment systems λ T ∩ we can derive

T ∩ λx.x : (σ → σ) ∩ (τ → τ ) A corresponding ∆-term is: λx:σ.
x , λx:τ.x that can be typed in all of the typed systems of the ∆-chair as follows

x:σ T R x : σ T R λx:σ.x : σ → σ x:τ T R x : τ T R λx:τ.x : τ → τ λx.x R λx.x T R λx:σ.x , λx:τ.x : (σ → σ) ∩ (τ → τ ) Example 3.

(Auto application).

In all of the intersection type assignment systems we can derive

T ∩ λx.x x : ((σ → τ ) ∩ σ) → τ A corresponding ∆-term is: λx:(σ → τ ) ∩ σ.(pr 1 x)(pr 2 x)
that can be typed in all of the typed systems of the ∆-chair as follows As another example, we can also derive

x:(σ → τ ) ∩ σ T R x : (σ → τ ) ∩ σ x:(σ → τ ) ∩ σ T R pr 1 x : σ → τ x:(σ → τ ) ∩ σ T R x : (σ → τ ) ∩ σ x:(σ → τ ) ∩ σ T R pr 2 x : σ x:(σ → τ ) ∩ σ T R (pr 1 x)(pr 2 x) : τ T R λx:(σ → τ ) ∩ σ.(pr 1 x)(pr 2 x) : (σ → τ ) ∩ σ → τ Example 3.3 (Some examples in ∆ CDS R ). In λ CDS
T CDS ∩ λx.x : σ → σ ∩ U A corresponding ∆-term is: λx:σ. x , x U that can be typed in ∆ CDS R as follows x:σ T CDS R x : σ x:σ T CDS R x : σ σ T CDS U x:σ T CDS R x U : U x R x x:σ T CDS R x , x U : σ ∩ U T CDS R λx:σ. x , x U : σ → σ ∩ U Example 3.4 (An example in ∆ CDV R
). In λ CDV ∩ we can prove the commutativity of intersection, i.e.

T CDV ∩ λx.x : σ ∩ τ → τ ∩ σ A corresponding ∆-term is: λx:σ ∩ τ.pr 2 x , λx:σ ∩ τ.pr 1 x (σ∩τ )→(τ ∩σ)
that can be typed in ∆ CDV R as follows

x:σ ∩ τ T CDS R x : σ ∩ τ x:σ ∩ τ T CDS R pr 2 x : τ T CDS R λx:σ ∩ τ.pr 2 x : (σ ∩ τ ) → τ x:σ ∩ τ T CDS R x : σ ∩ τ x:σ ∩ τ T CDS R pr 1 x : σ T CDS R λx:σ ∩ τ.pr 1 x : (σ ∩ τ ) → σ λx.x R λx.x T CDS R λx:σ ∩ τ.pr 2 x , λx:σ ∩ τ.pr 1 x : ((σ ∩ τ ) → τ ) ∩ ((σ ∩ τ ) → σ) * T CDS R λx:σ ∩ τ.pr 2 x , λx:σ ∩ τ.pr 1 x (σ∩τ )→(τ ∩σ) : (σ ∩ τ ) → (τ ∩ σ) where * is ((σ ∩ τ ) → τ ) ∩ ((σ ∩ τ ) → σ) T CDV (σ ∩ τ ) → (τ ∩ σ).
Example 3.5 (Another polymorphic identity in ∆ T = β ). In all the ∆ T = β you can type this ∆-term: λx:σ.x , (λx:τ →τ.x) (λx:τ.x)

The typing derivation is thus:

x:σ T = β x : σ T = β λx:σ.x : σ → σ x:τ → τ T = β x : τ → τ T = β λx:τ →τ.x : (τ → τ ) → (τ → τ )
x:τ T = β x : τ More precisely, we have:

T BCD ∩ Ω : U A corresponding ∆-term whose essence is Ω is: (λx:U.x U→U x) (λx:U.x U→U x) U that can be typed in ∆ BCD R as follows * T BCD R λx:U.x U→U x : U → U * T BCD R λx:U.x U→U x : U → U U → U T BCD U T BCD R (λx:U.x U→U x) U : U T BCD R (λx:U.x U→U x) (λx:U.x U→U x) U : U where * is x:U T BCD R x : U U T BCD U → U x:U T BCD R x U→U : U → U x:U T BCD R x : U x:U T BCD R x U→U x : U In λ BCD ∩ we can type x:U → U T BCD ∩ x : (U → U) ∩ (σ → U) A corresponding ∆-term whose essence is x is:
x , λy:σ.x y U that can be typed in ∆ BCD = βη as follows:

x:U → U T BCD = βη x : U → U x:U → U, y:σ T BCD = βη x : U → U x:U → U, y:σ T BCD = βη y : σ σ U x:U → U, y:σ T BCD = βη y U : U x:U → U, y:σ T BCD = βη x y U : U x:U → U T BCD = βη λy:σ.x y U : σ → U x = βη λy.x y x:U → U T BCD = βη x , λy:σ.x y U : (U → U) ∩ (σ → U)
Note that the = βη condition has an interesting loophole, as it is well-known that λ BCD ∩ does not enjoy = η -conversion property. Theorem 5.1(1) will show that we can construct a ∆-term which does not correspond to any λ BCD ∩ derivation.

Example 3.7 (Pottinger).

The following examples can be typed in all the type theories of the ∆-chair (we also display in square brackets the corresponding pure λ-terms typable in λ T ∩ ). These are encodings from the examples à la Curry given by Pottinger in [START_REF] Pottinger | A type assignment for the strongly normalizable λ-terms[END_REF].

[λx.λy.

x y] T R λx:(σ → τ ) ∩ (σ → ρ).λy:σ. (pr 1 x) y) , (pr 2 x) y : (σ → τ ) ∩ (σ → ρ) → σ → τ ∩ ρ [λx.λy.x y] T R λx:σ → τ ∩ ρ. λy:σ.pr 1 (x y) , λy:σ.pr 2 (x y) : (σ → τ ∩ ρ) → (σ → τ ) ∩ (σ → ρ) [λx.λy.x y] T R λx:σ → ρ.λy:σ ∩ τ.x (pr 1 y) : (σ → ρ) → σ ∩ τ → ρ [λx.λy.x] T R λx:σ ∩ τ.λy:σ.pr 2 x : σ ∩ τ → σ → τ [λx.λy.x y y] T R λx:σ → τ → ρ.λy:σ ∩ τ.x (pr 1 y) (pr 2 y) : (σ → τ → ρ) → σ ∩ τ → ρ [λx.x] T R λx:σ ∩ τ.pr 1 x : σ ∩ τ → σ [λx.x] T R λx:σ. x , x : σ → σ ∩ σ [λx.x] T R λx:σ ∩ (τ ∩ ρ). pr 1 x , pr 1 pr 2 x , pr 2 pr 2 x : σ ∩ (τ ∩ ρ) → (σ ∩ τ ) ∩ ρ
In the same paper, Pottinger lists some types that cannot be inhabited by any intersection type assignment in an empty context, namely:

T ∩ σ → (σ ∩ τ ) T ∩ (σ → τ ) → (σ → ρ) → σ → τ ∩ ρ T ∩ ((σ ∩ τ ) → ρ) → σ → τ → ρ
It is not difficult to verify that the above types cannot be inhabited by any of the type systems of the ∆-chair because of the failure of the essence condition in the strong pair type rule.

Example 3.8 (Intersection is not the conjunction operator). This counter-example is from the corresponding counter-example à la Curry given by Hindley [START_REF] Hindley | Coppo-Dezani types do not correspond to propositional logic[END_REF] and Ben-Yelles [START_REF] Ben-Yelles | Type assignment in the lambda-calculus: syntax and semantics[END_REF]. The intersection type

(σ → σ) ∩ ((σ → τ → ρ) → (σ → τ ) → σ → ρ)
where the left part of the intersection corresponds to the type for the combinator I and the right part for the combinator S cannot be assigned to a pure λ-term. Analogously, the same intersection type cannot be assigned to any ∆-term.

3.1. On synchronization and subject reduction. For the typed systems ∆ T ≡ , strong pairs have an intrinsic notion of synchronization: some redexes need to be reduced in a synchronous fashion unless we want to create meaningless ∆-terms that cannot be typed. Consider the ∆-term (λx:σ.x) y , (λx:σ.x) y . If we use the -→ reduction relation, then the following reduction paths are legal:

(λx:σ.x) y , (λx:σ.x) y β (λx:σ.x) y , y β β y , (λx:σ.x) y β y , y

More precisely, the first and second redexes are rewritten asynchronously, thus they cannot be typed in any typed system ∆ T ≡ , because we fail to check the left and the right part of the strong pair to be the same: the -→ reduction relation prevents this loophole and allows to type all redexes. In summary, -→ can be thought of as the natural reduction relation for the typed systems ∆ T ≡ .

4. Metatheory of ∆ T R 4.1. General properties. Unless specified, all properties applies to the intersection typed systems ∆ T R . The Church-Rosser property is proved using the technique of Takahashi [START_REF] Takahashi | Parallel reductions in λ-calculus[END_REF]. The parallel reduction semantics extends Definition 2.4 and it is inductively defined as follows.

Definition 4.1 (Parallel reduction semantics).

x =⇒ x u ∆ =⇒ u ∆ ∆ σ =⇒ (∆ ) σ if ∆ =⇒ ∆ ∆ 1 ∆ 2 =⇒ ∆ 1 ∆ 2 if ∆ 1 =⇒ ∆ 1 and ∆ 2 =⇒ ∆ 2 λx:σ.∆ =⇒ λx:σ.∆ if ∆ =⇒ ∆ (λx:σ.∆ 1 ) ∆ 2 =⇒ ∆ 1 [∆ 2 /x] if ∆ 1 =⇒ ∆ 1 and ∆ 2 =⇒ ∆ 2 ∆ 1 , ∆ 2 =⇒ ∆ 1 , ∆ 2 if ∆ 1 =⇒ ∆ 1 and ∆ 2 =⇒ ∆ 2 pr i ∆ =⇒ pr i ∆ if ∆ =⇒ ∆ and i ∈ {1, 2} pr i ∆ 1 , ∆ 2 =⇒ ∆ i if ∆ i =⇒ ∆ i and i ∈ {1, 2}
Intuitively, ∆ =⇒ ∆ means that ∆ is obtained from ∆ by simultaneous contraction of some βpr i -redexes possibly overlapping each other. Church-Rosser can be achieved by proving a stronger statement, namely

∆ =⇒ ∆ implies ∆ =⇒ ∆ * (4.1)
where ∆ * is a ∆-term determined by ∆ and independent from ∆ . The statement (4.1) is satisfied by the term ∆ * which is obtained from ∆ by contracting all the redexes existing in ∆ simultaneously.

Strong normalization.

The idea of the strong normalization proof is to embed typable terms of the ∆-calculus into Church-style terms of a target system, which is the simply-typed λ-calculus with pairs, in a structure-preserving way (and forgetting all the essence side-conditions). The translation is sufficiently faithful so as to preserve the number of reductions, and so strong normalization for the ∆-calculus follows from strong normalization for simply-typed λ-calculus with pairs. A similar technique has been used in [START_REF] Harper | A framework for defining logics[END_REF] to prove the strong normalization property of LF and in [START_REF] Bucciarelli | Intersection types and λ-definability[END_REF] to prove the strong normalization property of a subset of λ CD ∩ . The target system has one atomic type called •, a special constant term u • of type • and an infinite number of constants c σ of type σ for any type of the target system. We denote by B × M : σ a typing judgment in the target system. Definition 4.15 (Forgetful mapping).

• On intersection types.

|a i | def = • ∀a i ∈ A |σ ∩ τ | def = |σ| × |τ | |σ → τ | def = |σ| → |τ |
The map can be easily extended to basis B.

• On ∆-terms. |x| B def = x |u ∆ | B def = u • |λx:σ.∆| B def = λx.|∆| B,x:σ |∆ 1 ∆ 2 | B def = |∆ 1 | B |∆ 2 | B | ∆ 1 , ∆ 2 | B def = (|∆ 1 | B , |∆ 2 | B ) |pr i ∆| B def = pr i |∆| B |∆ τ | B def = c |σ|→|τ | |∆| B if B T R ∆ : σ
The following technical lemma states some properties of the forgetful function.

Lemma 4.16.

(1) If B T R ∆ : σ, then |∆| B is defined, and, for all

B ⊇ B, |∆| B ≡ |∆| B ; (2) |∆ 1 [∆ 2 /x]| B ≡ |∆ 1 | B [|∆ 2 | B /x]; (3) If ∆ 1 -→ ∆ 2 , then |∆ 1 | B -→ |∆ 2 | B ; (4) If B T R ∆ : σ then |B| × |∆| B : |σ|. Proof.
(1) by induction on the derivation;

(2) by induction on ∆ 1 . The only interesting part is ∆ 1 ≡ λy:σ.∆ 1 : by induction hypothesis, we have that

|∆ 1 [∆ 2 /x]| B,x:σ ≡ |∆ 1 | B,x:σ [|∆ 2 | B,x:σ /x]. Therefore, we see that |(λy:σ.∆ 1 )[∆ 2 /x]| B ≡ λy:σ.|∆ 1 [∆ 2 /x]| B,x:σ ≡ λy:σ.|∆ 1 | B,x:σ [|∆ 2 | B,x:σ /x],
but, from point (1), we know that |∆ 2 | B,x:σ ≡ |∆ 2 | B , and we conclude;

(3) by induction on the context of the redex;

(4) by induction on the derivation.

Strong normalization follows easily from the above lemmas.

Theorem 4.17 (Strong normalization). If B T R ∆ : σ, then ∆ is strongly normalizing. Proof. Using Lemma 4.16 and the strong normalization of the simply typed λ-calculus with cartesian pairs. 5. Typed systems à la Church vs. type assignment systems à la Curry

Relation between type assignment systems λ T

∩ and typed systems ∆ T R . It is interesting to state some relations between type assignment systems à la Church and typed systems à la Curry. An interesting property is the one of isomorphism, namely the fact that whenever we assign a type σ to a pure λ-term M , the same type can be assigned to a ∆-term such that the essence of ∆ is M . Conversely, for every assignment of σ to a ∆-term, a valid type assignment judgment of the same type for the essence of ∆ can be derived. Soundness, completeness and isomorphism between intersection typed systems for the ∆calculus and the corresponding intersection type assignment systems for the λ-calculus are defined as follows.

(3) (Isomorphism, ∆ T R ∼ λ T ∩ ). ∆ T R λ T ∩ and ∆ T R λ T ∩ .
The following properties and relations between typed and type assignment systems can be verified.

Theorem 5.2 (Soundness, completeness and isomorphism).

The following properties between ∆-calculi and type assignment systems λ T ∩ are verified.

∆ T R ∆ T R λ T ∩ ∆ T R λ T ∩ ∆ CD ≡ √ √ ∆ CDV ≡ √ √ ∆ CDS ≡ √ √ ∆ BCD ≡ √ √ ∆ CD = β √ √ ∆ CDV = β √ √ ∆ CDS = β √ √ ∆ BCD = β √ √ ∆ CDV = βη × √ ∆ BCD = βη × √ Proof.
( ) Soundness for ∆ T ≡ . Let ∆ be such that B T ≡ ∆ : σ. We proceed by induction on the derivation. All cases proceed straightforwardly since all rules of the type and subtype system T ≡ correspond exactly to the rules of the same name in the corresponding type assignment system T ∩ and in the same type theory T . Therefore M ≡ ∆ can be easily be defined and derived with type σ. Soundness for ∆ T = β . We first show the admissibility of the following type assignment rule

B T ∩ M : σ B T ∩ N : τ M = β N B T ∩ M : σ ∩ τ (∩I) adm
in all λ T ∩ as follows: we know these type assignment systems have the subject reduction and the typed-expansion property for β (see Corollary 14.2.3 and Proposition 14.2.4(i) of [START_REF] Henk | Lambda calculus with types[END_REF] The essence of pr 2 λy:U.x U→U y , x is λy.x y, but, if σ is an atomic type (different than U):

x:σ T BCD ∩ λy.x y : σ ( ) Let M be such that B T ∩ M : σ for a given B. We proceed by induction on the derivation. All cases proceed straightforwardly since all rules of the type and subtype assignment system T ∩ correspond exactly to the rules of the same name in the corresponding typed system T R and in the same type theory T . Therefore a ∆-term can be easily be constructed and derived with type σ;

The last theorem characterizes the class of strongly normalizing ∆-terms.

Theorem 5.3 (Characterization).

Every strongly normalizing λ-term can be type-annotated so as to be the essence of a typable ∆-term.

Proof. We know that every strongly normalizing λ-term M is typable in λ T ∩ . By Theorem 5.2 we have that ∆ T R λ T ∩ , therefore there exists some typable ∆, such that M ≡ ∆ . We can finally state decidability of type checking (TC) and type reconstruction (TR).

Theorem 5.4 (Decidability of type checking and type reconstruction).

∆ T R TC/TR ∆ CD ≡ √ ∆ CDV ≡ √ ∆ CDS ≡ √ ∆ BCD ≡ √ ∆ CD = β √ ∆ CDV = β √ ∆ CDS = β × ∆ BCD = β × ∆ CDV = βη √ ∆ BCD = βη × Proof.
Both type checking and type reconstruction can be proved by induction on the structure of ∆, using the decidability of T BCD proved by Hindley [START_REF] Hindley | The simple semantics for Coppo-Dezani-Sallé types[END_REF] (see also [START_REF] Liquori | A decidable subtyping logic for intersection and union types[END_REF]). By Theorem 5.2, the essences of all the ∆-terms, which are typable in ∆ CD = β , ∆ CDV = β , or ∆ CDV = βη , are typable in λ CD ∩ or λ CDV ∩ , therefore they are strongly normalizing. As a consequence, the sidecondition ∆ 1 R ∆ 2 is decidable for ∆ CD = β , ∆ CDV = β , and ∆ CDV = βη and so type reconstruction and type checking are decidable too. Type reconstruction and type checking are not decidable in ∆ CDS = β , ∆ BCD = β , and ∆ BCD = βη , because u ∆ 1 , u ∆ 2 is typable if and only if ∆ 1 = β ∆ 2 (resp. ∆ 1 = βη ∆ 2 ). However, ∆ 1 and ∆ 2 are arbitrary pure λ-terms, and both β-equality and βη-equality are undecidable. 5.2. Subtyping and explicit coercions. The typing rule ( T ) in the general typed system introduces type coercions: once a type coercion is introduced, it cannot be eliminated, so de facto freezing a ∆-term inside an explicit coercion. Tannen et al. [START_REF] Tannen | Inheritance as implicit coercion[END_REF] showed a translation of a judgment derivation from a "Source" system with subtyping (Cardelli's Fun [START_REF] Cardelli | On understanding types, data abstraction, and polymorphism[END_REF]) into an "equivalent" judgment derivation in a "Target" system without subtyping (Girard system F with records and recursion). In the same spirit, we present a translation that removes all explicit coercions. Intuitively, the translation proceeds as follows: every derivation ending with rule

B T R ∆ : σ σ T τ B T R ∆ τ : τ ( T )
is translated into the following (coercion-free) derivation

B T R σ T τ : σ → τ B T R ∆ B : σ B T R σ T τ ∆ B : τ (→E)
where R is a suitable relation such that R R . Note that changing of the type theory is necessary to guarantee well-typedness in the translation of strong pairs. Summarizing, we provide a type preserving translation of a ∆-term into a coercion-free ∆-term such that ∆ = βη ∆ .

The following example illustrates some trivial compilations of axioms and rule schemes of Figure 1.

Example 5.5 (Translation of axioms and rule schemes of Figure 1). (refl) the judgment x:σ T R x , x σ : σ ∩ σ is translated to a coercion-free judgment x:σ T = β x , (λy:σ.y) x : σ ∩ σ (incl) the judgment x:σ ∩τ T R x, x τ : (σ ∩τ )∩τ is translated to a coercion-free judgment x:σ ∩ τ T = β x , (λy:σ ∩ τ.pr 2 y) x : (σ ∩ τ ) ∩ τ (glb) the judgment x:σ T R x , x σ∩σ : σ ∩ (σ ∩ σ) is translated to a coercion-free judgment x:σ T = β x , (λy:σ. y , y (2) The translation -B is defined on ∆ as follows. By looking at the above translation functions we can see that if B T R ∆ : σ, then ∆ B is defined and it is coercion-free. The following lemma states that a coercion function is always typable in ∆ T = βη , that it is essentially the identity and that, without using the rule schemes (→∩), (U → ), and (→) the translation can even be derivable in ∆ T = β . Lemma 5.7 (Essence of a coercion is an identity).

) x : σ ∩ (σ ∩ σ) (U top ) the judgment x:σ T R x , x U : σ ∩ U is translated to a coercion-free judgment x:σ T = β x , (λy:σ.u y ) x : σ ∩ U (U → ) the judgment x:U T R x, x σ→U : U∩(σ → U) is translated to a coercion-free judgment x:U T = βη x , (λf :U.λy:σ.u (f y) ) x : U ∩ (σ → U) (→∩) the judgment x:(σ → τ ) ∩ (σ → ρ) T R x σ→τ ∩ρ : σ → τ ∩ ρ is translated to a coercion-free judgment x:(σ → τ ) ∩ (σ → ρ) T = βη (λf :(σ → τ ) ∩ (σ → ρ).
u ∆ B def = u ∆ B x B def = x λx:σ.∆ B def = λx:σ. ∆ B,x:σ ∆ 1 ∆ 2 B def = ∆ 1 B ∆ 2 B ∆ 1 , ∆ 2 B def = ∆ 1 B , ∆ 2 B pr i ∆ B def = pr i ∆ B i ∈ {1, 2} ∆ τ B def = σ T τ ∆ B if B T R ∆ : σ.
(1) If σ T τ , then T = βη σ T τ : σ → τ and σ T τ = βη λx.x; (2) If σ T τ without using the rule schemes (→∩), (U → ), and (→), then T = β σ T τ : σ → τ and σ T τ = β λx.x.

Proof. The proofs proceed in both parts by induction on the derivation of σ T τ . For instance, in case of (glb), we can verify that T = β λx:ρ. ρ T σ x , ρ T τ x : ρ → σ ∩ τ using the induction hypotheses that ρ T σ (resp. ρ T τ ) has type ρ → σ (resp. ρ → τ ) and has an essence convertible to λx.x.

We can now prove the coherence of the translation as follows.

Figure 1 :

 1 Figure 1: Minimal type theory min , axioms and rule schemes (see Fig. 13.2 and 13.3 of [BDS13])

Figure 3 :

 3 Figure 3: Type theories λ CD ∩ , λ CDS ∩ , λ CDV ∩ , and λ BCD ∩ . The ref. column refers to the original article these theories come from.

∩

  we can derive T CDS ∩ (λx.λy.x) : σ → U → σ and using this type assignment, we can derive z:σ T CDS ∩ (λx.λy.x) z z : σ. A corresponding ∆-term is: (λx:σ.λy:U.x) z z U that can be typed in ∆ CDS R as follows z:σ, x:σ, y:U T CDS R x : σ z:σ, x:σ T CDS R λy:U.x : U → σ z:σ T CDS R λx:σ.λy:U.x : σ → U → σ z:σ T CDS R z : σ z:σ T CDS R (λx:σ.λy:U.x) z : U → σ z:σ T CDS R z : σ σ T CDS U z:σ T CDS R z U : U z:σ T CDS R (λx:σ.λy:U.x) z z U : σ

T=

  β λx:τ.x : τ → τ T = β (λx:τ →τ.x) (λx:τ.x) : τ → τ λx.x = β (λx.x) (λx.x) T = β λx:σ.x , (λx:τ →τ.x) (λx:τ.x) : (σ → σ) ∩ (τ → τ ) Example 3.6 (Two examples in ∆ BCD ≡ and ∆ BCD = βη ). In λ BCD ∩ we can can type any term, including the non-terminating term Ω def = (λx.x x) (λx.x x)

Definition 5. 1

 1 (Soundness, completeness and isomorphism).Let ∆ T R and λ T ∩ . (1) (Soundness, ∆ T R λ T ∩ ). B T R ∆ : σ implies B T ∩ ∆ : σ; (2) (Completeness, ∆ T R λ T ∩). B T ∩ M : σ implies there exists ∆ such that M ≡ ∆ and B T R ∆ : σ;

  , respectively). As a consequence, if B T ∩ M : σ, and B T ∩ N : τ , and M = β N , then B T ∩ M : τ . Then the proof proceeds by induction on the derivation of B T = β ∆ : σ. The most important case is when the last used rule is (∩I): by induction we get B T ∩ ∆ 1 : σ, and B T ∩ ∆ 2 : τ , and ∆ 1 = β ∆ 2 , and, by the essence definition, ∆ 1 , ∆ 2 = β ∆ 1 . Apply rule (∩I) adm and conclude with B T ∩ ∆ 1 : σ ∩ τ . ( ) Loss of soundness in ∆ CDV = βη is proved via the following counterexample, where B def = {x:(σ → τ ) ∩ ρ}. B, y:σ T CDV = βη x : (σ → τ ) ∩ ρ B, y:σ T CDV = βη pr 1 x : σ → τ B, y:σ T CDV = βη y : σ B, y:σ T CDV = βη (pr 1 x) y : τ B T CDV = βη λy:σ.(pr 1 x) y : σ → τ B T CDV = βη x : (σ → τ ) ∩ ρ B T CDV = βη pr 2 x : ρ λy.x y = βη x B T CDV = βη λy:σ.(pr 1 x) y , pr 2 x : (σ → τ ) ∩ ρ B T CDV = βη pr 2 λy:σ.(pr 1 x) y , pr 2 x : ρ The essence of pr 2 λy:σ.(pr 1 x) y , pr 2 x is λy.x y, but, if ρ is an atomic type: x:(σ → τ ) ∩ ρ T CDV ∩ λy.x y : ρ Loss of soundness in ∆ BCD = βη is proved via the following counterexample: x:σ, y:U T BCD = βη x : σ σ T U → U x:σ, y:U T BCD = βη x U→U : U → U x:σ, y:U T BCD = βη y : U x:σ, y:U T BCD = βη x U→U y : U x:σ T BCD = βη λy:U.x U→U y : U → U x:σ T BCD = βη x : σ λy.x y = βη x x:σ T BCD = βη λy:U.x U→U y , x : (U → U) ∩ σ x:σ T BCD = βη pr 2 λy:U.x U→U y , x : σ

=T=T=T=

  λy:σ. (pr 1 f ) y , (pr 2 f ) y ) x : σ → τ ∩ ρ (→) the judgment x:σ → τ ∩ ρ T R x , x σ∩ρ→τ : (σ → τ ∩ ρ) ∩ (σ ∩ ρ → τ ) is translated to a coercion-free judgment x:σ → τ ∩ ρ T = βη x , (λf :σ → τ ∩ ρ.λy:σ ∩ ρ.pr 1 (f (pr 1 y))) x : (σ → τ ∩ ρ) ∩ (σ ∩ ρ → τ ) (trans) the judgment x:σ T R x , (x U ) σ→U : σ ∩ (σ → U) is translated to a coercion-free judgment x:σ T = βη x , (λf :U.λy:σ.u (f y) ) ((λy:σ.u y ) x) : σ ∩ (σ → U)The next definition introduces two maps translating subtype judgments into explicit coercions functions and ∆-terms into coercion-free ∆-terms. Definition 5.6 (Translationsand -B ).(1) The minimal type theory min and the extra axioms and schemes are translated as follows. β λx:σ.x : σ → σ(incl 1 ) σ ∩ τ T σ def = T = β λx:σ ∩ τ.pr 1 x : σ ∩ τ → σ (incl 2 ) σ ∩ τ T τ def = T = β λx:σ ∩ τ.pr 2 x : σ ∩ τ → τ (glb) ρ T σ ρ T τ ρ T σ ∩ τ def = T = β λx:ρ. ρ T σ x , ρ T τ x : ρ → σ ∩ τ (trans) σ T τ τ T ρ σ T ρ def = T = β λx:σ. τ T ρ ( σ T τ x) : σ → ρ (U top ) σ T U def = T = β λx:σ.u x : σ → U (U → ) U T σ → U def = βη λf :U.λx:σ.u (f x) : U → (σ → U) Let ξ 1 def = (σ → τ ) ∩ (σ → ρ) and ξ 2 def = σ → τ ∩ ρ (→∩) ξ 1 T ξ 2 def = βη λf :ξ 1 .λx:σ. (pr 1 f ) x , (pr 2 f ) x : ξ 1 → ξ 2 Let ξ 1 def = σ 1 → τ 1 and ξ 2 def = σ 2 → τ 2 (→) σ 2 T σ 1 τ 1 T τ 2 σ 1 → τ 1 T σ 2 → τ 2 def = βη λf :ξ 1 .λx:σ 2 . τ 1 T τ 2 (f ( σ 2 T σ 1 x)) : ξ 1 → ξ 2

Figure 5 :

 5 Figure 5: On the left: source systems. On the right: target systems without the ( T ) rule.

Theorem 5. 8 (

 8 Coherence). If B T R ∆ : σ, then B T R ∆ B : σ and ∆ B R ∆ , where ∆ T R and ∆ T R are respectively the source and target intersection typed systems given in Figure 5.Proof. By induction on the derivation. We illustrate the most important case, namely when the last type rule is ( T ). In this case ∆ τ B is translated to σ T τ ∆ B . By induction hypothesis we have that B T R ∆ : σ, and by Lemma 5.7 we have thatB T R σ T τ : σ → τ ; therefore B T R ∆ τ B : τ .Moreover, we know that σ T τ R λx.x, and this gives ∆ τ B R ∆ B . Again by induction hypothesis we have that ∆ B R ∆ , and this gives the thesis ∆ τ B R ∆ τ .

  Several calculi à la Church appeared in the literature: they more or less capture the power of intersection types; we briefly review them.

1.1. λ-calculi with intersection types à la Church.

The Forsythe programming language by Reynolds

[START_REF] Reynolds | Preliminary design of the programming language Forsythe[END_REF]

annotates a λ-abstraction with types as in λx:σ 1 |• • •|σ n .M . However, we cannot type a typed term, whose type erasure is the combinator K ≡ λx.λy.x, with the type (σ

Definition 4.2 (The map * ).

The next technical lemma will be useful in showing that Church-Rosser for -→ -→ can be inherited from Church-Rosser for =⇒.

Lemma 4.3.

(1

(1 ) can be proved by induction on the context of the redexes, while (2 ), (3 ), and (4 ) can be proved by induction on the structure of ∆ 1 . Now we have to prove the Church-Rosser property for the parallel reduction.

Lemma 4.4 (Confluence property for =⇒).

Proof. By induction on the shape of ∆.

∆ is not a β-redex, then, for some ∆ 1 and ∆ 2 , we have that

then, for some ∆ 1 and ∆ 2 , we have that ∆ 1 =⇒ ∆ 1 , ∆ 2 =⇒ ∆ 2 and we have 2 subcases:

thanks to point (3) of Lemma 4.3; • if ∆ ≡ pr i ∆ 1 and ∆ 1 is not a strong pair, then, for some ∆ 1 , we have that ∆ 1 =⇒ ∆ 1 and ∆ ≡ pr i ∆ 1 , therefore, by induction hypothesis, ∆ =⇒

and we have 2 subcases:

The Church-Rosser property follows.

Theorem 4.5 (Confluence).

Proof. Thanks to the first two points of Lemma 4.3, we know that -→ -→ is the transitive closure of =⇒, therefore we can deduce the confluence property of -→ -→ with the usual diagram chase, as suggested below.

∆ 0,0

The next lemma says that all type derivations for ∆ have an unique type.

Lemma 4.6 (Unicity of typing).

If B T R ∆ : σ, then σ is unique. Proof. By induction on the shape of ∆.

The next lemma proves inversion properties on typable ∆-terms.

Lemma 4.7 (Generation).

(1

R ∆ τ : ρ, then ρ ≡ τ and there is σ such that σ T τ and B T R ∆ : σ. Proof. The typing rules are uniquely syntax-directed, therefore we can immediately conclude.

The next lemma says that all subterms of a typable ∆-term are typable too. Lemma 4.9 (Free-variable properties).

(1) If B T R ∆ : σ, and B ⊇ B, then

By induction on the derivation of B T R ∆ : σ. The next lemma also says that essence is closed under substitution.

Lemma 4.10 (Substitution).

(1)

(1) by induction on the shape of ∆ 1 ;

(2) by induction on the derivation. As an illustration, we show the case when the last applied rule is (∩I). Then we have that B, x:σ T R ∆ 1 , ∆ 1 : τ ∩τ and B T R ∆ 2 : σ; by induction hypothesis we have

In order to prove subject reduction, we need to prove that reducing ∆-terms preserve the side-condition ∆ 1 R ∆ 2 when typing the strong pair ∆ 1 , ∆ 2 . We prove this in the following lemma.

Lemma 4.11 (Essence reduction).

(1

If ∆ 1 is a redex, then we have three cases:

R , and thanks to Lemma 4.7(4), we have that

For the contextual closure, we have that ∆ 1 ≡ ∆[∆ /x], where ∆[ ] is a surrounding context and ∆ is a redex, and ∆ 2 is ∆[∆ /x] where ∆ is the contractum of ∆ . Then, by Lemma 4.8 we know that ∆ is typable and then we conclude by Lemma 4.10.

The next theorem states that all the ∆ T ≡ typed systems preserve synchronous βpr i -reduction, and all the ∆ T = β and ∆ T = βη typed systems preserve βpr i -reduction. Theorem 4.12 (Subject reduction for βpr i ).

(1

If ∆ 1 is a βpr i -redex, then we proceed as usual using Lemmas 4.7 and 4.10. For the contextual closure, we proceed by induction on the derivation: we illustrate the most important case, namely (∩I) where we have to check that the essence condition is preserved. According to R we distinguish two cases:

(1) (Case where R is ≡).

• by Lemma 4.11 we have that ∆ 1 R ∆ 1 and ∆ 2 R ∆ 2 ;

• by induction hypothesis we have that

The next theorem states that some of the typed systems on the back of the ∆-chair preserve η-reduction.

Theorem 4.13 (Subject reduction for η for T CDV , T BCD ).

then we proceed as usual using Lemmas 4.7 and 4.9. For the contextual closure the proof proceeds exactly as in Theorem 4.12.

Remark 4.14 (About subject expansion). We know that some of the intersection type assignment systems à la Curry (viz. λ BCD ∩ and λ CDS ∩ ) satisfy the subject β-expansion property: one may ask whether this property can also be meaningful in typed systems à la Church. It is not surprising to see that the answer is negative because type-decorations of bound variables are hard-coded in the λ-abstraction and cannot be forgotten. As a trivial example of the failure of the subject-expansion in all the typed systems, consider the following reduction:

(λx:σ.x) (λx:σ.x) -→ (λx:σ.x) Obviously we can type T R (λx:σ.x) : σ → σ but T R (λx:σ.x) (λx:σ.x) : σ → σ.