Simon Krause

Volodymyr Bon

Irena Senkovska

Ulrich Stoeck

Dirk Wallacher

Daniel M Többens

Stefan Zander

Renjith S Pillai

Guillaume Maurin

François-Xavier Coudert

Stefan Kaskel

A pressure-amplifying framework material with negative gas adsorption transitions

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

In MOFs, novel guest-assisted phenomena, such as ligand flip [START_REF] Fairen-Jimenez | Opening the gate: Framework flexibility in ZIF-8 explored by experiments and simulations[END_REF] , gating [START_REF] Kondo | Novel expansion/shrinkage modulation of 2D layered MOF triggered by clathrate formation with CO 2 molecules[END_REF] , and breathing [START_REF] Serre | An explanation for the very large breathing effect of a metal-organic framework during CO2 adsorption[END_REF][START_REF] Ferey | Large breathing effects in three-dimensional porous hybrid matter: facts, analyses, rules and consequences[END_REF] of the framework lead to adsorption isotherms with S-shape, wide hysteresis and multiple steps [START_REF] Salles | Multistep N2 breathing in the metal-organic framework Co(1,4-benzenedipyrazolate)[END_REF] , which give rise to new, previously unattainable potential applications [START_REF] Schneemann | Flexible metal-organic frameworks[END_REF] . As a rule of thermodynamics, at constant temperature the absolute amount of substance in the adsorbed phase (n ads ) always increases with increasing pressure of the adsorptive (p), resulting in a positive slope (1) in a single component adsorption isotherm (Fig. 1a) [START_REF] Thommes | Physisorption of gases, with special reference to the evaluation of surface area and pore size distribution[END_REF] .

(dn ads /dp) ≥ 0 (1) In the following we describe a material with a paradoxical negative adsorption step causing an unexpected pressure amplification triggered by a unique structural transition of a nanoporous framework. We show that this novel phenomenon is observed upon adsorption of various gas molecules at characteristic temperature and pressure in DUT-49, a framework with very high porosity. Initially, DUT-49 was discovered as a high performance methane storage material for natural gas vehicles [START_REF] Stoeck | A highly porous metal-organic framework, constructed from a cuboctahedral super-molecular building block, with exceptionally high methane uptake[END_REF] . The extremely high excess methane storage capacity of 308 g kg -1 at 110 bar and 298 K motivated us to elucidate the adsorption mechanism at lower temperatures. However, a methane adsorption isotherm recorded at 111 K revealed a peculiar drop that was originally regarded as an instrumental failure (Fig. 1b). Repeated isotherm measurements at 111 K gave evidence of a perfectly reproducible negative adsorption step around 10 kPa, strongly deviating from the previously reported adsorption profile at 298 K (up to 110 bar). With a drop of ∆n NGA = -8.62 mmol g -1 the NGAstep alone surpasses the adsorption capacity of commercially available nanoparticles and even of some zeolites [START_REF] Traa | Handbook of Porous Solids 1015-1057[END_REF] . Thus it is by no means negligible in volumetric adsorption experiments and causes a massive response and pressure amplification of ∆p NGA =2.27 kPa in the measuring cell (Fig. 1f) in stark contrast to any rigid microporous solids (Fig. 1e). This corresponds to a specific ∆p NGA for methane adsorption at 111 K of up to 493 kPa g -1 (Supplementary Tab. S1).

Additional adsorption experiments using n-butane at 298 K lead to a distinct NGA step at 30 kPa (Fig. 1c) with a kinetic profile (Fig. 1g) similar to that of methane (111 K) while isotherms of N 2 at 77 K (Supplementary Fig. S5) show a typical type I slope illustrating the subtle and specific impact of guest interaction on NGA in DUT-49. Gravimetric adsorption experiments with n-butane at 298 K in parallel to DSC support the results obtained from volumetric adsorption experiments and additionally reveal a combination of exothermic and endothermic processes during NGA substantiating the unique and complex mechanism of the transformation (Fig. 1d, Supplementary Fig. S24). Exposing samples of DUT-49 to n-butane is in particular illustrative since NGA can be explored at room temperature below 100 kPa corresponding to conditions easily attained in a standard laboratory environment. Visual monitoring of the sample during the adsorption experiment reveals macroscopic movement of the particle ensemble caused by the massive gas release during NGA, followed by a pronounced shrinkage of the packed bed volume by ca. 20 % (Fig. 1h, supplementary video 1). Based on this macroscopic observation we suspected NGA to be related to massive structural transformations in the crystalline solid. Real time parallelized adsorption/diffraction/EXAFS experiments carried out at the BESSY II light source at HZB (Berlin) using an improved setup [START_REF] Bon | In situ monitoring of structural changes during the adsorption on flexible porous coordination polymers by X-ray powder diffraction: Instrumentation and experimental results[END_REF] allowed us to elucidate the structural transformations in situ.

Synchrotron PXRD data collected during methane adsorption at 111 K indicate two distinct structural transitions of DUT-49op at 10 kPa and 45-65 kPa correlating to the steps in the isotherm (Fig. 2a and2b).

DUT-49op is an assembly of cuboctahedral metal-organic polyhedra (MOPs) formed by Cu 2 -paddle-wheel units and 9H-carbazole-3,6-dicarboxylates connected by biphenylene units forming an fcu topology [START_REF] Stoeck | A highly porous metal-organic framework, constructed from a cuboctahedral super-molecular building block, with exceptionally high methane uptake[END_REF] . Wide open voids (1.0, 1.7 and 2.4 nm) originate from an ordered arrangement of MOPs, an expanded analogue of a cubic close packing of atoms but with huge tetrahedral and octahedral voids (Fig. 3, a-c). During NGA the highly porous framework undergoes a colossal contraction of the unit cell from V = 100,072 Å 3 (ρ calc = 0.287 g • cm -3 ) to a highly squeezed intermediate, DUT-49cp with a cell volume of only 47,282 Å 3 (ρ calc = 0.661 g • cm -3 ) (Supplementary Fig. S34) corresponding to a unit cell change of more than 50,000 Å 3 (Fig. 2c). This initial transformation is reversible and as the pores are completely filled, expansion back to the original DUT-49op is observed (Supplementary Fig. S35).

From a structural point of view the contraction originates from concerted rotation of the MOPs along the threefold axis running along [111], leading to a severe deformation of the ligand (Fig. 3e,supplementary video2).

Yet, the connectivity of the framework is preserved during the transformation and the porosity of the MOPs (d Pore = 10.1 to 9.9 Å) is only slightly affected. EXAFS spectra collected in situ during methane adsorption at contrast, the pore diameter of the tetrahedral voids is strongly reduced from 16.9 to 10.6 Å and the mesoporous octahedral voids deform even more drastically from 23.9 to 7.8 Å, resulting in a massive overall pore volume reduction by 61 % (see also visualization in supplementary video 2).

During desorption of methane at 111 K two gradual phase transitions from DUT-49op to DUT-49ip (V = 94457 Å 3 , a = 45.54 Å, ρ = 0.332 g • cm -3 ) in the pressure range from 30 -20 kPa and to DUT-49cp at pressures lower than 20 kPa were observed, resulting in a wide hysteresis. Remarkably, during desorption at 111 K the framework does not switch back to the open form even at very low pressures (Supplementary Fig. S6).

However, transformation into DUT-49op can be achieved by heating at a constant methane pressure of 100 kPa from 111 K to 298 K followed by evacuation (Supplementary Fig. S7,S9). In situ PXRD/adsorption experiments of n-butane at 298K show similar DUT-49op -DUT-49cp transitions as observed for methane adsorption at 111 K (Supplementary Fig. S32).

Grand Canonical Monte Carlo simulations performed for methane at 111 K in both DUT-49op and DUT-49cp shed light on the microscopic adsorption mechanism in play. The experimental adsorption isotherm is precisely reproduced by simulating two adsorption regimes, starting with pore filling of DUT-49op up to 10 kPa, but continued adsorption in the contracted DUT-49cp (Fig. 4b, analogous observation for n-butane at 298 K; Supplementary Fig. S41). Methane occupies the smaller MOP cavities before gradually travelling over the tetrahedral and octahedral cages of DUT-49op with increasing pressure to attain a complete exploration of the mesopores at 11 kPa (Fig. 4c). Indeed, this scenario strongly suggests that the filling of the mesopores triggers the structure contraction responsible for NGA.

Further analysis by quantum chemistry calculations at Density Functional Theory (DFT) level showed that guest free DUT-49cp is energetically significantly destabilized (∆E = 91 kJ mol -1 per linker molecule) as compared to DUT-49op due to the highly strained organic ligand (Fig. 3a,e). Upon adsorption, this energy difference is overcome by the higher affinity of methane for the contracted-pore structure due to the much smaller pores with deeper energy well of DUT-49cp. Given the adsorption enthalpies of DUT-49cp and DUT-49op (∆H ads ≈ 17 kJ mol -1 and 10 kJ mol -1 respectively) (Supplementary Fig. S44, Tab. S13), the difference in adsorption enthalpy in the transition region, ∆N ads x ∆∆H ads ≈ 130 kJ mol -1 , is in magnitude comparable to ∆E, explaining why adsorption compensates the energy penalty of the structural transition (Supplementary Tab. S15). Analysis of the elastic properties of DUT-49op completes this picture: While the bulk modulus of 8.7 GPa is in the usual range for metal-organic frameworks [START_REF] Tan | Mechanical properties of hybrid inorganic-organic framework materials: establishing fundamental structure-property relationships[END_REF] , the minimal shear modulus of the structure is relatively low at 1.5 GPa, with a strong nonlinearity showing a soft deformation mode that can be triggered by adsorption.

Summarizing, in NGA a highly overloaded metastable state is created by adsorption in a hierarchical pore structure which is spontaneously released when the energy barrier is overcome. Reduction of porosity through network deformation triggered by adsorption-induced stress and subsequent release of previously adsorbed gas is the result. Extended equilibration times up to several hours (Supplementary Fig. S14) refute that this phenomenon is caused by inadequate equilibration of the system but indicate the presence of long-lived metastable states, possibly due to the vast extent of deformation and crossover of pore sizes (Fig. 3d), compared with prominent purely microporous breathing systems such as MIL-53 [START_REF] Serre | An explanation for the very large breathing effect of a metal-organic framework during CO2 adsorption[END_REF] . This implies internal reshuffling of molecules in DUT-49 from rigid MOP pores into contracted octahedral voids. Along these lines is also the temperature dependence of NGA: Adsorption of methane at 91, 111, 101, and 121 K (Fig. 4a,d) and n-butane at 273 -308 K (Supplementary Fig. S10) suggest even a slight I∆n NGA I increase with temperature up to 9.87 mmol(CH 4 ) g -1 at 121 K while the pore contraction mechanism and relative pressure (p/p 0 = 0.1-0.15) responsible for NGA is retained (Supplementary Fig. S27,S30) clearly supporting that filling of the mesopores induces the contraction (Fig. 4a,c).

To our knowledge, pressure amplifying materials of this magnitude have never been reported before.

Metastable cation complexes in zeolite materials could be considered as a rare analogue [START_REF] Riekert | Instability of sorption complexes in synthetic faujasites[END_REF] . Beyond the fundamental fascination of this new phenomenon, implications for technological applications cannot be emphasized strongly enough. Conceptually, these new materials contain all required features for the design of threshold sensitive micropneumatic devices, or stimuli responsive self-propelling systems. In this respect, negative gas adsorption frameworks may be useful as mechanical actuators responding selectively towards changes in the environment, capable to transform a high amount of latent strain into pressure. This phenomenon is certainly unique and novel in the field of porous solids. • g -1 , free pore volume 2.94 cm 3 g -1 ) (b) and DUT-49cp (simulated accessible surface area 2908 m 2 g -1 , free pore volume 1.13 cm 3 g -1 ) (f), color code for the atoms: C

"! #! $! %! &' &$ &( &) ## #$ ! "! #! $! )! *!! ! *! "! &! #! '! $! (! +

Figure 1 I

 1 Figure 1 I Gas adsorption isotherms, pressure and kinetic profiles. a, Typical profile of type I adsorption isotherms for a non-breathing microporous solid and corresponding dn/dp 24 . b, c, adsorption isotherms (blue) and corresponding derivatives (red) of DUT-49 for methane at 111 K (b) and butane at 298 K (c). ∆n NGA represents the NGA-step in the isotherm. d, Gravimetric adsorption in parallel to dynamic scanning calorimetry (DSC), ∆m NGA represents the mass of the gas, released during NGA. e, f, g, Corresponding kinetic pressure profiles for typical adsorption behavior of a non-breathing microporous solid (e) and observed during the NGAstep for methane at 111 K (f) and n-butane at 298 K (g), gray areas indicate the dosing interval. h, Snapshots of video (Supplementary video 1) recorded during the n-butane adsorption steps at 298 K (c, g) (the capillary diameter is 1 mm and the sample bed 5 cm in height at t = 0s).

Figure 2 I

 2 Figure 2 I In situ powder X-ray diffraction (PXRD) during methane adsorption at 111 K. a, Methane adsorption and desorption isotherms at 111 K collected in situ. The points corresponding to collected PXRD patterns are represented as solid symbols. b, Contour plot of the PXRD pattern evolution during adsorption (blue) and desorption (red). (op = open pore phase (cubic, F23, a = 46.427(4) Å), cp = contracted pore phase (cubic, Pa3 , a = 36.1603(2) Å), ip = intermediate pore phase (cubic, Pa3 , a = 45.542(2) Å)). c, Lattice parameter evolution during adsorption and desorption.

Figure 3 I

 3 Figure 3 I Structure of DUT-49op and DUT-49cp. a, e, Conformation of 9,9'-([1,1'-biphenyl]-4,4'-diyl)bis(9Hcarbazole-3,6-dicarboxylate) in DUT-49op (a) and DUT-49cp (e). b, View of the crystal structure along [110] for DUT-49op (simulated accessible surface area 5049 m 2• g -1 , free pore volume 2.94 cm 3 g -1 ) (b) and DUT-49cp (simulated accessible surface area 2908 m 2 g -1 , free pore volume 1.13 cm 3 g -1 ) (f), color code for the atoms: C

(

  dark grey), N (blue), O (red), Cu (cyan), H (light grey). Guest molecules are omitted for clarity. c,g, Pore representation of DUT-49op (c) and DUT-49cp (g) along [110] as natural tilings of nbo net. Color code for pore representation: cuboctahedral MOP cavity (green), tetrahedral cavity (yellow), octahedral cavity (orange). d, Evolution of pore sizes and free pore volume during contraction from DUT-49op to DUT-49cp and h, Evolution of density and accessible geometric surface area. Details about the simulation of intermediate structures, free pore volume, accessible surface area and pore sizes are given in Fig. S40.

Figure 4 I

 4 Figure 4 I Temperature dependent methane adsorption and simulations. a, d, Methane adsorption isotherms at different temperatures. b, Experimental (gray) and simulated methane sorption isotherm at 111 K based on the crystal structures of DUT-49op (red) and DUT-49cp (blue). c, Maps of the occupied positions of methane (green) in 1000 equilibrated frames for a given pressure for DUT-49op and at the transition pressure (11 kPa) of DUT-49cp (bottom frame), color code for the atoms: C (dark grey), N (blue), O (red), Cu (cyan), H (light grey). e, Schematic representation of stress-based model for adsorption-induced structural transformation 28 , equilibrium transition (gray line), metastable transition (black arrows), open-pore phase (red line), contracted-pore phase (blue line), arrows indicate the transition observed for DUT-49.

  < &L1&'< .$ ;;; M N&"< &L1&'< .$ ;;; M K/"< "2(*4< NOP0C@#" .$ ;;; M K/"< "2(*4< NOP0C@!" .$ ;;; M J&$%.-& ./"#'3&/ 9((#4 < .$ @; M N&"< .$ @; M K/"< .$ ;=; M N&"< .$ ;=; M K/"< .$ ;;; M N&"< .$ ;;; M K/"< .$ ;?; M N&"< .$ ;?; M % J&$%.-& ./"#'3&/ 9(#4&,*4&" 1&' *-2$ ,&44: ⊃

Acknowledgements:

V.B. thanks the German Federal Ministry for education and research (Project BMBF No 05K13OD3). S.Kr., V.B., I.S. and S.Ka. thank HZB for financial support and allocation of synchrotron radiation beamtime at KMC-2 beamline. F.-X.C. acknowledges the access to HPC resources from GENCI (grant No. x2015087069). Authors thank Ulrike Koch for SEM images as well as Lev Sarkisov and Alain Fuchs for helpful discussions. These authors contributed equally to this work: Simon Krause & Volodymyr Bon Author Contributions: S. Kr. and U. S. synthesized and activated the investigated material; S. Kr., V. B., I. S. and S. Ka. conducted and interpreted volumetric and gravimetric sorption experiments; S. Kr, V. B., D. W. and D. M. T. conducted the in situ PXRD investigations, S. Kr, V. B., D. W. and S. Z. conducted the in situ EXAFS investigations; V. B. performed crystal structure solution and structure modeling; S. Kr. performed filming and animation of the structural transitions; F. X. C. performed quantum mechanical calculations; G. M. and R. S. P. performed Grand Canonical Monte Carlo simulations of adsorption; S. Kr., V.B., I. S., F. X. C. S., G. M. and S. Ka. wrote the manuscript.

Author Information: Crystal structures of DUT-49op in vacuum at 111 K, DUT-49cp⊃432CH 4 (number of methane molecules per unit cell) at 0.28 relative pressure of methane at 111 K during adsorption, DUT-49op⊃1344CH 4 at 0.97 relative pressure of methane at 111 K during adsorption, DUT-49ip⊃1176CH 4 at 0.25 relative pressure of methane at 111 K during desorption are available free of charge from the Cambridge Crystallographic Data Centre www.ccdc.cam.ac.uk/data_request/cif under reference numbers CCDC-1413081, CCDC-1413083, CCDC-1413082 and CCDC-1413084, respectively. Reprints and permissions information is available at www.nature.com/reprints. The authors declare no competing financial interests. Readers are welcome to comment on the online version of the paper. Correspondence and requests for materials should be addressed to Stefan Kaskel (stefan.kaskel@chemie.tu-dresden.de).


Lisa Allali

Paul Brauner

Inpl Loria

A semantic normalization proof for a system with recursors

Semantics methods have been used to prove cut elimination theorems for a long time. It is only recently that they have been extend to prove strong normalization results, in particular for theories in deduction modulo. However such semantic methods did not apply for systems with recursors like Gödel system T. We show in this paper how super natural deduction provides a bridge between superconsistency of arithmetic and strong normalization of system T. We then generalize this result to a family of inductive types before discussing the dependant case.

Introduction

When building a new theory, there are several criteria one wants this theory to meet. In particular the cut elimination property which means that the cut rule is redundant. This property ensures the consistency of the theory. In an intuitionistic framework (as it is the case in the present paper) it also gives the so-called witness property: if a proof is ending by the introduction of the existential quantifier one can exhibit a witness of this existence. Normalization of a theory is also a desirable property. It ensures the termination of the proof reduction process, gives a way to construct witnesses, and eases the potential implementation of the theory. In a system where all the cuts are captured by the reduction rules (like in the typed lambda calculus), cut elimination is a consequence of normalization. Gentzen was the first to prove, with a syntactic method, the theorem of cut elimination in sequent calculus(Hauptsatz) [START_REF] Gentzen | Untersuchungen über das logische schließen[END_REF]. More recently semantics approaches have been introduced (for instance in [START_REF] Prawitz | Hauptsatz for higher order logic[END_REF][START_REF] Takahashi | A proof of cut-elimination theorem in simple type theory[END_REF][START_REF] Peter | Resolution in type theory[END_REF][START_REF] Hermant | Semantic cut elimination in the intuitionistic sequent calculus[END_REF]) for building proof with respect to some notion of model that has been used by De Marco and Lipton [START_REF] Demarco | Completeness and cutelimination in the intuitionistic theory of types[END_REF] to prove cut elimination of the Intuitionistic Higher-Order Logic, and by Okada [START_REF] Okada | A uniform semantic proof for cut-elimination and completeness of various first and higher order logics[END_REF] for intuitionistic Linear Logic (first and higher-order). The bright side of semantic proofs is that they abstract from synctactic details intrinsic to the type system and concentrate on essential arguments. Therefore, they obediently adapt to language extentions and allow to characterize classes of theo-ries that meet cut elimination property. More recently, a link between such semantic methods and normalization results has been done in the frame of deduction modulo [START_REF] Dowek | Proof normalization modulo[END_REF]. This semantic criterion, called superconsistency, implies the normalization property of every theory expressed as a rewrite system. This has led for instance to the semantic proofs that Heyting's arithmetic (i.e. Peano axioms considered in an intuitionistic setting) is not only consistent, but also verifies the strong normalization property [START_REF] Allali | Algorithmic equality in Heyting arithmetic modulo[END_REF] [START_REF] Dowek | Arithmetic as a theory modulo[END_REF]. Although systems with recursors enjoy syntactic proofs of strong normalization (cf Tait's proof for Gödel system T [START_REF] Tait | Intensional interpretation of functionals of finite type I[END_REF]), they have been reluctant to this method so far. Recursors are used to compute with inductive types on which today's proof-assistants heavily rely to express most theories. This is especially the case of the COQ proof assistant [START_REF] Werner | Une Théorie des Constructions Inductives[END_REF][START_REF] Paulin-Mohring | Inductive definitions in the system coqrules and properties[END_REF][START_REF] Gimenez | A tutorial on recursive types in coq[END_REF]. Also many recent programming languages with support for dependant types such as AGDA [START_REF] Norell | Towards a practical programming language based on dependent type theory[END_REF] include such recursors. Recursors allow the user to easily describe recursive functions and properties while ensuring the strong normalization of the system, which is proved (syntactically) once for all in the metatheory.

In this paper we propose to bridge the gap between deduction modulo and systems with recursors by exhibiting an intermediate system. This system relies on supernatural deduction, an instance of the superdeduction principle [START_REF] Brauner | Principles of superdeduction[END_REF] for natural deduction. Supernatural deduction is yet another way to integrate a theory into natural deduction in the form of inferences rules and had initially been introduced in order to provide a typing system for the rewriting calculus [START_REF] Cirstea | The rewriting calculus -Part I and II[END_REF]. Fortunately, system T computational behaviour is naturally captured (with no complexity speed-up) by some terms of this calculus whose typing rules exactly match those of the recursors. It is therefore sufficient to prove normalization of supernatural deduction for this particular theory to obtain that of system T. That's where semantic methods come into play. Indeed, a precedent paper [START_REF] Brauner | Normalization in supernatural deduction and in deduction modulo[END_REF] has shown that deduction modulo and supernatural deduction are equivalently normalizing for the same theory. In other words: the way a theory is injected into a deduction system is immaterial for the normalization property. We shall then use super-consistency arguments to ensure normalization of the supernatural deduction system simulating system T reductions. This is done by providing a family of so-called B-models for the theory from which this later supernatural deduction system has been derived.

The semantics arguments being clearly identified, we then generalize the whole reasoning to a system with recursors à la system T for a certain family of mutually inductive types. This confirms the validity of our approach and provides the foundations of a possible implementation (this system has actually already been played with in lemuridae, a proof-assistant prototype for the sequent calculus counterpart of supernatural deduction).

System T being rather a programming language than a deduction system, we finally discuss the extension of our approach to dependant types, i.e. predicate logic. Simulation through supernatural deduction is still valid. On the semantic side, the system T being in some way a impoverished version of arithmetic, its super-consistency [START_REF] Allali | Algorithmic equality in Heyting arithmetic modulo[END_REF] fits our needs. We show how our method adapts to deduction system with rewriting. The paper ends with a conjecture that a much larger family of inductive types could be captured by rewriting, as pioneered in [START_REF] Blanqui | Inductive types in the calculus of algebraic constructions[END_REF].

Framework

Deduction systems

Predicate logic

Our starting point is natural deduction for predicate logic. The proof-term language is given by the following grammar, whose constructs are respectively typed by the usual typing rules (Ax), (⇒ I), (⇒ E), (∧I), (∧E 1 ), (∧E 2 ), (∨I 1 ), (∨I 2 ), (∨E), (⊥E), (∀I), (∀E), (∃I) and (∃E) (see [START_REF] Girard | Proofs and Types[END_REF] for instance).

π ::= α | λα.π | (π π ′ ) | π, π ′ | fst(π) | snd(π) | i(π) | j(π) | (δ π 1 α.π 2 β.π 3 ) | I | (δ ⊥ π) | λx.π | (π t) | t, π | (δ ∃ π x.α.π ′ )
The variables x, y, . . . are variables of the first-order theory while α, β, . . . are proof variables. Notice that the variables α,β and x are bound in λα.π, λx.π, (δ π 1 , α.π 2 , β.π 3 ) and (δ ∃ π, x.α.π ′ ). As usual, the process of cut elimination is modeled by (generalized) β-reduction, whose rules are re-minded below.

(λα.π 1 π 2 ) ⊲ π 1 {α := π 2 } fst( π 1 , π 2 ) ⊲ π 1 snd( π 1 , π 2 ) ⊲ π 2 δ (i(π 1 )) α.π 2 β.π 3 ⊲ π 2 {α := π 1 } δ (j(π 1 )) α.π 2 β.π 3 ⊲ π 2 {β := π 1 } (λx.π t) ⊲ π 1 {x := t} δ ∃ t, π 1 x.α.π ′ ⊲ π 2 {x := t, α := π 1 }

Deduction Modulo (DM)

Deduction Modulo is a formalism that aims at distinguishing reasoning from computation in proofs. Modern type systems feature a rule so-called conversion rule which allows to identify propositions which are equal modulo betaconversion.

(CONV)

Γ ⊢ t : T T ≡ β T ′ Γ ⊢ t : T ′
A side-effect of this rule is to allow computation inside the proof, the computation being performed by proof reduction. The idea of deduction modulo [START_REF] Dowek | Theorem proving modulo[END_REF] is to study the phenomenon of computation inside a proof in a simpler framework: predicate logic, where propositions are identified by a congruence. The congruence depends on the theory. It is usually defined as the symmetric and transitive closure of a rewrite system over first-order terms and propositions. Therefore, the typing rules of deduction modulo are those of natural deduction, modulo the congruence. This may be explicited by a rephrasing of the inference rules, as shown for the implication elimination below.

(⇒E) Γ ⊢ C Γ ⊢ A Γ ⊢ B C ≡ A ⇒ B
The other rules of deduction modulo are build in the same way upon natural deduction (see figure 3 in appendix for the full system). In this paper, we restrict ourselves to theories expressed by proposition rewrite systems defined as follows. We call them computational theories. Definition 1 (Proposition rewrite system). We call proposition rewrite rule every rule R : P → ϕ rewriting atomic propositions into propositions build upon the language of predicate logic restricted to the connectives ⇒ and ∀. Moreover, we suppose that F V(ϕ) ⊆ F V(P ). We define a proposition rewrite system as an orthogonal, hence confluent set of proposition rewrite rules.

We shall call DM R the deduction modulo system parametrized by the rewrite system R. The proof-terms are left unchanged w.r.t natural deduction, only the types are identified.

Example 1 (Equality on naturals).

Let us consider the rewrite system R formed by the proposition rewrite rule R eq : (S x) = (S y) → x = y. Then the term λα.α has type (100 = 100) ⇒ (0 = 0) (among others) in DM R with only one step of reasoning but 100 steps of rewriting that are transparent in the proof:

Ax

(100 = 100) ≡ (0 = 0) α : 100 = 100 ⊢ α : 0 = 0 (⇒I) ⊢ λα.α : (100 = 100) ⇒ (0 = 0)

In deduction modulo, proof reduction may however not terminate, depending on the theory defined by R. This is the case for very simple (and even consistent) theories like the one defined by P → (P ⇒ P ) [START_REF] Dowek | Proof normalization modulo[END_REF]. On the other hand, the strong normalization of DM R implies the consistency of R. Therefore, finding criteria which entails the strong normalization of deduction modulo is an active research topic, which has lead to elegant proofs of normalization for arithmetic and set theory [START_REF] Dowek | Arithmetic as a theory modulo[END_REF][START_REF] Allali | Algorithmic equality in Heyting arithmetic modulo[END_REF][START_REF] Dowek | Cut elimination for zermelo's set theory[END_REF].

Supernatural deduction (SND)

While deduction modulo succeeds in hiding purely computational steps of reasoning, it fails at getting rid of the "noise" of trivial proof steps. Supernatural deduction [START_REF] Houtmann | Cohérence de la déduction surnaturelle[END_REF][START_REF] Brauner | Principles of superdeduction[END_REF] addresses this issue by turning a theory R into new inference rules for natural deduction. As an example, the rewrite rule

R ⊆ : A ⊆ B → ∀x (x ∈ A ⇒ x ∈ B) is translated into the following inference rules. (R ⊆ I) Γ, x ∈ A ⊢ x ∈ B Γ ⊢ A ⊆ B x / ∈ FV(Γ) (R ⊆ E) Γ ⊢ A ⊆ B Γ ⊢ t ∈ A Γ ⊢ t ∈ B
The original idea of supernatural deduction is to propose a proof-term language that keeps trace of new rules during proof-reduction while raising the notion of cut to the level of predicates ((R ⊆ I) -(R ⊆ E) cuts for the example above).

Let us see the formal definition of this system. We call SND R the supernatural deduction system associated to R. The proof-terms are those of natural deduction extended with two constructs:

π ::= λR( -→ x ) | (π R( -→ m)) | . . .
They allow to interpret the super-rules. In the pattern R( -→ x ) the constructor R is applied to a sequence of variables that may be either term or proof variables. In the term R( -→ m) it is applied to a sequence of terms that may be either terms of the theory or proof-terms. We can now define the typing rules that correspond to the terms above. Definition 2. The arity of a formula ϕ is a sequence of ∀ and ⇒ symbols defined by induction on ϕ as follows

• if ϕ is atomic arity(ϕ) = [ ], • if ϕ = ϕ 1 ⇒ ϕ 2 then arity(ϕ) = (⇒,arity(ϕ 2 )), • if ϕ = ∀x ϕ 1 then arity(ϕ) = (∀,arity(ϕ 1 )).
Let ϕ be a formula, a sequence for ϕ is a sequence of distinct variables such that the n-th variable of the sequence is a proof variable if the n-th element of the arity of ϕ is ⇒ and a term variable otherwise.

We note -→ x variable sequences. Moreover for any variable t,

(t [ ]) = t and if -→ x = (x, -→ x ′ ) then (t -→ x ) = ((t x) -→ x ′ ).
If C has type φ and -→ x is a sequence for φ, we may say that -→ x is a sequence for C.

Definition 3 (Computation of the introduction rules).

Consider a proposition rewrite rule R : P → ϕ. Consider a sequence l for ϕ of variables that do not occur in the rule. We associate to R an introduction rule for P of the form

(R I) premI(Γ, ϕ, l) Γ ⊢ (λR(l).π) : P cond(Γ,ϕ,l)
Where the sequent premI(Γ, ϕ, l) and the condition cond(Γ, ϕ, l) are defined by induction on the structure of ϕ as follows

• if ϕ is atomic then premI(Γ, ϕ, l) = (Γ ⊢ π : ϕ) cond(Γ, ϕ, l) = ∅ • premI(Γ, A ⇒ B, (α,l)) = premI((Γ, α : A), B, l) cond(Γ, A ⇒ B, (α,l)) = cond((Γ, A), B, l) • premI(Γ, ∀x A, (y,l)) = premI(Γ, A{x := y}, l) cond(Γ, ∀x A, (y,l)) = cond(Γ, A{x := y}, l) ∪ {y ∈ F V(Γ)}

Definition 4 (Computation of the elimination rules).

Consider a proposition rewrite rule R : P → ϕ. Consider a sequence l for ϕ of names. We associate to R an elimination rule for P of the form

(R E) Γ ⊢ π : P premE(Γ, ϕ, l) concl(Γ, (π R(l)), ϕ, l)
Where the multiset of sequents premE(Γ, ϕ, l) and the sequent concl(Γ, π ′ , ϕ, l) are defined by induction on the structure of ϕ as follows

• if ϕ is atomic then concl(Γ, π ′ , ϕ, l) = (Γ ⊢ π ′ : ϕ) premE(Γ, ϕ, l) = ∅ • concl(Γ, π ′ , A ⇒ B, (τ,l)) = concl(Γ, π ′ , B, l) premE(Γ, A ⇒ B, (τ,l)) = {Γ ⊢ τ : A} ∪ premE(Γ, B, l) • concl(Γ, π ′ , ∀x A, (t,l)) = concl(Γ, π ′ , A{x := t}, l) premE(Γ, ∀x A, (t,l)) = premE(Γ, A{x := t}, l)
Example 2 (Proof-terms for the inclusion). Our definition of ⊆ uses a witness and charges an assumption into the context. Thus, the associated proof-terms are those given by the following typing rules:

(R ⊆ I) Γ, α:(x ∈ X) ⊢ A : (x ∈ Y ) Γ ⊢ λR ⊆ (x, α).A : (X ⊆ Y ) x / ∈ FV(Γ) (R ⊆ E) Γ ⊢ A : (X ⊆ Y ) Γ ⊢ B : (t ∈ X) Γ ⊢ A R ⊆ (t, B) : (t ∈ Y )
Definition 5 (Generalized cut elimination). The elimination of a generalized cut is represented by a reduction which transmits the witnesses and the lemmas to the proof.

(λR( -→ x ).π R( -→ m)) ⊲ ρ π{ ----→ x := m}
When seeing supernatural deduction proof-terms as very simple ρ-terms of the rewriting calculus [START_REF] Cirstea | Rewriting calculus with fixpoints: Untyped and first-order systems[END_REF], the generalized cut elimination is then a ρ-reduction step. Hence the notation.

Supernatural deduction modulo (SNDM)

We finally define supernatural deduction modulo, which combines both systems.

Definition 6 (Supernatural deduction modulo).

Let R 1 and R 2 be two rewrite systems composed of proposition rewrite rules. We call supernatural deduction R 1 modulo R 2 (SNDM R1 R2 ) the deduction system formed by SND R1 where the propositions are considered modulo R 2 after the computation of the supernatural deduction rules.

Notice that we fall back in the case of deduction modulo (resp. supernatural deduction) when R 1 (resp. R 2 ) is empty. Let us now state the main result about supernatural deduction modulo.

Proposition 1 (SNDM soundness and completeness).

Let R 1 and R 2 be two proposition rewrite systems. SNDM R1 R2 is sound and complete with respect to natural deduction within the theory formed by axioms of the form

∀ -→ x (P ( -→ x ) ⇔ ϕ( -→ x )) for each proposition rewrite rule P → ϕ present in R 1 ∪ R 2 .
Proof. By combining the similar results for deduction modulo and supernatural deduction respectively stated in [START_REF] Dowek | Theorem proving modulo[END_REF] and [START_REF] Houtmann | Cohérence de la déduction surnaturelle[END_REF].

Several criteria have been studied that ensure deduction modulo or supernatural deduction strong normalization. Transferring them from one system to another has been extensively studied in [START_REF] Brauner | Normalization in supernatural deduction and in deduction modulo[END_REF]. We adapt here one of the results that suits our needs.

Proposition 2 (Strong normalization property transfer).

Let R 1 and R 2 be two proposition rewrite systems. Strong normalization of DM R1∪R2 implies that of SNDM R2 R1 .

Proof. The idea is to translate the λR( -→ x ).π R( -→ m) redexes of SND by λ -→ x .π -→ m ones in deduction modulo which reduce to π{ ----→ x := m} in a finite number of steps. The translation is well-typed thanks to the congruence of deduction modulo.

Semantic tools

Let us see now a semantic criterion over computational theories that implies deduction modulo (thus supernatural deduction) strong normalization. It has been introduced in [START_REF] Dowek | Truth values algebras and proof normalization[END_REF] and used in [START_REF] Allali | Algorithmic equality in Heyting arithmetic modulo[END_REF] to prove strong normalization of a computational presentation of Heyting's arithmetic.

Definition 7 ((full) Pseudo Heyting algebra). Let B be a set and ≤ a relation on

B. A structure B, ≤ , ∧, ∨, ⊥, ⊤, ∀, ∃, ⇒ is a Pseudo Heyting algebra if forall x, y ,z, c in B and a in ℘(B), • ≤ is a preorder on B, • ⊥ is a minimum of B for ≤, • ⊤ is a maximum of B for ≤, • x
-x ∈ a ⇒ ∀a ≤ x, -(∀x ∈ a c ≤ x) ⇒ c ≤ ∀a, -x ∈ a ⇒ x ≤ ∃a, -(∀x ∈ a x ≤ c) ⇒ ∃a ≤ c. • x ≤ y ⇒z ⇔ x ∧y ≤ z.
Definition 8 (Ordered pseudo Heyting algebra). An ordered pseudo Heyting algebra is a pseudo Heyting algebra together with a relation ⊑ on B such that

• ⊑ is an order relation, • ⊤ ≤ b and b ⊑ b ′ then ⊤ ≤ b ′ ,
• ⊤ is a maximal element for ⊑ and ⊥ is a minimal element for ⊑, • ∧, ∨, ∀, ∃ are monotonous, ⇒ is left anti-monotonous and right monotonous.

Definition 9 (Complete ordered PHA). An ordered pseudo Heyting algebra is said to be complete if every subset of B has a greatest lower bound for ⊑.

Definition 10 (Modulo intuitionistic model).

Let L be a language. An Intuitionist model M of L is :

• a set M , • a complete ordered pseudo Heyting algebra B,

• for each function symbol f of arity n a function f from M n to M , • for each predicate symbol P of arity n a function P from M n to B.

Definition 11 (Denotation).

Let M be a model, A be a proposition and φ be an assignment. We define A φ as follows:

x φ = φ(x) ⊥ φ = ⊥ ⊤ φ = ⊤ f (t 1 , . . . , t n ) φ = f ( t 1 φ , . . . , t n φ ) P (t 1 , . . . , t n ) φ = P ( t 1 φ , . . . , t n φ ) A ∧ B φ = A φ ∧ B φ A ∨ B φ = A φ ∨ B φ A ⇒ B φ = A φ ⇒ B φ ∀x A φ = ∀{ A φ,x:=v | v ∈ M } ∃x A φ = ∃{ A φ,x:=v | v ∈ M }
Definition 12 (Models for computational theory). A model of a computational theory whose rewrite rules are

R 1 → R ′ 1 , . . . , R n → R ′ n is such that for each assign- ment φ, R i φ = R ′ i φ for 1 ≤ i ≤ n.

Definition 13 (Super-consistency). A computational theory is super-consistent if, for each compete ordered Heyting algebra B, there exists a B-model of this theory.

Finally, the main property of a super-consistent theory is to bear a model valuated in the reducibility candidates algebra and thus to normalize [START_REF] Dowek | Proof normalization modulo[END_REF].

Proposition 3 (Normalization). If a computational theory

R is super-consistent, then each proof in DM R1 strongly normalizes.

As a consequence, by proposition 2, if a computational theory R 1 ∪ R 2 is super-consistent then SNDM R2 R1 strongly normalizes.

Gödel System T

We introduce in this section a theory DM ǫ,nat and prove that its super-consistency implies the strong normalization of system T.

Definition 14. The system T is a subset of natural deduction restricted to (Ax), (⇒I) and (⇒E). We add

• the constants nat, 0, S and a infinity of symbols rec τ where τ is formed with nat and ⇒ • the axioms 0 : nat, S : nat ⇒ nat and the axiom scheme The aim of this section is to provide an original semantic proof of system T normalization: we will first introduce a rewrite system defining a deduction modulo system DM ǫ,nat . Then we show the super-consistency of DM ǫ,nat which implies its normalization. Finally we migrate from DM ǫ,nat to a supernatural deduction system SNDM nat ǫ which faithfully mimics system T proofs and computational behavior. A final lemma reduces strong normalization for the system T to strong normalization for SNDM nat ǫ and permits to conclude that system T is normalizing, as the process of migrating from deduction modulo to supernatural deduction preserves the strong normalization property (proposition 2).

rec τ : τ ⇒ (nat ⇒ τ ⇒ τ ) ⇒ nat ⇒ τ • the reduction rules λx.t u ⊲ t{x := u} rec τ a f 0 ⊲ a rec τ a f (S n) ⊲ f n (rec τ a f n) Example 3 (

The DM ǫ,nat system

Definition 15 (DM ǫ,nat ). For any proposition P we can form with nat and ⇒ we add a constant ṗ. We add a constant ǫ. The rewrite rules are:

ǫ( ṗ) → P nat → ∀p (ǫ(p) ⇒ (nat ⇒ ǫ(p) ⇒ ǫ(p)) ⇒ nat ⇒ ǫ(p))
Theorem 1. The DM ǫ,nat system is super-consistent.

Proof. Let B be an ordered and complete PHA. We build a B-model M of DM ǫ,nat as follows: The domain M of M is B. ǫ = id. We look for an interpretation of nat such that nat = ∀p (ǫ(p) ⇒ (nat ⇒ ǫ(p) ⇒ ǫ(p)) ⇒ nat ⇒ ǫ(p)) . For any element f of B, we build a model M f where nat is interpreted by f . Let Φ be a function from

B to B mapping f to ∀p (ǫ(p) ⇒ (nat ⇒ ǫ(p) ⇒ ǫ(p)) ⇒ nat ⇒ ǫ(p)) M f .
B is ordered and complete and Φ is monotone (because nat only appears in positive position in ∀p (ǫ(p)

⇒ (nat ⇒ ǫ(p) ⇒ ǫ(p)) ⇒ nat ⇒ ǫ(p)))
. Thus Φ has a fixpoint F . We chose this F to interpret nat in M. Finally for each ṗ we chose : p = P M . By construction M is a B-model of DM ǫ,nat . Thus DM ǫ,nat is super-consistent. We replace the rewrite rule

nat → ∀p (ǫ(p) ⇒ (nat ⇒ ǫ(p) ⇒ ǫ(p)) ⇒ nat ⇒ ǫ(p))
by the inference rules of figure 1. The associated instance of the ρ reduction rule is :

λR nat (x, α, β).π R nat (t, π 0 , π s )⊲ ρ π{x, α, β := t, π 0 , π s } Lemma 1. SNDM nat ǫ is normalizing.
Proof. By proposition 2.

Our goal is to deduce from this normalization theorem that system T is terminating. To do so, we need to prove that we can simulate the computational behaviour of the system T in SNDM nat ǫ , in particular that the two reduction rules of the re cursor are simulated in the only ρ rule. The constructors 0 and S are encoded by the following proof-terms in SNDM nat ǫ .

ν 0 = λR nat (p, α, β).α ν S = λn.λR nat (p, α, β). (β n (λx.λy.λz.(z R nat (p, y, z) α β n)))
The reader may point up here that ν S is not in normal form and could be have been reduced to λn.λR nat (p, α, β).(β n (n R nat (p, α, β))). This is due to the fact that we have chosen to curry rec τ , unlike other presentations of system T which impose that the recursor is always applied to three arguments at once. As a consequence, the β-expanded version of ν S presented above eases the proof of lemma 3. We recognize then in ν 0 and ν S the number 0 and the successor function defined on Parigot integers [START_REF] Parigot | Programming with proofs: A second order type theory[END_REF], which are a recursive (compared to iterative) version of Church integers.

Definition 17 (Translation from system T to SNDM

nat ǫ ). t u = t u λx.t = λx. t rec τ nat = λx.λy.λz.(z R nat ( τ , x, y)) O = ν 0 S = ν S x = x if x is a variable Lemma 2 (Soundness). For all π : T in System T then π : T in SNDM nat ǫ .
Proof. By induction on π.

Lemma 3 (Simulation).

Let π and π ′ be two proofs in system T such that π ⊲ π ′ , then π ⊲ + ρ π ′ in SND nat .

Proof. By induction on π.

The non trivial cases are the following:.

• rec τ nat u v 0 ⊲ u rec τ nat u v 0 = λx.λy.λz.(z R nat ( τ , x, y)) u v ν 0 ⊲ 3 ρ ν 0 R nat ( τ , u , v ) = λR nat (p, α, β).α(R nat ( τ , u , v )) ⊲ ρ u • rec τ nat u v (S n) ⊲ v n (rec τ nat u v n) rec τ nat u v (S n) = λu.λv.λt.(t R nat ( τ , u, v)) u v (ν S n ) ⊲ 3 ρ (ν S n ) R nat ( τ , u , v ) = (λn.λR nat (p, α, β). (β n (λx.λy.λz.(z R nat (p, y, z) α β n))) n ) R nat ( τ , u , v ) ⊲ 2 ρ v n (λx.λy.λz.(z R nat ( τ , y, z) u v n )) = v n (rec τ nat u v n) Theorem 2 (Relative normalization). The strong normal- ization of SNDM nat ǫ implies that of System T. Proof. Consider a reduction sequence π ⊲ π 1 ⊲ π 2 ⊲ . . . in system T. By lemma 3, π ⊲ + ρ π 1 ⊲ + ρ π 2 ⊲ + ρ .
. . is a reduction sequence in SNDM nat ǫ and thus is finite according to lemma 1. So is the one in system T.

Inductive types

We now generalize this result to a family of mutually inductive types. This opens the door to an implementation of a proof assistant with recursors but no primitive reduction rule for recursors.

Simple types with recursors

Let T Y be a set of type symbols and C a set of constructor symbols:

T Y ::= nat, btree, list, . . . C ::= 0, S, Cons, . . .

Definition 18 (Very strictly positive types).

Let RT be a subset of T Y. The set of very strictly positive types associated to RT is defined by:

PT (RT ) ::= RT | RT ⇒ PT (RT ) (RnatI) Γ, α : ǫ(x), β : nat ⇒ ǫ(x) ⇒ ǫ(x) ⊢ π : ǫ(x) Γ ⊢ λR nat (x, α, β).π : nat x ∈ FV(Γ) (RnatE) Γ ⊢ π : nat Γ ⊢ π 0 : ǫ(t) Γ ⊢ π s : nat ⇒ ǫ(t) ⇒ ǫ(t) Γ ⊢ π R nat (t, π 0 , π s ) : ǫ(t)
P i ) ∈ C × PT (RT )
where RT ⊆ T Y. We say that C i is a constructor for rt if the conclusion type of P i is rt, i.e. P i = . . . ⇒ rt.

Example 4 (Trees and Forests).

In the signature Σ constituted by the follwing set:

Node : frst ⇒ tree Leaf : frst Cons : tree ⇒ frst ⇒ frst
Node is a constructor for tree, Leaf and Cons are constructors for frst.

From here on let Σ be a signature for a subset RT of T Y. We call ST (simple types) the set of propositions formed by RT and ⇒. We call ML (minimal propositional logic) the subset of natural deduction restricted to (Ax), (⇒ I) and (⇒ E). In particular the proof-terms are restricted to variables, abstractions and applications.

For every rt ∈ RT , τ ∈ ST and ϕ ∈ PT we define a proposition ∆ τ rt (ϕ) by induction on ϕ as follows.

∆ τ rt (A) = τ if A ∈ RT ∆ τ rt (A ⇒ B) = A ⇒ ∆ τ rt (B) if A = rt ∆ τ rt (rt ⇒ B) = rt ⇒ τ ⇒ ∆ τ rt (B)
This intuitively corresponds to the part of a constructor in the elimination scheme we will associate to rt. As an example, ∆ τ nat (nat ⇒ nat) = nat ⇒ τ ⇒ τ . Definition 20 (Elimination scheme). To every recursive type rt ∈ RT we associate an elimination scheme ε τ parametrized by τ ∈ ST :

ε τ (rt) = ∆ τ rt (t 1 ) ⇒ . . . ⇒ ∆ τ rt (t n ) ⇒ rt ⇒ τ where t 1 , . . . , t n = {P i | (C i : P i ) ∈ Σ}
We then enrich the deduction system with respect to Σ by adding an axiom for each constructor of Σ as well as recursor constants for each recursive type typed by the corresponding elimination scheme.

Definition 21 (Simple type system with recursors).

ML Σ = ML ∪ Σ ∪ {rec τ rt : ε τ (rt) | rt ∈ RT }
Example 5 (Trees and Forests). Given the signature Σ of the previous example, ML Σ is the type system ML enriched with the axioms Node : frst ⇒ tree, Leaf : frst, Cons : tree ⇒ frst ⇒ frst as well as the two axiom schemes parametrized by τ :

rec τ tree : frst ⇒ tree ⇒ τ rec τ frst : τ ⇒ (tree ⇒ frst ⇒ τ ⇒ τ ) ⇒ frst ⇒ τ

Reduction rules

Let τ be some type. Let rt ∈ RT , (C : P ) be one of his constructors, ( -→ u , t) a sequence for rec τ rt , -→ x a sequence for C, and f a variable. We define the term Θ τ rt, -→ u ( -→ x , P, f ) by induction on both -→ x and P as follows.

Θ τ rt, - → u ([ ], rt, f ) = f Θ τ rt, - → u ((x, -→ x ′ ), A ⇒ B, f ) = Θ τ rt, - → u ( -→ x ′ , B, (f x)) if A = rt Θ τ rt, - → u ((x, -→ x ′ ), rt ⇒ B, f ) = Θ τ rt, - → u ( -→ x ′ , B, (f x (rec τ rt -→ u x)))
This corresponds to the right hand-side of the reduction rule we will associate to a constructor of rt. As an example, we get the following term for the type of the constructor S.

Θ τ nat,(a,f ) ((n), nat ⇒ nat, f ) = f n (rec τ nat a f n)
Definition 22 (Reduction rules associated to a type). Let τ be some type. Let rt ∈ RT . We name R τ rt the set of reduction rules composed of

(rec τ rt -→ u (C i -→ x i )) ⊲ Θ τ rt, - → u ( -→ x i , P i , u i )
for every (C i : P i ) constructor of rt, where -→ x i is a sequence for C i and -→ u is a sequence u 1 , . . . , u n of variables such that for all variable t, ( -→ u , t) is a sequence for rec τ rt . The set R(Σ) of reduction rules scheme parametrized by τ associated to a signature Σ is then naturally defined as:

R(Σ) = rt∈RT R τ rt
Example 6 (Trees and Forests). For the signature Σ proposed in example 5, we get the following reduction system.

rec τ tree u 1 (Node t 1 ) ⊲ u 1 t 1 rec τ frst u 1 u 2 Leaf ⊲ u 1 rec τ frst u 1 u 2 (Cons t 1 t 2 ) ⊲ u 2 t 1 t 2 (rec τ frst u 1 u 2 t 2 )
Definition 23 (ML Σ proof reduction). The proof-terms of ML Σ are identified by the union of R(Σ) and β-reduction.

Proposition 4 (Subject reduction). For all signature Σ, ML Σ enjoys the subject reduction property.

Proof. The rules of R(Σ) are type preserving.

Translation to SNDM

We will now encode both ML Σ judgments and computational behaviour into the SNDM R2 R1 supernatural deduction modulo system. The predicate symbols are those of RT along with a unary predicate ǫ. To each proposition τ ∈ ST we associate a constant symbol τ of sort κ. We finally define R 1 as the infinite proposition rewrite system which reifies them to the propositional level:

R 1 = {ǫ( τ ) → τ | τ ∈ ST } Remark 1.
The infinite nature of R 1 is not intrinsic of our encoding. We could actually have used a finite one consisting in one constant ṙt per recursive type symbol and its a decoding rule ǫ( ṙt) → rt, along with a binary predicate symbol ⇒ decoded by the rule ⇒(x, y) → x ⇒ y. As an example, the proposition ⇒( ⇒( ṅ at, ṅ at), ṅ at) would be congruent to (nat ⇒ nat) ⇒ nat in this setting. However, for the sake of simplicity, we stick to the infinite version in this paper.

Let us now define R 2 according to the signature Σ. For every rt ∈ RT , ϕ ∈ PT and first-order variable p, we define a proposition δ t rt (ϕ) by induction on the structure of ϕ as follows. Let us see now how we encode the constructors of ML Σ with proof-terms of SNDM R2 R1 . Let (C : P ) be a constructor of rt ∈ RT , (p, -→ u ) a sequence for R rt , -→ x a sequence for C, and f a proof variable. We define the term θ p rt, -→ u ( -→ x , P, f ) by induction on both -→ x and P as follows.

δ p rt (A) = ǫ(p) if A ∈ RT δ p rt (A ⇒ B) = A ⇒ δ p rt (B) if A = rt δ p rt (rt ⇒ B) = rt ⇒ ǫ(p) ⇒ δ p rt (B)
θ p rt, - → u ([ ], rt, f ) = f θ p rt, - → u ((x, -→ x ′ ), A ⇒ B, f ) = θ p rt, - → u ( -→ x ′ , B, (f x)) if A = rt θ p rt, - → u ((x, -→ x ′ ), rt ⇒ B, f ) = θ p rt, - → u ( -→ x ′ , B, (f x r(p, x, -→ u ))) Where r(p, x, -→ u ) = λ -→ v .λy.(y R rt (p, - → v ) -→ u x)
Definition 25 (Proof-term encoding a constructor). Let (C i : P i ) be a constructor of rt ∈ RT , -→ x a sequence for C i and (p, -→ u ) = p, u 1 , . . . , u n a sequence for R rt . We define the proof-term

ν Ci = λ -→ x .λR rt (p, -→ u ).θ p rt, - → u ( -→ x , P i , u i )
as the proof-term encoding the constructor C i .

Example 7 (Trees and Forests).

The proposition rewrite rules R tree and R frst respectively associated to tree and forest are:

rec τ tree → ∀p frst ⇒ ǫ(p) rec τ frst → ∀p ǫ(p) ⇒ (tree ⇒ frst ⇒ ǫ(p) ⇒ ǫ(p)) ⇒ ǫ(p)
= λ -→ x .λt.(t R rt ( τ , -→ x )) C = ν C x = x if x is a variable
Lemma 5 (Soundness). For all proof-term π in ML Σ , if π : T then π : T in SNDM R2 R1 . Proof. By induction on π. concerning their implementation. Indeed, the only way to get a proof of N(0) is through α while we are forced to re-use β to inhabit the type of ν S . Since the ρ-reduction rule is generic and not ad-hoc for this particular case, this indicates that the computational behaviour of the system is fully contained in the type of the induction scheme, which is a well-known result in System F.

Proving super-consistency of this theory is still possible using the same positivity argument. It has actually be done in [START_REF] Allali | Algorithmic equality in Heyting arithmetic modulo[END_REF], which proposes a deduction modulo presentation of Heyting's arithmetic and proves its normalization. The proof is a bit more technical since it requires a more complex description and semantic denotation of the constants encoding the propositions (those meant to instantiate ∀p in R N ). This still can be done in a finite number of rewrite rules using explicit substitutions as described in [START_REF] Kirchner | A finite first-order theory of classes[END_REF].

An exciting aspect of this later proof is that it not only expresses the induction scheme using a rewrite rule but also equality as well as + and × definitions, without changing anything to the proof. Put into perspective with the present work, this offers a flexible proof method to prove strong normalization of types systems with recursors mixed with function and proposition symbols defined by rewrite systems, which is a challenging research topic [START_REF] Blanqui | Definitions by rewriting in the calculus of constructions[END_REF][START_REF] Chrzaszcz | Towards rewriting in coq[END_REF].

One last remark concerning equality is that it is usually expressed by a parametrized inductive type which encodes the fact that it is the smallest reflexive predicate in systems like COQ. On the other hand, [START_REF] Allali | Algorithmic equality in Heyting arithmetic modulo[END_REF] encodes it by the following rewrite system.

0 = 0 → ⊤ (S n) = 0 → ⊥ (S n) = (S m) → n = m 0 = (S n) → ⊥
We conjecture that every parametrized inductive type can be simulated by a similar proposition rewrite system.

Conclusion

We have introduced a new semantic method to prove system T termination by exhibiting an intermediate system between deduction modulo and system T based on supernatural deduction. We then have extended the result to a family of inductive types and have finally shown how the method could be applied to Heyting arithmetic as a dependant version of system T with rewrite rules on proposition. This is the first step of a generalization of the results presented section 4 to a class of dependant inductive types à la Martin-Löf. Another research topic would be the encoding of parametrized inductive types by means of proposition rewrite rules as conjectured above. Finally, it would be interesting to instantiate the proposition rewrite system simulating system T for superdeduction applied to sequent calculus [START_REF] Brauner | Principles of superdeduction[END_REF]. This probably would provide a good intuition of what a classical calculus with recursors could looks like.

  ∧y is a lower bound of x and y, • x ∨y is a upper bound of x and y, • ∀ and ∃ (infinite lower and upper bounds) are functions from ℘(B) to B such that: • ∀ (infinite lower bound) is a function from ℘(B) to B such that:

  Functions in System T). + = λa : nat.λb : nat.(rec nat 0 λx : nat.λy : nat.(S y) b) × = λa : nat.λb : nat.(rec nat 0 λx : nat.λy : nat.(+ y a) b)

Corollary 1 .

 1 DM ǫ,nat is strongly normalizing. Proof. By proposition 3.

3. 2 .

 2 From DM ǫ,nat to SNDM nat ǫ Definition 16 (SNDM nat ǫ ). We keep the rewrite rule scheme: ǫ( ṗ) → P

Figure 1 .

 1 Figure 1. Typing rules of SND nat

Definition 24 (Proposition rewrite rules associated to rt). To

  Positivity For every rt type in RT and R rt : rt → φ the associated rewrite rule, the occurrences of rt are in positive position in φ.Proof. By induction on the type of rt constructors. These rules constitute R 2 : R 2 = {R rt | rt ∈ Σ} which means that for each rt ∈ RT we get two inference rules (rtI) and (rtE) whose general shape is given by figure2.

	Let us state the essential property of these rules.
	Lemma 4.

every recursive type rt ∈ RT we associate proposition rewrite rule R rt parametrized by τ ∈ ST :

R rt : rt → ∀p δ p rt (t 1 ) ⇒ . . . ⇒ δ p rt (t n ) ⇒ ǫ(p)

where t 1 , . . . , t n = {P i | (C i : P i ) ∈ Σ}

(rtI) Γ, α 1 : δ p rt (t 1 ), . . . α n : δ p rt (t n ) ⊢ π : ǫ(p) Γ ⊢ λR rt (x, α 1 , . . . , α n ).π : rt p ∈ FV(Γ) (rtE) Γ ⊢ π : rt Γ ⊢ π 0 : δ p rt (t 1 ) . . . Γ ⊢ π n : δ p rt (t n ) Γ ⊢ π R rt (t, π 0 , . . . , π s ) : ǫ(t)

Figure 2. General shape of SNDM R2

R1 typing rules Theorem 3 (Simulation). Let π and π ′ be two proofs in ML Σ such that π ⊲ π ′ , then π ⊲ + ρ π ′ .

Proof. The interesting case is that of rec τ rt -→ u t which is treated by induction on the constructors of rt.

Corollary 2 (Relative normalization). The strongnormalization of SND R2

R1 implies that of ML Σ .

Strong normalization

We shall now prove the super-consistency of DM R1∪R2 , therefore strong normalization of SNDM R2 R1 .

Proof. Let B be an ordered and complete PHA. We build a B-model M of R 1 ∪ R 2 as follows. The domain M of M is B. We therefore interpret ǫ by the identity on B.

To give an interpretation to the zero-ary predicates rt 1 , . . . , rt n of RT , the proof slightly differs from the one for System T since we have to handle mutually recursive types (trees and forests for instance). For every tuple (f 1 , . . . , f n ) of B n we can define a model M (f1,...,fn) of the language ∀, ⇒, rt 1 , . . . , rt n where rt 1 is interpreted by f 1 , rt 2 by f 2 , etc. We call E M the set made of of these models for every (f 1 , . . . , f n ) of B n . We then define a function

where f ′ i is the interpretation of the right hand-side of R r i in M (f1,...,fn) :

We extend now the order ⊑ to E M the following way:

Then by lemma 4, Φ is monotone for ⊑ and thus we can build a fixpoint M (F1,...,Fn) of Φ. We complete this model M (F1,...,Fn) by interpreting every τ by τ to obtain M. Corollary 3. For all signature Σ, ML Σ enjoys the strong normalization property.

Extension to Heyting arithmetic

The next natural extension of this system is to annotate types with dependant information. A dependant version of System T would be Heyting arithmetic. The type of the recursor is then decorated into the following induction scheme, where P is a proposition: P {0} ⇒ (∀y P {y} ⇒ P {S y}) ⇒ ∀n P {n} Let us see how to encode this system in supernatural deduction modulo as we have done for system T.

We first introduce a unary predicate N(n) which expresses the fact that n is a natural number. This is the dependent counterpart of nat. The associated proposition rewrite rule is then:

Where hered is defined as follows.

The associated super-rules are then

and the instance of the ρ-calculus reduction rule for R N is still the same as for R nat .

The real difference w.r.t. the non-dependant version is the type of β which now takes as an argument a first-order term n along with the proof of N(n) that it is a natural number. This is reflected by the type of 0 and S encodings:

An interesting point here is that, contrary to the nondependent case, the types of ν 0 and ν S left us no choice A. Deduction modulo typing rules


published or not. The documents may come   L'archive ouverte pluridisciplinaire

Investigating the stability of the LBM-BGK through an extended von Neumann analysis G. Wissocq, J.F. Boussuge, P. Sagaut

In the lattice Boltzmann method (LBM), the modeling of the collision operator is of paramount importance to recover a correct macroscopic fluid behavior, as well as for numerical stability purposes. The most simple and efficient choice is based on the Bhatnagar-Gross-Krook (BGK) approximation [START_REF] Bhatnagar | A Model for Collision Processes in Gases. I. Small Amplitude Processes in Charged and Neutral One-Component Systems[END_REF]. This collision operator is known to suffer from a lack of robustness when increasing the Mach and/or Reynolds numbers of the fluid flow. However, the origins of these instabilities remain an open question. In this context, the von Neumann analysis is a powerful tool to predict the stability bounds of a numerical scheme. It aims at evaluating the response of a system, described by a given set of equations, to linear perturbations. Originally widely used on Navier-Stokes (NS) based solvers, Sterling and Chen were among the firsts to apply it to the LBM by linearizing the collision operator around a base steady flow [START_REF] Sterling | Stability Analysis of Lattice Boltzmann Methods[END_REF]. In our work, the standard analysis is extended to the study of the eigenvectors of the linearized system [START_REF] Wissocq | An extended spectral analysis of the lattice Boltzmann method: modal interactions and stability issues[END_REF]. The computation of their moments provides the macroscopic information carried by each wave, which can be helpful to understand the physical behavior of the LBM. It leads to the identification of three kinds of waves: (1) physical waves, that are physically expected by the NS equations, (2) ghost waves, that have no macroscopic contribution in the linear approximation, and (3) numerical waves, that advect some macroscopic but unphysical information. Moreover, modal interactions occuring between physical and numerical modes can be highlighted by the analysis. Using the BGK operator, when increasing the Mach number of the mean flow, two phenomena progressively appear: curve veering and eigenvalue collision. These two kinds of modal interactions are illustrated on a simple case of harmonic oscillators and may be responsible for the strong instabilities observed with the BGK collision operator.

Figure 1 :

 1 Figure 1: Curve veering phenomenon observed in the stability analysis of the D1Q3 lattice at Ma = 0.7.