Armelle Jardin-Blicq

# The gamma-ray emission from 3HWC J1928+178

###### Abstract

The gamma-ray source 3HWC J1928+178, discovered by HAWC, is coincident with
the 82 kyr pulsar PSR J1928+1746, located 4 kpc away. It has not been reported
by any Imaging atmospheric Cherenkov Telescope (IACT), until the recent
detection of emission from this region by H.E.S.S., using an analysis adapted
to extended sources. No counterpart in GeV gamma-rays from Fermi-LAT data or
in X-ray has been reported so far. In this contribution, I give the
multiwavelength context of the region surrounding 3HWC J1928+178 and present a
multi-component model derived using the Multi-Mission Maximum Likelihood
framework (3ML). I explore the possibility to model the gamma-ray emission of
3HWC J1928+178 by an extended source with continuous diffuse emission.
Together with the age of the pulsar and its extended nature, it may indicate a
transition from a pulsar wind nebulae to a halo, where the electrons have
started to cool and diffuse away from the source.

##  1 Introduction

###  1.1 Astrophysical context

3HWC J1928+178 ($\ell=52.93$°, $b=0.2$°) is a gamma-ray source discovered by
HAWC and reported in the 3HWC catalogue [1] at the significance level of $\sim
15\sigma$. No Imaging Atmospheric Cherenkov Telescope (IACT) has detected it
before the confirmation by the H.E.S.S. collaboration[2], using an analysis
method adapted to extended sources. The origin of the observed very high
energy gamma-ray emission is still unclear. It may be associated with the
pulsar PSR J1928+1746, discovered at radio wavelength [3], although neither
the pulsar nor the pulsar wind nebulae (PWN) has been detected in the X-ray
energy range. In the vicinity of 3HWC J1928+178 is another HAWC source, 3HWC
J1930+188 ($\ell=54.03$°, $b=0.32$°), also detected by H.E.S.S. [4] and
VERITAS [5], associated with the PWN in the supernova remnant SNR G54.1+0.3.
It hosts the pulsar PSR 1930+1852. Finally, another energetic pulsar is
located nearby, PSR J1932+1916, associated with the Fermi source 3FGL
J1932.2+1916. The characteristics of the three pulsars are gathered in Table
1.

Table 1:  Characteristics of the pulsars located in the vicinity of 3HWC J1928+178 taken from the ATNF catalogue [6].  | PSR J1928+1746 | PSR J1930+1852 | PSR J1932+1916
---|---|---|---
celestial coordinates (ra °, dec °) | (292.18,17.77) | (292.62,18.87) | (293.08,19.28)
galactic coordinates (l °, b °) | (52.93,0.11) | (54.1,0.26) | (54.67,0.09)
distance (kpc) | 4.3 | 6.2 | -
age (kyr) | 82.6 | 2.9 | 35.4
period (s) | 0.069 | 0.14 | 0.21
spin down power (erg s-1) | $1.6\times 10^{36}$ | $1.2\times 10^{37}$ | $4.1\times 10^{35}$

###  1.2 The HAWC observatory and HAWC Data

The High Altitude Water Cherenkov (HAWC) gamma-ray observatory is located at a
latitude of 19°N in Mexico, and at 4100 m in altitude. HAWC is composed of 300
water tanks instrumented with four photomultiplier tubes (PMT). When the
secondary particles of an atmospheric air shower passes through HAWC, they
produce Cherenkov light in the water tanks and each PMT records the time and
amplitude of the signal. Combining the information of all the PMTs, we can
build the footprint of the shower on the detector and reconstruct the
parameters of the air shower. Each event is assigned to one of the 9 analysis
bin depending on the fraction of the water tanks that has been hit. Bin
definitions are given in [7]. For this analysis, 1523 days of HAWC data are
used and events falling in the analysis bins 4 to 9 are selected. It
corresponds to events triggering more than 25% of the array, which gives an
energy threshold of approximately 1 TeV. For this specific bin selection, the
sources 3HWC J1928+178 is refered to as HAWC J1928+178 in [2]. The
corresponding PSF of the instrument is $\sim$0.4° for bin 4 and decreases to
less than 0.2° for bin 9. More information about the detector, the event
reconstruction and the data analysis can be found in [8] and [7].

##  2 Modeling the region around 3HWC J1928+178

A multi-component fit based on a maximum likelihood approach is performed
using the Multi-Mission Maximum Likelihood framework (3ML) [9] and the HAWC
HAL111https://github.com/threeML/hawc_hal plugin. A model is defined for a
3.5° radius region around 3HWC J1928+178, convolved with the instrument
response and compared to the corresponding experimental data. Two models are
considered, described in the following paragraphs.

###  2.1 The four components model

Following an iterative procedure, a first model is defined composed of 2
components: a point-like component and an extended symmetric Gaussian
component at the location of the two HAWC sources 3HWC J1930+188 and 3HWC
1928+178 respectively. This choice is motivated by the fact that 3HWC
J1930+188 was detected as a point-like source by HAWC, H.E.S.S. [4] and
VERITAS [5], and by previous studies of 3HWC J1928+178 that showed that it is
likely extended [2] [10]. A simple power law
$\mbox{dN/dE}=\mbox{F}_{0}(\mbox{E}/\mbox{E}_{0})^{\Gamma}$ is assumed as
energy spectrum for all components. The fit is performed with the position,
size of the extended source, flux normalisation $\mbox{F}_{0}$ at
$\mbox{E}_{0}=10$ TeV and spectral index $\Gamma$ as free parameters. For each
model, a test statistic (TS) is computed that compares the likelihood that the
region is represented by the model against the hypothesis that there is
background fluctuations only:
$\mbox{TS}=2~{}\mbox{ln}(\mathcal{L}(\mbox{model})/\mathcal{L}(\mbox{background}))$.
According to Wilks’ theorem, the quantity TS follows a $\chi^{2}$ distribution
of N degrees of freedom, with N the difference in number of free parameters
between the model and the background [11]. If an excess is found in the
residual maps, a new component is added at the location of the excess and the
fit is performed again with the additional component. The procedure stops when
the addition of a new component does not improve the fit by more than
$\Delta\mbox{TS}=25$. The best model is found to be made of two point-like
sources close to the location of the pulsars PSR J1930+1852 and PSR
J1932+1916, and two extended sources represented by symmetric Gaussians. The
first one is found to have a size $\sigma=0.18$° (39% containment) and is
located at the position of 3HWC J1928+178. The second one is very extended
with a size $\sigma=1.43$° and seems to cover the whole region, likely trying
to account for some large scale gamma-ray emission, maybe diffuse emission
from the galactic plane. The output parameters can be found in Table 2 and the
model can be visualised on the top right panel of Figure 1.

###  2.2 The diffusion emission model

Alternatively, a diffusion model is considered for 3HWC J1928+178, assuming a
continuous injection of electrons and positrons at the location of the
remaining excess for 3HWC J1928+178 after the first fit. Similar to the
Geminga analysis [12], it is motivated by the fact that PSR J1928+1746 is a
rather old pulsar, that we don’t see any X-ray counterpart and that the
$\gamma$-ray emission seems extended. Indeed, the four components model shows
that 3HWC J1928+178 seems to be described by a superposition of a small
Gaussian on top of a very wide one, which are both incorporated in this
diffuse component for 3HWC J1928+178. This model is thus composed of three
components only: two point-like and one extended component with diffuse
emission. As described in [12], the $\gamma$-ray flux $f_{d}$ for 3HWC
J1928+178, as a function of the distance from the source $d$, is approximately
equal to:

$f_{d}=\frac{1.22}{\pi^{3/2}r_{d}(d+0.06r_{d})}\mbox{exp}\frac{-d^{2}}{r_{d}^{2}}$
(1)

where $r_{d}$ is the diffusion radius that is a free parameter fitted together
with the position of the three components and their spectral parameter. The
diffusion radius is found to be 2.68°. All the output parameters are gathered
in Table 2 and the model can be visualised on the bottom right panel of Figure
1.

Figure 1: Left: HAWC significance map with the location of the HAWC sources and the location of the pulsars. The white circle is the region of interest of 3.5° radius. Right: Significance map of the 4 components model at the top and the diffusion model at the bottom, with the position and size of each fitted components. Each map is 3.5° in radius.  Table 2:  Output values from the fit for the components of the two different models representing 3HWC J1928+178.  | 4 components model | diffusion model
---|---|---
hypothesis | Gaussian 1 | Gaussian 2 | continuous injection
(ra °, dec °) | (292.15±0.03, 17.90$\pm$0.04) | (292.05$\pm$0.15, 18.10$\pm$0.17) | (292.10$\pm$0.06, 17.98$\pm$ 0.02)
size ($\sigma$ or $r_{d}$) (°) | 0.18 $\pm$ 0.03 | 1.43 $\pm$ 0.16 | 2.68 $\pm$ 0.27
index | -2.09 $\pm$ 0.15 | -2.60 $\pm$ 0.08 | -2.58 $\pm$ 0.05
flux${}_{\mbox{\tiny 10 TeV}}$ ($\times 10^{-15}$ | 4.2 ${}_{\mbox{\tiny-1.1}}^{\mbox{\tiny+1.5}}$ | 40 ${}_{\mbox{\tiny-4}}^{\mbox{\tiny+5}}$ | 47 ${}_{\mbox{\tiny-5}}^{\mbox{\tiny+5}}$
TeV-1 cm-2 s-1)

##  3 Comparison between the 2 models

The diffusion model is slightly worse by $\Delta$TS = 8 than the model with 4
components (2 point-like and 2 extended sources) but it has less degrees of
freedom since it has only 3 components. To account for the difference in
number of degrees of freedom we can look at the Bayesian information criterion
number (BIC) for the two non-nested models used here [13], given by this
formula : $\mbox{BIC}=-2~{}\mbox{ln}(\mathcal{L})+k\mbox{ln}(n)$ where $k$ is
the number of free parameters and $n$ is the number of healpix pixels in the
ROI. It seems that the diffusion model is largely preferred with a difference
of $\Delta\mbox{BIC}=45$. Figure 2 shows the radial profiles centered on 3HWC
J1928+178 of the HAWC data, and for the two models. The profile of the Crab
nebula is plotted as a reference for the HAWC PSF, showing that the emission
is indeed extended. The profiles of both models follow closely the data.

Figure 2:  Radial profile centered on J1928 in step of 0.2°, for the HAWC data
(blue) with its standard deviation (grey band), the diffuse model (red) and
the 4 components model (green). The profile of the models is plotted for the
region of interest of 2° only. The profile of the crab nebula is also plotted
(black) as a reference for the HAWC PSF.  Figure 3: Spectral energy
distribution of 3HWC J1928+178 for the two models presented in this
contribution, for the energy range 3.5 - 51 TeV, corresponding to the median
energies of bin 4 and 9. The spectrum from the HAWC catalogue search for the
same analysis bins [2] and the flux point from LHAASO are also plotted for
comparison [14]. The shaded area correspond to the 1$\sigma$ statistical
uncertainties.

The spectral energy distribution is plotted in Figure 3 for the component
representing the source 3HWC J1928+178 for the two models. It is compared with
the spectrum from the HAWC automatic source search for the same set of data
[2]. The flux point from LHAASO [14] seems to be more compatible with the 4
components model, or imply a cut-off in the power low spectrum from the
diffusion model.

##  4 Discussion and conclusion

The 4 components model and the diffusion model are very similar in the sense
that they are in agreement with the hypotheses that 3HWC J1928+178 is
extended, and that the presence of a very large scale component is needed,
either maybe due the galactic diffuse emission in one case, or to the
diffusion of e± in the second case. The diffusion model, with 1 component less
and a lower BIC, seemed favoured. It may indicate that 3HWC J1928+178 is in a
transition phase to a TeV gamma-ray halo: the pulsar being rather old, the TeV
gamma-ray emission being extended, and the fact that no PWN has been detected
in X-ray are favouring this hypothesis. However, the fitted diffusion radius
$r_{d}$ is found to be 2.68°, i.e $\sim 400$ pc in diameter, since PSR
J1928+1746 is located 4.3 kpc away. It is huge compared to Geminga which has a
diffusion radius of 5.5° but is only 250 pc away from us, giving a size of 23
pc in diameter. This may disfavour this model. Moreover, the spectrum for 3HWC
J1928+178 from the 4 components model is in better agreement with the
measurement from LHAASO. A deeper study at the highest energy, using the
energy estimators developed by the HAWC collaboration [15] instead of the
analysis bins would help to clarify the presence of a cut-off.

## Acknowledgments

We acknowledge the support from: the US National Science Foundation (NSF); the
US Department of Energy Office of High-Energy Physics; the Laboratory Directed
Research and Development (LDRD) program of Los Alamos National Laboratory;
Consejo Nacional de Ciencia y Tecnología (CONACyT), México, grants 271051,
232656, 260378, 179588, 254964, 258865, 243290, 132197, A1-S-46288,
A1-S-22784, cátedras 873, 1563, 341, 323, Red HAWC, México; DGAPA-UNAM grants
IG101320, IN111716-3, IN111419, IA102019, IN110621, IN110521; VIEP-BUAP; PIFI
2012, 2013, PROFOCIE 2014, 2015; the University of Wisconsin Alumni Research
Foundation; the Institute of Geophysics, Planetary Physics, and Signatures at
Los Alamos National Laboratory; Polish Science Centre grant,
DEC-2017/27/B/ST9/02272; Coordinación de la Investigación Científica de la
Universidad Michoacana; Royal Society - Newton Advanced Fellowship 180385;
Generalitat Valenciana, grant CIDEGENT/2018/034; Chulalongkorn University’s
CUniverse (CUAASC) grant; Coordinación General Académica e Innovación (CGAI-
UdeG), PRODEP-SEP UDG-CA-499; Institute of Cosmic Ray Research (ICRR),
University of Tokyo, H.F. acknowledges support by NASA under award number
80GSFC21M0002. We also acknowledge the significant contributions over many
years of Stefan Westerhoff, Gaurang Yodh and Arnulfo Zepeda Dominguez, all
deceased members of the HAWC collaboration. Thanks to Scott Delay, Luciano
Díaz and Eduardo Murrieta for technical support.

## References

  * [1] A. Albert, R. Alfaro, C. Alvarez, J.R.A. Camacho, J.C. Arteaga-Velázquez, K.P. Arunbabu et al., _3HWC: The Third HAWC Catalog of Very-high-energy Gamma-Ray Sources_ , _Astrophysical Journal_ 905 (2020) 76 [2007.08582].
  * [2] H. Abdalla, F. Aharonian, F.A. Benkhali, E.O. Angüner, C. Arcaro, C. Armand et al., _Tev emission of galactic plane sources with HAWC and H.E.S.S._ , 2021.
  * [3] J.M. Cordes, P.C.C. Freire, D.R. Lorimer, F. Camilo, D.J. Champion, D.J. Nice et al., _Arecibo Pulsar Survey Using ALFA. I. Survey Strategy and First Discoveries_ , _The Astrophysical Journal_ 637 (2006) 446 [astro-ph/0509732].
  * [4] H. E. S. S. Collaboration, H. Abdalla, A. Abramowski, F. Aharonian, F.A. Benkhali, E.O. Angüner et al., _The H.E.S.S. Galactic plane survey_ , _A &A_ 612 (2018) A1 [1804.02432].
  * [5] V.A. Acciari, E. Aliu, T. Arlen, T. Aune, M. Bautista, M. Beilicke et al., _Discovery of Very High Energy $\gamma$-ray Emission from the SNR G54.1+0.3_, _ApJL_ 719 (2010) L69 [1005.0032].
  * [6] R.N. Manchester, G.B. Hobbs, A. Teoh and M. Hobbs, _The australia telescope national facility pulsar catalogue_ , _The Astrophysical Journal_ 129 (2005) 1993.
  * [7] A.U. Abeysekara, A. Albert, R. Alfaro, C. Alvarez, J.D. Álvarez, R. Arceo et al., _Observation of the Crab Nebula with the HAWC Gamma-Ray Observatory_ , _ApJ_ 843 (2017) 39 [1701.01778].
  * [8] A.J. Smith and HAWC Collaboration, _HAWC: Design, Operation, Reconstruction and Analysis_ , in _34th International Cosmic Ray Conference (ICRC2015)_ , vol. 34 of _International Cosmic Ray Conference_ , p. 966, July, 2015 [1508.05826].
  * [9] G. Vianello, R.J. Lauer, P. Younk, L. Tibaldo, J.M. Burgess, H. Ayala et al., _The Multi-Mission Maximum Likelihood framework (3ML)_ , _Proceedings of the 34th ICRC, The Hague, Netherlands_ (2015) [1507.08343].
  * [10] R. López-Coto, V. Marandon, F. Brun, for the HAWC collaboration and the HESS collaboration, _Morphological and spectral measurements of 2HWC J1928+177 with HAWC and H.E.S.S._ , _Proceedings of the 35th ICRC, Busan, Korea_ (2017) .
  * [11] S.S. Wilks, _The Large-Sample Distribution of the Likelihood Ratio for Testing Composite Hypotheses_ , _The Annals of Mathematical Statistics_ 9 (1938) 60 .
  * [12] A.U. Abeysekara, A. Albert, R. Alfaro, C. Alvarez, J.D. Álvarez, R. Arceo et al., _Extended gamma-ray sources around pulsars constrain the origin of the positron flux at Earth_ , _Science_ 358 (2017) 911 [1711.06223].
  * [13] G. Schwarz, _Estimating the Dimension of a Model_ , _The Annals of Statistics_ 6 (1978) 461 .
  * [14] Z. Cao, F. Aharonian, Q. An, Axikegu, L.X. Bai, Y.X. Bai et al., _Ultrahigh-energy photons up to 1.4 petaelectronvolts from 12 gamma-ray Galactic sources_ , _Nature_ 594 (2021) 33–36.
  * [15] A.U. Abeysekara, A. Albert, R. Alfaro, C. Alvarez, J.D. Álvarez, J.R.A. Camacho et al., _Measurement of the Crab Nebula Spectrum Past 100 TeV with HAWC_ , _The astrophysical Journal_ 881 (2019) 134 [1905.12518].

## Full Authors List: HAWC Collaboration

A.U. Abeysekara48, A. Albert21, R. Alfaro14, C. Alvarez41, J.D. Álvarez40,
J.R. Angeles Camacho14, J.C. Arteaga-Velázquez40, K. P. Arunbabu17, D. Avila
Rojas14, H.A. Ayala Solares28, R. Babu25, V. Baghmanyan15, A.S. Barber48, J.
Becerra Gonzalez11, E. Belmont-Moreno14, S.Y. BenZvi29, D. Berley39, C.
Brisbois39, K.S. Caballero-Mora41, T. Capistrán12, A. Carramiñana18, S.
Casanova15, O. Chaparro-Amaro3, U. Cotti40, J. Cotzomi8, S. Coutiño de León18,
E. De la Fuente46, C. de León40, L. Diaz-Cruz8, R. Diaz Hernandez18, J.C.
Díaz-Vélez46, B.L. Dingus21, M. Durocher21, M.A. DuVernois45, R.W.
Ellsworth39, K. Engel39, C. Espinoza14, K.L. Fan39, K. Fang45, M. Fernández
Alonso28, B. Fick25, H. Fleischhack51,11,52, J.L. Flores46, N.I. Fraija12, D.
Garcia14, J.A. García-González20, J. L. García-Luna46, G. García-Torales46, F.
Garfias12, G. Giacinti22, H. Goksu22, M.M. González12, J.A. Goodman39, J.P.
Harding21, S. Hernandez14, I. Herzog25, J. Hinton22, B. Hona48, D. Huang25, F.
Hueyotl-Zahuantitla41, C.M. Hui23, B. Humensky39, P. Hüntemeyer25, A.
Iriarte12, A. Jardin-Blicq22,49,50, H. Jhee43, V. Joshi7, D. Kieda48, G J.
Kunde21, S. Kunwar22, A. Lara17, J. Lee43, W.H. Lee12, D. Lennarz9, H. León
Vargas14, J. Linnemann24, A.L. Longinotti12, R. López-Coto19, G. Luis-Raya44,
J. Lundeen24, K. Malone21, V. Marandon22, O. Martinez8, I. Martinez-
Castellanos39, H. Martínez-Huerta38, J. Martínez-Castro3, J.A.J. Matthews42,
J. McEnery11, P. Miranda-Romagnoli34, J.A. Morales-Soto40, E. Moreno8, M.
Mostafá28, A. Nayerhoda15, L. Nellen13, M. Newbold48, M.U. Nisa24, R. Noriega-
Papaqui34, L. Olivera-Nieto22, N. Omodei32, A. Peisker24, Y. Pérez Araujo12,
E.G. Pérez-Pérez44, C.D. Rho43, C. Rivière39, D. Rosa-Gonzalez18, E. Ruiz-
Velasco22, J. Ryan26, H. Salazar8, F. Salesa Greus15,53, A. Sandoval14, M.
Schneider39, H. Schoorlemmer22, J. Serna-Franco14, G. Sinnis21, A.J. Smith39,
R.W. Springer48, P. Surajbali22, I. Taboada9, M. Tanner28, K. Tollefson24, I.
Torres18, R. Torres-Escobedo30, R. Turner25, F. Ureña-Mena18, L. Villaseñor8,
X. Wang25, I.J. Watson43, T. Weisgarber45, F. Werner22, E. Willox39, J.
Wood23, G.B. Yodh35, A. Zepeda4, H. Zhou30

1Barnard College, New York, NY, USA, 2Department of Chemistry and Physics,
California University of Pennsylvania, California, PA, USA, 3Centro de
Investigación en Computación, Instituto Politécnico Nacional, Ciudad de
México, México, 4Physics Department, Centro de Investigación y de Estudios
Avanzados del IPN, Ciudad de México, México, 5Colorado State University,
Physics Dept., Fort Collins, CO, USA, 6DCI-UDG, Leon, Gto, México, 7Erlangen
Centre for Astroparticle Physics, Friedrich Alexander Universität, Erlangen,
BY, Germany, 8Facultad de Ciencias Físico Matemáticas, Benemérita Universidad
Autónoma de Puebla, Puebla, México, 9School of Physics and Center for
Relativistic Astrophysics, Georgia Institute of Technology, Atlanta, GA, USA,
10School of Physics Astronomy and Computational Sciences, George Mason
University, Fairfax, VA, USA, 11NASA Goddard Space Flight Center, Greenbelt,
MD, USA, 12Instituto de Astronomía, Universidad Nacional Autónoma de México,
Ciudad de México, México, 13Instituto de Ciencias Nucleares, Universidad
Nacional Autónoma de México, Ciudad de México, México, 14Instituto de Física,
Universidad Nacional Autónoma de México, Ciudad de México, México, 15Institute
of Nuclear Physics, Polish Academy of Sciences, Krakow, Poland, 16Instituto de
Física de São Carlos, Universidade de São Paulo, São Carlos, SP, Brasil,
17Instituto de Geofísica, Universidad Nacional Autónoma de México, Ciudad de
México, México, 18Instituto Nacional de Astrofísica, Óptica y Electrónica,
Tonantzintla, Puebla, México, 19INFN Padova, Padova, Italy, 20Tecnologico de
Monterrey, Escuela de Ingeniería y Ciencias, Ave. Eugenio Garza Sada 2501,
Monterrey, N.L., 64849, México, 21Physics Division, Los Alamos National
Laboratory, Los Alamos, NM, USA, 22Max-Planck Institute for Nuclear Physics,
Heidelberg, Germany, 23NASA Marshall Space Flight Center, Astrophysics Office,
Huntsville, AL, USA, 24Department of Physics and Astronomy, Michigan State
University, East Lansing, MI, USA, 25Department of Physics, Michigan
Technological University, Houghton, MI, USA, 26Space Science Center,
University of New Hampshire, Durham, NH, USA, 27The Ohio State University at
Lima, Lima, OH, USA, 28Department of Physics, Pennsylvania State University,
University Park, PA, USA, 29Department of Physics and Astronomy, University of
Rochester, Rochester, NY, USA, 30Tsung-Dao Lee Institute and School of Physics
and Astronomy, Shanghai Jiao Tong University, Shanghai, China, 31Sungkyunkwan
University, Gyeonggi, Rep. of Korea, 32Stanford University, Stanford, CA, USA,
33Department of Physics and Astronomy, University of Alabama, Tuscaloosa, AL,
USA, 34Universidad Autónoma del Estado de Hidalgo, Pachuca, Hgo., México,
35Department of Physics and Astronomy, University of California, Irvine,
Irvine, CA, USA, 36Santa Cruz Institute for Particle Physics, University of
California, Santa Cruz, Santa Cruz, CA, USA, 37Universidad de Costa Rica, San
José , Costa Rica, 38Department of Physics and Mathematics, Universidad de
Monterrey, San Pedro Garza García, N.L., México, 39Department of Physics,
University of Maryland, College Park, MD, USA, 40Instituto de Física y
Matemáticas, Universidad Michoacana de San Nicolás de Hidalgo, Morelia,
Michoacán, México, 41FCFM-MCTP, Universidad Autónoma de Chiapas, Tuxtla
Gutiérrez, Chiapas, México, 42Department of Physics and Astronomy, University
of New Mexico, Albuquerque, NM, USA, 43University of Seoul, Seoul, Rep. of
Korea, 44Universidad Politécnica de Pachuca, Pachuca, Hgo, México,
45Department of Physics, University of Wisconsin-Madison, Madison, WI, USA,
46CUCEI, CUCEA, Universidad de Guadalajara, Guadalajara, Jalisco, México,
47Universität Würzburg, Institute for Theoretical Physics and Astrophysics,
Würzburg, Germany, 48Department of Physics and Astronomy, University of Utah,
Salt Lake City, UT, USA, 49Department of Physics, Faculty of Science,
Chulalongkorn University, Pathumwan, Bangkok 10330, Thailand, 50National
Astronomical Research Institute of Thailand (Public Organization), Don Kaeo,
MaeRim, Chiang Mai 50180, Thailand, 51Department of Physics, Catholic
University of America, Washington, DC, USA, 52Center for Research and
Exploration in Space Science and Technology, NASA/GSFC, Greenbelt, MD, USA,
53Instituto de Física Corpuscular, CSIC, Universitat de València, Paterna,
Valencia, Spain


Left bipositions: $\mathtt{asc}(a,\,x,\,k\cdot c)=(a\cdot\ell,\,x,\,k\cdot
c)$, where $\ell\geqslant 0$ is the unique integer such that
$(a\cdot\ell,\,x,\,k\cdot c)\in{\mathtt{bisupp}(P)}$.

    * –

Right bipositions ($\mathtt{abs}$): if $t(\overline{a})=\lambda x$,
$\mathtt{asc}(a,\,\varepsilon)=(a\cdot
0,\,\varepsilon),~{}\mathtt{asc}(a,\,1\cdot c)=(a\cdot 0,\,c)$ and
$\mathtt{asc}(a,\,k\cdot c)=(a\cdot 0,\,x,\,k\cdot c)$ if $k\geqslant 2$.

    * –

Right bipositions ($\mathtt{app}$): if $t(\overline{a})=\char 64\relax$,
$\mathtt{asc}(a,\,c)=(a\cdot 1,\,1\cdot c)$.

  * •

$\mathtt{Asc}(\mathtt{p})$ is a right biposition and is defined as the highest
right biposition related to $\mathtt{p}$ by $\mathtt{asc}$.

    * –

Right bipositions: if $\mathtt{p}=(a,c)$, let $h$ be maximal such that
$\mathtt{asc}^{h}(\mathtt{p})$ is defined. In that case, we set
$\mathtt{Asc}(\mathtt{p})=\mathtt{asc}^{h}(\mathtt{p})$.

    * –

Left bipositions: if $\mathtt{p}=(a,x,k\cdot c)$, let $h$ be maximal (if it
exists) such that $\mathtt{asc}^{h}(\mathtt{p})$ exists. In that case,
$\mathtt{asc}^{h}(\mathtt{p})$ is of the form $(a_{0},x,k\cdot c)$ with
$t(a_{0})=x$. We set then $\mathtt{Asc}(\mathtt{p})=(a_{0},c)$.

Since $t\in\Lambda^{001}$ (and not in $\Lambda^{111}\setminus\Lambda^{001}$),
$\mathtt{Asc}(\mathtt{p})$ is defined for any right biposition $\mathtt{p}$.
If $P$ is quantitative, then $\mathtt{Asc}(\mathtt{p})$ is also defined for
any left biposition.

An examination of the $\mathtt{app}$-rule shows that, if $t(a)=\char
64\relax$, for all $k\geqslant 2$ and $c\in\mathbb{N}^{*}$:

$(a\cdot 1,k\cdot c)\leftrightarrow(a\cdot k,c)\hskip 28.45274pt(E1)$

Indeed, if $t|_{a}=u\,v$ is typed—say that $u:(k\cdot S_{k})_{{k\in
K}}\rightarrow T$ and
$(v:S_{k}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[k]})_{k\in
K}$—the domain of the arrow typing $u$ correspond to the types assigned to the
argument $u$ (if $c\in\mathtt{supp}(S_{k})$, then $(a\cdot 1,k\cdot c)$ and
$(a\cdot k,c)$ are both in ${\mathtt{bisupp}(P)}$).

Now, assume that $P$ is still quantitative, $t|_{b}=(\lambda x.r)s$,
$a\in{\mathtt{bisupp}(P)}$, $\overline{a}=b$,
$k\in\mathtt{Tr}^{\lambda}_{P}(a)$. Thus, $t|_{a\cdot 1}=\lambda x.r:(k\cdot
S_{k})_{{k\in K}}\rightarrow T$ and
$(s:S_{k}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[k]})_{k\in
K}$. Let $c\in\mathtt{supp}(S_{k})$ and $\mathtt{p}:=(a\cdot 1,k\cdot
c)\in{\mathtt{bisupp}(P)}$. Notice that $\mathtt{asc}{p}=(a\cdot 10,x,k\cdot
c)$ and $\mathtt{Asc}(\mathtt{p})=(a\cdot 10\cdot a_{k},c)$. Thus:

$(a\cdot 1,k\cdot c)\leftrightarrow(a\cdot 10\cdot a_{k},c)\hskip
28.45274pt(E2)$

In particular, by $(E1)$ and $(E2)$:

$(a\cdot 10\cdot a_{k},\,c)\leftrightarrow(a\cdot k,\,c)$

This relation specifies that the types of the occurrences of $x$ match the
types of the argument $s$ of the redex, i.e., if $c\in\mathtt{supp}(S_{k})$,
both $(a\cdot k,c)$ (pointing in $s:S_{k}$) and $(a\cdot 10\cdot a_{k},c)$
(pointing in $x:S_{k}$) are in ${\mathtt{bisupp}(P)}$.

######  Lemma 53.

Assume that $P$ is quantitative, $P\stackrel{{\scriptstyle
b}}{{\rightarrow}}_{\\!\beta}P^{\prime}$, $t|_{a}=(\lambda x.r)s$ and
$\mathtt{p}\in{\mathtt{bisupp}(P)}$. If $\mathtt{Res}_{b}(\mathtt{p})$ is not
defined, one of the following cases occur:

  * •

If $\mathtt{p}$ is a left-biposition $(\alpha,y,k\cdot c)$ with
$\mathtt{Asc}(\mathtt{p})=:(\alpha_{*},c)$:

    * –

If $y\neq x$, then
$\mathtt{p}\leftrightarrow\mathtt{p}_{0}:=\mathtt{Asc}(\mathtt{p})$ and
$\mathtt{Res}_{b}(\mathtt{p}_{0})$ is defined.

    * –

If $y=x$, then $\alpha_{*}=a\cdot 10\cdot a_{k}$ for some $a$ and $k$ such
that $\overline{a}=b$ and $k\in\mathtt{Tr}^{\lambda}_{P}(a)$. Then
$\mathtt{p}\leftrightarrow\mathtt{p}_{0}:=(a\cdot 1,k\cdot c)$ by $(E3)$ and
$\mathtt{Res}_{b}(\mathtt{p}_{0})$ is defined.

  * •

If $\mathtt{p}$ is a right-biposition $(\alpha,c)$ with
$\mathtt{Asc}(\mathtt{p})=:(\alpha_{*},c_{*})$, then $\alpha=a\cdot
10\cdot\alpha_{0}$ for some $a$ such that $\overline{a}=b$:

    * –

If $t|_{a_{*}}=y\neq x$, then
$\mathtt{p}\leftrightarrow\mathtt{p}_{0}:=\mathtt{Asc}(\mathtt{p})$ and
$\mathtt{Res}_{b}(\mathtt{p}_{0})$ is defined.

    * –

If $t|_{a_{*}}=x$, let $k:=\mathtt{tr}^{P}(a_{*})$ and
$\mathtt{p}_{0}:=(a\cdot k,c_{*})$. Then
$\mathtt{p}\leftrightarrow\mathtt{p}_{0}$ and
$\mathtt{Res}_{b}(\mathtt{p}_{0})$ is defined by $(E3)$.

###### Proof.

The cases resorting to $(E3)$ are justified in the statement. Let us check
that we are exhaustive. Notice first that, when $\mathtt{p}$ is a left-
biposition, $\mathtt{Asc}(\mathtt{p})$ is always defined since $P$ is
quantitative. Moreover, when $(\alpha_{*},c):=\mathtt{Asc}(\mathtt{p})$, then
$t(\alpha_{*})=y$ for some $y\in\mathscr{V}$ ($\alpha_{*}$ points to an
$\mathtt{ax}$-rule).

  * •

If $y\neq x$, $\mathtt{Res}_{b}(\alpha_{*})$ and thus
$\mathtt{Res}_{b}(\alpha_{*},c)$ are both defined.

  * •

If $y=x$, $\mathtt{Asc}(\mathtt{p})$ is of the form $(a\cdot 10\cdot a_{k},c)$
for some $a$ satisfying $\overline{a}=b$. But, by $(E3)$,
$\mathtt{Asc}(\mathtt{p})$ is equinecessary to $(a\cdot k,c)$ (pointing inside
$s$), which always has a residual by definition of $\mathtt{Res}_{b}$.

∎

One then notices that Observation 25, which is crucial to prove correctness
(Lemma 6.3), is a corollary of Lemma 53.

###  C.3. Uniform Subject Expansion

We prove now the uniform subject expansion property for system $\mathtt{S}$.
By uniform, we mean that we use a function
$\lfloor\cdot\rfloor:\mathbb{N}\rightarrow\mathbb{N}^{*}$ to decide the value
of the axiom tracks in the axiom rules created during anti-reduction.
Uniformity is crucial to ensure that subject expansion is monotonic.

Assuming $t|_{b}=(\lambda x.r)s$ and $t\stackrel{{\scriptstyle
b}}{{\rightarrow}}_{\\!\beta}t^{\prime}$, we will built a derivation $P$
typing $t$ from a derivation $P^{\prime}$ typing $t^{\prime}$. The
constructions is based on the following observation: there are three kinds of
positions in $t^{\prime}$: (1) positions outside the reduct $r[s/x]$ (2)
positions inside $r$ (but outside an occurrence of $s$) (3) positions inside
an occurrence of $s$. Things are a bit less clear in $t$: we have (1)
positions outside the redex $(\lambda x.r)s$ (2) positions inside $r$ (3)
positions inside $s$ (4) positions corresponding to the application or the
abstraction of the redex $(\lambda x.r)s$. Moreover, inside $r$, one should
distinguish positions corresponding to $x$ (which is destroyed during
reduction) and the other positions. All this has been illustrated with Fig.
12.

Hypotheses. Let $P^{\prime}\rhd\Gamma\vdash t^{\prime}:\tau$ a quantitative
$\mathtt{S}$ derivation with $t^{\prime}|_{b}=r[s/x]$ and $t$ the term such
that $t|_{b}=(\lambda x.r)s$ and $t\stackrel{{\scriptstyle
b}}{{\rightarrow}}_{\\!\beta}t^{\prime}$. Let $\lfloor\cdot\rfloor$ be an
injective function from $\mathbb{N}\setminus\\{0,1\\}$ to $\mathtt{N}^{*}$. We
set $A^{\prime}=\mathtt{supp}(P^{\prime})$.

Building the support of $P$. We first build $A:=\mathtt{supp}(P)$ and a quasi-
residuation function $QR_{b}$ from $A$ to $A^{\prime}$.

We write $\mathtt{T}^{\prime}$, $\mathtt{C}^{\prime}$ and
$\mathtt{tr}^{\prime}$ for $\mathtt{T}^{P^{\prime}}$,
$\mathtt{C}^{P^{\prime}}$ and $\mathtt{tr}^{P^{\prime}}$. We set
$B=\mathtt{supp}(t)$, $B^{\prime}=\mathtt{supp}(t^{\prime})$ and
$A^{\prime}=\mathtt{supp}(P)$. Let $B_{x}=\\{\beta\in B\,|\,t(\beta)=x\\}$ (we
assume Barendregt convention),
$B^{\prime}_{s\varepsilon}=\mathtt{Res}_{b}(B)$,
$B^{\prime}_{s}={\beta^{\prime}_{0}\cdot\beta^{\prime}_{1}\in
B^{\prime}\,|\,\beta^{\prime}_{0}\in B^{\prime}_{s\varepsilon}}$ and
$A_{b}=\mathtt{Rep}_{P^{\prime}}(b)$,
$A^{\prime}_{s\varepsilon}=\\{\alpha^{\prime}\in
A^{\prime}\,|\,\overline{\alpha^{\prime}}\in B^{\prime}_{s\varepsilon}\\}$ and
$A^{\prime}_{s}=\\{\alpha^{\prime}\in
A^{\prime}\,|\,\overline{\alpha^{\prime}}\in B^{\prime}_{s}\\}$. Thus,
$A^{\prime}_{s\varepsilon}$ (resp. $A^{\prime}_{s}$) is the set of positions
(in $P^{\prime}$) of the occurrences of $s$ (resp. inside an occurrence of
$s$) resulting from substitution We set
$A^{\prime}_{s\mathtt{i}}=A^{\prime}_{s}\setminus A_{s\varepsilon}$ for the
set of positions internal to an occurrence of $s$.

Outside the redex and inside $r$. First, we set
$A^{0}_{b}=\\{\alpha^{\prime}\in
A^{\prime}\,|\,\overline{\alpha^{\prime}}\not\geqslant b\\}$,
$A^{\prime}_{r}=\\{al^{\prime}\in
A^{\prime}\,|\,\overline{\alpha^{\prime}}\geqslant
b,\,\overline{\alpha^{\prime}}\notin A^{\prime}_{s\mathtt{i}}\\}$ (note that
we have $\overline{\alpha^{\prime}_{0}}\in\mathtt{supp}(r)$) and
$A_{r}=\\{a\cdot
10\cdot\alpha^{\prime}_{0}\,|\,a\in\mathtt{Rep}_{P^{\prime}}(b),\,\alpha^{\prime}_{0}\in\mathbb{N}^{*},\,a\cdot\alpha^{\prime}_{0}\in
A^{\prime}_{r}\\}$ . Thus, $A^{0}_{b}$ is the set of position outside the
reduct in $t^{\prime}$ and $A_{r}$ corresponds to the set of positions inside
the subterm $r$ in $t$. We define $QR_{b}$ as the identity on $A^{0}_{b}$ and
by $QR_{b}(a\cdot 10\cdot\alpha^{\prime}_{0})=a\cdot\alpha^{\prime}_{0}$ from
$A_{r}$ to $A^{\prime}_{r}$.

We split $A_{r}$ in two: let $A^{x}_{b}=\\{a\cdot
10\cdot\alpha^{\prime}_{0}\,|\,a\in\mathtt{Rep}_{P^{\prime}}(b)\,a\cdot\alpha^{\prime}_{0}\in
A^{\prime}_{s\varepsilon}\\}$ and $A^{1}_{b}=A_{r}\setminus A^{x}_{b}$.
Intuitively, $A^{x}_{b}$ corresponds to the occurrences of $x$ in $t$ (which
are in $r$) whereas $A^{1}_{b}$ corresponds to the other positions inside the
subterm $r$ in $t$.

Inside $s$. We set $A_{s}=\\{a\cdot\lfloor a\cdot
10\cdot\alpha^{\prime}_{0}\rfloor\cdot\alpha_{1}\,|\,a\in\mathtt{Rep}_{P^{\prime}}(b),\,a\cdot\alpha_{0}\in
A^{\prime}_{s\varepsilon},\,a\cdot\alpha^{\prime}_{0}\cdot\alpha_{1}\in
A^{\prime}\\}$. Intuitively, $A_{s}$ will correspond to the position of $s$ in
$P$. Indeed, $a\cdot\alpha^{\prime}_{0}$ (resp. $a\cdot
10\cdot\alpha^{\prime}_{0}$) corresponds to an occurrence of $s$ in
$t^{\prime}$ (resp. of $x$ in $t$) whereas $a$ points to an
$\mathtt{app}$-rule typing the application of the redex $(\lambda x.r)s$
below. As we explained above, the natural number $k:=\lfloor a\cdot
10\cdot\alpha_{0}\rfloor$ gives us the axiom track that the occurrence of $x$
at position $a\cdot 10\cdot\alpha_{0}$ should be assigned while typing $t$.
Then, we should add an argument at $\mathtt{app}$-node $a$ on track $k$.
Hence, $a\cdot\lfloor a\cdot\alpha_{0}\rfloor$. We define $QR_{b}$ from
$A_{s}$ to $A^{\prime}_{s}$ by mapping $a\cdot\lfloor a\cdot
10\cdot\alpha^{\prime}_{0}\rfloor\cdot\alpha_{1}$ on
$a\cdot\alpha^{\prime}_{0}\cdot\alpha_{1}$ (note that
$a\cdot\alpha^{\prime}_{0}\in A^{\prime}_{s}$). Observe that this induces a
bijection from $A_{s}$ to $A^{\prime}_{s}$.

We may now define $A$, which will be the support of $P$, as a disjoint union:

$A:=A^{0}_{b}\cup A^{x}_{b}\cup A^{1}_{b}\cup
A_{s}\cup\mathtt{Rep}_{P^{\prime}}(b)\cup\mathtt{Rep}_{P^{\prime}}(b)\cdot 1$

We define $QR_{b}$ on $\mathtt{Rep}_{P^{\prime}}(b)$ as the identity and we
leave it undefined on $\mathtt{Rep}_{P^{\prime}}(b)\cdot 1$ (which corresponds
to the abstraction $\lambda x.r$). Since $A^{\prime}=A^{0}_{b}\cup
A^{\prime}_{r}\cup A^{\prime}_{s}$, we have that $QR_{b}$ is a function from
$A\setminus\mathtt{Rep}_{P^{\prime}}(b)\cdot 1$ to $A^{\prime}$.

Building types and contexts. We set, for all $\alpha\in
A\setminus\mathtt{Rep}_{P^{\prime}}(b)\cdot 1$,
$\mathtt{T}(\alpha)=\mathtt{T}^{\prime}(\alpha^{\prime})$ with
$\alpha^{\prime}=QR_{b}(\alpha)$. If $a\in\mathtt{Rep}_{P^{\prime}}(b)$, we
set $\mathtt{T}(a\cdot 1)=\mathtt{T}(a\cdot k)_{k\in
K}\rightarrow\mathtt{T}(a)$ where $K=\\{k\geqslant 2\,|\,a\cdot k\in A\\}$.

In order to define the contexts in $P$, we must observe that, in $r$ (inside
$(\lambda x.r)s$), $x$ is a placeholder for occurrence of $s$.

Since $P^{\prime}$ is quantitative, we have, for all $\alpha^{\prime}\in
A^{\prime}$, $y\in\mathscr{V}$,
$\mathtt{C}^{\prime}(\alpha^{\prime})(y)=(\mathtt{tr}^{\prime}(\alpha^{\prime}_{0})\cdot\mathtt{T}^{\prime}(\alpha^{\prime}_{0}))_{\alpha^{\prime}_{0}\in
A^{\prime}(\alpha^{\prime},y)}$ where
$A^{\prime}(\alpha^{\prime},y):=\mathtt{Ax}^{P^{\prime}}_{\alpha^{\prime}}(y)$.

Let $\alpha\in A_{r}$ and $\alpha^{\prime}:=QR_{b}(\alpha)$. For all
$y\in\mathscr{V}$, we set
$A^{\prime}_{0}(\alpha^{\prime},y):=A^{\prime}(\alpha^{\prime},y)\setminus
A^{\prime}_{s}$, the set of positions of axioms typing $y$ (in $P^{\prime}$)
above $\alpha^{\prime}$ which are not in any occurrence of $s$. We set
$A(x,\alpha)=\\{\alpha_{0}\in A^{x}_{b}\,|\,\alpha_{0}\geqslant\alpha\\}$ (the
positions of $x$ in $A$ above $\alpha$). If $\alpha_{0}\in A(x,\alpha)$, then
the axiom rule typing $x$ at position $\alpha_{0}$ is a placeholder for a
typed occurrence of $s$ at position $QR_{b}(\alpha_{0})$ in $P^{\prime}$. We
set $A^{\prime}_{x}(\alpha^{\prime},y):=\\{\alpha^{\prime}_{0}\in
A^{\prime}_{s\varepsilon}\,|\,\alpha^{\prime}_{0}\geqslant\alpha^{\prime}\\}$,
which is the set of positions in $P^{\prime}$ pointing to occurrences of $s$
above $\alpha^{\prime}$. We then define $\mathtt{C}(\alpha)$ case-wise:

  * •

If $\alpha\in A_{r}$, then
$\mathtt{C}(\alpha)=(\mathtt{tr}^{\prime}(\alpha^{\prime}_{0})\cdot\mathtt{T}^{\prime}(\alpha^{\prime}_{0}))_{\alpha^{\prime}_{0}\in
A^{\prime}_{0}(al^{\prime},y)}$. for all $y\neq x$ and
$\mathtt{C}(\alpha)(x)=(\lfloor\alpha_{0}\rfloor\cdot\mathtt{T}^{\prime}(QR_{b}(\alpha_{0})))_{\alpha_{0}\in
A(\alpha,x)}$. This latter definition is correct since $\lfloor\cdot\rfloor$
is injective.

  * •

If $\overline{\alpha}\not\geqslant b$ (i.e., $\alpha\in A^{0}_{b}$) or
$\alpha\in A_{s}$, then
$\mathtt{C}(\alpha)=\mathtt{C}^{\prime}(\alpha^{\prime})$

  * •

If $\alpha=a\cdot 1$ for some $a\in\mathtt{Rep}_{P^{\prime}}(b)$, then we set
$\mathtt{C}(\alpha)=(\mathtt{tr}^{\prime}(\alpha^{\prime}_{0})\cdot\mathtt{T}^{\prime}(\alpha^{\prime}_{0}))_{\alpha^{\prime}_{0}\in
A^{\prime}_{0}(al^{\prime},y)}$. for all $y\neq x$ and
$\mathtt{C}(\alpha)(x)=(\,)$

We define $\mathtt{Exp}_{b}(P^{\prime},\lfloor\cdot\rfloor,t)$ as the tree $P$
labelled with $\mathtt{S}$-judgments such that $\mathtt{supp}(P)=A$ and for
all $\alpha\in A$, $P(\alpha)=\mathtt{C}(\alpha)\vdash
t|_{\alpha}:\mathtt{T}(\alpha)$. For instance, the construction of $A_{r}$
depends on $t$. The construction of $A_{s}$ depends on $\lfloor\cdot\rfloor$.

We have, for all $\alpha\in A\setminus\mathtt{Rep}_{P^{\prime}}(b)$ and
$\alpha^{\prime}=QR_{b}(\alpha)$:

$\mathtt{T}(\alpha)=\mathtt{T}^{\prime}(\alpha^{\prime})\hskip
14.22636pt\hskip 14.22636pt\text{(type preservation)}$

Correction and monotonicity. Let $\alpha\in A$. We set
$\mathtt{Ch}(\alpha):=\\{\alpha\cdot k\in A\,|\,k\in\mathbb{N}\\}$
($\mathtt{Ch}$ stands for “children”). Thus, $\mathtt{Ch}(\alpha)$ corresponds
to the premises of $\alpha$ in $A$. Let $\alpha^{\prime}\in A^{\prime}$. We
set likewise $\mathtt{Ch}^{\prime}(\alpha^{\prime}):=\\{\alpha^{\prime}\cdot
k\in A^{\prime}\,|\,k\in\mathbb{N}\\}$. A case analysis shows that, if
$\alpha\in A^{0}_{b}\cup A^{1}_{b}\cup A_{s}$ and
$\alpha^{\prime}=QR_{b}(\alpha)$, then $QR_{b}$ induces a bijection from
$\mathtt{Ch}(\alpha)$ to $\mathtt{Ch}^{\prime}(\alpha^{\prime})$. By type
preservation, this implies that for all $\alpha\in A^{0}_{b}\cup A^{1}_{b}\cup
A_{s}$, $\alpha$ is given by a correct $\mathtt{S}$-rule.

We must also check that, for $\alpha\in
A^{x}_{b}\cup\mathtt{Rep}_{P^{\prime}}(b)\cup\mathtt{Rep}_{P^{\prime}}(b)\cdot
1$, $\alpha$ is correct: this easily follows from the definition of
$\mathtt{C}$ and $\mathtt{T}$. Thus, $P$ is correct and concludes with
$\mathtt{C}(\varepsilon)\vdash t:\mathtt{T}(\varepsilon)$, i.e., $C\vdash
t:T$, as expected.

To prove monotonicity, i.e., $P^{\prime}_{1}\leqslant_{\infty}P^{\prime}_{2}$
implies
$\mathtt{Exp}_{b}(P^{\prime}_{1},\lfloor\cdot\rfloor,t)\leqslant_{\infty}\mathtt{Exp}_{b}(P^{\prime}_{2},\lfloor\cdot\rfloor,t)$,
one needs to remark the two following crucial points: (1) the construction of
$A_{s}$, which depends on $\lfloor\cdot\rfloor$, is monotonic (2) if
$t(\alpha)=x$, then
$(\lfloor\alpha\rfloor\cdot\mathtt{T}_{1}(\alpha))\leqslant_{\infty}(\lfloor\alpha\rfloor\cdot\mathtt{T}_{2}(\alpha))$
because we assign the same axiom rule in the two singleton sequence types.
This ensures that
$\mathtt{C}_{1}(\alpha)\leqslant_{\infty}\mathtt{C}_{2}(\alpha)$ in all cases.

######  Remark 12.

  * •

The function $\lfloor\cdot\rfloor$ does not need to be total on
$\mathbb{N}\setminus\\{0,1\\}$, nor injective for the above construction to
work. It only needs to be defined for the positions of the axiom rules that
are created (i.e., $\lfloor\cdot\rfloor$ must be defined on $A^{x}_{b}$), so
that an axiom track is assigned for each axiom rule that is created by
expansion. And for all $\mathtt{Rep}_{P^{\prime}}(b)$, $\lfloor\cdot\rfloor$
needs to be injective on $\\{\alpha\in A^{x}_{b}~{}|~{}\alpha\geqslant a\\}$
(not on $\mathbb{N}^{*}$!), which is enough to ensure that no track conflict
occurs.

  * •

Thus, the monotonicity of expansion thus admits a variant, without having to
specify a function $\lfloor\cdot\rfloor$: if
$\,\\!{}^{f}\\!P^{\prime}\leqslant P$ type $t^{\prime}$ and
$t\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\\!\beta}t^{\prime}$, then there
exists $\,\\!{}^{f}\\!P\leqslant P$ typing $t$ such that
$P\stackrel{{\scriptstyle b}}{{\rightarrow}}_{\\!\beta}P^{\prime}$ and
$\,\\!{}^{f}\\!P\stackrel{{\scriptstyle
b}}{{\rightarrow}}_{\\!\beta}\,\\!^{f}\\!P$. For that, consider the function
$\lfloor\cdot\rfloor$ defined by
$\lfloor\alpha\rfloor=\mathtt{tr}^{P}(\alpha)$ for all
$\alpha\in\mathtt{supp}(P)$ such that $t(\alpha)$ is the variable of the
redex.

  * •

One way wonder how the expansion $P$ depends on the choice of
$\lfloor\cdot\rfloor$. It actually does not matter that much, because all the
possible expansions of $P^{\prime}$ are (in some sense) isomorphic, whatever
the values of the new axiom tracks are.

###  C.4. Quantitativity is stable under reducation and expansion.

We can now prove that quantitatitivity is stable under reduction and
expansion, as stated in Remark 6. This means that we did not lose any
generality after Sec. 6 by considering only quantitative derivations.

######  Lemma 54.

If $P\stackrel{{\scriptstyle b}}{{\rightarrow}}_{\\!\beta}P^{\prime}$, then
$P$ is quantitative iff $P^{\prime}$ is quantitative.

###### Proof.

  * •

Assume that $P\rhd C\vdash t:T$ is not quantitative, $t|_{b}=(\lambda x.r)s$
and that $t$ respects Barendregt convention. Thus, there are
$\alpha\in\mathtt{supp}(P)$, $y\in\mathscr{V}$ and $k\geqslant 2$ such that,
for all $d\geqslant 0$, there is $\alpha_{0}\geqslant a$ such that
$|\alpha_{0}|\geqslant d$, $k\in\mathtt{supp}(\mathtt{C}(\alpha_{0})(y))$.
Thus, $B:=\\{\alpha_{0}\geqslant
a~{}|~{}k\in\mathtt{supp}(\mathtt{C}(\alpha_{0})(x))\\}$, the set of
ascendants of $(\alpha_{0},y,k)$, defines (the postfix of) an infinite branch
of $\mathtt{supp}(P)$. There are three cases: (1) $B$ visits an occurrence of
$s$ (i.e., there is $\alpha_{0}\in B$ such that
$\overline{\alpha_{0}}\geqslant b\cdot 1$) (2) $B$ visits $r$ but no
occurrence of $s$ (3) $B$ does not visit the redex $(\lambda x.r)s$. By case
analysis and using the definition of $\mathtt{C}$, we obtain an infinite
branch $B^{\prime}$ in the derivation reduct $P^{\prime}$ which is in an
occurrence of $s$ in case (1), in $r$ but does not visit an occurrence of $s$
in case 2, is outside $r[s/x]$ in case (3). In case (1), we may replace
$(\alpha,y,k)$ by one of its ascendant and assume that $\alpha$ is in an
occurrence of $s$ without losing generality. Likewise, in case (2), we may
assume that $(\alpha,y,k)$ is in $r$.

  * •

The converse implication is proved by following back the steps of the above
proof and considering the definition of $\mathtt{C}$.

∎

###  C.5. Proof of the infinitary subject expansion property

We prove now infinitary subject expansion for system $\mathtt{S}$ Proposition
42.

As mentioned in Sec. 5.3, performing an expansion of a term inside a
derivation requires that we choose new axiom tracks. We will do this
uniformly, i.e., we fix an injection $\lfloor\cdot\rfloor$ from
$\mathbb{N}^{*}$ to $\mathbb{N}-\\{0,\,1\\}$ and any axiom rule created at
position $a$ will use the axiom track value $\lfloor a\rfloor$. As we have
seen (Sec. C.3), this ensures that expansion is monotonic.

Hypotheses. We consider an approximable $\mathtt{S}$-derivation
$P^{\prime}\rhd C^{\prime}\vdash t^{\prime}:T^{\prime}$ and a productive
reduction path $t=t_{0}\stackrel{{\scriptstyle
b_{0}}}{{\rightarrow}}_{\\!\beta}t_{1}\stackrel{{\scriptstyle
b_{1}}}{{\rightarrow}}_{\\!\beta}t_{2}\ldots t_{n}\stackrel{{\scriptstyle
b_{n}}}{{\rightarrow}}_{\\!\beta}t_{n+1}\rightarrow^{\infty}t^{\prime}$. Thus,
$\mathtt{ad}(b_{n})\rightarrow\infty$. We and set
$A^{\prime}=\mathtt{supp}(P^{\prime})$.

Assume $\,\\!{}^{f}\\!P^{\prime}\leqslant P^{\prime}$. Let $N\in\mathbb{N}$
such that, for all $n\geqslant
N,~{}b_{n}\notin\overline{\,\\!{}^{f}\\!A^{\prime}}$ with
$\,\\!{}^{f}\\!A^{\prime}=\mathtt{supp}(\,\\!^{f}\\!P^{\prime})$. For
$n\geqslant N$, we write $\,\\!{}^{f}\\!P^{\prime}(n)$ for the derivation
replacing $t^{\prime}$ by $t_{n}$ in $\,\\!{}^{f}\\!P^{\prime}$. This
derivation is correct according to the subject substitution lemma (Lemma 33),
since $t_{n}(\overline{a})=t^{\prime}(\overline{a})$ for all
$a\in\,\\!^{f}\\!A^{\prime}$.

We then write $\,\\!{}^{f}\\!P^{\prime}(n,~{}k)$ (with $0\leqslant k\leqslant
n$) the derivation obtained by performing $k$ expansions (w.r.t. our reduction
sequence and $\lfloor\cdot\rfloor$). Since $b_{n}$ is not in $A$, we observe
that $\,\\!{}^{f}\\!P^{\prime}(n+1,\,1)=\,\\!^{f}\\!P^{\prime}(t_{n})$.
Therefore, for all $n\geqslant
N,~\,\\!{}^{f}\\!P^{\prime}(n,\,n)=\,\\!^{f}\\!P^{\prime}(N,\,N)$. Since we
could replace $N$ by any $n\geqslant N$, $\,\\!{}^{f}\\!P$ is morally
$\,\\!{}^{f}\\!P^{\prime}(\infty,\,\infty)$. We write
$P=\mathtt{init}(P^{\prime})$ to refer to this deterministic construction
(which implicitly depends on $\lfloor\cdot\rfloor$).

We set
$\mathscr{D}=\\{\mathtt{init}(\,\\!^{f}\\!P^{\prime})~{}|~\,\\!{}^{f}\\!P^{\prime}\leqslant
P^{\prime}\\}$. Let us show that $\mathscr{D}$ is a directed set.

Let $\,\\!{}^{f}\\!P^{\prime}_{1},\,\,\\!^{f}\\!P^{\prime}_{2}\leqslant
P^{\prime}$. We set
$\,\\!{}^{f}\\!P^{\prime}=\mathop{\mathtt{sup}}(\,\\!^{f}\\!P^{\prime}_{1},\,\\!^{f}\\!P^{\prime}_{2})$,
so that $\,\\!{}^{f}\\!P^{\prime}$ is also finite. Let $N$ be great enough so
that $\forall n\geqslant N$, $b_{n}\notin\overline{\,\\!{}^{f}\\!A^{\prime}}$
with $\,\\!{}^{f}\\!A^{\prime}=\mathtt{supp}(\,\\!^{f}\\!P^{\prime})$.

We have $\,\\!{}^{f}\\!P^{\prime}_{i}\leqslant\,\\!^{f}\\!P^{\prime}$, so
$\,\\!{}^{f}\\!P_{i}^{\prime}(N)\leqslant\,\\!^{f}\\!P(N)$. Thus, by
monotonicity of uniform expansion,
$\,\\!{}^{f}\\!P^{\prime}_{i}(N,\,N)\leqslant\,\\!^{f}\\!P^{\prime}(N,\,N)$
i.e., $\mathtt{init}(\,\\!^{f}\\!P_{i})\leqslant\mathtt{init}(\,\\!^{f}\\!P)$.

Since $\mathscr{D}$ is directed, we can set
$P=\mathop{\mathtt{sup}}_{\\{\,\\!^{f}\\!P^{\prime}\,|\,\,\\!^{f}\\!P^{\prime}\leqslant
P^{\prime}\\}}\mathtt{init}(\,\\!^{f}\\!P^{\prime})$. Since for any
$\,\\!{}^{f}\\!P^{\prime}\leqslant P$ and the associated usual notations,
$\,\\!{}^{f}\\!\mathtt{C}(\varepsilon)=\,\\!^{f}\\!\mathtt{C}^{\prime}(\varepsilon)$,
$\,\\!{}^{f}\\!\mathtt{T}(\varepsilon)=\,\\!^{f}\\!\mathtt{T}^{\prime}(\varepsilon)$
and, by Lemma 46,
$\mathtt{C}(\varepsilon),~{}\mathtt{C}^{\prime}(\varepsilon),~{}\mathtt{T}(\varepsilon),~{}\mathtt{T}^{\prime}(\varepsilon)$
are the respective infinite joins of $\,\\!{}^{f}\\!\mathtt{C}(\varepsilon)$,
$\,\\!{}^{f}\\!\mathtt{C}^{\prime}(\varepsilon)$,
$\,\\!{}^{f}\\!\mathtt{T}(\varepsilon)$,
$\,\\!{}^{f}\\!\mathtt{T}^{\prime}(\varepsilon)$ when
$\,\\!{}^{f}\\!P^{\prime}$ ranges over $\mathtt{Approx}(P^{\prime})$, we
conclude that
$\mathtt{C}(\varepsilon)=\mathtt{C}^{\prime}(\varepsilon)=C^{\prime}$ and
$\mathtt{T}(\varepsilon)=\mathtt{T}^{\prime}(\varepsilon)=T^{\prime}$. In
particular, $C^{\prime}\vdash t:T^{\prime}$ is approximably derivable. This
concludes the proof of the infinitary subject expansion property.

###  C.6. Equinecessity and Bipositions of Null Applicative Depth

One may wonder whether every biposition (in a quantitative derivation $P$) is
equinecessary with a root biposition i.e., a biposition that is located in the
judgment concluding $P$. Such a biposition is of the form
$\mathtt{p}=(\varepsilon,c)$ with $c\in\mathtt{supp}(\mathtt{T}^{P}(0))$ or
$\mathtt{p}=(\varepsilon,x,k\cdot c)$ with $k\cdot
c\in\mathtt{supp}(\mathtt{C}^{P}(0)(x))$.

This would imply that, for a derivation $P$ to be approximable, it is enough
to have: “$P$ is quantitative and, for all
$\,\\!{}^{0}\\!B\subseteq{\mathtt{bisupp}(P)}$ finite set of root bipositions,
there exists $\,\\!{}^{f}\\!P\leqslant P$ such that
$\,\\!{}^{0}\\!B\subseteq{\mathtt{bisupp}(\,\\!^{f}\\!P)}$”. We call this
condition root approximability. $\mathtt{p}\in\,\\!^{0}\\!B$,

This is actually true in the finite case and so, for the approximable
derivation. However, this is not true for any derivation. We exhibit a
counter-example of this conjecture in this section i.e., a derivation that
root approximable but not approximable. We present this counter example with a
$\mathscr{R}$-derivation whereas it should be a $\mathtt{S}$-derivation (since
approximability is only an informal notion for System $\mathscr{R}$), but it
is easier to understand that way. Corresponding $\mathtt{S}$-derivations are
not difficult to define from our presentation.

The idea is to use a productive reduction path $t_{0}\rightarrow
t_{1}\rightarrow t_{2}\rightarrow\ldots\rightarrow^{\infty}t^{\prime}$ such
that no reduction step is erasing but there is a variable
$x\in\mathtt{fv}(t_{0})=\mathtt{fv}(t_{1})=\ldots$ such that
$x\notin\mathtt{fv}(t^{\prime})$ (i.e., there is an asymptotic erasure).

Let $\Delta_{*}=\lambda x.(\lambda z.y(x\,x\,z)$ and
$t=\Delta_{*}\,\Delta_{*}$, so that $t\rightarrow\lambda z.y(t\,z)$ (see Fig.
16). We have $t\equiv_{\\!\beta}\mathtt{Y}\,(\lambda tx.(\lambda z.y(tx)))$.

t$\longrightarrow$$y$ $t$$z$ $\char 64\relax$$\char 64\relax$$\lambda z$

Figure 16. Reduction of $t$

Note that $t\,f$ converges to the term $t^{\prime}=y{{}^{\omega}}$, which does
not contain $f$. Indeed, $t\,f\rightarrow(\lambda z.y(t\,z))f\rightarrow
y(t\,f)$ (non-erasing steps).

There are two derivations $\Psi_{1}$ and $\Psi_{2}$ respectively concluding
with $y:[[o]\rightarrow o]_{\omega}\vdash\lambda z.y(t\,z):[o]\rightarrow o$
and $y:[[o]\rightarrow o]_{\omega}\vdash\lambda z.y(t\,z):[\,]\rightarrow o$.
They are obtained from $\Psi^{\prime}_{1}$ and $\Psi^{\prime}_{2}$ from Fig 16
by a one-step expansion:

$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$y$
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$t$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{o}$$z$
$\char 64\relax$$\char 64\relax$$\lambda z$
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$\Psi^{\prime}_{1}\rhd y:[[o]\rightarrow o]_{\omega}\vdash\lambda
z.y(t\,z):[o]\rightarrow
o$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[o]\rightarrow
o}$$y$
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[\,]\rightarrow
o}$$t$$z$ $\char 64\relax$$\char 64\relax$$\lambda z$
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[\,]\rightarrow
o}$$\Psi^{\prime}_{2}\rhd y:[[o]\rightarrow o]_{\omega}\vdash\lambda
z.y(t\,z):[\,]\rightarrow o$

Figure 17. Two Derivations typing $t^{\prime}:=\lambda z.y(t\,z)$

Let $\Pi_{\Omega}$ a derivation concluding with $\vdash\Omega:o$. This
derivation is unsound and is intuitively not approximable: it is impossible to
find a finite derivation (of $\mathscr{R}_{0}$) concluding with
$\vdash\Omega:o$. Then using $\Psi_{1}$ and $\Pi_{\Omega}$ and an
$\mathtt{app}$-rule we can build a derivation $\Pi_{1}$ concluding with
$y:[[o]\rightarrow o]_{\omega}\vdash t\,\Omega:o$, in which the subterm
$\Omega$ is typed. We can also build a derivation $\Pi_{2}$ from $\Psi_{2}$
that also concludes with $y:[[o]\rightarrow o]_{\omega}\vdash t\,\Omega:o$.
This times, the subterm $\Omega$ is not typed.

It is not difficult to see that $\Pi_{2}$ is intuitively approximable, whereas
$\Pi_{1}$ is root approximable but not fully approximable. Roughly speaking,
the subderivation of $\Pi_{1}$ typing $\Omega$ is the only non-approximable
part of $\Pi_{1}$. Indeed:

  * •

$\Pi_{2}$ is not approximable since it contains a subderivation typing the
mute term $\Omega$.

  * •

Every (finite) approximation of $\Pi_{2}$ is an approximation of $\Pi_{1}$.
Thus, the join of the finite approximations of $\Pi_{1}$ is actually
$\Pi_{2}$.

This proves that root approximability is not equivalent to approximability,
and that root approximability actually accepts derivations which are partially
unsound.

##  Appendix D Approximability of normal derivations

In this Appendix, we describe all the quantitative derivations typing normal
forms in system $\mathtt{S}$ and we prove that all of them are approximable.

###  D.1. Called rank of a position inside a type in a derivation

We recall that the rank $\mathtt{rk}(a)$ of $a\in\mathbb{N}^{*}$ is defined by
$\mathtt{rk}(a)=\max(\mathtt{ad}(a),\max(a))$ (Definition 39). We reuse the
notation for constrain levels $\mathtt{clev}$ defined in Sec. 7.1 and the
notation $\mathtt{Call}(a)$ define in Sec. 7.2.

For each $a$ in $A$ and each position $c$ in $\mathtt{Call}(a)$ such that
$\mathtt{Call}(a)(c)\neq X_{a^{\prime}}$ (for all $a^{\prime}$), we define the
numbers $\mathtt{cr}_{\mathtt{out}}(a,c)$ and $\mathtt{cr}_{\mathtt{in}}(a,c)$
by:

  * •

When $a$ is a unconstrained node, $\mathtt{cr}_{\mathtt{out}}(a,c)$ is
$\mathtt{rk}(a)$ and $\mathtt{cr}_{\mathtt{in}}(a,c)=\mathtt{rk}(c)$.

  * •

When $a$ is a non-zero position: the respective values of
$\mathtt{cr}_{\mathtt{out}}(a,c)$ and $\mathtt{cr}_{\mathtt{in}}(a,c)$ for the
positions colored in red are $\mathtt{rk}(a)$ and $\mathtt{rk}(c)$.

$\mathtt{E}(\mathring{a})(x_{1})\mathbin{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow}}\mathtt{E}(\mathring{a})(x_{2})\mathbin{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow}}\ldots\mathbin{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow}}\mathtt{E}(\mathring{a})(x_{n})\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow\mathtt{T}(\mathring{a})}$

where $n=\mathtt{clev}(a)$. In particular,
$\mathtt{cr}_{\mathtt{out}}(a,1^{i})=\mathtt{ad}(a)$ and
$\mathtt{cr}_{\mathtt{in}}(a,1^{i})=0$ for $1\leqslant i\leqslant n$..

  * •

When $a$ is partial: the respective values of
$\mathtt{cr}_{\mathtt{out}}(a,c)$ and $\mathtt{cr}_{\mathtt{in}}(a,c)$ for the
positions colored in red are $\mathtt{rk}(a)$ and $\mathtt{rk}(c)$.

$\mathtt{R}_{1}(a)\mathbin{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow}}\ldots\mathbin{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow}}\mathtt{R}_{n}(a)\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\rightarrow\mathtt{T}(\mathring{a})}$

where $n=\mathtt{clev}(a)$. In particular,
$\mathtt{cr}_{\mathtt{out}}(a,1^{i})=\mathtt{ad}(a)$ for $1\leqslant
i\leqslant n$ and $\mathtt{cr}_{\mathtt{out}}(a,1^{n}\cdot c)=\mathtt{ad}(a)$.

For each $a\in A$ and each position $c$ in $\mathtt{T}(a)$, we define
$\mathtt{cr}_{\mathtt{out}}(a,c)$ and $\mathtt{cr}_{\mathtt{in}}(a,c)$ by
extending $\mathtt{cr}_{\mathtt{out}}$ and $\mathtt{cr}_{\mathtt{in}}$ via
substitution (this is formally done in the next section).

Again, for each $a\in A$, each variable $x$ and each position $c$ in
$\mathtt{C}(a)(x)(c)$, we define $\mathtt{cr}_{\mathtt{out}}(a,x,c)$ and
$\mathtt{cr}_{\mathtt{in}}(a,x,c)$ by extending $\mathtt{cr}_{\mathtt{out}}$
via substitution.

The definition of $\mathtt{cr}_{\mathtt{out}}(a,c)$,
$\mathtt{cr}_{\mathtt{out}}(a,x,c)$, $\mathtt{cr}_{\mathtt{in}}(a,c)$ and
$\mathtt{cr}_{\mathtt{in}}(a,x,c)$) are sound, because in $\mathtt{E}(a)(x)$
and $\mathtt{R}_{i}(x)$, the $X_{a^{\prime}}$ occur at depth $\geqslant 1$ in
$\mathtt{Call}(a^{\prime})$.

######  Definition 55.

If $\mathtt{p}\in{\mathtt{bisupp}(P)}$, we define called rank of $\mathtt{p}$
by

$\mathtt{cr}(\mathtt{p})=\max(\mathtt{cr}_{\mathtt{out}}(\mathtt{p}),\,\mathtt{cr}_{\mathtt{in}}(\mathtt{p}))$

###  D.2. Truncation of rank $n$

We present more formally the definitions of the last section and we recall
that $\mathtt{rk}(a)=\max(\mathtt{ad}(a),\,\max(a))$ for $a\in\mathbb{N}^{*}$.

As we saw above, a quantitative derivation typing a normal form can be
reconstructed from its supports and the types assigned in the unconstrained
positions. Thus, in a quantitative derivation $P$ typing a normal form $t$
such that $\mathtt{supp}(P)=A$, every $\mathtt{p}\in{\mathtt{bisupp}(P)}$
(with $\mathtt{p}=(a,c)$ or $\mathtt{p}=(a,x,c)$) must come from (so to say)
an $(a^{\prime},c^{\prime})$ with $a\geqslant a^{\prime}$. We call
$a^{\prime}$ the calling outer position and $c^{\prime}$ the calling inner
position of $\mathtt{p}$. Let us define them formally now.

For all $a\in A$ and $k\in\mathbb{N}$, we set, by induction on $k$,
$\mathtt{T}^{0}(a)=X_{a}$ and
$\mathtt{T}^{k+1}(a)=\mathtt{T}^{k}(a)[\mathtt{Call}(a^{\prime})/X_{a^{\prime}}]_{a^{\prime}\in\mathbb{N}^{*}}$
and for all $k\in\mathbb{N}$, we set
$\mathtt{supp}_{*}(\mathtt{T}^{k}(a))=\\{c\in\mathtt{supp}(\mathtt{T}^{k}(a))\,|\,\forall
a^{\prime}\in\mathbb{N}^{*},~{}\mathtt{T}^{k}(a)(c)\neq X_{a^{\prime}}\\}$.
Thus,
$\mathtt{supp}(\mathtt{T}(a))=\cup_{k\in\mathbb{N}}\mathtt{supp}_{*}(\mathtt{T}^{*}(a))$
for all $a\in A$.

If $c\in\mathtt{supp}(\mathtt{T}(a))$, there is a minimal $k\in\mathbb{N}$
such that $c\in\mathtt{supp}_{*}(\mathtt{T}^{k}(a))$. We denote it
$\mathtt{cd}(a)(c)$ (call-depth of $c$ at pos. $a$).

When $k=\mathtt{cd}(a)(c)$, there are unique
$c^{\prime}\in\mathtt{supp}(\mathtt{T}(a)),\;c^{\prime\prime}\in\mathbb{N}^{*}$
and $a^{\prime}\in A$ such that $c=c^{\prime}\cdot c^{\prime\prime},\
\mathtt{T}^{k-1}(a)(c^{\prime})=X_{a^{\prime}}$ (we have necessarily
$a\leqslant a^{\prime}$ since $a^{\prime}$ is called by $a$),
$c^{\prime\prime}\in\mathtt{supp}_{*}(\mathtt{Call}(a^{\prime}))$ and
$\mathtt{Call}(a^{\prime})(c^{\prime\prime})=\mathtt{T}(a)(c)$. We write
$a^{\prime}=\mathtt{cop}(a,c)$ (calling outer position of $c$ at position
$a$), $c^{\prime}=\mathtt{cip}(a,c)$ (calling inner position of $c$ at
position $a$) and $c^{\prime\prime}=\mathtt{pf}(a,c)$ (postfix of $c$ at
position $a$). Then, we set
$\mathtt{cr}_{\mathtt{out}}(a,c):=\mathtt{rk}(a^{\prime})$ and
$\mathtt{cr}_{\mathtt{in}}(a,c)=\mathtt{rk}(c^{\prime\prime})$. Finally, we
may define $\mathtt{cr}(a,c)$ by
$\mathtt{cr}(a,c)=\max(\mathtt{cr}_{\mathtt{out}}(a,c),\mathtt{cr}_{\mathtt{in}}(a,c))$.
Implicitly, $\mathtt{cr}(a,c)$ depends on $P$, but $P$ is omitted from the
notation.

  * •

We set $A_{n}=\\{a\in A\,|\,\mathtt{rk}(a)\leqslant n\\}$.

  * •

For all $\mathring{a}\in\mathring{A}_{n}$, we define
$\mathring{\mathtt{T}}_{n}(\mathring{a})$ by removing all the positions $c$
such that $\mathtt{rk}(c)>n$, i.e., $\mathring{\mathtt{T}}_{n}(\mathring{a})$
is the restriction of $\mathring{\mathtt{T}}(\mathring{a})$ on
$\\{c\in\mathtt{supp}(\mathring{\mathtt{T}}(\mathring{a}))\,|\,\mathtt{rk}(c)\leqslant
n\\}$.

Since $t$ is in $\Lambda^{001}$ (and not in
$\Lambda^{111}\setminus\Lambda^{001}$), $A_{n}$ is finite. Since, for all
$a\in A$, $\mathtt{T}(a)$ is in $\mathtt{Typ}$ (and not in
$\mathtt{Typ}^{111}\setminus\mathtt{Typ}$), the type
$\mathring{\mathtt{T}}_{n}(\mathring{a})$ is finite for all
$\mathring{a}\in\mathring{A}_{n}$.

We define $P_{n}$ as the natural extension of
$(A_{n},\mathring{\mathtt{T}}_{n})$. We retrieve contexts $\mathtt{C}_{n}$ and
types $\mathtt{T}_{n}$ such that, for all $a\in A_{n}$,
$P_{n}=\mathtt{C}_{n}(a)\vdash t|_{a}:\mathtt{T}_{n}(a)$.

######  Lemma 56.

For all $k\in\mathbb{N},\;a\in A,\;c\in\mathbb{N}^{*}$, we have
$\mathtt{rk}(a)\leqslant n$ and $c\in\mathtt{supp}(\mathtt{T}_{n}^{k}(a))$ iff
$c\in\mathtt{supp}(\mathtt{T}^{k}(a))$ and $\mathtt{cr}(a,c)\leqslant n$.
In that case, $\mathtt{T}^{k}(a)(c)=\mathtt{T}_{n}^{k}(a)(c)$.

###### Proof.

By a simple but tedious induction on $k$. The notations $\mathtt{cop}_{n}$,
$\mathtt{cip}_{n}$, $\mathtt{pf}_{n}$ and $\mathtt{T}^{k}_{n}$ for the ad hoc
definitions of calling outer positions and so on for $P_{n}$.

  * •

Case $k=0$:
$\Rightarrow$: if $\mathtt{rk}(a)\leqslant n$ and
$c\in\mathtt{supp}(\mathtt{T}_{n}^{0}(a))$, then $\mathtt{rk}(a)\leqslant n$
and $c=\varepsilon$. By definition,
$\mathtt{cr}_{\mathtt{out}}(a,\varepsilon)=\mathtt{rk}(a)\leqslant n$ and
$\mathtt{cr}_{\mathtt{in}}(a)(\varepsilon)=\mathtt{rk}(\varepsilon)=0$. Thus,
$\mathtt{cr}(a,c)\leqslant n$.
$\Leftarrow$: conversely, if $c\in\mathtt{supp}(\mathtt{T}^{0}(a))$ and
$\mathtt{cr}(a,\,c)\leqslant n$, we have likewise $c=\varepsilon$ and
$\mathtt{cop}(a,\varepsilon)=a$, so
$\mathtt{rk}(a)=\mathtt{cr}_{\mathtt{out}}(a,c)\leqslant n$. So
$c=\varepsilon\in\mathtt{T}_{n}^{0}(a)$.

  * •

Case $k+1$: $\Rightarrow$: we assume that $\mathtt{rk}(a)\leqslant n$ and
$c\in\mathtt{supp}(\mathtt{T}^{k}_{n}(a))$. We have two cases, whether
$c\in\mathtt{supp}_{*}(\mathtt{T}^{k}_{n}(a))$ or not. If
$c\in\mathtt{supp}_{*}(\mathtt{T}^{k}_{n}(a))$, then
$\mathtt{T}^{k+1}_{n}(a)(c)=\mathtt{T}^{k}_{n}(a)(c)$. By induction
hypothesis, we have $\mathtt{T}^{k}_{n}(a)(c)=\mathtt{T}^{k}(a)(c)$. This
implies $\mathtt{T}^{k+1}(a)(c)=\mathtt{T}^{k}(a)(c)$ and also,
$\mathtt{T}^{k+1}_{n}(a)(c)=\mathtt{T}^{k+1}(a)(c)$. Thus, let us assume
$c\notin\mathtt{supp}_{*}(\mathtt{T}^{k}_{n}(a))$.

We have once again two cases, whether
$c\in\mathtt{supp}(\mathtt{T}^{k}_{n}(a))$ or not.

Assume first that $c\in\mathtt{supp}(\mathtt{T}^{k}_{n}(a))$. Since
$c\notin\mathtt{supp}_{*}(\mathtt{T}^{k}_{n}(a))$, we have
$\mathtt{T}_{n}^{k}(a)(c)=X_{a^{\prime}}$ where
$a^{\prime}=\mathtt{cop}(a,c)$. Then
$\mathtt{T}^{k+1}_{n}(a)(c)=\mathtt{T}^{=}\mathtt{Call}_{n}(a^{\prime})(\varepsilon)$.
Moreover, the induction hypothesisapplies to $(a,c)$ and gives
$\mathtt{cr}(a,c)\leqslant n$ and
$\mathtt{T}^{k}(a)(c)==\mathtt{T}^{k}_{n}(X_{a^{\prime}})$. Thus,
$\mathtt{T}^{k+1}(a)(c)=\mathtt{Call}(a^{\prime})(\varepsilon)$ and
$\mathtt{rk}(a^{\prime})=\mathtt{cr}_{\mathtt{out}}(a,c)\leqslant n$. Since
$a\leqslant a^{\prime}$, we have $\mathtt{rk}(a)\leqslant n$. Since
$\mathtt{rk}(\varepsilon)=0$, we have
$\mathtt{Call}_{n}(a^{\prime})(\varepsilon)=\mathtt{Call}(a^{\prime})(\varepsilon)$.
So
$\mathtt{T}^{k+1}(a)(c)=\mathtt{T}^{k+1}_{n}(a)(\varepsilon)=\mathtt{Call}_{n}(a^{\prime})(\varepsilon)$.

We assume now that $c\notin\mathtt{supp}(\mathtt{T}^{k}_{n}(a))$. Since
$c\in\mathtt{supp}(T^{k+1}_{n}(a))\setminus\mathtt{supp}(\mathtt{T}^{k}_{n}(a))$,
there are unique $a^{\prime}\in A_{n}$,
$c^{\prime\prime}\in\mathtt{supp}(T^{k}_{n}(a))$ and
$c^{\prime\prime}\in\mathbb{N}^{*}$ such that $c=c^{\prime}\cdot
c^{\prime\prime}$, $\mathtt{T}^{k}_{n}(a)(c)=X_{a^{\prime}}$. In particular,
$\mathtt{T}^{k}_{n}(a)(c)=\mathtt{T}^{k}_{n}(a^{\prime})(c^{\prime\prime})$.
We have two subcases:

    * –

Case $\mathtt{T}^{k+1}_{n}(a)(c)\neq X_{a^{\prime\prime}}$ for all
$a^{\prime\prime}$. In that case, $a^{\prime}=\mathtt{cop}_{n}(a,c)$,
$c^{\prime}=\mathtt{cip}_{n}(a,c)$ and
$c^{\prime\prime}=\mathtt{pf}_{n}(a,c)$. We have
$c^{\prime\prime}\in\mathtt{supp}_{*}(\mathtt{Call}_{n}(a^{\prime}))\leqslant\mathtt{supp}(\mathtt{Call}(a^{\prime}))$.
This entails in particular
$\mathtt{T}^{k+1}(a)(c)=\mathtt{Call}_{n}(a^{\prime})(c)=\mathtt{T}^{k+1}_{n}(a,c)$.
Moreover, we have
$\mathtt{cr}_{\mathtt{out}}(a,c)=\mathtt{rk}(a^{\prime})\leqslant n$ since
$a\in A_{n}$ and
$\mathtt{cr}_{\mathtt{in}}(a,c)=\mathtt{rk}(c^{\prime\prime})\leqslant n$
since $c^{\prime\prime}\in\mathtt{supp}(\mathtt{T}_{n}(a^{\prime}))$. Thus,
$\mathtt{cr}(a,c)\leqslant n$.

    * –

Case $\mathtt{T}^{k+1}_{n}(a)(c)=X_{a^{\prime\prime}}$ for some
$a^{\prime\prime}\geqslant a^{\prime}$. In that case,
$a^{\prime\prime}=\mathtt{cop}_{n}(a,c)$, $c=\mathtt{cip}_{n}(a,c)$ and
$\mathtt{pf}_{n}(a,c)=\varepsilon$. Due to the form of
$\mathtt{Call}_{n}(\\_)$, ${}^{\prime\prime}=1^{i}\cdot\ell$ for some
$j<\mathtt{clev}(a^{\prime})$ and $\ell=\lfloor a^{\prime}\rfloor\geqslant 2$.
By induction hypothesis,
$\mathtt{T}^{k}(a)(c^{\prime})=\mathtt{T}^{k}_{n}(a)(c^{\prime})$, so
$\mathtt{T}^{k}(a)(c^{\prime})=X_{a^{\prime}}$. Since
$c^{\prime\prime}=1^{i}\cdot\ell\in\mathtt{supp}(\mathtt{Call}_{n}(a^{\prime}))$
and $\mathtt{Call}_{n}(a^{\prime})\leqslant\mathtt{Call}(a^{\prime})$, we also
have $\mathtt{Call}(a^{\prime})(c^{\prime\prime})=X_{a^{\prime\prime}}$. Thus,
$\mathtt{T}^{k+1}(a)(c)=X_{a^{\prime\prime}}=\mathtt{T}^{k+1}_{n}(a)(c)$.
Moreover,
$\mathtt{cr}_{\mathtt{out}}(a,c)=\mathtt{rk}(a^{\prime\prime})\leqslant n$
since $a^{\prime\prime}\in A_{n}$, and
$\mathtt{cr}_{\mathtt{in}}(a,c)=\mathtt{rk}(\varepsilon)=0$, so
$\mathtt{cr}(a,c)\leqslant n$.

$\noindent\Leftarrow$: conversely, if $a\in A,\
c\in\mathtt{supp}(\mathtt{T}^{k+1}(a))$ and $\mathtt{cr}(a,c)\leqslant n$, we
assume that $a\notin\mathtt{supp}_{*}(\mathtt{T}^{k}(a))$ (if
$a\in\mathtt{supp}_{*}(\mathtt{T}^{k}(a))$, the case is straightforwardly
handled by induction hypothesis).

Assume first that $c\in\mathtt{supp}(\mathtt{T}^{k}(a))$ and
$\mathtt{T}^{k}(a)=X_{a^{\prime}}$. Then
$\mathtt{rk}(a^{\prime})=\mathtt{cr}_{\mathtt{out}}(a,c)\leqslant n$, so that
$a^{\prime}\in A_{n}$, and
$\mathtt{T}^{k+1}(a)=\mathtt{Call}_{n}(a^{\prime})(\varepsilon)$. By induction
hypothesison $(a,c)$, $a\in A_{n}$, $c\in\mathtt{supp}(\mathtt{T}^{k}_{n}(a))$
and $\mathtt{T}^{k}_{n}(a)(c)=X_{a^{\prime}}$, so
$\mathtt{T}^{k+1}_{n}(\varepsilon)=\mathtt{Call}_{n}(a^{\prime})(\varepsilon)$.
Since $\mathtt{Call}_{n}(a^{\prime})\leqslant\mathtt{Call}(a)$, we have
$\mathtt{Call}_{n}(a^{\prime})=\mathtt{Call}(a^{\prime})(\varepsilon)$, which
is equal to $\mathtt{T}^{k+1}(a)(c)$ since
$\mathtt{T}^{k}(a)(c)=X_{a^{\prime}}$. Thus,
$\mathtt{T}^{k+1}_{n}(a)(cc)=\mathtt{T}^{k+1}(a)(c)$.

We assume now that $c\notin\mathtt{supp}(\mathtt{T}^{k}(a))$. Since
$c\in\mathtt{supp}(T^{k+1}(a))\setminus\mathtt{supp}(\mathtt{T}^{k}(a))$,
there are unique $a^{\prime}\in A$, $c^{\prime}\in\mathtt{supp}(T^{k}(a))$ and
$c^{\prime\prime}\in\mathbb{N}^{*}$ such that $c=c^{\prime}\cdot
c^{\prime\prime}$, $\mathtt{T}^{k}(a)(c)=X_{a^{\prime}}$. By induction
hypothesison $c^{\prime}$, $\mathtt{rk}(a)\leqslant n$,
$c^{\prime}\in\mathtt{supp}(T^{k}_{n}(a))$ and
$\mathtt{T}^{k}_{n}(a)(c^{\prime})=\mathtt{T}^{k}(a)(c)=X_{a^{\prime}}$. In
particular,
$\mathtt{T}^{k}(a)(c)=\mathtt{T}^{k}(a^{\prime})(c^{\prime\prime})$. We have
two subcases:

    * –

If $\mathtt{T}^{k+1}(a)(c)\neq X_{a^{\prime\prime}}$ for all
$a^{\prime\prime}$, then $a^{\prime}=\mathtt{cop}(a,c)$,
$c^{\prime}=\mathtt{cip}(a,c)$ and $c^{\prime\prime}=\mathtt{pf}(a,c)$.
Moreover,
$\mathtt{rk}(c^{\prime\prime})=\mathtt{cr}_{\mathtt{in}}(a,c)\leqslant\mathtt{cr}(a,c)\leqslant
n$, so ${}^{\prime\prime}\in\mathtt{supp}(\mathtt{Call}_{n}(a^{\prime}))$. By
definition of $\mathtt{T}^{k+1}_{n}(a)$,
$\mathtt{T}^{k+1}=\mathtt{Call}_{n}(a^{\prime})(c^{\prime})$. Since
$\mathtt{Call}_{n}(a^{\prime})\leqslant\mathtt{Call}(a^{\prime})$, we have
$\mathtt{Call}_{n}(a^{\prime})(c^{\prime})=\mathtt{Call}(a)(c^{\prime})$,
which is equal to $\mathtt{T}^{k+1}(a)(c)$. Thus,
$\mathtt{T}^{k+1}_{n}(a)(c)=\mathtt{T}^{k+1}(a)(c)$.

    * –

If $\mathtt{T}^{k+1}(a)(c)=X_{a^{\prime\prime}}$ for some
$a^{\prime\prime}\geqslant a^{\prime}$. In that case,
$a^{\prime\prime}=\mathtt{cop}(a,c)$, $c=\mathtt{cip}(a,c)$ and
$\mathtt{pf}(a,c)=\varepsilon$. Due to the form of $\mathtt{Call}(\\_)$,
${}^{\prime\prime}=1^{j}\cdot\ell$ for some $j<\mathtt{clev}(a^{\prime})$ and
$\ell=\lfloor a^{\prime}\rfloor\geqslant 2$. By definition of
$\mathtt{Call}_{n}(\\_)$, we also have $1^{j}\in\mathtt{Call}_{n}(a^{\prime})$
and $\mathtt{Call}_{n}(a^{\prime})(c^{\prime\prime})=X_{a^{\prime\prime}}$
($\mathtt{Call}_{n}(a^{\prime})$ and $\mathtt{Call}(a^{\prime})$ may only
differ on positions $\geqslant 1^{\mathtt{clev}(a^{\prime})}$ by
construction). By definition of $T^{k+1}_{n}$, we have
$T^{k+1}_{n}(a)(c)=\mathtt{Call}_{n}(a^{\prime})(X_{a^{\prime\prime}})$. In
particular, $T^{k+1}_{n}(a)(c)=\mathtt{T}^{k+1}(a)(c)$.

∎

###  D.3. A Complete Sequence of Derivation Approximations

We now prove Lemma 40:

######  Lemma.

If $P$ is a quantitative derivation typing a normal form $t$, then $P$ is
approximable.

###### Proof.

Let $\,\\!{}^{0}\\!B\subset{\mathtt{bisupp}(P)}$ a finite subset. We set
$n=\max\\{\mathtt{cr}(\mathtt{p})\,|\,\mathtt{p}\in B\\}$. Then
$\,\\!{}^{0}\\!B\subseteq{\mathtt{bisupp}(P_{n})}$.

In order to conclude, it is enough to prove that $P_{n}$ is a finite
derivation. For that, we notice that $A_{n}$ is finite and, for all $a\in
A_{n}$, $\mathtt{Call}_{n}(a)$ is finite and
$\mathtt{T}_{n}^{k+1}(a)=T_{n}^{n+1}(a)$ for all $k\geqslant n+1$, since
$\mathtt{T}^{n+1}_{n}(a)$ does not contain any $X_{a^{\prime}}$. In
particular, $\mathtt{T}_{n}(a)$ is finite. Since $A_{n}$ and all the
$\mathtt{T}_{n}(a)$ ($a$ ranging over $A$) are finite, $P_{n}$ is finite. ∎

##  Appendix E Infinitary Multiset Types

We present here a definition of type assignment system $\mathscr{R}$, which is
an infinitary version of Gardner-de Carvalho’s system $\mathscr{R}_{0}$.

Intuitively, a multiset is a sequence in which we have the positions (the
tracks) of the elements has been collapsed, e.g., the multiset
$[o_{1},o_{2},o_{1}]$ may be seen indifferently as the collapse of the
sequences $(3\cdot o_{1},5\cdot o_{2},7\cdot o_{2})$, $(2\cdot o_{1},8\cdot
o_{2},10\cdot o_{2})$ or $(3\cdot o_{2},5\cdot o_{1},7\cdot o_{2})$. Since
there are nesting of multisets in the finite types from System
$\mathscr{R}_{0}$, the types of $\mathscr{R}_{0}$ may be seen as an
inductive/nested collapse of finite types of System $\mathtt{S}$.

In order to build an infinitary version of $\mathscr{R}_{0}$ whose types will
feature infinitary nestings of multisets, it is natural to define those types
as coinductive collapse of sequences.

###  E.1. Types

Let $U_{1}$ and $U_{2}$ be two labelled trees or two sequences of labelled
trees (in the sense of Sec. 4 ). A 01-stable isomorphism from $U_{1}$ to
$U_{2}$ is a bijection $\phi$ from $\mathtt{supp}(U_{1})$ to
$\mathtt{supp}(U_{2})$ such that:

  * •

$\phi$ is monotonic for the prefix order.

  * •

If $a\cdot k\in\mathtt{supp}(U_{1})$ with $k=0$ or $k=1$, then $\phi(a\cdot
k)=\phi(a)=k$

  * •

For all $a\in\mathtt{supp}(U_{1})$, $U_{2}(\phi(a))=U_{1}(a)$.

Thus, a 01-stable isomorphism is either an isomorphism of labelled trees or an
isomorphism of sequences, which preserves tracks 0 and 1. We write
$U_{1}\equiv U_{2}$ when there is a 01-stable isomorphism from $U_{1}$ to
$U_{2}$. When $U$ is a tree, the definition implies that
$\phi(\varepsilon)=\varepsilon$. If $U_{1}$ and $U_{2}$ are types (resp.
sequence types), $\phi$ is called a type isomorphism (resp. sequence type
isomorphism).

Alternatively, we can define $U_{1}\equiv U_{2}$ for types and sequence types
by coinduction, without reference to 01-stable isomorphism:

  * •

$o\equiv o$

  * •

$(S_{k})_{{k\in K}}\equiv(S^{\prime}_{k})_{{k\in K}^{\prime}}$ if there is a
bijection $\rho:K\rightarrow K^{\prime}$ such that, for all ${k\in K}$,
$S_{k}\equiv S^{\prime}_{\rho(k)}$.

  * •

$(S_{k})_{{k\in K}}\rightarrow T\equiv(S^{\prime}_{k})_{{k\in
K}^{\prime}}\rightarrow T^{\prime}$ if $(S_{k})_{{k\in
K}}\equiv(S^{\prime}_{k})_{{k\in K}^{\prime}}$ and $T\equiv T^{\prime}$.

The set $\mathtt{Typ}_{\mathscr{R}}$ of types of System $\mathscr{R}$ is
defined as the quotient set $\mathtt{Typ}/\equiv$.

If $U$ is a $\mathtt{S}$-type or a sequence type, its equivalence class is
written $\overline{U}$. We may now define coinductively the notation of the
collapses of $\mathtt{S}$-types:

  * •

The equivalent class of a sequence type $F=(S_{k})_{{k\in K}}$ is the multiset
type written $[\overline{S_{k}}]_{k\in\mathtt{Rt}(F)}$

  * •

We write $\overline{F}\rightarrow\overline{T}$ for $\overline{F\rightarrow
T}$.

  * •

If $o$ is a type variable, $\overline{o}$ is the singleton $\\{o\\}$. In that
case, we just write (abusively) $o$ instead of $\overline{o}$ or $\\{o\\}$.

Countable sum $+_{i\in I}\overline{F^{i}}$ is defined on the set of multisets
types by using an arbitrary bijection $j$ from the pairwise disjoint countable
sum $\mathbb{N}\times(\mathbb{N}\setminus\\{0,1\\})$ to
$\mathbb{N}\setminus\\{0,1\\}$.

Let $(F^{i})_{{i\in I}}=((S^{i}_{k})_{{k\in K}(i)})_{{i\in I}}$ a countable
family of sequence type such that $I\subseteq\mathbb{N}$. We define
$\stackrel{{\scriptstyle j}}{{+}}_{{i\in I}}F^{i}$ as the sequence type
$F=(S_{k})_{{k\in K}}$ such that $K=\\{j(i,k)\,|\,i\in I,\,{k\in K}(i)\\}$
and, for all ${k\in K}$, $S_{k}$ is $S^{i}_{k_{0}}$ where $(i,k_{0})$ is the
unique pair such that $i\in I,\;k_{0}\in K(i)$ and $k=j(i,k_{0})$. We may then
prove that (1) if for all ${i\in I}$, $F^{i}\equiv G^{i}$, then
$\stackrel{{\scriptstyle j}}{{+}}_{{i\in I}}F^{i}\equiv\stackrel{{\scriptstyle
j}}{{+}}_{{i\in I}}G^{i}$ (2) the class of $\stackrel{{\scriptstyle
j}}{{+}}_{{i\in I}}F^{i}$ does not depend on $j$. Thus, we may define
countable sum operator + on multiset types. It is routine work to prove that
$+$ infinitarily associative and commutative on multiset types, as expected.

###  E.2. Typing rules

An $\mathscr{R}$-context is a total function from the set of term variables
$\mathscr{V}$ to the set of infinitary multiset types. An
$\mathscr{R}$-judgment is a triple of the form $\Gamma\vdash t:\tau$ where $G$
is a $\mathscr{R}$-context, $t$ a 001-term and $\tau$ a $\mathscr{R}$-types.
The set of semi-rigid derivations is the set of trees (labelled with
$\mathscr{R}$-judgments) defined coinductively by the following rules:

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 25.64218pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=54.06215pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:[\tau]\vdash x:\tau$}}}}\hskip 14.22636pt\hskip 14.22636pt{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
4.8611pt\hbox{$\displaystyle\penalty 1\Gamma;x:[\sigma_{i}]_{{i\in I}}\vdash
t:\tau$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=81.43246pt\hbox{\kern
3.00003pt$\mathtt{abs}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\Gamma\vdash\lambda x.t:\,[\sigma_{i}]_{{i\in
I}}\rightarrow\tau$}}}}$ ${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash
t:[\sigma_{i}]_{{i\in I}}\rightarrow\tau\hskip 14.22636pt(\Delta_{k}\vdash
u:\sigma_{k})_{{k\in K}}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=140.93605pt\hbox{\kern
3.00003pt$\mathtt{app}$}}}\hbox{\kern 0.0pt\kern
33.50844pt\hbox{$\displaystyle\Gamma+_{{k\in K}}\Delta_{k}\vdash
t\,u:\,\tau$}}}}$

Why do we say that these derivations are semi-rigid? Because the argument of
derivations are still placed on argument tracks ${k\in K}$, while obviously,
they should not matter when we work with multisets. Let $P_{1}$ and $P_{2}$ be
two semi-rigid derivations. We define the set of $\mathscr{R}$-derivation as
the quotient set of that of semi-derivation by the relation $\equiv$.

An element of $\mathtt{Deriv}_{\mathscr{R}}$ is usually written $\Pi$, whereas
an element of $\mathtt{Deriv}_{*}$ is written $P$ (as for system
$\mathtt{S}$). Notice the derivation $\Pi$ and $\Pi^{\prime}$ of Sec. 3.6 and
Fig. 7 are objects of $\mathtt{Deriv}$.

###  E.3. Quantitativity and Coinduction in System $\mathscr{R}$

Let $\Gamma$ be any context. Exactly as in Sec. 5.2, we can use the infinite
branch of $f^{\infty}$ to give the following variant of derivation
$\Pi^{\prime}$ from Sec. 3.6, which respects the rules of system
$\mathscr{R}$:

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 48.72198pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=97.44397pt\hbox{\kern
3.00003pt$\mathtt{ax}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
f:[[o]\rightarrow o]\vdash f:[o]\rightarrow o$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\hskip 14.22636pt\Pi^{\prime}_{\Gamma}\rhd f:[[o]\rightarrow
o]_{\omega}+\Gamma\vdash f^{\infty}:o$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=272.02855pt\hbox{\kern
3.00003pt$\mathtt{app}$}}}\hbox{\kern 0.0pt\kern
86.49239pt\hbox{$\displaystyle f:[[o]\rightarrow o]_{\omega}+\Gamma\vdash
f^{\infty}:o$}}}}$

The notion of quantitativity (Definition 16) can be adapted while considering
multisets:

######  Definition 57.

  * •

A semi-rigid derivation $P$ is quantitative if, for all
$a\in\mathtt{supp}(P),~{}\Gamma(a)(x)=[\tau(a^{\prime})]_{a^{\prime}\in\mathtt{Ax}^{P}_{a}{x}}$.

  * •

A $\mathscr{R}$-derivation $\Pi$ is quantitative if any of its semi-rigid
representatives is (in that case, all of them are quantitative).

In the next subsection, we show that a derivation $\Pi$ from system
$\mathscr{R}$ can have both quantitative and not quantitative, approximable
and not approximable representatives in System $\mathtt{S}$. It once again
shows that rigid constructions allow a more fine-grained control than system
$\mathscr{R}$ does on derivations.

###  E.4. Representatives and Dynamics

A $\mathtt{S}$-derivation $P$ represents a derivation $\Pi$ if the semi-rigid
derivation $P_{*}$ defined by $\mathtt{supp}(P_{*})=\mathtt{supp}(P)$ and
$P_{*}(a)=\overline{C(a)}\vdash t|_{a}:\,\overline{T(a)}$, is a semi-rigid
representative of $\Pi$. We write $P_{1}\equiv_{\mathscr{R}}P_{2}$ when two
$\mathtt{S}$-derivations $P_{1}$ and $P_{2}$ both represent the same
$\mathscr{R}$-derivation $\Pi$.

######  Proposition 58.

If a $\mathtt{S}$-derivation $P$ is quantitative, then the
$\mathscr{R}$-derivation $\overline{P}$ is quantitative in system
$\mathscr{R}$.

Using natural extensions (Sec. 7.2), it easy to prove:

######  Proposition 59.

If $\Pi$ is a quantitative derivation typing a 001-normal form, then, there is
a quantitative rigid derivation $P$ such that $\overline{P}=\Pi$.

###### Proof.

Let $P(\ast)$ be a semi-rigid derivation representing $\Pi$. We set
$A=\mathtt{supp}(P(\ast))$ and for all full position $a\in A$, we choose a
representative $T(\mathring{a})$ of $\tau(a)$. We apply then the canonical
construction of Sec. 7.2, which yields a rigid derivation $P$ such that
$P_{*}=P(\ast)$ (we show that, for all $a\in A$, $T(a)$ represents $\tau(a)$).
∎

We can actually prove that every quantitative $\mathscr{R}$-derivation can be
represented with a $\mathtt{S}$-quantitative rigid derivation and that we can
endow it with every possible infinitary reduction choice [Via18]. However, a
quantitative derivation can also have a not quantitative rigid representative,
as we see below with $\Pi^{\prime}$ and $\tilde{P}^{\prime}$.

We omit again the right side of axiom rules, e.g., $f:((2\cdot o)\rightarrow
o)_{2}$ stands for $f:((2\cdot o)\rightarrow o)_{2}\vdash f:(2\cdot
o)\rightarrow o$. Moreover, outer tracks are indicated between red square
brackets.

$P^{\prime}_{2}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 38.11104pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=78.99986pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
f\\!:\\!(2\mathord{\cdot}(2\cdot o)\rightarrow
o)\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[1]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\ \hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt
plus 0.0001fil\hbox{\kern 38.11104pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=78.99986pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
f\\!:\\!(3\mathord{\cdot}(2\cdot o)\rightarrow
o)\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[1]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\ P^{\prime}_{4}\rhd
f\\!:\\!(k\mathord{\cdot}(2\cdot o)\rightarrow o)_{k\geqslant 4}\vdash
f^{\infty}:o\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[2]}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=255.97725pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 66.00613pt\hbox{$\displaystyle
f:(k\mathord{\cdot}(2\cdot o)\rightarrow o)_{k\geqslant 3}\vdash
f^{\infty}:o\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[2]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=408.41476pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 148.336pt\hbox{$\displaystyle
f:(k\mathord{\cdot}(2\cdot o)\rightarrow o)_{k\geqslant 2}\vdash
f^{\infty}:o$}}}}$

$\tilde{P}^{\prime}_{2}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 38.11104pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=78.99986pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
f\\!:\\!(2\mathord{\cdot}(2\cdot o)\rightarrow
o)\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[1]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\hskip 5.69046pt\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 38.11104pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=78.99986pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
f\\!:\\!(4\mathord{\cdot}(2\cdot o)\rightarrow
o)\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[1]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\hskip 5.69046pt\tilde{P}^{\prime}_{5}\rhd
f\\!:\\!(k\mathord{\cdot}(2\cdot o)\rightarrow o)_{k=3\vee k\geqslant 5}\vdash
f^{\infty}:o\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[2]}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=268.39482pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 72.21492pt\hbox{$\displaystyle
f:(k\mathord{\cdot}(2\cdot o)\rightarrow o)_{k\geqslant 3}\vdash
f^{\infty}:o\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[2]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=421.5228pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 154.89001pt\hbox{$\displaystyle
f:(k\mathord{\cdot}(2\cdot o)\rightarrow o)_{k\geqslant 2}\vdash
f^{\infty}:o$}}}}$

$\tilde{P}^{\prime}_{k}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 38.37146pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=79.5207pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
f\\!:\\!(k\mathord{\cdot}(2\cdot o)\rightarrow
o)\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[1]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\hskip 14.22636pt\tilde{P}^{\prime}_{k+1}\rhd
f\\!:\\!(i\mathord{\cdot}(2\cdot o)\rightarrow o)_{i=3\vee i\geqslant
k+1}\vdash
f^{\infty}:o\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[2]}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=280.4983pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 85.85098pt\hbox{$\displaystyle
f:(i\mathord{\cdot}(2\cdot o)\rightarrow o)_{i\geqslant k}\vdash
f^{\infty}:o$}}}}\hskip 14.22636pt\hskip 14.22636pt\text{(for $k\geqslant
5$)}$

Figure 18. Representing $\Pi^{\prime}$

• We define ${R_{o}}$ by ${R_{o}}:=(k\cdot{R_{o}})_{k\geqslant 2}\rightarrow
o$ and Let $P_{k}$ ($k\geqslant 2$) and $P$ be the following
$\mathtt{S}$-derivations:

$P_{k}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 38.37146pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=79.5207pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
f\\!:\\!(k\mathord{\cdot}(2\cdot o)\rightarrow
o)\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[1]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\ \hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt
plus 0.0001fil\hbox{\kern 25.54987pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=53.87752pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:\,(2\mathord{\cdot}{R_{o}})\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[1]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2(\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
29.5505pt\hbox{$\displaystyle\penalty 1\phantom{.}$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=61.8788pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:(i\mathord{\cdot}{R_{o}})\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[i-1]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2)_{i\geqslant 3}$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=201.05661pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 53.07468pt\hbox{$\displaystyle
x:(i\mathord{\cdot}{R_{o}})_{i\geqslant 2}\vdash
x\,x:o\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[2]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=354.01497pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 109.73341pt\hbox{$\displaystyle
f:(k\mathord{\cdot}(2\cdot o)\rightarrow o)\vdash
f(x\,x):o\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[0]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=388.2338pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 140.54767pt\hbox{$\displaystyle
f:(k\mathord{\cdot}(2\cdot o)\rightarrow o)\vdash\Delta_{f}:{R_{o}}$}}}}$

$P={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 10.80966pt\hbox{$\displaystyle\penalty
1P_{2}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[1]}\hskip
14.22636pt(P_{k}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[k-1]})_{k\geqslant
3}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=113.12338pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
f:(k\mathord{\cdot}(2\cdot o)\rightarrow o)_{k\geqslant
2}\vdash\Delta_{f}\Delta_{f}$}}}}$

• Let $\tilde{P}_{k}$ ($k\geqslant 2$) and $\tilde{P}$ be the following
$\mathtt{S}$-derivations:

$\tilde{P}_{k}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 41.70305pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=86.18388pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
f:(k\mathord{\cdot}(2\cdot o)\rightarrow
o)~{}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[1]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\ \hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt
plus 0.0001fil\hbox{\kern 26.38152pt\hbox{$\displaystyle\penalty
1\phantom{.}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=55.54082pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:(3\mathord{\cdot}{R_{o}})~{}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[1]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
26.38152pt\hbox{$\displaystyle\penalty 1\phantom{.}$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=55.54082pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:(2\mathord{\cdot}{R_{o}})~{}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[2]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2(\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
31.21547pt\hbox{$\displaystyle\penalty 1\phantom{.}$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=65.20872pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle
x:(i\mathord{\cdot}{R_{o}})~{}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[i-1]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2)_{i\geqslant 4}$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=295.80948pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 100.45111pt\hbox{$\displaystyle
x:(i\mathord{\cdot}{R_{o}})_{i\geqslant 2}\vdash
x\,x:o\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[2]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=450.43102pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 157.94144pt\hbox{$\displaystyle
f:(k\mathord{\cdot}(2\cdot o)\rightarrow o)\vdash
f(x\,x):o\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[0]}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=479.64984pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 186.25569pt\hbox{$\displaystyle
f:(k\mathord{\cdot}(2\cdot o)\rightarrow o)\vdash\Delta_{f}:{R_{o}}$}}}}$

$\tilde{P}={tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 8.91382pt\hbox{$\displaystyle\penalty
1\tilde{P}_{2}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[1]}\hskip
14.22636pt(\tilde{P}_{k}\,\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{[k-1]})_{k\geqslant
3}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern
0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=104.82477pt\hbox{\kern
3.00003pt${}$}}}\hbox{\kern 0.0pt\kern 0.0pt\hbox{$\displaystyle f:((2\cdot
o)\rightarrow o)_{k\geqslant 2}\vdash\Delta_{f}\Delta_{f}$}}}}$

• The rigid derivations $P$ and $\tilde{P}$ both represent $\Pi$. Intuitively,
subject reduction in $P$ will consist in taking the first argument $P_{3}$,
placing it on the first occurrence of $x$ in $f(x\,x)$ (in $P_{2}$) and
putting the other $P_{k}$ ($k\geqslant 4$) in the different axiom rules typing
the second occurrence of $x$ in the same order, i.e., , for $k\geqslant 3$,
$P_{k}$ is moved from track $k-1$ to track $k-2$. There is a simple decrease
on the track number and we can go this way towards $P^{\prime}_{2}$ typing
$f^{\infty}$.

The rigid derivation $\tilde{P}$ process the same way, except it will always
skip $\tilde{P}_{3}$ ($\tilde{P}_{3}$ will remain on track 2). Morally, we
perform subject reduction “by-hand” while avoiding to ever place
$\tilde{P}_{3}$ in head position, i.e., $\tilde{P}_{3}$ is never “consumed” by
reduction.

A computation shows that infinitary reductions performed in $P$ and
$\tilde{P}_{2}$ yield respectively to $P^{\prime}_{2}$ and
$\tilde{P}^{\prime}_{2}$ of Fig. 18.

Thus, $P^{\prime}$ and $\tilde{P}^{\prime}$ both represent $\Pi^{\prime}$
(from Sec. 3.6), but $P^{\prime}$ is quantitative whereas $\tilde{P}^{\prime}$
is not (the track $3$ type assigned to $f$ does not end in an axiom leaf).
This proves that quantitativity is not stable up to the limit of a productive
reduction path and that $\tilde{P}$ is not approximable by Proposition 36.

Moreover, by Proposition 41, $P^{\prime}_{2}$ is approximable. By infinitary
subject expansion, $P_{2}$ also is (actually, one may also use the
$\mathtt{S}$-representatives of $\Pi_{n}$ and $\Pi^{\prime}_{n}$ in Fig. 7 to
approximate $P$ and $P^{\prime}$ arbitrarily).

Conclusion. Thus, $\Pi$ and $\Pi^{\prime}$ have both approximable and not
approximable representatives. Actually, $\Pi$ has a representative which is
quantitative but not approximable. This proves that approximability cannot be
defined in system $\mathscr{R}$.