Koray Kayabol
email: koray.kayabol@inria.fr

Vladimir A Krylov ⋆⋆

Josiane Zerubia
email: josiane.zerubia@inria.fr

Unsupervised Classification of SAR Images using Hierarchical Agglomeration and EM

Keywords: High resolution SAR, TerraSAR-X, classification, texture, multinomial logistic, Classification EM, hierarchical agglomeration

We implement an unsupervised classification algorithm for high resolution Synthetic Aperture Radar (SAR) images. The foundation of algorithm is based on Classification Expectation-Maximization (CEM). To get rid of two drawbacks of EM type algorithms, namely the initialization and the model order selection, we combine the CEM algorithm with the hierarchical agglomeration strategy and a model order selection criterion called Integrated Completed Likelihood (ICL). We exploit amplitude statistics in a Finite Mixture Model (FMM), and a Multinomial Logistic (MnL) latent class label model for a mixture density to obtain spatially smooth class segments. We test our algorithm on TerraSAR-X data.

Introduction

Finite Mixture Model (FMM) is a suitable statistical model to represent SAR image histogram and to perform a model based classification [START_REF] Titterington | Statistical Analysis of Finite Mixture Disributions[END_REF], [START_REF] Oliver | Understanding Synthetic Aperture Radar Images[END_REF]. One of the first uses of FMM in SAR image classification may be found in [START_REF] Masson | SEM Algorithm and Unsupervised Statistical Segmentation of Satellite Images[END_REF]. A combination of several different probability density functions (pdfs) into a FMM has been used in [START_REF] Krylov | Supervised Enhanced Dictionary-Based SAR Amplitude Distribution Estimation and Its Validation With Very High-Resolution Data[END_REF] for high resolution SAR images. The EM algorithm [START_REF] Dempster | Maximum Likelihood from Incomplete Data via the EM Algorithm[END_REF], [START_REF] Redner | Mixture Densities, Maximum Likelihood and the EM Algorithm[END_REF] has been used for parameter estimation in latent variable models such as FMM. Two drawbacks of FMM based classification with EM algorithm can be sorted as 1) determination of the necessary number of class to represent the data and 2) initialization of the classes. By the term unsupervised, we refer to an initialization independent algorithm which is also able to determine the model order as in [START_REF] Palubinskas | An Unsupervised Clustering Method using the Entropy Minimization[END_REF], [START_REF] Figueiredo | Unsupervised Learning of Finite Mixture Models[END_REF]. There are some stochastic methods used in image segmentation like Reversible Jump Markov Chain Monte Carlo in [START_REF] Wilson | Segmentation of Textured Satellite and Aerial Images by Bayesian Inference and Markov Random Fields[END_REF], but their computational complexity is high ⋆ Koray Kayabol carried out this work during the tenure of an ERCIM "Alain Bensoussan" Postdoctoral Fellowship Programme. ⋆⋆ Vladimir A. Krylov carried out this work with the support of INRIA Postdoctoral Fellowship.

and sometimes they may reach an over segmented maps. Using the advantage of categorical random variables [START_REF] Kayabol | SAR Image Classification with Non-stationary Multinomial Logistic Mixture of Amplitude and Texture Densities[END_REF], we prefer to use an EM based algorithm called Classification EM (CEM) [START_REF] Celeux | A Classification EM Algorithm for Clustering and Two Stochastic Versions[END_REF] whose computational cost is lower than both the stochastic methods and the conventional EM algorithm. In classification step, CEM uses the Winner-Take-All principle to allocate each data pixel to the related class according to the posterior probability of latent class label. After the classification step of CEM, we estimate the parameters of the class densities using only the pixels which belong to that class.

Running the EM type algorithms several times for different model orders to determine the order based on a criterion is a simple approach to reach a parsimonious solution. In [START_REF] Fraley | Model-based Clustering, Discriminant Analysis, and Density Estimation[END_REF], a combination of hierarchal agglomeration [START_REF] Ward | Hierarchical groupings to optimize an objective function[END_REF], EM and Bayesian Information Criterion (BIC) [START_REF] Schwarz | Estimating the Dimension of a Model[END_REF] is proposed to find the necessary number of classes in the mixture model. [START_REF] Figueiredo | Unsupervised Learning of Finite Mixture Models[END_REF] performs a similar strategy with Component-wise EM [START_REF] Celeux | A Component-wise EM Algorithm for Mixtures[END_REF] and Minimum Message Length (MML) criterion [START_REF] Wallace | An Information Measure for Classification[END_REF][START_REF] Wallace | Estimation and Inference by Compact Coding[END_REF]. In this study, we combine hierarchal agglomeration, CEM and ICL [START_REF] Biernacki | Assessing a Mixture Model for Clustering with the Integrated Completed Likelihood[END_REF] criterion to obtain an unsupervised classification algorithm.

We use a mixture of Nakagami densities for amplitude modelling. To obtain smooth and segmented class label maps, a post-processing can be applied to roughly classified class labels, but a Bayesian approach allows to include smoothing constraints to classification problems. We assume that each latent class label is a categorical random variable which is a special version of the multinomial random variable where each pixel belongs to only one class [START_REF] Titterington | Statistical Analysis of Finite Mixture Disributions[END_REF]. We introduce a spatial interaction within each binary map adopting multinomial logistic model [START_REF] Krishnapuram | Sparse Multinomial Logistic Regression: Fast Algorithms and Generalization Bounds[END_REF], [START_REF] Kayabol | SAR Image Classification with Non-stationary Multinomial Logistic Mixture of Amplitude and Texture Densities[END_REF] to obtain a smooth segmentation map.

In Section 2 and 3, the MnL mixture model and CEM algorithm are given. We give the details of the agglomeration based unsupervised classification algorithm in Section 4. The simulation results are shown in Section 5. Section 6 presents the conclusion and future work.

Multinomial Logistic Mixture of Amplitude based Densities

We assume that the observed amplitude at the nth pixel, s n ∈ R + , where n ∈ R = {1, 2, . . . , N } represents the lexicographically ordered pixel index, is free from any noise and instrumental degradation. Every pixel in the image has a latent class label. Denoting K the number of classes, we encode the class label as a K dimensional categorical vector z n whose elements z n,k , k ∈ {1, 2, . . . , K} have the following properties: 1) z n,k ∈ {0, 1} and 2)

K k=1 z n,k = 1.
We may write the probability of s n as the marginalization of the joint probability of

p(s n , z n |Θ, π n ) = p(s n |z n , Θ)p(z n |π n ), [1], as p(s n |Θ, π n ) = zn p(s n |z n , Θ)p(z n |π n ) = zn K k=1 [p(s n |θ k )π n,k ] z n,k (1)
where π n,k = p(z n,k = 1) represent the mixture proportions, π n = [π n,1 , . . . , π n,K ], θ k is the parameter of the class density and Θ = {θ 1 , . . . , θ K } is the set of the parameters. If z n is a categorical random vector and the mixture proportions are spatially invariant, (1) is reduced to classical FMM as follow:

p(s n |Θ) = K k=1 p(s n |θ k )π k (2)
We prefer to use the notation in (1) to show the contribution of the multinomial density of class label, p(z n ), into finite mixture model more explicitly. We give the details of the class and the mixture densities in the following two sections.

Class Amplitude Densities

Our aim is to use the amplitude statistics to classify the SAR images. For this purpose, we model the class amplitudes using Nakagami density, which is a basic theoretical multi-look amplitude model for SAR images [START_REF] Oliver | Understanding Synthetic Aperture Radar Images[END_REF]. We express the Nakagami density with parameters µ k and ν k as in [START_REF] Oliver | Understanding Synthetic Aperture Radar Images[END_REF], [START_REF] Kayabol | SAR Image Classification with Non-stationary Multinomial Logistic Mixture of Amplitude and Texture Densities[END_REF] as

p A (s n |µ k , ν k ) = 2 Γ (ν k ) ν k µ k ν k s 2ν k -1 n e -ν k s 2 n µ k . ( 3
)
We denote θ k = {µ k , ν k }.

Mixture Density -Class Prior

The prior density p(z n,k |π n,k ) of the categorical random variable is naturally an iid multinomial density, but we are not able to obtain a smooth class label map if we use an iid multinomial. We need to use a density which models the spatial smoothness of the class labels as well. We use a contrast function which emphasizes the high probabilities while attenuating the low ones, namely Logistic function [START_REF] Krishnapuram | Sparse Multinomial Logistic Regression: Fast Algorithms and Generalization Bounds[END_REF]. The logistic function allows us to make an easier decision by discriminating the probabilities closed to each other. In this model, We are also able to introduce spatial interactions of the categorical random field by defining a binary spatial auto-regression model. Our MnL density for the problem at hand is written as

p(z n |Z ∂n , η) = K k=1 exp(ηv k (z n,k )) K j=1 exp(ηv j (z n,j )) z n,k (4)
where

v k (z n,k ) = 1 + m∈M(n) z m,k . (5)
and

Z ∂n = {z m : m ∈ M(n), m = n}

Classification EM Algorithm

Since our purpose is to cluster the observed image pixels by maximizing the marginal likelihood given in (1), we suggest to use EM type algorithm to deal with the summation. The EM log-likelihood function is written as

Q EM (Θ|Θ t-1 ) = N n=1 K k=1 z n,k log{p(s n |θ k )π n,k }p(z n,k |s n , Z ∂n , Θ t-1 ) (6)
where we include the parameter η to parameter set Θ = {θ 1 , . . . , θ K , η}.

If we used the exact EM algorithm to find the maximum of Q(Θ|Θ t-1 ) with respect to Θ, we would need to maximize the parameters for each class given the expected value of the class labels. Instead of this, we use the advantage of working with categorical random variables and resort to Classification EM algorithm [START_REF] Celeux | A Classification EM Algorithm for Clustering and Two Stochastic Versions[END_REF]. After classification step, we can partition the pixel domain R into K non-overlapped regions such that R = K k=1 R k and R k R l = 0, k = l and consequently, we may write the classification log-likelihood function as

Q CEM (Θ|Θ t-1 ) = K k=1 m∈R k log{p(s m |θ k )π m,k }p(z m,k |s m , Z ∂m , Θ t-1 ) (7)
The CEM algorithm incorporates a classification step between the E-step and the M-step which performs a simple Maximum-a-Posteriori (MAP) estimation to find the highest probability class label. Since the posterior of the class label p(z n,k |s n , Z ∂n , Θ t-1 ) is a discrete probability density function of a finite number of classes, we can perform the MAP estimation by choosing the maximum class probability. We summarize the CEM algorithm for our problem as follows:

E-step: For k = 1, . . . , K and n = 1, . . . , N , calculate the posterior probabilities

p(z n,k |s n , Z ∂n , Θ t-1 ) = p(s n |θ t-1 k ) exp(η t-1 v k (z n,k )) K j=1 exp(η t-1 v j (z n,j )) (8)
given the previously estimated parameter set Θ t-1 . C-step: For n = 1, . . . , N , classify the nth pixel into class j as z n,j = 1 by choosing j which maximizes the posterior p(z n,k |s n , Z ∂n , Θ t-1 ) over k = 1, . . . , K as j = arg max

k p(z n,k |s n , Z ∂n , Θ t-1 ) (9)
M-step: To find a Bayesian estimate, maximize the classification log-likelihood in [START_REF] Palubinskas | An Unsupervised Clustering Method using the Entropy Minimization[END_REF] with respect to Θ as

Θ t-1 = arg max Θ Q CEM (Θ|Θ t-1 ) (10)
To maximize this function, we alternate among the variables µ k , ν k and η. We use the following methods to update the parameters: analytical solution of the first derivative for µ k , zero finding of the first derivative for ν k and Newton-Raphson update equation for η.

Unsupervised Classification Algorithm

In this section, we present the details of the unsupervised classification algorithm. Our strategy follows the same general philosophy as the one proposed in [START_REF] Ward | Hierarchical groupings to optimize an objective function[END_REF] and developed for mixture model in [START_REF] Figueiredo | Unsupervised Learning of Finite Mixture Models[END_REF][START_REF] Fraley | Model-based Clustering, Discriminant Analysis, and Density Estimation[END_REF]. We start the CEM algorithm with a large number of classes, K = K max , and then we reduce the number of classes to K ← K -1 by merging the weakest class in probability to the one that is most similar to it with respect to a distance measure. The weakest class may be found using the average probabilities of each class as

k weak = arg min k 1 N k n∈R k p(z n,k |s n , Z ∂n , Θ t-1 ) (11)
Kullback-Leibler (KL) type divergence criterions are used in hierarchical texture segmentation for region merging [START_REF] Scarpa | Hierarchical Multiple Markov Chain Model for Unsupervised Texture Segmentation[END_REF]. We use a symmetric KL type distance measure called Jensen-Shannon divergence [START_REF] Lin | Divergence Measures Based on the Shannon Entropy[END_REF] which is defined between two probability density functions, i.e. p k weak and p k , k = k weak , as

D JS (k) = 1 2 D KL (p k weak ||q) + 1 2 D KL (p k ||q) (12)
where q = 0.5p k weak + 0.5p k and

D KL (p||q) = k p(k) log p(k) q(k) (13)
We find the closest class to k weak as

l = arg min k D JS (k) (14)
and merge them to constitute a new class R l ← R l R k weak . We repeat this procedure until we reach the predefined minimum number of classes K min . We determine the necessary number of classes by observing the ICL criterion explained in Section 4.3. The details of the initialization and the stopping criterion of the algorithm are presented in Section 4.1 and 4.2. The summary of the algorithm can be found in Table 1.

Initialization

The algorithm can be initialized by determining the class areas manually in case that there are a few number of classes. We suggest to use an initialization strategy for completely unsupervised classification. It removes the user intervention from the algorithm and enables to use the algorithm in case of large number of classes. First, we run the CEM algorithm for one global class. Using the cumulative distribution of the fitted Nakagami density g = F A (s n |µ 0 , ν 0 ) where g ∈ [0, 1] and dividing [0, 1] into K equal bins, we can find our initial class parameters as µ k = F -1 A (g k |µ 0 , ν 0 ), k = 1, . . . , K where g k 's are the centers of the bins. We initialize the other parameters using the estimated parameters of the global class. Initialize the classes defined in Section 4.1 for K = K max . While K ≥ K min , do While the condition in ( 15) is false, do E-step: Calculate the posteriors in (8) C-step: Classify the pixels regarding to (9) M-step: Estimate the parameters of amplitude and texture densities as (10) Find the weakest class using [START_REF] Celeux | A Classification EM Algorithm for Clustering and Two Stochastic Versions[END_REF] Find the most similar class to the weakest class using [START_REF] Fraley | Model-based Clustering, Discriminant Analysis, and Density Estimation[END_REF][START_REF] Ward | Hierarchical groupings to optimize an objective function[END_REF][START_REF] Schwarz | Estimating the Dimension of a Model[END_REF] Merge these two classes

R l ← R l R k weak K ← K -1

Stopping Criterion

We observe the normalized and weighted absolute difference between sequential values of parameter set θ k to decide the convergence of the algorithm. We assume that the algorithm has converged, if the following expression is satisfied:

K k=1 N k |θ t k -θ t-1 k | N |θ t-1 k | ≤ 10 -3 (15)

Choosing the Number of Classes

Although the SAR images which we used have a small number of classes, we validate our assumption on number of classes using the Integrated Completed Likelihood (ICL) [START_REF] Biernacki | Assessing a Mixture Model for Clustering with the Integrated Completed Likelihood[END_REF]. Even though BIC is the most used and the most practical criterion for large data sets, we prefer to use ICL because it is developed specifically for classification likelihood problem, [START_REF] Biernacki | Assessing a Mixture Model for Clustering with the Integrated Completed Likelihood[END_REF], and we have obtained better results than BIC in the determination of the number of classes. In our problem, the ICL criterion may be written as

ICL(K) = N n=1 K k=1 log{p(s n | θk ) ẑn,k p(ẑ n,k | Ẑ∂n , η)} - 1 2 d K log N (16)
where d K is the number of free parameters. In our case, it is

d K = 12 * K + 1.
ẑn,k is the maximum a posterior estimate of z n,k found in C-step. We also use the BIC criterion for comparison. It can be written as

BIC(K) = N n=1 log K k=1 p(s n | θk )p(z n,k |Z ∂n , η) - 1 2 d K log N (17)

Simulation Results

This section presents the high resolution SAR image classification results of the proposed method called AML-CEM (Amplitude density mixtures of MnL with CEM), compared to the corresponding results obtained with other methods which are DSEM-MRF [START_REF] Krylov | Supervised High-Resolution Dual-Polarization SAR Image Classification by Finite Mixtures and Copulas[END_REF] and K-MnL. We have also tested supervised version of AML-CEM [START_REF] Kayabol | SAR Image Classification with Non-stationary Multinomial Logistic Mixture of Amplitude and Texture Densities[END_REF] where training and testing sets are determined by selecting some spatially disjoint class regions in the image, and we run the algorithm twice for training and testing. The sizes of the windows for texture and label models are selected to be 3×3 and 13×13 respectively by trial and error. We initialize the algorithm as described in Section 4.1 and estimate all the parameters along the iterations. The K-MnL method is the sequential combination of K-means clustering for classification and Multinomial Logistic label model for segmentation to obtain a fairer comparison with the K-means clustering since K-means does not provide any segmented map. The weak point of the K-means algorithm is that it does not converge to the same solution every time, since it starts with random seed. Therefore, we run the K-MnL method 20 times and select the best result among them.

We tested the algorithms on the following TerraSAR-X image:

-TSX1: 1200 × 1000 pixels, HH polarized TerraSAR-X Stripmap (6.5 m ground resolution) 2.66-look geocorrected image which is acquired over Sanchagang, China (see Fig. 1(a)). c Infoterra.

For TSX1 image in Fig. 1(a), the full ground-truth map has been generated manually. Fig. 1 shows the classification results where the red colored regions indicate the misclassified parts according to 3-classes ground-truth map. We can see the plotted ICL and BIC values with respect to number of classes in Fig. 2. The variations in the ICL and BIC plots are slowed down after 3. ICL reaches its maximum value at 4. Since the difference between the values at 3 and 4 is very small and our aim is to find the minimum number of classes, we may say that the mixture model with 3 number of classes is almost enough to represent this data set. Fig. 3 shows several classification maps found with different numbers of classes. From this figure, we can see the evolution of the class maps along the agglomeration based algorithm. The numerical accuracy results are given in Table 2 for 3-classes. The supervised AML-CEM gives the best result over all. In supervised methods, the accuracy results of K-MnL is a bit better than those of unsupervised AML-CEM, but K-MnL is able to provide these results in case of a given number of classes. Due to this, we may call K-MnL as a semi-supervised method.

The simulations were performed on MATLAB platform on a PC with Intel Xeon, Core 8, 2.40 GHz CPU. The total 57 iterations are performed in 5.07 minutes for K = 1, . . . , 8 to plot the graphic in Fig. 2 and the total number of the processed pixels are about 1.2 millions.

Conclusion and Future Work

Using an agglomerative type unsupervised classification method, we eliminate the negative effect of the latent class label initialization. According to our experiments, the larger number of classes, we start the algorithm with, the more initial value independent results, we obtain. Consequently, the computational cost is increased as a by-product. The classification performance may be increased by including additional features as texture or polarization.

  is the set which contains the neighbors of z n in a window M(n) defined around n. The function v k (z n,k ) returns the number of labels which belong to class k in the given window. The mixture density in (4) is spatially-varying with given function v k (z n,k ) in[START_REF] Dempster | Maximum Likelihood from Incomplete Data via the EM Algorithm[END_REF].

Fig. 1 .

 1 Fig. 1. (a) TSX1 image, (b), (c) and (d) classification maps obtained by K-MnL, supervised and unsupervised ATML-CEM methods. Dark blue, light blue, yellow and red colors represent water, wet soil, dry soil and misclassified areas, respectively.

Fig. 2 .

 2 Fig. 2. ICL and BIC values of the classified TSX1 image for several numbers of sources (from 1 to 8).

Fig. 3 .

 3 Fig. 3. Classification maps of TSX1 image obtained with unsupervised ATML-CEM method for different numbers of classes K = {2,3,5,8}.

Table 1 .

 1 Unsupervised CEM algorithm for classification of amplitude based mixture model.

Table 2 .

 2 Accuracy of the classification of TSX1 image in water, wet soil and dry soil areas and average. water wet soil dry soil average DSEM-MRF (Sup.) 90.00 69.93 91.28 83.74 AML-CEM (Sup.) 88.98 71.21 93.06 84.42 K-MnL (Semi-sup.) 89.71 86.13 72.42 82.92 AML-CEM (Unsup.) 88.24 62.99 96.39 82.54

Acknowledgments. The authors would like to thank Aurélie Voisin (Ariana INRIA, France) for interesting discussions and Astrium-Infoterra GmbH for providing the TerraSAR-X image.


AN INSERTION OPERATOR PRESERVING INFINITE REDUCTION SEQUENCES

A common way to show the termination of the union of two abstract reduction systems, provided both systems terminate, is to prove they enjoy a specific property (some sort of "commutation" for instance). This specific property is actually used to show that, for the union not to terminate, one out of both systems must itself be non-terminating, which leads to a contradiction. Unfortunately, the property may be impossible to prove because some of the objects that are reduced do not enjoy an adequate form.

The purpose of this article is then threefold. It first introduces an operator enabling to insert a reduction step on such an object, and therefore to change its shape, while still preserving the ability to use the property. Of course, some new properties should be verified.

Secondly, as an instance of our technique, the operator is applied to relax a well-known lemma stating the termination of the union of two termination abstract reduction systems.

Finally, this last lemma is applied in a peculiar and in a more general way to show the termination of some lambda-calculi with inductive types augmented with specific reductions dealing with: (1) copies of inductive types; and (2) with the representation of symmetric groups.

INTRODUCTION

1.1. Motivation. Given two reduction systems, one common way to prove the termination of the union of both systems goes this way:

(1) if one or both systems are themselves terminating;

(2) and some other property (e.g. some sort of "commutation") is verified; then the application of an appropriate lemma concludes the expected result. This gives an instance of so-called modular proofs in rewriting theory.

The lemma in question is itself often proved by first supposing that the union is not terminating and then, using properties 1 and 2, by showing that it leads to a contradiction (typically: one can build a reduction sequence beginning by an infinite fragment of one out of both reductions, while it is already known to be terminating, by hypothesis).

The ability to build an infinite reduction sequence out of another one (also terminating) is crucial and is usually ensured by property 2. Some examples of such a property may be found in [START_REF] Bachmair | Commutation, transformation, and termination[END_REF]. One nice feature of such a proof technique is that it often relies on simple diagram chasing.

Sometimes, however, these proofs will not work because there are some cases where the objects (whatever they may be: terms, trees, graphs, or so) are too complex for the diagrams to be closed. On the other hand, there are situations s.t. if the object at the root of the diagram satisfied yet another condition, the diagram in question could be closed. If this condition could itself be obtained for a reduct of the root object, the method still works , using a slightly modified version of the original lemma with subsequent conditions.

For this, we define an operator transforming an infinite reduction sequence into another one by inserting a given reduction step at the beginning of the sequence. Then we give an example of how it may be used to derive the new lemma ensuring that the union of two reduction systems is terminating. Finally, we use this new lemma to redo and generalise some proofs carried out in different articles [START_REF] Chemouil | Remarks on isomorphisms of simple inductive types[END_REF], Soloviev and Chemouil, 2004, Chemouil, 2005].

1.2. Terminology and Notations. Most of our terminology and notations come from [START_REF] Baader | Term Rewriting and All That[END_REF]] and [Terese, 2003] : Definition 1.1 (Abstract Reduction System). An Abstract Reduction System (ARS for short) is a structure A := (A, {→ R | R ∈ I}), where A is a set of objects and {→ R | R ∈ I} is a set of binary reduction relations on A indexed by a set I. being finite) s.t. the second element of the last pair in u coincides with the first element of the first pair in v.

1.3. The Adjournment Lemma. Let us now give an example of a lemma deriving the termination of the union of two ARS. This lemma has known a few variants and various names (see [START_REF] Bachmair | Commutation, transformation, and termination[END_REF], Geser, 1990, Doornbos and von Karger, 1998, Chemouil and Soloviev, 2003]).

Definition 1.3 (Adjournment). Let R and S be two reduction relations. Then S is adjournable w.r.t. R if S R ⊆ R (RS) * . S R ⊆ R (RS) * is the relational way to write the following statement:

∀ r∀ s∀ t • r → S s ∧ s → R t ⇒ ∃ u • r → R u ∧ u * → RS t .
The corresponding diagram is the following.

S R 1 1 R B B RS * t t
Lemma 1.1 (Adjournment). Let R and S be two reduction relations s.t.:

• R ⇓; • S ⇓; • S is adjournable w.r.t. R.
Then RS ⇓.

Proof. Let R and S be two reduction relations s.t. R ⇓, S ⇓ and S is adjournable w.r.t. R. Suppose RS is not terminating. Then, there exists an infinite sequence of RS-reductions, alternating finite subsequences of Rand S-reductions, as R and S both terminate. Therefore, going from the beginning of the sequence, one can "pull up" an R-reduction by adjourning the first S-reduction followed by an R-reduction. Iterating this process yields an infinite R-reduction sequence. Contradiction. 1.4. Example. Though useful, this lemma is not powerful enough to deal with some special reductions which we added to a simply-typed λ-calculus with inductive types. This is why we devised the insertion operator to be presented. But let us first give a quick glance at an example of a situation where usual results do not apply well or at all (this situation is dealt with in full detail in Section 4.3).

Our example appears in a simply-typed λ-calculus with inductive types (that is, recursive types with only strictly-positive occurrences of recursion type variables). Briefly (see Section 4.1 for full details), the β µ -reduction rule for primitive recursion is given by:

- → t (c i - → r ) → βµ t i - → r ------→ ( - → t r 0 ) -------→ ( - → t • r 1 ) ,
where -→ t is the recursion operator, (c i -→ r ) is a constructor of an inductive type together with its parameters, r 0 is the result of recursive calls on a non-functional parameter, and r 1 is the result of recursive calls on a functional parameter.

Let us now write [n] for the set {i ∈ N | 1 i n}. The set [n] is then represented by an inductive type, denoted n := µα (c n 1 : α, . . . , c n n : α) (there can be various representations, just by changing names of constructors, of course). Then, to every function f :

[n] → [m] corresponds a term f : n → m of the form c m f (1) , . . . , c m f (n)
n,m , with m := µα (c m 1 : α, . . . , c m m : α). Now, suppose one wants to embed the notion of symmetric group σ n into the reduction relation (see Section 4.3 for full details). In such a setting, it is well-known that any permutation s = id can be decomposed in a unique way (up to the ordering of factors) in a product of cycles with mutually disjoint carriers. Composition of disjoint cycles is commutative but it remains possible to set up an ordering <, lexicographical for instance, on cycles in order to obtain a canonical decomposition. Hence, every map f :

[n] → [n] (n 2) is equal to a product of m mutually disjoint cycles (m 2) f 1 , . . . , f m : f = f 1 • • • • • f m (with f 1 < . . . < f m ).
This obviously leads to defining a so-called θ -reduction by

f r → θ f 1 (. . . (f m r) . . .)
for every permutation f ∈ σ n , for all n 2, where f is decomposed into m 2 mutually disjoint cycles {f 1 , . . . , f m } ⊆ σ n .

Then, to show termination of βηθ -reduction (which includes β µ θ reduction as well as other usual reduction rules, such as β → -reduction and η → -expansion), there is a difficulty: if we try to adjourn θ w.r.t. βη, we get the following diagram for β µ -reduction:

C f c i θ v v βµ 8 8 C f 1 (. . . (f m c i ) . . .) βµ B B C c f (i) C f 1 (. . . (f m-1 c fm(i) ) . . .) βµ * a a
which does not enable us to state much. Now, let us call β n -reduction the fragment of β µ applying to terms f : n → n; we then have:

f c n i → βn c n f (i)
for all f : n → n.

One can then notice that adjournment would be usable provided terms were initially in β n -normal form, first. There lies the idea of the operator devised in this paper which precisely enables to change the shape of objects, while preserving infinite reduction sequences dealt with in proofs of lemmas such as the Adjournment Lemma.

1.5. Outline of the Paper. In Section 2, we define the operator inserting a reduction step at the beginning of a reduction sequence, yielding a new one which is proved to be infinite if the first one was. We also give some simple sufficient conditions when the operator verifies a certain property. Then, in Section 3, we define a specialised form of the Adjournment Lemma enabling to deal with some complex situations.

Finally, in Section 4, we show how this new lemma was used on two situations regarding the addition of some extensional rewrite rules in a simply-typed λ-calculus with inductive types. A first exposition of these situations can be found in [Chemouil, 2005] and [START_REF] Soloviev | Some algebraic structures in lambda-calculus with inductive types[END_REF] without as much abstraction and as many details as in the present article.

AN INSERTION OPERATOR

2.1. Intuition. Let us first give some intuition. Let U and T be ARS. We are going to define an insertion operator, inserting a given T -reduction (t, t ) at the beginning of a possibly infinite sequence of U -reductions (provided a few properties are verified, of course), thus yielding a new sequence. Using a particular relation S on objects from both sequences, the operator will ensure that the sequence shall be infinite if the initial sequence was.

Intuitively, the idea underlying our technique, for a finite sequence, is the following: given a sequence u ∈ U * , we build a new sequence Θ t,t S (u) ∈ U * in such a way that, to every reduction step in u, there corresponds some reduction(s) in Θ t,t S (u) after which it is possible to "find again" the original sequence u through S. Because of this idea of return to the initial sequence, we point this relation from the new sequence back to the initial (this is expressed using an oriented arrow in the accompanying diagram).

S Θ t,t S (u) H H u∈U * F F
Indeed, inserting a T -reduction at the beginning of u implies that many descendants of the object reduced by T are likely to be in a shape, in Θ t,t S (u), different than the shape of the descendants of the same object not reduced initially, in u. The relation S enables to draw a correspondence between the descendants in both sequences.

2.2. The Lemma.

Definition 2.1 (Prosimulation). Let U be an ARS and S be a binary relation on the domain of

U . Then S prosimulates U if S → U ⊆ * → U S.
Notice that this definition is correct as the domain of * → U is the same as the one of U . Choosing the letter S for this relation is not fortuitous: indeed, this is to recall the notion of simulation from concurrency theory. In this discipline, a simulation is a relation between labelled transition systems and provides a behavioural abstraction of such a system. In our context, S is a simulation from U to U * . Note that some similar questions related to simulation were also studied independently in [Lengrand, 2005]

S r ∈U * G G S Θ t,t S (v) H H v∈U * F F (IH) r∈U G G
Remark 2.1. As for the last case, note that we only use this definition for deterministic or finite and bounded cases, hence the case when there exist arbitrarily many r such that Θ t,t S (u) := Θ t,t S (v) r will not occur.

Notice that properties (I1) and (I2) are verified in both cases. In particular, the second property enables us to extend the operator to infinite reduction sequences: indeed, appending a new reduction step to an initial finite sequence keeps unchanged the reduction sequence corresponding to the initial fragment.

As will be made clearer later, the aim of this operator is just to constructively assess the existence of an infinite sequence given another one.

Definition 2.3 (Echo). Let → be a reduction relation and S a relation on objects. Then S echoes → if

∀ a 0 • ∀ a S a 0 • ∃ N ∈ N * • ∀ a 0 → • • • → a N • ∃ k ∈ {1, . . . , N } • ∃ b S a k • a + → b .
In other words, S echoes → if, going from an object a 0 and any object a s.t. a S a 0 , we can find a bound N > 0 s.t., for every finite fragment of length N of any sequence of reductions (possibly infinite) beginning by a 0 , there is an object a k in this fragment (with k 1) with an object b s.t. b S a k which, itself, derives from a in at least one step. This is informally expressed in the following diagram:

a S + G G b S ) 7 G G . . . a 0 G G . . . G G a k G G . . . G G a N G G . . .
Intuitively, one can see that if the initial sequence is infinite, the resulting one will also be infinite, as echoing ensures that, for some finite fragments of sufficient length in the initial sequence, the resulting sequence will also contain reduction steps.

Lemma 2.1 (Insertion). Let U , T be ARS and S a relation s.t. S prosimulates and echoes U . Then, for any infinite sequence u of U -reductions, beginning by t, and every T -reduction (t, t ) s.t. (t , t) ∈ S, the sequence Θ t,t S (u) is also infinite. Proof. Let u be an infinite sequence of U -reductions beginning by an object t 0 . As S prosimulates U , we can build Θ t0,t S (u). This sequence cannot end as, because S echoes U , there necessarily exists a bound to the length of initial fragments of u for which there is at least a reduction step in Θ t0,t S (u). This process of stepping along u and finding corresponding steps in Θ t0,t S (u) can be iterated infinitely as u is not terminating.

2.3. Some Sufficient Conditions. We now discuss the case when U enjoys specific properties, then when S is not only an arbitrary relation but a reduction relation itself.

2.3.1. Insertability and Echoing. Suppose we have T U . The insertion operator is initially defined for finite sequences, but so as to be extendible to non-terminating ones. As a consequence, as we want the sequence Θ t,t S (u) to be infinite provided the sequence u is, two cases are possible:

• In the case where a reduction in u comes from U \ T , it should be echoed by at least one Ureduction. • On the other hand, if it is a T -reduction, there could even be no corresponding U -reduction because inserting a T -reduction at the very beginning of Θ t,t S (u) implies that, perhaps, the Treduction which stood in u is not needed anymore at the same time in Θ t,t S (u). Furthermore, it is important to be ever able to "come back" to u through S. It is then necessary to ensure that the following diagrams can be closed.

S y Ñ U + 3 3 U \T A A (I + ) S y Ñ S z Ò U * 2 2 T A A (I * ) S z Ò
Definition 2.4 (Insertability). Let U , T be ARS and S a binary relation on the domain of U . Then T can be inserted in U w.r.t. S if:

• T U ;

• (I + ) S → U \→ T ⊆ + → U S; • (I * ) S → T ⊆ * → U S.
Lemma 2.2. Let U , T be ARS and S a binary relation on the domain of U s.t.:

• T is finitely branching ;

• T can be inserted in U w.r.t. S; • T ⇓.
Then S prosimulates and echoes U .

Proof. First, T can be inserted in U w.r.t. S, therefore S obviously prosimulates U . Furthermore, by König's Lemma, the fact that T is finitely branching and terminating implies it is always possible to find, for every initial term, the bound necessary to echoing.

Corollary 2.1. Let U , T be ARS and S a binary relation on the domain of U s.t.:

• T can be inserted in U w.r.t. S; • T ⇓.
Then, for any infinite sequence u of U -reductions, beginning by t, and every T -reduction (t, t ) s.t.

(t , t) ∈ S, the sequence Θ t,t S (u) is also infinite. 2.3.2. Case where the Prosimulation is a Reduction. The situation can be even more particular. Indeed, S may be a reduction sequence itself, from terms appearing in Θ t,t S (u) to those in u. For instance, we shall use the operator to insert an η → -expansion, in Section 4.2. The relation S could be defined as the inverse of an η → -expansion. Unfortunately, it is not always obvious to define the inverse of such a reduction as it is context sensitive. But we know that η -1 → ⊆ η → (where η → is η → -contraction) and this is therefore the relation we shall use for S. (Nevertheless, considering a reduction relation for S is not an obligation as we shall see in Section 4.3.) Generally, as we insert a T -reduction at the beginning of the sequence, it will be necessary to be able to come back to the initial sequence by "anti-reducing" the descendants of the subterm which was T -reduced initially. As these descendants may enjoy several occurrences, we shall therefore consider a relation T such that T -1 ⊆ T (in other words: (t , t) ∈ T ) and we shall take T * for S. In this case, the Lemma 2.2 imposes to solve diagrams of the following shape:

T * } } U + 3 3 U \T A A (I + ) T * u u T * ~U * 2 2 T A A (I * ) T * u u
As such, the lemma is not easy to use because of the universal quantification on arbitrary-length sequences of T -reductions. The following sufficient conditions are general enough and much simpler to prove.

Lemma 2.3.

T (U \ T ) ⊆ U * (U \ T ) U * T * ∧ T T ⊆ U * T * ⇒ (I + ) ∧ (I * ).
Proof. We respectively write (I + ) and (I * ) for the two members from the left-hand side of the implication.

T Ñ Ñ U * G G U \T G G U * ) ) U \T D D (I + ) T * r r T ~U * 2 2 T A A (I * ) T * u u
Notice first that

(I + ) ⇒ T (U \ T ) ⊆ U * T * , hence (I * ) ∧ (I + ) ⇒ T U ⊆ U * T * .
Writing ( * ) for T * U * ⊆ U * T * , we obviously have (by induction)

T U ⊆ U * T * ⇒ ( * ) . then (I * ) ∧ ( * ) ⇒ (I * ).
We now show that (I + ) ∧ ( * ) ⇒ (I + ) by induction on the length of T * :

• if the length is null, we obviously have

U + 1 1 U \T B B as U \T 1 1 U \T B B
• otherwise the sequence is of the form T * T and we have

T * U * G G U + G G T * U * G G T * T * ( * ) (IH) ( * ) T U * G G U \T G G U * G G T * (I + ) U \T G G Corollary 2.2. Let U , T and T be ARS s.t.: • T U ; • T ⇓ ; • T -1 ⊆ T ; • T (U \ T ) ⊆ U * (U \ T ) U * T * ; • T T ⊆ U * .
Then, for any infinite sequence u of U -reductions, beginning by t, and every T -reduction (t, t ), the sequence Θ t,t S (u) is also infinite.

AN APPLICATION OF INSERTION IN REWRITING: PRE-ADJUSTED ADJOURNMENT

It is rather usual in rewriting theory and λ-calculus to fall upon theorems stating the termination of a reduction relation by supposing first the existence of an infinite sequence of reductions and by showing then that it leads to a contradiction. The proof of the Adjournment Lemma (Lemma 1.3) gives a perfect example of such a situation.

In this kind of cases, if the premises for the definition of the insertion operator are met, it is possible to insert a finite number of reductions ahead of the initial infinite sequence, still preserving the nontermination and thus the possibility to find a contradiction. We shall see in section 4.2 that adjournment alone does not suffice to prove the termination of the union of two particular relations because there is a case where a term must be η → -expanded beforehand in a certain way. Our insertion operator enables us precisely to insert these necessary η → -expansions. In this particular case, S is the η → -contraction which enables to return to the initial sequence. We shall also use the operator in its full generality (i.e. without S being a reduction relation) in section 4.3. Definition 3.1 (Conditional Adjournment). Let R and S be ARS and P a predicate on objects. Then S is adjournable w.r.t. R under condition P if

∀ a∀ b∀ c • P (a) ∧ a → S b ∧ b → R c ⇒ ∃ d • a → R d * → RS c .
The necessity of conditional adjournment became clear to us during our study of non-standard reductions in calculi with inductive types. We think that in case of non-standard reductions, for example, representing mathematical content of the theories formulated in Logical Frameworks it will be rather a rule that ordinary methods based on permutation or ordinary adjournment of conversions turn out to be insufficient.

Definition 3.2 (Realisation). Let T be an ARS, P a predicate on objects and a and object. Then T realises P for a if ∃ b • a * → T b ∧ P (b). We shall also say that T realises P if T realises P for any object a.

Lemma 3.1 (Pre-Adjusted Adjournment). Let R, S, and T be ARS, S a relation and P a predicate on objects s.t.:

• S is adjournable w.r.t. R under condition P ; Suppose now RS is not terminating, i.e. there is (at least) one infinite sequence of RS-reductions. Take any sequence beginning by an object a 0 . As R and S are terminating, we can deduce that this sequence is made up from an infinite alternation of finite fragments of Rand S-reductions. Now, we apply the following process: we follow the sequence from the beginning until reaching the first occurrence of an S-reduction immediately followed by an R-reduction, for an object a. In other words, we have initially a finite fragment X of reductions, where X = R * S * (that is X = R * or X = R * S + ), leading to a. The sequence is therefore of the following form

• T ⊆ R ; • R ⇓ ; • S ⇓ ; • T
a 0 X G G a S G G R G G RS ∞ G G .
There are now two possibilities regarding a:

• Either P (a): it is then possible to adjourn the S-reduction following a, thus obtaining:

a 0 X G G a S G G R 9 9 R G G RS ∞ G G b RS * t t
• Or ¬P (a): it is then possible to insert a T -reduction from a, keeping a infinite sequence of RS-reductions:

a 0 X G G a S G G T ⊆R 9 9 R G G RS ∞ G G b RS ∞ G G Now, if X = R *
, the new infinite sequence begins with a fragment of R-reductions longer than in the initial sequence (as T ⊆ R). It is therefore possible to iterate this process from b, and to keep lengthening the initial fragment of R-reductions. If X = R * S + , it is necessary to iterate this process once more from a 0 because the new sequence is of the form

a 0 R * G G S * G G c S G G R G G b RS ∞ G G
and a new conditional adjournment (possibly foregone by insertions to realise P for c) is therefore necessary to extend the initial fragment of R-reductions.

In both cases, the initial fragment of S-reductions gets smaller and we build a fragment of R-reductions which is longer and longer, which is an infinite process as RS does not terminate. But R ⇓.

APPLICATIONS IN LAMBDA-CALCULUS

We now present two applications of our Pre-Adjusted Adjournment Lemma. They were first presented in [Soloviev andChemouil, 2004, Chemouil, 2005] but very briefly, due to lack of space. These studies motivated the creation of the insertion operator. We will now enter into more details.

4.1. The Setting. Let us first recall the setting of our work, which is a simply-typed λ-calculus featuring arrow, product and unit types, all together with computational and extensional rewrite rules, as well as inductive types (i.e. some special case of more general recursive types) with computational rewrite rules corresponding to structural recursion.

Definition 4.1 (Types). Define, by mutual induction:

• the set T of types α ∈ TV α ∈ T (V ) 1 ∈ T (1) ρ ∈ T σ ∈ T (ρ × σ) ∈ T (×) ρ ∈ T σ ∈ T (ρ → σ) ∈ T (→) - → κ = ∅ - → c ⊆ C α ∈ TV - → κ ⊆ Sch(α) µα ( - → c : - → κ ) ∈ T (µ)
• the set Sch(α) of (constructor) schemas on a type variable α

- → ρ ⊆ T - → ρ ⊆ SPos(α) - → ρ → α ∈ Sch(α) (SCH)
• the set SPos(α) of strictly positive operators over a type variable α

ρ ∈ T α ∈ FV(ρ) ρ ∈ SPos(α) (SPOSPAR) - → ρ ⊆ T α ∈ FV( - → ρ ) - → ρ → α ∈ SPos(α) (SPOSREC)
• and the set of free type variables (defined the usual way).

One can remark that a schema κ on α is written ρ 1 → . . . → ρ m → α (m 0). If m = 0, the schema is called empty. If it is non-empty, every ρ j is either a strictly-positive operator where α is not free; or a strictly-positive of the form σ 1 → . . . → σ p → α (with 1 j m). In the first case, we speak of a parametric operator and, in the second case, of a 0-recursive operator if -→ σ = ∅ or of a 1-recursive operator otherwise (by analogy with Gödel's finite type recursive functionals).

Example 4.1. Essentially, the strictly-positive approach for inductive types enables to define infinitely branching trees with finite depth. A typical example is given by the representation O of Brouwer's ordinals (where N is the inductive type of natural numbers):

O := µα (0 : α, S : α → α, L : (N → α) → α) .
Here, α is an empty schema, α → α is 0-recursive and

(N → α) → α is 1-recursive.
Definition 4.2 (Preterms). The set of preterms is generated by the following grammar:

t ::= x | | t, t ρ×σ | p 1 ρ×σ t | p 2 ρ×σ t | λx ρ t | (t t) | (c - → t ) | - → t µα ( - → c : - → κ ),ρ , with c ∈ C and x ∈ V.
Preterms of the form -→ t µα ( - → c : -→ κ ),ρ stand for recursors in the sense of Gödel's System T. They contain as many recursion terms as their domain contains constructors. On the other hand, preterms of the form c -→ t inhabit an inductive type. Finally, p 1 and p 2 are projections (we will sometimes write p i to speak about any projection). We now introduce typing the usual way.

δ μ,σ c := - → ρ [α := μ] → -→ ρ [α := σ] → σ ,
where

ρ := ∅ if ρ is a parametric operator, ρ if ρ is a recursive operator.
Example 4.2. Recursion types for Brouwer's ordinals, to any type σ, are:

δ O,σ 0 = σ δ O,σ S = O → σ → σ δ O,σ Γ r : ρ → σ Γ s : ρ Γ (rs) : σ (→-E) (c, - → ρ → α) ∈ μ Γ - → r : - → ρ [α := μ] Γ (c - → r ) : μ (µ-I) Γ - → t : --→ δ μ,σ c Γ - → t μ,σ : μ → σ (µ-E)
Definition 4.5 (Terms). A term is a well-typed preterm.

We now introduce the reduction relation operating on the basic calculus. The computational aspect is expressed by β-reduction while the extensional one is expressed by η-reduction. First of all, given two terms g : σ → τ and f : -→ ρ → σ, we write g

• f := λ - → x - → ρ • g (f - → x ).
Definition 4.6 (β-reduction). We define β-reduction the following way:

(λxr)s → β→ r[x := s] p 1 r, s → β× 1 r p 2 r, s → β× 2 s - → t (c i - → r ) → βµ t i - → r -→ ∆ r
where

∆ r :=      - → t r if the operator corresponding to r is 0-recursive, - → t • r if the operator corresponding to r is 1-recursive,

∅

otherwise.

Example 4.3. Here are the rules for β µ -reduction on Brouwer's ordinals:

t 0 , t S , t L 0 → βµ t 0 t 0 , t S , t L (S p) → βµ t S p ( t 0 , t S , t L p) t 0 , t S , t L (L k) → βµ t L k ( t 0 , t S , t L • k) .
To simplify matters, we shall order operators so that every canonical object c -→ r inhabiting an inductive type is of the form c -→ r p -→ r 0 -→ r 1 , where:

• operators corresponding to -→ r p are parametric ;

• operators corresponding to -→ r 0 are 0-recursive ;

• operators corresponding to -→ r 1 are 1-recursive.

Hence β µ -reduction can be written:

- → t (c i - → r ) → βµ t i - → r ------→ ( - → t r 0 ) -------→ ( - → t • r 1 ) .
Is is now common to define η-reduction as an expansive rule. Though it is then context dependent, its metatheory is usually nicer than for η-contraction which does not behave well when combined with a rule for the unit type (see [Di Cosmo, 1995, Di Cosmo, 1996a, Di Cosmo and Kesner, 1993, Di Cosmo and Kesner, 1996a[START_REF] Cosmo | Rewriting with extensional polymorphic lambda-calculus[END_REF][START_REF] Cosmo | Rewriting with extensional polymorphic lambda-calculus[END_REF]).

Definition 4.7 (η-reduction). Define η-reduction by:

r → η→ λx ρ • rx if      r : ρ → σ,
x / ∈ FV(r), r is not an abstraction nor in applicative position. r → η× p 1 r, p 2 r if r is of product type, r is not a pair nor projected.

r → η1 if r : 1, r = .

Theorem 4.1. βη ⇓ ∧ βη .

Proof. β ⇓ and β are proven using respectively the Tait-Girard method [START_REF] Girard | Proofs and Types[END_REF] and the Tait-Martin-Löf method [Barendregt, 1984] and Newman's Lemma. Then η-reductions are added using standard abstract techniques such as Akama-Di Cosmo's Lemma [START_REF] Cosmo | Rewriting with extensional polymorphic lambda-calculus[END_REF].

(In [Soloviev andChemouil, 2004, Chemouil, 2005], we also have a so-called ν-reduction which implements extensionality on inductive representations of the product and unit types: adding this reduction also yields a convergent system. However, this reduction is not important regarding the topic of the present article, so we will not consider it here.) 4.2. Copies. We now rework the notion of copy of an inductive type introduced in [Chemouil, 2005] using the specialised Pre-Adjusted Adjournment Lemma. 4.2.1. Isomorphisms of Types. We first define the notion of isomorphism of types: we need a typed λcalculus together with an equivalence relation ∼ on terms, an associative composition operator • ρ,σ,τ : (σ → τ ) → (ρ → σ) (simply written •) and a term id ρ : ρ → ρ neutral for • (for all types ρ, σ, τ ). Here, • and id ρ can be defined the obvious way, but not necessarily. Definition 4.8 (Isomorphism of Types). Two types ρ and σ are isomorphic, written ρ ∼ = σ, if there exist two terms f : ρ → σ and g : σ → ρ s.t. f • g ∼ id σ and g • f ∼ id ρ .

It is important to notice that an isomorphism between types might be provable but not computable. This is the reason why it is necessary to devise a rewriting relation implementing ∼ and prove its termination and confluence. 4.2.2. Taxonomy. Definition 4.9 (Copy). Let there be two types π and π and two inductive types ϕ and ϕ s.t. if π appears in ϕ, it is only as a parameter or as the full domain of the functional argument of a 1-recursive operator. Let there also be two terms f : π → π and f : π → π (to take into account co-and contravariant arguments).

Then, ϕ is a copy of ϕ induced by f and f if the first type only differs from the second one by constructor names and by the fact that zero or several occurrences of π in ϕ are replaced by π in ϕ .

If we have a computable isomorphism

f : π ∼ = π : f , µα ( - → c : - → κ ) and µα ( - → c : - → κ )
are called faithful copy of one another. If π does not appear in µα ( -→ c : -→ κ ) or if no occurrence of it is replaced (in other words: ϕ and ϕ only differ by constructor names), we shall speak of carbon copy. We then have carbon copy ⊆ faithful copy ⊆ copy.

In this article, we shall be at best interested in faithful copies.

Remark 4.1. Notice that we will not consider possible constructor reorderings, here. On the contrary, we shall consider that every c i in µα ( -

→ c : - → κ ) corresponds precisely to c i in µα ( - → c : - → κ ).
Obviously, faithful copies form provable isomorphisms. We shall make them computably isomorphic by adding an adequate reduction (χ). 4.2.3. Maximal Abstracted Form and Choice Representation. This section is here to introduce 2 technical definitions which shall be useful later.

Definition 4.10 (Maximal Abstracted Form). Given a term r, we call maximal abstracted form of r the term written r s.t. r begins by as many λ-abstractions as the arity of r.

Remark that r * → η→ r . However, the maximal abstracted form of a term may differ from its η →normal form because the strict subterms of r may not be in normal form in the first case.

We aim at defining terms fc and fc realising the mapping from a type to another one, as long as the latter is a faithful copy of the former, induced by terms f and f . To do so, we present here a notation enabling to precise which occurrence of a parameter if modified. Implicitly, we imagine a user has "selected" or "chosen" previously these occurrences.

Definition 4.11 (Choice). We shall write f r for f r if r : π corresponds to an occurrence to be replaced, and for r otherwise.

Similarly, we shall write g •f for g • f if g has domain π and must be replaced, and for g otherwise.

Remark 4.2. This notation will only be used in particular contexts, to obtain subterms f (f r) or g •f •f all the time, for terms f and f s.t. f : π ∼ = π : f .

Notice that f (f r) = r and g •f •f = g if no replacement is carried out. Else, as f and f are computable isomorphisms by the relation → R , we have f

(f r) = f (f r) * → R r and g •f •f = g • f • f * → R g . 4.2.4. Realising Faithful Copies. We shall write fc : µα ( - → c : - → κ ) → µα ( - → c : - → κ ) and fc : µα ( - → c : - → κ ) → µα ( - → c : - → κ )
for terms generated from two faithful copies and terms f : π ∼ = π : f . Informally, making a difference between parametric, 0-recursive and 1-recursive arguments, we shall have:

fc (c i - → r p - → r 0 - → r 1 ) = c i ----→ (f r p ) ----→ (fc r 0 ) --------→ (fc • r 1 •f ) .
We can see that choices may only appear in parameters or 1-recursive arguments as π is necessarily different from the recursion variable in inductive types.

Example 4.4. Suppose we have a type P isomorphic to N through f : N ∼ = P : f and the following two inductive types:

ϕ := µα (c 1 : α, c 2 : ((N → N) → α) → α, c 3 : N → α → α, c 4 : (N → α) → α) ϕ := µα (c 1 : α, c 2 : ((N → N) → α) → α, c 3 : P → α → α, c 4 : (P → α) → α) .
We decide to replace some occurrences of the parameter N by P. The definition of the isomorphism fc : ϕ → ϕ is then:

fc c 1 := c 1 fc (c 2 k) := c 2 k fc (c 3 h t) := c 3 (f h) (fc t) fc (c 4 k) := c 4 (fc • k • f ) .
As we write in Definition 4.9, the replaced parameter for a 1-recursive operator must be the full domain of the functional argument. For this reason, we could only make a replacement for c 2 if we considered N → N as a parameter, and not N as it the case here. If one wishes to modify also this part, it is necessary to make a copy in two steps, that is by defining a sequence of copies ϕ ϕ ϕ , with ϕ := µα (c 1 : α, c 2 : ((P → P) → α) → α, c 3 : P → α → α, c 4 : (P → α) → α) .

Definition 4.12. Let ϕ := µα ( -→ c : -→ κ ) and ϕ := µα ( -→ c : -→ κ ) be faithful copies induced by f : π ∼ = π : f . Benefiting from the ordering convention stated on p. 13, every constructor c i has type

κ i [α := ϕ] = - → τ → - → ϕ → ------→ ( - → σ → ϕ) → ϕ,
where -→ τ corresponds to parameters, -→ ϕ to 0-recursive operators and ------→ ( -→ σ → ϕ) to 1-recursive operators.

We define the term fc : ϕ → ϕ (and similarly fc ) by

fc := - → a ϕ,ϕ
where every a i is the → βη -normal form of

λ - → p - → τ λ - → z - → ϕ λ - → u ---→ - → σ →ϕ λ - → r - → ϕ λ - → s ----→ - → σ →ϕ • c i --→ (f p) - → r ----→ (s •f ) .
Remark that fc and fc are closed terms, because f and f are (being isomorphisms).

Lemma 4.1. ϕ and ϕ are provably isomorphic.

Proof. For every canonical object c

i - → r p - → r 0 - → r 1 , we have indeed fc (fc x) * ↔ βη x: fc (fc (c i - → r p - → r 0 - → r 1 )) → βµ fc (a i - → r p - → r 0 - → r 1 ----→ (fc r 0 )) -----→ (fc • r 1 )) * → β→ fc (c i ---→ (f r p ) ----→ (fc r 0 ) --------→ (fc • r 1 •f )) → βµ a i ---→ (f r p ) ----→ (fc r 0 ) --------→ (fc • r 1 •f ) -------→ (fc (fc r 0 )) -----------→ (fc • fc • r 1 •f ) * → β→ c i -------→ (f (f r p )) -------→ (fc (fc r 0 )) -------------→ (fc • fc • r 1 •f •f ) We now use the fact that f (f x) * ↔ βη x : * ↔ βη c i - → r p -------→ (fc (fc r 0 )) --------→ (fc • fc • r 1 )
By (IH), we notice the particular shape of the last arguments (cf. subsection 4.2.5):

* ↔ βη c i - → r p - → r 0 --→ r 1 ← η→ c i - → r p - → r 0 - → r 1 .
As this isomorphism is provable but not computable, we propose to embed it into the calculus in the following way. Definition 4.13 (χ-reduction). Define χ-rewriting by: (χ 1 ) fc (fc r) → χ r (χ 2 ) fc (fc r) → χ r , and χ-reduction as its contextual closure.

Lemma 4.2 (Substitutivity and Compatibility).

• r → χ r ⇒ r[x := s] → χ r [x := s] ; • s → χ s ⇒ r[x := s] * → χ r[x := s ].
Proof. Easy inductions. 4.2.5. Convergence. We must now show the convergence of βηχ-reduction. Unfortunately, it does not seem possible to use a simulation or Akama-Di Cosmo's Lemma. Still, we wish to use abstract techniques, like adjournment.

The Adjournment Lemma seems adequate to show the termination, but suppose we have a term

- → t (fc (fc (c i - → r p - → r 0 - → r 1 )))
and following reductions:

- → t (fc (fc (c i - → r p - → r 0 - → r 1 ))) → χ - → t (c i - → r p - → r 0 - → r 1 ) → βµ t i - → r p - → r 0 - → r 1 -----→ ( - → t r 0 ) -------→ ( - → t • r 1 ) .
Adjourning the χ-reduction w.r.t. the βη-reduction means looking for a term s s.t.

- → t (fc (fc (c i - → r p - → r 0 - → r 1 ))) → βµ s * → βηχ t i - → r p - → r 0 - → r 1 -----→ ( - → t r 0 ) -------→ ( - → t • r 1 ) ,
because the only other possible reduction in that case is β µ . But the sequence we end up with is rather of the following form:

- → t (fc (fc (c i - → r p - → r 0 - → r 1 ))) → βµ * → βην - → t (c i - → r p - → r 0 --→ r 1 ) * → βην t i - → r p - → r 0 --→ r 1 ------→ ( - → t r 0 ) --------→ ( - → t • r 1 ) * → β→ t i - → r p - → r 0 --→ r 1 ------→ ( - → t r 0 ) -------→ ( - → t • r 1 ) .
As a consequence, if copies do not contain 1-recursive operator, the proof by adjournment is straightforward. Otherwise, one can see in the previous example that adjournment would have been possible provided the 1-recursive arguments had been in maximal abstracted form. This is what we are going to do using our Pre-Adjusted Adjournment Lemma.

Lemma 4.3. χ ⇓ ∧ χ .

Proof. Obvious.

We shall now use the insertion operator in the case where the relation S is a reduction relation containing the inverse of η → : Definition 4.14 (η → -reduction). We define η → -rewriting (or η → -contraction) by

λx ρ • rx → η → r if x / ∈ FV(r),
and η → -reduction as its contextual closure.

Lemma 4.4. η → can be inserted βηχ w.r.t. η → .

Proof. First of all, we obviously have η → βηχ. By Lemma 2.3, we now have to show

→ η → → βη×,1χ ⊆ * → βηχ → βη×,1χ * → βηχ * → η → and → η → → η→ ⊆ * → βηχ * → η → . (see Appendix A for relevant diagram chasing).
Lemma 4.5. βηχ ⇓.

Proof. We define a condition P on terms s.t. 1-recursive arguments be in maximal abstracted form. One has:

• η → βη ;

• βη ⇓ by Theorem 4.1;

• χ ⇓ by Lemma 4.3;

• η → realises P as 1-recursive arguments are not in applicative position;

• η → can be inserted in βηχ w.r.t. η → by Lemma 4.4 and η → ⇓. Hence, by Lemma 2.2, η → prosimulates and echoes βηχ. Moreover, as η -1 → ⊆ η → , we know that for any pair (t, t ) ∈ η → , we have indeed (t , t) ∈ η → . Using the Pre-Adjusted Adjournment Lemma, we are left with proving that χ can be adjourned w.r.t. βη under condition P (see Appendix B for relevant diagram chasing).

Lemma 4.6. βηχ .

Proof. By Lemma 4.5 and Newman's Lemma, it is enough to show that βηχ LC. As βη and χ , there is only left to show that ← βη → χ ⊆ * → βηχ * ← βηχ . We do not detail fully this easy proof as confluence is not the focus of this article. 4.3. The Symmetric Group. Our purpose in [START_REF] Soloviev | Some algebraic structures in lambda-calculus with inductive types[END_REF] was to add some other extensional rewrite rules on inductive types corresponding to some extensional relations between inductive types (see [Chemouil, 2005] for a quite detailed explanation of the problem).

As a matter of fact, one purpose was to embed the notion of symmetric group into the reduction relation. This study began as part of the project 'Type Theory and Formal Calculus', sponsored by Liapunov Institute. The idea, presented in [START_REF] Flegontov | Type theory in differential equations[END_REF], consisted in formalising groups acting on some differential equations into a proof assistant. Equations were represented as vectors of parameters (seen as elements of an inductive type) and the group itself as symmetries acting on coefficients.

Let us first write [n] for the set {i ∈ N | 1 i n}. The set [n] is then represented by an inductive type, denoted n := µα (c n 1 : α, . . . , c n n : α) (there can be various representations, just by changing names of constructors, of course). Then, to every function f :

[n] → [m] corresponds a term f : n → m of the form c m f (1) , . . . , c m f (n) n,m , with m := µα (c m 1 : α, . . . , c m m : α).
Consider now the case of a map f : [n] → [n] and the associated term f : n → n. It is then possible to study the representation of the symmetric group σ n in type theory. Let us first recall some basics of Group Theory. Definition 4.15 (Group). A group (G, * , • -1 , 1) is a set G together with a binary map * , a unary map • -1 and an element 1 ∈ G s.t.:

• * is associative;

• 1 is neutral for * ; • every element x has a symmetric x -1 (i.e. s.t. ∀ x ∈ G • x * x -1 = x -1 * x = 1).
Definition 4.16 (Permutation). A permutation is a bijection from a finite set to itself.

The carrier of a permutation on a set is made of those elements which aren't invariant under the permutation.

Lemma 4.7 (Symmetric Group). The set of permutations on [n], together with composition as the product, is a group, called the symmetric group of order n and denoted σ n . Definition 4.17 (Cycle). A cycle on a set E is a permutation s s.t. there is {a 1 , . . . , a n } ⊆ E s.t.

s(a i ) = a i+1 for i < n; s(a n ) = a 1 s(b) = b for b / ∈ {a 1 , . . . , a n }.
Theorem 4.2. Every permutation s = id can be decomposed in a unique way (up to the ordering of factors) in a product of cycles with mutually disjoint carriers.

Composition of disjoint cycles is commutative but it remains possible to set up an ordering <, lexicographical for instance, on cycles in order to obtain a canonical decomposition. Hence, every map f :

[n] → [n] (n 2) is equal to a product of m mutually disjoint cycles (m 2) f 1 , . . . , f m : f = f 1 • • • • • f m (with f 1 < . . . < f m ).
This obviously leads to the following: Definition 4.18 (θ -reduction). We define θ -reduction by f r → θ f 1 (. . . (f m r) . . .) for every permutation f ∈ σ n , for all n 2, where f is decomposed into m 2 mutually disjoint cycles {f 1 , . . . , f m } ⊆ σ n .

Lemma 4.8 (Substitutivity and compatibility).

• r → θ r ⇒ r[x := s] → θ r [x := s] ; • s → θ s ⇒ r[x := s] * → θ r[x := s ].
Proof. Easy inductions.

Lemma 4.9. θ ⇓ ∧ θ .

Proof. Obvious.

Let us call β n -reduction the fragment of β µ applying to terms f : n → n; we then have:

f c n i → βn c n f (i)
for all f : n → n.

Then, to show termination of βηθ -reduction, there is a difficulty: if we try to adjourn θ w.r.t. βη, we get the following diagram for β µ -reduction:

C f c i θ v v βµ 8 8 C f 1 (. . . (f m c i ) . . .) βµ B B C c f (i) C f 1 (. . . (f m-1 c fm(i) ) . . .) βµ * a a
This suggests to use pre-adjusted adjournment using as a condition the fact that terms must be in β nnormal form. The lemma must be used in full generality (i.e. not w.r.t. a reduction). Notice that it would be hard to consider a deterministic reduction relation β n containing the inverse of β n . Indeed, the inverse image of a constructor c i by the relation β n is generally of cardinality strictly greater than 1. Intuitively, β n is not injective.

Nevertheless, after a first observation of the situation, we can see that the inverse image by β n is finite and that β n -redices are closed terms: therefore, it remains possible to build systematically S by choosing a term g s.t. g c i → βn c f (i) . This shall only collapse, be duplicated or be reduced (even after the decomposition of g itself) to c f (i) .

It is this remark which motivated the definition of insertion as not necessarily depending on a reduction relation.

Definition 4.19. Let f be a permutation in σ n . We now define a binary relation S f on terms the following way. Given two terms a and a , tag with different numbers every subterm of a of the form c f (i) , for all i, and denote by L a the list of these labelled constructors.

Then a S f a if there exists a substitution ζ, mapping a labelled constructor to a term, s.t.:

• a ζ = a;

• and, for all

c f (i) ∈ L a , one has c f (i) ζ * → βn c f (i) (
where is a label).

It is now important to notice that it is not enough to show that β n -reduction can be inserted in βηθ w.r.t. S f . Indeed, a β n -redex happens to be also a θ -redex. Write θ β n for the set of θ -reductions whose left-hand sides are β n -redices, that is of the form f c i (obviously θ β n ⊆ θ ).

Lemma 4.10. (ii) S f echoes βηθ .

β n ∪ (θ β n ) ⇓.
Proof. (i) Obvious.

(ii) We must show that

∀ a 0 • ∀ a S f a 0 • ∃ N ∈ N * • ∀ a 0 → βηθ • • • → βηθ a N • ∃ k ∈ {1, . . . , N } • ∃ b S f a k • a + → βηθ b .
Let a 0 and a be s.t. a S f a 0 . In other words, there is a substitution ζ mapping a term to a labelled constructor s.t. a ζ = a 0 and, for all c f (i) ∈ L a , we have c f (i) ζ * → βn c f (i) . Now, consider all possible reduction sequences beginning by a 0 and taken from β n ∪ (θ β n ). As this latter relation terminates (by Lemma 4.10), there exists a bound -let us write it N 0 -to the length of these sequences. Define N := N 0 + 1.

Let there be an arbitrary sequence of length N of the shape a 0 → βηθ • • • → βηθ a N . We must find a number k ∈ {1, . . . , N } s.t. there is a b s.t. b S f a 1 and a + → βηθ b . There are two possibilities:

• Either we have a 0 → βηθ \βn a 1 : in this situation, it is enough to put k = 1 and to apply the same reduction on a thus obtaining b s.t. b S f a 1 . One should notice here that the value of N is not important when such a reduction is applied to a 0 . This comes from the fact that subterms of a 0 in the image of ζ are β n -redices and therefore, here, can only collapse or be duplicated (in the general case, they may also enjoy a β n -reduction). The echoing is therefore obviously determined. • Or, we have a 0 → βn∪(θ βn) a 1 . In that case, we can glance through the sequence a 0 → βn∪(θ βn)

• • • → βηθ a N until reaching the first occurrence of a reduction different from β n and θ β n . It necessarily exists as N > N 0 : its ordering number is the sought k and it is enough to echo it the same way than in the previous case.

Lemma 4.12. βηθ ⇓.

Proof. We define a condition P on terms s.t. these are in β n -normal form. We have:

• β n θ βη ; • βη ⇓ by Theorem 4.1 ; • θ ⇓ by Lemma 4.9 ; • β n θ obviously realises P (in fact, β n is enough) ; • S f prosimulates and echoes βηθ by Lemma 4.11. By the Pre-Adjusted Adjournment Lemma (Lemma 3.1), we just need to show that θ is adjournable w.r.t. βη under condition P (see Appendix C for relevant diagram chasing). Lemma 4.13. βηθ .

Proof. As βηθ ⇓ and βη and θ by Lemmas 4.12 and 4.9 and Theorem 4.1, it is enough to show that βη and θ locally commute. We do not detail this easy proof here as confluence is not the focus of this article. Proof. First of all, we obviously have η → βηχ. By Lemma 2.3, we now have to show

→ η → → βη×,1χ ⊆ * → βηχ → βη×,1χ * → βηχ * → η → and → η → → η→ ⊆ * → βηχ * → η → .
We do so by considering the possible overlaps for a context C [], without detailing too much this demonstration which is quite simple:

• β → : C [λy • (λxr)sy] η → v v β→ A A C [(λxr)s] β→ A A C [λy • r[x := s]y] η → t t C [r[x := s]] C [(λxλy • ry)s] η → v v β→ A A C [(λxr)s] β→ 6 6 C [(λy • ry)[x := s]y] C [λy • r[x := s]y] η → s s C [r[x := s]] C [(λy • (λxr)y)s] η → v v β→ 2 C [(λxr)s] β→ B B C [r[x := s]] C [(λxr)(λy • sy)] η → v v β→ A A C [(λxr)s] β→ B B C [r[x := λy • sy]] η → * s s C [r[x := s]] • β ×1 (the same for β ×2 ) : C [λx • p 1 r, s x] η → v v β× 1 @ @ C [p 1 r, s ] β× 1 C C C [λx • rx] η → s s C [r] C [p 1 λx • rx, s ] η → v v β× 1 @ @ C [p 1 r, s ] β× 1 C C C [λx • rx] η → s s C [r] C [p 1 r, λx • sx ] η → v v β× 1 C [p 1 r, s ] β× 1 C C C [r]
• β µ : for this reduction, one case is more complex.

-We may simply have:

C λx • - → t (c i - → r ) x η → y y βµ @ @ C - → t (c i - → r ) βµ 8 8 C λx • t i - → r ------→ ( - → t r 0 ) -------→ ( - → t • r 1 )x η → u u C t i - → r ------→ ( - → t r 0 ) -------→ ( - → t • r 1 )
-Or the rewriting step may happen on a recursion terms: * If q the ith recursion term, we end up with:

C - → p , λx • qx, - → r , s, - → t (c i - → u ) η → { { βµ 8 8 C - → p , q, - → r , s, - → t (c i - → u ) βµ 6 6 C (λx • qx) - → u ------→ ( - → t u 0 ) -------→ ( - → t • u 1 ) η → /β→ w w C q - → u ------→ ( - → t u 0 ) -------→ ( - → t • u 1 ) * Otherwise C - → p , λx • qx, - → r , s, - → t (c i - → u ) η → t t βµ C - → p , q, - → r , s, - → t (c i - → u ) βµ B B C s - → u ------→ ( - → t u 0 ) -------→ ( - → t • u 1 )
-Finally, the rewriting step may concern one out of arguments, writing -→ r = ( -→ p , q, -→ s )

and -→ u = ( -→ p , λx • qx, -→ s ), which is likely to be parametric or 1-recursive: Proof. We define a condition P on terms s. C p 1 r, fc (fc s)

C - → t (c i - → u ) η → y y βµ @ @ C - → t (c i - → r ) βµ 8 8 C t i - → u ------→ ( - → t u 0 ) -------→ ( - → t • u 1 ) η → * v v C t i - → r ------→ ( - → t r 0 ) -------→ ( - → t • r 1 ) • η ×,1 χ : in C [r], r cannot be contracted as it is not of functional type. • η → : C [λx • rx] η → y y C [r]
χ v v β× 1 C [p 1 r, s ] β× 1 C C C [r]
• β µ : for this reduction, one case is a little bit more complex.

-We may have:

C fc (fc ( - → t (c i - → r ))) χ y y βµ A A C - → t (c i - → r ) βµ 8 8 C fc (fc (t i - → r ------→ ( - → t r 0 ) -------→ ( - → t • r 1 ))) χ u u C t i - → r ------→ ( - → t r 0 ) -------→ ( - → t • r 1 )
-Recall that, because of the condition P , 1-recursive arguments are in maximal abstracted form, hence the following diagram:

C - → t (fc (fc (c i - → r p - → r 0 - → r 1 ))) χ w w βη + 9 9 C - → t (c i - → r p - → r 0 - → r 1 ) C - → t (c i - → r p - → r 0 - → r 1 )
-The χ-redex can be a recursion term: * If fc (fc q) is the ith term, then we necessarily have -→ u = ∅ :

C -→ p , fc (fc q), -→ r , s, -→ t c i χ w w βµ 6 6 C -→ p , q, -→ r , s,

- → t c i βµ C C C fc (fc q) χ u u C [q] * Otherwise, if it is s, for instance: C - → p , fc (fc q), - → r , s, - → t (c i - → u ) χ t t βµ C - → p , q, - → r , s, - → t c i βµ B B C s - → u --------------→ ( - → p , q, - → r , s, - → t u o )
---------------→ ( -→ p , q, -→ r , s,

- → t • u 1 )
-Finally, the χ-redex can be an argument, in which case we have the following diagram, writing -→ r = ( -→ p , q, -→ s ) and -→ u = ( -→ p , fc (fc q), -→ s ) :

C - → t (c i - → u ) χ y y βµ @ @ C - → t (c i - → r ) βµ 8 8 C t i - → u ------→ ( - → t u 0 ) -------→ ( - → t • u 1 ) χ * v v C t i - → r ------→ ( - → t r 0 ) -------→ ( - → t • r 1 )
• For η-reduction, no interesting overlap is possible as r is necessarily of inductive type in fc (fc r) and therefore cannot enjoy a η-reduction.

APPENDIX C. PROOF OF LEMMA 4.12 Lemma 4.12. βηθ ⇓.

Proof. We define a condition P on terms s.t. these are in β n -normal form. We have:

• β n θ βη ; • βη ⇓ by Theorem 4.1 ; • θ ⇓ by Lemma 4.9 ; • β n θ obviously realises P (in fact, β n is enough) ;

• S f prosimulates and echoes βηθ by Lemma 4.11.

By the Pre-Adjusted Adjournment Lemma (Lemma 3.1), we just need to show that θ is adjournable w.r.t. βη under condition P .

As θ -reduction is compatible and context insensitive (Lemma 4.8), the contexts C [] that we consider, focussing on the possible overlaps, enjoy a simple form. • β µ . For this reduction, the situation is a bit more complex:

-Notice first that it is not possible to have a context of the form C -→ t (f c i ) because it would not be in β n -normal form. However, we may have: -Otherwise, the θ -redex can appear as a recursion term.

* Either f q is the ith recursion term, in which case we have: x x C f 1 (. . . (f m q) . . .)

C - → p , f q, - → r ,

  Definition 4.3 (Recursion Type). Given a constructor c ∈ μ with schema -→ ρ → α and any type σ, the recursion type δ μ,σ c of c is defined by:

Proof.

  It is enough to show that β n θ ⇓, which can be deduced from β n ⇓, θ ⇓ and the fact that → βn ⊆ → θ + → βn . Lemma 4.11. (i) S f prosimulates βηθ ;

  APPENDIX A. PROOF OF LEMMA 4.4 Lemma 4.4. η → can be inserted βηχ w.r.t. η → .

  • rx] APPENDIX B. PROOF OF LEMMA 4.5 Lemma 4.5. βηχ ⇓.

CC

  fc (fc r[x := s]) χ s s C [r[x := s]] C (λx • fc (fc r))s fc (fc r)[x := s] C fc (fc r[x := s]) x := fc (fc s)] χ * s s C [r[x := s]]• β ×1 (the same for β ×2 ) :C fc (fc (p 1 r, s ))

C

  (. . . (f m ((λxr)s)) . . .) β→ B B C f r[x := s] θ u u C f 1 (. . . (f m r[x := s]) . . .) C (λx f r)s θ t t β→ @ @ C (λx f 1 (. . . (f m r) . . .))s β→ C C C (f r)[x := s] C (f 1 (. . . (f m r) . . .))[x := s] C f r[x := s] θ t t C f 1 (. . . (f m r[x := s]) . . .) C (λxr) (f s) ) (f 1 (. . . (f m s) . . .)) β→ B B C r[x := f s] θ * u u C r[x := f 1 (. . . (f m s) . . .)] • β ×1 (the same for β ×2 ) : C f (p 1 r, s ) (. . . (f m (p 1 r, s ) . . .) p 1 r, f 1 (. . . (f m s) . . .) β× 1 D D C [r]

  (. . . (f m t i ) . . .)

.

  Definition 2.2 (Insertion Operator). Let U , T be ARS, S a relation, u a finite sequence of U -reductions beginning with an object t and (t, t ) a T -reduction, s.t.:

	• Otherwise, u = v r with v ∈ U * and r ∈ U . Then, we have Θ t,t S (u) := Θ t,t S (v) r with:
	• S prosimulates U ;
	• and (t , t) ∈ S.
	We define an insertion operator Θ t,t S which, from the sequence u, yields a new sequence Θ t,t S (u) begin-
	ning with the T -reduction (t, t ), and ensuring that:
	(I1) the diagram	Θ t,t S (u)	I I can be closed by S, that is:	Θ t,t S (u)	I I
	t			t		S
		u∈U *	E E		u∈U *	E E
	(I2) and Θ t,t S (u r) = Θ t,t S (u) r where r ∈ U * .
	The sequence Θ t,t S (u) is defined by recursion on u:
	• If u is empty, we insert the T -reduction: Θ t,t S (u) := (t, t ) ∈ T . As (t , t) ∈ S, we have:
			T	t P P
			t	S
				t

  realises 3 P ; • S prosimulates RS ; • S echoes RS. Then RS ⇓. Proof. By Lemma 2.1, there exists Θ t,t S that preserves infinite sequences of R-reductions beginning by t, for any T -reduction (t, t ) s.t. (t , t) ∈ S.

  t. 1-recursive arguments be in maximal abstracted form. One has: • η → βη ; • βη ⇓ by Theorem 4.1; • χ ⇓ by Lemma 4.3; • η → realises P as 1-recursive arguments are not in applicative position; • η → can be inserted in βηχ w.r.t. η → by Lemma 4.4 and η → ⇓. Hence, by Lemma 2.2, η → prosimulates and echoes βηχ. Moreover, as η -1 → ⊆ η → , we know that for any pair (t, t ) ∈ η → , we have indeed (t , t) ∈ η → . Using the Pre-Adjusted Adjournment Lemma, we are left with proving that χ can be adjourned w.r.t. βη under condition P As χ-reduction is context insensitive and is compatible (Lemma 4.2), the contexts C [] we consider, focussing on possible overlaps, have a simple form.

In fact, as the following proof shows, it would even be enough to state that: for any object b, if ¬P (b) then b is not T -normal.

L = (N → O) → (N → σ) → σ .Definition 4.4 (Typing). The typing relation Γ t : ρ is defined by induction on preterms:(x, ρ) ∈ Γ Γ x : ρ (V ) Γ : 1 (1-I) Γ r : ρ Γ s : σ Γ r, s ρ×σ : ρ × σ (×-I) Γ r : ρ × σ Γ (p 1 ρ×σ r) : ρ (×-E1) Γ r : ρ × σ Γ (p 2 ρ×σ r) : σ (×-E2)Γ, x : ρ r : σ Γ (λx ρ r) : ρ → σ (→-I)

* Otherwise this term can be s :

-Finally the θ -redex can appear as a parameter of a constructor. Write -→ u = ( -→ p , f q, -→ s )

and -→ r = ( -→ p , f 1 (. . . (f m q) . . .), -→ s ):

• For η, there is no interesting overlap because of typing issues.

ACKNOWLEDGEMENT

The author wishes to thank Sergei Soloviev for useful advice and Freiric Barral for interesting discussions; as well as the anonymous referees for their detailed and fruitful comments.