# Analytical model for laser-assisted recombination of hydrogenic atoms

Gavriil Shchedrin1 and Alexander Volberg2 1Department of Physics and Astronomy
and National Superconducting Cyclotron Laboratory, Michigan State University,
East Lansing, Michigan 48824, USA  2Department of Mathematics, Michigan State
University, East Lansing, Michigan 48824, USA<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

We introduce a new method that allows one to obtain an analytical cross
section for the laser-assisted electron-ion collision in a closed form. As an
example we perform a calculation for the hydrogen laser-assisted
recombination. The $S$-matrix element for the process is constructed from an
exact electron Coulomb-Volkov wave function and an approximate laser modified
hydrogen state. An explicit expression for the field-enhancement coefficient
of the process is expressed in terms of the dimensionless parameter
$\kappa=\left|{e\varepsilon_{0}}/{q\omega_{0}}\right|^{2}$, where $e$ and $q$
are the electron charge and momentum respectively, and $\varepsilon_{0}$ and
$\omega_{0}$ are the amplitude and frequency of the laser field respectively.
The simplified version of the cross section of the process is derived and
analyzed within a soft photon approximation.

###### pacs:

32.80.Rm, 34.50.Rk

##  1 Introduction

Atomic scattering processes in the presence of a harmonic laser field is a
significant part of contemporary atomic physics [1]. A simple and accurate
theoretical model for laser-assisted atomic scattering processes would allow
one to explain their distinctive properties. The standard theoretical approach
for laser-assisted electron-ion collisions consists of the construction of the
$S$-matrix element for the corresponding process. The electron wave function
in a combined Coulomb-laser field is given by the well-known Coulomb-Volkov
state. The dressed state of the atom is described by the classical time-
dependent perturbation series. Within these approximations the $S$-matrix
element was derived and numerically analyzed.

The goal of this paper is the construction of a simple analytical model for an
electron-ion collision in a harmonic laser field. Namely, we have developed a
new method that allows to derive an analytical expression for the cross
section of a laser-assisted atomic scattering process in closed form. The new
step consists in the using of the Bessel generating function as an argument
for the Plancherel theorem. This allows one to perform the summation over the
number of field harmonics so that the analytical expression for the cross
section of the process can be explicitly written. As an example, we perform a
calculation for a laser assisted hydrogen recombination process. An exact
expression for the field-enhancement coefficient is given in terms of the
dimensionless parameter
$\kappa=\left|{e\varepsilon_{0}}/{q\omega_{0}}\right|^{2}$.

The article is organized as follows. In Section II, the problem is formulated
with the necessary knowledge concerning the standard field-free hydrogen
recombination process. In Section III we give the $S$-matrix element for the
hydrogen laser-assisted recombination process based on the electron Coulomb-
Volkov wave function and the laser modified hydrogen state. In Section IV we
perform a detailed analysis of the Coulomb-Volkov wave function. In Sections V
and VI we obtain partial and general differential cross sections of the laser-
assisted hydrogen recombination. Section VII is devoted to the analysis of the
soft photon approximation, in which a simplified differential cross section of
the process is derived and analyzed. Section VIII summarizes the results and
advantages of the developed method.

##  2 Laser-assisted hydrogen recombination

The goal of this paper is to provide an analytical expression for a laser
assisted hydrogen recombination process,

$p+e+L\hbar{\omega_{0}}\longrightarrow{H+\hbar{\omega}}.$ (1)

The additional term $L\hbar{\omega_{0}}$ ($L$ is the number of harmonics)
indicates the presence of a laser field,

$\vec{\varepsilon}=\vec{\varepsilon}_{0}\sin{\omega_{0}t},$ (2)

and points out the conservation of quasienergy. Here $\vec{\varepsilon}_{0}$
is the amplitude of the field and $\omega_{0}$ is the field frequency.

The final result for the analytical cross section of the process (1) can be
directly applied to the following laser-assisted recombination processes of
i. hydrogenic atom (for instance, $He^{+}$)

$^{Z}_{A}X^{+}+e+L\hbar{\omega_{0}}\longrightarrow{{}_{A}^{Z}X+\hbar{\omega}},$
(3)

ii. antihydrogen atom

$\bar{p}+{e}^{+}+L\hbar{\omega_{0}}\longrightarrow{\bar{H}+\hbar{\omega}},$
(4)

iii. positronium atom formation

$e+{e}^{+}+L\hbar{\omega_{0}}\longrightarrow{Ps+\hbar{\omega}}.$ (5)

Creation of an antihydrogen atom [2] has become a driving force in
contemporary atomic physics. Of particular interest in this area is the
accuracy the value of the fine structure constant $\alpha=e^{2}/\hbar{c}$
which can be improved by comparing atomic spectra of hydrogen and antihydrogen
atoms. Exploration of these spectra provides a unique opportunity for studying
basic symmetries in physics, including the CPT invariance [3].

The main reaction leading to the formation of the antihydrogen atom in modern
experiments [2, 4] is the three-body process which was a subject of recent
theoretical calculations [5, 6]. The laser assisted antihydrogen recombination
process (4), being dominated by the three-body process, was studied
experimentally [7] and theoretically [8, 9], but the analytical expression for
this process has not been found prior to this work.

The differential cross section of the reaction for the standard field-free
hydrogen recombination process is well known due to the principle of detailed
balance between the differential cross section of photo-recombination,
$d\sigma_{fi}/d\Omega_{f}$, and that of photo-ionization,
$d\sigma_{if}/d\Omega_{i}$, [10]:

$\frac{d\sigma_{fi}}{d\Omega_{f}}=\frac{k^{2}}{q^{2}}\frac{d\sigma_{if}}{d\Omega_{i}},$
(6)

where $k$ and $q$ are the momenta of the outgoing photon and electron,
respectively.

The well-known expression for the differential photo-ionization cross section
$d\sigma_{if}/d\Omega_{i}$ is given by [11, 12]:

$\frac{d\sigma_{if}}{d\Omega_{i}}=2^{4}\frac{e^{2}\omega}{m{\xi^{4}}}\left(\frac{\xi^{2}}{\xi^{2}+1}\right)^{5}\frac{e^{-4\xi{arccot{\xi}}}}{1-e^{-2\pi\xi}}\frac{(1-\cos^{2}{\theta})}{(W_{0}-\hbar\omega)^{2}},$
(7)

where $W_{0}$ is the ionization potential of the hydrogen atom from the
continuum threshold to the ground state. Here $\omega$ is the frequency of the
photon emitted at the angle $\theta$ relative to the incoming electron, and
$m$ and $e$ are the mass and electrical charge of the electron. The
dimensionless parameter $\xi$ is defined as

$\xi={\frac{{Z\hbar}}{{a_{0}q}}}=\frac{\eta}{q},$ (8)

where $Z$ is the nuclear charge ($Z=1$), $a_{0}$ is the Bohr radius, and
$\eta={Z\hbar}/a_{0}$

##  3 The $S$-matrix element

The $S$-matrix element describing the photo-recombination process (1) in the
presence of the laser field (2) is given by [12, 8, 9]:

$S=-ie\int{d{t}}{\langle{{\Psi}^{H}_{0}(\vec{r},t)|(\vec{\epsilon}\cdot{\nabla})e^{-i(\vec{k}\cdot\vec{r}/\hbar-\omega{t})}|\chi^{e}(\vec{r},t)\rangle}},$
(9)

where $\chi^{e}(\vec{r},t)$ is the Coulomb-Volkov wave function of the
electron in the field of the proton and external laser field,
$\vec{\epsilon},\vec{k}$ and $\omega$ are the polarization vector, momentum
and frequency of the emitted photon, respectively, and
$\Psi^{H}_{0}(\vec{r},t)$ is the wave function of the hydrogen in the laser
field $\vec{\varepsilon}$, (2).

Using the standard technique of transformation to the rotating frame we can
obtain the electron wave function in the total Coulomb-laser field [13]

$\displaystyle\chi^{e}(\vec{r},t)=e^{\frac{\pi{\xi}}{2}}\Gamma(1-i\xi)F(i\xi,1;i(qr-\vec{q}\cdot\vec{r})/\hbar)$
(10)
$\displaystyle\times\exp\left[-\frac{ie}{\hbar{mc}}\int^{t}_{0}\vec{q}\cdot\vec{A}(\tau)d\tau-\frac{ie^{2}}{2\hbar{mc^{2}}}\int^{t}_{0}A^{2}d\tau+\frac{i\vec{q}\cdot\vec{r}}{\hbar}-\frac{i{E_{i}}t}{\hbar}\right],$

where $\vec{q}$ is the momentum of the incoming electron, $q=|\vec{q}|$,
$r=|\vec{r}|$, $F(a,b;x)$ is the confluent hypergeometric function, $E_{i}$ is
the initial kinetic energy of the incoming electron, and $c$ is the speed of
light.

In the harmonic laser field (2) the vector-potential $\vec{A}$ is defined as

$\vec{A}(t)=\frac{c\vec{\varepsilon}_{0}}{\omega_{0}}\cos{\omega_{0}t}\equiv{\vec{A}_{0}}\cos{\omega_{0}t}.$
(11)

In what follows we will use the velocity gauge (or $A\cdot{p}$ gauge).
Therefore the term in the square brackets in (10),
$({ie^{2}}/{2\hbar{mc^{2}}})\int^{t}_{0}A^{2}d\tau$, can be neglected [13].
Evaluation of the remaining integral over $\tau$ in (10) yields

$\displaystyle\chi^{e}(\vec{r},t)=\Gamma(1-i\xi)F(i\xi,1;i(qr-\vec{q}\cdot\vec{r})/\hbar)$
(12)
$\displaystyle\times\exp{i\left[\frac{\vec{q}\cdot\vec{r}}{\hbar}+\frac{e\vec{q}\cdot\vec{\alpha}_{0}\sin{\omega_{0}t}}{m\hbar}-\frac{E_{i}t}{\hbar}-\frac{i\pi{\xi}}{2}\right]},$

where $\vec{\alpha}_{0}=\vec{\varepsilon}_{0}/{\omega^{2}_{0}}$.

Using first-order perturbation theory for deriving the hydrogen wave function
in the presence of the laser field we obtain [8, 9, 10]

$\displaystyle\Psi^{H}_{n}(\vec{r},t)=e^{-iW_{n}t/{\hbar}}$ (13)
$\displaystyle\times\left\\{{\psi_{n}(\vec{r})}-\frac{1}{2}\sum_{m\neq{n}}\left(\frac{e^{i\omega_{0}{t}/\hbar}}{\omega_{mn}+\omega_{0}}+\frac{e^{-i\omega_{0}{t}/\hbar}}{\omega_{mn}-\omega_{0}}\right)\langle{m|\frac{e\vec{A_{0}}\cdot\vec{p}}{\hbar{mc}\omega_{0}}|n\rangle}\psi_{m}(\vec{r})\right\\},$

where $\psi_{m}(\vec{r})$ is the wave function for the atomic electron in the
field-free state $|m\rangle$ with energy $W_{m}$, and
$\omega_{mn}=(W_{m}-W_{n})/\hbar$. The summation in (13) is extended over the
full set of atomic electron states in the absence of the laser field. In the
derivation of (13) it was assumed that none of the denominators were close to
zero [10].

For the optical frequency of the laser we have $\omega_{0}\ll{\omega_{n0}}$
and therefore we get the following expression for $\Psi^{H}_{0}(\vec{r},t)$,
which holds true even over a broader frequency range [8]:

$\displaystyle\Psi^{H}_{0}(\vec{r},t)=e^{-iW_{0}t/\hbar}\left(1+\frac{ie(\vec{\varepsilon}_{0}\cdot\vec{r})}{\hbar{\omega_{0}}}\cos{\omega_{0}t}\right)\psi^{H}_{0}(\vec{r}),$
(14)

where

$\psi^{H}_{0}(\vec{r})=\sqrt{\frac{{Z^{3}}}{{\pi{a^{3}_{0}}}}}e^{-\eta{r}}\equiv{C_{0}e^{-\eta{r}}}$
(15)

##  4 The Coulomb-Volkov wave function

In order to perform the time integration in the $S$-matrix element (9) we
decompose the electron wave function $\chi^{e}(\vec{r},t)$ given by (12) over
the Bessel functions $J_{L}(z)$. For this purpose we introduce the Bessel
generating function:

$\exp(iz\sin{u})=\sum_{L=-\infty}^{L=+\infty}J_{L}(z)\exp(iLu).$ (16)

To simplify the $S$-matrix element (9) we use the recurrence relation for the
Bessel functions:

$J_{L+1}(z)+J_{L-1}(z)=\frac{2L}{z}J_{L}(z).$ (17)

Performing the time integration in (9) and with the aid of the Gauss theorem
we obtain the following expression for the $S$-matrix element in the dipole
approximation ($(\vec{k}\cdot\vec{r})\ll{1}$)

$S=-2\pi{i}\sum_{L=-\infty}^{L=+\infty}f_{L}\delta(W_{0}+\hbar{\omega}-E_{i}+L\hbar{\omega_{0}}),$
(18)

where

$f_{L}=e^{\frac{\pi{\xi}}{2}}\Gamma(1-i\xi){C_{0}}\left[J_{L}(z)\omega(L)\left(I_{1}+\frac{L}{z}I_{2}\right)\right].$
(19)

Here we have introduced the following notations:

$z=\frac{e(\vec{q}\cdot\vec{\alpha}_{0})}{{m\hbar}},$ (20)

$I_{1}=\eta\hbar\int{d\vec{r}}{\psi}^{H}_{0}(\vec{r})\frac{(\vec{\epsilon}\cdot\vec{r})}{r}\chi^{e}(\vec{r}),$
(21)

$I_{2}=\frac{ie}{\omega_{0}}\int{d\vec{r}}{{\psi}}^{H}_{0}(\vec{r})\left(-(\vec{\varepsilon}_{0}\cdot{\vec{\epsilon}})+\eta\frac{(\vec{\varepsilon}_{0}\cdot\vec{r})(\vec{\epsilon}\cdot\vec{r})}{r}\right)\chi^{e}(\vec{r}),$
(22)

and

$\hbar{\omega(L)}=E_{i}-W_{0}+L\hbar{\omega_{0}}\equiv{E_{i0}+L\hbar{\omega_{0}}}.$
(23)

Exploiting the well-known integral involving the confluent hypergeometric
function [12, 14]

$\displaystyle\int{d\vec{r}}e^{i(\vec{q}-\vec{p})\cdot\vec{r}/\hbar-\eta{r}/\hbar}\frac{F(i\xi,1,i(qr-\vec{q}\cdot\vec{r}))}{r}=4{\pi}\hbar^{2}\frac{[\vec{p}^{2}+(\eta-i{q})^{2}]^{-i{\xi}}}{[(\vec{q}-\vec{p})^{2}+\eta^{2}]^{1-i\xi}},$
(24)

we get the following expression for (21):

$I_{1}=8\pi{i}\hbar^{4}(\vec{\epsilon}\cdot\vec{e}_{q})\frac{\xi(1-i\xi)}{q^{2}(1+\xi^{2})^{2}}e^{-2\xi{arccot{\xi}}},$
(25)

and the corresponding expression for (22):

$\displaystyle
I_{2}=-8\pi{i}\hbar^{4}\frac{\xi{e}}{\omega_{0}}\frac{e^{-2(1+\xi){arccot{\xi}}}}{q^{3}(1+\xi^{2})^{2}}\left((\vec{\varepsilon}_{0}\cdot\vec{\epsilon})-2(\vec{\epsilon}\cdot{\vec{e}_{q}})(\vec{\varepsilon}_{0}\cdot{\vec{e}_{q}})\frac{(2-i\xi)}{(1-i\xi)}\right),$
(26)

where $\vec{e}_{q}\equiv{\vec{q}/q}$ is a unit vector.

##  5 The partial cross section

The partial cross section of the reaction (1) with fixed $L$ is given by

$d\sigma_{L}=2\pi\frac{e^{2}}{2q\omega(L)}|f_{L}|^{2}\delta(W_{0}+\omega-
E_{i}+L\hbar{\omega_{0}})\frac{d^{3}k}{(2\pi)^{3}}.$ (27)

The integration over $\omega$ yields

$\displaystyle\frac{d\sigma_{L}}{d\Omega}=\frac{e^{2}C^{2}_{0}}{8{\pi}^{2}q(1-e^{-2\pi{\xi}})}\left(E_{i}-W_{0}+L\hbar{\omega_{0}}\right)^{3}$
(28)
$\displaystyle\times|J_{L}(z)|^{2}\left(|I_{1}|^{2}+\frac{2Re(I_{1}I_{2})}{z}L+\frac{L^{2}}{z^{2}}|I_{2}|^{2}\right).$

Here the constant $C_{0}$ was defined in (15). The total cross section of the
reaction (1) in the laser field (2) is obtained with

$\frac{d\sigma}{d\Omega}=\sum^{L=+\infty}_{L=-\infty}\frac{d\sigma_{L}}{d\Omega}.$
(29)

##  6 The summation procedure and cross section

We introduce a new step that allows one to analytically sum up the infinite
series (29). The summation over $L$ in (29) is performed with the aid of the
Plancherel theorem [15],

$\frac{1}{2\pi}\int^{2\pi}_{0}{|f(x)|^{2}dx}=\sum^{n=+\infty}_{n=-\infty}|c_{n}|^{2},$
(30)

where $c_{n}$ are the Fourier coefficients of the function $f(x)$,

$c_{n}=\frac{1}{2\pi}\int^{2\pi}_{0}{f(x)e^{i\pi{nx}}}dx.$ (31)

The application of the Plancherel theorem to the Bessel generating function
(16) leads to the following equalities [16]:

$\displaystyle\sum_{L=-\infty}^{L=+\infty}J^{2}_{L}(z)=1,$ (32)
$\displaystyle\sum_{L=-\infty}^{L=+\infty}L^{2}J^{2}_{L}(z)=\frac{z^{2}}{2},$
(33)
$\displaystyle\sum_{L=-\infty}^{L=+\infty}L^{2n-1}J^{2}_{L}(z)=0,n\in{{Z}_{+}}$
(34)
$\displaystyle\sum_{L=-\infty}^{L=+\infty}L^{4}J^{2}_{L}(z)=\frac{z^{2}(4+3z^{2})}{8}.$
(35)

Performing the summation over the photon polarizations we obtain the closed
analytical expression for the cross section of the process (1):

$\displaystyle\frac{d\sigma}{d\Omega}=\frac{e^{2}C_{0}^{2}E_{i0}^{3}}{8{\pi}^{2}q(1-e^{-2\pi{\xi}})}\left\\{|I_{1}|^{2}+\left[\frac{|I_{2}|^{2}}{2}\right.\right.$
(36)
$\displaystyle+\frac{3\hbar\omega_{0}z^{2}}{2E_{i0}^{2}}\left(\frac{2E_{i0}\cdot{Re(I_{1}I_{2})}}{z}+\hbar\omega_{0}|I_{1}|^{2}\right)$
$\displaystyle+\left.\left.\frac{\hbar^{2}\omega_{0}^{2}z^{2}(4+3z^{2})}{8E_{i0}^{3}}\left(\frac{3E_{i0}|I_{2}|^{2}}{z^{2}}+\frac{2\hbar\omega_{0}\cdot{Re(I_{1}I_{2})}}{z}\right)\right]\right\\}.$

Here $I_{1}$ specifies the space integral (25) for the field-free
recombination process. $I_{2}$ is the spatial integral (26) of the laser-
assisted recombination process. The parameter
$z=e(\vec{q}\cdot\vec{\alpha}_{0})/{m\hbar}=e(\vec{q}\cdot{\vec{\varepsilon}_{0}})/{m\hbar{\omega^{2}_{0}}}$
was introduced in (20), where $\vec{q}$, $\varepsilon_{0}$, and $\omega_{0}$
denote the momentum of the incoming electron, the amplitude of the laser
field, and the field frequency, respectively. The parameter
$E_{i0}\equiv{E_{i}-W_{0}}$ is the difference between the kinetic energy of
the incoming electron and the hydrogen ground state. The constant
$C_{0}=\sqrt{{Z^{3}}/{\pi{a^{3}_{0}}}}$ represents the normalization constant
(15) of the hydrogen wave function (14) in the ground state.

It can be seen that in the zero-field limit, which corresponds to $z\equiv{0}$
and $I_{2}\equiv{0}$, the square brackets in (36), which are responsible for
the laser modified cross section, are identically zero.

To the best of our knowledge, such a closed expression for the laser assisted
hydrogen recombination was not given in the literature up until now.

An explicit summation over the photon polarizations is given by the following
equalities

$\displaystyle\sum_{\lambda}\epsilon^{\lambda*}_{\mu}\epsilon^{\lambda}_{\nu}=\delta_{\mu\nu},$
(37)
$\displaystyle\sum_{\lambda}(\vec{a}\cdot\vec{\epsilon}^{\lambda})^{2}=a^{2}(1-\cos^{2}{\vartheta}),$

where $\vartheta$ is the angle between the vector $\vec{a}$, and the momentum
of an outgoing photon $\vec{k}$.

The corresponding expressions for (25) and (26) with an explicit summation
over the photon polarizations are given by the following equalities

$\sum_{\lambda}\left|I_{1}\right|^{2}=2^{6}\pi^{2}\hbar^{8}\frac{\xi^{2}e^{-4\xi{arccot{\xi}}}}{q^{4}(1+\xi^{2})^{3}}(1-\cos^{2}{\theta}),$
(38)
$\displaystyle\sum_{\lambda}\left|I_{2}\right|^{2}=2^{6}\pi^{2}\hbar^{8}\frac{{e^{2}}\xi^{2}}{\omega_{0}^{2}}\frac{e^{-4(1+\xi){arccot{\xi}}}}{q^{6}(1+\xi^{2})^{5}}\times$
(39)
$\displaystyle\left[\varepsilon^{2}_{0}(1-\cos^{2}{\phi})(1+\xi^{2})-4(\vec{\varepsilon}_{0}\cdot{\vec{e}_{q}})^{2}(2+\xi^{2})+4(\vec{\varepsilon}_{0}\cdot{\vec{e}_{q}})^{2}(4+\xi^{2})(1-\cos^{2}{\theta})\right],$

and by the corresponding expression for the interference term

$\sum_{\lambda}Re(I_{1}I_{2})=2^{6}\pi^{2}\hbar^{8}\frac{{e}\xi^{2}}{\omega_{0}}\frac{e^{-2(1+2\xi){arccot{\xi}}}}{q^{5}(1+\xi^{2})^{4}}(\vec{\varepsilon}_{0}\cdot{\vec{e}_{q}})(4\cos^{2}{\theta}-3),$
(40)

where $\theta$ is the angle between the momentum of incoming electron
$\vec{q}$ and the momentum of an outgoing photon $\vec{k}$. The angle $\phi$
is formed by vector $\vec{\varepsilon}_{0}$ and vector $\vec{k}$.

In order to give an estimation for the order of magnitude of the laser field
correction to the recombination process we employ the Keldysh dimensionless
tunneling parameter [17]:

$\gamma=\frac{\omega_{0}}{e\varepsilon_{0}}\sqrt{2mW_{0}},$ (41)

which for characteristic numerical values
$\varepsilon_{0}\equiv{|\vec{\varepsilon}_{0}}|\sim{5\times 10^{7}}$ V/cm, and
$\hbar{\omega_{0}}\sim{1}$ eV, and $W_{0}=13.6$ eV has the value
$\gamma\sim{4}$.

The parameter $z$ (20) can be easily expressed in terms of the Keldysh
tunneling parameter and for the case $E_{i}\sim{W_{0}}=13.6$ eV has the
following numerical value

$z=\frac{e(\vec{q}\cdot\vec{\alpha_{0}})}{{m\hbar}}=\frac{2\sqrt{E_{i}W_{0}}}{\gamma{\hbar{\omega_{0}}}}\sim{7},$
(42)

and the parameter $\xi$ given by (8) can be estimated as

$\xi={\frac{{Z\hbar}}{{a_{0}q}}}\sim{1}.$ (43)

Finally we get the following estimations for the field-influenced terms
confined by the square brackets (36)

$\frac{|I_{2}|^{2}}{|I_{1}|^{2}}\sim{\kappa\equiv{\left|\frac{e\varepsilon_{0}}{q\omega_{0}}\right|^{2}}=\frac{1}{\gamma^{2}}\frac{W_{0}}{E_{i}}\sim{\frac{1}{16}}},$
(44)
$\frac{\hbar{\omega_{0}}z}{E_{i0}}\frac{Re(I_{1}I_{2})}{|I_{1}|^{2}}\sim{\kappa}\sim{\frac{1}{16}},$
(45)
$\frac{(\hbar{\omega_{0}}z)^{2}{|I_{1}|^{2}}}{E^{2}_{i0}{|I_{1}|^{2}}}\sim{\kappa}\sim{\frac{1}{16}},$
(46)
$\frac{\hbar^{2}\omega_{0}^{2}(4+3z^{2})}{E_{i0}^{2}}\frac{|I_{2}|^{2}}{|I_{1}|^{2}}\sim{\kappa^{2}}\sim{\frac{1}{256}},$
(47)
$\frac{(\hbar\omega_{0})^{3}z(4+3z^{2})}{E_{i0}^{3}}\frac{Re(I_{1}I_{2})}{|I_{1}|^{2}}\sim{\kappa^{2}}\sim{\frac{1}{256}}.$
(48)

The field-influenced terms, $\left|I_{1}\right|^{2}$ and
$\left|I_{2}\right|^{2}$, are positive and accompany the recombination
process. According to (40) the interference term, $Re(I_{1}I_{2})$, is
positive under the following conditions

$\displaystyle(\vec{\varepsilon}_{0}\cdot{\vec{e}_{q}})>0,\theta\in\left(-\frac{\pi}{6};\frac{\pi}{6}\right)\bigcup\left(\frac{5\pi}{6};\frac{7\pi}{6}\right);$
(49)
$\displaystyle(\vec{\varepsilon}_{0}\cdot{\vec{e}_{q}})<0,\theta\in\left(\frac{\pi}{6};\frac{5\pi}{6}\right)\bigcup\left(-\frac{5\pi}{6};-\frac{\pi}{6}\right).$

In the particular case with
$(\vec{\varepsilon}_{0}\cdot{\vec{e}_{q}})\equiv{0}$ the interference terms
are absent.

Based on the obtained estimations (44)-(48) we do not see the predicted [9]
laser contraction of the hydrogen (antihydrogen) recombination process.

The basic estimations, (44)-(48), show that the field influence terms are
directly expressed in terms of the dimensionless parameter
$\kappa=\left|{e\varepsilon_{0}}/{q\omega_{0}}\right|^{2}$. It is proportional
to the intensity of the laser field, $|\varepsilon_{0}|^{2}$, and inversely
proportional to the square of the field frequency, $1/\omega_{0}^{2}$. This is
justified by the chosen electron (12) and hydrogen (14) laser modified states,
where in both cases there is a dependence on the reciprocal field frequency.
The spatial integral of the laser-assisted recombination (26) is more
sensitive to the momentum of the incoming electron than the field-free spatial
integral (25). This results in the inverse proportionality between $\kappa$
and $q^{2}={2mE_{i}}$.

The parameter
$\kappa\equiv{\left|{e\varepsilon_{0}}/{q\omega_{0}}\right|^{2}}={1}/{\gamma^{2}}{W_{0}}/{E_{i}}$
governs the laser-assisted recombination process and points out a possible
ways for an increasing a hydrogen laser-assisted recombination rate. An
increase of the parameter $\kappa$ by lowering the parameter ${\gamma^{2}}$ is
the most natural way to improve a recombination rate of a hydrogen atom in a
laser field. Although it is experimentally feasible, this path has to be
examined carefully due to an arising ionization processes of the produced
hydrogen atom. Ionization processes have not been considered in the proposed
model and therefore a quantitative treatment requires a full solution of the
time-dependent Schrödinger equation [18].

The binding electron energy $W_{0}$ is a well-defined value and can not be
used in the increasing the laser-assisted recombination rate. The ultimate
possibility to increase the parameter $\kappa$ is decreasing the relative
kinetic energy between electron and a proton $E_{i}$ for which one can achieve
a reasonably small value which would mean improving a laser-assisted
recombination rate. This fact has a clear physical explanation: for a quasi-
static regime in the inverse to the laser-assisted recombination process, i.e.
in the laser-assisted photo-ionization process, the energy of the emitted
photo-electrons has a peak at zero value. In our case of laser-assisted
recombination process this peak corresponds to a maxima value of photo-
recombination rate.

##  7 The soft photon approximation

The cross section given by (36) is an exact result for the laser assisted
hydrogen recombination process under the proposed approximations for the
electron and hydrogen laser modified wave functions. To clarify the meaning of
the obtained result we shall introduce a soft photon approximation. This
allows one to reveal the meaning of each term in the expression for the cross
section of the process given by (36). With this approximation the frequency of
the emitted photon is independent of the number of the field harmonics $L$:

$\hbar\omega=E_{i}-W_{0}+L\hbar{\omega_{0}}\simeq{E_{i}-W_{0}}.$ (50)

This is justified as the low-frequency field limit, or the soft photon limit
[8]. In this case we are able to produce a simple but non-trivial result. In
the soft photon approximation the corresponding expression for the partial
”soft photon” cross section is given by

$\displaystyle\frac{d\sigma^{sf}_{L}}{d\Omega}=\frac{e^{2}C^{2}_{0}}{8{\pi}^{2}q(1-e^{-2\pi{\xi}})}\left(E_{i}-W_{0}\right)^{3}$
(51)
$\displaystyle\times|J_{L}(z)|^{2}\left(|I_{1}|^{2}+\frac{2Re(I_{1}I_{2})}{z}L+\frac{L^{2}}{z^{2}}|I_{2}|^{2}\right).$

Performing the summation (29) over $L$ by means of the equalities (32)-(34) we
get the following simple result:

$\displaystyle\frac{d\sigma^{sf}}{d\Omega}=\frac{e^{2}C^{2}_{0}}{8{\pi}^{2}q(1-e^{-2\pi{\xi}})}{E_{i0}^{3}}\left(|I_{1}|^{2}+\frac{|I_{2}|^{2}}{2}\right).$
(52)

Here the first term $|I_{1}|^{2}$ corresponds to the standard laser-free
recombination process whereas the second term $|I_{2}|^{2}$ is responsible for
the field modified electron (12) and hydrogen (14) states. In the zero-field
limit $I_{2}\equiv{0}$ and (52) recovers the standard field-free recombination
cross section. We have to note that within the limits of the present
approximation (50) the interference terms $Re(I_{1}I_{2})$ are absent. Thus in
this and only this particular case does the square of the $S$-matrix element
(18) equal the sum of the squares of its terms. So we have proved:

Theorem The S-matrix element

$S=-2\pi{i}\sum_{L=-\infty}^{L=+\infty}f_{L}\delta(W_{0}+\hbar{\omega}-E_{i}+L\hbar{\omega_{0}})$

with

$f_{L}=e^{\frac{\pi{\xi}}{2}}\Gamma(1-i\xi){C_{0}}\left[J_{L}(z)\omega(L)\left(I_{1}+\frac{L}{z}I_{2}\right)\right]$

under the approximation

$\hbar\omega=E_{i}-W_{0}+L\hbar{\omega_{0}}\simeq{E_{i}-W_{0}\neq{\hbar\omega(L)}},$

equals to the sum of the squares of individual terms

$|S|^{2}=\left|2\pi{e}^{\frac{\pi{\xi}}{2}}\Gamma(1-i\xi){C_{0}}\right|^{2}\delta^{2}(W_{0}+\hbar\omega-
E_{i})\omega^{2}\left(|I_{1}|^{2}+\frac{|I_{2}|^{2}}{2}\right).$

The Theorem reveals the meaning of each term in the expression for the laser-
assisted hydrogen photo recombination given by (36). The first term in the
braces (36), $|I_{1}|^{2}$, is responsible for the field-free recombination
process. The first term in the square brackets (36), $|I_{2}|^{2}/2$, reflects
the laser-modified electron and hydrogen states and does not take into account
the changes in the frequency of the emitted photon, according to the Theorem.
The four terms in the parentheses (36) are the only terms which contribute to
the change of the frequency of the emitted photon in the process.

##  8 Summary

In this paper we have developed a new method that allows one to obtain an
analytical cross section for the laser-assisted electron-ion collision. The
standard $S$-matrix formalism is used for describing of the collision process.
The $S$-matrix element is constructed from the electron Coulomb-Volkov wave
function in the combined Coulomb-laser field, and the hydrogen laser modified
state. By the aid of the Bessel generating function, the $S$-matrix element is
decomposed into an infinite series of the field harmonics.

We have introduced a new step to obtain an analytical expression for the cross
section of the process. The main theoretical novelty is the application of the
Plancherel theorem to the Bessel generating function. This allows one to
obtain an analytical expression for the laser assisted hydrogen photo
recombination process.

The laser-assisted hydrogen recombination process has been chosen in order to
verify the proposed method. The field-enhancement coefficient is evaluated in
an analytical way. The final expression for a laser-assisted hydrogen
recombination process is presented by the sum of the field-free hydrogen cross
section and the laser-assisted addition. The field-dependent terms are
expressed through the dimensionless parameter
$\kappa\equiv{\left|{e\varepsilon_{0}}/{q\omega_{0}}\right|^{2}}$.

By introducing a soft photon approximation, based on the assumption of the
independence between the frequency of the emitted photon and the field
harmonics, the square of the $S$-matrix element is represented by the sum of
the squares of its individual terms. We provide the proof of the corresponding
theorem.

The developed method will allow one to reconsider a wide range of problems
related to electron-ion collisions in an external field with the goal of
obtaining an analytical expression for the cross sections of the corresponding
process. The time-dependent problem generated by the infinite series of the
Coulomb-Volkov wave function is exactly separated from the spatial dependence
and thus can be analytically solved by the method.

One of the challenging problems in modern electron-ion collision theory is the
calculation of a laser assisted three-body hydrogen formation process. As far
as we know an analytical solution for this important process has not been
found. The developed method allows one to obtain an analytical expression for
this process.

## Acknowledgements

The authors are grateful to L. N. Labzowsky and V. G. Zelevinsky for valuable
discussions. Also we are thankful to the Referees for a number of helpful
suggestions for the improvement of this paper.

G.S. acknowledges the support from the Institute for the Quantum Sciences at
Michigan State University.

## References

## References

  * [1] Mittleman M H 1993 Introduction to the Theory of Laser-Atom Interactions (New York: Plenum Press)
Joachain C J 1994 Laser Interaction with Atoms, Solids and Plasmas (New York:
Plenum Press)

  * [2] Gabrielse G et al 2002 ATRAP collaboration Phys. Rev. Lett 89 213401
Amoretti M et al 2002 ATHENA Collaboration Nature 419 456

  * [3] Gabrielse G et al. 2010 CERN-SPSC-2010-006 http://cdsweb.cern.ch/record/1234581/files/
  * [4] Amoretti M 2006 et al ATHENA Collaboration Phys. Rev. Lett. 97 213401
Gabrielse G 2008 et al ATRAP collaboration Phys. Rev. Lett. 100 113001

  * [5] Pohl T, Vrinceanu D, and Sadeghpour H R 2008 Phys. Rev. Lett. 100 223201
  * [6] Robicheaux F 2004 Phys. Rev. A 70 022510
Roy S, Ghosh Deb S, and Sinha C 2008 Phys. Rev. A 78 022706

  * [7] Gabrielse G 2005 Adv. At., Mol., Opt. Phys. 50 155
  * [8] Reiss H R 1980 Phys. Rev. A 22 1786
Byron F W, Francken P, and Joachain C J 1987 J. Phys. B 20 5487
Franken P, Joachain C 1987 Phys. Rev. A 35, 1590
Franken P, Joachain C 1990 J. Opt. Soc. Am. B 7 554

  * [9] Shu-Min L, Ji C, Jian-Ge Z, and Hong-Jun Y 1993 Phys. Rev. A 47 1197
Shu-Min L, Yan-Gang M, Zi-Fang Z, Ji C, and Yao-Yang L 1998 Phys. Rev. A 58
2615

  * [10] Landau L D and Lifschitz E M 1977 Quantum Mechanics (Non-Relativistic Theory) (Oxford, England: Pergamon Press)
  * [11] Stobbe M 1930 Ann. Phys. 7 661
  * [12] Akhiezer A I and Berestetskii V B 1965 Quantum Electrodynamics (New York: Interscience Publishers)
  * [13] Jain M and Tzoar N 1978 Phys. Rev. A 18 538
  * [14] Akhiezer A I and Merenkov N P 1996 J. Phys. B 29 2135
  * [15] Rudin W 1976 Principles of Mathematical Analysis (New York: McGraw-Hill)
  * [16] Bateman G and Erdelyi A 1953 Higher Transcendental Functions (New York: McGraw-Hill)
Gradshteyn I S and Ryzhik I M 1965 Table of Integrals, Series and Products
(New York: Academic Press)

  * [17] Keldysh L V 1965 Sov. Phys. JETP 20 1307
  * [18] K. C. Kulander 1987 Phys. Rev. A 35 445
J. L. Krause, K. J. Schafer, and K. C. Kulander, 1992 Phys. Rev. A 45 4998


Nested have been widely studied in the past 25 years, both theoretically using category theory, and practically in programming languages such as . They consist in recursive polymorphic where the type parameter changes throughout the recursion. They have a variety of applications such as modelling memory or modelling constraints over regular without relying on dependent types. In this work, we focus on a specific subset of nested which we call Linked Nested DataTypes (). We show that some usual such has List and Maybe, as well as some well-known nested such as Nest and even Bush can be built as various instances of . We proceed by presenting , a library, developed both in and , which focuses on the set of constructs that can be spread directly from the parameter on which a is built, to the itself. These spreadable elements are of two kinds, functions, such as folds and map, and properties, such as the congruence of map or the satisfaction of a given predicate for at least one, or all, elements of the structure. We make use of the dependent type system of both and to model the latter. This paper ends with a discussion about

various interesting topics that were raised throughout our development such as the issue of termination, the comparison of our tools and the proof effort required to extend with additional elements.

§ INTRODUCTION

Data structures are key in handling many programming challenges. From the easiest algorithms to more advanced features or conceptually challenging programs, choosing the right data structure is often mandatory in programming activities. Functional programming, and associated languages, usually provide constructs to model such structures, which can be summed up as , where a type is defined with a list of constructors, each of which builds an element of the type  using a given number of inputs. While imperative and object-oriented languages do have , they often manifest in a different manner, which will not be considered in this paper. These are widely used in programming activities and can model various concepts, depending on the type system of the language in which they are defined. They can represent concrete data, in usual functional programming languages such as and , and even properties in dependently typed languages such as  [13] and  [2], both of which have been used in this work.

As mentioned before, relying on relevant to conduct programming activities is essential, even more so when said types are meant to model some high-level specification over concrete data. To help users in selecting the right , they are categorized and studied. Our work takes place in that area. The simplest are the enumerations, where a type is built from a set of constant values, modelled by a set of unparametrized constructors.
More interesting allow  constructors to have parameters. When one or more of these parameters are typed with the type that is being defined, the in question is recursive, a family of types which is all the more interesting. This family is particularly used and studied and is tied to the notion of induction. Among these recursive , a distinction exists between regular and non-regular, also called nested,  [1, 3, 8].

A is regular when its type parameter – if any – is always the same whenever it appears in the definition. In other words, if the type is polymorphic, then its type parameters are the same both in the signature of the type, as well as in the recursive constructors. Famous examples of regular are  lists and trees, defined in as follows, where  is the type parameter:

data List a = Empty | Cons(a, List a)
data Tree a = Tip a | Bin(Tree a, Tree a)

A is non-regular, or nested, when its type parameter changes between the type signature and at least one of its  instances in the constructors. Well-known nested are the nests (sometimes called pow in the literature) and, most of all, the bushes, where the nesting (the way the type parameter changes) is done with the type definition itself, as shown below:

data Nest a = Zero a | Succ (Nest (a, a))
data Bush a = BLeaf  | BNode (a, Bush (Bush a))

Nested have been widely studied since 1998 [3], both theoretically using category theory, and practically in programming languages such as . Many approaches deal with nested as an abstract notion, and try to theorize their use, regardless of their inner structure. Others are particularly interested in the folds that can be written on these structures [4, 9, 12, 7, 14]. Folding nested values is indeed mandatory because, due to the constrained nature of their type, this is the main way users have to interact with the value itself. Furthermore, these folds have to, and can, be as generic as possible, leading to the definition of powerful iterators, as well as induction principles. In his thesis [1], Bayley is also interested in the genericity of other functions such as zip or membership. Our work shares this advocated approach of genericity around nested .

In order to extend the number of notions that can be generic over nested , we do not consider all their possible incarnations. Rather, we focus on a subset of all the possible nested , which we call . Moreover, we are interested in functions and properties that we can obtain for free from their definition, in the same spirit as Theorems for free [16], the deriving mechanism of  [11], or even the use of Finger Trees [10]. Finger Tree is a general nested , parametrized by a monoid, the instantiation of which can lead to ordered sequences or interval trees. Indeed, our are characterized by a common structure with a changing type parameter, responsible for nesting the structure differently.

To that purpose, we have developed a core library, named , available on the first author's github page[], in both and , making it accessible to a large number of users. This library provides the users with several nested , defined as instances of , as well as a core set of spreadable components that are elements derivable
from the type parameter to the nested itself.
These spreadable elements are of two kinds, functions, such as folds and map, and properties, such as the congruence of map or the satisfaction of a given predicate for at least one, or all, elements of the structure.
This paper presents the content of this library, with the following outline.

Section <ref> presents the thought process behind the definition of our , while also giving examples of that can be built from them. Section <ref> and <ref> provide examples of spreadable constructs that can be derived for our from the corresponding definitions of the underlying type parameter. Section <ref> focuses on computational such aspects, while Section <ref> focuses on logical ones. Section <ref> shows a visual summary of these elements. Finally, Section <ref> proposes a discussion around some limitations and open questions that remain to be answered and that would benefit future works.

Throughout these sections, snippets of code are presented, which come from the implementation of our work. These are type-checked pieces of code, ensuring their correctness, which is made possible through the use of , a tool to combine code with  documents.

§ INTRODUCING LINKED NESTED DATATYPES ()

§.§ Introductory examples: ,  and

The most common inductive is the type of lists which consists of an arbitrary number of elements linked one after the other. Written inductively using , lists can be defined, as usual, using two constructors: the constant empty list [] and the cons operator _::_ written in an infix manner using underscores. We use the subscript $_0$ to mean this definition is not derived from .

Lists are parametrized by a given type  from a given level of universe . An interesting feature of such a type – that is usually not mentioned, although relevant in our case – is that the recursive constructor takes as a parameter an element of type  where  is parametrized by the same type parameter as its definition, namely . This makes it a regular rather than a nested one, where such a type parameter is assumed to vary throughout the recursion. As a first example of such a nested , let us consider the  :

In this case, the recursive constructor – purposely named identically as the one for lists – takes as a parameter an element of type  where  is a pair of elements of type . This makes  a nested , where its type parameter evolves throughout the recursion using, in this case, the function , which we call a type transformer. As visible, both  and  are very similar in their structure, and their only difference is the type parameter on which the newly defined type is recursively called. As a last example, let us consider the  , nested with itself:

In this case, not only does the type parameter changes in the recursive call, but it changes with a dependence to the type that is being defined. While picturing lists and nests is fairly simple, picturing a bush is challenging. Thankfully, while the parameter change depends on  itself, the form of the type is fairly similar to lists and nests, which calls out for a common denominator between the three – and possibly more – types, thus leading to a better picturing and understanding of bushes in the process. This is such a case where providing a relevant abstraction can significantly ease the study of its concrete counterparts, which is especially true for bushes, and motivates our approach.

§.§ Definition of

The common denominator between the three aforementioned types is a structure we capture in our concept of . are parametrized by a , that is an entity which, given a level of universe  and a type living in , provides another type living in . In , our type transformers are called ; they live in Set$\omega$ (a sort above all others), and are defined as follows:

This leads to the following definition:

It is interesting to note that this applied to a certain is itself a , that is, for any  of type , we have that  also is a  . Thus, LNDT is informally of type [The signature of the related definition had to be tweaked a little to match Agda's distinction between type parameters and the sort of the datatype, a distinction marked by the colon.]. As a consequence , in addition to defining spreadable properties over , also introduces a certain number of in the process, as shown in Figure <ref>.

§.§ ,  and  as instances of

Tuples Naturally, the three types considered as examples, ,  and  can be written as instances of , once we provide the right for each of them. While the for  will be the type itself, we can notice that the required for  and  can be abstracted in a notion that we call :

A tuple indexed by  and parametrized by a type  is a collection of  elements of type . This is similar to the dependent types of vectors, where  stands for a list of  elements of type . However, tuples are more convenient in our case because we never want them to be empty, which vectors can be, and they induce in our development some technical conveniences, on which we will not linger.

N-perfect trees Having defined the tuples, the family of based on them follows. They are parametrized by the size of the tuple on which they depend:

We can notice that based on  of a certain index  can actually be seen as ($n+1$)-perfect trees [18]. Any value for $n$ gives us a certain type of tree, with two examples being  and , as defined in the following paragraph. They are perfect in the sense that all the nodes at a given depth either have no child or ($n+1$) children, which means that the overall number of nodes is $\sum\limits_{i=0}^k (n + 1)^i$, where $k$ is the depth of the tree.

Lists, nests and bushes Thanks to the previous notions, we can finally jump to the definitions of ,  and , seen as with specific :

This definition of  requires to ignore termination checking – although it is not shown here, it is required nevertheless –, which was not the case when defining . This comes from the fact that positivity checking differs from termination checking. While the two definitions are equivalent, the first one relies on positivity checking because it is directly defined as a while the second one relies on termination checking since it is defined as an instance of .

Such a termination checking cannot automatically succeed, which makes the use of  as well as functions over  and  unsafe. rejects both definitions as unsafe and disallows their use, while allows these definitions but considers them unsafe. This has the upside that working with bushes is possible in , although the problem of termination checking to make their use safe remains and will be further discussed in Section <ref>.

Examples Here is an example of :

An example of :

And an example of :

§.§  as instance of

Another possible instance of , is actually – and surprisingly – the usual  type ( in ML-like languages)
which is built from the  , corresponding to the logical negation.

The idea comes from the fact that such a  always builds empty types, thus only allowing the structure to be empty (using ), or to contain a single element (using ), since any further nesting will not be inhabited.

In addition, by using the  keyword provided by , which allows the developer to define aliases usable in pattern-matching situations, we can provide an alternate definition of the  type as an instance of , by mapping  to  and () to (). By doing so, we ensure that this definition and the usual one are syntactically equivalent, in addition to behaving the same way.

This type has the right semantics, which means that any element of type  is either of the form  or , as expected. This has been proven in although the proof is not presented here. While defining  in this alternate manner is not necessarily relevant per se, it is interesting to see another way of building such a type, as well as to notice that , thanks to the  mechanism, allows the developer to use this type exactly as one would use the usual  type from the current standard library. Moreover, discovering hidden patterns between types is often enlightening, and always exciting.

§.§ Multi-layered

As noticed in Section <ref>, for any  of type ,  has type  too, which means that we can keep building new interesting by chaining multiple calls to . While we say "interesting", it is fair to say that not all such attempts indeed bear that characteristic. However, some do, and below is an example of a second degree that can be built, and from which multiple features will be retrieved for free, thanks to the spreadable properties depicted later on. We call this type :

Here is an example of an inhabitant of , starting with a natural number, then a list of natural numbers, then a list of lists of natural numbers, and so on:

§.§ Overview of our

Figure <ref> shows an overview of the that were defined in LibNDT, and how they relate with one another. The light green boxes represent concrete types while the others are abstract types which were used to build them. For instance, the box labelled "Maybe" and the arrows that depart from it, depict that the type  is the result of the instantiation of  with  as a parameter. In the case of the  type, the label of the related box is underlined to indicate that the definition is not safe.

Type transformers in LibNDT

§ COMPUTATIONAL COMMON BEHAVIOURS

However tempting regrouping these types under a common denominator is, the relevance of this process depends on the possibility to express behaviours at the level which could then be instantiated to any of its instances. The remaining of this paper stands as a list of arguments in favour of this relevance, that is, a list of behaviours that can indeed be expressed for . Such behaviours will be regrouped into two classes: computational ones, that is concrete functions relying on the content of , and logical ones, that is properties either directly bound to or functions that work on them. In other words, the first class contains functions that process elements from while the second class contains everything else. This section depicts our results regarding the first class of common behaviours.

§.§ Mapping

When considering functions that work on collections of elements, a few examples come to mind, the first of which is the  primitive. The reasoning behind  is well-known and natural: when possible, using some function , to transform elements of type  to elements of type , it should be possible to transform a collection of elements of type  to a collection of elements of type  through a procedure, parametrized by , called . We begin by studying this assumption for .

Building map functions for  As this is our first example of common behaviour, let us consider, in details, the steps in our reasoning. Since lists are the simplest example of , we can start by considering the usual  function written on lists. Below is the common definition of maps for lists (subscripted by $_0$), which bears no understanding difficulties.

Writing a similar function for nests is more challenging because the tail of the nest is not of the same type of the nest itself, which means the same function  cannot be passed as it is in the recursive call.

However different, these two have a lot in common, which can be captured using , as long as the way the function  must be transformed throughout the recursion is provided. By taking as parameter this transformation of function, and calling it , we propose the following implementation for .

While the signature of this function is not straightforward, it is possible to make it clearer by noticing a certain regularity in its core, which can be made visible as follows:

This definition gives an abstract signature to  for which it is possible, given a function from  to , to build a function from  to  that is, a map function. Using this new notation, the map function over has a far better looking – and much more explicit – signature.

The latter definition gives us an important insight as to what  stands for: it is a procedure that ensures it is possible to map on provided it is possible to map over the on which they are build. This is the first property that justifies the spreadable aspect of this library: we study which elements can be transported from  to , and  as defined earlier is one of them.

Instantiating map functions In order to deduce map functions for , all is needed is to define a map function for the on which they are based. The first function, which can be spread to the corresponding , is called the seed for the associated behaviour. In this case, the behaviour is the ability to map over a given type. Here is the map seed for tuples:

The definitions of maps for are hence straightforward:

We can notice that the map function on bushes is recursively generated using itself, solely relying on  as a way of computing a result. In other words, the seeds for bushes will never have to be defined and any behaviour on bushes is always solely generated with the associated spreadable property.

Examples of usage of map functions As a first example, here is a list of natural numbers on which the successor function is mapped:

As a second example, we define a bush of natural numbers on which we map the function of multiplication by two:

In both cases,  is a correctly typed term regarding the signature of the function, which means both sides of the equality are indeed the same. These examples are by no means a proof of correctness of the  functions, but rather a convincing argument in favour of our approach and definitions.

Back to squared lists Squared lists are second degree , in the sense that they are built by  two successive  nestings. However, regardless of the number of successive nestings, we can provide a map function as long as the seed – the original – provides a map function itself. The map function  for squared lists is obtained as follows:

As an example of usage of this newly created map function, we can apply a multiplication by two on all elements of the example
defined in Section <ref>.

As shown in this example, nesting several times over a given does not alter our ability to provide free functions from the seed of the chain. Throughout this paper, more examples of spreadable behaviours will be given, all of which can be spread several times similarly. As a consequence, we will not explicitly go back to squared lists in the rest of the paper.

§.§ Folding

Another common behaviour which can be defined over directly are the fold functions, right or left, which walk through the structure while combining their content using a given operator and a given seed. While we described the whole thought process behind the map function, we will, from now on, only give the property that is spreadable and the associated definitions. Both folds are spreadable and can thus be transported from  to . Both folds share the same abstract type:

Then, assuming we can fold over the type parameter, we can propagate this fold to in two ways, left or right. Below is the left propagation, while the right one is also present in the library:

As an example of left fold on an inner , we define the left fold on tuples:

This leads to the definition of folds for our . Here are the left folds for bushes and nests, with the respective seeds the fold on tuples, and itself.

Here is an example of left folding a nest of strings:

And an example of left folding a bush of strings:

§.§ Summary

This section exhibited three spreadable elements, that can be built freely for  when they exist on , these are the two folds, left and right, and the map function. These elements can be regrouped inside a record which contains all spreadable properties, which we call , and which will be enriched with logical properties in the next section. From these elements, it is possible to build additionnal functions directly, such as  (the number of elements contained in a specific structure) and , returning a list of these elements. This has been done in the library but is not shown here.

§ LOGICAL COMMON BEHAVIOURS

Until now, we considered functions on which provide a concrete value from such types, without any type dependence to values of any kind. In other words, most of what has been shown earlier could have equally been developed in a classical functional programming language with polymorphic types. Yet, we work with dependent types, which enlarges the boundaries of what can be expressed around our . This section shows examples of what we call logical properties, which means any definition about whose type is dependent. They include primitive predicates over , predicates around the computational aspects of alongside decidability properties.

§.§ Primitive predicates for

§.§.§ Predicate transformers

Our first idea is to express the satisfaction of a predicate by all elements, or at least one element inside our . In other words, we want to define, given a predicate , the usual predicates  and  over any .

The first step in that direction is to define the type of predicate transformer, transforming a predicate over a certain type  to a predicate over , where  is a certain . The definition is as follows, where  is the type for unary predicates ():

This specification now defined, we need to find inhabitants for them on our , the semantics of which should be respectively  and . Both have been defined and can be found in the library, however, we only show  in details here. Since a is defined using a certain as a parameter, this needs to be associated with a predicate transformer itself, so that our can provide its extended version. In other words, we look from an inhabitant of  provided we have an inhabitant of . This is built as an inductive , similarly as the usual definition of  over lists, for instance.

There are two cases, either the first element of the structure satisfies , or one of the elements of the tail of the structure satisfies  nested with , which is the predicate transformer associated with the underlying . In order to give examples, we define the predicate transformer  over tuples, so that it can be propagated to nests and lists.

This definition uses  which represents in the logical union and consists of two cases: either the tuple contains a single element, in which case  itself is returned, or it contains more that one, in which case either the first element satisfies , or one of the others satisfies it recursively. From this, we define  for nests and bushes, relying on  on tuples and itself respectively.

Here is an example of  over bushes, with the proof that the number $10$ is a member of a bush. It can be found somewhere in the third bush, following the chain of  and  from .

§.§.§ Decidability transformers

Since we are able to propagate a predicate transformer, we would like to tackle the propagation of the decidability of predicates. To do so, we express what it means for a predicate transformer to preserve decidability.

From this definition, we can prove that our predicate transformers  and  over do preserve decidability on the condition that the underlying predicate transformer does so. Proofs are omitted, although here is the signature relative to :

More concretely, this means that in our library, the decidability of a predicate  can be propagated to the decidability of  and  for all our . In other words, we are able to decide if at least one, or all elements of a do satisfy , even for bushes.

§.§ Predicates over computational aspects

A second logical family over revolves around the satisfaction of predicates for the functions we have defined. This is a wide area that consists in giving specification for our functions and proving that they
do satisfy their specification. Although our functions are low-level and not composite, which makes the specification process all the harder, we have several such examples in our library, despite only one being presented here, the congruence of a mapping. In other words, we present the proof that mapping with a function  is the same as mapping with a function  on any provided these function coincide on every input (aka are extensionally equal). We start by defining this abstract property.

We provide the proof that our preserve the congruence of a mapping. It means that, if

is congruent over a  then  is congruent over . The proof is done inductively, and is shown here as an example of such a proof in , although hardly understandable for non users, admittedly.

§.§ Summary

This section provided examples of logical properties expressed around our . We showed that we can build predicates over that stand for the membership modulo a predicate, named , and the satisfaction of a predicate for all members of a , named . We showed that these were decidable provided the unary predicate over their elements is decidable. We also showed an example of specification for one of our computational behaviour:  mapping with a given function, which stays congruent. All these elements were built with the same underlying idea  used throughout this paper: the propagation of properties from  to  where  is a . Next section summarizes all our definitions in a single picture.

§ PICTURING THE SPREADABLE ELEMENTS OF

Overview of the library

Our spreadable properties, most of which have been mentioned throughout this paper, are regrouped into four categories, each corresponding to a concrete data structure in , modelled as a record:

*  contains the two folds, left and right, with three additionnal functions, ,  and  which, respectively, counts the number of elements in our structure, flattens the structure into a list, and produces a string representation of the structure.

*  contains a map function, with two related properties, the congruence and the composition associated with it

*  contains the proof of decidability of equality between .

*  contains two predicate extensions over , the “at least one element”, and the “all elements” satisfying a given underlying predicate, alongside their decidability and additional derived constructs: the membership in a , its decidability, and the emptiness of a .

All these elements are regrouped into a  record which contains all spreadable elements of the library, and thus is characterized by .

§ DISCUSSION

This last section brings together a set of observations and open questions that remain to be discussed and that we would like to underline. Most of these elements have been mentioned throughout the paper and need additional explanation. They are displayed in no particular order.

and  Our development was presented in , but is also available in , as mentioned earlier. Having these two implementations of our ideas was fruitful in terms of providing users with our contribution, as well as in noticing differences between the tools. The main one lies in the definition of  which is accepted by and refused by , regardless of the use of to define it () or not (). This means that is, in that regard, more restrictive than in the sense that it refuses any definition from which subsequent functions would be troublesome in terms of termination proofs. accepts these definitions –  directly,  when termination checking is disabled – although subsequent definitions do indeed induce termination proofs issues in both cases. The good thing about being able to define  is that we can work with them by forcing the termination checker to trust us, although this leads to an unsafe development. Working in this manner is of course discouraged when dealing with safety issues, but it can prove to be interesting to handle this hard-to-grasp type. In our work, all functions that work on  do so in such a way that they are recursively defined using themselves, with a base case hard to picture, although they produce relevant results. This would be interesting to see how and if could be extended to accept similar definitions, to what extend, and at which cost.

The issue of termination As mentioned earlier,  is troublesome in terms of termination, which is unsurprising considering the nature of this datatype. In that regard, languages in which bushes can be used do not usually embed a termination checker and instead rely on trusting the developers ; and when they do like in , it needs to be turned off for the time being. An open question is to what extend such a termination could be proven. Considering the definition of  provided in Section <ref>, , it is highly unlikely that any termination checker would ever accept this definition, and that any of the usual termination techniques (exhibiting a well-founded order, using sized types, etc.) would allow to extend it in a way that they do. To tackle this issue, it is possible to give an alternate, more verbose definition of  using an indexation of the number of times  is encapsulated. This definition is accepted by but also by , as shown by the following snippet:
Inductive BushN : nat -> Type -> Type :=
| Base (a : Set) : a -> BushN O a
| NilBN (a : Set) (n : nat) : BushN (S n) a
| ConsBN (a : Set) (n : nat) :
BushN n a -> BushN (S (S n)) a -> BushN (S n) a.

This was tested in our library, but it remains unclear to which extend this solves the termination issue while providing the same expressiveness. Furthermore, such a definition does not comply with our overall pattern captured by the notion of . Overall, the termination issue over  remains open.

Automated term generation comes with an automated term generator, named , which, when called, attempts to build a term in a certain context with respect to a certain goal. works fine with , except for  where termination issues appear in the process of term generation. More precisely, while functions on , although we are not able to prove it, do terminate, automated term generation over  does not.  As far as we could observe, this behaviour might come from 's heuristic to explore possible terms with the maximum number of elements, rather than the opposite. This would however be interesting to investigate deeper why this happens, and if this would be relevant to implement different heuristics inside and similar automated theorem provers, to fix this issue.

Extending with more spreadable elements provides a representation of several using our notion of , all of them consisting in a collection of elements structured in a head-tail manner. Each of the original types that we model as instances of comes in the literature with a set of candidate functions for abstraction over . Most of the usual functions coming from , for instance, have been considered as possible functions to define for as a whole. Currently, consists of several , on which 16 functions (either computational, logical or additionnal) can be derived automatically from the underlying to the corresponding . Possibly, many more functions could be added to this set, although a lot of them have been considered and ultimately proved impossible to abstract. An example of such a case is the idea of defining  using  which seems both appealing, because it would reduce the minimal bricks of our , and promising, since  can indeed be written using  when considering . However, in practice, this is impossible due to type requirements. Indeed, the intuitive way of building  using , which works for lists, is the following:

map f = foldr (λ a l → f a ∷ l) []

This does not transpose into any because,  is of type  although  expects an element of type , where  is of type . Since  is the identity for , it works, but it is a special case and can only be generalized for any  such as . The common ancestor of both  and , when considering , is the induction principle derived from the definition, and one cannot be written using the other. As a side note, this induction principle is successfully generated by , and can be written in .

Another example of failed attempt at abstraction is the  function, which cannot be extended to because the structures need to be similar to be zipped together, and for instance any two bushes have little chance to be similar enough. We are confident, however, that more functions could be abstracted, especially in the logical area. For instance, we were interested in specifying contracts on our computation functions and were wondering if we could for instance prove, using our notion of membership and our notion of mapping that, given a  and an element  such that  is a member of , the fact that  is a member of . This should hold, however, it proved to be hard both to express and to prove. We are confident that this can be proven in our library; however, this requires a strict discipline on how to reliably find invariants in recursive function over , when the signature of the function contains elements that are not concerned by this recursivity. This remains an open question and will most likely be the subject of future work.

Extending with additional  Since, by nature, the work presented in this article only applies to a specific subset of nested , there are some other nested which are not handled in our work. An example are the well-known Finger Trees [10] which require an additional constructor to be defined – although some tricks using  and  could be considered. This observation leads to interesting questions as to how our work could be extended to nested that do not directly satisfy the structure we propose in . Such questions have been tackled over regular in different ways, which would be interesting to consider when relying on our work to use nested . These possibilities are as follows:

* A first possibility is to rely on even higher abstractions, which means studying nested as an abstract notion rather than a concrete family of inductive types. This is possible and has been done in other works such as [1]. However, this suffers from the usual drawback of high level abstraction: they are very far from concrete preoccupations and thus can hardly be used to obtain free code for their instances. In our case, the structure depicted in is essential to any of the concrete elements we have, which enforces a strong confidence in the level of abstraction we chose.

* A second possibility is to resort to meta-programming, which exists in with frameworks such as “Coq à la carte” [6] or more recently “MetaCoq” [15] and which is currently under development in . Such a meta-programming would allow us to define new at runtime, but it is not yet clear to us if this would allow us to reuse some of our result with little effort, if any.

* A third promising possibility would be to use ornaments [17, 5]. Ornaments are a way to build a hierarchy between from which functions can be derived with a certain degree of automation. Using ornaments would possibly allow to handle many more nested .

§ CONCLUSION

Assessments In this paper, we have defined a restricted class of nested with a similar structure, the . All different instances of are built using a different parameter called a . We studied these types over two axes: first, we studied a family of types that can successfully be seen as a , and second, we built a set of functions, whether computation or logical, which can be derived automatically from the underlying to the corresponding . Throughout this investigation, we developed a library regrouping these elements, called . This library was developed both in and in . The main difference between the two implementations is that allowed us to define the type , on which all our functions can be applied. is a small library, which contains the most fundamental notions to working with , and which will be extended with new elements in the future.

Limitations In that regard, our work has several limitations, most of which have already been discussed in Section <ref>, and can be summarized as follows. Our work is focused on a specific subset of nested , which is thus less generic than other higher level approaches, although it provides a bigger operational part. Our library could be used to model even more , and could be extended with additional spreadable properties. Moreover, our library does allow the user access to the  type when using , but this use is unsafe by nature, since termination issues are yet to be tackled. Finally, our approach provides a generic framework over , although we do not provide a way to export the notions it contains to other kinds of nested .

Perspectives These limitations bring perspectives to our work. We would like to extend to cover a wider ground in terms of possible instances of , as well as in terms of possible spreadable properties. We would also like to extend to handle more kinds of . This could be done using meta-programming or ornaments. We would also like to investigate some termination issues, based on  but not limited to. Indeed, our work contributes to raising the question of proofs of termination regarding recursive function when the defined function is passed as parameter inside its body to another function. Finally, we would like to investigate to which extend proof assistants should accept the type  and similar types, and the cost of such an acceptance.

[1]
authorIan Bayley (year2001):
titleGeneric Operations on Nested Datatypes.
Ph.D. thesis, schoolUniversity of Oxford.

[2]
authorYves Bertot &
authorPierre Castéran
(year2004): titleInteractive theorem proving and
program development. Coq'Art: The Calculus of inductive constructions.

[3]
authorRichard Bird &
authorLambert Meertens
(year1998): titleNested datatypes.
In editorJohan Jeuring, editor:
booktitleMathematics of Program Construction,
publisherSpringer Berlin Heidelberg, addressBerlin,
Heidelberg, pp. pages52–67, 10.1007/BFb0054285.

[4]
authorRichard Bird &
authorRoss Paterson
(year1999): titleGeneralised Folds for Nested
journalFormal Aspects of Computing
volume11(number2), p. pages200–222,

[5]
authorPierre-Evariste Dagand &
authorConor McBride
(year2014): titleTransporting functions across
journalJournal of Functional Programming
volume24(number2-3), p. pages316–383,

[6]
authorBenjamin Delaware,
authorBruno C. d. S. Oliveira &
authorTom Schrijvers
(year2013): titleMeta-Theory à La Carte.
In: booktitleProceedings of the 40th Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
seriesPOPL '13, publisherAssociation for Computing
Machinery, addressNew York, NY, USA, p.
pages207–218, 10.1145/2429069.2429094.

[7]
authorPeng Fu & authorPeter
Selinger: titleDependently Typed
Folds for Nested Data Types.

[8]
authorRalf Hinze (year1998):
titleNumerical Representations as Higher-Order Nested
typeTechnical Report.

[9]
authorRalf Hinze (year1999):
titleEfficient Generalized Folds.
typeTechnical Report.

[10]
authorRalf Hinze & authorRoss
Paterson (year2006):
titleFinger trees: a simple general-purpose data
journalJournal of Functional Programming
volume16(number2), p. pages197–217,

[11]
authorJosé Pedro Magalhães,
authorAtze Dijkstra,
authorJohan Jeuring &
authorAndres Löh
(year2010): titleA Generic Deriving Mechanism
for Haskell.
In: booktitleProceedings of the Third ACM Haskell
Symposium on Haskell, seriesHaskell '10,
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, p. pages37–48,

[12]
authorClare Martin,
authorJeremy Gibbons &
authorIan Bayley (year2004):
titleDisciplined, efficient, generalised folds for nested
journalFormal Asp. Comput. volume16,
pp. pages19–35, 10.1007/s00165-003-0013-6.

[13]
authorUlf Norell (year2009):
titleDependently Typed Programming in Agda.
pp. pages1–2, 10.1007/978-3-642-04652-0_5.

[14]
authorChris Okasaki
(year1998): titlePurely Functional Data
publisherCambridge University Press,

[15]
authorMatthieu Sozeau,
authorAbhishek Anand,
authorSimon Boulier,
authorCyril Cohen,
authorYannick Forster,
authorFabian Kunze,
authorGregory Malecha,
authorNicolas Tabareau &
authorThéo Winterhalter
(year2020): titleThe MetaCoq Project.
journalJ. Autom. Reason.
volume64(number5), pp. pages947–999,

[16]
authorPhilip Wadler
(year1989): titleTheorems for Free!
In: booktitleProceedings of the Fourth International
Conference on Functional Programming Languages and Computer Architecture,
seriesFPCA '89, publisherAssociation for Computing
Machinery, addressNew York, NY, USA, p.
pages347–359, 10.1145/99370.99404.

[17]
authorThomas Williams,
authorPierre-Évariste Dagand &
authorDidier Rémy
(year2014): titleOrnaments in Practice.
In: booktitleProceedings of the 10th ACM SIGPLAN
Workshop on Generic Programming, seriesWGP '14,
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, p. pages15–24,

[18]
authorYuming Zou &
authorPaul E. Black
(year2019): titleperfect binary tree.