A Dubois

G Moneron

A C Boccara

Thermal-light full-field optical coherence tomography in the 1.2 µm wavelength region

Keywords: Optical coherence tomography, Biomedical imaging, Optical tomography, Microscopy, Infrared camera PACS classification codes: 42.25.Hz Interference, 42.25.Kb coherence, 42.30-d Imaging and optical processing

Full-field optical coherence tomography with dynamic focusing correction is demonstrated in the 1.2 µm wavelength region using an Indium Gallium Arsenide area camera as image sensor and a halogen lamp as illumination source. An axial image resolution of 1.6 µm is measured in air (~ 1.1 µm in tissue) which is the best resolution ever achieved in OCT in this wavelength region. En face tomographic images are produced using a phase-shifting method requiring the acquisition of only two phase-opposed interferometric images. In spite of a relatively moderate detection sensitivity of 80 dB within 1.0 s image acquisition time, ultrahigh resolution imaging in highly scattering biological tissues is possible without immersion medium.

Introduction

Optical coherence tomography (OCT) is an emerging imaging technique which provides information on biological tissue morphology [1][2][3]. OCT has the potential to replace conventional biopsy and histopathology, provided that millimeter-range penetration depth and micrometer-scale resolution are possible.

OCT penetration depth depends on scattering and absorption of light within the biological tissues. The intensity of light scattered by particles varies with the optical wavelength  as 1 k  ,

where k > 0 is a parameter which depends on the particle size, geometry and refractive index [4].

Light scattering in biological tissues cannot be easily modeled but it obviously becomes weaker as wavelength is increased [5][6][7]. The absorption of light in tissue is dominated by the absorption by water, since water is the main constituent of biological media. The absorption by water is minimal at the wavelength of  ~ 0.5 µm and has a general trend to increase with wavelength as shown in Fig.

1 [8]. The optimal wavelength to maximize the OCT imaging penetration results from the best trade-off between absorption and scattering. Previous works have shown better penetration depth in highly scattering tissues for OCT operating in the 1.3 µm wavelength region compared to 0.8 µm [7].

The axial resolution of OCT is proportional to 2 0   , where   is the center wavelength and  is the spectral width of the light source [3]. Increasing the center wavelength thus requires increasing the spectral width in a quadratic manner in order to maintain the axial resolution. Efforts have been concentrated on the development of broad-bandwidth light sources in the 1.3 µm wavelength region that would permit OCT micrometer-scale resolution [9,10].

Recently, 1.4 µm axial resolution in ex vivo human skin and arterial biopsies has been demonstrated using a broad-bandwidth light source based on a pulsed erbium fiber laser coupled with a highly nonlinear fiber to generate a supercontinuum in the 1300 nm wavelength region [11].

Full-field OCT is an original approach of OCT, which uses spatially and temporally incoherent light to illuminate the whole field to be imaged [12][13][14][15]. In contrast with conventional OCT, full-field OCT provides tomographic images in the en face (transverse) orientation without scanning of a light beam. The tomographic images are obtained by combination of interferometric images acquired with an image sensor such as a CCD (charge coupled device) digital camera. Full-field OCT, sometimes referred to as full-field optical coherence microscopy, is based on an interference microscope illuminated with a simple white-light lamp. Due to the ultra-short coherence length of this illumination source, the axial resolution is better than that of conventional OCT. The transverse resolution of full-field OCT is similar to that of microscopy, which is better than the one of OCT producing axially-oriented tomographic images. We recently demonstrated an ultrahigh resolution of 0.7 µm  1.0 µm (axial  transverse) in tissues with fullfield OCT at ~ 0.8 µm center wavelength using a halogen lamp and a silicon-based CCD camera [16].

In this paper we present a thermal-light full-field OCT system operating in the 1.2 µm wavelength region where the imaging depth in tissue is presumably greater owing to lower scattering. This new system uses an Indium Gallium Arsenide (InGaAs) area camera and a simplified method for faster image acquisition. We mention that this kind of camera has already been used for full-field OCT imaging with a mode-locked Cr4+:forsterite laser [17]. The spatial resolution and detection sensitivity were however relatively weak. We demonstrate here ultrahigh spatial resolution full-field OCT without immersion medium thanks to dynamic focusing adjustments. Numerical simulations have been performed to quantify the effect of water dispersion and absorption on the axial resolution. The performances of the instrument are reported. Tomographic images relatively deep inside highly scattering tissue such as mouse skin are presented.

Principle

Experimental set-up

The principle of full-field OCT relies on low coherence interference microscopy. The experimental arrangement is based on a bulk Michelson interferometer with identical microscope objectives in both arms, as depicted in Fig. 2. This configuration is referred to as the Linnik interferometer [14,[START_REF] Davidson | Integrated Circuit Metrology, Inspection, and Process Control[END_REF]19]. An easy way to produce light with extremely broad and smooth spectrum with adjustable center wavelength is to use a thermal light source [20]. The black body radiation spectrum is given by Planck's law [START_REF] Heitler | The Quantum Theory of Radiation[END_REF]:

  2 5 21 () exp / 1 hc I hc kT     , ( 1
)
where T is the temperature of the black body, h the Planck's constant, c the speed of light, and k the Boltzmann's constant. At the temperature of 2250 K, the maximum of the black body radiation spectrum is at  = 1.3 µm with a full width at half maximum (FWHM) of  = 1.55 µm. A tungsten halogen lamp is not truly a black body. Its spectrum is however very broad and a lot of infrared light can be emitted. The drawback of a thermal light source such as a halogen lamp is its low brightness. As a consequence it cannot be used for scanning OCT.

Nevertheless, the low spatial coherence of a thermal source is a great advantage for full-field imaging. A halogen lamp is indeed particularly appropriate for full-field OCT in the near infrared.

A halogen lamp (12V-100W), with a stabilized DC power supply, is incorporated in a classical Köhler system for homogeneous illumination of the whole microscope objective fields.

Light is split into the reference and sample arms by a broadband beam-splitter. After recombination by the beam splitter, the sample and reference images are projected onto an image sensor using an achromatic doublet lens optimized around 1.3 µm. The image sensor is an Indium Gallium Arsenide (InGaAs) area camera (model SU320MS-1.7RT Snapshot commercialized by Sensors Unlimited, Inc). The camera has 320 × 256 pixels with 25 µm pitch, delivers 100 % fill factor and has > 70% quantum efficiency from 1.0 µm to 1.6 µm. The camera frame rate is 50 Hz. Dry microscope objectives are used without immersion media because of the absorption of infrared light by water. The reference mirror is a piece of glass providing 4% reflectivity. The objective in the object arm is mounted on a motorized translation stage for dynamic focusing adjustments as will be explained later. The object can be translated in the axial direction using another motorized translation stage in order to image at different depths.

Image acquisition

Due to the low temporal coherence of the illumination source, interference occurs only when the optical path lengths of the two interferometer arms are nearly identical. The interference fringes are comprised in a narrow envelop with width equal to the coherence length of the source. When a biological object is placed under the microscope objective in the object arm, the light reflected by the reference mirror interferes with the light reflected or backscattered by the sample structures contained in a limited volume (the "coherence volume"). This volume is a slice orthogonal to the objective axis, located at a depth inside the object defined by an optical path length difference of zero (this depth defines the "coherence plane"). The thickness of the slice is determined by the width of the fringe envelop. The extraction of the fringe envelop yields therefore an en face tomographic image.

The fringe envelope is extracted using a simple phase-shifting method to optimize the operation speed. A high acquisition speed is of particular importance for imaging of biological objects which cannot remain immobile during long times. Two phase-opposed interferometric images are produced by making the reference mirror oscillating between two positions distant of a quarter of the illumination center wavelength (i.e. ~ 0.3 µm). The photon flux on each pixel of the CCD (coordinates (x,y)) can be written for the two reference mirror positions as

0 1 0 2 ( , ) ( , ) 2 ( , ) cos ( , ) 4 ( , ) ( , ) 2 ( , ) cos ( , ) 4 in c ref o b j ref in c ref o b j ref I I x y R x y R R x y R x y I I x y R x y R R x y R x y                    , (2)
  1, 2 1, 2 0 ( , )
,

T E x y N I x y d t    (3)
To maximize the signal-to-noise ratio, the illumination flux is adjusted so that the camera pixel wells are close to saturation. The number of photoelectrons produced by each pixel is then close to the full-well capacity  sat . Since R obj (x,y) << R ref , we can write according to Eq. ( 2) that

  0 4 sat ref inc IT RR    . ( 4
)
By combining the previous equations, we obtain the following relation:

      2 2 2 12 2 8 cos ref sat obj ref inc R E E N R RR    . ( 5
)
The en face tomographic image, R obj (x,y), can be thus calculated from two phase-opposed interferometric images as expressed in Eq. ( 5). Actually, the fringe envelope is not truly extracted since the phase (x,y) is not eliminated. Due to the size and distribution of the structures in most biological media, the fringes are generally not visible in the images. The most important function of signal acquisition in OCT is to eliminate the contribution of the light which has not interfered. This function is perfectly accomplished by the method presented here. A home-written Visual C++ software was developed to calculate and display the tomographic image in real-time (frame rate of 1 Hz for 2×25 accumulated images).

Dynamic focusing adjustments

As the object is translated in the axial direction to obtain en face tomographic images deeper and deeper, the coherence plane and the focal plane move away from each other because the optical path in air is progressively replaced by an optical path in the biological tissues with higher refractive index (see Fig. 3). Note that this phenomenon is very weak when water immersion microscope objectives are used since biological tissues have refractive index close to that of water [START_REF] Lai | [END_REF].

In a Linnik interference microscope the contrast of the interferometric signal is reduced if one of the objectives is not perfectly in focus [14]. For this reason, the coherence plane must coincide with the focal plane of the objectives in full-field OCT, otherwise the tomographic images vanishes. Focusing adjustments are therefore required as the object is moved up. Using the Snell's law at third order in incidence angle , we calculate that in order to image at a depth z below the surface of the object with refractive index n, the object must be elevated of a distance equal to n×z, while the objective in the object arm must be elevated of a distance

2 1 n Zz n      . ( 6
)
Two computer-controlled motorized translation stages are used to move up both the object and the objective (see Fig. 1).

Performances

Spatial resolution

The axial resolution of our full-field OCT system is governed by the effective optical spectrum, which is given by the product of the halogen lamp spectrum, the spectral response of the camera and the spectral transmission of the system optical components. We measured the interferogram response of the system in air using a silver mirror as object (see Fig. 4 a). The effective spectrum was deduced from Fourier transform of the interferogram (see Fig. 4 b). The center wavelength was found to be at  = 1.2 µm and the FWHM of the fringe envelope to be 1.6 µm. Assuming a tissue refractive index of 1.4, the axial resolution for superficial tissue imaging is therefore ~ 1.1 µm. This is the best axial resolution ever achieved in OCT in this wavelength region. If the optical dispersion is not equal in the two interferometer arms, the axial resolution is degraded [23]. We have performed numerical simulations including the effect of water dispersion and absorption to quantify the degradation of axial resolution when imaging in water, the reference arm being in air [24]. The actual effective spectrum (shown in Fig. 4 b) is considered in the calculations. According to these simulations the degradation of the axial resolution is only of a factor of 1.25 at a depth of 500 µm (see Fig. 5). Dynamic compensation of dispersion is therefore not required in this system. We simply placed fixed antireflection-coated glass plates in both arms to compensate for dispersion mismatch introduced by the microscope objectives which are not perfectly identical (see Fig. 2)

In principle, the transverse resolution is imposed by the numerical aperture of the objectives and the illumination wavelength. Because the objectives are designed for visible light, optical aberrations however degrade the transverse resolution. By imaging the edge of a silicon wafer we estimated the transverse resolution to be  3 µm in air [25][26][27].

Detection sensitivity

Detection sensitivity is a crucial parameter in OCT, because it determines the image quality and the maximum depth to which imaging is possible. The detection sensitivity of full-field OCT depends essentially on the charge capacity of the camera pixels [14][15][16]. The InGaAs camera has a large pixel full well capacity of sat  = 810 5 electrons. Assuming the measurements to be shotnoise limited, the tomographic image would then be calculated as

    2 1 1 2 2 EE       , where
 is an additive noise with the following properties:

1 2 1 2 22 2 12 0                 . ( 7
)
The angle brackets in Eq. ( 7) denote a time average. We assume that the shot-noise results from the fundamental photon noise. According to the Poisson statistic, the shot-noise variance 2  is then equal to the number of photons detected by each camera pixel multiplied by their quantum efficiency. Since the illumination flux is adjusted so that the well of each camera pixel is close to saturation and N images are accumulated, we have 2

sa t N  
. The background noise in our imaging instrument can be regarded as the average value of a tomographic image when there is no interference (i.e. when E 1 = E 2 ). This background noise is equal to  

Considering that the minimum detectable reflectivity corresponds to a signal-to-noise ratio equal to 1 we establish, using Eq. ( 8) and Eq. ( 5) with

Theoretical values of R min as a function of the number N of image accumulation are plotted in Fig. 6.

Measurements of the detection sensitivity are also reported in Fig. 6. The measured sensitivity is ~ 10 dB above the theoretical shot-noise resulting from the ultimate photon noise.

This difference is due to a significant electrical noise of the InGaAs camera. Accumulating images yields to an increase of the detection sensitivity. In practice, we accumulate 225 images, which represents an acquisition time of 1.0 s. A detection sensitivity of 80 dB is then reached.

Image example

To illustrate the performances of the new full-field OCT system presented in this paper, we imaged skin of a mouse ear ex vivo. Figure 6 shows a vertical (XZ) tomographic image reconstructed from a stack of en face tomographic images acquired with steps of 1 µm. In spite of the moderate detection sensitivity, we can image through the entire thickness of the ear ( 300 µm). These results shows that the illumination wavelength in the 1.2 µm region is appropriate for imaging inside highly scattering biological media.

Conclusion

In summary, we have developed a full-field OCT system with dynamic focusing correction operating in the 1.2 µm wavelength region. By use of a simple halogen lamp, the best resolution ever achieved by OCT at this wavelength is obtained. The system uses dry microscope objectives, which is of great interest for applications where immersion media cannot be used.

The image field is currently limited by the low number of pixels of the camera. With the development of high resolution InGaAs area cameras, this limitation will probably be overcome in a near future. Moreover, high-resolution high-speed cameras would enable pixel binning to improve the detection sensitivity while maintaining short image acquisition times.

Figure captions

  where (x,y) represents the optical phase and I 0 is the photon flux at the entrance of the interferometer. R ref is the (uniform) reference mirror reflectivity, R obj (x,y) is the proportion of light reflected by the object which interferes and R inc (x,y) the proportion of light reflected by the object and collected by the microscope objective, which does not interfere. In other words, R obj (x,y) represents the reflectivity distribution of the sample structures contained in the coherence volume. R obj (x,y) thus corresponds to an en face tomographic image. The camera acquires a number N of image pairs. The images corresponding to the same reference mirror positions are summed. The two resulting images (E 1 (x,y), E 2 (x,y)) correspond to N times the integration of the photon flux (I 1 (x,y), I 2 (x,y)) over the camera exposure time T. We denote by  the quantum efficiency of the camera. The total number of photoelectrons delivered by each camera pixel is

  -noise ratio in an image can thus be written as

(

  in average over the image), that the smallest detectable reflectivity R obj = R min is

Fig. 1 :Fig. 2 .

 12 Fig.1: Optical absorption of water [data from Reference 8].

Fig. 3 .

 3 Fig.3. The interferometer is adjusted so that the focal plane and coherence plane coincide at the surface of the object (A). When the object is elevated of a distance e, the coherence plane is then located at e/n below the object surface, and the focal plane at ne (B). The focal plane matches the coherence plane again if the objective is elevated of a distance e(1-1/n 2 ) (C).

Fig. 4 .Fig. 5 .

 45 Fig. 4. Interferogram response of the system measured in air (a). The interferogram envelop has a full width at half maximum of 1.6 µm. The effective spectrum of the system (b) is calculated by Fourier transform of the interferogram. The center wavelength is measured to be of 1.2 µm.

Fig. 6 . 5 .Fig. 7 .

 657 Fig. 6. Detection sensitivity as a function of image accumulation. The theoretical sensitivity is calculated using Eq. (9) with R ref = 0.04, R inc = 0.01, sat  =810 5 .

Fig. 1

 1 Fig. 1

Fig. 2 16Fig. 3

 23 Fig.2

Fig. 4 18Fig. 5

 45 Fig.4

Fig. 6 20Fig. 7

 67 Fig. 6


Chantal Keller
email: keller@lix.polytechnique.fr

Benjamin Werner
email: werner@lix.polytechnique.fr

Importing HOL Light into Coq

We present a new scheme to translate mathematical developments from HOL Light to Coq, where they can be re-used and rechecked. By relying on a carefully chosen embedding of Higher-Order Logic into Type Theory, we try to avoid some pitfalls of inter-operation between proof systems. In particular, our translation keeps the mathematical statements intelligible. This translation has been implemented and allows the importation of the HOL Light basic library into Coq.

1 Introduction

The curse of Babel?

Proof-systems are software dedicated to the development of mechanically checked formal mathematics. Each such system comes with its own logical formalism, its own mathematical language, its own proof language and proof format, its own libraries. A consequence is that it is largely impossible to reuse a formal development of one system in another, at least not without a re-implementation requiring important amounts of human work and skills.

This situation is about as old as proof-systems themselves, has often been deplored and is mostly felt as a modern form of the curse of Babel.

On the other hand, if the large number of human languages sometimes hinders comprehension between people, it also gives them a broader set of means to express themselves. It is well known that many subtleties of an original text are often "lost in translation". A similar point can be made in the case of formal mathematics: certain formalisms and systems can allow smoother developments of, say, real analysis, while others will be more at ease with fields involving large combinatorial case analyzes.

For these reasons, automatic translation between proof-systems is a tempting and old idea. It has, however, been hindered by various theoretical and practical obstacles. We here describe a new attempt that opens new possibilities. The ideas underlying this work are:

-We focus on one particular case, the translation from HOL Light to Coq.

-This work is specific to this case, and builds upon a careful study of the logical formalisms of both systems and the way they are implemented. -In this particular case, we provide a good translation, in the following sense: the statements of the theorems translated from HOL Light remain intelligible and can be incorporated into further developments made in Coq.

Embedding Higher-Order Logic into Coq

As it is often the case when logic meets implementation, there are two aspects in this work:

1. The choice of logical embedding: in our case, statements and proofs of HOL Light have to be translated into counterparts in Coq's type theory. For instance, one often distinguishes between deep and shallow embeddings. The choice of this translation is central and will be discussed below. 2. The way to actually implement this translation. This will depend on issues like the way the two systems represent proofs, whether the translating function processes proof objects or proof scripts, etc. . .

Deep and shallow embeddings

In order to represent terms from one logical framework A inside another formalism B, we have two possible ways:

-A deep embedding: define data-types in B that represent types and terms of A; we can then define, inside B, what it means to be provable in A. -A shallow embedding: represent types and terms of A using their counterparts in B; this translation must preserve provability.

A deep embedding can ease things on the implementation side: we have access to the structure of the terms, and we can reason about them. Furthermore, the data types serve as a well-defined interface between the two systems. However, our ultimate aim is to obtain actual Coq theorems3 . For that, we concretely need a shallow embedding. In a previous work by F. Wiedijk [START_REF] Wiedijk | Encoding the HOL Light logic in Coq[END_REF], theorems from HOL Light were directly translated through a shallow encoding. Wiedijk observed that automation was difficult to perform that way. Furthermore, and although he used a shallow embedding, the theorems he obtained were still somewhat awkward in Coq. For instance, we would like to see the theorem ∀a, ∃b, a = b to be translated in Coq in forall (A:Type)(a:A), exists b, a = b whereas Wiedijk obtains forall (A:hol_type), hol_thm (hol''forall A (hol_Abs A hol''bool (fun (a:A)=> hol''exists A (hol_Abs hol''bool (fun (x:A)=> hol''eq A x a))))).

To avoid these pitfalls, we are going to obtain this shallow encoding going through a deep one. Frameworks like type theories allow to lift a deep embedding into a shallow one. This operation is called reflection from a proof theoretic point of view; through a proofs-as-programs perspective it can be understood as a compilation operation and corresponds to one of the two steps of normalization by evaluation (NbE) [START_REF] Berger | An inverse of the evaluation functional for typed lambda-calculus[END_REF]. In this work we adapt a previous formalization of NbE in Coq [START_REF] Garillot | Simple types in type theory: Deep and shallow encodings[END_REF].

To conclude, from HOL Light, we get deeply embedded terms; then we translate them into Coq theorems using a process similar to the computation part of normalization by evaluation.

Motivations and difficulties

Embedding the Higher-Order Logic into Coq means defining a model of this logical framework, and so proving its coherence. The confidence we can have about the HOL Light theorem prover is thus increased. And this is enforced by the ability we have to check in Coq the theorems that were proved in HOL Light.

When translating theorems from HOL Light to Coq, we will have to take into account the differences between the two systems: as they often make different choices in the way a same mathematical corpus is formalized, one can therefore fear that a translated theorem is difficult to reuse in the target system, or that its statement becomes obscured.

Finally, one expects such a translation to be robust to changes in both proofsystems, and to be as efficient as possible in terms of time and memory consumption.

Related work

Interaction between HOL and Coq There already have been some attempts to share proofs between HOL systems and Coq, some of which are being developed now. One solution is to rely on an independent tool that will, at the same time, check the proof and perform the translation [START_REF] Denney | A prototype proof translator from hol to coq[END_REF][START_REF] Dedukti | a universal proof checker[END_REF]. Closer to our approach, it is conceivable to transform a theorem in the HOL system into a theorem in Coq, and check it in Coq, using its HOL proof as a guideline. F. Wiedijk [START_REF] Wiedijk | Encoding the HOL Light logic in Coq[END_REF] observed that directly using a shallow encoding was hard to automate and resulted in rather unintelligible theorems in Coq.

Recording and exporting HOL proofs Efficient systems to record and export HOL proofs have already been developed, both for the HOL prover [START_REF] Wong | Recording and checking HOL proofs[END_REF] and for HOL Light [START_REF] Obua | Importing HOL into Isabelle/HOL[END_REF][START_REF] Hurd | OpenTheory: Package Management for Higher Order Logic Theories[END_REF]. These works pursue the same motivations as ours: to import HOL proofs into a theorem prover. Since Obua's tool [START_REF] Obua | Importing HOL into Isabelle/HOL[END_REF] is far more stable and easier for a direct exportation to Coq, we reused his code on the HOL Light side (proof recording), and changed the exportation side to a Coq format. These changes are now distributed with the development version of HOL Light4 .

Outlines

In the next section, we see the main characteristics of HOL Light and Coq that serve our work. Section 3 is dedicated to the major part of our work: constructing a deep embedding of the HOL Light logic into Coq, that is defining data structures that represent types, terms and derivations of HOL Light. To relate this to our main goal, we have to work on two levels:

-Upstream: we record and export HOL Light proofs into this encoding.

-Downstream: inside Coq, we construct a lifting from the deep embedding to a shallow embedding. Each HOL Light construction is mapped to its Coq counterpart. Besides, we prove that each time we have a Coq object representing a correct HOL Light derivation, its translation is a correct Coq theorem (Section 4).

This way, from a proof tree imported from HOL Light, we can reconstruct a theorem statement and its proof, using reflection. We develop some aspects of the way to obtain reasonable performances in Section 5, thus obtaining the results described in Section 6. Finally, we discuss our approach and its perspectives.

HOL Light and Coq

HOL Light [START_REF] Harrison | HOL Light: A tutorial introduction[END_REF] and Coq [START_REF] Barras | The Coq proof assistant: reference manual[END_REF] are two interactive theorem provers written in OCaml [START_REF] Leroy | The OCaml Programming Language[END_REF]. Although the ancestries of Coq and HOL Light can both be traced back to LCF, there are important differences, between the logical formalisms as well as in the way they are implemented. For obvious matters of space, we here do not give a complete description of the two systems, but underline differences which are crucial for the translation.

A more detailed comparison between HOL [START_REF] Gordon | Introduction to HOL: A theorem proving environment for higher order logic[END_REF] and Coq has been established in [START_REF] Zammit | A comparative study of Coq and HOL[END_REF] and enhanced in [START_REF] Denney | A prototype proof translator from hol to coq[END_REF]. These studies also apply to HOL Light, which mainly differs from HOL by its smaller implementation.

The status of proofs

Proof systems like Coq and HOL Light share the same goal: to construct a formal proof. However, the status of these constructions is different in the two systems. This difference is directly related to the two formalisms.

HOL Light implements a variant of Church's Higher-Order Logic. A proof is a derivation in natural deduction. In the example below, Γ and ∆ are sets of hypotheses; s, t, u and x are objects of some well chosen types:

Γ ⊢ s = t ∆ ⊢ t = u Γ ∪ ∆ ⊢ s = u trans ⊢ x = x refl Γ ∪ ∆ ⊢ s(x) = u(x) mk comb
While such a derivation has an obvious tree structure, it is not constructed as such in the system's memory. HOL Light represents statements like Γ ⊢ s = t as objects of an ML abstract data type thm. The fact that this data type is abstract is the key to the system's safety5 : the only way to construct objects of type thm are well-understood primitive tactics corresponding to primitive inference rules. Thus, if a statement Γ ⊢ P can be represented in thm, it is indeed a theorem.

Coq implements a Type Theory where proofs are objects of the formalism6 . More precisely, "being a proof of P " is identical with "being of type P ", and as a consequence, the statements of the theory are of the form Γ ⊢ t : P .

This results in a very different architecture and safety model:

-The type-checker is the safety critical part of the system, its trusted computing base. -Theorems are constants: the statement is the type and the body is the proof.

Proofs are thus kept in the system's memory and can be re-checked.

Consequences Since Coq keeps proof-objects while HOL Light does not, we need to build these objects at some point in the translation process. The translated proofs can have a critical size. We will see below that this requires special care.

Computations and equality

In both formalisms, the objects are strongly normalizing typed λ-terms. The way normalization is performed is very different however. Coq allows to type actual functional programs: its objects include a purely functional and terminating kernel of ML. This leads to some computation over terms, and a notion of convertibility between β-equivalent terms. In HOL Light, no computation is performed, and two β-equivalent terms are only provably equal. Let us take an example.

In Coq, addition over unary natural numbers is defined as the usual program: Such programs come with a notion of computation, which defines a notion of intentional equality. In this case, extended β-reduction yields (with some syntactic sugar) 2 + 2 ⊲ β 4 and thus 2 + 2 = c 4.

Like in all Martin-Lf type theories, these, possibly complex, computations are taken into account in the formalism by the specific conversion rule:

(Conv) Γ ⊢ t : A Γ ⊢ B : s Γ ⊢ t : B (if A = c B)
As a consequence, computations are omitted in the proof; for instance the propositions even(2 + 2) and even(4) have exactly the same proofs.

Another consequence is that Coq and similar type theories need a notion of propositional equality which is distinct from the computational relation = c .

In HOL Light, on the other hand, one will prove the existence of addition, that is of a function verifying the properties 0 + x = x and S(x) + y = S(x + y). The equality predicate is the way to construct atomic propositions, and all constructions (∧, ∨, ⇒ connectors, quantifiers. . . ) are defined through combinations of equality and, in some cases, the ε-operator.

HOL Light's equality has specific rules corresponding to reflexivity, transitivity, extentionality, β and η-equivalence.

Consequences On the one hand, in Coq, the length of a proof can be reduced by maximizing the computational part, which does not appear in proofs. This principle is called computational reflection. In our development, proofs of the theorems that are imported from HOL Light use these computational capabilities of Coq.

On the other hand, in HOL Light, the absence of computation leads to big proofs. The advantage is that we avoid the implementation of a β-reduction over our representation of HOL Light's λ-terms and a conversion rule, really simplifying de facto proof checking.

Treatment of constants

Constants, that is the ability to have definitions, are essential to any mathematical development. Precisely because of the different statuses of equality, constants are treated differently in the two systems.

In Coq, constants are treated through the computational equality and the conversion rule. Whenever a constant is defined:

Definition c : A := body .
a new object c of type A is added to the environment, and the computational equality is extended by c = c body.

In HOL Light, constant unfolding is explicitly handled by the equality predicate. The corresponding definition will also yield an object c of type A, together with a theorem stating that c = body.

Consequences The fact that constants in HOL Light are unfolded only by invoking a specific theorem will turn out to be very convenient: it will allow us to map specific constants to previously defined Coq objects (see Section 4.3).

Classical logic

Whereas Coq's intentional type theory is constructive, HOL Light's logic is:

-Extensional: the η-equivalence is assumed (and functional extensionality can be deduced from it in HOL Light). -Classical: propositions are actually boolean terms; thus propositional extensionality is true by definition; furthermore the axiom of choice is assumed via the introduction of a primitive Hilbert ε-operator.

Consequences Given the fact that the classical reasoning is deeply embedded in HOL Light logic, there seems to be no alternative but to assume corresponding axioms in Coq (excluded middle, choice operator, extentionality). Indeed, we need to apply them when proving the coherence of HOL Light in Coq.

Type definitions

In Coq, type definitions are just regular definitions or inductive definitions. In HOL, there is no primitive notion of induction, and since types have a different status than terms, type definitions have to be handled specifically.

A user can define new types in different ways involving facilities such as induction, but they all rely on one mechanism: the schema of specification. This is implemented by the primitive rule new_basic_type_definition, which, given a property P : A → bool, a term x : A such that ⊢ P x holds, defines the type B = {y : A|P y}, and two constants (in the sense of section 2.3): the canonical injection from B to A and the injection from A to B whose behavior is specified only for elements y such that P y holds.

Consequences All the types in HOL Light are inhabited, since the base types are inhabited and a type definition has to be inhabited because we require ⊢ P x. This is useful to define the ε operator in a proper way without a condition of non-emptiness on the type.

Deep embedding: representing Higher-Order Logic in Coq

In this section, we represent Higher-Order Logic in Coq. The main originality is the computational definition of deduction at the end of the section. The basic definitions are quite standard, but some care is needed in order to make the later developments tractable and to keep memory consumption as low as possible as well as the computations efficient enough. In particular, it is mandatory to have explicit definitions.

Our encoding uses the SSReflect tactics and libraries package developed by G. Gonthier et al. [START_REF] Gonthier | A Small Scale Reflection Extension for the Coq system[END_REF], but the level of details of this paper does not allow us to make clear how crucial this is.

Types and terms

Names We need names for variables and definitions both for types and terms. These names have to be in an infinite countable set over which equality is decidable. For efficiency reasons, we chose positive, the Coq representation of binary natural numbers greater than 1.

In the rest of the paper, idT, defT, idV and defV, respectively representing types variables, types constants, terms variables and terms constants, stand for positive.

Types For types, we need variables and definitions, and we give a specific status to the two primitive definitions of HOL Light: bool and the functional arrow. A previously defined type is accessed through its name and the list of its arguments. Terms Terms are defined straightforwardly as an inductive type. For bound variables, we use a locally nameless representation [START_REF] Aydemir | Engineering formal metatheory[END_REF], which is simpler to reason about than a named representation. As for types, we distinguish some primitive term definitions: the equality, the ε choice operator, and the logical connectives. We group them together under the type cst, and obtain for terms this definition:

Inductive term : Type := | Dbr : nat → term | Var : idV → type → term | Cst : cst → term | Def : defV → type → term | App : term → term → term | Abs : type → term → term .
Typing This is our first use of computational reflection. Rather than defining typing judgments as an inductive relation, we directly define [START_REF] Garillot | Simple types in type theory: Deep and shallow encodings[END_REF] a typing algorithm. Given a De Bruijn context (a list of types) g and a term t, the function infer returns the type of t under the context g if it exists, and fails otherwise. wt g t A means that this term has type A under g, and is just a shortcut for "infer g t returns A". Since we consider simply typed terms, the definition of infer is easy.

Derivations

We now define HOL Light's logical framework. Typically, Coq's induction process and dependant types are well-suited to represent such judgments. Here is an extract of the inductive data-type that represents HOL Light derivations): They would be too verbose and difficult to build (for Drefl, how to prove wt nil t A?). Obua [START_REF] Obua | Importing HOL into Isabelle/HOL[END_REF] notices that it is sufficient to build a far more compact skeleton of the tree. This skeleton carries only minimal information; typically which inference rules have been used.

Following his code, we record proofs in HOL Light using an ML recursive type that represents this skeleton (which means this structure uses no dependent types anymore). We then export it straightforwardly into its twin Coq inductive type:

Inductive proof : Type := | Prefl : term → proof | Pconj : proof → proof → proof | Pconjunct1 : proof → proof | Pconjunct2 : proof → proof | ...

These twin OCaml and Coq types thus establish the bridge between HOL Light and Coq.

This structure is typed too loosely to guarantee the correctness of the derivation. Some objects of type proof do not correspond to actual proofs. For instance, Pconjunct1 stands for the elimination rule of ∧ on the left. Its argument should be a proof of a theorem that looks like Γ ⊢ A ∧ B, but this is not enforced in the proof inductive type.

However, a skeleton is sufficient to reconstruct a complete derivation when it exists, by making the necessary verifications. This is the job of the proof2deriv function:

-If p is a well-formed proof, then proof2deriv p returns h and t, and we can establish that deriv h t stands (this is lemma proof2deriv_correct). -If not, proof2deriv fails.

Once more computational reflection is used to deduce deriv h t from a proof.

In the previous section, we show how to export HOL Light proofs and obtain in Coq objects of type deriv h t for a certain h and t, that is to say deeply written theorems. To interact with Coq theorems, we want to have a shallow reading of these theorems. That is why we define a translation from deep to shallow. This translation has already been implemented in [START_REF] Garillot | Simple types in type theory: Deep and shallow encodings[END_REF] for a simply typed λ-calculus with only named variables. Here it is trickier with De Bruijn indices and definitions.

General idea

For the moment, we suppose given an interpretation function I to interpret variables and definitions names. Its meaning is detailed in Section 4.3.

We first define [•] I , a translation function on types, that maps, for instance, Bool to Prop and the arrow to the arrow of Coq (see its precise typing below). We then define | • | I , a translation function on terms, that respects their types. Informally, it means that when a term t has type T , then |t| I belongs to [T ] I :

if Γ ⊢ t : T then |t| I ∈ [T ] I

Implementation

It is important for all the types in HOL Light to be inhabited, as we noticed in Section 2.5. We now cope with this by stating that the translation of a type must be an inhabited Type. Inhabited Types can be represented by a record: Definitions The interpretation of definitions is a key point to preserve the intelligibility of theorems. Interpretation for types and terms definitions are respectively defined by: Definition type_definition_tr := defT → list type_translation → type_translation . Definition term_definition_tr := defV → forall ( A : type ) , tr_type I A .

Imagine we have a HOL Light term t bringing into play objects of type num, the type for natural numbers defined with zero (_0) and successor (SUC). If we apply sem_term to t with an object of type type_definition_tr that maps (num,[]) to nat and a object of type term_definition_tr that maps (_0,num) to O and (SUC,num→num) to S, we obtain a Coq term that corresponds to t, but it is a standard Coq theorem, and it would have been written that way directly in Coq.

Besides, this process is fully flexible: if instead of nat, we map num to N, the Coq type for binary natural numbers, then we get the same term in this different formalism of naturals. Notation In the remaining of the article, the interpretation functions are still abbreviated as I.

Adequacy of derivations w.r.t. semantics

We can now establish that this translation applied to correct HOL Light derivations produce correct Coq theorems. By a correct Coq theorem, we mean a term that is locally closed, has type Bool, and whose translation is a correct Coq proposition whatever the interpretation functions might be:

Definition has_sem ( t : term ) : Prop := match sem_term nil t with | Some ( existT Bool evT ) ⇒ forall I , evT I | _ ⇒ False end .

We can establish the following theorem:

Theorem sem_deriv : forall ( h : hyp_set ) ( t : term ) , deriv h t → forall I , sem_hyp I h → has_sem I t .

where sem_hyp I h checks that has_sem I holds for each term of h. Since has_sem is a function, the proofs of the translated theorems are computationally reflexive again.

Conclusion of parts 3 and 4

When a theorem is being proved in HOL Light, its proof is recorded. It can be exported as an object p: proof that we expect to be correct (because it comes from a HOL Light proof). Given this object, we define a set of hypotheses h and a conclusion t with proof2deriv. proof2deriv_correct gives a computationally reflexive proof that these objects correspond to a derivation. If h is empty, we can apply has_sem to t, to get the Coq version of this theorem (which is very close to one would have written directly in Coq), and we have a computationally reflexive proof of this theorem applying sem_deriv.

Improving efficiency

As such this process allows, in principle, to import HOL Light theorems and to check them. . . In practice, it would take too much time and use too much memory. We stopped when the exported files reached 200 Gb; Obua reports a similar experience [START_REF] Obua | Importing HOL into Isabelle/HOL[END_REF].

Sharing

Proofs Obua uses the natural sharing for proofs that comes from the user: when a piece of proof is used more than twice, it is shared. This sharing is not optimal, and it depends on the user's implementation, but it is very simple, it does not need too much memory (using a hash-table to perform hash-consing on proofs would really increase the memory consumption), and it is sufficient to considerably reduce the size of the exported files. In Coq, this sharing is kept by adding one constructor to the inductive type proof:

Inductive proof : Type := |...| Poracle : forall h t , deriv h t → proof .

For each proof coming from HOL Light, the corresponding derivation is immediately computed. It can be called in a following proof thanks to the constructor Poracle.

Types and terms We share types and terms using standard hash-consing presented in [START_REF] Filliâtre | Type-safe modular hash-consing[END_REF].

Opaque proofs

In Coq, even with sharing, objects of type proof can be arbitrary big. Our idea to avoid keeping them in memory is to:

distribute the theorems coming from HOL Light into separate files, and when compiling the (n + 1) th file, load only the statements of the theorems of the first n files, but not the opaque proofs (this can be done with the option -dont-load-proofs of Coq's compiler); -put the objects of type proof inside Coq opaque proofs.

Computation

In addition to its internal reduction mechanism, Coq includes an optimized bytecode-based virtual machine to evaluate terms. It is less tunable, but rather more efficient that the internal mechanism. It is well suited for the full evaluation required by computational reflection.

Results

Implementation

Our implementation is free software and can be found online [START_REF]Our implementation[END_REF]. Looking back at the two main objectives of this work, efficiency and usability, we observe some limitations to the first goal, while the second one is rather fulfilled.

Tests

The tests were realized on a virtual machine that is installed on a DELL server PowerEdge 2950, with 2 processors Intel Xeon E5405 (quad-core, 2GHz) and 8 Gb RAM, with CentOS (64 bits). We are able to import and to check in Coq HOL Light proofs from:

-The standard library: what is loaded by default when launching HOL Light.

-The Model directory: a proof of consistency and soundness of HOL Light in HOL Light [START_REF] Harrison | Towards self-verification of HOL Light[END_REF] (which, again, enforces the confidence in HOL Light). -The elementary linear algebra tools developed in Multivariate/vectors.ml.

The results are summed up in Table 1. For each benchmark, we report the number of theorems that were exported, the number of lemmas generated by sharing, the time to interpret theorems and record their proofs in HOL Light, the time to export theorems to Coq, the time of compilation in Coq, the size of the generated Coq files, the maximal virtual memory used by OCaml, and the maximal virtual memory used by Coq. In the next two paragraphs, we analyze the origins of compilation time and memory consumption, and present some possible solutions. Time and memory in Coq Our proof sharing system has the major drawback to lead to a complete blow-up of the number of exported statements, as the first columns of Table 1 attest. Moreover, all these statements need to be kept in memory because all the theorems depend on one another.

The time of Coq's compilation thus cannot be less than quadratic in the number of Coq files, since compiling the (n + 1) th file imports files 1 to n. The other operations that are expensive in time are:

the parsing of the proof objects; -the evaluation of the computationally reflexive proofs. Concerning this last item, it is important to notice that Coq's virtual machine can run such a big computation. Computational reflection sounds thus a good way to import proofs, at least in Coq.

In other words: sharing limits the memory consumed by proof objects, but the resulting number of statements then becomes a problem. The compilation time is not too restrictive, since the incoming theorems have to be compiled once for all. Moreover, it requires far less human work to automatically export some theorems and compile it with our tool than to prove them from scratch in Coq. Memory is a large limitation for a user though, since he or she needs to import all the Coq files even to use only the last theorem. It would be convenient to be able not to load the intermediary lemmas, but it does not seem possible with our present proof objects implementation.

Memory in OCaml

The fact that proofs are kept is not the only limiting factor for OCaml's memory: during exportation, we create big hash-tables to perform hash-consing and to remember theorem statements. If we keep the present proof format, we definitely would have to reduce the extra-objects we construct for exportation.

Conclusion Now that we have something reliable for a rather simple proof format, a next step is to switch to a more compact format such as the ones presented in [START_REF] Berghofer | Proof terms for simply typed higher order logic[END_REF] or [START_REF] Hurd | OpenTheory: Package Management for Higher Order Logic Theories[END_REF].

Usability

We now give an example from integer arithmetic of an interaction between HOL Light and Coq's theorems. We map HOL Light's definitions as stated in Table 2.

Given the usual notation to say "a divides b":

Notation " a | b " := ( Nmod b a = 0) .

we import the theorem MOD_EQ_0 from HOL Light: The proof is only five lines long, because it is straightforward from hollight_MOD_EQ_0_thm. As Coq's standard library does not have any lemmas about division and modulo in N, proving this statement from scratch would certainly not be trivial.

Conclusion and future work

The new way to translate theorems and proofs from HOL Light to Coq presented in this paper fills the gap between those two interactive theorem provers. We solve both theoretical and practical problems coming from the different frameworks the two provers are based on. Relying on the computational power of Coq (reflection), our translation is both able to restore theorems meanings in Coq and give a small proof of them. The implementation scales up to non trivial libraries. We are limited by usual performance issues, but at a much later point. To manage to import even larger developments, like the geometric properties used in the Flyspeck project [START_REF]The Flyspeck project[END_REF], we need to reduce compilation time and virtual memory used. This may be possible by improving the proof format and changing the way we perform sharing.

Possible future directions include:

translating HOL proofs to other systems with rich computation capabilities; -integrating other external tools in Coq, such as other interactive theorem provers or automatic theorem provers, without compromising its soundness.

Fixpoint

  plus ( n m : nat ) : nat := match n with | O = > m | S p = > S ( plus p m ) end .

  Inductive type : Type := | TVar : idT → type | Bool : type | Arrow : type → type → type | TDef : defT → list_type → type with list_type : Type := | Tnil : list_type | Tcons : type → list_type → list_type .

  Inductive deriv : hyp_set → term → Prop := | Drefl : forall t A , wt nil t A → deriv hyp_empty ( heq A t t ) | Dconj : forall h1 h2 a b , deriv h1 a → deriv h2 b → deriv ( hyp_union h1 h2 ) ( a hand b ) | Dconj1 : forall h a b , deriv h ( a hand b ) → deriv h a | Dconj2 : forall h a b , deriv h ( a hand b ) → deriv h b | ... It would however be impractical to have HOL Light generate such derivations.

  Record type_translation : Type := mkTT { ttrans : > Type ; tinhab : ttrans }. The translation function [•] I , a.k.a. tr_type, maps a HOL type to a type_translation: tr_type : forall I , type → type_translation The translation function | • | I , a.k.a. sem_term, is as a refinement of the typing function infer (see Section 3.1). In addition to typing a term, it gives its Coq translation (note that its definition is eased by the use of dependant types): sem_term : context → term → option { ty : type & forall I , tr_type I ty } 4.3 The interpretation functions Variables We have three kinds of variables to interpret: type variables, named term variables and De Bruijn indices. We map each of them to Coq objects with respect to their types.

  Theorem h olli ght_M OD_E Q_0_ thm : forall x x0 : N , x0 <> 0 → x0 | x = ( exists a : N , x = a * x0 ) .and combine it with one Coq's theorem using tactics to prove:Lemma div_mult : forall a b , a <> 0 → a | b → forall k , a | k * b .

Table 1 .

 1 Benchmarking the standard library and Model.

	Bench.	Number Theorems Lemmas Rec.	Time Exp. Comp. H.D.D. Virt. OCaml Virt. Coq Memory
	Stdlib	1,726	195,317 2 min 30 6 min 30 10h 218 Mb	1.8 Gb	4.5 Gb
	Model	2,121	322,428 6 min 30 29 min 44h 372 Mb	5.0 Gb	7.6 Gb
	Vectors	2,606	338,087 6 min 30 21 min 39h 329 Mb	3.0 Gb	7.5 Gb

Table 2 .

 2 Mapping of definitions. In Coq, N is the type of binary natural numbers, and is defined in NArith. In HOL Light, num is the type of unary natural numbers.

	HOL Light	num	+	*	DIV	MOD
	Coq	N	Nplus Nmult Ndiv Nmod

If John Harrison provides us with, say, Wiles' proof of Fermat's theorem in HOL Light, we want to translate it to the "real" Coq formulation of this famous result, and not the theorem "Fermat's theorem as stated in HOL is provable in HOL".

The development version of HOL Light is currently available at http://hol-light. googlecode.com/svn/trunk

And to the safety of related systems (LCF, HOL).

This is one aspect of the Curry-Howard isomorphism; another aspect is that the Type Theory is constructive, but this point is less central here.

Acknowledgments We are particularly grateful to Carlos Simpson who suggested the use of normalization by evaluation for translating HOL proofs to Coq and provided the stimulus for this work. We also thank John Harrison and Steven Obua who provided useful help with the code of HOL Light. We finally thank the anonymous reviewers for their useful remarks.


Chantal Keller

❦❡••❡r❅•✐①✳

Thorsten Altenkirch

♥ ♦ Tt✳❛❝✳✉❦

Hereditary Substitutions for Simple Types, Formalized

Keywords: Hereditary substitutions, Type Theory, normalizer, decidability of βη-equality

We analyze a normalization function for the simply typed λcalculus based on hereditary substitutions, a technique developed by Pfenning et al. The normalizer is implemented in ❆❣❞❛, a total language where all programs terminate. It requires no termination proof since it is structurally recursive which is recognized by ❆❣❞❛'s termination checker. Using ❆❣❞❛ as an interactive theorem prover we establish that our normalization function precisely identifies βη-equivalent terms and hence can be used to decide βηequality. An interesting feature of this approach is that it is clear from the construction that βη-equality is primitive recursive.

Introduction

Among the different ways to establish the decidability of some equality for λ-calculi (e.g. see [START_REF] Altenkirch | Tait in one big step[END_REF][START_REF] Pierce | Types and programming languages[END_REF]), it seems natural in a programming point of view to give a normalization function, and to prove that it computes a canonical form for any term. This approach is well-suited for an implementation, and it thus becomes important to be able to analyze it in order to prove, for instance, termination of the process.

In this paper, we define a normalizer that β-reduces and ηexpands simply typed λ-terms. We use it to establish a formal verification of the decidability of the βη-equality for this calculus.

The normalizer and the proofs are implemented in ❆❣❞❛ [START_REF]❤tt♣✿✴✴✇✐❦✐✳♣♦rt❛•✳❝❤❛•♠❡rs✳s❡✴❛❣❞❛[END_REF][START_REF] Norell | Towards a Practical Programming Language Based on Dependent Type Theory[END_REF].

❆❣❞❛ is a programming language with dependent types. We exploit this property in two ways. First, the typing system is powerful enough to ensure some non trivial properties of the functions defined in this language. Secondly, we can use ❆❣❞❛ as an interactive theorem prover. Thus, ❆❣❞❛ is our metalanguage all along the paper. The source code can be found online [START_REF]The decidability of the βη-equivalence using hereditary substitutions[END_REF].

which are adapted to a formal development since closed terms have a unique form (Section 2.2).

The normalizer implements hereditary substitutions (Section 3) [START_REF] Watkins | A Concurrent Logical Framework: The Propositional Fragment[END_REF], which preserve canonical forms by substituting and reducing the redices that can appear from substitution at the same time. An important aspect of hereditary substitution is that it can be defined using structural induction; hence, it can be implemented in total Type Theory without any termination proof. In our development, ❆❣❞❛'s termination checker is able to check that the normalizer does terminate (Section 3.4).

We prove the completeness (Section 4) and the soundness (Section 5) of our normalizer, in order to conclude that it decides the βη-equivalence of two terms.

We finally discuss related work (Section 6) and conclude (Section 7).

The simply typed λ-calculus

We start by introducing our calculus. Its particularity is that we only define well typed terms: terms are objects of an inductive family parameterized by types. This presentation of the simply typed λ-calculus is formally described in [START_REF] Altenkirch | Monadic Presentations of Lambda Terms Using Generalized Inductive Types[END_REF], for instance. It is very convenient to use in ❆❣❞❛, which supports dependent type programming and inductive declarations.

The calculus

The set of types (❚②) is defined by a simple inductive definition: ❞❛t❛ ❚② : ❙❡t ✇❤❡r❡

• : ❚② ❴⇒❴ : ❚② → ❚② → ❚② Inductive definitions are introduced in ❆❣❞❛ with the keywords ❞❛t❛ and ✇❤❡r❡. Each following line defines a new constructor of this inductive type, giving its type. ❙❡t is ❆❣❞❛'s type of types, and the ❴•❴ notation is used to define mixfix operators.

For terms, we use (typed) De Bruijn indices to represent variables [START_REF] De Bruijn | Lambda Calculus Notation with Nameless Dummies: a Tool for Automatic Formula Manipulation With Application to the Church-Rosser Theorem[END_REF]. We thus need a context that maps each free variable to a type. Since we do not have to store names, a context (❈♦♥) can be represented as a list of types:

❞❛t❛ ❈♦♥ : ❙❡t ✇❤❡r❡ ε : ❈♦♥ , : ❈♦♥ → ❚② → ❈♦♥
As explained above, the sets of variables (❱❛r) and terms (❚♠) are objects of an inductive family indexed by types and contexts:

❞❛t❛ ❱❛r : ❈♦♥ → ❚② → ❙❡t ✇❤❡r❡ ✈③ : ❢♦r❛•• {Γ σ } → ❱❛r (Γ, σ) σ ✈s : ❢♦r❛•• {τ Γ σ } → ❱❛r Γ σ → ❱❛r (Γ, τ ) σ ❞❛t❛ ❚♠ : ❈♦♥ → ❚② → ❙❡t ✇❤❡r❡ ✈❛r : ❢♦r❛•• {Γ σ } → ❱❛r Γ σ → ❚♠ Γ σ Λ : ❢♦r❛•• {Γ σ τ } → ❚♠ (Γ, σ) τ → ❚♠ Γ (σ ⇒ τ ) ❛♣♣ : ❢♦r❛•• {Γ σ τ } → ❚♠ Γ (σ ⇒ τ ) → ❚♠ Γ σ → ❚♠ Γ τ
In ❆❣❞❛, curly brackets surround the implicit arguments of a constructor or a function. Usually, these arguments can be automatically infered by ❆❣❞❛, so they do not have to be given when the constructor or the function is applied. For a matter of space, in the paper, we skip them also in type declarations when it does not lead to any ambiguity: we consider that any symbol appearing in the type of a constructor or a function that is not previously defined is an implicit argument. For instance, the type of ❛♣♣ would now be written:

❛♣♣ : ❚♠ Γ (σ ⇒ τ ) → ❚♠ Γ σ → ❚♠ Γ τ 2.

Working with De Bruijn indices

De Bruijn indices have the nice property to give a unique representation to any closed term, which makes them easy to implement. They are not natural to use for a human being, though. For clarity, this section presents some tools to work with De Bruijn indices in our calculus.

Vocabulary

First, we use a rigid vocabulary all along the paper:

• If ①✿ ❱❛r Γ σ, we call ① an index.

• If ①✿ ❱❛r Γ σ, we say that ① is parameterized by Γ.

• We say that ① and ② represent the same variable if they would have the same name in a named representation, but are not parameterized by the same context.

For instance, the λ-term:

λf.λz.f ((λx.f x) z)
is encoded in ❆❣❞❛ by Λ (Λ (❛♣♣ (✈❛r (✈s ✈③)) (❛♣♣ (Λ (❛♣♣ (✈❛r (✈s (✈s ✈③))) (✈❛r ✈③))) (✈❛r ✈③)))) In this term, the two occurrences of ✈❛r ✈③ do not represent the same variable (it can be x or z), whereas ✈s ✈③ and ✈s (✈s ✈③) do represent the same variable (f ).

Removal from a context

In our calculus, many constructions rely on removing an index parameterized by a context Γ from Γ. This is made possible by the following function:

❴✲❴ : {σ : ❚②} → (Γ : ❈♦♥) → ❱❛r Γ σ → ❈♦♥ ε ✲ () (Γ, σ) ✲ ✈③ = Γ (Γ, τ ) ✲ (✈s ①) = (Γ ✲ ①), τ
In ❆❣❞❛, functions are defined in a Haskell-like syntax: the first line gives the type of the function, and the other lines give its definition with (possibly) a case analysis. The () notation is useful to discriminate absurd cases: here, it is impossible for an index to be parameterized by the empty context ε.

Weakening

In a calculus with contexts and De Bruijn indices, weakening is also a very standard construction: it is often used to avoid capture. It means adding extra-information in a context parameterizing an index:

✇❦✈ : (① : ❱❛r Γ σ) → ❱❛r (Γ ✲ ①) τ → ❱❛r Γ τ ✇❦✈ ✈③ ② = ✈s ② ✇❦✈ (✈s ①) ✈③ = ✈③ ✇❦✈ (✈s ①) (✈s ②) = ✈s (✇❦✈ ① ②) 2.

Treatment of variable equality

We established in section 2.2.1 that the same index can represent different variables and, conversely, the same variable can be represented by different indices. Comparing variables is thus non trivial.

We introduce a predicate ❊q❱ specifying if two indices parameterized by the same context represent the same variable or not. Its return value is more precise than a boolean: it does not only answer "yes" or "no", but also gives additional information to justify it.

Its definition is the following one:

❞❛t❛ ❊q❱ : ❱❛r Γ σ → ❱❛r Γ τ → ❙❡t ✇❤❡r❡ s❛♠❡ : {① : ❱❛r Γ σ } → ❊q❱ ① ① ❞✐✛ : (① : ❱❛r Γ σ) → (② : ❱❛r (Γ ✲ ①) τ ) → ❊q❱ ① (✇❦✈ ① ②)
It relies on two properties:

1. The only way for ① and ② to represent the same variable is to be equal.

2. If ① and ② do not represent the same variable, then there exists an index ③ such that ① ≡ ✇❦✈ ② ③ (≡ stands for Leibniz equality, with the three usual functions r❡✢, s②♠ and tr❛♥s). The intuition behind this property is that if ① and ② do not represent the same variable, then ① "exists" in Γ ✲ ②: this is the index ③. ① is thus the weakening of ③ when ② is added to the context. To summarize, for any variables ① and ②, ❊q❱ ① ② is inhabited by:

• s❛♠❡ if ① ≡ ②; • ❞✐✛ ① ③ if ② ≡ ✇❦✈ ① ③.
① ②)) | (❞✐✛ ① ②) = ❞✐✛ (✈s ①) (✈s ②)
The ✇✐t❤ construction allows pattern matching on a recursively computed result. Dot patterns (✳① for instance) tag ❆❣❞❛ terms whose construction is constrained by the value of the predicate.

Term weakening

Weakening is also defined for terms, if we add an index into the De Bruijn context parameterizing them:

✇❦❚♠ : (① : ❱❛r Γ σ) → ❚♠ (Γ ✲ ①) τ → ❚♠ Γ τ ✇❦❚♠ ① (✈❛r ✈) = ✈❛r (✇❦✈ ① ✈) ✇❦❚♠ ① (Λ t) = Λ (✇❦❚♠ (✈s ①) t) ✇❦❚♠ ① (❛♣♣ t1 t2) = ❛♣♣ (✇❦❚♠ ① t1) (✇❦❚♠ ① t2) 2.

The substitution function

The substitution function substitutes all occurrences of a free variable ① in some term t by another term ✉. The type we give to the substitution function is:

(t : ❚♠ Γ τ ) → (① : ❱❛r Γ σ) → (✉ : ❚♠ (Γ ✲ ①) σ) → ❚♠ (Γ ✲ ①) τ .
❆❣❞❛'s typing ensures two fundamental properties of such a substitution:

1. Substitution is type preserving: since ① has the same type (σ) as ✉, the type of t (τ ) is preserved.

2. Since the result is parameterized by Γ ✲ ①, we know that ① does not appear free in it. Variable equality defined in section 2.2.4 plays a main role in substitution. Indeed, in the case where t is an index ②, we need to know whether ① and ② represent the same variable or not.

We define the substitution for variables:

s✉❜st❱❛r : ❱❛r Γ τ → (① : ❱❛r Γ σ) → ❚♠ (Γ ✲ ①) σ → ❚♠ (Γ ✲ ①) τ s✉❜st❱❛r ✈ ① ✉ ✇✐t❤ ❡q ① ✈ s✉❜st❱❛r ✈ ✳✈ ✉ | s❛♠❡ = ✉ s✉❜st❱❛r . (✇❦✈ ✈ ①) ✳✈ ✉ | ❞✐✛ ✈ ① = ✈❛r ①
and for terms:

s✉❜st : ❚♠ Γ τ → (① : ❱❛r Γ σ) → ❚♠ (Γ ✲ ①) σ → ❚♠ (Γ ✲ ①) τ s✉❜st (✈❛r ✈) ① ✉ = s✉❜st❱❛r ✈ ① ✉ s✉❜st (Λ t) ① ✉ = Λ (s✉❜st t (✈s ①) (✇❦❚♠ ✈③ ✉)) s✉❜st (❛♣♣ t1 t2) ① ✉ = ❛♣♣ (s✉❜st t1 ① ✉) (s✉❜st t2 ① ✉) 2.

Convertibility

The conversion relation we consider in this paper is the βηequivalence (βη✲≡), defined as an inductive predicate:

❞❛t❛ ❴βη✲≡❴ : ❚♠ Γ σ → ❚♠ Γ σ → ❙❡t ✇❤❡r❡ ❜r❡✢ : {t : ❚♠ Γ σ } → t βη✲≡ t ❜s②♠ : t1 βη✲≡ t2 → t2 βη✲≡ t1 ❜tr❛♥s : t1 βη✲≡ t2 → t2 βη✲≡ t3 → t1 βη✲≡ t3 ❝♦♥❣Λ : t1 βη✲≡ t2 → Λ t1 βη✲≡ Λ t2 ❝♦♥❣❆♣♣ : t1 βη✲≡ t2 → ✉1 βη✲≡ ✉2 → ❛♣♣ t1 ✉1 βη✲≡ ❛♣♣ t2 ✉2 ❜❡t❛ : ❛♣♣ (Λ t) ✉ βη✲≡ s✉❜st t ✈③ ✉ ❡t❛ : Λ (❛♣♣ (✇❦❚♠ ✈③ t) (✈❛r ✈③)) βη✲≡ t
It is an equivalence (❜r❡✢, ❜s②♠ and ❜tr❛♥s) that is congruent with the constructors of λ-terms (❝♦♥❣Λ and ❝♦♥❣❆♣♣), and that identifies terms differing from one step of β-reduction (❜❡t❛) or one step of η-expansion (❡t❛).

Normalization and hereditary substitutions

We recall our goal is to show that the conversion relation we have just defined is decidable. We are going to establish this by normalization.

Normal forms

We first define the set of normal forms (◆❢). In our context, normal forms are:

• neutral terms (◆❡, ♥❡): variables applied to as many normal arguments as their "arity". Lists of such arguments are called spines ❙♣ and are parameterized by two types:

1. The first type refers to the type of the variable.

2. The second type refers to the resulting type of the application.

Since we define long βη-normal forms, a neutral term is normal only if its type is •.

• λ-abstractions (λ♥).

♠✉t✉❛• ❞❛t❛ ◆❢ : ❈♦♥ → ❚② → ❙❡t ✇❤❡r❡ λ♥ : ◆❢ (Γ, σ) τ → ◆❢ Γ (σ ⇒ τ ) ♥❡ : ◆❡ Γ • → ◆❢ Γ • ❞❛t❛ ◆❡ : ❈♦♥ → ❚② → ❙❡t ✇❤❡r❡ , : ❱❛r Γ σ → ❙♣ Γ σ τ → ◆❡ Γ τ ❞❛t❛ ❙♣ : ❈♦♥ → ❚② → ❚② → ❙❡t ✇❤❡r❡ ε : ❙♣ Γ σ σ , : ◆❢ Γ τ → ❙♣ Γ σ ρ → ❙♣ Γ (τ ⇒ σ) ρ
Here, the set of normal forms is not defined as a subset of the set of terms. However, it can be easily seen as such through the canonical injection (⌈❴⌉):

♠✉t✉❛• ⌈❴⌉ : ◆❢ Γ σ → ❚♠ Γ σ ⌈ λ♥ ♥ ⌉ = Λ ⌈ ♥ ⌉ ⌈ ♥❡ ♥ ⌉ = ❡♠❜◆❡ ♥ ❡♠❜◆❡ : ◆❡ Γ σ → ❚♠ Γ σ ❡♠❜◆❡ (✈, s) = ❡♠❜❙♣ s (✈❛r ✈) ❡♠❜❙♣ : ❙♣ Γ σ τ → ❚♠ Γ σ → ❚♠ Γ τ ❡♠❜❙♣ ε ❛❝❝ = ❛❝❝ ❡♠❜❙♣ (♥, s) ❛❝❝ = ❡♠❜❙♣ s (❛♣♣ ❛❝❝ ⌈ ♥ ⌉)
Note that the function ❡♠❜❙♣, that maps spines into terms, is defined using an accumulator.

We are now going to define a normalization function ♥❢ : ❚♠ Γ σ → ◆❢ Γ σ, that maps each term to a normal representative. This representative corresponds to the semantics given to the initial term. In order to establish the decidability of the βηequivalence, we thus need to establish that the normalization function satisfies the following two properties:

1. Normalization maps convertible terms to identical normal forms (we call it soundness: an equality in the syntax is also true in the semantics):

s♦✉♥❞♥❡ss : {t ✉ : ❚♠ Γ σ } → t βη✲≡ ✉ → ♥❢ t ≡ ♥❢ ✉ 2.
Terms are convertible to their normal forms (we call it completeness, since it ensures that an equality in the semantics is also true in the syntax):

❝♦♠♣•❡t❡♥❡ss : (t : ❚♠ Γ σ) → ⌈ ♥❢ t ⌉ βη✲≡ t
A consequence of these two properties is that convertibility is exactly reflected by having the same normal forms:

{t ✉ : ❚♠ Γ σ } → t βη✲≡ ✉ ↔ ♥❢ t ≡ ♥❢ ✉
Since the equality of normal forms is obviously decidable (by simple inductions on types, contexts and normal forms), it follows that convertibility is decidable.

Auxiliary functions

We quickly present some auxiliary functions on normal forms and spines.

First, as for indices (see Section 2.2.3) and terms (see Section 2.3), we often need to weaken the context parameterizing a normal form or a spine. We hence have two functions to perform this weakening, whose definitions are direct adaptations of ✇❦❚♠ (so we do not give them here):

♠✉t✉❛• ✇❦◆❢ : (① : ❱❛r Γ σ) → ◆❢ (Γ ✲ ①) τ → ◆❢ Γ τ ✇❦❙♣ : (① : ❱❛r Γ σ) → ❙♣ (Γ ✲ ①) τ ρ → ❙♣ Γ τ ρ
Spines are lists of normal forms; so while it is immediate to add a normal form at the beginning of a spine, we have to define a function that adds an element at the end of a spine:

❛♣♣❙♣ : ❙♣ Γ ρ (σ ⇒ τ ) → ◆❢ Γ σ → ❙♣ Γ ρ τ ❛♣♣❙♣ ε ✉ = (✉, ε) ❛♣♣❙♣ (t, ts) ✉ = (t, ❛♣♣❙♣ ts ✉)

The normalization function

We now define a normalizer as an ❆❣❞❛ function that transforms a term into a normal form of the same type. This normalizer implements hereditary substitutions [START_REF] Watkins | A Concurrent Logical Framework: The Propositional Fragment[END_REF]. The idea behind these substitutions is to perform a syntactical substitution and normalize a term at the same time.

The normalization function is defined with the aid of two auxiliary functions that perform η-expansion, and four auxiliary functions that perform β-reduction.

η-expansion

Variables and neutral terms are η-expanded as much as possible depending on their types:

♠✉t✉❛• ♥✈❛r : ❢♦r❛•• {σ } → ❱❛r Γ σ → ◆❢ Γ σ ♥✈❛r {σ } ① = ♥❡✷♥❢ {σ } (①, ε) ♥❡✷♥❢ : ❢♦r❛•• {σ } → ◆❡ Γ σ → ◆❢ Γ σ ♥❡✷♥❢ {•} ①♥s = ♥❡ ①♥s ♥❡✷♥❢ {σ ⇒ τ } (①, ♥s) = λ♥ (♥❡✷♥❢ {τ } (✈s ①, ❛♣♣❙♣ (✇❦❙♣ ✈③ ♥s) (♥✈❛r {σ } ✈③)))

β-reduction

Four functions perform the β-reduction:

• The function [❴✿❂❴] substitutes a variable by a normal form inside a normal form.

• The function ❴❁❴✿❂❴❃ substitutes a variable by a normal form inside a spine.

• The function ❴✸❴ applies a normal form to a spine.

• The function ♥❛♣♣ launches the β-reduction.

♠✉t✉❛•

[❴✿❂❴] :

◆❢ Γ τ → (① : ❱❛r Γ σ) → ◆❢ (Γ ✲ ①) σ → ◆❢ (Γ ✲ ①) τ (λ♥ t) [① ✿❂ ✉] = λ♥ (t [(✈s ①) ✿❂ (✇❦◆❢ ✈③ ✉)]) (♥❡ (②, ts)) [① ✿❂ ✉] ✇✐t❤ ❡q ① ② (♥❡ (①, ts)) [✳① ✿❂ ✉] | s❛♠❡ = ✉ ✸ (ts ❁ ① ✿❂ ✉ ❃) (♥❡ (. (✇❦✈ ① ②✬), ts)) [✳① ✿❂ ✉] | ❞✐✛ ① ②✬ = ♥❡ (②✬, ts ❁ ① ✿❂ ✉ ❃) ❴❁❴✿❂❴❃ : ❙♣ Γ τ ρ → (① : ❱❛r Γ σ) → ◆❢ (Γ ✲ ①) σ → ❙♣ (Γ ✲ ①) τ ρ ε ❁ ① ✿❂ ✉ ❃ = ε (t, ts) ❁ ① ✿❂ ✉ ❃ = (t [① ✿❂ ✉]), (ts ❁ ① ✿❂ ✉ ❃) ❴✸❴ : ◆❢ Γ σ → ❙♣ Γ σ τ → ◆❢ Γ τ t ✸ (✉, ✉s) = (♥❛♣♣ t ✉) ✸ ✉s t ✸ ε = t ♥❛♣♣ : ◆❢ Γ (σ ⇒ τ ) → ◆❢ Γ σ → ◆❢ Γ τ ♥❛♣♣ (λ♥ t) ✉ = t [✈③ ✿❂ ✉]
We now describe the mechanism behind these functions.

t [① ✿❂ ✉ ]:
1. syntactically substitutes ① by ✉ in t; and 2. normalizes the result at the same time: it is the essence of hereditary substitutions. Its definition is a case analysis on t:

• If t is λ♥ t✬, then substitute ① by ✉ in t✬ (① and ✉ have to be weakened to avoid capture).

• If t is ♥❡ (①, ts), then apply ✉ to ts✬, where ts✬ is ts where ① is substituted by ✉. This application is the role of the ❴✸❴ function.

• If t is ♥❡ (②, ts) where ② does not represent the same variable as ①, then ② is unchanged and the substitution carries on in ts.

ts ❁ ① ✿❂ ✉ ❃ substitutes ① by ✉ in all the normal forms appearing in ts. It is a simple case analysis on ts.

t ✸ ts successively applies t to each element of ts, by a simple case analysis on ts.

♥❛♣♣ t ✉ β-reduces the application of a normal form t to a normal form ✉, by a call to [❴✿❂❴]. As t has a functional type, the typing ensures that it is a λ-abstraction.

The normalization function

The definition of the normalization function is now very straightforward: variables are η-expanded, applications are β-reduced, and λs are normalized under the λ:

♥❢ : ❚♠ Γ σ → ◆❢ Γ σ ♥❢ (✈❛r ①) = ♥✈❛r ① ♥❢ (Λ t) = λ♥ (♥❢ t) ♥❢ (❛♣♣ t ✉) = ♥❛♣♣ (♥❢ t) (♥❢ ✉)
We notice that ❆❣❞❛'s type system ensures that normalization is type preserving: the type of the output normal form is the same as the type of the input term.

Termination of the normalizer

For soundness reasons, ❆❣❞❛ is a total language: only terminating programs can be written. It automatically checks termination using a variant of the termination checker of ❢♦❡t✉s [START_REF] Abel | A predicative analysis of structural recursion[END_REF]: it computes the completed call graph of the functions and the corresponding call matrices. This process can only search for structural arguments to establish termination. One major interest of hereditary substitutions is to be structurally recursive, which is recognized by ❆❣❞❛.

The first two functions ♥✈❛r and ♥❡✷♥❢ are decreasing on the type of their arguments; their termination is thus very simple to establish.

We detail how ❆❣❞❛'s termination checker establishes termination for the four functions [❴✿❂❴], ❴❁❴✿❂❴❃, ❴✸❴ and ♥❛♣♣. For an obvious matter of intelligibility, we are not going to give all the call matrices1 , but only the call graph with the relevant call matrices. For a different formalization, [START_REF] Abel | Implementing a normalizer using sized heterogeneous types[END_REF] gives a proof of the termination of hereditary substitutions using sized types.

Table 1 associates a lexicographical combination of structural orders to each function. We have written the types that are involved in the termination argument à la Church to make things clearer. Figure 1 represents the call graph of the four functions:

• Each node corresponds to a function. We recall the lexicographical orders described in Table 1 under the name of each function.

• Each edge corresponds to a possible call of a function by another function. It is labelled with a summary of the corresponding call matrix (when a function calls itself, we add a prime symbol to the call arguments). In any circuit in the graph with starting and ending vertex s, the measure associated to s decreases for the lexicographical order. It ensures that these mutual definitions terminate.

Function

t1 [①1 σ 1 ✿❂ ✉1 ] ts2 ❁ ①2 σ 2 ✿❂ ✉2 ❃ Measure (σ1,t1) (σ2,ts2) Function t3 σ 3 ✸ ts3 ♥❛♣♣ t4 σ 4 ✉4 Measure (σ3) (σ4)
:= u2 > (σ2, ts2) t σ 3 3 ✸ ts3 (σ3) t1 [ x σ 1 1 := u1 ] (σ1,t1) napp t σ 4 4 u4 (σ4) ( σ 1 = σ 2 , t 1 < t s 2 ) ( σ 2 = σ 1 , t s 2 < t 1 ) (σ ′ 1 = σ1, t1' < t1) (σ3 = σ1) (σ4 = σ3) (σ ′ 3 < σ3) (σ1 < σ4) (σ ′ 2 = σ2, ts2' < ts2)
Figure 1. Call-graph in hereditary substitutions

Analyzing the normalizer

Once the definitions are established, the remainder of our development consists of an analysis of the normalizer in order to prove completeness and soundness (see Section 3.1). The next two sections give some hints how to perform these proofs, with few details. One can consult the source code [START_REF]The decidability of the βη-equivalence using hereditary substitutions[END_REF] for a higher level of detail.

In our context, the proofs in ❆❣❞❛ mainly rely on two techniques, that we call generalization and the introduction of commutation lemmas. Only one proof presented in Section 5 needs special care.

Generalization

As all the functions are inductively defined, it is natural to conduct the proofs by induction as well. As a consequence, in order to prove a statement, we very often need to generalize over some variables appearing in it; otherwise, some of the induction cases are not provable.

For instance, we want to prove

❝♦♥❣❙✉❜st✬ : (t : ❚♠ (Γ, σ) τ ) → ✉1 βη✲≡ ✉2 → s✉❜st t ✈③ ✉1 βη✲≡ s✉❜st t ✈③ ✉2
by induction over t. The variable and application cases do not pose any problem, but in the abstraction case, we would have to prove: s✉❜st t (✈s ✈③) (✇❦❚♠ ✈③ ✉1) βη✲≡ s✉❜st t (✈s ✈③) (✇❦❚♠ ✈③ ✉2) which does not ensue from the induction hypothesis. To make it work, we have to generalize over ✈③ into:

❝♦♥❣❙✉❜st : (t : ❚♠ Γ τ ) → (① : ❱❛r Γ σ) → ✉1 βη✲≡ ✉2 → s✉❜st t ① ✉1 βη✲≡ s✉❜st t ① ✉2

Commutation lemmas

Most of the intermediary results we introduce are commutation lemmas. Informally, these are statements of the form

❢ (❣ ①) ∼ ❣ (❢ ①)
where ∼ is either βη✲≡ or ≡. For instance, in order to prove completeness (Section 4), we introduce the following lemma:

❝♦♠♣❆♣♣ : (t1 : ◆❢ Γ (σ ⇒ τ )) → (t2 : ◆❢ Γ σ) → ⌈ ♥❛♣♣ t1 t2 ⌉ βη✲≡ ❛♣♣ ⌈ t1 ⌉ ⌈ t2 ⌉
that states that embedding (⌈❴⌉) and application (♥❛♣♣ and ❛♣♣) commute.

Proof of completeness

Completeness states that any term is βη-equivalent to its normal form. To show this property, we have to establish it for all the auxiliary functions that define ♥❢ in Section 3.3: all these functions have to return a term that is βη-equivalent to their argument.

For the two functions that perform η-expansion, we have to prove the following properties:

Lemma 1. The η-expansion of a term t is βη-equivalent to t: ♠✉t✉❛• ❝♦♠♣◆❡ : (♥ : ◆❡ Γ σ) → ⌈ ♥❡✷♥❢ ♥ ⌉ βη✲≡ ❡♠❜◆❡ ♥ ❝♦♠♣❱❛r : (✈ : ❱❛r Γ σ) → ⌈ ♥✈❛r ✈ ⌉ βη✲≡ ✈❛r ✈
Proof. The two properties are proved by a mutual induction:

• over σ for ❝♦♠♣◆❡;

• using ❝♦♠♣◆❡ for ❝♦♠♣❱❛r.

For the four functions that perform β-reduction, we have to prove commutation lemmas between the functions that define hereditary substitutions ( [❴✿❂❴], ❴❁❴✿❂❴❃, ✸ and ♥❛♣♣) and the functions that define the embedding from normal forms to terms (⌈❴⌉ and ❡♠❜❙♣): Lemma 2. Hereditary substitutions and embeddings commute:

♠✉t✉❛• s✉❜st❊♠❜❙♣ : (ts : ❙♣ Γ τ ρ) → (① : ❱❛r Γ σ) → (t : ◆❢ (Γ ✲ ①) σ) → (❛❝❝ : ❚♠ Γ τ ) → ❡♠❜❙♣ (ts ❁ ① ✿❂ t ❃) (s✉❜st ❛❝❝ ① ⌈ t ⌉) βη✲≡ s✉❜st (❡♠❜❙♣ ts ❛❝❝) ① ⌈ t ⌉ ❛♣♣◆❢❊♠❜❙♣ : (✉ : ◆❢ Γ σ) → (ts : ❙♣ Γ σ •) → ⌈ ✉ ✸ ts ⌉ βη✲≡ ❡♠❜❙♣ ts ⌈ ✉ ⌉ s✉❜st◆❢❙✉❜st : (t : ◆❢ Γ τ ) → (① : ❱❛r Γ σ) → (✉ : ◆❢ (Γ ✲ ①) σ) → ⌈ t [① ✿❂ ✉ ] ⌉ βη✲≡ s✉❜st ⌈ t ⌉ ① ⌈ ✉ ⌉ ❝♦♠♣❆♣♣ : (t1 : ◆❢ Γ (σ ⇒ τ )) → (t2 : ◆❢ Γ σ) → ⌈ ♥❛♣♣ t1 t2 ⌉ βη✲≡ ❛♣♣ ⌈ t1 ⌉ ⌈ t2 ⌉
Proof. The four properties are proven by a mutual induction:

• over ts for s✉❜st❊♠❜❙♣;

• over ts for ❛♣♣◆❢❊♠❜❙♣;

• over t for s✉❜st◆❢❙✉❜st;

• over t1 for ❝♦♠♣❆♣♣.

We are now able to establish our main theorem:

Theorem 1 (Completeness). Terms are convertible to their normal forms:

❝♦♠♣•❡t❡♥❡ss : (t : ❚♠ Γ σ) → ⌈ ♥❢ t ⌉ βη✲≡ t
Proof. By induction over t using ❝♦♠♣❱❛r (Lemma 1) and ❝♦♠♣❆♣♣ (Lemma 2).

Proof of soundness

Soundness states that the normalization function identifies two βηequivalent terms. We are going to prove it by induction over the proof of βη-equivalence of the two terms. This proof of soundness is longer than the proof of completeness, which is not really surprising since we have to provide a proof of equality, which is a relation more restrictive than the βηequivalence. But we also get stuck on the generalization of one lemma, that makes us introduce a new predicate to be able to formulate it. We now explain the intuition about the reasons of the introduction of this predicate.

In order to prove soundness in the case where t βη✲≡ ✉ is the rule ❡t❛, we would like to show that, if ✉ is a normal form, then the η-expansion of ✉ is equal to ✉:

❡t❛❊q

: (✉ : ◆❢ Γ (σ ⇒ τ )) → λ♥ (♥❛♣♣ (✇❦◆❢ ✈③ ✉) (♥✈❛r ✈③)) ≡ ✉
As ✉ is a normal form which has a functional type, it is a λabstraction λ♥ t for a certain normal form t. So this lemma is equivalent to proving the following proposition: Proposition 1.

(t : ◆❢ Γ τ ) → ✇❦◆❢ (✈s ✈③) t [✈③ ✿❂ ♥✈❛r ✈③] ≡ t
As explained in Section 3.5.1, this proof must be performed by induction over t; and to be able to conclude in the inductive case where t is an abstraction, we have to generalize over ✈③.

However, here, it is not as simple as in the example above: we are possibly misled by De Bruijn indices once more. We recall that the type of the function [① ✿❂ ✉] (described in section 3.3) states that if ① is typed in a context Γ, then ✉ is typed in Γ ✲ ①. It means that in Proposition 1, the two occurrences of ✈③ do not represent the same variable. In fact, they represent two consecutive variables in one context (which have the same type).

Hence, to generalize Proposition 1, it is necessary to generalize the two occurrences of ✈③ with two different names. But it is important to take into account the fact that they are consecutive, otherwise the lemma would not be correct. This is why we introduce a new predicate ♦♥❡❞✐✛ that precisely identifies consecutive indices in one context.

The predicate onediff

This predicate is very simple to define by induction: ✈③ and ✈s ✈③ follow one another; and if ① and ② follow one another, then ✈s ① and ✈s ② too.

❞❛t❛ ♦♥❡❞✐✛

: ❱❛r Γ σ → ❱❛r Γ τ → ❙❡t ✇❤❡r❡ ♦❞③ : ♦♥❡❞✐✛ ✈③ (✈s ✈③) ♦❞s : (① : ❱❛r Γ σ) → (② : ❱❛r Γ τ ) → ♦♥❡❞✐✛ ① ② → ♦♥❡❞✐✛ (✈s ①) (✈s ②) It is important to notice that ♦♥❡❞✐✛
♦♥❡❞✐✛▼✐♥✉s : (✐ • : ❱❛r Γ σ) → ♦♥❡❞✐✛ • ✐ → Γ ✲ ✐ ≡ Γ ✲ • Proof. By induction over ♦♥❡❞✐✛ • ✐.
since it allows us to transform a variable, a term or a normal form ✉ typed in the context Γ ✲ ✐ into the same object typed in Γ ✲ • for some Γ, ✐ and •.

If ♣ : Γ ≡ ∆ and ✉ is parameterized by Γ, then ! ♣ ❃ ✉ is ✉ parameterized by ∆. So, in the example above, if ♣✿ ♦♥❡❞✐✛ • ✐, then the result of the transformation is ! ♦♥❡❞✐✛▼✐♥✉s ✐ • ♣ ❃ ✉.

The η-equality for normal forms

The predicate defined in the previous section now allows us to generalize Proposition 1 that way (detailed above):

Lemma 4. s✉❜st◆❢❊q : (✐ : ❱❛r Γ τ ) → (t : ◆❢ (Γ ✲ ✐) σ) → (• : ❱❛r Γ τ ) → (❦ : ❱❛r (Γ ✲ •) τ ) → (♣ : ♦♥❡❞✐✛ • ✐) → ✇❦✈ ✐ (! s②♠ (♦♥❡❞✐✛▼✐♥✉s ✐ • ♣) ❃ ❦) ≡ • → (✇❦◆❢ ✐ t) [• ✿❂ (♥✈❛r ❦)] ≡ ! ♦♥❡❞✐✛▼✐♥✉s ✐ • ♣ ❃ t
The intuition behind this statement is that we generalize in Proposition 1 all the indices that appear:

(✇❦◆❢ ✐ t) [• ✿❂ (♥✈❛r ❦)]
and add the two constraints:

• ♦♥❡❞✐✛ • ✐: • and ✐ are two consecutive indices; • ✇❦✈ ✐ (! s②♠ (♦♥❡❞✐✛▼✐♥✉s ✐ • ♣) ❃ ❦) ≡ •: • and ✇❦✈ ✐ (! s②♠ (♦♥❡❞✐✛▼✐♥✉s ✐ • ♣) ❃ ❦) represent the same variable.
These two conditions are sufficient to establish Lemma 4, and are verified by Proposition 1. Its proof only requires techniques presented in Section 3.5. The η-equality for normal forms is now a direct consequence of s✉❜s◆❢❊q:

Lemma 5. The η-equality is true for normal forms:

❡t❛❊q : (✉ : ◆❢ Γ (σ ⇒ τ )) → λ♥ (♥❛♣♣ (✇❦◆❢ ✈③ ✉) (♥✈❛r ✈③)) ≡ ✉ ❡t❛❊q (λ♥ ✉) =
r❡✢λ♥ (s✉❜st◆❢❊q (✈s ✈③) ✉ ✈③ ✈③ ♦❞③ r❡✢)

The β-equality for normal forms

Similarly to completeness, to prove soundness in the case where βη✲≡ is ❜❡t❛, we have to prove the following commutation lemma: Lemma 6. Normalization and substitution commute:

♥❢❙✉❜st◆❢ : (t : ❚♠ Γ τ ) → (① : ❱❛r Γ σ) → (✉ : ❚♠ (Γ ✲ ①) σ) → (♥❢ t) [① ✿❂ (♥❢ ✉)] ≡ ♥❢ (s✉❜st t ① ✉)
The proof is a rather technical but uses techniques presented in Section 3.5.

Proof of soundness

We are now able to establish our main theorem: Theorem 2 (Soundness). The normal forms of two convertible terms are equal:

s♦✉♥❞♥❡ss : {t ✉ : ❚♠ Γ σ } → t βη✲≡ ✉ → ♥❢ t ≡ ♥❢ ✉ Proof.
By induction over t βη✲≡ ✉, using ❡t❛❊q (Lemma 5) in the ❡t❛ case and and ♥❢❙✉❜st◆❢ (Lemma 6) in the ❜❡t❛ case. The other cases are trivial.

Conclusion of Sections 4 and 5:

The reverse of Theorem 2 (soundness) is a direct consequence of Theorem 1 (completeness):

Consequence 1. Two terms whose normal forms are equal are convertible.

❝♦♥✈❡rt♥❢ : (t ✉ : ❚♠ Γ σ) → ♥❢ t ≡ ♥❢ ✉ → t βη✲≡ ✉
It follows that two terms are βη-equivalent if and only if their normal forms are equal. As equality on normal forms is obviously decidable, we can conclude that βη-equivalence is decidable.

Moreover, we expect that our algorithm that decides equivalence (normalize and check the equality of normal forms) uses only first order primitive recursion. We did not prove it formally, but it seems reasonable to say that it follows from construction. It makes clear that βη-equivalence is primitive recursive.

Related work

Hereditary substitutions were first introduced by Watkins et al. [START_REF] Watkins | A Concurrent Logical Framework: The Propositional Fragment[END_REF] to define a normalizer for the Concurrent Logical Framework. Their property to preserve canonical forms during substitution makes them a nice approach to an implementation of substitutions for Logical Frameworks [START_REF] Crary | Explicit Contexts in LF (Extended Abstract)[END_REF][START_REF] Harper | Mechanizing metatheory in a logical framework[END_REF] and Higher-Order Abstract Syntax [START_REF] Pientka | A type-theoretic foundation for programming with higherorder abstract syntax and first-class substitutions[END_REF]. Abel [START_REF] Abel | Implementing a normalizer using sized heterogeneous types[END_REF] already noticed that the fact that hereditary substitutions are structurally recursive makes it easy to automatically check the termination of the algorithm they provide. We exploit the two properties:

• The fact that canonical forms are preserved by hereditary substitutions ensures the correct typing given to the substitution function.

• The fact that it is structurally recursive allows us to implement it in ❆❣❞❛ without any need of an explicit termination proof.

The lemmas presented in this paper do not bring something new by their statements, but by their proofs. In fact, hereditary substitutions were studied in many different contexts [START_REF] Abel | Syntactic Metatheory of Higher-Order Subtyping[END_REF][START_REF] Harper | Mechanizing metatheory in a logical framework[END_REF][START_REF] Pfenning | Church and Curry: Combining intrinsic and extrinsic typing[END_REF], and most of our theorems are already proved in those papers. The main difference is that they use a named representation of variables. Indeed, one major contribution of this paper is to adapt hereditary substitutions to De Bruijn indices (with the drawbacks we know, but with advantage that due to the fact that closed terms have a unique representation) and to implement it in an interactive theorem prover based on Type Theory.

Using dependant types in order to define directly the set of well-typed terms is not new. Its formalization has been studied in different interactive theorem provers based on dependant types, such as ❆❣❞❛ [START_REF] Altenkirch | Monadic Presentations of Lambda Terms Using Generalized Inductive Types[END_REF] and ❈♦q [START_REF] Benton | Strongly typed term representations in Coq[END_REF].

Also related is David's work on arithmetical proofs of normalization results, e.g. see [START_REF] David | Normalization without reducibility[END_REF]. Besides, [START_REF] Altenkirch | Tait in one big step[END_REF] uses big step normalization to show decidability of a substitution calculus -this work has also been formalized in ❆❣❞❛.

Conclusion

This paper implements in ❆❣❞❛ a normalizer for the simply typed λ-calculus, and proves that this normalizer can be used to decide the βη-equality over terms. It exploits some aspects of ❆❣❞❛ and, more generally, of programming languages with dependent types:

• Dependent types are not only used to express theorems' statements, but also serve to define particular sets. Here, the parameterization of variables, terms and normal forms by contexts and types is a useful and natural way to define only the subset of λterms we are interested in. It is important to notice that ❆❣❞❛'s implementation of dependent types makes it straightforward to manipulate such objects. ❆❣❞❛'s dependent typing also ensures properties about functions just "by definition".

• ❆❣❞❛'s termination checker is powerful enough to analyze non trivial mutually inductive definitions.

• Conversely, hereditary substitutions give a nice way to define a normalizer within total Type Theory, without constructing a proof of termination of a partial function. This could be extended to more complex type systems, for instance with polymorphism [START_REF] Abel | Implementing a normalizer using sized heterogeneous types[END_REF].

Lemma 3 .

 3 If • and ✐ follow one another in Γ, then Γ ✲ ✐ and Γ ✲ • are equal:

Table 1 .

 1 Decreasing measures in hereditary substitutions

	σ 2 ts2 < x 2

The call matrices can be obtained by compiling our source file ❤s✉❜st✳❛❣❞❛ with the option ✲✈ ✺, for instance.

Acknowledgments

We thank Conor McBride, who suggested the idea and introduced some very convenient notations such as Γ ✲ ①. We also thank Andreas Abel for his useful help and comments about hereditary substitutions. We are grateful to the anonymous reviewers for their accurate comments and suggestions.