format: text

text:
# References

Tests of relativity using a microwave resonator
Peter Wolf1,2, Sébastien Bize2, André Clairon2, André N. Luiten3, Giorgio Santarelli2, Michael E. Tobar3

1Bureau International des Poids et Mesures, Pavillon de Breteuil, 92312 Sèvres Cedex, France
2BNM-SYRTE, Observatoire de Paris, 61 Av. de l’Observatoire, 75014 Paris, France
3University of Western Australia, School of Physics, Nedlands 6907 WA, Australia

## Abstract

The frequencies of a cryogenic sapphire oscillator and a hydrogen maser are compared to set new constraints on a possible violation of Lorentz invariance. We determine the variation of the oscillator frequency as a function of its orientation (Michelson-Morley test) and of its velocity (Kennedy-Thorndike test) with respect to a preferred frame candidate. We constrain the corresponding parameters of the Mansouri and Sexl test theory to $`\delta \beta +1/2=(1.5\pm 4.2)\times 10^9`$ and $`\beta \alpha 1=(3.1\pm 6.9)\times 10^7`$ which is equivalent to the best previous result for the former and represents a 30 fold improvement for the latter.

PACS number(s): 03.30.+p, 06.30.Ft
The Einstein equivalence principle (EEP) is at the heart of special and general relativity  and a cornerstone of modern physics. One of the constituent elements of EEP is Local Lorentz invariance (LLI) which, loosely stated, postulates that the outcome of any local test experiment is independent of the velocity of the (freely falling) apparatus. The central importance of this postulate in modern physics has motivated tremendous work to experimentally test LLI . Additionally, nearly all unification theories (in particular string theory) violate the EEP at some level  which further motivates experimental searches for such violations of the universality of free fall  and of Lorentz invariance .

The vast majority of modern experiments that test LLI rely essentially on the stability of atomic clocks and macroscopic resonators , therefore improvements in oscillator technology have gone hand in hand with improved tests of LLI. Our experiment is no exception, the 30 fold improvement being a direct result of the excellent stability of our cryogenic sapphire oscillator. Additionally its operation at a microwave frequency allows a direct comparison to a hydrogen maser which provides a highly stable and reliable reference frequency.

Numerous test theories that allow the modeling and interpretation of experiments that test LLI have been developed. Kinematical frameworks  postulate a simple parametrisation of the Lorentz transformations with experiments setting limits on the deviation of those parameters from their special relativistic values. A more fundamental approach is offered by theories that parametrise the coupling between gravitational and non-gravitational fields (TH$`ϵ\mu `$  or $`\chi `$g  formalisms) which allow the comparison of experiments that test different aspects of the EEP. Finally, formalisms based on string theory  have the advantage of being well motivated by theories of physics that are at present the only candidates for a unification of gravity and the other fundamental forces of nature.

Owing to their simplicity the kinematical frameworks of  have been widely used to model and interpret many previous experiments testing LLI . In order to compare our results to those experiments we will follow this route in the present work (an analysis of our experiment in the light of other test theories being relegated to a future publication). Those frameworks postulate generalized transformations between a preferred frame candidate $`\mathrm{\Sigma }(T,𝐗)`$ and a moving frame $`\mathrm{S}(t,𝐱)`$ where it is assumed that in both frames coordinates are realized by identical standards (e.g. hydrogen masers for the time coordinates). We start from the transformations of  (in differential form) for the case where the velocity of S as measured in $`\mathrm{\Sigma }`$ is along the positive X-axis, and assuming Einstein synchronization in S (we will be concerned with signal travel times around closed loops so the choice of synchronization convention can play no role):

$$dT=\frac{1}{a}\left(dt+\frac{vdx}{c^2}\right);dX=\frac{dx}{b}+\frac{v}{a}\left(dt+\frac{vdx}{c^2}\right);dY=\frac{dy}{d};dZ=\frac{dz}{d}$$
(1)
with $`c`$ the velocity of light in vacuum in $`\mathrm{\Sigma }`$. Using the usual expansion of the three parametrs $`(a1+\alpha v^2/c^2+𝒪(c^4);b1+\beta v^2/c^2+𝒪(c^4);d1+\delta v^2/c^2+𝒪(c^4))`$, setting $`c^2dT^2=dX^2+dY^2+dZ^2`$ in $`\mathrm{\Sigma }`$, and transforming according to (1) we find the coordinate travel time of a light signal in S:

$$dt=\frac{dl}{c}\left(1\left(\beta \alpha 1\right)\frac{v^2}{c^2}\left(\frac{1}{2}\beta +\delta \right)\mathrm{sin}^2\theta \frac{v^2}{c^2}\right)+𝒪(c^4)$$
(2)
where $`dl=\sqrt{dx^2+dy^2+dz^2}`$ and $`\theta `$ is the angle between the direction of light propagation and the velocity v of S in $`\mathrm{\Sigma }`$. In special relativity $`\alpha =1/2;\beta =1/2;\delta =0`$ and (1) reduces to the usual Lorentz transformations. Generally, the best candidate for $`\mathrm{\Sigma }`$ is taken to be the frame of the cosmic microwave background (CMB)  with the velocity of the solar system in that frame taken as $`v_{}377`$ km/s, decl. $`6.4^{}`$, $`RA11.2`$h.

Michelson-Morley type experiments  determine the coefficient $`P_{MM}=(1/2\beta +\delta )`$ of the direction dependent term. At present the most stringent limit on that parameter is $`|P_{MM}|3.2\times 10^9`$  determined over 23 years ago in an outstanding experiment whose uncertainty has not been approached since. Our experiment is the first one that can confirm that result with roughly equivalent uncertainty $`(4.2\times 10^9)`$. Kennedy-Thorndike experiments  measure the coefficient $`P_{KT}=(\beta \alpha 1)`$ of the velocity dependent term. The most stringent limit on $`|P_{KT}|`$ has been recently improved from  by a factor 3 to $`|P_{KT}|2.1\times 10^5`$ . We improve this result by a factor of 30 to $`|P_{KT}|6.9\times 10^7`$. Finally clock comparison and Doppler experiments measure $`\alpha `$, currently limiting it to $`|\alpha +1/2|8\times 10^7`$ . The three types of experiments taken together then completely characterize any deviation from Lorentz invariance in this particular test theory.

Our cryogenic oscillator consists of a sapphire crystal of cylindrical shape operating in a whispering gallery mode (see fig. 1 for a schematic drawing and  for a detailed description). Its coordinate frequency can be expressed by $`\nu =m/t_c`$ where $`t_c`$ is the coordinate travel time of a light signal around the circumference of the cylinder (of radius $`r`$) and $`m`$ is a constant. From (2) the relative frequency difference between the sapphire oscillator and the hydrogen maser (which realizes coordinate time in S) is

$$\frac{\mathrm{\Delta }\nu (t)}{\nu _0}=P_{KT}\frac{v(t)^2}{c^2}+P_{MM}\frac{v(t)^2}{c^2}\frac{1}{2\pi }_0^{2\pi }\mathrm{sin}^2\theta (t,\phi )𝑑\phi +𝒪(c^3)$$
(3)
where $`\nu _0=m/(2\pi r/c)`$, $`v(t)`$ is the (time dependent) speed of the lab in $`\mathrm{\Sigma }`$, and $`\phi `$ is the azimuthal angle of the light signal in the plane of the cylinder. The periodic time dependence of $`v`$ and $`\theta `$ due to the rotation and orbital motion of the Earth with respect to the CMB frame allow us to set limits on the two parameters in (3) by adjusting the periodic terms of appropriate frequency and phase (see  for calculations of similar effects for several types of oscillator modes). Given the limited durations of our data sets ($``$ 9.5 days) the dominant periodic terms arise from the Earth’s rotation, so retaining only those we have $`𝐯(t)=𝐮+𝛀\times 𝐑`$ with $`𝐮`$ the velocity of the solar system with respect to the CMB, $`𝛀`$ the angular velocity of the Earth, and $`𝐑`$ the geocentric position of the lab. We then find after some calculation

$$\begin{array}{cc}\mathrm{\Delta }\nu /\nu _0& =P_{KT}(H\mathrm{sin}\lambda )\hfill \\ & +P_{MM}(A\mathrm{cos}\lambda +B\mathrm{cos}(2\lambda )+C\mathrm{sin}\lambda +D\mathrm{sin}\lambda \mathrm{cos}\lambda +E\mathrm{sin}\lambda \mathrm{cos}(2\lambda ))\hfill \end{array}$$
(4)
where $`\lambda =\mathrm{\Omega }t+\varphi `$, and A-E and $`\varphi `$ are constants depending on the latitude and longitude of the lab $`(48.7^{}`$N and $`2.33^{}`$E for Paris). Numerically $`H2.6\times 10^9`$, $`A8.8\times 10^8`$, $`B1.8\times 10^7`$, C-E of order $`10^9`$. We note that in (4) the dominant time variations of the two combinations of parameters are in quadrature and at twice the frequency which indicates that they should decorelate well in the data analysis allowing a simultaneous determination of the two (as confirmed by the correlation coefficients below). Adjusting this simplified model to our data we obtain results that differ by less than 10% from the results presented below that were obtained using the complete model ((3) including the orbital motion of the Earth).

The cryogenic sapphire oscillator (CSO) is compared to a commercial (Datum Inc.) active hydrogen maser whose frequency is also regularly compared to caesium and rubidium atomic fountain clocks in the laboratory . Both oscillators are operated in temperature controlled rooms, with the temperature sensitive electronics mounted on an actively temperature stabilized panel. The CSO resonant frequency at 11.932 GHz is compared to the 100 MHz output of the hydrogen maser. The maser signal is multiplied up to 12 GHz of which the CSO signal is subtracted. The remaining $``$ 67 MHz signal is mixed to a synthesizer signal at the same frequency and the low frequency beat at $``$ 64 Hz is counted, giving access to the frequency difference between the maser and the CSO. The instability of the comparison chain has been measured and does not exceed a few parts in $`10^{16}`$. The typical stability of the measured CSO - maser frequency after removal of a linear frequency drift is shown in fig. 1.

Our experimental data consists of seven sets of measured values of $`\mathrm{\Delta }\nu /\nu _0`$ of varying length (2.8 to 9.5 days, 37 days in total) taken in Nov./Dec. 2001 and Mar./Apr./Sep. 2002 (see fig. 2). The sampling times $`\tau _0`$ are generally 100 s except for the first two sets for which $`\tau _0=12`$ s and $`5000`$ s respectively. To analyze our data we simultaneously adjust an offset and a rate (natural frequency drift, typically $`2\times 10^{18}`$ s-1) per data set and the two parameters of the model (3), a total of 16 parameters. In the model (3) we take into account the rotation of the Earth and the Earth’s orbital motion, the latter contributing little as any constant or linear terms over the durations of the individual data sets are absorbed by the adjusted offsets and rates. To ensure homogeneity between the data sets we average all sets to $`\tau _0=5000`$ s.

We first carry out an ordinary least squares (OLS) adjustment obtaining $`|P_{MM}|=(2.8\pm 3.6)\times 10^9`$ and $`|P_{KT}|=(4.3\pm 2.8)\times 10^7`$. The correlation coefficient between the two parameters is less than 0.01 indicating that the two are indeed well decorelated and can be determined simultaneously. All other correlation coefficients between either of the two parameters and the 14 adjusted offsets and rates are less than 0.07. We note, however, that the residuals have a significantly non-white behavior as one would expect from the slope of the Allan deviation of fig. 1. The power spectral density (PSD) of the residuals when fitted with a power law model of the form $`S_y(f)=kf^\mu `$ yields typically $`\mu 1.5`$. In the presence of non-white noise OLS is not the optimal regression method  as it can lead to significant underestimation of the parameter uncertainties .

An alternative method is weighted least squares (WLS)  which allows one to account for non-random noise processes in the original data by pre-multiplying both sides of the design equation (our equation (3) plus the 14 offsets and rates) by a weighting matrix containing off diagonal elements. To determine these off diagonal terms we first carry out OLS and adjust the $`S_y(f)=kf^\mu `$ power law model to the PSD of the post-fit residuals determining a value of $`\mu `$ for each data set. We then use these $`\mu `$ values to construct a weighting matrix following the method of fractional differencing described, for example, in . The WLS regression yields $`|P_{MM}|=(1.5\pm 3.1)\times 10^9`$ and $`|P_{KT}|=(3.1\pm 3.7)\times 10^7`$ ($`1\sigma `$ uncertainties), with the correlation coefficient between the two parameters less than 0.01 and all other correlation coefficients $`<0.07`$. The best fit power law of the WLS residuals is now compatible with $`\mu 0`$. The inset of fig. 2 shows the last data set (Sep. 2002) and the best fit model after pre-multiplication of both by the weighting matrix.

The two methods give similar results for the two parameters but we consider WLS as more reliable and take its outcome as the final results of our statistical analysis.

Systematic effects at diurnal or semi-diurnal frequencies with the appropriate phase could partially cancel a putative sidereal signal as our total data span ($``$ 293 days) allows only partial separation of the diurnal from the sidereal signal. The statistical uncertainties of $`P_{MM}`$ and $`P_{KT}`$ obtained from the WLS fit above correspond to sidereal and semi-sidereal terms (from (4)) of $`1\times 10^{15}`$ and $`6\times 10^{16}`$ respectively so any systematic effects exceeding these limits need to be taken into account in the final uncertainty. We expect the main contributions to such effects to arise from temperature, pressure and magnetic field variations that would affect the hydrogen maser, the CSO and the associated electronics, and from tilt variations of the CSO which are known to affect its frequency. Measurements of the tilt variations of the CSO show amplitudes of 4.6 $`\mu `$rad and 1.6 $`\mu `$rad at diurnal and semi-diurnal frequencies. To estimate the tilt sensitivity we have intentionally tilted the oscillator by $``$ 5 mrad off its average position which led to relative frequency variations of $`3\times 10^{13}`$ from which we deduce a tilt sensitivity of $`6\times 10^{17}\mu `$rad-1. This value corresponds to a worst case scenario as we expect a quadratic rather than linear frequency variation for small tilts around the vertical. Even with this pessimistic estimate diurnal and semi-diurnal frequency variations due to tilt do not exceed $`3\times 10^{16}`$ and $`1\times 10^{16}`$ respectively and are therefore negligible with respect to the statistical uncertainties. The temperature sensitive electronics were mounted on an actively temperature controlled panel reducing temperature fluctuations by about one order of magnitude. Temperature measurements of the CSO lab and the electronics panel taken during some of the experimental runs show room temperature variations with amplitudes of 0.3 C and 0.1 C for the diurnal and semi-diurnal components which are reduced to 0.04 C and 0.01 C on the panel. The hydrogen maser is kept in a dedicated clock room with temperature variations below the above values. Measurements of magnetic field, temperature and atmospheric pressure in that room and the maser sensitivities as specified by the manufacturer allow us to exclude any systematic effects on the maser frequency that would exceed the statistical uncertainties above. Switching off the temperature stabilization of the electronics panel shows no discernible effect so we are confident in excluding any systematic effects from that source. When heating and cooling the CSO lab by $`3^{}`$C we see frequency variations of $`5\times 10^{15}`$ per C. From the temperature measurements during the experimental runs we therefore deduce a total diurnal and semi-diurnal effect of $`1.5\times 10^{15}`$ and $`5.0\times 10^{16}`$ respectively. We assume the pessimistic scenario where all of the diurnal and semi-diurnal effect is present at the neighboring sidereal and semi-sidereal frequencies which leads (from (3)) to uncertainties from systematic effects of $`\pm 5.8\times 10^7`$ on $`P_{KT}`$ and $`\pm 2.8\times 10^9`$ on $`P_{MM}`$. We note that the phase of the perturbing systematic signal will vary over the course of our measurements due to natural causes (meteorology, daytime changes etc.) and to the sidereal/diurnal frequency difference so our final uncertainties given below are the quadratic sums of the above values and the statistical uncertainties from the WLS adjustment.

In summary, we have reported an experimental test of Lorentz invariance that simultaneously constrains two combinations of the three parameters of the Mansouri and Sexl test theory (previously measured individually by Michelson-Morley and Kennedy-Thorndike experiments). Our experiment limits $`|\delta \beta +1/2|4.2\times 10^9`$ which for the first time confirms the 1979 value of , and $`|\beta \alpha 1|6.9\times 10^7`$ which improves the best present limit  by a factor of 30. As a result, the Lorentz transformations are confirmed in this particular test theory with an overall uncertainty of $`8\times 10^7`$ limited now by the determination of $`\alpha `$ from Doppler and clock comparison experiments . This is likely to be improved in the coming years by experiments such as ACES (Atomic Clock Ensemble in Space ) that will compare ground clocks to clocks on the international space station aiming at a 10 fold improvement on the determination of $`\alpha `$. We hope to improve our experiment by a better characterization and control of systematic effects (in particular due to temperature) and by further data integration. This should allow us to improve our limits by another factor 2 or 3 in the near future.

Acknowledgements: Helpful discussions with Christophe Salomon and Gérard Petit are gratefully acknowledged as well as financial support by the Australian Research Council and CNES. P.W. is supported by CNES research grant 793/02/CNES/XXXX.

Fig. 1. Typical relative frequency stability of the CSO - H-maser difference after removal of a linear frequency drift. The inset is a schematic drawing of the cylindrical sapphire oscillator with the Poynting vector $`𝐏`$ in the whispering gallery (WG) mode, the velocity $`𝐯(t)`$ of the cylinder with respect to the CMB, and the relevant angles for a photon in the WG mode.

Fig.2. Measured relative frequency difference between the CSO and the hydrogen maser after removal of the adjusted offsets and rates, and best fit model (3) of Lorentz invariance violation (solid line). The inset shows the last data set after pre-multiplication of the data and the model by the weighting matrix of the WLS adjustment (for presentation purposes data points were averaged by a factor 2). The error bar is the maximum signal amplitude within the final 1$`\sigma `$ uncertainties of the parameters.


text:
# Phase transitions, massive gravitons and effective action in braneworld theory

## 1 Introduction

Recent developments in string theory  and the attempts to resolve the hierarchy problem  suggest that the observable world can be a brane embedded in a higher-dimensional spacetime with a certain number of noncompact dimensions. Moreover, string-inspired field theories imply the existence of several branes interacting and propagating in the multi-dimensional bulk. Their dynamics manifests itself for the observer as an effective four-dimensional theory that, in the cosmological context should explain the origin of structure in the Universe by means of an inflationary or some other scenario , explain its particle phenomenology, and shed light on problems such as a possibly observable cosmological acceleration .

The efficient way of description for the braneworld scenario is the method of effective action. Here we calculate this action in the two-brane Randall-Sundrum model within the holographic setup characteristic of the AdS/CFT-correspondence interpretation of this model  – the braneworld action as a functional of two brane geometries effectively incorporating the dynamics of multi-dimensional gravitational field in the bulk. First we dwell on the definition of this action as an alternative to the conventional Kaluza-Klein description. In the approximation quadratic in the curvature we obtain it as a nonlocal functional of two induced metrics on branes and the corresponding radion fields. We show how conventional Kaluza-Klein bulk modes arise as the set of zeros of the nonlocal form factors of the action and analyze the first two levels of the Kaluza-Klein tower – massless and massive gravitons – within the low-derivative gradient expansion. Then we consider the reduced version of this action obtained by integrating out the fields on the negative-tension brane invisible from the viewpoint of the Planckian brane observer. We show that for small interbrane separation this action describes a Brans-Dicke type theory with the nonminimally coupled radion field and local Weyl-squared short distance corrections. For large interbrane distances it explicitly features the recovery of the Einstein theory with nonlocal short-distance corrections reflecting the well-known AdS/CFT correspondence principle. The renormalization group flow responsible for this transition between the local and nonlocal phases of the theory can be realized dynamically by means of the repulsive interbrane potential of the radion field. This generates the inflationary  and other cosmological scenarios alternative to models of colliding branes .

## 2 Braneworld effective action – alternative to Kaluza-Klein reduction

Let us clarify the difference between the Kaluza-Klein and braneworld definitions of the effective actions. In Kaluza-Klein setting the construction of the effective action consists in the well-known procedure of decomposing the multi-dimensional field $`\mathrm{\Phi }(x,y)`$, where $`x`$ are the visible (four-dimensional) coordinates and $`y`$ are the coordinates of extra dimensions, in a certain complete set of harmonics $`Z_n(y)`$ on the $`y`$-space, $`\mathrm{\Phi }(x,y)=_n\varphi _n(x)Z_n(y)`$, and substituting the result into the fundamental action $`S[\mathrm{\Phi }(x,y)]`$ of the field $`\mathrm{\Phi }(x,y)`$. Subsequent integration over $`y`$ gives the effective action for an infinite tower of fields $`\{\varphi _n(x)\}`$ in $`x`$-spacetime,

$$S[\mathrm{\Phi }(x,y)]=𝑑x𝑑yL(\mathrm{\Phi }(x,y),\mathrm{\Phi }(x,y))=𝑑xL_{\mathrm{eff}}(\{\varphi _n(x)\},\{\varphi _n(x)\}).$$
(1)
The harmonics $`Z_n(x)`$ are usually taken as eigenmodes of the $`y`$-part of the full wave operator of the theory with eigenvalues $`m_n^2`$ – the masses of the Kaluza-Klein modes. This type of action was built for the two-brane Randall-Sundrum scenario in . This action, however, is very often not helpful in the braneworld context, because it does not convey a number of its important features like non-compactness of extra dimensions , recovery of the four-dimensional Einstein gravity , and its interpretation in terms of the AdS/CFT-correspondence .

These features can be described in a holographic formalism in which a natural variable is the value of the field at the brane in question, $`\varphi (x)=\mathrm{\Phi }(x,y_{\mathrm{brane}})`$. Unlike in Kaluza-Klein description, its effective action $`S_{\mathrm{eff}}[\varphi (x)]`$ is obtained from the fundamental action $`S[\mathrm{\Phi }]`$ by a more nontrivial procedure – by substituting in $`S[\mathrm{\Phi }]`$ a solution of the classical equations of motion for $`\mathrm{\Phi }(x,y)`$ in the bulk, $`\mathrm{\Phi }=\mathrm{\Phi }[\varphi (x)]`$, parametrized by their boundary values on the branes, that is $`S_{\mathrm{eff}}[\varphi (x)]=S\left[\mathrm{\Phi }[\varphi (x)]\right]`$. This construction obviously generalizes to the case of several branes $`\mathrm{\Sigma }_I`$ enumerated by the index $`I`$ and the set of brane fields $`\varphi ^I=\mathrm{\Phi }(\mathrm{\Sigma }_I)`$.

Such a definition corresponds to the tree-level approximation for the quantum effective action

$$\mathrm{exp}\left(iS_{\mathrm{eff}}[\varphi ]\right)=D\mathrm{\Phi }\mathrm{exp}\left(iS[\mathrm{\Phi }]\right)|_{\mathrm{\Phi }(\mathrm{\Sigma })=\varphi },$$
(2)
where the functional integration over the bulk fields runs subject to these brane boundary conditions. The scope of this formula is very large, because it arises in very different contexts. In particular, its Euclidean version $`(iSS_{\mathrm{Euclid}})`$ underlies the construction of the no-boundary wavefunction in quantum cosmology . Semiclassically, in the braneworld scenario, it represents a Hamilton-Jacobi functional, and its evolutionary equations of motion in the “fifth time” $`y`$ can be interpreted as renormalization-group equations . It also underlies the effective action formulation of the AdS/CFT-correspondence principle between supergravity theory on an $`AdS_5\times S^5`$ background and the superconformal field theory (super-Yang-Mills) on its infinitely remote boundary .

## 3 Two-field action in two-brane Randall-Sundrum model and massive gravitons

Here we consider the two-brane Randall-Sundrum model with $`Z_2`$ orbifold identification of points on the compactification circle of the fifth coordinate . The action of this model equals

$`S[G,g]={\displaystyle \frac{1}{16\pi G_5}}{\displaystyle d^5xG^{1/2}\left({}_{}{}^{5}R(G)2\mathrm{\Lambda }_5\right)}`$
$`+{\displaystyle \underset{I}{}}{\displaystyle _{\mathrm{\Sigma }_I}}d^4xg^{1/2}\left({\displaystyle \frac{1}{8\pi G_5}}[K]\sigma _I\right),`$ (3)
where the index $`I=\pm `$ enumerates two branes with two brane tensions $`\sigma _\pm `$ and $`[K]`$ is the trace of the extrinsic curvature jump on branes. These branes are located at antipoidal points of the circle labelled by the values of the $`y`$, $`y=y_\pm ,y_+=0,|y_{}|=d`$. $`Z_2`$-symmetry identifies the points on the circle $`y`$ and $`y`$. When the brane tensions are opposite in signs and fine tuned in magnitude to the values of the negative cosmological constant $`\mathrm{\Lambda }_5`$ and the 5-dimensional gravitational constant $`G_5`$ according to the relations

$`\mathrm{\Lambda }_5={\displaystyle \frac{6}{l^2}},\sigma _+=\sigma _{}={\displaystyle \frac{3}{4\pi G_5l}},`$ (4)
then in the absence of matter on branes this model admits the solution with the AdS metric in the bulk ($`l`$ is its curvature radius),

$`ds^2=dy^2+e^{2|y|/l}\eta _{\mu \nu }dx^\mu dx^\nu ,`$ (5)
$`0=y_+|y|y_{}=d`$, and with flat induced metric $`\eta _{\mu \nu }`$ on both branes . The metric on the negative tension brane is rescaled by the value of compactification factor $`\mathrm{exp}(2d/l)`$ providing a possible solution for the hierarchy problem . With fine tuning (4) this solution exists for arbitrary brane separation $`d`$ – two flat branes stay in equilibrium.

Take now the case when induced metrics on branes differ from the background values by perturbations

$`g_{\mu \nu }^\pm (x)=a_\pm ^2\eta _{\mu \nu }+h_{\mu \nu }^\pm (x)`$ (6)
(with $`a_\pm =a(y_\pm )`$ given in terms of the interbrane distance $`a_+=1,a_{}=e^{2d/l}a`$), which induce the perturbed solution of Einstein equations in the bulk

$`ds^2=dy^2+e^{2|y|/l}\eta _{\mu \nu }dx^\mu dx^\nu +h_{AB}(x,y)dx^Adx^B,`$ (7)
and consider the calculation of the braneworld action of the above type in the approximation quadratic in $`h_{\mu \nu }^\pm (x)`$. In the wording of Sect.2 the braneworld action of $`\varphi (x)=(g_{\mu \nu }^\pm (x),\psi ^\pm (x)`$, $`S_{\mathrm{eff}}[\varphi (x)]=S_4[g_{\mu \nu }^\pm (x),\psi ^\pm (x)]`$, is invariant under the two four-dimensional diffeomorphisms acting on the branes. In the linearized approximation they reduce to the transformations of metric perturbations, $`h_{\mu \nu }^\pm h_{\mu \nu }^\pm +f_{\mu ,\nu }^\pm +f_{\nu ,\mu }^\pm `$, with two independent local vector field parameters $`f_\mu ^\pm =f_\mu ^\pm (x)`$. Therefore the action is expressible in terms of the tensor invariants of these transformations — linearized Ricci tensors of $`h_{\mu \nu }=h_{\mu \nu }^\pm (x)`$,

$`R_{\mu \nu }^\pm ={\displaystyle \frac{1}{2}}\left(\mathrm{}h_{\mu \nu }+h_{\nu ,\lambda \mu }^\lambda +h_{\mu ,\lambda \nu }^\lambda h_{,\mu \nu }\right)^\pm ,`$ (8)
on flat four-dimensional backgrounds of both branes.

Due to metric perturbations the branes no longer stay at fixed values of the fifth coordinate. Up to four-dimensional diffeomorphisms, their embedding variables consist of two four-dimensional scalars — the radions $`\psi ^\pm (x)`$ — which also enter as arguments of the braneworld action. In the Randall-Sundrum gauge, $`h_{A5}=0`$, $`h_{\mu \nu }^{}{}_{}{}^{,\nu }=h_\mu ^\mu =0`$, these embeddings are defined by the equations

$`\mathrm{\Sigma }_\pm :y=y_\pm +{\displaystyle \frac{l}{a_\pm ^2}}\psi ^\pm (x),y_+=0,y_{}=d.`$ (9)
The answer for the braneworld action, which we advocate here, and which can be derived either by the direct substitution of the linearized solution (7) of bulk Einstein equations in (3)  or by functionally integrating effective 4-dimensional equations of motion , is given in terms of the invariant fields of the above type, $`(R_{\mu \nu }^\pm (x),\psi ^\pm (x))`$, by the following spacetime integral of a $`2\times 2`$ quadratic form,

$`S_4[g_{\mu \nu }^\pm ,\psi ^\pm ]={\displaystyle \frac{1}{16\pi G_4}}{\displaystyle }d^4x[𝐑_{\mu \nu }^T{\displaystyle \frac{2𝐅(\mathrm{})}{l^2\mathrm{}^2}}𝐑^{\mu \nu }+{\displaystyle \frac{1}{6}}𝐑^T{\displaystyle \frac{𝐊(\mathrm{})6𝐅(\mathrm{})}{l^2\mathrm{}^2}}𝐑`$
$`3(\mathrm{}𝚿+{\displaystyle \frac{1}{6}}𝐑)^T{\displaystyle \frac{𝐊(\mathrm{})}{l^2\mathrm{}^2}}(\mathrm{}𝚿+{\displaystyle \frac{1}{6}}𝐑)].`$ (10)
Here $`G_4`$ is an effective four-dimensional gravitational coupling constant,$`G_4=G_5/l`$, $`(𝐑^{\mu \nu },𝚿)`$ and $`(𝐑_{\mu \nu }^T,𝚿^T)`$ are the two-dimensional columns

$`𝐑_{\mu \nu }=\left[\begin{array}{c}R_{\mu \nu }^+(x)\\ R_{\mu \nu }^{}(x)\end{array}\right],𝚿=\left[\begin{array}{c}\psi ^+(x)\\ \psi ^{}(x)\end{array}\right]`$ (15)
and rows $`𝐑_{\mu \nu }^T=\left[R_{\mu \nu }^+(x)R_{\mu \nu }^{}(x)\right],𝚿^T=\left[\psi ^+(x)\psi ^{}(x)\right]`$ of the Ricci curvatures and radions associated with two branes. The nonlocal form factors in (10) express in terms of the nonlocal operator $`𝐅(\mathrm{})`$ the following $`2\times 2`$-matrix valued function of the $`\mathrm{}`$

$`𝐅(\mathrm{})={\displaystyle \frac{1}{J_2^+Y_2^{}J_2^{}Y_2^+}}\left[\begin{array}{cc}\sqrt{\mathrm{}}z_+u_+(z_{})& 2/\pi \\ 2/\pi & \sqrt{\mathrm{}}z_{}u_{}(z_+)\end{array}\right],`$ (18)
$`u_\pm (z)=Y_1^\pm J_2(z\sqrt{\mathrm{}})J_1^\pm Y_2(z\sqrt{\mathrm{}}),`$ (19)
$`J_\nu ^\pm J_\nu (z_\pm \sqrt{\mathrm{}}),Y_\nu ^\pm Y_\nu (z_\pm \sqrt{\mathrm{}}),`$ (20)
expressible in terms of the Bessel ($`J_\nu `$) and Neumann ($`Y_\nu `$) cylindrical functions. The second form factor $`𝐊(\mathrm{})`$ equals $`𝐊(\mathrm{})=𝐅(\mathrm{})+l^2\mathrm{}\mathrm{diag}[1,\mathrm{\hspace{0.17em}1}/a^2]`$.

The zero-eigenvalue eigenvectors of these nonlocal operators correspond to propagating modes of the theory. In the sector of transverse-traceless metric perturbations (graviton sector), for example, these modes $`𝐯_n(x)`$ are defined by the equation $`𝐅(m_n^2)𝐯_n=0`$, where $`m_n`$ are the masses of these excitations, $`(\mathrm{}m_n^2)𝐯_n(x)=0`$, given by the roots $`\mathrm{}=m_n^2`$ of the equation $`\mathrm{det}𝐅(\mathrm{})=0`$. For the operator (18) these equation reduces to

$$\mathrm{det}𝐅(\mathrm{})\mathrm{}\left(Y_1^{}J_1^+Y_1^+J_1^{}\right)=0$$
(21)
and thus gives a well-known mass spectrum of Kaluza-Klein modes in the Randall-Sundrum model, because these combination of Bessel functions is exactly the left-hand side of the eigenvalue problem for the harmonics $`Z_n(y)`$ satisfying the relevant Neumann-type boundary conditions on the two branes.

Eq. (21) shows that the massless graviton is guaranteed to exist in the spectrum, its localization on the positive-tension (Planckian) brane reflecting the recovery of Einstein theory on this brane for low energies satisfying the bounds

$$l\sqrt{\mathrm{}}1,\frac{l\sqrt{\mathrm{}}}{a}1.$$
(22)
In this domain the nonlocal form factor can be expanded in powers of derivatives to have the structure

$`{\displaystyle \frac{𝐅(\mathrm{})}{l^2}}=𝐌+𝐃\mathrm{}+O(\mathrm{}^2),`$ (23)
$`𝐌={\displaystyle \frac{1}{l^2}}{\displaystyle \frac{4}{1a^4}}\left[\begin{array}{cc}a^4& a^2\\ a^2& 1\end{array}\right],𝐃={\displaystyle \frac{1a^2}{6(1+a^2)^2}}\left[\begin{array}{cc}a^2+3& 2\\ 2& 3+a^2\end{array}\right],`$ (28)
which contains both the mass matrix $`𝐌`$ and the matrix of the kinetic term $`𝐃`$. The mass matrix is degenerate in accordance with the presence of the massless mode, $`\mathrm{det}𝐌=0`$, $`\mathrm{rank}𝐌=1`$, while the kinetic matrix is positive definite. This allows one to simultaneously diagonalize the both matrices in the basis of new fields $`h_{\mu \nu }^0`$ and $`h_{\mu \nu }^M`$, so that the low-energy action in the graviton sector describes two fields — the massless graviton and the massive transverse-traceless tensor of the mass $`M`$,

$`S_{\mathrm{graviton}}[h_{\mu \nu }^0,h_{\mu \nu }^M]={\displaystyle \frac{1}{32\pi G_4}}{\displaystyle d^4x\left(h_0\mathrm{}h_0+h_M(\mathrm{}M^2)h_M\right)},`$ (29)
$`M^2={\displaystyle \frac{24}{l^2}}{\displaystyle \frac{a^2(1+a^2)}{(1a^2)^2}}.`$ (30)
In view of standard arguments of gauge invariance under the two diffeomorphism transformations above, the massless graviton has two dynamical degrees of freedom, while the massive tensor field has all five polarizations of a generic transverse-traceless tensor field.

Strictly speaking, even the lowest-lying massive mode cannot be consistently described within the low-derivative expansion (because the mass (30) as a candidate for $`m_1^2`$ violates the second of the low-energy restrictions (22)). However, numerical calculation of the first nontrivial root, $`m_1=\sqrt{\mathrm{}}`$, of (21) shows that for a wide range of values of $`a`$ it coincides with good precision with (30). Therefore, the massive graviton mode with the mass (30) seems to provide a good description of the first non-zero level. Its application in the form of the phenomenon of radion induced graviton oscillations, potentially interesting in the gravitational wave astronomy, is considered in .

## 4 Local to nonlocal phase transitions and AdS/CFT correspondence

The difficulties with a consistent description of massive modes originate from the fact that the low-energy approximation on the Planckian brane turns out to belong the physical high-energy limit on the negative-tension brane (remember that the physical energy there is determined by the scale of $`\eta ^{\mu \nu }_\mu _\nu /a^2`$). This situation becomes even worse for large brane separation $`a=\mathrm{exp}(d/l)0`$. To avoid this difficulty let us consider the reduced version of the braneworld action corresponding to tracing (integrating) out the fields on the negative-tension brane. This procedure can be motivated by a simple physical fact that this brane is invisible from the viewpoint of the observer sitting on the Planckian brane. In the tree-level approximation this reduction, $`S_{\mathrm{eff}}[\varphi ^+,\varphi ^{}]S_{\mathrm{red}}[\varphi ^+]`$, is equivalent to the exclusion of the fields on the negative-tension brane in terms of those on the positive-tension one, $`S_{\mathrm{red}}[\varphi ^+]=S_{\mathrm{eff}}[\varphi ^+,\varphi ^{}[\varphi ^+]]`$, as solutions of their respective equations of motion, $`\delta S_{\mathrm{eff}}[\varphi ^\pm ]/\delta \varphi ^{}=0`$, $`\varphi ^{}=\varphi ^{}[\varphi ^+]`$.

Below we present the result of this reduction in two energy domains — one corresponding to (22) and another for the case of large brane separation when the second of inequalities (22) is violated. For small or finite interbrane distance in the range of (22) the low-energy reduced action has the following form

$`S_{\mathrm{red}}[g_{\mu \nu },\phi ]={\displaystyle }d^4x\sqrt{g}[({\displaystyle \frac{m_P^2}{16\pi }}{\displaystyle \frac{1}{12}}\phi ^2)R+{\displaystyle \frac{1}{2}}\phi \mathrm{}\phi `$
$`+{\displaystyle \frac{l^2m_P^2}{32\pi }}\kappa (\phi ^2)C_{\mu \nu \alpha \beta }^2],`$ (31)
$`\kappa (\phi ^2)={\displaystyle \frac{1}{4}}\left[\mathrm{ln}{\displaystyle \frac{1}{a^2}}(1a^2){\displaystyle \frac{1}{2}}(1a^2)^2\right]_{a^2=4\pi \phi ^2/3m_P^2}.`$ (32)
in terms of the new scalar field $`\phi (x)`$ — the reparametrization of the original radion field,

$$\phi (x)=\sqrt{\frac{3}{4\pi }}m_Pe^{d/l\psi (x)},$$
(33)
and the four-dimensional Planck mass, $`m_P=\sqrt{l/G_5}`$. This action represents the Eistein gravity nonminimally coupled to the Brans-Dicke type scalar $`\phi `$ describing the local, depending on $`x`$, distance between the branes and having the short distance corrections in terms of the squared Weyl tensor $`C_{\mu \nu \alpha \beta }^2`$ with local (but $`\phi `$-dependent) coeffficient (32).

For large interbrane distance corresponding to high-energy domain on the invisible brane,

$$l\sqrt{\mathrm{}}1,\frac{\sqrt{\mathrm{}}}{a}1,$$
(34)
this action has a different behavior

$`S_{\mathrm{red}}[g_{\mu \nu }]={\displaystyle \frac{m_P^2}{16\pi }}{\displaystyle d^4x\sqrt{g}\left[R+\frac{l^2}{2}C_{\mu \nu \alpha \beta }k(\mathrm{})C^{\mu \nu \alpha \beta }\right]},`$ (35)
$`k(\mathrm{})={\displaystyle \frac{1}{4}}\left(\mathrm{ln}{\displaystyle \frac{4}{l^2(\mathrm{})}}𝐂\right).`$ (36)
Radion field essentially decouples from gravity and Weyl-squared term becomes nonlocal with the logarithmic form factor characteristic of the AdS/CFT-correspondence phenomenon — immitation of quantum logarithms of conformal field theory on the brane by the tree-level (super)gravitational action calculated in the bulk .

Transition from the local phase (31) to the nonlocal phase (35) of the theory represents the renormalization group flow (AdS flow) interpolating between the limits of small and large interbrane distances. The scalar field $`\phi `$ starting at $`\phi =\sqrt{3/4\pi }m_P`$, ($`a=1`$ – the point of coinciding branes) tends to zero, ($`a0`$ – the limit of large interbrane separation). The condensate of this field in the form of the Coleman-Weinberg type of potential logarithmic in $`\phi ^2/m_P^2`$, $`\kappa (\phi ^2)`$, (32), then delocalizes into the logarithmic form factor $`k(\mathrm{})`$, (36), of the Weyl squared term. The dominant logarithmic term of $`\kappa (\phi ^2)(1/4)\mathrm{ln}(m_P^2/\phi ^2)`$ at $`\phi 0`$ instead of an infinite growth saturates at the logarithmic scale of the graviton radiation characterized by spacetime inhomogeneity of the Weyl tensor – the logarithmic nonlocality of $`k(\mathrm{})(1/4)\mathrm{ln}(4/l^2\mathrm{})`$. The physics of this transition is transparent: the tower of massive Kaluza-Klein modes which are infinitely heavy at the initial point of merging branes (see (30) at $`a1`$), for $`a0`$ becomes very light — its spectrum getting practically continuous and resulting in a cumulative effect in the form of the logarithmic nonlocality characteristic of the AdS/CFT-correspondence.

## 5 Conclusions. Radion induced inflation and dynamical realization of the AdS flow

Thus, we have constructed the holographic type braneworld action in the two-brane Randall-Sundrum model, demonstrated the existence of massive graviton modes in its spectrum and showed that it features the renormalization group flow from small to large interbrane distances associated with different, respectively, local and nonlocal phases of the theory.

From physics viewpoint it is certainly interesting to see whether this flow can be realized at the dynamical level, that is enforced as a solution of effective equations of motion. In  it was suggested that a small detuning of brane tensions from their Randall-Sundrum values (4) leads to the origin of the four-dimensional cosmological term in the action (31). Then after the reparametrization of this action to the Einstein frame of new fields $`(\overline{g}_{\mu \nu },\varphi )`$ (with $`\varphi `$ minimally coupled to $`\overline{g}_{\mu \nu }`$ and related to the old field $`\phi `$ by $`\phi =\sqrt{3/4\pi }m_P\mathrm{tanh}(\sqrt{4\pi /3}\varphi /m_P)`$) one finds that the new field $`\varphi `$ acquires the potential, $`V(\varphi )\mathrm{cosh}^4(\sqrt{4\pi /3}\varphi /m_P)`$, capable to maintane a slow-roll inflation. It corresponds to two branes diverging under the repulsive force of this interbrane potential (remember, that the limit $`\varphi 0`$ corresponds to $`a0`$) and, thus, dynamically realizes the renormalization flow of the above type. This model qualitatively differs from the inflation and other scenarios of colliding branes . Unfortunately, this model suffers from an essential drawback. This is the necessity to introduce by hand a four-dimensional cosmological constant — the brane tension detuning of the above type.

Interestingly, the present results suggest a natural mechanism of interbrane repulsion based on the Weyl-squared term of (31) and (35). When the brane Universe is filled with the graviton radiation $`C_{\mu \nu \alpha \beta }^2>0`$, and for small brane separation this term forms the interbrane potential $`(l^2/2)\kappa (\phi ^2)C_{\mu \nu \alpha \beta }^2`$. It has a maximum at the point of coinciding branes $`a=1`$ because the coefficient $`\kappa (\phi ^2)`$, Eq. (32), is strictly positive. The repelling force is very small, though, and vanishes at $`a=1`$, because of the behaviour of $`\kappa (\phi ^2)(1a^2)^3/12`$, $`a^2=4\pi \phi ^2/3m_P^2`$ (note that the expression (32) represents the logarithm $`\mathrm{ln}(1/a^2)`$ with exactly the first two terms of its Taylor series in $`(1a^2)`$ subtracted). Unfortunately, this potential is strictly negative, because $`\kappa (\phi ^2)0`$, and, therefore, cannot maintain inflation. Rather, it can serve as a basis of brane models with $`AdS_4`$ geometry embedded in $`AdS_5`$ . It can also be useful in the model of “thick” branes in the Big Crunch/Big Bang transitions of ekpyrotic and cyclic cosmologies .

Thus, the two-brane model is likely to have a natural mechanism to realize the AdS flow dynamically. Concrete implications of this flow and the corresponding transitions between the local and nonlocal phases of the theory still have to be worked out. In particular, they might be important in view of the growing interest in nonlocal modifications of gravity within the cosmological constant problem . They are currently under study.

## Acknowledgements

A.O.B. and A.Yu.K. are grateful for the hospitality of the Theoretical Physics Institute, University of Cologne, where a major part of this work has been done due to the support of the DFG grant 436 RUS 113/333/0-2. A.Yu.K. is also grateful to CARIPLO Science Foundation. The work of A.O.B. was supported by the Russian Foundation for Basic Research under the grants No 02-02-17054 and No 00-15-96566, while A.Yu.K. was supported by the RFBR grants No 02-02-16817 and No 00-15-96699. A.R. is supported by the DFG Graduiertenkolleg “Nonlinear Differential Equations”.


text:
# An Elementary Fragment of Second-Order Lambda Calculus

## 1 Introduction and Related Work

Machine-independent characterizations of computational complexity classes are at the core of the research area called *Implicit Computational Complexity* which has received a lot of attention recently. The goal is to give natural descriptions of these classes by *conceptual* means, mostly derived from mathematical logic. In particular it is desirable to go without any explicit mention of bounds or ad hoc initial functions.

The second-order, or polymorphic lambda calculus (System $`F`$)  provides a particularly natural framework for this purpose, as all data-types, such as natural numbers, binary words or trees, can be encoded therein without the use of constructors or initial functions. Unfortunately, full system $`F`$ has a computational strength far beyond anything reasonable in this context: all functions provably total in second-order arithmetic can be defined.

Recently there have been approaches to define fragments of system $`F`$ with a weaker computational strength. Altenkirch and Coquand  proposed a fragment characterizing the functions provably recursive in Peano Arithmetic by restricting type abstraction to first-order types in a single variable. Earlier, Leivant  has used stratification of type abstraction to obtain a fragment characterizing the fourth level $`𝔈_4`$ of the Grzegorczyk hierarchy .

Here we give a characterization of the third level $`𝔈_3`$ of the Grzegorczyk hierarchy, that is, the Kalmár elementary recursive functions. In order to achieve this, we use a stratification of type abstractions into only two levels. This alone would give a system in which all definable functions are elementary recursive. However, the class would presumably not be exhausted, as, for example, subtraction seems to be undefinable.

Therefore we use a primitive product type former and allow a quantified variable of the lowest level to be instantiated by a finite product of itself. Note that product types are definable in system $`F`$, however using an additional type quantifier and thus disturbing our stratification.

Different restrictions of system $`F`$ based on linear logic, and characterizing also the elementary recursive functions, as well as polynomial time, were introduced by Girard  and further elaborated by several authors .

## 2 Definitions

The elementary recursive functions are a natural subclass of the primitive recursive functions that was first defined by Kalmár . A function $`f(x,\stackrel{}{y})`$ is a bounded sum (a bounded product), if it is defined from $`g(x,\stackrel{}{y})`$ by

$$f(x,\stackrel{}{y})=\underset{i=0}{\overset{x1}{}}g(i,\stackrel{}{y})\left(\text{ resp. }f(x,\stackrel{}{y})=\underset{i=0}{\overset{x1}{}}g(i,\stackrel{}{y})\right).$$

The elementary recursive functions are the least class of number-theoretic functions that contains the constant $`0`$, all projections, successor, addition, modified subtraction $`x\dot{}y:=\mathrm{max}(xy,0)`$, multiplication and is closed under composition and bounded sums and products.

It is well-known that the elementary recursive functions coincide with the third level $`𝔈_3`$ of the Grzegorczyk hierarchy , and that they coincide as well with the functions computable in time or space bounded by an elementary recursive function (see e.g. ).

The functions $`\lambda n\mathrm{\hspace{0.17em}.\hspace{0.17em}2}_k(n)`$ for $`k`$ are inductively defined as follows: $`2_0(n)=n`$ and $`2_{k+1}(n)=2^{2_k(n)}`$. For every fixed $`k`$, this function is elementary recursive, but the binary function $`\lambda kn\mathrm{\hspace{0.17em}.\hspace{0.17em}2}_k(n)`$ is not: $`\lambda k\mathrm{\hspace{0.17em}.\hspace{0.17em}2}_k(1)`$ eventually majorizes every elementary recursive function.

### The system.

We now give a formal definition of our system, by means of a type assignment calculus. So terms are only the terms of the untyped lambda calculus with pairs, i.e., given by the grammar

$$r,s::=xrs\lambda x.rr,sr𝖫r𝖱,$$

where $`x`$ ranges over an infinite set of variables. We define types of level $`n`$ for a natural number $`n`$. However, we will use only the types of level at most $`2`$. Our type variables also come in different levels; let $`\alpha _n`$ range over variables of level $`n`$.

###### Definition.

The types $`\tau _n`$ of level $`n`$ and the flat types $`\tau _0^{}`$ of level $`0`$ are inductively given by the following grammar:

$`\tau _n`$ $`:=\alpha _n\tau _n\tau _n\tau _n\times \tau _n\alpha _k.\tau _k`$
$`\tau _0^{}`$ $`:=\alpha _0\tau _0^{}\times \tau _0^{}`$
where $`k<n`$ and $`\mathrm{𝖥𝖵}(\tau _k)\{\alpha _k\}`$.

Note that this notion of the level of a type differs from the notion commonly used in the literature, so it should more correctly be called *modified level*. However, since the usual notion is not used in the present work, for sake of brevity we just use the term *level* for the modified notion.

Also note that with respect to our notion of the level of a type, there are no closed types of level $`0`$.

### Contexts and Judgments.

A context $`\mathrm{\Gamma }`$ is a set of pairs $`x:\tau `$ of variables and types, where the variables occurring in a context have to be distinct. A typing judgment is of the form $`\mathrm{\Gamma }r:\tau `$ and expresses that $`r`$ has type $`\tau `$ in the context $`\mathrm{\Gamma }`$. The typing rules are:

$`(\text{var})`$ $`{\displaystyle \frac{}{\mathrm{\Gamma }x:\tau }}`$ $`\text{if }x:\tau \text{ occurs in }\mathrm{\Gamma }`$
$`(I)`$ $`{\displaystyle \frac{\mathrm{\Gamma },x:\sigma r:\rho }{\mathrm{\Gamma }\lambda x.r:\sigma \rho }}`$ $`(E){\displaystyle \frac{\mathrm{\Gamma }r:\sigma \rho \mathrm{\Gamma }s:\sigma }{\mathrm{\Gamma }rs:\rho }}`$
$`(\times I)`$ $`{\displaystyle \frac{\mathrm{\Gamma }r:\rho \mathrm{\Gamma }s:\sigma }{\mathrm{\Gamma }r,s:\rho \times \sigma }}`$
$`(\times E^1)`$ $`{\displaystyle \frac{\mathrm{\Gamma }r:\sigma \times \rho }{\mathrm{\Gamma }r𝖫:\sigma }}`$ $`(\times E^2){\displaystyle \frac{\mathrm{\Gamma }r:\sigma \times \rho }{\mathrm{\Gamma }r𝖱:\rho }}`$
$`(I)`$ $`{\displaystyle \frac{\mathrm{\Gamma }r:\tau _k}{\mathrm{\Gamma }r:\alpha _k.\tau _k}}`$ $`\text{if }\alpha _k\mathrm{𝖥𝖵}(\mathrm{\Gamma })`$
$`(E^1)`$ $`{\displaystyle \frac{\mathrm{\Gamma }r:\alpha _k.\tau _k}{\mathrm{\Gamma }r:\tau _k[\alpha _k:=\sigma _{\mathrm{}}]}}`$ $`\text{if }\mathrm{}k\text{ and }\mathrm{𝖥𝖵}(\sigma _{\mathrm{}})=\mathrm{}`$
$`(E^2)`$ $`{\displaystyle \frac{\mathrm{\Gamma }r:\alpha _0.\tau _0}{\mathrm{\Gamma }r:\tau _0[\alpha _0:=\sigma _0^{}]}}`$ $`\text{where }\sigma _0^{}\text{ is flat type.}`$
We will tacitly use the obvious fact that $`\mathrm{\Gamma }r:\tau `$ holds only if all the free variables of $`r`$ are assigned a type in $`\mathrm{\Gamma }`$. The rules are formulated in such a way that weakening is admissible. By a simple induction on the derivation one verifies:

###### Proposition 1 (Weakening).

If $`\mathrm{\Gamma }\mathrm{\Gamma }^{}`$ and $`\mathrm{\Gamma }r:\tau `$, then $`\mathrm{\Gamma }^{}r:\tau `$.

### Reductions.

Our system is equipped with the usual reductions of lambda calculus with pairs. Let $``$ be the reflexive and transitive closure of the reduction given by the compatible closure of the conversions below, i.e., by allowing application of these conversions to arbitrary subterms.

$`(\lambda x.r)s`$ $`r[x:=s]`$
$`r,s𝖫`$ $`r`$
$`r,s𝖱`$ $`s.`$
We denote the induced congruence relation by $`=_\beta `$, i.e., $`=_\beta `$ is the symmetric and transitive closure of $``$. For technical reasons, in some proofs we will also need the notion of $`\beta \eta `$-equality, denoted by $`=_{\beta \eta }`$. It is defined like $`=_\beta `$, but based on the conversions above together with $`\eta `$-conversion

$$\lambda x.txt$$

with the proviso that $`x`$ is not free in $`t`$.

It is easily verified that our reductions preserve typing.

###### Proposition 2 (Subject Reduction).

If $`\mathrm{\Gamma }r:\tau `$ and $`rr^{}`$, then $`\mathrm{\Gamma }r^{}:\tau `$.

### Statement of the main result.

For every type $`\tau `$, we define the type

$$\tau ^{}:=(\tau \tau )(\tau \tau ).$$

For a natural number $`n`$, the Church numeral $`\underset{¯}{n}`$ is $`\lambda fx.f^nx`$, it can have type $`\tau ^{}`$ for every $`\tau `$. The types of natural numbers are $`\mathrm{𝖭𝖺𝗍}_0:=\alpha _0.\alpha _{0}^{}{}_{}{}^{}`$ and $`\mathrm{𝖭𝖺𝗍}_1:=\alpha _1.\alpha _{1}^{}{}_{}{}^{}`$. It can be shown that the only closed normal inhabitants of the types $`\mathrm{𝖭𝖺𝗍}_i`$ are the Church numerals, and the identity combinator $`\mathrm{𝗂𝖽}:=\lambda x.x`$, which is equivalent to the numeral $`\underset{¯}{1}`$ under $`\eta `$-conversion.

A function $`f:^k`$ is *representable*, if there is a term $`t_f`$ such that $`t_f:\mathrm{𝖭𝖺𝗍}_1^k\mathrm{𝖭𝖺𝗍}_0`$ and for all $`\stackrel{}{n}^k`$, it holds that $`t_f\underset{¯}{\overset{}{n}}=_\beta \underset{¯}{f(\stackrel{}{n})}`$. We shall prove below, as Corollary 19, that the representable functions are exactly the elementary recursive functions.

### Notation.

As usual, lists of notations for terms, numbers etc. that only differ in successive indices are denoted by leaving out the indices and putting an arrow over the notation. It is usually obvious where to add the missing indices, otherwise we add dots wherever an index is left out. We use one dot if the index runs with the innermost arrow, two dots if the index runs with the next innermost arrow etc., so that e.g. the expression

$$\stackrel{}{t_{}\stackrel{}{n_,}}$$

stands for a sequence of the form

$$t_1n_{1,1}\mathrm{}n_{1,k_1},\mathrm{},t_rn_{r,1}\mathrm{}n_{r,k_r}.$$

## 3 Completeness

In this section we show one direction of our claim, namely we show that every elementary recursive function can be represented by a term. To start, it is easy to check that the usual basic arithmetic functions can have the following types

$$\begin{array}{ccccc}𝗌𝗎𝖼\hfill & :=& \lambda nsz.s(nsz)\hfill & :& \tau ^{}\tau ^{}\hfill \\ 𝖺𝖽𝖽\hfill & :=& \lambda mnsz.ms(nsz)\hfill & :& \tau ^{}\tau ^{}\tau ^{}\hfill \\ 𝗆𝗎𝗅𝗍\hfill & :=& \lambda mns.m(ns)\hfill & :& \tau ^{}\tau ^{}\tau ^{}\hfill \end{array}$$

for every $`\tau `$. We use these to program a downward typecast, that is a function

$$:=\lambda n.n𝗌𝗎𝖼\underset{¯}{0}:\tau ^{}\tau ^{}$$

with the property $`\underset{¯}{n}=_\beta \underset{¯}{n}`$. Note that $``$ also has the type $`\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{}\mathrm{𝖭𝖺𝗍}_0`$, since $`𝗌𝗎𝖼`$ can be typed as $`\mathrm{𝖭𝖺𝗍}_0\mathrm{𝖭𝖺𝗍}_0`$ by instantiating the argument $`n:\mathrm{𝖭𝖺𝗍}_0`$ as $`n:\alpha _{0}^{}{}_{}{}^{}`$. Note moreover that $`𝖺𝖽𝖽`$ and $`𝗆𝗎𝗅𝗍`$, by a similar argument, can also have type $`\mathrm{𝖭𝖺𝗍}_0\mathrm{𝖭𝖺𝗍}_0\mathrm{𝖭𝖺𝗍}_0`$.

The predecessor can be implemented of type $`\mathrm{𝖭𝖺𝗍}_0\mathrm{𝖭𝖺𝗍}_0`$ as follows: in the context where we have variables $`s:\alpha _0\alpha _0`$ and $`z:\alpha _0`$, as abstract successor and zero, we get the term $`P:=\lambda p.s(p𝖫),p𝖫`$ of type $`(\alpha _0\times \alpha _0)(\alpha _0\times \alpha _0)`$, such that the $`n`$-fold iteration of $`P`$ applied to $`z,z`$ reduces to $`s^nz,s^{n\dot{}1}z`$, for every $`n0`$. Thus the argument $`n:\mathrm{𝖭𝖺𝗍}_0`$ is instantiated as $`n:(\alpha _0\times \alpha _0)^{}`$ by the rule $`(E^2)`$, and we get

$$n:\mathrm{𝖭𝖺𝗍}_0\lambda sz.nPz,z𝖱:\alpha _{0}^{}{}_{}{}^{}$$

and an application of $`(I)`$ and $`(I)`$ yields that the predecessor $`𝗉𝗋𝖾𝖽:=\lambda nsz.nPz,z𝖱`$ is typeable as $`𝗉𝗋𝖾𝖽:\mathrm{𝖭𝖺𝗍}_0\mathrm{𝖭𝖺𝗍}_0`$.

We obtain subtraction $`𝗌𝗎𝖻:=\lambda mn.n𝗉𝗋𝖾𝖽m`$ by iterating the predecessor, of type $`𝗌𝗎𝖻:\mathrm{𝖭𝖺𝗍}_0\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{}\mathrm{𝖭𝖺𝗍}_0`$. Obviously, for $`m,n`$ we have $`𝗌𝗎𝖻\underset{¯}{m}\underset{¯}{n}=_{\beta \eta }\underset{¯}{m\dot{}n}`$.

Testing for zero can also be easily programmed as $`\chi _0:=\lambda nxy.n(\lambda z.y)x`$, which has type $`\chi _0:\mathrm{𝖭𝖺𝗍}_0\alpha _0\alpha _0\alpha _0`$, and the operational semantics if $`n=0`$ then $`x`$ else $`y`$, i.e., with the properties $`\chi _0\underset{¯}{0}xy=_\beta x`$ and $`\chi _0\underset{¯}{n+1}xy=_\beta y`$. To obtain the typing, we instantiate the input $`n:\mathrm{𝖭𝖺𝗍}_0`$ as $`n:\alpha _{0}^{}{}_{}{}^{}`$ by $`(E^2)`$.

Next we define a function $`T_0`$ such that for natural numbers $`n`$ and $`m`$, we have $`T_0\underset{¯}{0}\underset{¯}{m}=_{\beta \eta }\underset{¯}{m}`$, and $`T_0\underset{¯}{n+1}\underset{¯}{m}=_{\beta \eta }\underset{¯}{m+1}`$, as

$$T_0:=\lambda nxszs^{}z^{}.\chi _0n(s(xsz)s^{}z^{})(xszs^{}z^{})$$

The term $`T_0`$ can have the type $`\mathrm{𝖭𝖺𝗍}_0\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{}`$, which is verified as follows: in the context $`x:\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{}`$, $`s:\mathrm{𝖭𝖺𝗍}_0\mathrm{𝖭𝖺𝗍}_0`$, $`z:\mathrm{𝖭𝖺𝗍}_0`$ we obtain the terms $`xsz`$ and $`s(xsz)`$ of type $`\mathrm{𝖭𝖺𝗍}_0`$. These are instantiated with the rule $`(E^2)`$ as being of type $`\alpha _{0}^{}{}_{}{}^{}`$, and with $`s^{}:\alpha _0\alpha _0`$ and $`z^{}:\alpha _0`$ we get $`s(xsz)s^{}z^{}:\alpha _0`$ and $`xszs^{}z^{}:\alpha _0`$. Therefore we obtain

$$\mathrm{\Gamma }\lambda s^{}z^{}.\chi _0n(s(xsz)s^{}z^{})(xszs^{}z^{}):\alpha _{0}^{}{}_{}{}^{},$$

where $`\mathrm{\Gamma }`$ is the context $`n:\mathrm{𝖭𝖺𝗍}_0,x:\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{},s:\mathrm{𝖭𝖺𝗍}_0\mathrm{𝖭𝖺𝗍}_0,z:\mathrm{𝖭𝖺𝗍}_0`$, and an application of $`(I)`$ followed by several $`(I)`$ gives the claimed typing of $`T_0`$. It is easily verified by straightforward calculations that $`T_0`$ has the claimed operational behaviour.

We use $`T_0`$ to implement an upward typecast that works with the aid of a large parameter of suitable type, i.e., a term $`:\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{}\mathrm{𝖭𝖺𝗍}_0\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{}`$ with the property that $`\underset{¯}{m}\underset{¯}{n}=_{\beta \eta }\underset{¯}{n}`$ as long as $`mn`$. This can be implemented as

$$:=\lambda mn.m(\lambda x.T_0(𝗌𝗎𝖻nx)x)\underset{¯}{0},$$

i.e., the function $`\lambda x.T_0(𝗌𝗎𝖻nx)x`$, which operationally behaves as

if $`x<n`$ then $`x+1`$ else $`x`$,
is iterated $`m`$ times, starting at $`0`$, to the effect that in the first $`n`$ iterations, the value is increased by $`1`$, and thereafter the value is $`n`$, and thus remains the same.

Now by use of the typecast, a more useful type-homogeneous subtraction, but again with the aid of a large parameter, can be defined as

$$\stackrel{~}{\mathrm{𝗌𝗎𝖻}}:=\lambda mnk.m(𝗌𝗎𝖻(n)k):\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{},$$

with the property that $`\stackrel{~}{\mathrm{𝗌𝗎𝖻}}\underset{¯}{m}\underset{¯}{n}\underset{¯}{k}=_{\beta \eta }\underset{¯}{n\dot{}k}`$ as long as $`mn\dot{}k`$.

###### Definition.

For a type $`\tau `$, let $`\tau ^{(0)}:=\tau `$, and $`\tau ^{(k+1)}:=(\tau ^{(k)})^{}`$.

To iterate the above construction, assume we have a subtraction

$$\stackrel{~}{\mathrm{𝗌𝗎𝖻}}_k:\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+1)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k)},$$

and note that $`T_0`$ can have type $`\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+1)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+1)}`$ for every $`k`$, since $`\chi _0`$ can have type $`\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+1)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k)}`$ (in fact, $`\chi _0`$ can have any type of the form $`\tau ^{}\tau \tau \tau `$). Thus we can program an upward typecast

$$_k:=\lambda mn.m(\lambda x.T_0(\stackrel{~}{\mathrm{𝗌𝗎𝖻}}_k(m)n(x))x)\underset{¯}{0}$$

of type $`_k:\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+2)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+1)}`$, which again can be used to define a subtraction

$$\stackrel{~}{\mathrm{𝗌𝗎𝖻}}_{k+1}:=\lambda mn_1n_2._km\left(\stackrel{~}{\mathrm{𝗌𝗎𝖻}}_k(m)(n_1)(n_2)\right)$$

of type $`\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+2)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+1)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+1)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+1)}`$. Thus inductively we get subtractions $`\stackrel{~}{\mathrm{𝗌𝗎𝖻}}_k`$ and upward typecasts $`_k`$ for every $`k`$. We also define iterated upward typecasts $`_k^{\mathrm{}}:\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{})}`$ by

$$_k^0:=\lambda mn.n\text{and}_k^{\mathrm{}+1}:=\lambda mn._{k+\mathrm{}}m(_k^{\mathrm{}}(m)n).$$

From now on we will omit the index $`k`$ in $`_k`$, $`_k^{\mathrm{}}`$ and $`\stackrel{~}{\mathrm{𝗌𝗎𝖻}}_k`$ when it can be inferred from the context. We are ready to state our main lemma:

###### Lemma 3.

For every elementary recursive function $`f:^n`$ and $`k`$, there are a closed term $`t`$ and $`\mathrm{},r`$ and a list $`\stackrel{}{\eta }`$ of types, where each $`\eta `$ is of the form $`\eta ::=\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k)}\eta ^{}(\eta \times \eta )^{}`$, such that

$$t:\stackrel{}{\eta }\stackrel{}{\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{})}}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k)}$$

and for all $`\stackrel{}{n}^n`$, $`t\underset{¯}{\overset{}{L}}\underset{¯}{\overset{}{n}}=_{\beta \eta }\underset{¯}{f(\stackrel{}{n})}`$ as long as $`L2_r(\stackrel{}{n})`$.

Note that we plug in the same numeral $`\underset{¯}{L}`$ for all the arguments of the types $`\stackrel{}{\eta }`$. Also note that only simple types over $`\mathrm{𝖭𝖺𝗍}_0`$ are used as these types $`\stackrel{}{\eta }`$, and this is the only property used in the application and proof. A statement similar to this lemma was offered by Simmons  as a characterization of the Kalmár elementary recursive functions.

Before we prove the main lemma, we shall first use it to derive the main theorem of this section, the representability of all elementary recursive functions:

###### Theorem 4.

For every elementary recursive function $`f:^n`$ there is a closed term $`T:\mathrm{𝖭𝖺𝗍}_1^n\mathrm{𝖭𝖺𝗍}_0`$ such that $`T\underset{¯}{\overset{}{n}}=_{\beta \eta }\underset{¯}{f(\stackrel{}{n})}`$ for all $`\stackrel{}{n}^n`$.

###### Proof.

From the lemma for $`f`$ and $`k=1`$, we obtain a term $`t`$ and $`\mathrm{},r,\stackrel{}{\eta }`$ with the properties stated there. As we can always move to bigger values of $`r`$, we may without loss of generality assume $`r`$ to be at least $`2`$ and even.

Let $`s:=r/2`$. For each type $`\eta _i`$, instantiate each input $`n:\mathrm{𝖭𝖺𝗍}_1`$ as $`n:\eta _{i}^{}{}_{}{}^{(s)}`$, which is possible by $`(E^1)`$ since $`\eta _{i}^{}{}_{}{}^{(s)}`$ is a closed type of level $`1`$. Now use $`𝖺𝖽𝖽:\eta _{i}^{}{}_{}{}^{(s)}\eta _{i}^{}{}_{}{}^{(s)}\eta _{i}^{}{}_{}{}^{(s)}`$ to compute $`S:=\stackrel{}{n}`$ of type $`\eta _{i}^{}{}_{}{}^{(s)}`$. Next form the term $`N:=(\mathrm{}((S\underset{¯}{2})\underset{¯}{2})\mathrm{}\underset{¯}{2})`$, with $`r`$ occurrences of the numeral $`\underset{¯}{2}`$, of type $`\eta _i`$.

Instantiate the inputs $`\stackrel{}{n}`$ again by $`(E^1)`$ at the closed, level $`1`$ type $`\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(\mathrm{})}`$, and form $`T:=\lambda \stackrel{}{n}.(t\stackrel{}{N}\stackrel{}{n})`$. As for every input $`\stackrel{}{n}`$, $`N`$ evaluates to a numeral $`\underset{¯}{L}`$ with $`L2_r(\stackrel{}{n})`$, the term $`T`$ has the required properties, by the lemma. ∎

###### Corollary 5.

For every elementary recursive function $`f:^n`$ there is a closed term $`T:\mathrm{𝖭𝖺𝗍}_1^n\mathrm{𝖭𝖺𝗍}_0`$ such that $`T\underset{¯}{\overset{}{n}}\underset{¯}{f(\stackrel{}{n})}`$ for all $`\stackrel{}{n}^n`$.

###### Proof.

Take $`\lambda \stackrel{}{n}sz.T\stackrel{}{n}sz`$ for the term $`T`$ obtained from the theorem. For every $`\stackrel{}{n}`$ consider the $`\beta `$-normal of $`(\lambda \stackrel{}{n}sz.T\stackrel{}{n}sz)\underset{¯}{\overset{}{n}}`$, which is a closed, $`\beta `$-normal term of type $``$, starting with two abstractions, hence a numeral. So it has to be $`\underset{¯}{f(\stackrel{}{n})}`$, for otherwise two distinct numeral would be $`\beta \eta `$-equal, which by the well known confluence of lambda calculus with pairs is not the case. ∎

###### Proof of the Lemma.

We have produced terms representing the base functions successor, addition, subtraction and multiplication above. For $`S`$, $`+`$ and $`\times `$, we can set $`\mathrm{}=r=0`$ and $`\stackrel{}{\eta }`$ empty for any $`k`$.

Concerning subtraction $`\dot{}`$, for $`k=0`$ we use the term $`\lambda nk.𝗌𝗎𝖻(n)k`$ and set $`r=0`$, $`\mathrm{}=1`$ and $`\stackrel{}{\eta }`$ empty, and for $`k1`$ we use $`\stackrel{~}{\mathrm{𝗌𝗎𝖻}}_k`$, and we set $`\mathrm{}=r=0`$ and $`\stackrel{}{\eta }`$ contains the single type $`\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+1)}`$.

In the following, note that by the properties of $``$, whenever we have a term $`t`$ of type $`\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{})}`$, we can obtain a term $`^{\mathrm{}}t`$ with the same value of type $`\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k)}`$.

For closure under composition, let $`f(\stackrel{}{n})=g(\stackrel{}{h_{}(\stackrel{}{n})})`$ and $`k`$ be given. By the induction hypothesis for $`g`$ and $`k`$, we have a term $`t_g`$, numbers $`\mathrm{}_g`$ and $`r_g`$ and a list $`\stackrel{}{\eta }`$ of types such that the claim of the lemma holds for these.

Also, the induction hypothesis for each $`h_i`$ and $`k+\mathrm{}_g`$ yields terms $`t_i`$ and $`\mathrm{}_i,r_i`$ and types $`\stackrel{}{\eta _{,i}}`$, such that the claim holds for these.

Let $`\mathrm{}:=\mathrm{}_g+\mathrm{max}_i\mathrm{}_i`$. Since the functions $`h_i`$ are elementary recursive, $`h_i(\stackrel{}{n})`$ is also elementary, and therefore there is an $`s`$ such that $`_ih_i(\stackrel{}{n})2_s(\stackrel{}{n})`$. For variables $`\stackrel{}{v}`$ and $`\stackrel{}{w_{,i}}`$, which we give the types $`\stackrel{}{\eta }`$ and $`\stackrel{}{\eta _{,i}}`$, respectively, we set

$$t:=\lambda \stackrel{}{v}\stackrel{}{\stackrel{}{w}}\stackrel{}{n}.t_g\stackrel{}{v}\stackrel{}{(t_{}\stackrel{}{w_,}\stackrel{}{(^\mathrm{}\mathrm{}_g\mathrm{}_{}n_{})})}$$

such that $`t`$ has type $`\stackrel{}{\eta }\stackrel{}{\stackrel{}{\eta }}\stackrel{}{\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{})}}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k)}`$. By the induction hypothesis, for $`r:=\mathrm{max}(r_g+s,\stackrel{}{r})`$ we have $`t\underset{¯}{\overset{}{L}}\stackrel{}{\underset{¯}{\overset{}{L}}}\underset{¯}{\overset{}{n}}=_{\beta \eta }\underset{¯}{f(\stackrel{}{n})}`$ as long as $`L2_r(\stackrel{}{n})`$.

For closure under bounded sums, let $`f(\stackrel{}{n},m)=_{i=0}^{m1}g(\stackrel{}{n},i)`$ and $`k`$ be given. By the induction hypothesis for $`g`$ and $`k+1`$, we have a term $`t_g`$, numbers $`\mathrm{}`$ and $`r`$ and a list $`\stackrel{}{\eta }`$ of types such that the claim of the lemma holds. Define

$$\stackrel{~}{\chi }_0:=\lambda nxysz.\chi _0n(xsz)(ysz)$$

of type $`(\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)})^3\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)}`$, with the same operational semantics as $`\chi _0`$, i.e., for $`i,j`$ we have $`\stackrel{~}{\chi }_0\underset{¯}{0}\underset{¯}{i}\underset{¯}{j}=_{\beta \eta }\underset{¯}{i}`$ and $`\stackrel{~}{\chi }_0\underset{¯}{n+1}\underset{¯}{i}\underset{¯}{j}=_{\beta \eta }\underset{¯}{j}`$. For variables $`v:\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+2)}`$, $`\stackrel{}{w}`$ of the types $`\stackrel{}{\eta }`$ and $`\stackrel{}{n},m`$ of type $`\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)}`$, we have

$$T:=\lambda xy.\stackrel{~}{\chi }_0(\stackrel{~}{\mathrm{𝗌𝗎𝖻}}vmy)x(𝖺𝖽𝖽x(^{\mathrm{}}v(t_g\stackrel{}{w}\stackrel{}{n}y))),$$

of type $`\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)}`$.

As long as a sufficiently large numeral $`\underset{¯}{L}`$ is substituted for the variables $`v`$ and $`\stackrel{}{w}`$, $`T`$ operationally behaves as

> if $`y<m`$ then $`x+g(\stackrel{}{n},y)`$ else $`x`$.

More precisely, $`L`$ has to be large enough so that all values of $`g(\stackrel{}{n},i)`$ are computed correctly, that is, $`L2_r(\stackrel{}{n}+m)`$, and we need $`Lg(\stackrel{}{n},i)`$ for the typecast $`^{\mathrm{}}`$ to work properly. Next, we define

$$P:=\lambda p.T(p𝖫)(p𝖱),𝗌𝗎𝖼(p𝖱)$$

of type $`(\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)}\times \mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)})(\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)}\times \mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)})`$. When this term, having the operational semantics

$$s,i\{\begin{array}{cc}s+g(\stackrel{}{n},i),i+1\hfill & \text{if }i<m\hfill \\ s,i+1\hfill & \text{otherwise,}\hfill \end{array}$$

is iterated starting from the pair $`0,0`$, by use of a sufficiently large numeral of type $`(\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)}\times \mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)})^{}`$, the values $`g(\stackrel{}{n},i)`$ for $`i=0,\mathrm{},m1`$ are summed up in the left component. Thus to represent $`f`$, we define the term

$$t:=\lambda uv\stackrel{}{w}\stackrel{}{n}m.^{\mathrm{}+1}\left(uP\underset{¯}{0},\underset{¯}{0}𝖫\right)$$

of type

$$(\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)}\times \mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+1)})^{}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k+\mathrm{}+2)}\stackrel{}{\eta }\stackrel{}{\mathrm{𝖭𝖺𝗍}^{(k+\mathrm{}+1)}}\mathrm{𝖭𝖺𝗍}_{0}^{}{}_{}{}^{(k)}$$

By the induction hypothesis and the construction, we get the property that $`t\underset{¯}{L}\underset{¯}{L}\underset{¯}{\overset{}{L}}\underset{¯}{\overset{}{n}}\underset{¯}{m}=_{\beta \eta }\underset{¯}{f(\stackrel{}{n},m)}`$ as long as $`L`$ is sufficiently large. To be more precise, $`L`$ needs to satisfy the requirements above for $`T`$ to be computed correctly, and $`Lm`$ in order to complete the summation. Therefore, let $`s`$ be such that for every $`m`$ and $`im`$ we have $`g(\stackrel{}{n},i)2_s(\stackrel{}{n}+m)`$, which exists since $`g`$ is elementary recursive, and let $`r^{}:=\mathrm{max}(r,s)`$. Then all conditions on $`L`$ are satisfied if $`L2_r^{}(\stackrel{}{n}+m)`$.

Closure under bounded products is shown in the same way, only with $`𝖺𝖽𝖽`$ in the definition of $`T`$ replaced by $`𝗆𝗎𝗅𝗍`$, and the iteration of $`P`$ is started at $`1,0`$. ∎

## 4 Soundness

In this section we show the other direction of our claim, that is, we show that every term of type $`\mathrm{𝖭𝖺𝗍}_1\mathrm{𝖭𝖺𝗍}_0`$ denotes a function on Church numerals computable in elementary space. The main idea is to use the elementary bound for traditional cut-elimination in propositional logic. In this section we will deal only with types of level at most $`1`$, so let $`\tau `$, $`\rho `$, $`\sigma `$ range over those types within this section. Note that every instantiation of $`\mathrm{𝖭𝖺𝗍}_1`$ is a type of level $`1`$. Types of level $`0`$ and $`1`$ are almost simple types (corresponding to propositional logic) with the exception of quantification of $`\alpha _0`$. These quantifiers however, can only be instantiated with flat types of the form $`\alpha _0\times \mathrm{}\times \alpha _0`$. Hence we can get a notion of cut-rank that is invariant under generalization and instantiation of level $`0`$, if we ignore pairs. Fortunately we can do so, as the reduction of a pair-redex reduces the size of the term and hence does not do any harm. So we define the rank $`\mathrm{rk}(\tau )`$ of a type $`\tau `$ inductively as follows:

$`\mathrm{rk}(\alpha )`$ $`:=0`$
$`\mathrm{rk}(\rho \times \sigma )`$ $`:=\mathrm{max}(\mathrm{rk}(\rho ),\mathrm{rk}(\sigma ))`$
$`\mathrm{rk}(\rho \sigma )`$ $`:=\mathrm{max}(\mathrm{rk}(\rho )+1,\mathrm{rk}(\sigma ))`$
$`\mathrm{rk}(\alpha .\rho )`$ $`:=\mathrm{rk}(\rho )`$
We inductively define a relation $`\mathrm{\Gamma }_k^mr:\tau `$ saying that $`\mathrm{\Gamma }r:\tau `$ can be derived by a typing derivation of height $`m`$ and cut-rank $`k`$:

$`(\text{var}){\displaystyle \frac{}{\mathrm{\Gamma }_k^mx:\tau }}`$ $`\text{if }x:\tau \text{ occurs in }\mathrm{\Gamma }\text{ and }m,k0`$
$`(I){\displaystyle \frac{\mathrm{\Gamma },x:\sigma _k^mr:\rho }{\mathrm{\Gamma }_k^{m+1}\lambda x.r:\sigma \rho }}`$
$`(E){\displaystyle \frac{\mathrm{\Gamma }_k^mr:\sigma \rho \mathrm{\Gamma }_k^m^{}s:\sigma }{\mathrm{\Gamma }_k^{m^{\prime \prime }}rs:\rho }}`$ $`\text{if }\mathrm{rk}(\sigma )<k`$
$`(\times I){\displaystyle \frac{\mathrm{\Gamma }_k^mr:\rho \mathrm{\Gamma }_k^m^{}s:\sigma }{\mathrm{\Gamma }_k^{m^{\prime \prime }}r,s:\rho \times \sigma }}`$
$`(\times E^1){\displaystyle \frac{\mathrm{\Gamma }_k^mr:\sigma \times \rho }{\mathrm{\Gamma }_k^{m+1}r𝖫:\sigma }}`$ and analogous for $`(\times E^2)`$
$`(I){\displaystyle \frac{\mathrm{\Gamma }_k^mr:\tau }{\mathrm{\Gamma }_k^{m+1}r:\alpha .\tau }}`$ $`\text{if }\alpha \mathrm{𝖥𝖵}(\mathrm{\Gamma })`$
$`(E^2){\displaystyle \frac{\mathrm{\Gamma }_k^mr:\alpha .\tau }{\mathrm{\Gamma }_k^{m+1}r:\tau [\alpha :=\sigma ^{}]}}`$ $`\text{where }\sigma ^{}\text{ is a flat type.}`$
where $`m^{\prime \prime }:=\mathrm{max}(m,m^{})+1`$. As the rules are precisely those of our typing judgment for types of level at most $`1`$, we have the following property for typing derivations of level at most $`1`$: if $`\mathrm{\Gamma }r:\tau `$ then there are $`m`$, $`k`$ such that $`\mathrm{\Gamma }_k^mr:\tau `$. On the other hand, the following property obviously holds and motivates our interest in this notion:

$$\mathrm{\Gamma }_k^mr:\tau \text{implies}|r|2^m$$

The rules are formulated in such a way that weakening is admissible.

###### Proposition 6 (Weakening).

If $`\mathrm{\Gamma }_k^mr:\tau `$, $`\mathrm{\Gamma }^{}\mathrm{\Gamma }`$, $`m^{}m`$, $`k^{}k`$ then $`\mathrm{\Gamma }^{}_k^{}^m^{}r:\tau `$.

The next proposition, which can be shown by a trivial induction on $`\tau _0^{}`$ or $`\tau `$, respectively, explains formally why we can allow instantiations with flat types of level $`0`$ without any harm: the rank is not altered!

###### Proposition 7.

For a flat type $`\tau _0^{}`$ of level $`0`$ we have $`\mathrm{rk}(\tau _0^{})=0`$ and $`\mathrm{rk}(\tau [\alpha _0:=\tau _0^{}])=\mathrm{rk}(\tau )`$.

Knowing that the rank of a type is not altered by substituting in a flat type, the cut-rank, being a rank, is not altered as well, hence an induction on $`\mathrm{\Gamma }_k^mt:\tau `$ shows:

###### Proposition 8.

If $`\mathrm{\Gamma }_k^mt:\tau `$ and $`\tau _0^{}`$ is a flat type of level $`0`$ then $`\mathrm{\Gamma }[\alpha _0:=\tau _0^{}]_k^mt:\tau [\alpha _0:=\tau _0^{}]`$

Using this proposition a simple induction on $`m`$ shows that a derivation $`\mathrm{\Gamma }_k^mt:\tau `$ can be transformed in such a way that the rule $`(I)`$ is never followed by $`(E^2)`$. So from now on we tacitly assume all derivations to be free from those $`(I)`$-$`(E^2)`$-redexes, as for example in the proof of the next proposition, which then is a simple analysis of the last rule of the derivation.

###### Proposition 9.

If $`\mathrm{\Gamma }_k^mr,s𝖫:\rho `$ then $`\mathrm{\Gamma }_k^mr:\rho `$ and if $`\mathrm{\Gamma }_k^mr,s𝖱:\sigma `$ then $`\mathrm{\Gamma }_k^ms:\sigma `$.

As usual, induction on the first derivation shows that cuts can be performed at the cost of summing up heights.

###### Lemma 10.

If $`\mathrm{\Gamma },x:\rho _k^ms:\sigma `$ and $`\mathrm{\Gamma }_k^m^{}r:\rho `$ then $`\mathrm{\Gamma }_k^{m+m^{}}s[x:=r]:\sigma `$.

In order to be able to reduce the cut rank, we first show an “inversion”-lemma, that is, we show that under certain conditions terms of arrow-type can be brought into abstraction form.

###### Lemma 11 (Inversion).

If $`\mathrm{rk}(\mathrm{\Gamma })k`$ and $`\mathrm{\Gamma }_k^mt:\rho \sigma `$ where $`\mathrm{rk}(\rho )k`$, then there are $`t^{}`$ and $`x`$ with $`t=_\beta \lambda x.t^{}`$ such that $`\mathrm{\Gamma },x:\rho _k^mt^{}:\sigma `$.

###### Proof.

Induction on $`m`$ and case distinction according to $`t`$.

The case $`t=x\stackrel{}{s}`$ is impossible, since $`x`$ would have to occur in $`\mathrm{\Gamma }`$ and hence $`\mathrm{rk}(\mathrm{\Gamma })>k`$. The case $`t=r,s\stackrel{}{t}`$ is also impossible since $`\stackrel{}{t}`$ has to be empty, as we assume $`t`$ to be free of pair-redexes, and therefore $`t`$ would have to have a pair type.

So the only remaining case is that $`t`$ is of the form $`t=(\lambda y.r)\stackrel{}{t}`$. The claim is trivial if $`\stackrel{}{t}`$ is empty. So without loss of generality we might assume $`t`$ to be $`t=(\lambda y.r)s\stackrel{}{s}`$, with $`y`$ not free in $`s,\stackrel{}{s}`$. The abstraction $`\lambda y.r`$ must have been introduced from a derivation $`\mathrm{\Gamma },y:\tau _k^mr:\stackrel{~}{\tau }`$ with $`\mathrm{rk}(\tau )<k`$ for otherwise the cut would not have been allowed. Hence, for some $`m^{}`$ with $`m^{}+2m`$ we get

$$\mathrm{\Gamma },y:\tau _k^m^{}r\stackrel{}{s}:\rho \sigma \text{ and }\mathrm{\Gamma }_k^{m^{}+1}s:\tau $$

Hence by the induction hypothesis we get a new variable $`x`$ and a term $`t^{}`$ such that $`r\stackrel{}{s}=_\beta \lambda x.t^{}`$ and $`\mathrm{\Gamma },y:\tau ,x:\rho _k^m^{}t^{}:\sigma `$. From that we conclude $`\mathrm{\Gamma },x:\rho _k^{m^{}+2}(\lambda y.t^{})s:\sigma `$ and note $`\lambda x.(\lambda y.t^{})s=_\beta \lambda x.t^{}[y:=s]=(\lambda x.t^{})[y:=s]=_\beta (r\stackrel{}{s})[y:=s]=r[y:=s]\stackrel{}{s}=_\beta (\lambda y.r)s\stackrel{}{s}=t`$, hence the claim. ∎

###### Lemma 12 (Cut-rank reduction).

If $`\mathrm{\Gamma }_{k+1}^mt:\rho `$, $`\mathrm{rk}(\mathrm{\Gamma })k`$, and $`\mathrm{rk}(\rho )k+1`$ then $`\mathrm{\Gamma }_k^{2^m}t^{}:\rho `$ for some $`t^{}=_\beta t`$.

###### Proof.

Induction on $`m`$. The only interesting cases are $`(I)`$ and $`(E)`$. Concerning $`(I)`$ we are in the situation that $`\mathrm{\Gamma }_{k+1}^{m+1}\lambda x.r:\sigma \tau `$ was concluded from $`\mathrm{\Gamma },x:\sigma _{k+1}^mr:\tau `$. With $`\rho =\sigma \tau `$ we have $`\mathrm{rk}(\mathrm{\Gamma })k`$, $`\mathrm{rk}(\sigma )<\mathrm{rk}(\rho )k+1`$ and $`\mathrm{rk}(\tau )\mathrm{rk}(\rho )k+1`$. Hence an application of the induction hypothesis yields $`\mathrm{\Gamma },x:\sigma _k^{2^m}r^{}:\tau `$ from which we conclude $`\mathrm{\Gamma }_k^{2^m+1}\lambda x.r^{}:\sigma \tau `$ which, by weakening, suffices, since $`2^m+12^{m+1}`$.

Concerning the case $`(E)`$ we are in the situation that $`\mathrm{\Gamma }_{k+1}^{m+1}ts:\rho `$ was concluded from $`\mathrm{\Gamma }_{k+1}^mt:\sigma \rho `$ and $`\mathrm{\Gamma }_{k+1}^ms:\sigma `$. The only case that is not immediate by the induction hypothesis is if $`\mathrm{rk}(\sigma )=k`$. Then the induction hypothesis gives us $`\mathrm{\Gamma }_k^{2^m}t^{}:\sigma \rho `$ for some $`t^{}=_\beta t`$. By our assumption $`\mathrm{rk}(\mathrm{\Gamma })k`$, hence by inversion we get $`\mathrm{\Gamma },x:\sigma _k^{2^m}t^{\prime \prime }:\rho `$ for some new $`x`$ and $`t^{\prime \prime }`$ such that $`\lambda x.t^{\prime \prime }=_\beta t^{}=_\beta t`$. Also by the induction hypothesis we get $`\mathrm{\Gamma }_k^{2^m}s:\sigma `$. By Lemma 10 we get $`\mathrm{\Gamma }_k^{2^m+2^m}t^{\prime \prime }[x:=s]:\rho `$ which yields the claim since $`t^{\prime \prime }[x:=s]=_\beta (\lambda x.t^{\prime \prime })s=_\beta ts`$. ∎

###### Corollary 13.

If $`_{k+1}^mt:\alpha ^{}`$ then $`_1^{2_k(m)}t^{}:\alpha ^{}`$ for some $`t^{}=_\beta t`$.

###### Proposition 14.

If $`t`$ normal and $`\mathrm{\Gamma }t:\tau _0^{}`$ for some $`\mathrm{\Gamma }`$ with $`\mathrm{rk}(\mathrm{\Gamma })1`$ then $`t`$ is $`\lambda `$-free.

###### Proof.

Inspection of the typing rules yields that the only rule introducing a $`\lambda `$ is $`(I)`$, which creates an arrow-type. In order for the whole term to be of arrow-free type, the rule $`(E)`$ has to be used, either creating a redex or requiring a variable of rank at least $`2`$. ∎

###### Definition.

A term $`t`$ is *quasinormal*, if every redex in $`t`$ is of the form $`r,s𝖫`$ or $`r,s𝖱`$ with $`\lambda `$-free $`r`$ and $`s`$

We remark the trivial property that the normal form of a quasinormal term $`t`$ can be computed in space bound by the length of $`t`$. We also note that Proposition 14 also holds for quasinormal terms, since the only types discarded by a redex are those of terms which are $`\lambda `$-free by definition. Moreover, a simple induction on $`t`$ shows:

###### Proposition 15.

If $`t`$ is quasinormal and $`s`$ is $`\lambda `$-free and quasinormal then $`t[x:=s]`$ is quasinormal.

From that proposition, Proposition 14 and Lemma 10 we immediately get:

###### Corollary 16.

If $`\mathrm{\Gamma },x:\sigma ^{}_1^mr:\rho `$ and $`\mathrm{\Gamma }_1^m^{}s:\sigma ^{}`$ and $`r`$ and $`s`$ are quasinormal then $`\mathrm{\Gamma }_1^{m+m^{}}r[x:=s]:\rho `$ and $`r[x:=s]`$ is quasinormal.

This corollary allows us to show our last ingredient for the soundness theorem: we can transform a term with cut-rank $`1`$ into a quasinormal one at exponential cost.

###### Lemma 17.

If $`\mathrm{\Gamma }_1^mt:\tau `$ then $`\mathrm{\Gamma }_1^{2^m}t^{}:\tau `$ for some quasinormal $`t^{}`$ with $`t^{}=_\beta t`$.

###### Proof.

Induction on $`m`$. If $`t`$ is not quasinormal, it has a subterm of the form $`(\lambda x.r)s`$. Then, for some $`\mathrm{\Delta }`$, $`\sigma `$, $`\rho `$ and $`k`$ we have $`\mathrm{\Delta },x:\sigma _1^kr:\rho `$, and $`\mathrm{\Delta }_1^{k+1}s:\sigma `$ from which $`\mathrm{\Delta }_1^{k+2}(\lambda x.r)s:\rho `$ was concluded. Since the cut was allowed, we have $`\mathrm{rk}(\sigma )<1`$. Hence, by the induction hypotheses we get a quasinormal $`s^{}=_\beta s`$ such that $`\mathrm{\Delta }_1^{2^{k+1}}s^{}:\sigma `$. Also by induction hypothesis we get a quasinormal $`r^{}=_\beta r`$ such that $`\mathrm{\Delta },x:\sigma _1^{2^k}r^{}:\rho `$. By Corollary 16 we get $`\mathrm{\Delta }_1^{2^k+2^{k+1}}r^{}[x:=s^{}]:\rho `$ and $`r^{}[x:=s^{}]`$ is quasinormal, hence the claim. ∎

We are now ready to show that every representable function is elementary recursive. To keep the notation simple, we only state and prove this for unary functions, but the generalization to higher arities is straightforward.

###### Theorem 18.

If $`t:\mathrm{𝖭𝖺𝗍}_1\mathrm{𝖭𝖺𝗍}_0`$ then $`t`$ denotes an elementary function on Church numerals.

###### Proof.

We have $`x:\mathrm{𝖭𝖺𝗍}_1tx:\mathrm{𝖭𝖺𝗍}_0`$. Since all our terms are also typeable in usual system $`F`$, hence strongly normalizing, and since subject reduction holds, we can find (in maybe long time, which however is independent of the input) a normal term $`t^{}=_\beta tx`$ and $`x:\mathrm{𝖭𝖺𝗍}_1t^{}:\mathrm{𝖭𝖺𝗍}_0`$. Since $`t^{}`$ is normal, inspection of the typing rules yields that every occurrence of $`x`$ must be within some context, that is, of the form

$$(E^1)\frac{x:\mathrm{𝖭𝖺𝗍}_1x:\mathrm{𝖭𝖺𝗍}_1}{x:\mathrm{𝖭𝖺𝗍}_1x:\xi ^{}}$$

for some level $`1`$ type $`\xi `$, without (free) variable $`\alpha _1`$. Let $`c`$ be the maximum of the ranks of all the $`\xi `$’s occurring in that derivation and $`k`$ the number of occurrences of such $`\xi `$’s (note that $`c`$ and $`k`$ are still independent of the input).

Now, let a natural number $`n`$ be given. Replacing all $`x:\xi ^{}`$ by derivations of $`\underset{¯}{n}:\xi ^{}`$ yields a term $`t^{\prime \prime }=_\beta t\underset{¯}{n}`$ and a derivation $`_c^{k(n+2)+2|t^{}|}t^{\prime \prime }:\mathrm{𝖭𝖺𝗍}_0`$. The bound on the height of the derivation is obtained as follows: there are $`k`$ derivations of height $`n+2`$ yielding $`n:\xi ^{}`$ and these are plugged into the derivation of $`t^{}:\mathrm{𝖭𝖺𝗍}_0`$. In the latter derivation there is at most one inference for each symbol in $`t^{}`$ followed possible by a single quantifier inference.

Using Corollary 13 we obtain a term $`\stackrel{~}{t}=_\beta t^{\prime \prime }=_\beta t\underset{¯}{n}`$ such that$`_1^{2_{c+1}(k(n+2)+2|t^{}|)}\stackrel{~}{t}:\mathrm{𝖭𝖺𝗍}_0`$. Hence Lemma 17 and the remark on computing the normal form of a quasinormal term provides means to calculate the normal form of $`t\underset{¯}{n}`$ in elementary space. (Note that all the intermediate terms are also of elementary bounded size.) ∎

Together with Theorem 4 we obtain the claimed characterization.

###### Corollary 19.

The representable functions are precisely the elementary recursive functions.

Note that our characterization does not mean that the normalization procedure for terms typeable in our system is elementary recursive. The following easy counterexample shows that this is indeed not the case: the terms $`(\mathrm{}((\underset{¯}{2}\underset{¯}{2})\underset{¯}{2})\mathrm{}\underset{¯}{2})`$ with $`n`$ occurrences of $`\underset{¯}{2}`$ are of size $`O(n)`$, but their normal forms are the numerals $`\underset{¯}{2_n(1)}`$ of size $`\mathrm{\Omega }(2_n(1))`$. Thus the normalization function has super-elementary growth.