15319 LABEL:LastPageFeb. 26, 2018Aug. 21, 2019

The research described in this paper is supported by JSPS KAKENHI Grant Number
17K00011, JSPS Core to Core Program and FWF (Austrian Science Fund) projects
P27528, T789 and P27502. A preliminary version of this paper appeared in the
proceedings of the 2nd International Conference on Formal Structures for
Computation and Deduction [HMSW17] and we also incorporated parts of our
preceding work [HMS14].

# Abstract Completion, Formalized

Nao Hirokawaa  aSchool of Information Science, JAIST, Nomi, Japan
<EMAIL_ADDRESS>,  Aart Middeldorpb  bDepartment of Computer Science,
University of Innsbruck, Innsbruck, Austria
<EMAIL_ADDRESS>,  Christian
Sternagelb  and  Sarah Winklerb

###### Abstract.

Completion is one of the most studied techniques in term rewriting and
fundamental to automated reasoning with equalities. In this paper we present
new correctness proofs of abstract completion, both for finite and infinite
runs. For the special case of ground completion we present a new proof based
on random descent. We moreover extend the results to ordered completion, an
important extension of completion that aims to produce ground-complete
presentations of the initial equations. We present new proofs concerning the
completeness of ordered completion for two settings. Moreover, we revisit and
extend results of Métivier concerning canonicity of rewrite systems. All
proofs presented in the paper have been formalized in Isabelle/HOL.

###### Key words and phrases:

term rewriting, abstract completion, ordered completion, canonicity,
Isabelle/HOL

##  1\. Introduction

Reasoning with equalities is pervasive in computer science and mathematics,
and has consequently been one of the main research areas of automated
deduction. Indeed completion as introduced by Knuth and Bendix [KB70] has
evolved into a fundamental technique whose ideas appear throughout automated
reasoning whenever equalities are present. Many variants of the original
calculus have since been proposed.

Bachmair, Dershowitz, and Hsiang [BDH86] recast completion procedures as
inference systems. This style of presentation, _abstract completion_ , has
become the standard to describe completion procedures and _proof orders_ the
accompanying tool to establish correctness [BDH86, BDP89, B91], that is, that
under certain conditions, exhaustive application of the inference rules
results in a terminating and confluent rewrite system whose equational theory
is equivalent to the initial set of equations.

In this paper we present new, modular correctness proofs, not relying on proof
orders, for five abstract completion systems presented in the literature.
Here, we use _modular_ in the following sense: Proof orders have to be
powerful (and thus complex) enough to cover all intermediate results (that is,
proof orders are a _global_ method), while for our new proofs, we _locally_
apply well-founded induction with an order that is just strong enough for the
current intermediate result. All proofs are fully formalized in Isabelle/HOL.
First, we consider finite (KBf) and infinite (KBi) runs of classical Knuth-
Bendix completion [KB70]. These two settings demand different proofs since in
the latter case the inference system exhibits a stronger side condition. While
our correctness proof for KBf relies on a new notion we dub _peak
decreasingness_ , for the case of KBi we employ a simpler version of this
criterion called _source decreasingness_. To enhance applicability by covering
efficient implementations, our proofs support the critical pair criterion
known as primality [KMN88].

The relevance of infinite runs is illustrated by the following example.

Consider the set of equations
$\mathcal{E}=\\{\mathsf{aba}\approx\mathsf{bab}\\}$ of the three-strand
positive braid monoid. Kapur and Narendran [KN85] proved that $\mathcal{E}$
admits no _finite_ complete presentation. However, taking the Knuth-Bendix
order [KB70] with $\mathsf{a}$ and $\mathsf{b}$ of weight $1$ and
$\mathsf{a}>\mathsf{b}$ in the precedence, completion produces in the limit
the following infinite complete presentation of $\mathcal{E}$

$\displaystyle\\{\mathsf{aba}\to\mathsf{bab}\\}\cup\\{\mathsf{ab}^{n}\mathsf{ab}\to\mathsf{babba}^{n-1}\mid
n\geqslant 2\\}$

which can be used to decide the validity problem for $\mathcal{E}$.111Burckel
[B01] constructed a complete rewrite system consisting of four rules with an
additional symbol, which is no longer a complete presentation of $\mathcal{E}$
but can be also used to decide the validity problem for $\mathcal{E}$.

Completion procedures, when successful, produce a complete system. Natural
questions include whether such systems are unique and whether all complete
systems for a given set of equations can be obtained by completion. For
canonical systems, which are complete systems that satisfy an additional
normalization requirement, Métivier [M83] obtained interesting results. In
this paper we revisit and extend his work.

A special case of KBf that is known to be decidable is the completion of
ground systems [S93]. We present new correctness and completeness proofs for
the corresponding inference system KBg, based on the recent notion of random
descent [vOT16].

On a given set of input equalities, Knuth-Bendix completion can behave in
three different ways: it may (1) succeed to compute a complete system in
finitely many steps, (2) fail due to unorientable equalities, or (3)
continuously compute approximations of a complete system without ever
terminating. As a remedy to problem (2), ordered completion was developed by
Bachmair, Dershowitz, and Plaisted [BDP89]. Ordered completion never fails and
can produce a ground-complete system in the limit. Although the price to be
paid is that the resulting system is in general only complete on ground terms,
this is actually sufficient for many applications in theorem proving.
Refutational theorem proving [BDP89] owes its semi-decidability to the
unfailing nature of ordered completion. Again employing peak decreasingness,
we obtain a new correctness proof of ordered completion (KBo). Next, we turn
to completeness results for ordered completion, that is, to sufficient
criteria for an ordered completion procedure to produce a complete system. We
first reprove the case of a total reduction order, which assumes a slightly
stronger notion of simplifiedness than the original result [BDP89] though.
Then we consider the completeness result for linear completion (KBl) due to
Devie [D91].

For easy reference, Table 1 provides pointers to the main definitions and
results we present in this paper.

Table 1. Roadmap. | KBf | KBg | KBi | KBo | KBl
---|---|---|---|---|---
inference system | LABEL:def:KBf | LABEL:def:KBg | LABEL:def:KBi | LABEL:def:KBo | LABEL:def:KBl
fairness | LABEL:def:KBf_fairness | – | LABEL:def:KBi_fairness | LABEL:def:KBo_fairness | LABEL:def:KBl_fairness
correctness | LABEL:thm:KBf_correctness | LABEL:thm:KBg_correctness | LABEL:thm:KBi_correctness | LABEL:thm:complete_presentation_okb | LABEL:thm:KBl_correctness
|  |  |  | LABEL:thm:KBo_correctness |
completeness | – | LABEL:thm:KBg_completeness | – | LABEL:thm:KBo_completeness | LABEL:thm:KBl_completeness

The remainder of this paper is organized as follows. We present required
preliminaries in Section 2, followed by the abstract confluence criteria of
peak and source decreasingness, as well as a fairly detailed analysis of
critical pairs. In Section LABEL:sec:finite_runs we recall the inference rules
for (abstract) Knuth-Bendix completion and present our formalized correctness
proof for finite runs. In Section LABEL:sec:canonicity we present our results
on canonical systems and normalization equivalence. We discuss ground
completion in Section LABEL:sec:ground_completion. Infinite runs are the
subject of Section LABEL:sec:infinite_runs and in Section
LABEL:sec:ordered_completion we extend our correctness results to ordered
completion. Completeness of ordered completion is the topic of Section
LABEL:sec:completeness. We conclude in Section LABEL:sec:conclusion with a few
suggestions for future research.

Our formalizations are part of the _Isabelle Formalization of Rewriting_
IsaFoR [TS09]222http://cl-informatik.uibk.ac.at/isafor version 2.37. Below we
list the relevant Isabelle theory files grouped by their subdirectories inside
IsaFoR:

thys/Abstract_Completion/
---
Abstract_Completion.thy
Completion_Fairness.thy
CP.thy
Ground_Completion.thy
Peak_Decreasingness.thy
Prime_Critical_Pairs.thy
thys/Confluence_and_Completion/
---
Ordered_Completion.thy
thys/Normalization_Equivalence/
Encompassment.thy
Normalization_Equivalence.thy

In the remainder we provide hyperlinks (marked by check-square-o) to an HTML
rendering of our formalization. Moreover, whenever we say that a proof is
“formalized,” what we mean is that it is“formalized in Isabelle/HOL.” And when
we “present a formalized proof,” we give a textual representation of a
formalized proof.

This paper and the accompanying formalization are substantially extended and
revised versions of some of our previous work we published in the ITP [HMS14]
and FSCD [HMSW17] conferences. The former presented a new correctness proof
for finite runs of Knuth-Bendix completion. Its modular design separates
concerns rather than relying on a single proof order, thus rendering it more
formalization friendly. In revised form, these results are included in Section
LABEL:sec:finite_runs. The FSCD contribution extended this novel proof
approach to both infinite runs and ordered completion (see Sections
LABEL:sec:infinite_runs and LABEL:sec:ordered_completion). It moreover
incorporated canonicity results (Section LABEL:sec:canonicity). In addition to
these results we present new and formalized proofs of correctness and
completeness of ground completion (Section LABEL:sec:ground_completion), as
well as completeness of ordered completion for two different cases (Section
LABEL:sec:completeness). At the end of each section, we remark on the novelty
of the respective results and their proofs.

##  2\. Preliminaries

We assume familiarity with the basic notions of abstract rewrite systems, term
rewrite systems, and completion [B91, BN98], but nevertheless shortly
recapitulate terminology and notation that we use in the remainder.

###  2.1. Rewrite Systems

For an arbitrary binary relation
$\mathchoice{\xrightarrow[\alpha]{}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}$,
we write $\mathchoice{\xleftarrow[\alpha]{}}{\mathrel{\hskip
13.58234pt\hskip-13.58234pt\hbox{$\vphantom{\leftarrow}{}_{\vphantom{\alpha}}$}\hskip-13.58234pt\hbox{$\vphantom{\leftarrow}{}_{\alpha}$}{\leftarrow}}}{\mathrel{\hskip
9.55882pt\hskip-9.55882pt\hbox{$\vphantom{\leftarrow}{}_{\vphantom{\alpha}}$}\hskip-9.55882pt\hbox{$\vphantom{\leftarrow}{}_{\alpha}$}{\leftarrow}}}{\mathrel{\hskip
7.5588pt\hskip-7.5588pt\hbox{$\vphantom{\leftarrow}{}_{\vphantom{\alpha}}$}\hskip-7.5588pt\hbox{$\vphantom{\leftarrow}{}_{\alpha}$}{\leftarrow}}}$,
$\smash{\xleftrightarrow[\smash{\raisebox{2.0pt}{$\scriptstyle\alpha$}}]{}}$,
$\mathchoice{\xrightarrow[\alpha]{=}}{\rightarrow_{\alpha}^{=}}{\rightarrow_{\alpha}^{=}}{\rightarrow_{\alpha}^{=}}$,
$\mathchoice{\xrightarrow[\alpha]{+}}{\rightarrow_{\alpha}^{+}}{\rightarrow_{\alpha}^{+}}{\rightarrow_{\alpha}^{+}}$,
and
$\mathchoice{\xrightarrow[\alpha]{*}}{\rightarrow_{\alpha}^{*}}{\rightarrow_{\alpha}^{*}}{\rightarrow_{\alpha}^{*}}$
to denote its _inverse_ , its _symmetric closure_ , its _reflexive closure_ ,
its _transitive closure_ , and its _reflexive transitive closure_ ,
respectively. The reflexive, transitive, and symmetric closure
$\smash{\xleftrightarrow[\smash{\raisebox{2.0pt}{$\scriptstyle\alpha$}}]{*}}$
of
$\mathchoice{\xrightarrow[\alpha]{}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}$
is called _conversion_ , and a sequence of the form
$c_{0}\mathrel{\smash{\xleftrightarrow[\smash{\raisebox{2.0pt}{$\scriptstyle\alpha$}}]{}}}c_{1}\mathrel{\smash{\xleftrightarrow[\smash{\raisebox{2.0pt}{$\scriptstyle\alpha$}}]{}}}\cdots\mathrel{\smash{\xleftrightarrow[\smash{\raisebox{2.0pt}{$\scriptstyle\alpha$}}]{}}}c_{n}$
is referred to as a conversion between $c_{0}$ and $c_{n}$ (of length $n$).
For a binary relation $R$ without arrow notation, we also write $R^{-1}$ for
its _inverse_ and $R^{\pm}$ for its _symmetric closure_ $R\cup R^{-1}$. We
further use $\downarrow_{\alpha}$ as abbreviation for the _joinability
relation_
$\mathchoice{\xrightarrow[\alpha]{*}}{\rightarrow_{\alpha}^{*}}{\rightarrow_{\alpha}^{*}}{\rightarrow_{\alpha}^{*}}\cdot\mathchoice{\xleftarrow[\alpha]{*}}{\mathrel{\hskip
13.58234pt\hskip-13.58234pt\hbox{$\vphantom{\leftarrow}{}_{\vphantom{\alpha}}^{*}$}\hskip-13.58234pt\hbox{$\vphantom{\leftarrow}{}_{\alpha}^{\vphantom{*}}$}{\leftarrow}}}{\mathrel{\hskip
9.55882pt\hskip-9.55882pt\hbox{$\vphantom{\leftarrow}{}_{\vphantom{\alpha}}^{*}$}\hskip-9.55882pt\hbox{$\vphantom{\leftarrow}{}_{\alpha}^{\vphantom{*}}$}{\leftarrow}}}{\mathrel{\hskip
7.5588pt\hskip-7.5588pt\hbox{$\vphantom{\leftarrow}{}_{\vphantom{\alpha}}^{*}$}\hskip-7.5588pt\hbox{$\vphantom{\leftarrow}{}_{\alpha}^{\vphantom{*}}$}{\leftarrow}}}$,
where from here on $\cdot$ denotes relation composition. If
$a\mathchoice{\xrightarrow[\alpha]{}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}b$
for no $b$ then we say that $a$ is a _(
$\mathchoice{\xrightarrow[\alpha]{}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}$-)normal
form_. The set of all normal forms of a given relation
$\mathchoice{\xrightarrow[\alpha]{}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}$
is denoted by
$\mathsf{NF}({\mathchoice{\xrightarrow[\alpha]{}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}})$.
By
$a\mathchoice{\xrightarrow[\alpha]{!}}{\rightarrow_{\alpha}^{!}}{\rightarrow_{\alpha}^{!}}{\rightarrow_{\alpha}^{!}}b$
we abbreviate
${a\mathchoice{\xrightarrow[\alpha]{*}}{\rightarrow_{\alpha}^{*}}{\rightarrow_{\alpha}^{*}}{\rightarrow_{\alpha}^{*}}b}\land{b\in\mathsf{NF}({\mathchoice{\xrightarrow[\alpha]{}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}})}$
and we call $b$ a _normal form of $a$_. Given two binary relations
$\mathchoice{\xrightarrow[\alpha]{}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}$
and
$\mathchoice{\xrightarrow[\beta]{}}{\rightarrow_{\beta}}{\rightarrow_{\beta}}{\rightarrow_{\beta}}$,
we use
$\mathchoice{\xrightarrow[\alpha]{}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}/\mathchoice{\xrightarrow[\beta]{}}{\rightarrow_{\beta}}{\rightarrow_{\beta}}{\rightarrow_{\beta}}$
as shorthand for the _relative rewrite relation_
$\mathchoice{\xrightarrow[\beta]{*}}{\rightarrow_{\beta}^{*}}{\rightarrow_{\beta}^{*}}{\rightarrow_{\beta}^{*}}\cdot\mathchoice{\xrightarrow[\alpha]{}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}\cdot\mathchoice{\xrightarrow[\beta]{*}}{\rightarrow_{\beta}^{*}}{\rightarrow_{\beta}^{*}}{\rightarrow_{\beta}^{*}}$.
An _abstract rewrite system_ (ARS for short) $\mathcal{A}$ is a set $A$, the
carrier, equipped with a binary relation $\to$. Sometimes we partition the
binary relation into parts according to a set $I$ of indices (or labels). Then
we write $\mathcal{A}=\langle
A,{\\{{\mathchoice{\xrightarrow[\alpha]{}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}}\\}}_{\alpha\in
I}\rangle$ where we denote the part of the relation with label $\alpha$ by
$\mathchoice{\xrightarrow[\alpha]{}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}$,
that is,
${\to}=\bigcup~{}\\{{\mathchoice{\xrightarrow[\alpha]{}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}{\rightarrow_{\alpha}}}\mid\alpha\in
I\\}$.

We assume a given signature $\mathcal{F}$ and a set of variables
$\mathcal{V}$. The set of terms built up from $\mathcal{F}$ and $\mathcal{V}$
is denoted by $\mathcal{T}(\mathcal{F},\mathcal{V})$, while
$\mathcal{T}(\mathcal{F})$ denotes the set of ground terms. _Positions_ are
strings of positive integers which are used to address subterms. The set of
positions in a term $t$ is denoted by $\mathcal{P}\mathsf{os}(t)$. The subset
consisting of the positions addressing function symbols in $t$ is denoted by
$\mathcal{P}\mathsf{os}_{\mathcal{F}}(t)$ whereas
$\mathcal{P}\mathsf{os}_{\mathcal{V}}(t)=\mathcal{P}\mathsf{os}(t)-\mathcal{P}\mathsf{os}_{\mathcal{F}}(t)$
is the set of variable positions in $t$. We write $p\leqslant q$ if $p$ is a
prefix of $q$ and $p\parallel q$ if neither $p\leqslant q$ nor $q\leqslant p$.
If $p\leqslant q$ then the unique position $r$ such that $pr=q$ is denoted by
$q\backslash p$. A _substitution_ is a mapping $\sigma$ from variables to
terms such that its domain $\\{x\in\mathcal{V}\mid\sigma(x)\neq x\\}$ is
finite. Applying a substitution $\sigma$ to a term $t$ is written $t\sigma$. A
variable substitution is a substitution from $\mathcal{V}$ to $\mathcal{V}$
and a _renaming_ is a bijective variable substitution. A term $s$ is a
_variant_ of a term $t$ if $s=t\sigma$ for some renaming $\sigma$. A pair of
terms $(s,t)$ is sometimes considered an _equation_ , then we write $s\approx
t$, and sometimes a _(rewrite) rule_ , then we write $s\to t$. In the latter
case we assume the _variable condition_ , that is, that the left-hand side $s$
is not a variable and that variables of the right-hand side $t$ are all
contained in $t$. A set $\mathcal{E}$ of equations is called an _equational
system_ (ES for short) and a set $\mathcal{R}$ of rules a _term rewrite
system_ (TRS for short). Sets of pairs of terms $\mathcal{E}$ induce a
_rewrite relation_
$\mathchoice{\xrightarrow[\mathcal{E}]{}}{\rightarrow_{\mathcal{E}}}{\rightarrow_{\mathcal{E}}}{\rightarrow_{\mathcal{E}}}$
by closing their components under contexts and substitutions. A rewrite step
$s\to_{\mathcal{E}}t$ at a position $p\in\mathcal{P}\mathsf{os}(s)$ is called
_innermost_ and denoted by $s\xrightarrow{\smash{\mathsf{i}}}_{\mathcal{E}}t$
if no proper subterm of $s|_{p}$ is reducible in $\mathcal{E}$. The
_equational theory_ induced by $\mathcal{E}$ consists of all pairs of terms
$s$ and $t$ such that $s\xleftrightarrow{}^{*}_{\mathcal{E}}t$. If $\ell\to r$
is a rewrite rule and $\sigma$ is a renaming then the rewrite rule
$\ell\sigma\to r\sigma$ is a _variant_ of $\ell\to r$. A TRS is said to be
_variant-free_ if it does not contain rewrite rules that are variants of each
other.

Two terms $s$ and $t$ are called _literally similar_ , written $s\doteq t$, if
$s\sigma=t$ and $s=t\tau$ for some substitutions $\sigma$ and $\tau$. Two TRSs
$\mathcal{R}_{1}$ and $\mathcal{R}_{2}$ are called _literally similar_ ,
denoted by $\mathcal{R}_{1}\doteq\mathcal{R}_{2}$, if every rewrite rule in
$\mathcal{R}_{1}$ has a variant in $\mathcal{R}_{2}$ and vice versa. The
following result is folklore; we formalized the non-trivial proof.

######  Lemma 1.

Two terms $s$ and $t$ are variants of each other if and only if $s\doteq t$.
check-square-o

We say that $s$ _encompasses_ $t$, written
$s\mathrel{\makebox[0.0pt]{\makebox[9.0pt][r]{\raise
0.9pt\hbox{$\cdot$}}}{\unrhd}}t$, whenever $s=C[t\sigma]$ for some context $C$
and substitution $\sigma$. _Proper encompassment_ is defined by
${\mathrel{\ooalign{\hss$\rhd$\hss\cr\kern 1.72218pt\raise
0.0pt\hbox{\scalebox{1.0}{$\cdot$}}}}}={\mathrel{\makebox[0.0pt]{\makebox[9.0pt][r]{\raise
0.9pt\hbox{$\cdot$}}}{\unrhd}}\setminus\mathrel{\reflectbox{$\mathrel{\makebox[0.0pt]{\makebox[9.0pt][r]{\raise
0.9pt\hbox{$\cdot$}}}{\unrhd}}$}}}$ and known to be well-founded. The identity
${\mathrel{\makebox[0.0pt]{\makebox[9.0pt][r]{\raise
0.9pt\hbox{$\cdot$}}}{\unrhd}}}={\mathrel{\ooalign{\hss$\rhd$\hss\cr\kern
1.72218pt\raise 0.0pt\hbox{\scalebox{1.0}{$\cdot$}}}}}\cup{\doteq}$ is well-
known. For a well-founded order $>$, we write $>_{\mathsf{mul}}$ to denote its
_multiset extension_ and $>_{\mathsf{lex}}$ to denote its _lexicographic
extension_ as defined by Baader and Nipkow [BN98].

A TRS $\mathcal{R}$ is _terminating_ if $\to_{\mathcal{R}}$ is well-founded,
and _weakly normalizing_ if every term has a normal form. It is
_(ground-)confluent_ if
$s\mathrel{{\vphantom{\mathrel{\leftarrow}}{}^{\hbox{\hskip
7.07785pt\hbox{$\scriptstyle*$}}}_{\hbox{\hskip
7.64723pt\hbox{$\scriptstyle\mathcal{R}$}}}}{\mathrel{\leftarrow}}}\cdot\to_{\mathcal{R}}^{*}t$
implies
$s\to_{\mathcal{R}}^{*}\cdot\mathrel{{\vphantom{\mathrel{\leftarrow}}{}^{\hbox{\hskip
7.07785pt\hbox{$\scriptstyle*$}}}_{\hbox{\hskip
7.64723pt\hbox{$\scriptstyle\mathcal{R}$}}}}{\mathrel{\leftarrow}}}t$ for all
(ground) terms $s$ and $t$. It is _(ground-)complete_ if it is terminating and
(ground) confluent. We say that $\mathcal{R}$ is a _complete presentation_ of
an ES $\mathcal{E}$ if $\mathcal{R}$ is complete and
${\xleftrightarrow{}^{*}_{\mathcal{R}}}={\xleftrightarrow{}^{*}_{\mathcal{E}}}$.
A TRS $\mathcal{R}$ is _left-reduced_ if
$\ell\in\mathsf{NF}(\mathcal{R}\setminus\\{\ell\to r\\})$ for every rewrite
rule $\ell\to r$ in $\mathcal{R}$, and _right-reduced_ if
$r\in\mathsf{NF}(\mathcal{R})$ for every rewrite rule $\ell\to r$ in
$\mathcal{R}$. A _reduced_ TRS is left- and right-reduced. A reduced complete
TRS is called _canonical_.

We make use of the following result due to Bachmair and Dershowitz [BD86],
where _quasi-commutation_ of $R$ over $S$ means that the inclusion $S\cdot
R\subseteq R\cdot{(R\cup S)}^{*}$ holds.

######  Lemma 2.

Let $R$ and $S$ be binary relations.

  1. (1)

If $R$ quasi-commutes over $S$ then well-foundedness of
$\mathrel{R}/\mathrel{S}$ and $R$ coincide. check-square-o

  2. (2)

If $\mathrel{R}/\mathrel{S}$ and $S$ are well-founded then $R\cup S$ is well-
founded. check-square-o

######  Lemma 3.

If $R$ is a well-founded rewrite relation then
$\mathrel{(R\cup{\mathrel{\ooalign{\hss$\rhd$\hss\cr\kern 1.72218pt\raise
0.0pt\hbox{\scalebox{1.0}{$\cdot$}}}}})}/\mathrel{\mathrel{\makebox[0.0pt]{\makebox[9.0pt][r]{\raise
0.9pt\hbox{$\cdot$}}}{\unrhd}}}$ is well-founded. check-square-o

######  Proof 2.1.

First we show the inclusion
${\mathrel{\makebox[0.0pt]{\makebox[9.0pt][r]{\raise
0.9pt\hbox{$\cdot$}}}{\unrhd}}\cdot\mathrel{R}}\subseteq{\mathrel{R}\cdot\mathrel{\makebox[0.0pt]{\makebox[9.0pt][r]{\raise
0.9pt\hbox{$\cdot$}}}{\unrhd}}}$. Suppose
$s\mathrel{\makebox[0.0pt]{\makebox[9.0pt][r]{\raise
0.9pt\hbox{$\cdot$}}}{\unrhd}}t\mathrel{R}u$. So $s=C[t\sigma]$ for some
context $C$ and substitution $\sigma$. Because $R$ is closed under contexts
and substitutions, $s\mathrel{R}C[u\sigma]$. Moreover,
$C[u\sigma]\mathrel{\makebox[0.0pt]{\makebox[9.0pt][r]{\raise
0.9pt\hbox{$\cdot$}}}{\unrhd}}u$. This establishes the inclusion, and we
conclude that $R$ (quasi-)commutes over
$\mathrel{\makebox[0.0pt]{\makebox[9.0pt][r]{\raise
0.9pt\hbox{$\cdot$}}}{\unrhd}}$. Because $R$ is well-founded, it follows from
Lemma


#  Testing CPT Invariance by High-Precision Comparisons
of Fundamental Properties of Protons and Antiprotons at BASE

E.J. Wursten  1 M.J. Borchert  1,2,3 J.A. Devlin  1,4 S.R. Erlewein  1,4,5 M.
Fleck  1,6 J.A. Harrington  1,5 J.I. Jäger  4,5 B.M. Latacz  1 P. Micke  1,4,5
G. Umbrazunas  1,7 F. Abbass  8 M. Bohman  1,5 S. Kommu  8 D. Popper  8 M.
Wiesinger  1,5 C. Will  5 H. Yildiz  8 K. Blaum  5 Y. Matsuda  6 A. Mooser  5
C. Ospelkaus  2,3 A. Soter  7 W. Quint  9 J. Walz  8 Y. Yamazaki  1 C. Smorra
1,8 and S. Ulmer1 1Ulmer Fundamental Symmetries Laboratory, RIKEN, Wako,
351-0198, Japan
2Institut für Quantenoptik, Leibniz Universität Hannover, 30167 Hannover,
Germany
3Physikalisch-Technische Bundesanstalt, 38116 Braunschweig, Germany
4CERN, 1217 Meyrin, Switzerland
5Max-Planck-Institut für Kernphysik, 69117, Heidelberg, Germany
6Graduate School of Arts and Sciences, University of Tokyo, Tokyo 153-0041,
Japan
7Eidgenössische Technische Hochschule Zürich, 8092 Zürich, Switzerland
8Institut für Physik, Johannes Gutenberg-Universität, 55099 Mainz, Germany
9GSI-Helmholtzzentrum für Schwerionenforschung GmbH, 64291 Darmstadt, Germany

###### Abstract

The BASE collaboration at the Antiproton Decelerator facility of CERN compares
the fundamental properties of protons and antiprotons using advanced Penning-
trap systems. In previous measurement campaigns, we measured the magnetic
moments of the proton and the antiproton, reaching (sub-)parts-in-a-billion
fractional uncertainty. In the latest campaign, we have compared the proton
and antiproton charge-to-mass ratios with a fractional uncertainty of 16 parts
in a trillion. In this contribution, we give an overview of the measurement
campaign, and detail how its results are used to constrain nine spin-
independent coefficients of the Standard-Model Extension in the proton and
electron sector.

##  1 Introduction

The Baryon Antibaryon Symmetry Experiment (BASE) collaboration is dedicated to
the study of protons and antiprotons with ultrahigh precision. Comparisons of
fundamental properties of such matter–antimatter conjugates provide tests of
CPT invariance, one of the cornerstones of the Standard Model of Particle
Physics. The BASE collaboration operates several Penning-trap experiments at
different locations. At CERN’s Antiproton Decelerator facility, primarily two
types of measurements take place. Firstly, the charge-to-mass ratio of the
antiproton is compared (in situ) to that of the negatively-charged hydrogen
ion, currently reaching a fractional uncertainty of 16 parts per trillion.[1]
Secondly, the magnetic moment of the antiproton is measured. The magnetic
moment of the proton is measured at a dedicated experiment in Mainz,[2]
reaching a fractional uncertainty of 300 parts per trillion, which is 5 times
more precise than the antiproton experiment.[3] These comparisons of
fundamental properties can be interpreted in terms of the Standard-Model
Extension (SME),[4] yielding constraints on different types of coefficients of
the model in the proton (and electron) sector.

##  2 Comparing antiproton and proton charge-to-mass ratios

The principle of an antiproton-to-proton charge-to-mass ratio comparison at
BASE is the measurement of the cyclotron frequency
$\omega_{\mathrm{c}}{=}qB/m$ of the two particles while stored in a Penning
trap. Here, $B$ is the magnetic field of the Penning trap and $(q/m)$ the
charge-to-mass ratio of the trapped particle. The cyclotron frequency
$\omega_{\mathrm{c}}$ is inferred from the three eigenmotions of the trapped
particle, which are detected by monitoring the image currents induced in the
electrodes of the Penning trap.

To suppress systematic effects related to residual magnetic-field gradients
and trap-polarity inversion,[6] the antiproton is not directly compared to the
proton, but to the negatively charged hydrogen ion H-. The mass of the H- ion
is given by

$m_{\text{H}^{-}}=m_{\mathrm{p}}\left(1+2\frac{m_{e}}{m_{\mathrm{p}}}-\frac{E_{\mathrm{b}}}{m_{\mathrm{p}}c^{2}}-\frac{E_{\mathrm{a}}}{m_{\mathrm{p}}c^{2}}+\frac{\alpha_{\text{H}^{-}}B^{2}}{m_{\mathrm{p}}c^{2}}\right)=m_{\mathrm{p}}R.$
(1)

Here, $m_{e}$ is the electron mass, $E_{\mathrm{b}}$ is the binding energy of
the electron in hydrogen, $E_{\mathrm{a}}$ is the afﬁnity energy of the second
electron, and the last term accounts for the electrical polarizability
$\alpha_{\text{H}^{-}}$ of the hydrogen ion. Measurements of the cyclotron
frequencies of the antiproton $\bar{\text{p}}$ and the H- ion in the same
magnetic field $B$ give access to the dimensionless ratio of charge-to-mass
ratios

$R_{\bar{\mathrm{p}},\mathrm{H}^{-}}=\frac{\omega_{\mathrm{c},\bar{\mathrm{p}}}}{\omega_{\mathrm{c},\mathrm{H}^{-}}}=\frac{(q/m)_{\bar{\mathrm{p}}}}{(q/m)_{\mathrm{H}^{-}}}\,.$
(2)

Assuming that CPT invariance holds, the theoretical prediction is that
$R_{\bar{\mathrm{p}},{\text{H}^{-}}}$ is identical to
$R=1{.}001\,089\,218\,753\,80(3)$.[5]

Figure 1: (a) Illustration of the BASE multi-Penning-trap system. (b)
Configurations of the Penning-trap potentials for cyclotron-frequency
measurements of H- (top) and $\bar{\text{p}}$ (bottom).

In practice, the cyclotron frequency-measurements on $\bar{\text{p}}$ and H-
are not done simultaneously in the same Penning trap, but one after the other,
shuttling the particles into and out of a dedicated measurement trap. A sketch
of the multi-Penning-trap system that is used in these experiments is shown in
Fig. 1(a). A cloud of H- and $\bar{\text{p}}$ delivered by the Antiproton
Decelerator is stored in the reservoir trap on the left. A single ion of each
species is extracted from the reservoir trap and can be stored in different
park electrodes along the trap stack on the right or shuttled into the
measurement trap for a cyclotron-frequency measurement. Figure 1(b) shows the
Penning-trap-potential configurations that are used to perform cyclotron-
frequency measurements on H- (top) and $\bar{\text{p}}$ (bottom). The
measurement of one individual cyclotron frequency takes about $110\,$s.
Together with the required particle exchange, the determination of a single
frequency ratio $R_{\bar{\mathrm{p}},\mathrm{H}^{-}}$ takes about 4 min. We
have accumulated a total of about 24 000 such cyclotron-frequency-ratio
measurements using different techniques during the last measurement campaign,
spanning 1.5 years of sampling time. The resulting ratio of antiproton-to-
proton charge-to-mass ratios is

$\frac{(q/m)_{\bar{\mathrm{p}}}}{(q/m)_{\mathrm{p}}}=R_{\bar{\text{p}},\text{H}^{-}}/R=-1.000\,000\,000\,003\,(16)\,,\cite[cite]{[\@@bibref{Number}{Borchert2022}{}{}]}$
(3)

constituting an improvement of a factor of 4 compared to the previous
measurement campaign.[6] This improvement was possible due to several upgrades
of the apparatus, eliminating previous systematic limitations and considerably
improving the stability of the experiment.

##  3 Constraining SME coefficients with BASE

The results of a charge-to-mass ratio comparison can be interpreted as a test
of Lorentz and CPT symmetry, as outlined in detail in Ref. [Ding2020].
Applying the SME framework to the Penning trap, the energy levels
$E_{n,s}^{w}$ and corresponding energy shifts ${\delta}E_{n,s}^{w}$ due to the
SME terms in the Lagrangian can be calculated for a trapped particle. Here,
$n=0,1,2,...$ indicates the relativistic Landau level number, $s=\pm 1$ the
spin state relative to the magnetic field $B$ and $w$ the species of the
particle. The cyclotron frequencies that we measure in our experiment can be
expressed as differences between energy levels
$\hbar\omega_{\mathrm{c},w}^{s}=E_{1,s}^{w}-E_{0,s}^{w}$, giving the
dependence of the measured cyclotron frequencies on the SME coefficients, as
laid out in Ref. [Ding2020]. Do note that we distinguish the spin state $s$ in
our definition of the cyclotron frequency $\omega_{\mathrm{c},w}^{s}$, as both
spin orientations are possible during our frequency measurements in the
Penning trap. The shift of the antiproton cyclotron frequency is then written
as
$\delta\omega_{\mathrm{c},\bar{\mathrm{p}}}^{s}={\delta}E_{1,s}^{\bar{\mathrm{p}}}-{\delta}E_{0,s}^{\bar{\mathrm{p}}}$,
whereas the shift of the $\mathrm{H}^{-}$ frequency can be approximated as

$\delta\omega_{\mathrm{c},\mathrm{H}^{-}}=\delta\omega_{\mathrm{c},\mathrm{p}}^{s}+\left(\delta\omega_{\mathrm{c},e}^{\uparrow}+\delta\omega_{\mathrm{c},e}^{\downarrow}\right),$
(4)

where the last term takes into account that the electron pair is in a singlet
spin state. The charge-to-mass ratio comparison of Eq. (3) can then be
interpreted as follows:

$\frac{(|q|/m)_{\bar{\mathrm{p}}}}{(|q|/m)_{\mathrm{p}}}-1=\frac{\omega_{\mathrm{c},\bar{\mathrm{p}}}}{R\,\omega_{\mathrm{c},\mathrm{H}^{-}}}-1=\frac{\delta\omega_{\mathrm{c},\bar{\mathrm{p}}}^{s1}-R\,\delta\omega_{\mathrm{c},\mathrm{p}}^{s2}-R\,\left(\delta\omega_{\mathrm{c},e}^{\uparrow}+\delta\omega_{\mathrm{c},e}^{\downarrow}\right)}{R\,\omega_{\mathrm{c},\mathrm{H}^{-}}},$
(5)

yielding the following limit for the time-averaged component of the model

$\hbar|\delta\omega_{\mathrm{c},\bar{\mathrm{p}}}^{s1}-R\,\delta\omega_{\mathrm{c},\mathrm{p}}^{s2}-R\,\left(\delta\omega_{\mathrm{c},e}^{\uparrow}+\delta\omega_{\mathrm{c},e}^{\downarrow}\right)|<1.96\times
10^{-27}\,\mathrm{GeV}.$ (6)

After transforming from the local laboratory frame to the standard Sun-
centered inertial reference frame,[4] we can use Eq. (6) to individually
constrain the nine spin-independent SME coefficients summarized in Table 3.

Individual constraints on spin-independent electron and proton coefficients of
the SME.  Coefficient Limit (68% C.L.) $|\tilde{c}_{e}^{XX}|$,
$|\tilde{c}_{e}^{YY}|$ $<7.79\cdot 10^{-15}$ $|\tilde{c}_{e}^{ZZ}|$
$<4.96\cdot 10^{-15}$
$|\tilde{c}_{\mathrm{p}}^{XX}|,|\tilde{c}_{\mathrm{p}}^{*XX}|$,
$|\tilde{c}_{\mathrm{p}}^{YY}|,|\tilde{c}_{\mathrm{p}}^{*YY}|$ $<2.86\cdot
10^{-11}$ $|\tilde{c}_{\mathrm{p}}^{ZZ}|,|\tilde{c}_{\mathrm{p}}^{*ZZ}|$
$<1.82\cdot 10^{-11}$

Since the spin state of the used antiprotons and hydrogen ions is not known a
priori nor measured, we cannot constrain the spin-dependent coefficients
contained within $\delta\omega_{\mathrm{c},\bar{\mathrm{p}}}^{s}$ and
$\delta\omega_{\mathrm{c},\mathrm{p}}^{s}$. Similarly, due to the singlet
state of the electron pair, all spin-dependent electron coefficients cancel
out and cannot be constrained either.

##  4 Outlook

We can study the temporal variations of the ratio of antiproton-to-proton
charge-to-mass ratios at harmonics of the sidereal day and the sidereal year
as we have a sampling period of 4 min and taken data for 1.5 years. Such an
analysis is currently ongoing and will significantly expand the number of SME
coefficients that can be constrained.

In addition, we are currently working towards a ten-fold improved measurement
of the antiproton magnetic moment, which will allow us to improve constraints
on another twelve coefficients of the SME. Furthermore, there are plans to
integrate the spin-detection techniques developed for the current magnetic-
moment campaign into the next charge-to-mass ratio campaign. Knowing the
antiproton and H- spin state would give us access to the spin-dependent proton
coefficients listed in Ref. [Ding2020].

## Acknowledgments

We acknowledge technical support by CERN. We acknowledge financial support by
the RIKEN EEE pioneering project funding, the RIKEN SPDR and JRA program, the
Max Planck Society, the European Union (FunI-832848, STEP-852818), CRC 1227
“DQ-mat”(DFG 274200144), the Cluster of Excellence “Quantum Frontiers” (DFG
390837967), AVA-721559, the CERN fellowship program, and the Helmholtz-
Gemeinschaft. This work was supported by the Max-Planck–RIKEN–PTB Center for
Time, Constants, and Fundamental Symmetries (C-TCFS).

## References

  * [1] M.J. Borchert et al., Nature 601, 53 (2022).
  * [2] G. Schneider et al., Science 358, 1081 (2017).
  * [3] C. Smorra et al., Nature 550, 371 (2017).
  * [4] Data Tables for Lorentz and CPT Violation, V.A. Kostelecký and N. Russell, 2023 edition, arXiv:0801.0287v16.
  * [5] S. Alighanbari et al., Nature 581, 152 (2020).
  * [6] S. Ulmer et al., Nature 524, 196 (2015).
  * [7] Y. Ding and M.F. Rawnak, Phys. Rev. D 102, 056009 (2020).