# On different ways to quantize Soft-Collinear Effective Theory

Christian W. Bauer  Ernest Orlando Lawrence Berkeley National Laboratory,
University of California, Berkeley, CA 94720  Oscar Catà  Ernest Orlando
Lawrence Berkeley National Laboratory, University of California, Berkeley, CA
94720  Grigory Ovanesyan  Ernest Orlando Lawrence Berkeley National
Laboratory, University of California, Berkeley, CA 94720

###### Abstract

Collinear fields in soft collinear effective theory (SCET) can be made
invariant under collinear gauge transformations by multiplying them with
collinear Wilson lines. We discuss how we can quantize SCET directly in terms
of these gauge invariant fields, allowing to directly calculate $S$ matrix
elements using the gauge invariant collinear fields. We also show how for each
collinear direction SCET can be written in terms of fields whose interactions
are given by the usual QCD Lagrangian, and how external operators coupling
these different directions can be constructed.

Soft collinear effective theory (SCET) Bauer:2000ew ; Bauer:2000yr ;
Bauer:2001ct ; Bauer:2001yt  is by now a rather mature effective field theory
with wide applications in $B$ physics and collider physics. SCET describes QCD
in the kinematic regime where the energy of particles is far in excess of
their (invariant) mass. Short distance physics is contained in Wilson
coefficients which are determined order by order in perturbation theory. Long
distance physics on the other hand is described by separate collinear fields
for each light-like direction, together with Wilson lines $Y_{n}$ describing
the usoft physics interactions between the different collinear directions.
Since there are no direct interactions between collinear fields in different
directions, gauge invariance requires the presence of Wilson lines to render
collinear fermions and gauge bosons gauge invariant.

There are several equivalent versions of SCET used in the literature. The
original formulation of SCET Bauer:2000ew ; Bauer:2000yr  described the
interactions between the gauge dependent collinear quark $\xi_{n}$ and gluon
$A_{n}$ fields, with the leading order Lagrangian given by111We here omit any
reference to gauge-fixing and potential ghost terms. We will address the
quantization of gauge fields later on.

$\displaystyle{\cal{L}}_{I}^{n}(\xi_{n},A_{n})$ $\displaystyle=$
$\displaystyle{\bar{\xi}}_{n}\left[in\\!\cdot\\!D_{n}+iD\\!\\!\\!\\!/_{n}^{\perp}\frac{1}{i{{\bar{n}}}\\!\cdot\\!D_{n}}iD\\!\\!\\!\\!/_{n}^{\perp}\right]\frac{{\bar{n}}\\!\\!\\!/}{2}\xi_{n}$
(1) $\displaystyle-\frac{1}{2}{\mathrm{Tr}}\,F^{n}_{\mu\nu}F_{n}^{\mu\nu}\,,$

with the standard definition of the covariant derivative and the field
strength tensor

$iD_{n}^{\mu}=i\partial^{\mu}_{n}+g_{s}A_{n}^{\mu}\,,\qquad
F_{n}^{\mu\nu}=\frac{i}{g_{s}}[D_{n}^{\mu},D_{n}^{\nu}]\,,\\\ $ (2)

where the partial derivative $\partial_{n}$ is given in terms of the label
operator introduced in Bauer:2001ct

$i\partial_{n}^{\mu}={\bar{n}}\\!\cdot\\!{\cal P}\frac{n^{\mu}}{2}+{\cal
P}_{\perp}^{\mu}+in\\!\cdot\\!\partial\frac{{\bar{n}}^{\mu}}{2}\,.$ (3)

In order to construct gauge invariant operators containing collinear fermions,
these fermions are required to appear in the gauge invariant combination

$\chi_{n}=W_{n}^{\dagger}\xi_{n}\,,\\\ $ (4)

where $W_{n}$ is the collinear Wilson line Bauer:2001ct

$W_{n}={\rm P}\exp\left[-ig_{s}\\!\int_{0}^{\infty}\\!{\rm
d}s\,\,{\bar{n}}\\!\cdot\\!A_{n}({\bar{n}}s+x)\right]\,.$ (5)

Using a simple field redefinition, one can easily obtain the collinear
Lagrangian in terms of these gauge invariant combinations

$\displaystyle{\cal{L}}_{II}^{n}(\chi_{n},A_{n})$ $\displaystyle=$
$\displaystyle{\bar{\chi}}_{n}W^{\dagger}_{n}\left[in\\!\cdot\\!D_{n}+iD\\!\\!\\!\\!/_{n}^{\perp}\frac{1}{i{{\bar{n}}}\\!\cdot\\!D_{n}}iD\\!\\!\\!\\!/_{n}^{\perp}\right]\frac{{\bar{n}}\\!\\!\\!/}{2}W_{n}\chi_{n}$
(6) $\displaystyle-\frac{1}{2}{\mathrm{Tr}}\,F^{n}_{\mu\nu}F_{n}^{\mu\nu}\,.$

Since the fields $\chi_{n}$ are gauge invariant, the combination
$W_{n}^{\dagger}D_{n}^{\mu}W_{n}$ has to be gauge invariant as well. Thus, we
can define Arnesen

${\cal{D}}_{n}^{\mu}=W_{n}^{\dagger}D_{n}^{\mu}W_{n}\,.$ (7)

The gauge invariant derivative operator ${\cal{D}}_{n}^{\mu}$ can be written
in terms of the partial derivative and a gauge invariant gluon field
${\cal{B}}_{n}^{\mu}$

$i{\cal{D}}_{n}^{\mu}=i\partial_{n}^{\mu}+g_{s}{\cal{B}}_{n}^{\mu}\,,$ (8)

where

${\cal{B}}_{n}^{\mu}=\left[\frac{1}{{\bar{n}}\\!\cdot\\!\partial}\left[i{\bar{n}}\\!\cdot\\!{\cal
D}_{n},i{\cal
D}_{n}^{\mu}\right]\right]=\frac{1}{g_{s}}\left[W_{n}^{\dagger}iD_{n}^{\mu}W_{n}\right]\,,$
(9)

and the derivatives only act within the square brackets. In terms of these
fields, the Lagrangian reads

$\displaystyle{\cal{L}}_{III}^{n}(\chi_{n},{\cal B}_{n})$ $\displaystyle=$
$\displaystyle{\bar{\chi}}_{n}\left[in\\!\cdot\\!{\cal D}_{n}+i{\cal
D}\\!\\!\\!\\!/_{n}^{\perp}\frac{1}{i{\bar{n}\\!\cdot\\!\partial}}i{\cal
D}\\!\\!\\!\\!/_{n}^{\perp}\right]\frac{{\bar{n}}\\!\\!\\!/}{2}\chi_{n}$ (10)
$\displaystyle-\frac{1}{2}{\mathrm{Tr}}\,{\cal{F}}^{n}_{\mu\nu}{\cal{F}}_{n}^{\mu\nu}\,,$

where we have defined

${\cal
F}_{n}^{\mu\nu}=\frac{i}{g_{s}}[{\cal{D}}_{n}^{\mu},{\cal{D}}_{n}^{\nu}]\,.$
(11)

A sample of Feyman rules for the three different formulations of SCET is shown
in Fig. 1.

$\displaystyle V^{(1)}_{{\cal L}_{I}}$ $\displaystyle=$
$=igT^{A}\\!\left[n^{\mu}+\frac{\gamma^{\mu}_{\perp}p\\!\\!\\!/_{\perp}}{\bar{n}\cdot
p}+\frac{p\\!\\!\\!/^{\prime}_{\perp}\gamma^{\mu}_{\perp}}{\bar{n}\cdot
p^{\prime}}-\frac{p\\!\\!\\!/_{\perp}^{\prime}p\\!\\!\\!/_{\perp}}{\bar{n}\cdot
p^{\prime}\bar{n}\cdot p}\bar{n}^{\mu}\right]\\!\frac{{\bar{n}}\\!\\!\\!/}{2}$
$\displaystyle V^{(2)}_{{\cal L}_{I}}$ $\displaystyle=$
$=ig^{2}\\!\left[\frac{T^{A}T^{B}}{\bar{n}\cdot(p-q)}\gamma_{\perp}^{\mu}\gamma_{\perp}^{\nu}+\frac{T^{B}T^{A}}{\bar{n}\cdot(q+p^{\prime})}\gamma_{\perp}^{\nu}\gamma_{\perp}^{\mu}\right]\\!\frac{{\bar{n}}\\!\\!\\!/}{2}+(\ldots)$
$\displaystyle V^{(1)}_{{\cal L}_{II}}$ $\displaystyle=$ $=V^{(1)}_{{\cal
L}_{I}}+igT^{A}\\!\left[\frac{1}{\bar{n}\cdot(p-p^{\prime})}\left(\frac{p^{2}}{\bar{n}\cdot
p}-\frac{p^{\prime 2}}{\bar{n}\cdot
p^{\prime}}\right)\bar{n}^{\mu}\right]\\!\frac{{\bar{n}}\\!\\!\\!/}{2}$
$\displaystyle V^{(2)}_{{\cal L}_{II}}$ $\displaystyle=$ $=V^{(2)}_{{\cal
L}_{I}}+(\ldots)$ $\displaystyle V^{(1)}_{{\cal L}_{III}}$ $\displaystyle=$
$=igT^{A}\\!\left[n^{\mu}+\frac{\gamma^{\mu}_{\perp}p\\!\\!\\!/_{\perp}}{\bar{n}\cdot
p}+\frac{p\\!\\!\\!/^{\prime}_{\perp}\gamma^{\mu}_{\perp}}{\bar{n}\cdot
p^{\prime}}\right]\\!\frac{{\bar{n}}\\!\\!\\!/}{2}$ $\displaystyle
V^{(2)}_{{\cal L}_{III}}$ $\displaystyle=$
$=ig^{2}\\!\left[\frac{T^{A}T^{B}}{\bar{n}\cdot(p-q)}\gamma_{\perp}^{\mu}\gamma_{\perp}^{\nu}+\frac{T^{B}T^{A}}{\bar{n}\cdot(q+p^{\prime})}\gamma_{\perp}^{\nu}\gamma_{\perp}^{\mu}\right]\\!\frac{{\bar{n}}\\!\\!\\!/}{2}$
$\displaystyle\Delta_{{\cal L}_{III}}$ $\displaystyle=$
$=-i\frac{\delta^{AB}}{k^{2}+i\epsilon}\left(g_{\mu\nu}-\frac{{\bar{n}}_{\mu}k_{\nu}+{\bar{n}}_{\nu}k_{\mu}}{{\bar{n}}\cdot
k}\right)$ Figure 1: A subset of Feynman rules for the three different
formulations of SCET. The (…) denote terms which do not contribute to the
tadpole diagram of Fig. 2b) in Feynman gauge.

It is well known that the dynamics of SCET with a single collinear direction
is identical to full QCD. This is of course expected, since one can perform a
simple Lorentz boost along the direction $n$ to make all momentum components
of the collinear field similar in magnitude. Since this eliminates any large
ratio of scales, the interactions have to be those of full QCD. This implies
that for example the wave function renormalization in SCET is equivalent to
that of full QCD, as was first shown in Bauer:2000ew ; Bauer:2000yr . This
equivalence has been used in the literature in order to simplify perturbative
calculations in SCET (vid., for instance, Becher:2006qw ).

It is the purpose of this paper to study the relationship between different
formulations of SCET. We work out the relationship between SCET using gauge
dependent and gauge invariant degrees of freedom, as well as the relationship
between full QCD and collinear fields in a single direction further. One of
the features of the original formulation of SCET is that collinear gluons are
coupled to the quark fields in a non-linear way. This means that there are an
infinite number of vertices consisting of quark-antiquark and an arbitrary
number of collinear gluons, whose Feynman rules get increasingly complicated.
This makes the theory particularly unfriendly for computations beyond the one-
loop order.

We will show how to quantize SCET directly in terms of the gauge invariant
degrees of freedom, and write the theory as a path integral over these gauge
invariant fields. We will also discuss how to re-express the theory using only
the interactions of full QCD. This first gives a precise field theoretical
understanding of the well known property of SCET that the dynamics in a given
collinear direction are equivalent to that of full QCD. Our formulation using
directly the generating functional will extend this result to include
interactions between different collinear directions through local operators.
One can hope that these results will simplify the perturbative calculation of
matching coefficients in the future, since much of the SCET calculations are
now identical to the corresponding QCD results.

It will prove instructive, however, to first illustrate this equivalence
between different formulations of SCET using a simple one-loop calculation.
Consider the two point correlator of two gauge invariant fermion fields

$\langle 0|T\chi_{n}(x)\bar{\chi}_{n}(y)|0\rangle=\langle
0|TW^{\dagger}_{n}(x)\xi_{n}(x)\bar{\xi}_{n}(y)W_{n}(y)|0\rangle\,.$ (12)

The Fourier transform of this correlator is what is known in the literature as
the jet function, and plays a crucial role in any process containing external
collinear particles. In the original formulation of SCET in terms of $\xi_{n}$
and $A_{n}$ fields there are four diagrams contributing at one loop, which are
shown in Fig. 2. The first two diagrams are entirely built out of interactions
contained in the Lagrangian of the theory, while in the last two diagrams one
of the gluon couplings comes from the Wilson lines $W_{n}$ or
$W_{n}^{\dagger}$. Using the Feynman rules given in Fig. 1, one can easily
obtain the result

$\displaystyle
D_{I,a}=g_{s}^{2}\frac{n\mspace{-10.0mu}/\mspace{3.0mu}}{2}\frac{{\bar{n}}\\!\cdot\\!p}{p^{2}}C_{F}(2-D)\int\frac{d^{D}k}{(2\pi)^{D}}\left[\frac{1}{2}\frac{1}{(k^{2}+i\epsilon)((k+p)^{2}+i\epsilon)}-\frac{{\bar{n}}\\!\cdot\\!p}{p^{2}}\frac{1}{(k^{2}+i\epsilon){\bar{n}}\\!\cdot\\!(k+p)}\right]\,,$
(13) $\displaystyle
D_{I,b}=g_{s}^{2}\frac{n\mspace{-10.0mu}/\mspace{3.0mu}}{2}\left(\frac{{\bar{n}}\\!\cdot\\!p}{p^{2}}\right)^{2}C_{F}(2-D)\int\frac{d^{D}k}{(2\pi)^{D}}\frac{1}{(k^{2}+i\epsilon){\bar{n}}\\!\cdot\\!(k+p)}\,,$
(14) $\displaystyle
D_{I,c}=D_{I,d}=g_{s}^{2}\frac{n\mspace{-10.0mu}/\mspace{3.0mu}}{2}\frac{{\bar{n}}\\!\cdot\\!p}{p^{2}}C_{F}(n\\!\cdot\\!{\bar{n}})\int\frac{d^{D}k}{(2\pi)^{D}}\frac{{\bar{n}}\\!\cdot\\!(k+p)}{(k^{2}+i\epsilon)((k+p)^{2}+i\epsilon){\bar{n}}\\!\cdot\\!k}\,.$
(15)

Note that the tadpole diagram is canceled exactly against the second term in
the first diagram. Performing the remaining integrals and summing the diagrams
one obtains the well known result Manohar:2003vb

$\displaystyle
D_{I}=i\frac{\alpha_{s}C_{F}}{4\pi}\frac{n\mspace{-10.0mu}/\mspace{3.0mu}}{2}\frac{{\bar{n}}\\!\cdot\\!p}{p^{2}}\left(\frac{\mu^{2}}{-p^{2}}\right)^{\epsilon}\left[\frac{4}{\epsilon^{2}}+\frac{3}{\epsilon}+7-\frac{\pi^{2}}{3}\right]\,.$
(16)

Figure 2: Diagrams contributing to the gauge invariant jet function at one
loop.

We can repeat this calculation using the formulation of SCET in terms of
$\chi_{n}$ and $A_{n}$ fields. This removes the last two diagrams of Fig. 2,
since there are no Wilson lines in the definition of the correlator when
written in terms of $\chi_{n}$ fields. However, the extra Wilson lines in the
collinear Lagrangian change the Feynman rules in the way shown in Fig. 1.
While this does not change the result for the second diagram, the first
diagram is now

$\displaystyle D_{II,a}$ $\displaystyle=$ $\displaystyle
g_{s}^{2}\frac{n\mspace{-10.0mu}/\mspace{3.0mu}}{2}\frac{{\bar{n}}\\!\cdot\\!p}{p^{2}}C_{F}\int\frac{d^{D}k}{(2\pi)^{D}}\Bigg{[}(2-D)\left(\frac{1}{2}\frac{1}{(k^{2}+i\epsilon)((k+p)^{2}+i\epsilon)}-\frac{{\bar{n}}\\!\cdot\\!p}{p^{2}}\frac{1}{(k^{2}+i\epsilon){\bar{n}}\\!\cdot\\!(k+p)}\right)$
(17)
$\displaystyle+2n\\!\cdot\\!{\bar{n}}\frac{{\bar{n}}\\!\cdot\\!(k+p)}{(k^{2}+i\epsilon)((k+p)^{2}+i\epsilon){\bar{n}}\\!\cdot\\!k}-(n\\!\cdot\\!{\bar{n}})^{2}\frac{{\bar{n}}\\!\cdot\\!p}{p^{2}}\frac{1}{(k^{2}+i\epsilon){\bar{n}}\\!\cdot\\!k}\Bigg{]}\,.$

The first two terms reproduce the result for $D_{I,a}$, and the third
reproduces $D_{I,c}+D_{I,d}$. Finally, the fourth term in $D_{II,a}$ vanishes,
since it is odd as $k\to-k$. Thus, the sum of all diagrams is identical in
both versions of the theory.

Showing that we can reproduce this result using the fully gauge invariant
$\chi_{n}$ and ${\cal B}_{n}$ fields is a little more tricky. This is because
now there are no Wilson lines whatsoever, neither in the definition of the
correlator nor in the Lagrangian of Eq. (10). Thus, it is not immediately
obvious how the contributions from diagrams $D_{c}$ and $D_{d}$ are reproduced
in this case. However, care has to be taken when deriving the gluon
propagator. The ${\cal B}_{n}$ field is by construction explicitly invariant
under collinear gauge transformations, and the usual procedure of adding an
arbitrary gauge-fixing term to the Lagrangian is not valid. However, from the
definition of ${\cal B}_{n}^{\mu}$ in Eq. (9) one easily verifies the
constraint ${\bar{n}}\\!\cdot\\!{\cal B}_{n}=0$ (see Eqs. (29) and (30)
below). Thus, the propagator of a ${\cal B}_{n}$ field has to satisfy the
condition ${\bar{n}}_{\mu}\Delta_{\cal B}^{\mu\nu}=0$. As we will discuss in
more detail later, the propagator takes the form Bassetto:1984dq ;
Veliev:2001gp

$(\Delta_{{\cal
B}})_{\mu\nu}^{ab}(k)=\frac{-i\delta^{ab}}{k^{2}+i\epsilon}\left(g_{\mu\nu}-\frac{{\bar{n}}_{\mu}k_{\nu}+{\bar{n}}_{\nu}k_{\mu}}{{\bar{n}}\\!\cdot\\!k}\right)\,.$
(18)

Using this propagator for the gauge invariant gluon field one can easily
verify that

$D_{III,a}=D_{II,a}\,,\quad D_{III,b}=D_{II,b}\,.$ (19)

Thus, the three formulations of SCET give identical results to one another for
the two point correlator of two gauge invariant collinear fermion fields.

In order to generalize this discussion to any matrix element, we quantize the
theory directly in terms of the various fields. This is achieved by using the
path integral formulation, working directly with the generating functional of
the theory

$Z[J]=\int\\!{\cal{D}}{\bar{\xi}}_{n}{\cal{D}}\xi_{n}{\cal{D}}A_{n}^{\mu}\,{\mathrm{exp}}\left[i\int\\!d^{4}x\,{{\cal{S}}_{I}}(\xi_{n},A_{n}^{\mu},J_{n})\right]\,,$
(20)

where we have defined

$\displaystyle{\cal{S}}_{I}$ $\displaystyle=$
$\displaystyle\sum_{n}\big{[}{\cal{L}}^{n}_{I}+{\bar{J}}_{n}^{\xi}\xi_{n}+{\bar{\xi}}_{n}J_{n}^{\xi}+{\bar{J}}_{n}^{\chi}W^{\dagger}_{n}\xi_{n}+{\bar{\xi}}_{n}W_{n}J_{n}^{\chi}$
(21) $\displaystyle+J_{n\mu}^{A}A_{n}^{\mu}+J_{n\mu}^{\cal B}{\cal
B}_{n}^{\mu}(A_{n})$ $\displaystyle+\sum_{k}{J}_{k}{\cal
O}_{k}\left(W_{n}^{\dagger}\xi_{n},{\cal B}_{n}^{\mu}(A_{n})\right)\,.$

A few comments are in order to understand our notation. First, the integration
in Eq. (20) is over all fields with different directions $n$. Second, the
subscripts $I,II,III$ indicate which version of SCET we are using, with
Lagrangians given in Eqs. (1), (6) and (10) above. Third, we have added
separate currents for the gauge invariant fields
$\chi_{n}=W_{n}^{\dagger}\xi_{n}$ and ${\cal B}_{n}^{\mu}={\cal
B}_{n}^{\mu}(A_{n})=\frac{1}{g_{s}}[W_{n}^{\dagger}iD_{n}^{\mu}W_{n}]$, as
well as for the gauge dependent fields $\xi_{n}$ and $A_{n}$. This allows us
to calculate correlators with gauge invariant fields, such as the jet
function, as well as those with gauge dependent fields, as is often done in
matching calculations to QCD. Finally, we have indicated currents $J_{k}$ for
any local operator in SCET. Such operators are typically written in terms of
the gauge invariant fields, and an example would be the production current for
two collinear fields in opposite directions, ${\cal
O}_{2}=\bar{\chi}_{n}\Gamma\chi_{{\bar{n}}}$.

In order to obtain the generating functional with the Lagrangian written in
terms of $\chi_{n}$ fields, we make the field redefinition given in Eq. (4),
which just amounts to a change in the integration variable in the generating
functional. Since $W_{n}^{\dagger}W_{n}=1$, one can easily show that the
integration measure is the same when written in terms of the $\chi_{n}$ fields

${\cal D}\xi_{n}{\cal D}\bar{\xi}_{n}{\cal D}A_{n}^{\mu}={\cal D}\chi_{n}{\cal
D}\bar{\chi}_{n}{\cal D}A_{n}^{\mu}\,.$ (22)

Thus, the generating functional can be written as

$Z[J]=\int\\!{\cal{D}}{\bar{\chi}}_{n}{\cal{D}}\chi_{n}{\cal{D}}A_{n}^{\mu}\,{\mathrm{exp}}\left[i\\!\int\\!d^{4}x\,{\cal{S}}_{II}(\chi_{n},A_{n}^{\mu},J_{n})\right]\,,$
(23)

with

$\displaystyle{\cal{S}}_{II}$ $\displaystyle=$
$\displaystyle\sum_{n}\big{[}{\cal{L}}^{n}_{II}+{\bar{J}}_{n}^{\xi}W_{n}\chi_{n}+{\bar{\chi}}_{n}W_{n}^{\dagger}J_{n}^{\xi}+{\bar{J}}_{n}^{\chi}\chi_{n}+{\bar{\chi}}_{n}J_{n}^{\chi}$
(24) $\displaystyle+J_{n\mu}^{A}A_{n}^{\mu}+J_{n\mu}^{\cal B}{\cal
B}_{n}^{\mu}(A_{n})\big{]}$ $\displaystyle+\sum_{k}{J}_{k}{\cal
O}_{k}(\chi_{n},{\cal B}_{n}(A_{n}))\,.$

In other words, any matrix element written in terms of $\xi_{n}$ and $A_{n}$
fields is identical to the matrix element written in terms of $\chi_{n}$ and
$A_{n}$ fields, as long as the interactions between the fields are given by
the Lagrangian ${\cal L}_{II}$ instead of ${\cal L}_{I}$.

Next, we discuss the relation between the gauge dependent gluon field $A_{n}$
and the gauge invariant field ${\cal B}_{n}$. The Yang Mills action is given
by

$Z_{\rm YM}=\int\\!{\cal D}A_{n}^{\mu}\,e^{iS_{\rm YM}[A_{n}]}\,,$ (25)

where

$S_{\rm YM}[A]=-\frac{1}{2}\int\\!d^{4}x\,\sum_{n}{\rm
Tr}\,F^{n}_{\mu\nu}F_{n}^{\mu\nu}\,.$ (26)

Recall that the relation between these two fields is given by

${\cal{B}}_{n}^{\mu}=\frac{1}{g_{s}}\left[W_{n}^{\dagger}iD_{n}^{\mu}W_{n}\right]\,,$
(27)

where $\partial_{n}^{\mu}$ acts only within the square brakets. Since the
Wilson lines $W_{n}$ are unitary, the Yang-Mills action can be written in
terms of the ${\cal B}_{n}^{\mu}$ fields as

$S_{\rm YM}[{\cal B}]=-\frac{1}{2}\int\\!d^{4}x\,\sum_{n}{\rm Tr}\,{\cal
F}^{n}_{\mu\nu}{\cal F}_{n}^{\mu\nu}\,,$ (28)

where ${\cal F}_{n}^{\mu\nu}$ is given in Eq. (11). However, in order to write
the generating functional in terms of the fields ${\cal B}_{n}$ requires
changing the integration measure as well, and that is where additional care
has to be taken. From the definition of the ${\cal B}_{n}$ field we can
immediately see that

${\bar{n}}\\!\cdot\\!{\cal B}_{n}=0\,,$ (29)

which follows from the well known relation of Wilson lines

${\bar{n}}\\!\cdot\\!D_{n}\,W_{n}=W_{n}\,{\bar{n}}\\!\cdot\\!\partial_{n}\,.$
(30)

Thus, while there are four components of the $A_{n}^{\mu}$ field, there are
only three components for the ${\cal B}_{n}^{\mu}$ field, making the Jacobian
for the change in the integration measure singular.

Of course, the fact that the ${\cal B}_{n}^{\mu}$ field has less independent
components than the $A_{n}^{\mu}$ field is not unexpected, given that the
former is gauge independent, while the latter contains all the gauge
redundancy. The only way one can obtain a meaningful definition of a Jacobian
factor is by removing the gauge redundancy and thus considering only three of
the four components of the $A_{n}^{\mu}$ field. This can be achieved using the
usual Faddeev-Popov procedure, by inserting a representation of unity into the
path integral (25) in the following form

$1=\int\\!{\cal D}\alpha(x)\,\delta[G(A_{n}^{\alpha})]\,\det\left(\frac{\delta
G(A_{n}^{\alpha})}{\delta\alpha}\right)\,,$ (31)

where $G(A_{n}^{\alpha})$ is some gauge-fixing function linear in the gauge
field. Here $\alpha(x)$ defines a specific gauge transformation and
$A_{n}^{\alpha}$ denotes the (infinitesimally) gauge transformed field

$(A^{\mu}_{n})^{\alpha}=A^{\mu}_{n}+\frac{1}{g_{s}}D^{\mu}_{n}\alpha\,.$ (32)

Note that for infinitesimal gauge transformations (from which all finite
transformations can be constructed), the determinant of $\delta
G/\delta\alpha$ is in general a function of $(A^{\mu}_{n})^{\alpha}$ but
independent of $\alpha$.

Following the standard treatment, the gauge invariance of both the action and
the integration measure allows one to write

$Z_{\rm YM}=\int\\!{\cal D}\alpha\int\\!{\cal
D}A_{n}^{\mu}\,\delta[G(A_{n})]\,E_{G}[A_{n}]\,,$ (33)

where we have defined

$E_{G}[A_{n}]=\det\left(\frac{\delta
G(A_{n}^{\alpha})}{\delta\alpha}\right)\\!\\![A_{n}]\,e^{iS_{\rm
YM}[A_{n}]}\,.$ (34)

One should remember that the determinant ${\rm det}(\delta G/\delta\alpha)$ is
independent of $\alpha$ and therefore the integral over the gauge freedom is
just a global factor that can be safely ignored. The important feature of this
way of writing the path integral is that the integration measure ${\cal
D}A_{n}^{\mu}\,\delta[G(A_{n})]$ contains only three components of the
$A_{n}^{\mu}$ field, and can thus be related to the integration measure of the
${\cal B}_{n}^{\mu}$ field. This allows us to formally write

${\cal D}A_{n}^{\mu}\,\delta[G(A_{n})]=J_{G}[{\cal B}_{n}]\,{\cal D}{\cal
B}_{n}^{\mu}\,\delta[{\bar{n}}\\!\cdot\\!{\cal B}_{n}]\,,$ (35)

where the Jacobian factor for the change of the integration measure
$J_{G}[{\cal B}_{n}]$ depends on the choice of the gauge-fixing condition $G$.
Combining these results together we find

$Z_{\rm YM}=\int\\!{\cal D}{\cal
B}_{n}^{\mu}\,\,\delta[{\bar{n}}\\!\cdot\\!{\cal B}_{n}]\,J_{G}[{\cal
B}_{n}]\,E_{G}[A_{n}({\cal B}_{n})]\,.$ (36)

Everything in this generating functional is known, except for the explicit
form of the Jacobian $J_{G}[{\cal B}_{n}]$ and the determinant inside
$E_{G}[A_{n}({\cal B}_{n})]$. Due to the non-linear nature of Eq. (27), their
expressions for a general gauge-fixing condition $G$ are very difficult to
derive. However, from the Faddeev-Popov procedure it is obvious that the
generating functional is identical for all choices of the gauge-fixing
condition $G$, since it was introduced as an arbitrary function in Eq. (31).
Thus, any choice of $G(A_{n})$ will do, and the easiest choice is light-cone
gauge, which uses

$G(A_{n})\equiv G_{\rm LC}(A_{n})={\bar{n}}\\!\cdot\\!A_{n}\,.$ (37)

In this case, we have ${\bar{n}}\\!\cdot\\!A_{n}=0$, which immediately implies
$W_{n}=1$, making the relation between the $A_{n}^{\mu}$ and ${\cal
B}_{n}^{\mu}$ fields trivial:

${\cal B}_{n}^{\mu}=A_{n}^{\mu}\,.$ (38)

Thus, in this particular gauge we find

$J_{G_{\rm LC}}[{\cal B}_{n}]=1\,,\qquad E_{G_{\rm LC}}[{\cal
B}_{n}]={\mathrm{det}}({\bar{n}}\\!\cdot\\!\partial)\,e^{iS_{\rm YM}[{\cal
B}_{n}]}\,,$ (39)

and we obtain the final form of the generating fuctional in terms of ${\cal
B}^{\mu}_{n}$ fields as

$Z_{\rm YM}=\int\\!{\cal D}{\cal
B}_{n}^{\mu}\,\delta[{\bar{n}}\\!\cdot\\!{\cal
B}_{n}]\,{\mathrm{det}}({\bar{n}}\\!\cdot\\!\partial)\,e^{iS_{\rm YM}[{\cal
B}_{n}]}\,.$ (40)

In other words, the Yang-Mills action in terms of the gauge invariant gluon
field ${\cal B}_{n}^{\mu}$ is identical to the one in terms of the field
$A_{n}^{\mu}$ in the light-cone gauge. Therefore, all Feynman rules for the
${\cal{B}}_{n}^{\mu}$ fields are identical to Feynman rules for the
$A_{n}^{\mu}$ fields in the light-cone gauge. In particular, this justifies
Eq. (18) as the right form of the gluon propagator for the ${\cal
B}_{n}^{\mu}$ fields. Incidentally, notice also that the determinant in Eq.
(40) is independent of the gauge field and therefore can be ignored, meaning
that the formulation with ${\cal B}_{n}^{\mu}$ fields is ghost-free. This
obviously complies with the well known fact that the light-cone gauge is
unitary and ghost fields decouple (see, for instance, tHooft ).

Having worked out how one can quantize SCET directly in terms of the gauge
invariant degrees of freedom, we next ask whether it is possible to write the
generating functional of SCET in terms of fields, whose interactions are given
by the interactions of full QCD. As we will show, this is indeed possible if
we restrict ourselves to leading order in the power counting, but requires
separate fields for each different collinear direction. We will also show how
to construct external operators coupling these different fields to one
another, such that any leading order correlation function in SCET can be
reproduced using only fields whose coupling to other fields is described by
the Lagrangian of full QCD. We do want to emphasize that this by no means
implies that SCET as an effective theory is useless. The power of SCET comes
from understanding the interactions between fields in different directions,
and while we can reproduce any leading order operator using fields that
resemble full QCD, we can neither easily implement power corrections, nor can
we derive the form of the leading order operators without the construction of
SCET. However, we can use this equivalence to calculate matrix elements in
SCET using the familiar Feynman rules of QCD, which will in general simplify
the required calculations at higher orders in perturbation theory.

We start by making the Ansatz

$Z[J]=\int\\!{\cal{D}}{\bar{\psi_{n}}}{\cal{D}}\psi_{n}{\cal{D}}A_{n}^{\mu}{\mathrm{exp}}\left[i\int\\!d^{4}x\,S_{\rm
QCD}(\psi_{n},A_{n},J)\right],$ (41)

where $S_{\rm QCD}$ is defined by

$\displaystyle S_{\rm QCD}$ $\displaystyle\\!\\!=\\!\\!$
$\displaystyle\sum_{n}\big{[}{\cal{L}}^{\rm
QCD}_{n}+{\bar{J}}^{\xi}_{n}{\cal{M}}^{\xi}_{n}\psi_{n}+{\bar{\psi}}_{n}{\bar{{\cal{M}}}}^{\xi}_{n}J^{\xi}_{n}+{\bar{J}}^{\chi}_{n}{\cal{M}}^{\chi}_{n}\psi_{n}$
(42)
$\displaystyle+{\bar{\psi}}_{n}{\bar{{\cal{M}}}}^{\chi}_{n}J^{\chi}_{n}+J_{n\mu}^{A}A_{n}^{\mu}+J_{n\mu}^{\cal
B}{\cal B}_{n}^{\mu}(A_{n})\big{]}$
$\displaystyle+\sum_{k}J_{k}{\cal{Q}}_{k}(\psi_{n},A_{n})\,,$

with

${\cal L}_{n}^{\rm QCD}=\bar{\psi}_{n}\,iD\\!\\!\\!\\!/\,\psi_{n}\,.$ (43)

The set of operators ${\cal Q}_{k}$ couple $k$ fields in different directions
$n_{1},...,n_{k}$. Our goal is to find expressions for ${\cal M}_{n}$ and
${\cal Q}_{k}$, such that the generating functional in Eq. (41) is equivalent
to the generating functional of SCET.

Let’s begin by setting all currents in the action to zero, leaving only the
Lagrangian ${\cal L}_{n}^{\rm QCD}$. One can write

$\psi_{n}(x)=\left(P_{n}+P_{\bar{n}}\right)\psi_{n}(x)\,,$ (44)

with the projection operators $P_{n}$ and $P_{\bar{n}}$ defined by

$P_{n}=\frac{n\\!\\!\\!/{\bar{n}}\\!\\!\\!/}{4}\,,\qquad
P_{\bar{n}}=\frac{{\bar{n}}\\!\\!\\!/n\\!\\!\\!/}{4}\,,$ (45)

and define

$\xi_{n}\equiv P_{n}\psi_{n}\,,\qquad\phi_{n}\equiv P_{\bar{n}}\psi_{n}\,.$
(46)

This allows us to write

$\displaystyle Z[J=0]$ $\displaystyle=$
$\displaystyle\int{\cal{D}}{\bar{\xi}_{n}}{\cal{D}}\xi_{n}{\cal{D}}{\bar{\phi}_{n}}{\cal{D}}\phi_{n}{\cal{D}}A_{n}^{\mu}$
$\displaystyle\times{\mathrm{exp}}\left[\sum_{n}i\\!\int\\!d^{4}x\,(\bar{\xi}_{n}+\bar{\phi}_{n})iD\\!\\!\\!\\!/\,(\xi_{n}+\phi_{n})\right]\,.$

Using the well-known formula for Gaussian integration,

$\displaystyle\int\\!{\cal{D}}\phi{\cal{D}}{\bar{\phi}}\,\,{\mathrm{exp}}\left[i\int\\!d^{4}x({\bar{\phi}}M\phi+{\bar{J}}\phi+{\bar{\phi}}J)\right]$
$\displaystyle\qquad={\mathrm{det}}(-iM)\,{\mathrm{exp}}\left[-i\int\\!d^{4}x{\bar{J}}\frac{1}{M}J\right]\,,$
(48)

it is straightforward to perform the integrals over $\phi_{n}$ explicitly. We
find

$Z[J=0]=\int\\!{\cal{D}}{\bar{\xi}_{n}}{\cal{D}}\xi_{n}{\cal{D}}A_{n}^{\mu}{\mathrm{exp}}\left[i\\!\int\\!d^{4}x\,\sum_{n}{\cal
L}_{n}^{\rm SCET}\right]\,,$ (49)

where

${\cal L}_{n}^{\rm
SCET}={\bar{\xi}}_{n}\left[in\\!\cdot\\!D+iD\\!\\!\\!\\!/_{\perp}\frac{1}{i{\bar{n}}\\!\cdot\\!D}iD\\!\\!\\!\\!/_{\perp}\right]\frac{{\bar{n}}\\!\\!\\!/}{2}\xi_{n}\,.$
(50)

Note that in getting to Eqs. (49) and (50) no expansion has been made, only
integration of modes in the generating functional. Also note that in Eq.(49)
we have omitted the determinant factor in Eq. (48). Indeed it is easy to show
that

$\displaystyle\det\left(\frac{n\\!\\!\\!/}{2}\bar{n}\\!\cdot\\!D\right)=\int\\!{\cal{D}}\eta_{n}{\cal{D}}{\bar{\eta}_{n}}\,\,{\mathrm{exp}}\left[-\\!\int\\!d^{4}x\,{\bar{\eta}_{n}}\left(\frac{n\\!\\!\\!/}{2}\bar{n}\\!\cdot\\!D\right)\eta_{n}\right]$
$\displaystyle=\int\\!{\cal{D}}\eta_{n}^{\prime}{\cal{D}}{\bar{\eta}}_{n}^{\prime}\,\,{\mathrm{exp}}\left[-\\!\int\\!d^{4}x\,{\bar{\eta}}_{n}^{\prime}\left(\frac{n\\!\\!\\!/}{2}W^{\dagger}_{n}\bar{n}\\!\cdot\\!DW_{n}\right)\eta_{n}^{\prime}\right]$
$\displaystyle=\det\left(\frac{n\\!\\!\\!/}{2}\bar{n}\\!\cdot\\!\partial\right),$
(51)

where we have defined $\eta_{n}^{\prime}=W_{n}^{\dagger}\eta_{n}$. Thus the
determinant is just an overall constant and can be ignored.

We can now move on and consider the addition of current terms in the action.
Keeping the currents ${\bar{J}}_{n}{\cal M}_{n}$ and ${\bar{\cal M}}_{n}J_{n}$
for the fields $\psi_{n}$ and $\bar{\psi}_{n}$, but still neglecting the
currents $J_{k}$ for the local operators ${\cal Q}_{k}$, and again performing
the integrals over $\phi_{n}$ and $\bar{\phi}_{n}$ gives

$\displaystyle
Z[J_{k}=0]=\int\\!{\cal{D}}{\bar{\xi}_{n}}{\cal{D}}\xi_{n}{\cal{D}}A_{n}^{\mu}\,{\mathrm{exp}}\left[i\\!\int\\!d^{4}x\,S^{\rm
SCET}(J_{k}=0)\right]\,,$

with

$\displaystyle S^{\rm SCET}(J_{k}=0)$ $\displaystyle=$
$\displaystyle\sum_{n}{\cal
L}_{I}^{n}+{\bar{J}}^{\xi}_{n}{\cal{M}}^{\xi}_{n}{\cal{R}}_{n}\xi_{n}+{\bar{\xi}}_{n}{\bar{\cal{R}}}_{n}{\bar{\cal{M}}}^{\xi}_{n}J^{\xi}_{n}+{\bar{J}}^{\chi}_{n}{\cal{M}}^{\chi}_{n}{\cal{R}}_{n}\xi_{n}+{\bar{\xi}}_{n}{\bar{\cal{R}}}_{n}{\bar{\cal{M}}}^{\chi}_{n}J^{\chi}_{n}+J_{n\mu}^{A}A_{n}^{\mu}+J_{n\mu}^{\cal
B}{\cal B}_{n}^{\mu}(A_{n})$ (53) $\displaystyle-\left(\bar{J}_{n}^{\xi}{\cal
M}_{n}^{\xi}+\bar{J}_{n}^{\chi}{\cal
M}_{n}^{\chi}\right)\frac{1}{i{\bar{n}}\\!\cdot\\!D}\frac{{\bar{n}}\\!\\!\\!/}{2}\left(\bar{\cal
M}_{n}^{\xi}J_{n}^{\xi}+\bar{\cal M}_{n}^{\chi}J_{n}^{\chi}\right)\,.$

Here we have defined

${\cal{R}}_{n}=\left[1+\frac{1}{i{\bar{n}}\\!\cdot\\!D}iD\\!\\!\\!\\!/_{\perp}\frac{{\bar{n}}\\!\\!\\!/}{2}\right]\,.$
(54)

In order for this action to be equal to the action of SCET given in Eq. (21)
(still with $J_{k}=0$), requires

$\displaystyle{\cal{M}}^{\xi}_{n}{\cal{R}}_{n}\xi_{n}\equiv\xi_{n}\,,\qquad{\cal{M}}^{\chi}_{n}{\cal{R}}_{n}\chi_{n}\equiv
W_{n}^{\dagger}\xi_{n}\,,$ (55)

in addition to having the second line in Eq. (53), corresponding to contact
terms arising when taking two derivatives of the generating functional with
respect to the currents $J_{n}^{\xi/\chi}$, vanish. There are two possible
solutions for each of the ${\cal{M}}^{\xi}_{n}$ and ${\cal{M}}^{\chi}_{n}$ to
satisfy Eq. (55), namely

$\displaystyle{\cal{M}}^{\xi}_{n}$ $\displaystyle={\cal{R}}_{n}^{-1}$
$\displaystyle{\rm or}\qquad{\cal{M}}^{\xi}_{n}$ $\displaystyle=P_{n}\,,$
$\displaystyle{\cal{M}}^{\chi}_{n}$
$\displaystyle=W_{n}^{\dagger}{\cal{R}}_{n}^{-1}$ $\displaystyle{\rm
or}\qquad{\cal{M}}^{\chi}_{n}$ $\displaystyle=W_{n}^{\dagger}P_{n}\,.$ (56)

While both of these solutions for ${\cal M}_{n}$ give the same answer, the
second choice is in practice much easier to use. This is because choosing
${\cal{M}}^{\xi}_{n}={\cal R}_{n}^{-1}$ in Eq. (42) adds couplings between
fermions and gluons to the current terms, complicating perturbative
calculations significantly. Furthermore, for the second solution the second
line in Eq. (53) vanishes as desired. Therefore, for
${\cal{M}}^{\xi}_{n}=P_{n}$ and ${\cal{M}}^{\chi}_{n}=W^{\dagger}_{n}P_{n}$ we
obtain for $J_{k}=0$ the desired result $S^{\rm SCET}=S_{I}$, where $S_{I}$ is
defined in Eq. (21).

Finally, we add the currents for the local operators ${\cal Q}_{k}$ back to
the action. Since these operators couple fields with different $n$’s to one
another, integrating out the $\phi_{n}$ fields is very complicated. However,
there is a simple choice for the operators ${\cal Q}_{k}$ that will directly
reproduce the form $\sum_{k}J_{k}{\cal O}_{k}$ present in the final answer,
Eq. (21). This is achieved by taking

${\cal Q}_{k}(\psi_{n},A_{n})={\cal O}_{k}(W_{n}^{\dagger}P_{n}\psi_{n},{\cal
B}_{n}(A_{n}))\,,$ (57)

with $P_{n}$ defined in Eq. (45). Since $P_{n}\psi_{n}=\xi_{n}$, this choice
eliminates any dependence on $\phi_{n}$ in ${\cal Q}_{k}$. Thus, the integrals
over $\phi_{n}$ can be performed as before and we therefore find

${\cal Q}_{k}(\psi_{n},A_{n})={\cal O}_{k}(W_{n}^{\dagger}\xi_{n},{\cal
B}_{n}(A_{n}))\,.$ (58)

In conclusion, the generating functional in terms of QCD fields

$Z[J]=\int{\cal{D}}{\bar{\psi_{n}}}{\cal{D}}\psi_{n}{\cal{D}}A_{n}^{\mu}{\mathrm{exp}}\left[i\int\\!d^{4}x\,S_{\rm
QCD}(\psi_{n},A_{n},J)\right]\,,$ (59)

with $S_{\rm QCD}$ defined by

$\displaystyle S_{\rm QCD}$ $\displaystyle\\!\\!=\\!\\!$
$\displaystyle\sum_{n}\big{[}{\cal{L}}^{\rm
QCD}_{n}+{\bar{J}}^{\xi}_{n}P_{n}\psi_{n}+{\bar{\psi}}_{n}P_{\bar{n}}J^{\xi}_{n}+{\bar{J}}^{\chi}_{n}W_{n}^{\dagger}P_{n}\psi_{n}$
(60)
$\displaystyle+{\bar{\psi}}_{n}P_{\bar{n}}W_{n}J^{\chi}_{n}+J_{n\mu}^{A}A_{n}^{\mu}+J_{n\mu}^{\cal
B}{\cal B}_{n}^{\mu}(A_{n})\big{]}$
$\displaystyle+\sum_{k}J_{k}{\cal{O}}_{k}(W^{\dagger}_{n}P_{n}\psi_{n},{\cal
B}_{n}(A_{n}))\,,$

is identical to the generating functional defined in Eqs. (20) and (21) in
terms of SCET fields. This proves that the collinear sector of SCET is
equivalent to a theory containing multiple copies of QCD, where the only
interactions between them are contained in the local operators ${\cal O}_{k}$.

So far we have only considered the collinear sector of SCET, but of course it
is well known that usoft degrees of freedom are required in order to reproduce
the long distance dynamics of QCD. On the other hand, it is also well known
that at leading order in the effective theory the interactions between usoft
and collinear particles can be removed to all orders in perturbation theory by
using the field redefinition Bauer:2001yt

$\xi_{n}\to Y_{n}\xi_{n}\,,$ (61)

where

$Y_{n}={\rm P}\exp\left[ig\\!\int_{0}^{\infty}\\!{\rm
d}s\,\,n\\!\cdot\\!A(ns+x)\right]\,.$ (62)

Thus, we can include the interactions with the usoft gluons by making a
similar field redefinition on the fields $\psi_{n}$. This implies that the
action given in Eq. (42), but now with

${\cal L}_{n}^{\rm
QCD}=\bar{\psi}_{n}\,\left(iD\\!\\!\\!\\!/+gn\\!\cdot\\!A_{us}\frac{{\bar{n}}\\!\\!\\!/}{2}\right)\,\psi_{n}\,$
(63)

reproduces both the collinear and usoft interactions of the collinear fields.

In conclusion, we have shown how SCET can be quantized either in terms of
gauge dependent or gauge invariant fields. In practice, most calculations in
the literature are performed using the gauge dependent degrees of freedom,
whereas the external operators have to depend on the gauge invariant fields.
Using our results, one can perform the calculations directly in terms of the
gauge invariant fields, reducing the number of Feynman diagrams significantly.
We have then moved on to show how the collinear sector of SCET is equivalent
to a theory constructed out of multiple decoupled copies of full QCD, in the
sense that each copy describes the interactions of fields in a given direction
and the different copies do not interact with one another. We have also shown
in detail how to construct the local operators describing precisely the
interactions between the different copies of QCD, such that any SCET
correlator at leading order can be reproduced.

###### Acknowledgements.

We would like to thank Iain Stewart for helpful discussions. This work was
supported in part by the Director, Office of Science, Office of High Energy
Physics of the U.S. Department of Energy under the Contract DE-AC02-05CH11231.
CWB acknowledges support from an LDRD grant from LBNL. OC would like to thank
the Fulbright Program and the Spanish Ministry of Education and Science for
financial support under grant number FU2005-0791 and also LBNL and UCB-BCTP
for their hospitality this past year.

## Appendix: Diagrammatic proof of the equivalence of QCD and SCET with one
collinear direction

In the main body of this paper we have shown that any collinear SCET diagram
can be obtained using a gener- ating functional in which the interactions
between the fields are equivalent to full QCD, but the external cur- rents are
modified to contain projection operators. This relation was first discussed in
Bauer:2000yr  and used in Becher:2006qw  to calculate jet functions in SCET.
In this appendix we want to prove this identity diagrammatically for the
correlator containing two collinear fermions and $N$ collinear gluons.

We will accomplish this by working out in both theories the Feynman diagrams
for $N$ gluons coupled to a fermion line, from which the correlator can be
constructed. Using this result we will then show that both of these
calculations lead to equivalent answers. Note that there are $N!$ possible
color structures, and for each of them the QCD result has to equal the SCET
result. We begin by showing this equivalence for the color structure
$T^{a_{1}}\,T^{a_{2}}\,\ldots\,T^{a_{N}}$, and then discuss how the result can
be modified to include the other color structures as well.

Define $Q^{(N)}$ and $S^{(N)}$ to be the QCD and SCET cor- relators for this
color structure in momentum space, multiplied by a factor of $p_{i}^{2}$ for
each internal propagator and with the factor $g_{s}^{N}$ removed. This gives

$\displaystyle
Q^{(N)}=P_{n}p\mspace{-10.0mu}/\mspace{3.0mu}_{0}\gamma^{\mu_{1}}p\mspace{-10.0mu}/\mspace{3.0mu}_{1}\dots\gamma^{\mu_{N}}p\mspace{-10.0mu}/\mspace{3.0mu}_{N}P_{\bar{n}}\,,$
(64) $\displaystyle S^{(N)}=\sum_{k=1}^{N}S^{(N-k)}L_{k}\,.$ (65)

The first equation follows simply from the QCD Feynman rules, while the SCET
equation is a recurrence formula, that takes into account all the
possibilities of having $k$ out of the $N$ gluons being emitted from a single
vertex. $L_{k}$ is therefore the Feynman rule for $k$-gluon emissions from a
single vertex, multiplied by a factor of $\prod_{i}p_{i}^{2}/g_{s}$ to account
for the removal of the factors $p_{i}^{2}$ and $g_{s}$, as discussed above:

$L_{k}\frac{{\bar{n}}\\!\\!\\!/}{2}=i(\bar{n}\\!\cdot\\!p_{N})\frac{p_{N-k+1}^{2}\cdots
p_{N-1}^{2}}{(-g)^{k}}V_{k}\,,$ (66)

with

$\displaystyle
V_{k}=\frac{i(-g)^{k}\bar{n}^{\mu_{N-k+2}}\dots\bar{n}^{\mu_{N-1}}}{\bar{n}\\!\cdot\\!p_{N-k+1}\dots\bar{n}\\!\cdot\\!p_{N-1}}\frac{\bar{n}\mspace{-10.0mu}/\mspace{3.0mu}}{2}\times$
(67)
$\displaystyle\times\Big{(}\gamma^{\mu_{N-k+1}}_{\perp}\gamma^{\mu_{N}}_{\perp}-\bar{n}^{\mu_{N}}\gamma^{\mu_{N-k+1}}_{\perp}\frac{p\mspace{-10.0mu}/\mspace{3.0mu}_{N}^{\perp}}{\bar{n}\\!\cdot\\!p_{N}}+$
$\displaystyle+\frac{p\mspace{-10.0mu}/\mspace{3.0mu}_{N-k}^{\perp}p\mspace{-10.0mu}/\mspace{3.0mu}_{N}^{\perp}}{\bar{n}\\!\cdot\\!p_{N-k}\bar{n}\\!\cdot\\!p_{N}}\bar{n}^{\mu_{N-k+1}}\bar{n}^{\mu_{N}}-\bar{n}^{\mu_{N-k+1}}\frac{p\mspace{-10.0mu}/\mspace{3.0mu}_{N-k}^{\perp}\gamma^{\mu_{N}}_{\perp}}{\bar{n}\\!\cdot\\!p_{N-k}}\Big{)}\,.$

We will show the equivalence $Q^{(N)}=S^{(N)}$ by induction. For $N=0$ it is
straightforward:

$\displaystyle Q^{(0)}$
$\displaystyle=P_{n}p\mspace{-10.0mu}/\mspace{3.0mu}_{0}P_{\bar{n}}=\frac{n\mspace{-10.0mu}/\mspace{3.0mu}}{2}\bar{n}\\!\cdot\\!p_{0},$
(68) $\displaystyle S^{(0)}$
$\displaystyle=\frac{n\mspace{-10.0mu}/\mspace{3.0mu}}{2}\bar{n}p_{0}=Q^{(0)}\,.$
(69)

Next, we assume that the statement $Q=S$ holds for $0,1,\dots N-1$ to show
that this leads to $Q^{(N)}=S^{(N)}$. This implies

$Q^{(N)}=\sum_{k=1}^{N}Q^{(N-k)}L_{k}\,.$ (70)

To prove Eq. (70) we rewrite the general QCD correlator $Q^{(N)}$ by pushing
the projection operator $P_{n}$ in Eq. (64) through the
$p\mspace{-10.0mu}/\mspace{3.0mu}_{n}$ and $\gamma^{\mu_{n}}$, to obtain

$Q^{(N)}=\frac{n\mspace{-10.0mu}/\mspace{3.0mu}}{2}\sum_{m=0}^{N}\sum_{l=1}^{C_{2N+1}^{2m}}\chi^{2m,2N+1}_{i_{1}\dots
i_{2m}}\,,$ (71)

where

$\displaystyle\chi^{2m,2N+1}_{i_{1}\dots
i_{2m}}={(-1)}^{i_{1}+\dots+i_{2m}-(1+\dots+2m)}\perp_{i_{1}}\dots\perp_{i_{2m}}$
$\displaystyle\quad\quad\quad\times(\bar{n}_{j_{1}}n_{j_{2}}\bar{n}_{j_{3}}\dots
n_{j_{2N-2m}}\bar{n}_{j_{2N+1-2m}})\,.$ (72)

Here $C_{k}^{l}$ denotes the binomial coefficient for $l$ choose $k$, and we
have used a shorthand notation in which $\bar{n}_{j}$ corresponds to
$\bar{n}\\!\cdot\\!p$ for even $j$ and to $\bar{n}^{\mu}$ for odd $j$ and
accordingly $\perp_{j}$ corresponds to
$p\mspace{-10.0mu}/\mspace{3.0mu}_{\perp}$ for even $j$, while
$\gamma_{\perp}^{\mu}$ for odd $j$.

We would like to comment on how we obtained this result. Expanding each
$\gamma$ matrix on the right hand side of the Eq. (64) according to
$\gamma^{\alpha}=\bar{n}^{\alpha}\frac{n\mspace{-10.0mu}/\mspace{3.0mu}}{2}+n^{\alpha}\frac{\bar{n}\mspace{-10.0mu}/\mspace{3.0mu}}{2}+\gamma^{\alpha}_{\perp}$
will result in terms with fixed number $0\leq N_{\perp}\leq 2N+1$ of
$\gamma_{\perp}$’s, together with $(2N+1-N_{\perp})$ of
$n\mspace{-10.0mu}/\mspace{3.0mu}$ or
${\bar{n}}\mspace{-10.0mu}/\mspace{3.0mu}$. Since the
$n\mspace{-10.0mu}/\mspace{3.0mu}$ and
${\bar{n}}\mspace{-10.0mu}/\mspace{3.0mu}$ terms have to alternate, and the
projection operator forces the first and last term to be
$n\mspace{-10.0mu}/\mspace{3.0mu}$, $N_{\perp}$ has to be an even number.

As a next step, we work out the sum on the right hand side of Eq. (70). Note
that the term $L_{k}$ contains factors of $p_{i}^{2}$ in the numerators, while
there are no such terms on the left hand side of Eq. (70). However, both
$Q^{(N-k)}$ and $L_{k}$ contain terms with
$p\mspace{-10.0mu}/\mspace{3.0mu}_{\perp}$, which can lead to
$p_{\perp}^{2}=p^{2}-n\\!\cdot\\!p\,{\bar{n}}\\!\cdot\\!p$. After a
straightforward, but lengthy calculation, one can show that

$\sum_{k=1}^{N}Q^{(N-k)}L_{k}=\frac{n\mspace{-10.0mu}/\mspace{3.0mu}}{2}\sum_{m=0}^{N}\sum_{l=1}^{C_{2N+1}^{2m}}\chi^{2m,2N+1}_{i_{1}\dots
i_{2m}}\,.$ (73)

Thus, both sides of Eq. (70) are equal and we have thus shown that
$Q^{(N)}=S^{(N)}$ for all values of $N$.

So far we have only dealt with the term with color structure $T^{a_{1}}\dots
T^{a_{N}}$. Keeping the general color structure allows us to write

$\displaystyle Q^{(N)}\rightarrow\sum_{l=1}^{N!}Q^{(N)}_{i_{1}\dots
i_{N}}T^{a_{i_{1}}}\dots T^{a_{i_{N}}}\,,$ (74) $\displaystyle
S^{(N)}\rightarrow\sum_{l=1}^{N!}S^{(N)}_{i_{1}\dots i_{N}}T^{a_{i_{1}}}\dots
T^{a_{i_{N}}}\,.$ (75)

What we have shown so far is that
$Q^{(N)}_{1,2,\dots,N}=S^{(N)}_{1,2,\dots,N}$. However, it is clear that the
proof goes through for any color permutation, with obvious replacements to
account for the different orderings of the gluons. Finally, notice that triple
or quartic gluon vertices do not change the result, since they are the same in
QCD and SCET. This completes the proof.

## References

  * (1) C. W. Bauer, S. Fleming and M. E. Luke, Phys. Rev. D 63, 014006 (2000) [arXiv:hep-ph/0005275].
  * (2) C. W. Bauer, S. Fleming, D. Pirjol and I. W. Stewart, Phys. Rev. D 63, 114020 (2001) [arXiv:hep-ph/0011336].
  * (3) C. W. Bauer and I. W. Stewart, Phys. Lett. B 516, 134 (2001) [arXiv:hep-ph/0107001].
  * (4) C. W. Bauer, D. Pirjol and I. W. Stewart, Phys. Rev. D 65, 054022 (2002) [arXiv:hep-ph/0109045].
  * (5) C. M. Arnesen, J. Kundu and I. W. Stewart, Phys. Rev. D 72, 114002 (2005) [arXiv:hep-ph/0508214].
  * (6) T. Becher and M. Neubert, Phys. Lett. B 637, 251 (2006) [arXiv:hep-ph/0603140].
  * (7) A. V. Manohar, Phys. Rev. D 68, 114019 (2003) [arXiv:hep-ph/0309176].
  * (8) A. Bassetto, M. Dalbosco, I. Lazzizzera and R. Soldati, Phys. Rev. D 31, 2012 (1985).
  * (9) E. V. Veliev, Phys. Lett. B 498, 199 (2001).
  * (10) G. ’t Hooft, Nucl. Phys. B 75, 461 (1974), L. H. Ryder, Cambridge, Uk: Univ. Pr. ( 1985) 443p.


11institutetext: University of Innsbruck, Austria 22institutetext: University
of Warsaw, Poland 22email:
shawn.wangqingxiang<EMAIL_ADDRESS>
# JEFL: Joint Embedding of Formal Proof Libraries

Qingxiang Wang 11 Cezary Kaliszyk 1122 0000-0002-8273-6059

###### Abstract

The heterogeneous nature of the logical foundations used in different
interactive proof assistant libraries has rendered discovery of similar
mathematical concepts among them difficult. In this paper, we compare a
previously proposed algorithm for matching concepts across libraries with our
unsupervised embedding approach that can help us retrieve similar concepts.
Our approach is based on the fasttext implementation of Word2Vec, on top of
which a tree traversal module is added to adapt its algorithm to the
representation format of our data export pipeline. We compare the
explainability, customizability, and online-servability of the approaches and
argue that the neural embedding approach has more potential to be integrated
into an interactive proof assistant.

###### Keywords:

Unsupervised Embedding Concept Alignments Proof Formalization System
Integration.

##  1 Introduction

One of the challenges hindering massive formalization of mathematics is the
heterogeneous nature of the logical frameworks used in various interactive
proof assistants [11, 27, 8, 13]. When formalizing proofs against one formal
library, it is informative to explore whether and how similar things are done
in other libraries. Such exploration has to be done manually and would usually
require expertise in the other proof assistants. It would be nice if a tool
could let users more systematically explore and discover commonality among
formal libraries.

Not only can such a tool be an informative recommender when integrated into an
interactive proof assistant, but exploring commonalities among formal
libraries is also an interesting problem per se. Through time, multiple
versions of the same or similar mathematical concepts have been formalized
separately, resulting in repetitive work [21]. To the mathematically oriented,
it is quite irksome that identical mathematical concepts must require
idiosyncratic formalizations in order to achieve assurance. We believe that by
investigating their commonalities, insights on improving interoperability
among proof assistants can be obtained, thereby advancing the frontiers of
combining systems.

Previous works [4, 6] on this problem let us obtain a data export pipeline
that could transform data from six proof assistants into a common term
representation format (Fig. 1), on top of which an iterative pattern-matching
algorithm that could output constant/theorem pairs with high similarity scores
was invented by Gauthier. The alignments between the concepts across multiple
proof libraries or within one library have been useful for tasks including
conjecturing [7], browsing multiple libraries simultaneously [25], and proof
automation using learned alignments [5].

The Gauthier approach, while being remarkably effective and useful, lacks
explainability, customizability and online-servability that hamper its
integration into proof assistants. By these three notions we mean the lack of
mathematical intuitiveness, lack of room for customization, and lack of
possibility for system integration, respectively. We introduce an alternative
embedding approach based on the superb engineering of the fasttext
implementation [1]. This new approach could potentially overcome these
drawbacks while providing competitive performance. It could also serve as a
highly configurable experiment platform for studying the alignment of multiple
proof assistant libraries. We coin this research JEFL, as an acronym for Joint
Embedding of Formal Libraries.

HOL4 HOL-Light Isabelle Coq Matita Mizar Exporters Preprocess Patternify
Scoring Iteration Main IO, Parsing… Gauthier et al. tt Vector Matrix Utils
Args Dict Model FastText Main / Server JEFLttsexp Figure 1: The architectural
relationship between Gauthier’s approach and JEFL. At the current stage, the
exporters dump text in the tt format (Section 2). JEFL reuses the IO/parsing
module of Gauthier and passes s-expressions to the fasttext implementation.

##  2 Previous Works and the tt Format

Exchanging formal developments within or across formal systems has been
studied through three strands of research. First, on the library translation
side, many tools that can partially translate proofs have been developed,
including those from HOL to Isabelle/HOL [26], HOL Light to Coq [20], HOL
Light to Isabelle/HOL [16], respectively. Second, on the ontology sharing
side, Bortin [2], Rabe [30], Hurd [14], So and Watt [32], and Carlisle et al.
[3] each made their own contribution translating specifications or formal
proof objects between formal or semi-formal mathematical representations.
These two strands of research mostly either solely provide guidelines on
manual processing or require manual work at a certain phase of their
framework.

The third strand comes from enhancements of ITP systems. Heras and
Komendantskaya [12] implemented a recurrent term clustering algorithm to find
proof similarities in Coq/SSReflect libraries. Urban [34] created tools for
large-scale retrieval of the Mizar Mathematical Library into a clausal format.
Kaliszyk and Urban [17] exported the core HOL Light library as well as the
Flyspeck [10] library to evaluate the relevance of lemmas by combining the
power of automated theorem provers. This work was later extended to a web
service [19] and experimented with using multiple representation formats and
different automated theorem provers in [18].

A byproduct along [17, 19, 18] was a collection of exporting and post-
processing techniques specific to HOL Light, including a TPTP-style [33] data
representation format which we internally called “the tt format”. The
formalism of tt is based on a simple term structure that is flexible enough to
represent the kernel representations of formal data on diverse logical
foundations, so there is a potential to export data from multiple proof
assistants into this common format. Based on the export of three HOL libraries
(HOL Light, HOL4, and Isabelle/HOL), Gauthier and Kaliszyk proposed the first
version of their scoring algorithm [4] and used for various conjecturing and
transfer learning tasks. A more comprehensive set of alignment experiments
refined the scoring algorithm, provided a more uniform pattern-matching and
guaranteed convergence, and was used on six proof assistant libraries (adding
Coq, Matita, and Mizar) [6].

Listing 2.1 and 2.2 illustrate the definition of the predecessor of the
naturals (PRE) of HOL Light being translated into a list of three tt items.
The last arguments of them can be parsed into term structures (Fig. 2) using
the type definition in Listing 2.2.

⬇

\-----------------------------------------------------------------------------

let PRE = new_recursive_definition num_RECURSION

‘(PRE 0 = 0) /\

(!n. PRE (SUC n) = n)‘;;

\-----------------------------------------------------------------------------

Listing 2.1: Definition of the predecessor of the naturals PRE in HOL Light.

⬇

\-----------------------------------------------------------------------------

01. tt(’const/arith/PRE’, ty, (’type/nums/num’ > ’type/nums/num’)).

02. tt(’thm/arith/PRE_0’, ax,

((’const/arith/PRE’ (’const/nums/NUMERAL’ ’const/nums/_0’)) =

(’const/nums/NUMERAL’ ’const/nums/_0’))).

03. tt(’thm/arith/PRE_1’, ax,

(![n : ’type/nums/num’]:

((’const/arith/PRE’ (’const/nums/SUC’ n)) = n))).

\-----------------------------------------------------------------------------

Listing 2.2: PRE transformed to three tt items.

⬇

\-----------------------------------------------------------------------------

type ttterm =

| Id of string (* may be a constant or variable *)

| Comb of ttterm * ttterm

| Abs of string * ttterm * ttterm;;

\-----------------------------------------------------------------------------

Listing 2.3: Type definition of tt term in OCaml for parsing.

The HOL Light and HOL4 exports directly use HOLyHammer’s export [18]. For
Isabelle, an ML component was implemented that extracts all theorems of the
theory and writes them together with the declared constants and types in a
text file. The Coq export to the tt format was implemented by Gauthier as part
of his work [6]. For Mizar, we rely on Urban’s MPTP pipeline [35] and
transform the intermediate XML2 representation.

Comb Id(:) Comb Id(PRE) Comb Id(>) Comb Id(num) Id(num) 01 Comb Id(=) Comb
Comb Id(PRE) Comb Id(NUMERAL) Id(0) Comb Id(NUMERAL) Id(0) 02 Comb Id(!) Abs n
Id(num) Comb Id(=) Comb Comb Id(PRE) Comb Id(SUC) Id(n) Id(n) 03ttsexp Figure
2: Term structures of the definition of PRE. The tokens PRE, num, NUMERAL and
SUC are short for const/arith/PRE, type/nums/num, const/nums/NUMERAL and
const/nums/SUC, respectively. Note that the constant const/arith/PRE is
included into the term 01 with a type assignment operator ’:’. This allows
embedding vectors to be assigned to the definition constants.

##  3 The Architecture of JEFL

In this paper, we focus on the core similarity discovery algorithm. Our claim
on advantages in JEFL is with respect to the algorithmic part of the system.
We leave the eventual integration of the whole framework into proof
assistants, with issues such as handling constants that have not been
encountered during training, as future work.

###  3.1 Similarity through Embedding

A natural way to find similarities among concepts is to treat our problem as a
distributed representation learning task. Generally speaking, given a
structure composed of atomic units, distributed representation learning seeks
to represent each of the atomic units with a low-dimensional vector. In
effect, all the units are embedded into a Euclidean space, with their
coordinates respecting the overall structure. The notion distributedness comes
from the fact that the vocabulary size of a corpus is much larger than the
dimension of a vector, and the information of an atomic unit is distributed in
the coordinates of a vector.

The vectors are learned by analyzing the context of each unit, i.e. the
information of units adjacent to or surrounding a target unit. Once vector
representations for units are learned, similarity between units can then be
computed by cosine similarity with a range from $[-1,1]$. For a set of units,
vector representation can be computed by taking average of the vectors, and
then similarity between different sets of units can also be computed using
cosine similarity.

Notable unsupervised distributed representation learning algorithms include
Pennington et al.’s GloVe algorithm [28] and Mikolov et al.’s Word2Vec
algorithm [23, 24]. In this paper, we use Mikolov’s Word2Vec algorithm.
Word2Vec works on texts or lists of word tokens. For each word in the training
corpus, a randomized span of words surrounding that word is picked to form the
context of that word. The context is then consumed by the Word2Vec model to
conduct one step of the stochastic gradient descent updates.

###  3.2 Adaptation of the tt Format in Word2Vec

To illuminate our technique, it is interesting to note that DeepWalk [29] and
Node2Vec [9], two methods on embedding large networks, also use Word2Vec as
their underlying algorithm. The data used by DeepWalk and Node2Vec are single-
graph datasets with nodes that contain heterogenous information such as social
profile details. To fit Word2Vec, first the node information of the graph has
to be transformed into a dictionary through data processing. Then we perform
random walks along the paths of the graph to generate node sequences that
resemble text corpus. For each node in a node sequence, the corresponding
context is generated as a span of nodes surrounding that node.

In our case, different from DeepWalk and Node2Vec, the formal library data in
the tt format are not a single graph but a collection of trees. More
precisely, in order to compare two libraries, we need two lists of tt items
from the two libraries to provide as training data. The tt items are parsed as
trees and then traversed in different ways to create sequences of node
constants. Examples of traversals include preorder, inorder, postorder
traversals and their reverses, random walks from the root to a leaf, or just
dump the leaves of a tree in some order. With clever design, these traversals
can also be combined to create hybrid orders. At the current phase we
implemented a simple weighted mechanism combining preorder, inorder and
postorder traversals. The weights of traversals are used to control the
learning rate for SGD updates and are hyperparameters determined before
training (Fig. 3). We anticipate further experimental insights when other
forms of traversals are implemented in the future.

Comb Id(!) Abs(x) Id(num) Comb Id(=) Comb Id(x) Id(x) pre:1 in:2 post:9 pre:2
in:1 post:1 pre:3 in:4 post:8 pre:4 in:3 post:2 pre:5 in:6 post:7 pre:6 in:5
post:3 pre:7 in:8 post:6 pre:8 in:7 post:4 pre:9 in:9 post:5 Comb Id ! Abs x
Id num Comb Id = Comb Id x Id xcbow(model, 0.5*lr, preorder_line); Id ! Comb
Id num Abs x Id = Comb Id x Comb Id xcbow(model, 0.3*lr, inorder_line); Id !
Id num Id = Id x Id x Comb Comb Abs x Combcbow(model, 0.2*lr, postorder_line);
ttsexp Figure 3: Preorder, inorder, and postorder traversals of a simple
theorem $\forall x:\text{num}.\left(x=x\right)$, with weights 0.5, 0.3, 0.2,
respectively. Example illustrated by calling the CBOW method of fasttext,
where lr is the learning rate and the third argument contains the token
sequence above it. Inside the CBOW method, for each token, a randomized span
of words surrounding that token is obtained to compute the hidden vector.

Both DeepWalk and Node2Vec directly use the Word2Vec implementation of the
Gensim [31] topic modeling library. For ease of future integration into proof
assistants we pick a dedicated Word2Vec implementation fasttext [15] as our
base platform. To make our customization less intrusive we add a custom tree
traversal module to the codebase of fasttext, also called the tt module (Fig.
1). The tt module parses the terms in the tt format and builds corresponding
trees in the memory of JEFL.

###  3.3 The SGD Updates of Word2Vec

It remains to discuss the core Word2Vec algorithm, which is divided into two
aspects: 1. what is the probability model for Word2Vec training and 2. how the
loss function is computed. In the former, there are the continuous bag-of-
words model (CBOW) and the skip-gram model. They appear at the step of the
training loop outside stochastic gradient descent (SGD) updates and determine
how data samples are used. In the latter, there are the softmax loss, the
hierarchical softmax loss, and the negative sampling loss. They compute the
loss function, at the same time determine the gradients and update the input
and output matrices. The two training models are compatible with the three
loss functions, so there are in total six variations of the Word2Vec
algorithm111As to writing of this paper, one more loss function (the one-vs-
all, or the ova loss) has been added to the latest version of fasttext, making
in total eight variations..

As the full Word2Vec algorithm is extensive, we briefly describe the
difference between skip-gram and CBOW using the simplest softmax case. We skip
detailed derivations and remind the reader of the abundance of study materials
of Word2Vec on the internet222The first author finds this note
https://github.com/renpengcheng-github/nlp/tree/master/3.word2vec (in Chinese)
particularly helpful in understanding Word2Vec..

Let $\mathcal{C}$ be the training corpus, $V$ be the size of the dictionary of
$\mathcal{C}$, and $D$ be the dimension of a word vector. Denote
$M\in\mathbb{R}^{V\times D}$ as the input matrix which we use to store all the
word vectors. Denote $N\in\mathbb{R}^{V\times D}$ as the output matrix which
we use to store customized data items depending on the loss function. Let
$w\in\left\\{1,2,\ldots,V\right\\}$ be a word, or more precisely, the index of
an actual word in the dictionary. We denote $M_{w}$ as the $w$-th row of the
input matrix $M$. Similarly we denote $N_{u}$ as the $u$-th row of the output
matrix $N$, given a word $u\in\left\\{1,2,\ldots,V\right\\}$. Both $M_{w}$ and
$N_{u}$ are $D$-dimensional row vectors. For each word $w$, denote
$\text{context}(w)$ as a randomized span of words surrounding $w$. Let
$\eta>0$ be the learning rate.

From the probability modeling point of view, CBOW amounts to maximizing the
log-likelihood of the form

$\displaystyle\mathcal{L}$
$\displaystyle=\log\prod_{w\in\mathcal{C}}P\left(w|\text{context}(w)\right)=\sum_{w\in\mathcal{C}}\log\text{softmax}(Nh^{T})_{w},$

where

$\displaystyle
h=\frac{1}{|\text{context}(w)|}\sum_{u\in\text{context}(w)}M_{u}$

is the hidden vector. The SGD updates are computed by taking increments of the
gradients of the objective (as we want to maximize the log-likelihood) 333We
use the term stochastic gradient descent here for convention though we are in
fact doing stochastic gradient ascent.

$\displaystyle N_{u}$
$\displaystyle:=N_{u}+\eta\left(\delta_{uw}-\text{softmax}(Nh^{T})_{u}\right)h$
$\displaystyle\text{for }u\in\\{1,\ldots,V\\}$ $\displaystyle M_{u}$
$\displaystyle:=M_{u}+\frac{\eta}{|\text{context}(w)|}\sum_{v=1}^{V}\left(\delta_{vw}-\text{softmax}(Nh^{T})_{v}\right)N_{v}$
$\displaystyle\text{for }u\in\text{context}(w)$

The skip-gram model amounts to maximizing the log-likelihood of the following
form

$\displaystyle\mathcal{L}$
$\displaystyle=\log\prod_{w\in\mathcal{C}}P\left(\text{context}(w)|w\right)=\log\prod_{w\in\mathcal{C}}\prod_{u\in\text{context}(w)}p(u|v)$
$\displaystyle=\sum_{w\in\mathcal{C}}\sum_{u\in\text{context}(w)}\log\text{softmax}(Nh^{T})_{u}$

where

$h=M_{w}$

is a $D$-dimensional row vector. For each $u\in\text{context}(w)$, the SGD
updates are

$\displaystyle N_{\widetilde{w}}$
$\displaystyle:=N_{\widetilde{w}}+\eta\left(\delta_{\widetilde{w}u}-\text{softmax}(Nh^{T})_{\widetilde{w}}\right)M_{w}$
$\displaystyle\text{for }\widetilde{w}\in\left\\{1,\ldots,V\right\\}$
$\displaystyle M_{w}$
$\displaystyle:=M_{w}+\eta\sum_{v=1}^{V}\left(\delta_{vu}-\text{softmax}(Nh^{T})_{v}\right)N_{v}.$

1:for $w\in\mathcal{C}$ do

2: Get sample $(w,\text{context}(w))$. $\triangleright$ See Section 3.2

3: if CBOW then

4: $h:=\mathbf{0}$

5: for $v\in\text{context}(w)$ do

6: $h:=h+M_{v}$

7: end for

8: $h:=h/|\text{context}(w)|$ $\triangleright$ 1\. Get hidden vector (cbow)

9: $g:=\mathbf{0}$

10: for $u\in\\{1,\ldots,V\\}$ do $\triangleright$ Room for speedup

11: $s:=\text{softmax}\left(Nh^{T}\right)_{u}$

12: $\alpha:=\eta\left(\delta_{uw}-s\right)$

13: $g:=g+\alpha N_{u}$ $\triangleright$ 2\. Accumulate gradient (cbow)

14: $N_{u}:=N_{u}+\alpha h$ $\triangleright$ 3\. Update output matrix (cbow)

15: end for

16: $g:=g/|\text{context}(w)|$

17: for $u\in\text{context}(w)$ do

18: $M_{u}:=M_{u}+g$ $\triangleright$ 4\. Update input rows (cbow)

19: end for

20: else$\triangleright$ Skip-gram

21: $h:=M_{w}$ $\triangleright$ 1\. Get hidden vector (skipgram)

22: for $u\in\text{context}(w)$ do

23: $g:=\mathbf{0}$

24: for $\widetilde{w}\in\left\\{1,\ldots,V\right\\}$ do $\triangleright$ Room
for speedup

25: $s:=\text{softmax}\left(Nh^{T}\right)_{\widetilde{w}}$

26: $\alpha:=\eta\left(\delta_{\widetilde{w}u}-s\right)$

27: $g:=g+\alpha N_{\widetilde{w}}$ $\triangleright$ 2\. Accumulate gradient
(skipgram)

28: $N_{\widetilde{w}}:=N_{\widetilde{w}}+\alpha h$ $\triangleright$ 3\.
Update output matrix (skipgram)

29: end for

30: $M_{w}:=M_{w}+g$ $\triangleright$ 4\. Update input rows (skipgram)

31: end for

32: end if

33:end for

Algorithm 1 Full algorithm for CBOW and skip-gram with softmax loss

###  3.4 The fasttext Implementation of Word2Vec

The full SGD update algorithm is shown in Algorithm 1. Notice that, for both
CBOW and skip-gram, in each round of model updates there are essentially four
identical steps: 1. obtain hidden vector, 2. accumulate gradient, 3. update
rows of the output matrix, and 4. update rows of the input matrix. This four-
step abstraction is general not only for softmax but also for hierarchical
softmax and negative sampling, which are specifically designed to speed up the
calculation of the inner loop in line 10, 24 of Algorithm 1.

The architecture of fasttext was inspired by this four-step abstraction. Since
its initial development in 2016, lots of advanced functionalities have been
added on top of the Word2Vec algorithm, including model quantization,
autotuning, python binding, etc. This makes the codebase large and many of
those functionalities are irrelevant to our research. Therefore we use an
earlier commit in late 2016 as our
base444c62abb89396a94520f009f9095874953735e0d75. In this commit, all six
variations of Word2Vec have been implemented and very few advanced
functionalities are added. Two of them worth mentioning are: 1. subsampling of
most frequent words, and 2. subword information enrichment trick. The first is
an extension of the Word2Vec algorithm in [24] to filter out disproportionally
frequent words in the training corpus. This function is disabled since it is
obvious in our dataset that the most frequent tokens are always Comb, Id, and
Abs, respectively, and they have to be included to allow for correct parsing
of tt items. The second is a feature in the fasttext implementation [15] which
breaks a word token into segments of character-level n-gram tokens. This is
also disabled since constants in our embedding task (e.g. ’const/arith/PRE’)
constitute a unique and separate entity, and enabling this feature would
normally increase the size of a training model by more than a hundred times.
The original src directory of this commit contains 2054 lines of C++ code
written in C++11.

##  4 Experimenting with JEFL

The core algorithm part of JEFL consists of 8 modules of the original fasttext
plus a custom module for term parsing and traversal (Fig. 1 right). We find
that the best way for customization is to add to the args module a new flag
(isTT) to denote whether our training corpus is a list of tt items or plain
texts. The normal process flow is not interrupted if this flag is false, so
JEFL can also train on plain text. If isTT is true, then subsampling is
suppressed when reading in the input files. This allows all tokens of tt terms
to be read so that term parsing can be done correctly. The tt items are read,
parsed and the parsed terms can be reconstructed as trees in the C++ side.
Helper functions are then called to traverse a tree in different orders, look
up the index values of its constants from a dictionary, and call fasttext’s
original CBOW or skip-gram method for SGD updates (Fig. 3).

We report our initial round of experiments with this platform and two formal
proof libraries, HOL4 and HOL Light, testing the performance of different
hyper-parameter combinations. There are in total 18723 and 16874 lines of tt
items in HOL4 and HOL Light, respectively. We concatenate and shuffle the
exported theorems from the two libraries, and then write them out as
s-expressions [22].555This gives a total of 35597 s-expressions for Word2Vec
training. We evaluate the performance by comparing against the 1000 highest-
scoring constant pairs, that have been manually checked by Gauthier in his
work, and considered here as a baseline.

|  Top-1 Hit |  Top-3 Hit |  Top-10 Hit |  Top-20 Hit
---|---|---|---|---
Tree-Dump |  51 |  101 |  188 |  261
Leaf-Dump |  21 |  61 |  96 |  144
Table 1: Comparison of theorem export formats. Tree-dump exports the whole tree representation in the given order, while leaf-dump exports only the sequence of data present in the leafs. |  Top-1 Hit |  Top-3 Hit |  Top-10 Hit |  Top-20 Hit
---|---|---|---|---
Skip-Gram |  54 |  108 |  264 |  283
CBOW |  51 |  101 |  188 |  261
Table 2: Comparison of models skip-gram and continuous bag of words. |  Top-1 Hit |  Top-3 Hit |  Top-10 Hit |  Top-20 Hit
---|---|---|---|---
Hierarchical Softmax |  78 |  161 |  304 |  419
Negative Sampling |  51 |  101 |  188 |  261
Table 3: Comparison of sampling hierarchical softmax vs. negative sampling (pre-,in-,post-order) |  Top-1 Hit |  Top-3 Hit |  Top-10 Hit |  Top-20 Hit
---|---|---|---|---
(0.33,0.33,0.33) |  51 |  101 |  188 |  261
(0.5,0.3,0.2) |  58 |  103 |  205 |  267
(1,0,0) |  53 |  110 |  204 |  256
(0.5,0.5,0) |  49 |  113 |  207 |  276
(0,0.5,0.5) |  57 |  106 |  203 |  268
Table 4: Combination of the effect of weights given to the different
traversals. The table shows the weights given to pre-order, in-order, and
post-order respectively, together with their effects on finding same constants
across libraries.

We present four sets of experiments for the initial comparison. We measure
JEFL’s performance against the Gauthier baseline by using the “Top-$N$ Hit”
metric, which means the inclusion of the correct answer from the closest $N$
neighbors of the target constant. By default, we use leaf-dump (sequences of
data present in the leafs), CBOW, negative sampling, and equal
(0.33,0.33,0.33) weights. For other key parameters of fasttext, we set vector
dimension as 100, learning rate 0.05, random uniform context window size 1 to
10, training epoch 5 (for most experiments we see little training progress
after epoch 5, so for a fair evaluation we stick with 5 epochs for all
evaluations), 5 negative samples for negative sampling loss, and 4 training
threads.

Experiment 1 (Table 1) tests the difference between tree-dump (dumping
s-expression) vs. leaf-dump (dumping leaves as token sequences). This
experiment is the first one to test that our customization blends with the
normal process flow of fasttext. We see that tree traversal gives better hit
rates than just use the leaves as the former uses more information in
training.

Experiment 2 (Table 2) tests the difference between skip-gram and CBOW. We see
that skip-gram performs better than CBOW in all hit rates. However, as noted
in Section 3.3, skip-gram takes longer time to train (this depends on the size
of the contexts, and in our experiments skip-gram takes about five times
longer). For ease of experiment, we fall back to use CBOW as our default.

Experiment 3 (Table 3) shows a clear advantage of hierarchical softmax over
negative sampling. We see a 60% increase in all the hit rates. We speculate
that this improvement is due to the fact, that the Huffman tree computation in
hierarchical softmax might put an advantage in mining patterns in tree-like
data structures.

Experiment 4 (Table 4) explores different combinations of weights in tree-
traversal. They all outperform leaf-dump, however, none of the combinations
performs significantly better than others. We plan to explore other forms of
traversal such as random walks to see further results.

##  5 Comparison with Iterative Pattern-Matching

In this section, we shortly recall the iterative pattern-matching algorithm
developed by Gauthier and Kaliszyk [6], and compare it with the work presented
here. The iterative pattern matching algorithm is based on the observation
that once mathematical information in different formal libraries is
represented in the same tt format, similar theorems or typing judgements (as
terms of tt) tend to have identical term structures. Accordingly, similar
constants (as leaves of terms) tend to locate in corresponding slots of a term
(Fig. 4). To abstract out common term structure, Gauthier invented the notion
pattern of a term. The pattern of a term $T$ is created by abstracting out, in
a canonical order, all the $T$’s non-logical constants. Two terms $T_{1}$ and
$T_{2}$ sharing the same pattern form a matching pair of terms. Corresponding
slots of a matching pair of terms induce a collection of matching pairs of
constants.

Comb Id(!) Abs(x) Id(num) Comb Id(=) Comb Comb Id(+) Comb Id(x) Id(0) Id(x)
Comb Id(!) Abs(x) Id($v_{1}$) Comb Id(=) Comb Comb Id($v_{2}$) Comb Id(x)
Id($v_{3}$) Id(x) Comb Id(!) Abs(x) Id(real) Comb Id(=) Comb Comb Id($\times$)
Comb Id(x) Id(1) Id(x) $T_{1}\quad\forall x:\mbox{num}.\ (\ x+0=x\
)$$T_{2}\quad\forall x:\mbox{real}.\ (\ x\times 1=x\ )$$P\quad\lambda
v_{1}\lambda v_{2}\lambda v_{3}.\ (\ \forall x:v_{1}.\ (\ x=x\ v_{2}\ v_{3}\
))$ttsexp Figure 4: $T_{1}$ and $T_{2}$ form a matching pair of terms with
pattern $P$. Three matching pairs of constants can be induced from this
pattern. We treat equality = and universal quantification ! as logical
constants. Bound variables are assumed to be normalized.

Given two formal libraries $L_{1}$ and $L_{2}$. Let $\\{t_{i}\\}_{1\leq i\leq
m}$ be the collection of all matching pairs of terms, with
$t_{i}=(t_{i1},t_{i2})$, $t_{i1}\in L_{1}$, and $t_{i2}\in L_{2}$. Let
$\\{c_{j}\\}_{1\leq j\leq n}$ be the collection of all matching pairs of
constants, with $c_{j}=(c_{j1},c_{j2})$. Let
$g(x)=x/(x+1):\mathbb{R}^{+}\rightarrow[0,1)$ be a strictly increasing
normalization function. Define an indicator function $\delta(c_{j},t_{i})$ and
set $\delta(c_{j},t_{i})=1$ if constant pair $c_{j}$ can be induced by term
pair $t_{i}$ and $0$ otherwise. Similarity scores between pairs of terms and
pairs of constants can be calculated using the following recurrence relations

$\begin{cases}\text{score}^{0}_{c}\left(c_{j}\right)=1,&j=1,\ldots,n.\\\
\text{score}^{T}_{t}\left(t_{i}\right)=w_{t}\left(t_{i}\right)\sum_{l=1}^{n}\delta(c_{l},t_{i})\,\text{score}^{T-1}_{c}(c_{l}),&i=1,\ldots,m.\\\
\text{score}^{T}_{t}\left(c_{j}\right)=g\left(w_{c}\left(c_{j}\right)\sum_{k=1}^{m}\delta(c_{j},t_{k})\,\text{score}^{T}_{t}(t_{k})\right),&j=1,\ldots,n.\end{cases}$
(1)

where $T=0,1,2,\ldots$ is the iteration step and the weighting functions for
terms $w_{t}\left(t_{i}\right)$ and constants $w_{c}\left(c_{j}\right)$ are
determined using heuristics

$\begin{cases}w_{t}\left(t_{i}\right)=\frac{1}{\ln\left(2+p(t_{i})\right)}\frac{1}{\ln\left(2+q(t_{i})\right)},&i=1,\ldots,m.\\\
w_{c}\left(c_{j}\right)=\frac{1}{\ln\left(2+r(c_{j1})\times
r(c_{j2})\right)},&j=1,\ldots,n.\\\ p\left(t_{i}\right)=\\#\\{\text{\small
term pairs sharing the same pattern as }t_{i}\\},&i=1,\ldots,m.\\\
q\left(t_{i}\right)=\\#\\{\text{\small constant pairs induced by
}t_{i}\\},&i=1,\ldots,m.\\\ r\left(c_{jd}\right)=\\#\\{\text{\small terms
containing }c_{jd}\\},\quad\quad\quad\quad\quad d=1\text{ or
}2,&j=1,\ldots,n.\end{cases}$ (2)

By rewriting equation (1) with respect to
$\text{score}^{T}_{t}\left(c_{j}\right)$ and using properties of $g$,
$\delta$, $w_{t}$, and $w_{c}$, Gauthier proved the convergence of this
scoring algorithm (using monotone convergence theorem coordinate-wise in
$[0,1]^{n}$) [6].

###  5.1 Advantages and Drawbacks of Iterative Pattern Matching

Gauthier’s iterative pattern-matching algorithm is cleverly designed.
Intuitively, the existence of a pattern already indicates a strong correlation
among term pairs, and the existence of constant pairs at corresponding slots
of a pattern already indicates a strong correlation among those constant
pairs; The indicator function $\delta$ transports “similarity awards” among
those pairs, while the weighting functions $w_{t}$ and $w_{c}$ penalize
frequently occurring patterns. Above all, the normalization function $g$
ensures the validity of the scores and is crucial for convergence of the
algorithm. All these components are intricately combined to make the whole
algorithm effective in discovering identical or similar mathematical concepts.

Nevertheless, Gauthier’s algorithm possesses some inherent drawbacks. From the
explainability angle, the balance between the heuristics ($w_{t}$, $w_{c}$ and
their components $p$, $q$, and $r$) in equation (2) and the score accumulation
terms ($\sum$ and $\delta$) in equation (1) is, to our mind, hard to explain
clearly and difficult to readjust. The convergence of the algorithm is mostly
due to the property of the normalization function $g$ but the link between
this convergence and how similarity scores are sorted is weak. The algorithm
works on spaces of similarity scores between matching pairs of terms and
constants, so from its beginning, the information on non-matching terms and
constants is thrown away, losing the possibility to look at the alignment of
different proof assistant libraries holistically.

Comparatively, our approach provides much more flexibility and intuitiveness.
Using distributed representation learning, all the constants are movable
points in Euclidean space and similarity between constants are naturally
described as cosine similarity between their coordinates. By using an
embedding approach, not only the “matching” pairs, but also similarity between
all pairs of constants can be retrieved and their computation is cheap.

From the customizability angle, the components of Gauthier’s algorithm are so
intricately combined that there seems little opportunity to adjust the
algorithm further. In the implementations of both [4] and [6], most of the
extra work is on preprocessing terms using combinations of rewriting rules to
create a varying set of patterns. These rewriting rules include, e.g.
rewriting to conjunctive normal forms, reordering commutative/associative
connectives, substituting subterms with definitions, as well as exposing
various levels of typing information. All these customizations are only
allowed in the preprocessing phase and limited to only employing rewriting
rules. Some of the typing exposure rules require specific knowledge of
representing a library in the tt format. As these rewriting-based
customizations have already been thoroughly investigated in [6], it seems to
us that further investigation along this line is destined to a diminishing
return.

Comparatively, customization of JEFL can be done at different phases of the
full training algorithm, such as the data generation phase, term traversal
phase, model update phase, etc. This multi-level customization can create
combinatorially much more room for parameter-tuning and experimentation.
Moreover, except data generation, all other customizations that are within the
algorithm can be more uniformly done. Specifically, data fields and command
parsing can be added to the args module, and then used at desired places of
the data flow.

From the online-servability angle, despite the fact that Gauthier’s algorithm
is overall fast and effective on small data, it is still quadratic on the size
of the input libraries, since it needs to enumerate all pairs of terms to find
patterns. Being a batch program without a separated and instantaneous
evaluation phase, it is not tempting to integrate the whole algorithm into an
actual interactive proof assistant. Moreover, even if it were to be used as an
online recommender, the only information we can retrieve would be limited to
only the matching pairs.

In JEFL, despite more computations are involved, training is linear with
respect to the size of the corpus. This makes JEFL more suitable for obtaining
similarity measurements on a large training corpus. JEFL provides a clear
separation between a training phase and an evaluation phase. The evaluation
phase is instant once the model is loaded. This allows JEFL to have more
potential to be integrated as a service. In the version of the fasttext commit
used in JEFL, if subword information is disabled, the size of most of the
models dumped after training are less than 5MB. This is a negligible size
comparing to the size of a modern proof assistant.

##  6 Conclusion

In this paper, we identify the need for commonality discovery among formal
libraries. We introduce our data pipeline, especially its preceding works, and
elaborate our internal tt formalism. Methodologically, we describe the
architecture of JEFL and make a series of first experiments to test the
efficacy of our experiment platform and provide a high-level comparative
analysis with the iterative pattern matching algorithm.

###  6.1 Limitations and Future Work

There are a lot of future possibilities in our JEFL platform. Continuing in
the current line of development, we still need to experiment on the other four
libraries and additionally explore similarity discovery of not only constants
but also terms. We could also explore the effect of vector initialization in
our discovery algorithm. To go deeper we could implement custom “dragging” and
“repelling” steps using geometric manipulation and intersperse these custom
steps with SGD updates. We have focused on one pair of libraries, which could
be extended to an embedding of multiple libraries combined. This would provide
further experiment opportunities. We also plan to use the newly discovered
samples from JEFL to do tasks such as conjecturing [7], cross-browsing [25],
and stronger learning for hammers [5]. Last but not least, we hope there could
be use cases to integrate our pipeline into an actual proof assistant and see
improved formalization productivity.

## Acknowledgements

We are largely indebted to Thibault Gauthier for his work on alignments and
the various data exports that we re-use. We thank Josef Urban for the Mizar
export and his invitation to Prague to discuss research. We also thank Tomáš
Mikolov for valuable insights for the current work. This work was supported by
the ERC grant no. 714034 SMART and by the University of Innsbruck PhD
scholarship.

## References

  * [1] Bojanowski, P., Grave, E., Joulin, A., Mikolov, T.: Enriching word vectors with subword information. Transactions of the Association for Computational Linguistics 5, 135–146 (2017), https://aclanthology.org/Q17-1010
  * [2] Bortin, M., Lüth, C.: Structured formal development with quotient types in isabelle/hol. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) Intelligent Computer Mathematics. pp. 34–48. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)
  * [3] Carlisle, D., Davenport, J., Dewar, M., Hur, N., Naylor, W.: Conversion between mathml and openmath. Technical Report 24.969, The OpenMath Society (2001)
  * [4] Gauthier, T., Kaliszyk, C.: Matching concepts across HOL libraries. In: Watt, S., Davenport, J., Sexton, A., Sojka, P., Urban, J. (eds.) Proc. of the 7th Conference on Intelligent Computer Mathematics (CICM’14). LNCS, vol. 8543, pp. 267–281. Springer Verlag (2014). https://doi.org/10.1007/978-3-319-08434-3_20
  * [5] Gauthier, T., Kaliszyk, C.: Sharing HOL4 and HOL Light proof knowledge. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015). LNCS, vol. 9450, pp. 372–386. Springer (2015). https://doi.org/10.1007/978-3-662-48899-7_26
  * [6] Gauthier, T., Kaliszyk, C.: Aligning concepts across proof assistant libraries. J. Symbolic Computation 90, 89–123 (2019). https://doi.org/10.1016/j.jsc.2018.04.005
  * [7] Gauthier, T., Kaliszyk, C., Urban, J.: Initial experiments with statistical conjecturing over large formal corpora. In: Kohlhase, A. (ed.) Work in Progress at the Conference on Intelligent Computer Mathematics 2016 (CICM-WiP 2016). CEUR, vol. 1785, pp. 219–228. CEUR-WS.org (2016)
  * [8] Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formalized Reasoning 3(2), 153–245 (2010). https://doi.org/10.6092/issn.1972-5787/1980, https://doi.org/10.6092/issn.1972-5787/1980
  * [9] Grover, A., Leskovec, J.: node2vec: Scalable feature learning for networks (2016)
  * [10] Hales, T.C.: Introduction to the Flyspeck project. In: Coquand, T., Lombardi, H., Roy, M.F. (eds.) Mathematics, Algorithms, Proofs. pp. 1–11. No. 05021 in Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany, Dagstuhl, Germany (2006), http://drops.dagstuhl.de/opus/volltexte/2006/432
  * [11] Harrison, J.: HOL Light: An overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2009). LNCS, vol. 5674, pp. 60–66. Springer (2009). https://doi.org/10.1007/978-3-642-03359-9_4, https://doi.org/10.1007/978-3-642-03359-9_4
  * [12] Heras, J., Komendantskaya, E.: Proof pattern search in coq/ssreflect. CoRR abs/1402.0081 (2014), http://arxiv.org/abs/1402.0081
  * [13] Huet, G.P., Herbelin, H.: 30 years of research and development around Coq. In: Jagannathan, S., Sewell, P. (eds.) ACM Symposium on Principles of Programming Languages, POPL 2014. pp. 249–250. ACM (2014). https://doi.org/10.1145/2535838.2537848, https://doi.org/10.1145/2535838.2537848
  * [14] Hurd, J.: The opentheory standard theory library. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods. pp. 177–191. Springer Berlin Heidelberg, Berlin, Heidelberg (2011)
  * [15] Joulin, A., Grave, E., Bojanowski, P., Mikolov, T.: Bag of tricks for efficient text classification. In: Proceedings of the 15th Conference of the European Chapter of the Association for Computational Linguistics: Volume 2, Short Papers. pp. 427–431. Association for Computational Linguistics, Valencia, Spain (Apr 2017), https://www.aclweb.org/anthology/E17-2068
  * [16] Kaliszyk, C., Krauss, A.: Scalable LCF-style proof translation. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Proc. of the 4th International Conference on Interactive Theorem Proving (ITP’13). LNCS, vol. 7998, pp. 51–66. Springer (2013), http://dx.doi.org/10.1007/978-3-642-39634-2_7
  * [17] Kaliszyk, C., Urban, J.: Lemma mining over HOL Light. In: LPAR. pp. 503–517 (2013)
  * [18] Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning 53(2), 173–213 (2014). https://doi.org/10.1007/s10817-014-9303-3, http://dx.doi.org/10.1007/s10817-014-9303-3
  * [19] Kaliszyk, C., Urban, J.: HOL(y)Hammer: Online ATP service for HOL Light. Mathematics in Computer Science 9(1), 5–22 (2015). https://doi.org/10.1007/s11786-014-0182-0
  * [20] Keller, C., Werner, B.: Importing hol light into coq. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving. pp. 307–322. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)
  * [21] Klein, G.: Proof engineering considered essential. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM 2014: Formal Methods - 19th International Symposium. LNCS, vol. 8442, pp. 16–21. Springer (2014). https://doi.org/10.1007/978-3-319-06410-9_2, https://doi.org/10.1007/978-3-319-06410-9_2
  * [22] McCarthy, J.: Recursive functions symbolic expressions and their computation by machine, Part I. Communications of the ACM 3(4), 184–195 (Apr 1960). https://doi.org/10/fvx5pv, http://dl.acm.org/citation.cfm?id=367177.367199, zSCC: NoCitationData[s0] Publisher: ACM ISBN: 0001-0782
  * [23] Mikolov, T., Chen, K., Corrado, G., Dean, J.: Efficient estimation of word representations in vector space. In: Bengio, Y., LeCun, Y. (eds.) 1st International Conference on Learning Representations, ICLR 2013, Scottsdale, Arizona, USA, May 2-4, 2013, Workshop Track Proceedings (2013), http://arxiv.org/abs/1301.3781
  * [24] Mikolov, T., Sutskever, I., Chen, K., Corrado, G.S., Dean, J.: Distributed representations of words and phrases and their compositionality. In: Burges, C.J.C., Bottou, L., Welling, M., Ghahramani, Z., Weinberger, K.Q. (eds.) Advances in Neural Information Processing Systems. vol. 26. Curran Associates, Inc. (2013), https://proceedings.neurips.cc/paper/2013/file/9aa42b31882ec039965f3c4923ce901b-Paper.pdf
  * [25] Müller, D., Gauthier, T., Kaliszyk, C., Kohlhase, M., Rabe, F.: Classification of alignments between concepts of formal mathematical systems. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) 10th International Conference on Intelligent Computer Mathematics (CICM’17). LNCS, vol. 10383, pp. 83–98. Springer (2017). https://doi.org/10.1007/978-3-319-62075-6_7
  * [26] Obua, S., Skalberg, S.: Importing hol into isabelle/hol. In: Furbach, U., Shankar, N. (eds.) Automated Reasoning. pp. 298–302. Springer Berlin Heidelberg, Berlin, Heidelberg (2006)
  * [27] Paulson, L.C.: Isabelle: The next seven hundred theorem provers. In: Lusk, E.L., Overbeek, R.A. (eds.) 9th International Conference on Automated Deduction, CADE 1988. LNCS, vol. 310, pp. 772–773. Springer (1988). https://doi.org/10.1007/BFb0012891, https://doi.org/10.1007/BFb0012891
  * [28] Pennington, J., Socher, R., Manning, C.D.: Glove: Global vectors for word representation. In: EMNLP. vol. 14, pp. 1532–1543 (2014)
  * [29] Perozzi, B., Al-Rfou, R., Skiena, S.: Deepwalk: Online learning of social representations. Proceedings of the 20th ACM SIGKDD international conference on Knowledge discovery and data mining (Aug 2014). https://doi.org/10.1145/2623330.2623732, http://dx.doi.org/10.1145/2623330.2623732
  * [30] Rabe, F.: The MMT API: A generic MKM system. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7961, pp. 339–343. Springer (2013). https://doi.org/10.1007/978-3-642-39320-4_25, https://doi.org/10.1007/978-3-642-39320-4_25
  * [31] Řehůřek, R., Sojka, P.: Software Framework for Topic Modelling with Large Corpora. In: Proceedings of the LREC 2010 Workshop on New Challenges for NLP Frameworks. pp. 45–50. ELRA, Valletta, Malta (May 2010), http://is.muni.cz/publication/884893/en
  * [32] So, C.M., Watt, S.M.: On the conversion between content mathml and openmath. In: Proc. of the Conference on the Communicating Mathematics in the Digital Era (CMDE 2006). pp. 169–182 (2006)
  * [33] Sutcliffe, G.: The TPTP world - infrastructure for automated reasoning. In: LPAR (Dakar). pp. 1–12 (2010)
  * [34] Urban, J.: MoMM - fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. on Artificial Intelligence Tools 15(1), 109–130 (2006), http://ktiml.mff.cuni.cz/~urban/MoMM/momm.ps
  * [35] Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning 37(1-2), 21–43 (2006). https://doi.org/10.1007/s10817-006-9032-3, https://doi.org/10.1007/s10817-006-9032-3