EPJ Web of Conferences Lattice2017  11institutetext: Institute for Theoretical
Physics, University of Regensburg, 93040 Regensburg, Germany 22institutetext:
Faculty of Mathematics and Physics, University of Ljubljana, 1000 Ljubljana,
Slovenia 33institutetext: Jozef Stefan Institute, 1000 Ljubljana, Slovenia
44institutetext: Helmholtz-Institut Mainz, 55099 Mainz, Germany
55institutetext: Johannes Gutenberg Universität Mainz, 55099 Mainz, Germany

# Charmonium resonances on the lattice

Gunnar Bali 11 Sara Collins 11 Daniel Mohler 4455 M. Padmanath 11 Stefano
Piemonte Speaker, 11<EMAIL_ADDRESS>Sasa Prelovsek
112233 Simon WeishÃupl Speaker, 11<EMAIL_ADDRESS>
###### Abstract

The nature of resonances and excited states near decay thresholds is encoded
in scattering amplitudes, which can be extracted from single-particle and
multiparticle correlators in finite volumes. Lattice calculations have only
recently reached the precision required for a reliable study of such
correlators. The distillation method represents a significant improvement
insofar as it simplifies quark contractions and allows one to easily extend
the operator basis used to construct interpolators. We present preliminary
results on charmonium bound states and resonances on the $N_{f}=2+1$ CLS
ensembles. The long term goal of our investigation is to understand the
properties of the X resonances that do not fit into conventional models of
quark-antiquark mesons. We tune various parameters of the distillation method
and the charm quark mass. As a first result, we present the masses of the
ground and excited states in the $0^{++}$ and $1^{--}$ channels.

##  1 Introduction

The mysterious properties of exotic QCD resonances have motivated an
increasing interest in non-perturbative lattice calculations during the last
decade. Monte-Carlo simulations of QCD regularized on the lattice can provide
an alternative insight into the fundamental mechanisms of strong interactions,
but the study of resonances is a challenge that requires a huge numerical and
theoretical effort. In particular, scattering of particles cannot be
investigated directly on an Euclidean space-time lattice, but, following the
Lüscher method Luscher , scattering amplitudes are instead extracted from the
finite volume dependence of the discrete energy levels of the spectrum of two
interacting particles in a box. Many simulations with either different volumes
or in different moving frames are needed and a large number of configurations
is required to measure the lattice energy levels with a sufficient precision
to compute scattering observables. Only recently lattice QCD calculations have
been able to reach sufficiently small lattice spacings and pion masses to
allow for a reliable study of QCD resonances with heavy flavor content.

The aim of our project is the understanding of the nature of charmonium(-like)
resonances and excited states near decay thresholds by means of non-
perturbative lattice simulations. In this contribution we present our recent
progress, regarding the calculation of the energy levels on the $N_{f}=2+1$
ensembles generated by the CLS collaboration. We employ the distillation
method, which significantly improves the computation of all diagrams involving
single-meson and two-meson correlation functions. In Section 2 we present the
current experimental status, the results of previous lattice investigations
and the motivations for our project. In Section 3 we describe the details of
our ensembles and the tuning of the charm quark mass, while in Section 4 we
give an overview of the distillation method and the parameters used in our
analysis. Our results are presented in Section 5 and are followed by the
conclusions in Section 6.

##  2 Experimental status and previous lattice investigations

Our final goal is to consider conventional and exotic charmonium(-like)
resonances. Here we focus on the vector and scalar channels. The resonances
are labeled “XY” states, the letter $Y(\dots)$ is used to denote the states
with quantum numbers $1^{--}$, while the letter $X(\dots)$ is used for all
other flavorless charmonium exotic resonances.

The two lightest states of the charmonium spectrum in the vector channel, the
$J/\psi$ and $\psi(2S)$, are relatively stable and decay by charm-quark
annihilation or weak interactions. The third state, the $\psi(3770)$, is a
resonance which decays by strong interactions, lying above the $\bar{D}D$
decay threshold. The decay modes of the $\psi(3770)$ are in agreement with
those of an excitation of a quark-antiquark meson. At higher energies, there
are many other states whose structure and constituents are unknown, like the
$Y(4260)$, where BESIII recently found two peaks $Y(4240)$ and $Y(4320)$
Ablikim:2016qzw . The higher peak is consistent with $Y(4360)$ reported
earlier. Our first step toward the study of these exotic states is to
investigate the resonance $\psi(3770)$, whose properties are well-known
experimentally and that can be used as a benchmark to estimate carefully the
systematic uncertainties of our computation of the phase shift.

The $\chi_{c0}$ is the lightest bound state in the charmonium spectrum with
quantum numbers $0^{++}$. The higher lying $X(3915)$ was discovered by Belle
in 2004 in $J/\psi\,\omega$ decays X3915  and was subsequently listed as the
first excited state $\chi_{c0}(2P)$ by the Particle Data Group PDGOld . This
identification was based on a determination of its quantum numbers by BaBar
Lees:2012xs , and has since been challenged. The OZI rule favors an excited
$\bar{c}c$ state decaying into $D\bar{D}$ mesons, but not via $J/\psi\,\omega$
X3915r1  and, at present, there is still no evidence for a resonance at 3915
MeV in the s-wave $D\bar{D}$ meson scattering channel. Considering “exotic”
interpretations of the state, a $\bar{c}c$-gluon exotic hybrid scenario has
been excluded by lattice calculations as such states appear to be
significantly heavier than all other low energy resonances Liu . The
suppression of $D\bar{D}$ meson decays could instead be explained easily if
the $X(3915)$ has a hidden strange content. A possible structure could be in
this case a bound state of two $D_{s}$ mesons, and the 20 MeV gap of $X(3915)$
from the $\bar{D}_{s}D_{s}$ decay threshold would be interpreted as the
binding energy of the meson molecule. The decays into $J/\psi\,\omega$ could
be explained in terms of the $\omega-\phi$ mixing X3915r4 . Even in this case
it is still difficult to explain why the $X(3915)$ has not yet been seen in
the $\eta\eta_{c}$ decay channel, given the larger mixing in pseudoscalar
light-strange sector with respect to the vector case X3915r3 . An appealing
hypothesis is that the $X(3915)$ is a $cs\bar{c}\bar{s}$ tetraquark, i.e. a
bound state with four valence quarks without a definite internal structure.

Another solution of this puzzle has been suggested in Zhou:2015uva , where the
authors argue that BaBar made an unjustified assumption in their analysis,
which results in the exclusion of $J^{PC}=2^{++}$ as the quantum numbers for
the $X(3915)$. Indeed the authors argue that the $X(3915)$ is simply the
already known $\chi_{c2}(2P)$ PDG . If the $X(3915)$ is not the first excited
state of the $\chi_{c0}$, there is the question of what the energy of such a
state could be. The Belle collaboration has recently reported a new scalar
charmoniumlike state $X^{\ast}(3860)$ that decays into $D\bar{D}$ mesons as
expected for the excited state of the $\chi_{c0}$ Chilikin:2017evr .

The lack of a deep knowledge of the scalar and vector exotic charmonium
resonances is a strong motivation for non-perturbative lattice calculations of
the scattering matrix. Previous investigations performed by some of us have
been able to extract the elastic scattering phase shift from a basis including
both quark-antiquark and $D\bar{D}$ interpolators in the scalar channel
Lang:2015sba . However, the study of the resonance structure did not resolve
the issue of the first excited scalar charmonium. These exploratory results,
which did not consider strange quarks in the valence or the sea sector, gave
an indication for a bound state $\chi_{c0}$ and a rather narrow resonance
slightly below $4\leavevmode\nobreak\ $GeV. More simulations are required to
reach a conclusive picture of the scalar resonances, particularly to address
the experimental $X^{\ast}(3860)$ and $X(3915)$ states. We plan to extend the
previous analysis by considering also a coupling to a hidden strange sector.
This will entail coupled scattering of $\bar{D}D$ and $\bar{D}_{s}D_{s}$
channels.

##  3 Lattice Setup

Figure 1: Dependency of the D-meson mass $m_{D}$ on the bare charm quark mass
$m$ for different $\kappa_{c}$ \- values. The two red points indicate the
previously tuned values of $\kappa_{c}$. The blue line indicates a linear fit
to determine the new value $\kappa_{c}=0.125220$ corresponding to a D-meson
with a mass 80 MeV lighter than its physical value.

We perform our analysis on the $N_{f}=2+1$ ensembles generated by the CLS
collaboration, see, for example, Refs. Bruno:2014jqa  and Bali:2016umi  for
details. Two ensembles have been so far considered, labeled as U101 and H105,
both with $m_{\pi}=280$ MeV and lattice spacing $a=0.0854$ fm, but with
different lattice volumes of $24^{3}\times 128$ and $32^{3}\times 96$,
respectively. Our lattice discretization of the QCD action includes non-
perturbatively $\mathcal{O}(a)$-improved Wilson fermions with tree-level
Symanzik improved gauge action. Open boundary conditions have been applied to
the fermion and gluon fields in the time direction, while they are periodic in
space.

The strange and the light quarks are dynamical and their masses are fixed in
the Monte-Carlo simulation, however, we have the freedom to choose the mass of
the (quenched) charm quark. The hopping parameter $k_{c}$, where the bare
quark mass $am_{c}=(1-8k_{c})/(2k_{c})$, is usually fixed so that the
experimental value of the spin average of the $J/\psi$ and the $\eta_{c}$
meson masses is reproduced. For the current project, for which we employ
ensembles with unphysical pion masses, this may result in the $\psi(3770)$
lying below the $D\bar{D}$ threshold, so that the s-wave decay into $D\bar{D}$
mesons would be forbidden. This scenario might be avoided by reducing the
charm quark mass. We therefore use two different $k_{c}$ interpolating between
a $D$ meson mass approximatively 80 MeV above and below its physical value to
try estimate how the energy levels move with respect to the threshold as a
function of the charm quark mass, see Fig. 1.

##  4 Distillation method and variational analysis

To study the charmonium spectrum, we use the distillation method (quark-field
smearing) Peardon:2009gh  and the variational analysis of the correlation
matrix between single and multi-particle operators at different timeslices.
The wave function is constructed from the eigenvectors of the 3D Laplace
operator $\nabla^{2}_{t}$ defined on a given timeslice $t$. A fermion wave
function defined on a single lattice point can be smeared by the
“distillation” operator

$\Box(t)=\sum_{i=0}^{N}\Psi_{i}(t)\Psi_{i}^{\dagger}(t)\,,$ (1)

where the sum runs over the eigenvectors $\Psi_{i}(t)$ of $\nabla^{2}_{t}$
corresponding to the $N$ lowest eigenvalues. The resulting wave function has a
GauÃian bell shape, whose width is controlled by the number of eigenvectors
included in the sum, typically of the order of $O(100)$. If $N$ is taken as
large as $3\times V_{3}$, to span the entire linear space, then the
distillation operator reduces to the identity operator and no smearing is
applied at all.

(a) Connected and disconnected pseudoscalar correlators

(b) Effective mass of the first excited state of the $\eta_{c}$

Figure 2:  2(a) Trace of the contribution to the pseudoscalar correlator for
strange and light quarks (related to $\eta$ and $\eta^{\prime}$ mesons). The
disconnected contributions $D_{ff}$ for the dynamical flavors $f$ are smaller
in magnitude but have a larger statistical uncertainty than the connected
contributions $C_{ff}$. 2(b) Effective mass plots for the first excited
charmonium state ($0^{-+}$) using 30, 60 and 90 Laplacian eigenvectors.

In the distillation method, a generic two-point correlation function can be
rewritten as a product of a combination of at least four matrices

$C(t,t_{0})=\textrm{Tr}\left[\phi^{B}(t)\tau(t,t_{0})\phi^{A}(t_{0})\tau(t_{0},t)\right]\,.$
(2)

The perambulators $\tau$, describing the fermion propagation between
eigenvectors at possibly different timeslices

$\tau(t,t_{0},i,j)_{\alpha\beta}=\Psi_{i}^{\dagger}(t)D^{-1}_{\alpha\beta}\Psi_{j}(t_{0})\,,$
(3)

are precomputed for the charm, the light and the strange quarks. The total
number of inversions required is $4\times N$. Afterwards, the perambulators
are combined with the $\phi^{\prime}s$

$\phi^{A}(t,i,j)_{\alpha\beta}=\Psi_{i}^{\dagger}(t)\Gamma^{A}(t)_{\alpha\beta}\Psi_{j}(t)\,,$
(4)

that carry all information about source/sink operators and quantum numbers.
Finally, the matrices $\phi$ and $\tau$ are multiplied and traced accordingly
to Eq. 2 to construct single-meson correlators and the more involved
expressions are required for multi-meson correlators. We always include
diagrams with disconnected or backtracking strange and light loops, neglecting
such contributions only for the charm. The disconnected contributions for the
light quarks are a typical source of large statistical fluctuations in the
correlation functions, see Fig. 2(a).

The first step of the distillation method is to choose the number of
eigenvectors $N$. The optimal width of the wave function for charmonium states
is expected to be smaller than that of light mesons. One therefore needs a
larger number of eigenvectors compared to similar analyses of light
resonances. Our strategy for searching for the optimal value of $N$ is to look
for the point where an increase of $N$ does not result to a reduction in the
error of the first excited state of the $\eta_{c}$, see Fig. 2(b). The number
of eigenvectors $N$ has been set to 90 for the U101 ensemble and to 150 for
the H105.

Table 1: Interpolating operators for the $1^{--}$ (left) and the $0^{++}$
(right) channel. All repeated indexes are summed over the spatial components
and derivatives are implemented in a symmetric form.

$T^{--}_{1}\ $ ($J^{PC}=1^{--},3^{--},4^{--},\dots$)
---
Label | Operator
0 | $\bar{q}\ \gamma_{i}\ q$
1 | $\bar{q}\ \gamma_{i}\gamma_{t}\ q$
2 | $\bar{q}\ \overrightarrow{\nabla}_{i}\ q$
3 | $\bar{q}\ \epsilon_{ijk}\gamma_{j}\gamma_{5}\overrightarrow{\nabla}_{k}\ q$
4 | $\bar{q}\ \overleftarrow{\nabla}_{k}\gamma_{i}\overrightarrow{\nabla}_{k}\ q$
5 | $\bar{q}\ \overleftarrow{\nabla}_{k}\gamma_{i}\gamma_{t}\overrightarrow{\nabla}_{k}\ q$
6 | $\bar{q}\ \overleftarrow{\Delta}\gamma_{i}\overrightarrow{\Delta}\ q$
7 | $\bar{q}\ \overleftarrow{\Delta}\gamma_{i}\gamma_{t}\overrightarrow{\Delta}\ q$
8 | $\bar{q}\ \overleftarrow{\Delta}\overrightarrow{\nabla}_{i}\ q$
9 | $\bar{q}\ \overleftarrow{\Delta}\epsilon_{ijk}\gamma_{j}\gamma_{5}\overrightarrow{\nabla}_{k}\ q$
10 | $\bar{q}\ |\epsilon_{ijk}|\gamma_{j}\overrightarrow{D}_{k}\ q$
11 | $\bar{q}\ |\epsilon_{ijk}|\gamma_{j}\gamma_{t}\overrightarrow{D}_{k}\ q$
12 | $O^{\bar{D}(-1)D(1)}\sim\bar{c}\gamma_{5}l\leavevmode\nobreak\ \bar{l}\gamma_{5}c$
13 | $O^{\bar{D}(-1)D(1)}\sim\bar{c}\gamma_{5}\gamma_{t}l\leavevmode\nobreak\ \bar{l}\gamma_{5}\gamma_{t}c$

$A^{++}_{1}\ $ ($J^{PC}=0^{++},4^{++},\dots$)
---
Label n | Operator
0 | $\bar{q}\ q$
1 | $\bar{q}\ \gamma_{i}\overrightarrow{\nabla}_{i}\ q$
2 | $\bar{q}\ \gamma_{i}\gamma_{t}\overrightarrow{\nabla}_{i}\ q$
3 | $\bar{q}\ \overleftarrow{\nabla}_{i}\overrightarrow{\nabla}_{i}\ q$
4 | $\bar{q}\ \overleftarrow{\Delta}\overrightarrow{\Delta}\ q$
5 | $\bar{q}\ \overleftarrow{\Delta}\gamma_{i}\overrightarrow{\nabla}_{i}\ q$
6 | $\bar{q}\ \overleftarrow{\Delta}\gamma_{i}\gamma_{t}\overrightarrow{\nabla}_{i}\ q$
7 | $O^{\bar{D}(0)D(0)}\sim\bar{c}\gamma_{5}l\leavevmode\nobreak\ \bar{l}\gamma_{5}c$
8 | $O^{\bar{D}(0)D(0)}\sim\bar{c}\gamma_{5}\gamma_{t}l\leavevmode\nobreak\ \bar{l}\gamma_{5}\gamma_{t}c$
9 | $O^{\bar{D}(p)D(-p)}\sim\bar{c}\gamma_{5}l\leavevmode\nobreak\ \bar{l}\gamma_{5}c$
10 | $O^{\bar{D}^{\ast}(0)D^{\ast}(0)}\sim\bar{c}\gamma_{i}l\leavevmode\nobreak\ \bar{l}\gamma_{i}c$
11 | $O^{\bar{D}^{\ast}(0)D^{\ast}(0)}\sim\bar{c}\gamma_{i}\gamma_{t}l\leavevmode\nobreak\ \bar{l}\gamma_{i}\gamma_{t}c$
12 | $O^{J/\psi(0)\omega(0)}\sim\bar{c}\gamma_{i}c\leavevmode\nobreak\ \bar{l}\gamma_{i}l$
13 | $O^{J/\psi(0)\omega(0)}\sim\bar{c}\gamma_{i}\gamma_{t}c\leavevmode\nobreak\ \bar{l}\gamma_{i}\gamma_{t}l$
14 | $O^{\bar{D}_{s}(0)D_{s}(0)}\sim\bar{c}\gamma_{5}s\leavevmode\nobreak\ \bar{s}\gamma_{5}c$
15 | $O^{\bar{D}_{s}(0)D_{s}(0)}\sim\bar{c}\gamma_{5}\gamma_{t}s\leavevmode\nobreak\ \bar{s}\gamma_{5}\gamma_{t}c$

Once the Laplacian eigenvectors are available, operators and perambulators can
be computed in parallel. So far we have implemented rest frame operators, see
the list in Tab. 1. Operators relevant for moving frames are being developed
sasa_proceeding  and will be employed in the near future. The energy levels
are finally computed from the solution of the generalized eigenvalue problem
of the correlation matrix

$C_{ij}(t)=\langle\mathcal{O}_{i}(t)\mathcal{O}_{j}^{\dagger}(0)\rangle\,,$
(5)

as the result of the fit to an exponential decay of the eigenvalues

$\lambda_{m}(t,t_{0})\propto
e^{-(t-t_{0})E_{m}}(1+\mathcal{O}(e^{-(t-t_{0})\Delta E_{m}}))$ (6)

from

$C(t)v_{m}(t,t_{0})=\lambda_{m}(t,t_{0})C(t_{0})v_{m}(t,t_{0})\,.$ (7)

We fix $t_{0}=2$ and we optimize the choice of the basis of operators by
looking at the normalized correlation matrix

$M_{ij}(t)=\frac{C_{ij}(t)}{\sqrt{C_{ii}(t)C_{jj}(t)}}\,.$ (8)

The structure of the matrix $M$ can help identify how the operators are
correlated and how different states can be effectively separated from each
others by a suitable choice of the operator basis. From Fig. 3, in the vector
channel we do not see strong correlations between two- and single-particle
operators, while a signal for stronger correlations appears in the scalar
channel.

(a) Vector channel (b) Scalar channel

Figure 3: Matrix plots of the normalized correlation matrix $M_{ij}(t)$ in Eq.
(8) at timeslice $t=5a$ for all operators in the $1^{--}$ (left) and the
$0^{++}$ (right) channels from table 1.

Translational invariance in the time direction is broken on gauge-field
configurations with open boundary conditions. Correlators must be computed
with source positions at least 28 timeslices away from the boundaries, a value
chosen by looking for boundary effects in the pion correlator. In addition, we
average on each configuration the correlators for eight different timesources,
well separated in order to reduce the autocorrelation. Finally, two
consecutive analyzed configurations are separated by twenty molecular dynamics
units and ten accept/reject Metropolis steps.

##  5 Results

(a) $\kappa_{c}=0.125220$ (b) $\kappa_{c}=0.123147$

Figure 4: Effective masses of the 5 lowest states in the $1^{--}$ channel with
$\kappa_{c}=0.125220$ and $\kappa_{c}=0.123147$, extracted with the
variational analysis method from a basis of 10 operators
$\\{0,1,4,5,7,8,10,11,12,13\\}$. The results are obtained from 125
configurations of the U101 ensemble.

The analysis of the two ensembles is not yet completed, therefore at the
moment we can present only the effective energy levels of the ensemble U101
for total momentum zero. Our plans for the near future is to double the
statistics on the U101 ensembles and to perform all contractions including
operators in moving frames; (full) distillation is used in this case. An
analogous study is planned on ensemble H105 with larger volume, where the
perambulators are already computed with stochastic distillation
Morningstar:2011ka . The final analysis will also have to consider the impact
of the reweighting factors of the positive twisted mass introduced to
stabilize the HMC trajectory, which have not yet been included. Finally, the
finite volume energies will be computed, and the scattering amplitudes will be
suitably parameterized. The main challenge will be the understanding of how
the various decay channels are coupled together for the $0^{++}$ resonances.

Nevertheless, we can already discuss the structure of the discrete spectrum of
energy levels and the impact of tuning the charm quark mass. In the $1^{--}$
channel, we are able to reliably extract five energy levels in total, see Fig.
4. The entire charmonium spectrum shifts as expected if the charm quark mass
is decreased. The comparison of the two different $\kappa_{c}$ reveals that
$E_{3}-2m_{D}$ is bigger on $k_{c}=0.125220$ than on $k_{c}=0.123147$, where
$E_{3}$ is related to $\psi(3770)$. It is therefore more likely that
$\psi(3770)$ is a resonance above threshold in the former case. The
statistical significance is still not high enough to draw a complete
conclusion on this point, and the determination of the error is still
preliminary. It is however clear that the systematic uncertainty of the tuning
of the $\kappa_{c}$ does not dramatically affect the physical picture that we
aim to investigate, but that a clever choice of the charm quark mass can help
to move the $\psi(3770)$ toward a resonance state.

(a) $\kappa_{c}=0.125220$ excluding strange (b) $\kappa_{c}=0.125220$
including strange

Figure 5: Effective masses of the 4 lowest states in the $0^{++}$ channel with
$\kappa_{c}=0.125220$, extracted with the variational analysis method from an
operator basis excluding (left) and including (right) scattering in mesons
with strange valence quarks. The results are obtained from 125 configurations
of the U101 ensemble.

The energy levels in the $0^{++}$ channel are presented in Fig. 5. As
expected, the inclusion of hidden strange sector operators in our basis
results in an additional scattering energy level above the one given by
$\bar{D}D$ in s-wave at zero momentum. At the physical point, the two
thresholds of $\bar{D}_{s}D_{s}$ and $\bar{D}D$ meson scattering are well
separated by approximatively 200 MeV. In our setup, extrapolating along the
constant $2m_{l}+m_{s}$ line, the gap between the two corresponding scattering
levels is reduced to about 100 MeV. This effect is driven by the fact that we
are working with a heavier than physical light quark mass and an unphysically
light strange quark mass, therefore the resulting analysis of the scattering
amplitude will necessarily have to take into account the additional scattering
channels given by strange mesons.

##  6 Conclusions

We reported on the non-perturbative lattice determination of the properties of
the resonances in the charmonium spectrum. We studied the impact of the tuning
of the charm quark mass on the lattice energy levels, finding evidences that
modifying $\kappa_{c}$ might be crucial to move the position of the $\bar{D}D$
threshold below the second exited states in the vector channel. The
preliminary results of the energy spectrum show that our target statistics are
sufficient to reliably estimate the scattering states relevant for extracting
the scattering amplitudes. The calculations of the contractions on the
remaining configurations as well as the analysis itself is ongoing. The plan
for the near future is to provide an analysis of scalar and vector charmonium
resonances on the two ensembles U101 and H105, including scattering in moving
frames.

##  7 Acknowledgements

Our code that implements the distillation method is written within the
framework of the Chroma software package Edwards:2004 . The inversion of the
Dirac operator is performed used the multigrid solver of Ref. Heybrock:2014iga
; Heybrock:2015kpy ; Richtmann:2016kcq ; Georg:2017diz . The simulations were
performed on the Regensburg iDataCool cluster, and the SFB/TRR 55 QPACE 2
Arts:2015jia  and QPACE 3 machines. We thank our colleagues in CLS for the
joint effort in the generation of the gauge field ensembles which form a basis
for the here described computation. The Regensburg group was supported by the
Deutsche Forschungs- gemeinschaft Grant No. SFB/TRR 55. M. P. acknowledges
support from EU under grant no. MSCA-IF-EF-ST-744659 (XQCDBaryons).

## References

  * (1) M. Lüscher, Commun. Math. Phys. 105, 153 (1986); M. Lüscher, Nucl. Phys. B354, 531 (1991); M. Lüscher, Nucl. Phys. B364, 237 (1991).
  * (2) BesIII Collaboration, Phys. Rev. Lett. 118 (2017), 092001.
  * (3) Belle Collaboration, Phys. Rev. Lett. 94(2005), 182002; Babar Collaboration, Phys. Rev. Lett. 101 (2008) 082001; Belle Collaboration, Phys. Rev. Lett. 104(2010) 092001
  * (4) J. Beringer et al. (Particle Data Group), Phys. Rev. D86, 010001 (2012) and 2013 partial update for the 2014 edition.
  * (5) J. P. Lees et al. [BaBar Collaboration], Phys. Rev. D 86, 072002 (2012) doi:10.1103/PhysRevD.86.072002].
  * (6) Feng-Kun Guo, Ulf-G.MeiÃner, “Where is the $\chi_{c0}(2P)$?”, Phys. Rev. D 86 (2012), 091501; Stephen Lars Olsen, “Is the X(3915) the $\chi_{c0}(2P)$?”, Phys. Rev. D 91(2015), 057501
  * (7) L. Liu, G. Moir, M. Peardon, S. M. Ryan, C. E. Thomas, P. Vilaseca, J. J. Dudek, R. G. Edwards, B. JoÃ, D. G. Richards, “Excited and exotic charmonium spectroscopy from lattice QCD”, JHEP 07 (2012) 126.
  * (8) Zhi-Gang Wang, “Scalar tetraquark state candidates: X(3915), X(4500) and X(4700)”, Eur. Phys. J. C77 (2017) 78.
  * (9) Xin Li and M. B. Voloshin, “X(3915) as a $D_{s}\bar{D}_{s}$ bound state”, Phys. Rev. D 91, 114014 (2015).
  * (10) Z. Y. Zhou, Z. Xiao and H. Q. Zhou, Phys. Rev. Lett. 115, no. 2, 022001 (2015).
  * (11) C. Patrignani et al. âReview of Particle Physicsâ. In: Chin. Phys. C40.10 (2016).
  * (12) K. Chilikin et al. [Belle Collaboration], Phys. Rev. D 95, 112003 (2017).
  * (13) C. B. Lang, L. Leskovec, D. Mohler and S. Prelovsek, “Vector and scalar charmonium resonances with lattice QCD,” JHEP 1509 (2015) 089.
  * (14) M. Bruno et al., “Simulation of QCD with N${}_{f}=$ 2 $+$ 1 flavors of non-perturbatively improved Wilson fermions,” JHEP 1502 (2015) 043.
  * (15) G. S. Bali et al. [RQCD Collaboration], “Lattice simulations with $N_{f}=2+1$ improved Wilson fermions at a fixed strange quark mass,” Phys. Rev. D 94 (2016) no.7, 074501.
  * (16) M. Peardon et al. [Hadron Spectrum Collaboration], “A Novel quark-field creation operator construction for hadronic physics in lattice QCD,” Phys. Rev. D 80 (2009) 054506.
  * (17) S. Prelovsek, G. Bali, S. Collins, D. Mohler, M. Padmanath, S. Piemonte, and S. Weishaeupl, “Charmonia in moving frames”, in Proceedings, 35th International Symposium on Lattice Field Theory (Lattice2017): Granada, Spain, to appear in EPJ Web Conf.
  * (18) C. Morningstar, J. Bulava, J. Foley, K. J. Juge, D. Lenkner, M. Peardon and C. H. Wong, Phys. Rev. D 83, 114505 (2011).
  * (19) R.G. Edwards, B. Joo (SciDAC, LHPC, UKQCD), “The Chroma Software System for Lattice QCD”, Nucl. Phys. Proc. Suppl. 140, 832 (2005).
  * (20) S. Heybrock, B. JoÃ, D.D. Kalamkar, M. Smelyanskiy, K. Vaidyanathan, T. Wettig, P. Dubey, “Lattice QCD with Domain Decomposition on Intel Xeon Phi Co-Processors”, SC ’14: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis.
  * (21) S. Heybrock, M. Rottmann, P. Georg, T. Wettig, “Adaptive algebraic multigrid on SIMD architectures”, PoS LATTICE2015, 036 (2016).
  * (22) D. Richtmann, S. Heybrock, T. Wettig, “Multiple right-hand-side setup for the DD-$\alpha$AMG ”, PoS LATTICE2015, 035 (2016).
  * (23) P. Georg, D. Richtmann, T. Wettig, “pMR: A high-performance communication library”, PoS LATTICE2016, 361 (2017).
  * (24) P. Arts _et al._ , “QPACE 2 and Domain Decomposition on the Intel Xeon Phi”, PoS LATTICE2014, 021 (2015).


Institute for Computation and Information Sciences, Radboud University, The
Netherlands and https://www.cs.ru.nl/~cynthiakop<EMAIL_ADDRESS>https://orcid.org/0000-0002-6337-2544 Institute for Computation and
Information Sciences, Radboud University, The Netherlands and
https://www.cs.ru.nl/~deividvale<EMAIL_ADDRESS>https://orcid.org/0000-0003-1350-3478 The authors are supported by the NWO TOP
project “ICHOR”, NWO 612.001.803/7571 and the NWO VIDI project “CHORPE”, NWO
VI.Vidi.193.075. Cynthia Kop and Deivid Vale Theory of computation Equational
logic and rewriting

# Tuple Interpretations and Applications to Higher-Order Runtime Complexity

Cynthia Kop  Deivid Vale

###### Abstract

Tuple interpretations are a class of algebraic interpretation that subsumes
both polynomial and matrix interpretations as it does not impose simple
termination and allows non-linear interpretations. It was developed in the
context of higher-order rewriting to study derivational complexity of
algebraic functional systems. In this short paper, we continue our journey to
study the complexity of higher-order TRSs by tailoring tuple interpretations
to deal with innermost runtime complexity.

###### keywords:

Complexity analysis, higher-order term rewriting, tuple interpretations

##  1 Introduction

The step-by-step computational model induced by term rewriting naturally gives
rise to a complexity notion. Here, complexity is understood as the number of
rewriting steps needed to reach a normal form. In the rewriting setting, a
complexity function bounds the length of the longest rewrite sequence
parametrized by the size of the starting term. Two distinct complexity notions
are commonly considered: derivational and runtime. In the former, the starting
term is unrestricted which allows initial terms with nested function calls.
The latter only considers rewriting sequences beginning with basic terms.
Intuitively, basic terms are those where a single function call is performed
with data objects as arguments.

There are many techniques to bound the runtime complexity of term rewriting
[2, 4]. However, most of the literature focuses on the first-order case. We
take a different approach and regard higher-order term rewriting. We present a
technique that takes advantage of tuple interpretations [3] tailored to deal
with an innermost rewriting strategy. The defining characteristic of tuple
interpretations is to allow for a split of the complexity measure into
abstract notions of _cost_ and _size_. The former is usually interpreted as
natural numbers, which accounts for the number of steps needed to reduce terms
to normal forms. Meanwhile, the latter is interpreted as tuples over naturals
carrying abstract notions of size.

##  2 Preliminaries

### The Syntax of Terms and Rules

We assume familiarity with the basics of term rewriting. We will here recall
notation for _applicative simply-typed term rewriting systems_.

Let $\mathcal{B}$ be a set of base types (or sorts). The set
$\mathcal{T}_{\mathcal{B}}$ of _simple types_ is built using the right-
associative $\Rightarrow$ as follows. Every $\iota\in\mathcal{B}$ is a type of
order $0$. If $\sigma,\tau$ are types of order $n$ and $m$ respectively, then
$\sigma\Rightarrow\tau$ is a type of order $\max(n+1,m)$. A signature is a
non-empty set $\mathcal{F}$ of function symbols together with a function
$\mathtt{typeOf}:\mathcal{F}\longrightarrow\mathcal{T}_{\mathcal{B}}$.
Additionally, we assume, for each $\sigma\in\mathcal{T}_{\mathcal{B}}$, a
countable infinite set of type-annotated variables $\mathcal{X}_{\sigma}$
disjoint from $\mathcal{F}$. We will denote $\mathsf{f},\mathsf{g},\dots$ for
function symbols and $x,y,\dots$ for variables.

This typing scheme imposes a restriction on the formation of terms which
consists of those expressions $s$ such that $s::\sigma$ can be derived for
some type $\sigma$ using the following clauses: (i) $x::\sigma$, if
$x\in\mathcal{X}_{\sigma}$; (ii) $\mathsf{f}::\sigma$, if
$\mathtt{typeOf}(\mathsf{f})=\sigma$; and (iii) $(s\,t)::\tau$, if
$s::\sigma\Rightarrow\tau$ and $t::\tau$. Application is left-associative. We
denote $\mathtt{vars}(s)$ for the set of variables occurring in $s$ and say
$s$ is _ground_ if $\mathtt{vars}(s)=\emptyset$. A rewriting rule $\ell\to r$
is a pair of terms of the same type such that
$\ell=\mathsf{f}\,\ell_{1}\dots\ell_{m}$ and
$\mathtt{vars}(\ell)\supseteq\mathtt{vars}(r)$. An applicative simply-typed
term rewriting system (shortly denoted TRS), is a set $\mathcal{R}$ of rules.
The rewrite relation induced by $\mathcal{R}$ is the smallest monotonic
relation that contains $\mathcal{R}$ and is stable under application of
substitution. A term $s$ is in normal form if there is no $t$ such that $s\to
t$. The innermost rewrite relation induced by $\mathcal{R}$ is defined as
follows:

  * •

$\ell\gamma\to^{i}r\gamma$, if $\ell\to r\in\mathcal{R}$ and all proper
subterms of $\ell\gamma$ are in $\mathcal{R}$-normal form;

  * •

$s\,t\to^{i}s^{\prime}\,t$, if $s\to^{i}s^{\prime}$; and
$s\,t\to^{i}s\,t^{\prime}$, if $t\to^{i}t^{\prime}$.

In what follows we only allow for innermost reductions. So, we drop the i from
the arrow, and $s\to t$ is to be read as $s\to^{i}t$. We shall use the
explicit notation if confusion may arise.

######  Example 2.1.

We will use a system over the sorts ${\rm Nature}$ (numbers) and
$\mathsf{list}$ (lists of numbers). Let $\mathsf{0}::{\rm Nature}$,
$\mathsf{s}::{\rm Nature}\Rightarrow{\rm Nature}$,
$\mathsf{nil}::\mathsf{list}$, $\mathsf{cons}::{\rm
Nature}\Rightarrow\mathsf{list}\Rightarrow\mathsf{list}$, and
$F,G\in\mathcal{X}_{{\rm Nature}\Rightarrow{\rm Nature}}$; types of other
function symbols and variables can be easily deduced.

$\begin{array}[]{rclcrcl}\mathtt{map}\,F\,\mathsf{nil}&\to&\mathsf{nil}&&\mathtt{comp}\,F\,G\,x&\to&F\,(G\,x)\\\
\mathtt{map}\,F\,(\mathsf{cons}\,x\,xs)&\to&\mathsf{cons}\,(F\,x)\,(\mathtt{map}\,F\,xs)&&\mathtt{app}\,F\,x&\to&F\,x\\\
\mathtt{d}\,\mathsf{0}&\to&\mathsf{0}&&\mathtt{add}\,x\,\mathsf{0}&\to&x\\\
\mathtt{d}\,(\mathsf{s}\,x)&\to&\mathsf{s}\,(\mathsf{s}\,(\mathtt{d}\,x))&&\mathtt{add}\,x\,(\mathsf{s}\,y)&\to&\mathsf{s}\,(\mathtt{add}\,x\,y)\\\
\end{array}$

### Functions and orderings

A quasi-ordered set $(A,\sqsupseteq)$ consists of a nonempty set $A$ and a
quasi-order $\sqsupseteq$ over $A$. A well-founded set $(A,>,\geq)$ is a
nonempty set $A$ together with a well-founded order $>$ and a compatible
quasi-order $\geq$ on $A$, i.e., $>{\circ}\geq{\subseteq}>$. For quasi-ordered
sets $A$ and $B$, we say that a function $f:A\longrightarrow B$ is weakly
monotonic if for all $x,y\in A$, $x\sqsupseteq_{A}y$ implies
$f(x)\sqsupseteq_{B}f(y)$. If $(B,>,\geq)$ is a well-founded set, then $>$ and
$\geq$ induce a point-wise comparison on $A\longrightarrow B$ as usual. If
$A,B$ are quasi-ordered, the notation $A\Longrightarrow B$ refers to the set
of all weakly monotonic functions from $A$ to $B$. Functional equality is
extensional. The unit set is the quasi-ordered set defined by
$\mathtt{unit}=(\\{\mathtt{u}\\},\sqsupseteq)$, where
$\mathtt{u}\sqsupseteq\mathtt{u}$.

##  3 Higher-Order Tuple Interpretations for Innermost Rewriting

To define interpretations, we will start by providing an interpretation of
_types_ (Def. 3.1). Types $\sigma$ are interpreted by tuples
$\llparenthesis\sigma\rrparenthesis$ that carry information about cost and
size. We will first show how application works in this newly defined cost-size
domain (Def. 3.3). Interpretation of types will then set the domain for the
tuple algebras we are interested in (Def. 3.6).

######  Definition 3.1 (Interpretation of Types).

For each type $\sigma$, we define the cost-size tuple interpretation of
$\sigma$ as
$\llparenthesis\sigma\rrparenthesis=\mathcal{C}_{\sigma}\times\mathcal{S}_{\sigma}$
where $\mathcal{C}_{\sigma}$ (respectively $\mathcal{S}_{\sigma}$) is defined
as follows:

$\displaystyle\mathcal{C}_{\sigma}$
$\displaystyle=\mathbb{N}\times\mathcal{F}^{\mathsf{c}}_{\sigma}$
$\displaystyle\mathcal{S}_{\iota}$
$\displaystyle=(\mathbb{N}^{K[\iota]},\sqsupseteq),\;K[\iota]\geq 1$
$\displaystyle\mathcal{F}^{\mathsf{c}}_{\iota}$ $\displaystyle=\mathtt{unit}$
$\displaystyle\mathcal{S}_{\sigma\Rightarrow\tau}$
$\displaystyle=\mathcal{S}_{\sigma}\Longrightarrow\mathcal{S}_{\tau}$
$\displaystyle\mathcal{F}^{\mathsf{c}}_{\sigma\Rightarrow\tau}$
$\displaystyle=(\mathcal{F}^{\mathsf{c}}_{\sigma}\times\mathcal{S}_{\sigma})\Longrightarrow\mathcal{C}_{\tau},$

where $\mathcal{F}^{\mathsf{c}}_{\sigma\Rightarrow\tau}$
($\mathcal{S}_{\sigma\Rightarrow\tau}$) is the set of weakly monotonic
functions from $\mathcal{F}^{\mathsf{c}}_{\sigma}\times\mathcal{S}_{\sigma}$
to $\mathcal{C}_{\tau}$ ($\mathcal{S}_{\sigma}$ to $\mathcal{S}_{\tau}$). The
quasi-ordering on those sets is the induced point-wise comparison. The set
$\llparenthesis\sigma\rrparenthesis$ is ordered as follows:
$((n,f),s)\succ((m,g),t)$ if $n>m$, $f\geq g$ and $s\sqsupseteq t$; and
$((n,f),s)\succcurlyeq((m,g),t)$ if $n\geq m$, $f\geq g$ and $s\sqsupseteq t$.

The cost tuple
$\mathcal{C}_{\sigma}=\mathbb{N}\times\mathcal{F}^{\mathsf{c}}_{\sigma}$ of
$\llparenthesis\sigma\rrparenthesis$ holds the cost information of reducing a
term of type $\sigma$ to its normal form. It is composed of a numeric and
functional component. Base types, which are naturally not functional, have the
unit set for $\mathcal{F}^{\mathsf{c}}_{\iota}$; the cost tuple of a base type
is then $\mathcal{C}_{\iota}=\mathbb{N}\times\mathtt{unit}$. Functional types
do possess an intrinsically functional component (the cost of _applying_ the
function), which in our setting is expressed by
$\mathcal{F}^{\mathsf{c}}_{\sigma\Rightarrow\tau}=\mathcal{F}^{\mathsf{c}}_{\sigma}\times\mathcal{S}_{\sigma}\Longrightarrow\mathcal{C}_{\tau}$.
For functional types the numeric component represents the cost of partial
application.

To determine the number $K[\iota]$, associated to each sort $\iota$, we use a
semantic approach that takes the intuitive meaning of the sort we are
interpreting into account. The sort ${\rm Nature}$ for instance represents
natural numbers, which we implement in unary format. Hence, it makes sense to
reckon the number of successor symbols occurring in terms of the form
$(\mathsf{s}^{n}\,\mathsf{0})::{\rm Nature}$ as their size. This gives us
$K[{\rm Nature}]=1$. Another example is the sort $\mathsf{list}$ (of natural
numbers): it is natural to regard measures like length and maximum element
size. This results in $K[\mathsf{list}]=2$. Example 3.7 below shows how to
interpret data constructors using this intuition.

The next lemma expresses the soundness of our approach, that is, cost-size
tuples define a well-founded domain for the interpretation of types.

######  Lemma 3.2.

For each type $\sigma$, the set $\mathcal{C}_{\sigma}$ is well-founded and
$\mathcal{S}_{\sigma}$ quasi-ordered. Their product, that is,
$(\llparenthesis\sigma\rrparenthesis,\succ,\succcurlyeq)$, is well-founded.

### Semantic Application

To interpret each term $s::\sigma$ to an element of
$\llparenthesis\sigma\rrparenthesis$ (Def. 3.6), we will need a notion of
application for cost-size tuples. Specifically, given a functional type
$\sigma\Rightarrow\tau$, a cost-size tuple
$\bm{f}\in\llparenthesis\sigma\Rightarrow\tau\rrparenthesis$, and
$\bm{x}\in\llparenthesis\sigma\rrparenthesis$, our goal is to define the
application $\bm{f}\cdot\bm{x}$ of $\bm{f}$ to $\bm{x}$. Let us illustrate the
idea with a concrete example: consider the type $\sigma=({\rm
Nature}\Rightarrow{\rm
Nature})\Rightarrow\mathsf{list}\Rightarrow\mathsf{list}$, which is the type
of $\mathtt{map}$ defined in Example 2.1. The function $\mathtt{map}$ takes as
argument a function $F$ of type ${\rm Nature}\Rightarrow{\rm Nature}$ and a
list $q$, and applies $F$ to each element of $q$. The cost interpretation of
$\mathtt{map}$ is a functional in $\mathcal{C}_{\sigma}$ parametrized by
functional arguments carrying the cost and size information of $F$ and a cost-
size tuple for $q$.

$\mathbb{N}\times\overbrace{(\underbrace{(\mathtt{unit}\times\mathbb{N}\Longrightarrow\mathbb{N}\times\mathtt{unit})}_{\text{cost
of }F}\times\underbrace{(\mathbb{N}\Longrightarrow\mathbb{N})}_{\text{size of
}F}\Longrightarrow(\mathbb{N}\times(\underbrace{\mathtt{unit}}_{\text{cost of
}q}\times\underbrace{\mathbb{N}^{2}}_{\text{size of
}q}\Longrightarrow\mathbb{N}\times\mathtt{unit})))}^{\text{the functional cost
of }\mathtt{map}},$

Hence, we write an element of such space as the tuple $(n,f^{\mathsf{c}})$.
Size sets are somewhat simpler with
$\underbrace{(\mathbb{N}\Longrightarrow\mathbb{N})}_{\text{size of
}F}\Longrightarrow\underbrace{\mathbb{N}^{2}}_{\text{size of
}q}\Longrightarrow\mathbb{N}^{2}$. Therefore, a functional cost-size tuple
$\bm{f}$ is represented by
$\bm{f}=\langle(n,f^{\mathsf{c}}),f^{\mathsf{s}}\rangle$. An argument to such
a cost-size tuple is then an element in the domain of $f^{\mathsf{c}}$ and
$f^{\mathsf{s}}$, respectively. Therefore, we apply $\bm{f}$ to a cost-size
tuple $\bm{x}$ of the form $\langle(m,g^{\mathsf{c}}),g^{\mathsf{s}}\rangle$
where $g^{\mathsf{c}}$ is the cost of computing $F$ and $g^{\mathsf{s}}$ is
the size of $F$. We proceed by applying the respective functions, so
$f^{\mathsf{c}}(g^{\mathsf{c}},g^{\mathsf{s}})=(k,h)$ belongs to
$\mathcal{C}_{\mathsf{list}}$, and add the numeric components together
obtaining:
$\bm{f}\cdot\bm{x}=\langle(n+m+k,f^{\mathsf{c}}(g^{\mathsf{c}},g^{\mathsf{s}})),f^{\mathsf{s}}(g^{\mathsf{s}})\rangle$.
Notice that this gives us a new cost-size tuple with cost component in
$\mathbb{N}\times(\mathcal{C}_{\mathsf{list}}\Longrightarrow\mathcal{C}_{\mathsf{list}})$
and size component in
$\mathcal{S}_{\mathsf{list}}\Longrightarrow\mathcal{S}_{\mathsf{list}}$.

######  Definition 3.3.

Let $\sigma\Rightarrow\tau$ be an arrow type,
$\bm{f}=\langle(n,f^{\mathsf{c}}),f^{\mathsf{s}}\rangle\in\llparenthesis\sigma\Rightarrow\tau\rrparenthesis$,
and
$\bm{x}=\langle(m,g^{\mathsf{c}}),g^{\mathsf{s}}\rangle\in\llparenthesis\sigma\rrparenthesis$.
The application of $\bm{f}$ to $\bm{x}$, denoted $\bm{f}\cdot\bm{x}$, is
defined by:

let $f^{\mathsf{c}}(g^{\mathsf{c}},g^{\mathsf{s}})=(k,h)$; then
$\langle(n,f^{\mathsf{c}}),f^{\mathsf{s}}\rangle\cdot\langle(m,g^{\mathsf{c}}),g^{\mathsf{s}}\rangle=\langle(n+m+k,h),f^{\mathsf{s}}(g^{\mathsf{s}})\rangle$

Semantic application is left-associative and respects a form of application
rule.

######  Lemma 3.4.

If $\bm{f}$ is in $\llparenthesis\sigma\Rightarrow\tau\rrparenthesis$ and
$\bm{x}$ is in $\llparenthesis\sigma\rrparenthesis$, then $\bm{f}\cdot\bm{x}$
belongs to $\llparenthesis\tau\rrparenthesis$.

######  Remark 3.5.

In order to ease notation, we project sets
$\pi_{1}:A\times\mathtt{unit}\longrightarrow A$ and
$\pi_{2}:\mathtt{unit}\times A\longrightarrow A$ and compose functions with
projections, so a function in $\mathtt{unit}\times A\Longrightarrow
B\times\mathtt{unit}$ is lifted to a function in $A\Longrightarrow B$. The
functional cost of $\mathtt{map}$ is then read as follows:

$\mathbb{N}\times\overbrace{(\underbrace{(\mathbb{N}\Longrightarrow\mathbb{N})}_{\text{cost
of }F}\times\underbrace{(\mathbb{N}\Longrightarrow\mathbb{N})}_{\text{size of
}F}\Longrightarrow(\mathbb{N}\times(\underbrace{\mathbb{N}^{2}}_{\text{size of
}q}\Longrightarrow\mathbb{N})))}^{\text{the functional cost of }\mathtt{map}}$

The $\mathbb{N}$ component of $C_{\sigma\Rightarrow\tau}$ is specific to
innermost rewriting (it does not occur in [3]). We need this to handle rules
of non-base type; for example, if $\mathtt{add}\,\mathsf{0}\to\mathtt{id}$,
then the cost tuple of $\mathtt{add}\ \mathsf{0}$ is
$(1,\lambda\\!\\!\\!\lambda x.0)$. However, since in _most_ cases the first
component is $0$, we will typically omit these zeroes and simply write for
instance $\lambda\\!\\!\\!\lambda Fq.f^{\mathsf{c}}(F,q)$ instead of
$(0,\lambda\\!\\!\\!\lambda F.\langle 0,\lambda\\!\\!\\!\lambda
q.f^{\mathsf{c}}(F,q)\rangle)$. To compute using Definition 3.3 we still use
the complete form.

Tuple algebras are higher-order weakly monotonic algebras [1] with cost-size
tuples as interpretation domain.

######  Definition 3.6 (Higher-order tuple algebra).

A higher-order tuple algebra over a signature
$(\mathcal{B},\mathcal{F},\mathtt{typeOf})$ consists of: (i) a family of
cost/size tuples
$\\{\llparenthesis\sigma\rrparenthesis\\}_{\sigma\in\mathcal{T}_{\mathcal{B}}}$
and (ii) an interpretation function $\mathcal{J}$ which maps each
$\mathsf{f}\in\mathcal{F}$ of type $\sigma$ to a cost-size tuple in
$\llparenthesis\sigma\rrparenthesis$.

######  Example 3.7.

Following the semantics discussed previously, we interpret the constructors
for both ${\rm Nature}$ and $\mathsf{list}$ as follows. We call the first
component of $\mathcal{S}_{\mathsf{list}}$ length and the second maximum
element size. Those are abbreviated using the letters $\mathsf{l}$ and
$\mathsf{m}$, respectively.

$\displaystyle\mathcal{J}_{\mathsf{0}}$ $\displaystyle=\langle 0,0\rangle$
$\displaystyle\mathcal{J}_{\mathsf{s}}$
$\displaystyle=\langle\lambda\\!\\!\\!\lambda x.0,\lambda\\!\\!\\!\lambda
x.x+1\rangle$ $\displaystyle\mathcal{J}_{\mathsf{nil}}$ $\displaystyle=\langle
0,\langle 0,0\rangle\rangle$ $\displaystyle\mathcal{J}_{\mathsf{cons}}$
$\displaystyle=\langle\lambda\\!\\!\\!\lambda xq.0,\lambda\\!\\!\\!\lambda
xq.\langle q_{\mathsf{l}}+1,\max(x,q_{\mathsf{m}})\rangle\rangle$

The cost-size tuples for $\mathsf{0}$ and $\mathsf{nil}$ are all $0$s, as
expected. The size components for $\mathsf{s}$ and $\mathsf{cons}$ describe
the increase in size when new data is created. We interpret functions from
Example 2.1 as follows:

$\begin{array}[]{rclrcl}\mathcal{J}_{\mathtt{app}}&=&\langle\lambda\\!\\!\\!\lambda
Fx.F^{\mathsf{c}}(x)+1,\lambda\\!\\!\\!\lambda Fx.F^{\mathsf{s}}(x)\rangle\\\
\mathcal{J}_{\mathtt{d}}&=&\langle\lambda\\!\\!\\!\lambda
x.x+1,\lambda\\!\\!\\!\lambda x.2x\rangle\\\
\mathcal{J}_{\mathtt{add}}&=&\langle\lambda\\!\\!\\!\lambda
xy.y+1,\lambda\\!\\!\\!\lambda xy.x+y\rangle\\\
\mathcal{J}_{\mathtt{comp}}&=&\langle\lambda\\!\\!\\!\lambda
FGx.F^{\mathsf{c}}(G^{\mathsf{s}}(x_{\mathsf{s}}))+1,\lambda\\!\\!\\!\lambda
FGx.F^{\mathsf{s}}(G^{\mathsf{s}}(x))\rangle\\\
\mathcal{J}_{\mathtt{map}}&=&\langle\lambda\\!\\!\\!\lambda
Fq.q_{\mathsf{l}}F^{\mathsf{c}}(q_{\mathsf{m}})+1,\lambda\\!\\!\\!\lambda
Fq.\langle
q_{\mathsf{l}},F^{\mathsf{s}}(q_{\mathsf{m}})\rangle\rangle\end{array}$

A valuation $\alpha$ is a function that maps each $x::\sigma$ to a cost-size
tuple in $\llparenthesis\sigma\rrparenthesis$. Due to innermost strategy, we
can assume the interpretation of every variable $x::\iota$ has zero cost. This
is formalized by assigning $\alpha(x)=\langle(0,\mathtt{u}),x^{s}\rangle$, for
all $x\in\mathcal{X}$ of base type. In this paper, we shall only consider
valuations that satisfy this property. Variables of functional type, however,
may carry cost information even though any instance of a redex needs to be
normalized. Hence, we set
$\alpha(F)=\langle(0,f^{\mathsf{c}}),f^{\mathsf{s}}\rangle$ when
$F::\sigma\Rightarrow\tau$.

######  Definition 3.8.

We extend $\mathcal{J}$ to an interpretation
$\llbracket\cdot\rrbracket_{\alpha,\mathcal{J}}$ of terms as follows:

$\displaystyle\llbracket x\rrbracket_{\alpha,\mathcal{J}}$
$\displaystyle=\alpha(x)$
$\displaystyle\llbracket\mathsf{f}\rrbracket_{\alpha,\mathcal{J}}$
$\displaystyle=\langle(n,\mathcal{J}_{\mathsf{f}}^{\mathsf{c}}),\mathcal{J}_{\mathsf{f}}^{\mathsf{s}}\rangle,n\in\mathbb{N}$
$\displaystyle\llbracket s\,t\rrbracket_{\alpha,\mathcal{J}}$
$\displaystyle=\llbracket s\rrbracket_{\alpha,\mathcal{J}}\cdot\llbracket
t\rrbracket_{\alpha,\mathcal{J}}$

We are interested in interpretations satisfying a compatibility requirement:

######  Theorem 3.9 (Innermost Compatibility Theorem).

Let $\alpha$ be a valuation. If
$\llbracket\ell\rrbracket_{\alpha,\mathcal{J}}\succ\llbracket
r\rrbracket_{\alpha,\mathcal{J}}$ for all rules $\ell\to r\in\mathcal{R}$,
then $\llbracket s\rrbracket_{\alpha,\mathcal{J}}\succ\llbracket
t\rrbracket_{\alpha,\mathcal{J}}$, whenever $s\to_{\mathcal{R}}^{i}t$.

One can check that the TRS from Example 2.1 interpreted as in Example 3.7
satisfy the compatibility requirement.

##  4 Higher-Order Innermost Runtime Complexity

In this section, we briefly limn how the cost-size tuple machinery allow us to
reason about innermost runtime complexity. We start by reviewing basic
definitions.

######  Definition 4.1.

A symbol $\mathsf{f}\in\mathcal{F}$ is a defined symbol if it occurs at the
head of a rule, i.e., there is a rule
$\mathsf{f}\,\ell_{1}\,\dots\,\ell_{k}\to r\in\mathcal{R}$. A symbol
$\mathsf{c}$ of order at most 1 is a data constructor if it is not a defined
symbol. A data term has the form $\mathsf{c}\,d_{1}\,\dots\,d_{k}$ with
$\mathsf{c}$ a constructor and each $d_{i}$ a data term. A term $s$ is basic
if $s::\iota$ and $s$ is of the form $\mathsf{f}\,d_{1}\,\dots\,d_{m}$ with
$\mathsf{f}$ a defined symbol and all $d_{1},\dots,d_{m}$ data terms. The set
$T_{\mathcal{B}}(\mathcal{F})$ collects all basic terms.

######  Remark 4.2.

Notice that our notion of data is intrinsically first-order. This is motivated
by applications of rewriting to full program analysis where even if higher-
order functions are used a program has type
$\iota_{1}\Rightarrow\dots\Rightarrow\iota_{m}\Rightarrow\kappa$. The sorts
$\iota_{i}$ are the input data types and $\kappa$ the output type of the
program.

######  Definition 4.3.

The innermost derivation height of $s$ is
$\mathtt{dh}_{\mathcal{R}}(s)=\\{n\mid\exists t:s\to^{n}t\\}$. The innermost
runtime complexity function with respect to a TRS $\mathcal{R}$ is
$\mathtt{irc}_{\mathcal{R}}(n)=\max\\{\mathtt{dh}_{\mathcal{R}}(s)\mid s\in
T_{\mathcal{B}}(\mathcal{F})\wedge|s|\leq n\\}$.

To reasonably bound the innermost runtime complexity of a TRS $\mathcal{R}$,
we require that size interpretations of constructors have their components
bounded by an additive polynomial, that is, a polynomial of the form
$\lambda\\!\\!\\!\lambda x_{1}\dots x_{k}.\sum_{i=1}^{k}x_{i}+a$, with
$a\in\mathbb{N}$.

We can build programs by adding a new $\mathtt{main}$ function taking data
variables as arguments and combine it with rules computing functions,
including higher-order ones. For instance, using rules from Example 2.1, we
can compute a program that adds a number $x$ to every element in a list $q$ as
follows: $\mathtt{main}\,x\,q\to\mathtt{map}\,(\mathtt{add}\,x)\,q$. Hence,
computing this program on inputs $\mathsf{n}$ and list $q$ is equivalent to
reducing the term $\mathtt{main}\,\mathsf{n}\,q$ to normal form. Its runtime
complexity is therefore bounded by the cost-tuple of
$\llbracket\mathtt{main}\,\mathsf{n}\,q\rrbracket$.

##  5 Conclusion

In this short paper, we shed light on how to use cost-size tuple
interpretations to bound innermost runtime complexity of higher-order systems.
We defined a new domain of interpretations that takes the intricacies of
innermost rewriting into account and defined how application works in this
setting. The compatibility result allows us to make use of interpretations as
a way to bound the length of derivation chains, as it is expected from an
interpretation method. As current, and future work, we are working on
automation techniques to find interpretations and develop a completely
rewriting-based automated tool for complexity analysis of functional programs.

## References

  * [1] C. Fuhs and C. Kop.  Polynomial interpretations for higher-order rewriting.  In Proc. RTA, 2012.  doi:10.4230/LIPIcs.RTA.2012.176.
  * [2] N. Hirokawa and G. Moser.  Automated complexity analysis based on the dependency pair method.  In Proc. IJCAR, 2008.  doi:10.1007/978-3-540-71070-7_32.
  * [3] C. Kop and D. Vale.  Tuple interpretations for higher-order complexity.  In Proc. FSCD, 2021.  doi:10.4230/LIPIcs.FSCD.2021.31.
  * [4] L. Noschinski, F. Emmes, and J. Giesel.  Analysing innermost runtime complexity of term rewriting by dependency pairs.  JAR, 2013.  doi:10.1007/s10817-013-9277-6.