0.83328ptt^{\prime}\theta\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,_{p}\mathrel{\dot{\approx}}s^{\prime}\theta}$

where $\mathcalx{G}^{-1}(D\theta)=D=D^{\prime}\mathrel{\lor}t\approx
t^{\prime}$ and
$\mathcalx{G}^{-1}(C\theta)=C=C^{\prime}\mathrel{\lor}s\mathrel{\dot{\approx}}s^{\prime}$.
Suppose that the position $p$ exists as a green subterm in $s$. Let $u$ be the
green subterm of $s$ at that position and $\sigma=\operatorname{mgu}(t,u)$
(which exists since $\theta$ is a unifier). If the variable condition holds
for $C$, $t$, $t^{\prime}$, $u$, and $\sigma$, then $\iota$ is liftable.

###### Proof.

The inference conditions of $\iota$ can be lifted to $D$ and $C$. That
$t\theta\approx t^{\prime}\theta$ is strictly eligible in $D\theta$ w.r.t.
$\mathit{GHSel}$ implies that $t\approx t^{\prime}$ is strictly eligible in
$D$ w.r.t. $\sigma$ and $\mathit{HSel}$. If
$s\theta\mathrel{\dot{\approx}}s^{\prime}\theta$ is (strictly) eligible in
$C\theta$ w.r.t. $\mathit{GHSel}$, then $s\mathrel{\dot{\approx}}s^{\prime}$
is (strictly) eligible in $C$ w.r.t. $\sigma$ and $\mathit{HSel}$. Moreover,
$D\theta\not\succeq C\theta$ implies $D\not\succeq C$, $t\theta\not\prec
t^{\prime}\theta$ implies $t\not\prec t^{\prime}$, and $s\theta\not\prec
s^{\prime}\theta$ implies $s\not\prec s^{\prime}$.

By assumption, $p$ is a position of $s$ and the variable condition holds.
Thus, the following inference $\iota^{\prime}\in\mathit{HInf}$ is applicable:

$\prftree[r]{\small{\textsc{Sup}}}{D^{\prime}\mathrel{\lor}t\approx
t^{\prime}\quad
C^{\prime}\mathrel{\lor}s\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328ptu\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,_{p}\mathrel{\dot{\approx}}s^{\prime}}{\operatorname{\mathcalx{pure}}((D^{\prime}\mathrel{\lor}C^{\prime}\mathrel{\lor}s\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328ptt^{\prime}\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,_{p}\mathrel{\dot{\approx}}s^{\prime})\sigma)}$

By Lemma 19.3, we have
$(\mathit{preconcl}(\iota^{\prime}))\theta=\mathit{concl}(\iota)$. Hence,
$\iota$ is the $\theta$-ground instance of $\iota^{\prime}$ and is therefore
liftable. ∎

The other Sup inferences might not be liftable, but they are redundant:

######  Lemma .

Let $\iota\in\mathit{GHInf}^{\mathit{GHSel}}$ be a Sup inference

$\prftree[r]{\small{\textsc{Sup}}}{D^{\prime}\theta\mathrel{\lor}t\theta\approx
t^{\prime}\theta\quad
C^{\prime}\theta\mathrel{\lor}s\theta\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328ptt\theta\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,_{p}\mathrel{\dot{\approx}}s^{\prime}\theta}{D^{\prime}\theta\mathrel{\lor}C^{\prime}\theta\mathrel{\lor}s\theta\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328ptt^{\prime}\theta\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,_{p}\mathrel{\dot{\approx}}s^{\prime}\theta}$

where $\mathcalx{G}^{-1}(D\theta)=D=D^{\prime}\mathrel{\lor}t\approx
t^{\prime}$ and
$\mathcalx{G}^{-1}(C\theta)=C=C^{\prime}\mathrel{\lor}s\mathrel{\dot{\approx}}s^{\prime}$.
Suppose that Lemma 19.3 does not apply. This could be either because the
position $p$ is below a variable in $s$ or because the variable condition does
not hold. Then
$\iota\in\mathit{GHRed}_{\mathrm{I}}^{\mathit{GHSel}}(\mathcalx{G}(N))$.

###### Proof.

By the definition of $\mathit{GHRed}_{\mathrm{I}}$, to show
$\iota\in\mathit{GHRed}_{\mathrm{I}}^{\mathit{GHSel}}(\mathcalx{G}(N))$, it
suffices to prove that $\\{E\in\mathcalx{F}(\mathcalx{G}(N))\mid
E\prec\mathcalx{F}(C\theta)\\}\models\mathcalx{F}(\mathit{concl}(\iota))$. Let
$\mathcal{I}$ be a first-order model of all
$E\in\mathcalx{F}(\mathcalx{G}(N))$ with $E\prec\mathcalx{F}(C\theta)$. We
must show that $\mathcal{I}\models\mathcalx{F}(\mathit{concl}(\iota))$. If
$\mathcal{I}\models\mathcalx{F}(D^{\prime}\theta)$, this is obvious. So we
further assume that $\mathcal{I}\not\models\mathcalx{F}(D^{\prime}\theta)$.
Since $D\theta\prec C\theta$ by the Sup inference conditions, it follows that
$\mathcal{I}\models\mathcalx{F}(t\theta\approx t^{\prime}\theta)$. By
congruence, it suffices to show $\mathcal{I}\models\mathcalx{F}(C\theta)$. We
proceed by a case distinction on the two possible reasons why Lemma 19.3 does
not apply:

Case 1: The position $p$ is below a variable in $s$. Then $t\theta$ is a
proper green subterm of $x\theta$ and hence a green subterm of
$x\theta\;\bar{w}$ for any arguments $\bar{w}$. Let $v$ be the term that we
obtain by replacing $t\theta$ by $t^{\prime}\theta$ in $x\theta$ at the
relevant position. It follows from our assumptions about $\mathcal{I}$ that
$\mathcal{I}\models\mathcalx{F}(t\theta\approx t^{\prime}\theta)$, and by
congruence, $\mathcal{I}\models\mathcalx{F}(x\theta\;\bar{w}\approx
v\;\bar{w})$ for any arguments $\bar{w}$. Hence,
$\mathcal{I}\models\mathcalx{F}(C\theta)$ if and only if
$\mathcal{I}\models\mathcalx{F}(C\\{x\mapsto v\\}\theta)$. By the inference
conditions we have $t\theta\succ t^{\prime}\theta$, which implies
$\mathcalx{F}(C\theta)\succ\mathcalx{F}(C\\{x\mapsto v\\}\theta)$ by
compatibility with green contexts. Therefore, we have
$\mathcal{I}\models\mathcalx{F}(C\\{x\mapsto v\\}\theta)$ and hence
$\mathcal{I}\models\mathcalx{F}(C\theta)$.

Case 2: The variable condition does not hold. In the extensional calculi, it
follows that $u$ has a variable head and jells with $t\approx t^{\prime}$. By
Definition 12.1, this means that $u$, $t$, and $t^{\prime}$ have the following
form: $u=x\;\bar{v}_{n}$ for some variable $x$ and a tuple of terms
$\bar{v}_{n}$ of length $n\geq 0$; $t=\tilde{t}\;\bar{x}_{n}$ and
$t^{\prime}=\tilde{t}\kern 0.83328pt^{\prime}\>\bar{x}_{n}$, where
$\bar{x}_{n}$ are variables that do not occur elsewhere in $D.$

For the intensional calculi, we have $u\in\mathcalx{V}$. Thus, $u$, $t$, and
$t^{\prime}$ can be written in the same form as described above for the
extensional calculi, with $n=0$.

Case 2.1 (Purifying calculi): First, we assume that $x$ occurs only with
arguments $\bar{v}_{n}$ in $C.$ For the intensional calculus, this must be the
case because $n=0$ and hence $x$ can only occur without arguments by the
definition of $\operatorname{\operatorname{\mathcalx{pure}}}$ and the literal
selection restriction. Define a substitution $\theta^{\prime}$ by
$x\theta^{\prime}=\tilde{t}\kern 0.83328pt^{\prime}\theta$ and
$y\theta^{\prime}=y\theta$ for other variables $y$. Since $t\theta\succ
t^{\prime}\theta$ by the inference conditions, we have $C\theta\succ
C\theta^{\prime}$. Moreover, $C\theta^{\prime}\in\mathcalx{G}(N)$. Then
$\mathcal{I}\models\mathcalx{F}(C\theta)$ by congruence, because
$\mathcal{I}\models\mathcalx{F}(C\theta^{\prime})$ and
$\mathcal{I}\models\mathcalx{F}(t\theta\approx t^{\prime}\theta)$.

Now we assume that $x$ occurs with arguments other than $\bar{v}_{n}$ in $C.$
This can only happen in the extensional calculus and by the selection
restrictions, $s\theta\mathrel{\dot{\approx}}s^{\prime}\theta$ must not be
selected in $C\theta$. Therefore, $s\theta$ is the maximal term in $C\theta$.
Then $s\not=x$ and hence $\bar{v}_{n}\not=\varepsilon$ because otherwise
$s\theta=x\theta$ would be smaller than the applied occurrence of $x\theta$ in
$C\theta$.

Define a substitution $\theta^{\prime\prime}$ such that
$x\theta^{\prime\prime}=\tilde{t}\kern 0.83328pt^{\prime}\theta$,
$y\theta^{\prime\prime}=\tilde{t}\kern 0.83328pt^{\prime}\theta$ for other
variables $y$ if $y\theta=s\theta$ and $C$ contains the literal $x\not\approx
y$, and $y\theta^{\prime\prime}=y\theta$ otherwise.

We show that $C\theta\succ C\theta^{\prime\prime}$ by proving that no literal
of $C\theta^{\prime\prime}$ is larger than the maximal literal
$s\theta\mathrel{\dot{\approx}}s^{\prime}\theta$ of $C\theta$ and that
$s\theta\mathrel{\dot{\approx}}s^{\prime}\theta$ appears more often in
$C\theta$ than in $C\theta^{\prime\prime}$.

For a literal of the form $x\not\approx y$, we have
$x\theta^{\prime\prime}\prec s\theta$ and $y\theta^{\prime\prime}\prec
s\theta$. For literals that are not of this form, by the definition of
$\operatorname{\operatorname{\mathcalx{pure}}}$ in the extensional calculus,
$x$ occurs always with arguments $\bar{v}_{n}$. Hence these literals are equal
or smaller in $C\theta^{\prime\prime}$ than in $C\theta$, because
$x\theta^{\prime\prime}\>\bar{v}_{n}\prec x\theta\;\bar{v}_{n}$ and
$y\theta^{\prime\prime}\preceq y\theta$. Therefore, no literal of
$C\theta^{\prime\prime}$ is larger than the maximal literal
$s\theta\mathrel{\dot{\approx}}s^{\prime}\theta$ of $C\theta$. Moreover, these
inequalities show that every occurrence of
$s\theta\mathrel{\dot{\approx}}s^{\prime}\theta$ in $C\theta^{\prime\prime}$
corresponds to an occurrence of
$s\theta\mathrel{\dot{\approx}}s^{\prime}\theta$ in $C\theta$ that corresponds
to a literal in $C$ without the variable $x$. Since at least one occurrence of
$s\theta\mathrel{\dot{\approx}}s^{\prime}\theta$ in $C\theta$ corresponds to a
literal in $C$ containing $x$,
$s\theta\mathrel{\dot{\approx}}s^{\prime}\theta$ appears more often in
$C\theta$ than in $C\theta^{\prime\prime}$. This concludes the argument that
$C\theta\succ C\theta^{\prime\prime}$. It follows that
$\mathcal{I}\models\mathcalx{F}(C\theta^{\prime\prime})$.

We need to show that $\mathcal{I}\models\mathcalx{F}(C\theta)$. There is a
PosExt inference from $D$ to
$D^{\prime}\mathrel{\lor}\tilde{t}\approx\tilde{t}\kern 0.83328pt^{\prime}$.
This inference is in $\mathit{HRed}_{\mathrm{I}}(N)$ because $N$ is saturated.
Therefore, $D^{\prime}\theta\mathrel{\lor}\tilde{t}\theta\approx\tilde{t}\kern
0.83328pt^{\prime}\theta$ is in
$\mathcalx{G}(N)\mathrel{\cup}\mathit{GHRed}_{\mathrm{C}}(\mathcalx{G}(N))$.
It follows that
$\mathcal{I}\models\mathcalx{F}(D^{\prime}\theta\mathrel{\lor}\tilde{t}\theta\approx\tilde{t}\kern
0.83328pt^{\prime}\theta)$ because this clause is smaller than
$\mathcalx{F}(D^{\prime}\theta)$ and hence smaller than
$\mathcalx{F}(C\theta)$. Since $\mathcalx{F}(D^{\prime}\theta)$ is false in
$\mathcal{I}$, we have
$\mathcal{I}\models\mathcalx{F}(\tilde{t}\theta\approx\tilde{t}\kern
0.83328pt^{\prime}\theta)$.

For every literal of the form $x\not\approx y$, where $y\theta=s\theta$, the
variable $y$ can only occur without arguments in $C$ because of the maximality
of $s\theta$. We distinguish two cases. If for every literal of the form
$x\not\approx y$ where $y\theta=s\theta$, we have
$\mathcal{I}\models\mathcalx{F}(y\theta^{\prime\prime}\approx y\theta)$, then
$\mathcal{I}\models\mathcalx{F}(C\theta)$ by congruence. If for some literal
of the form $x\not\approx y$ where $y\theta=s\theta$, we have
$\mathcal{I}\models\mathcalx{F}(y\theta^{\prime\prime}\not\approx y\theta)$,
then $\mathcal{I}\models\mathcalx{F}(y\theta\not\approx x\theta)$ because
$y\theta^{\prime\prime}=\tilde{t}\kern 0.83328pt^{\prime}\theta$,
$\mathcal{I}\models\mathcalx{F}(\tilde{t}\kern
0.83328pt^{\prime}\theta\approx\tilde{t}\theta)$, and
$\tilde{t}\theta=x\theta$. Hence a literal of $\mathcalx{F}(C\theta)$ is true
in $\mathcal{I}$ and therefore $\mathcal{I}\models C\theta$.

Case 2.2 (Nonpurifying calculi): Since the variable condition does not hold,
we have $C\theta\succeq C^{\prime\prime}\theta$, where
$C^{\prime\prime}=C\\{x\mapsto\tilde{t}\kern 0.83328pt^{\prime}\\}$. We cannot
have $C\theta=C^{\prime\prime}\theta$ because
$x\theta=\tilde{t}\theta\neq\tilde{t}\kern 0.83328pt^{\prime}\theta$ and $x$
occurs in $C$. Hence, we have $C\theta\succ C^{\prime\prime}\theta$.

By the definition of $\mathcal{I}$, $C\theta\succ C^{\prime\prime}\theta$
implies $\mathcal{I}\models\mathcalx{F}(C^{\prime\prime}\theta)$. We will use
equalities that are true in $\mathcal{I}$ to rewrite $\mathcalx{F}(C\theta)$
into $\mathcalx{F}(C^{\prime\prime}\theta)$, which implies
$\mathcal{I}\models\mathcalx{F}(C\theta)$ by congruence.

By saturation of $N$, for any well-typed $m$-tuple of fresh variables
$\bar{z}$, we can use a PosExt with premise $D$ (if $n>m$) or ArgCong
inference with premise $D$ (if $n<m$) or using $D$ itself (if $n=m$) to show
that $\mathcalx{G}(D^{\prime}\lor\tilde{t}\;\bar{z}\approx\tilde{t}\kern
0.83328pt^{\prime}\>\bar{z})\subseteq\mathcalx{G}(N)\cup\mathit{GHRed}_{\mathrm{C}}(\mathcalx{G}(N))$.
Hence,
$D^{\prime}\theta\mathrel{\lor}\tilde{t}\theta\;\bar{u}\approx\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u}$ is in
$\mathcalx{G}(N)\cup\mathit{GHRed}_{\mathrm{C}}(\mathcalx{G}(N))$ for any
ground arguments $\bar{u}$.

We observe that whenever $\tilde{t}\theta\;\bar{u}$ and $\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u}$ are smaller than the maximal term of
$C\theta$ for some arguments $\bar{u}$, we have

$\mathcal{I}\models\mathcalx{F}(\tilde{t}\theta\;\bar{u})\approx\mathcalx{F}(\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u})$

To show this, we assume that $\tilde{t}\theta\;\bar{u}$ and $\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u}$ are smaller than the maximal term of
$C\theta$ and we distinguish two cases: If $t\theta$ is smaller than the
maximal term of $C\theta$, all terms in $D^{\prime}\theta$ are smaller than
the maximal term of $C\theta$ and hence
$D^{\prime}\theta\lor\tilde{t}\theta\;\bar{u}\approx\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u}\prec C\theta$. If, on the other hand,
$t\theta$ is equal to the maximal term of $C\theta$,
$\tilde{t}\theta\;\bar{u}$ and $\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u}$ are smaller than $t\theta$. Hence
$\tilde{t}\theta\;\bar{u}\approx\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u}\prec t\theta\approx t^{\prime}\theta$ and
$D^{\prime}\theta\lor\tilde{t}\theta\;\bar{u}\approx\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u}\prec D\theta\prec C\theta$. In both cases,
since $\mathcalx{F}(D^{\prime}\theta)$ is false in $\mathcal{I}$ by
assumption,
$\mathcal{I}\models\mathcalx{F}(\tilde{t}\theta\;\bar{u})\approx\mathcalx{F}(\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u})$.

We proceed by a case distinction on whether $s\theta$ appears in a selected or
in a maximal literal of $C\theta$. In both cases we provide an algorithm that
establishes the equivalence of $C\theta$ and $C^{\prime\prime}\theta$ via
rewriting using (19.3). This might seem trivial at first sight, but we can
only use the equations (19.3) if $\tilde{t}\theta\;\bar{u}$ and
$\tilde{t}\kern 0.83328pt^{\prime}\theta\;\bar{u}$ are smaller than the
maximal term of $C\theta$. Moreover, $\bar{u}$ might itself contain positions
where we want to rewrite, so the order of rewriting matters.

Case 2.2.1: $s\theta$ is the maximal side of a maximal literal of $C\theta$.
Then, since $C\theta\succ C^{\prime\prime}\theta$, every term in $C\theta$ and
in $C^{\prime\prime}\theta$ is smaller than or equal to $s\theta$. Let $C_{0}$
and $\tilde{C}_{0}$ be the clauses resulting from rewriting
$\mathcalx{F}(t\theta)\mathrel{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color<EMAIL_ADDRESS>to0.0pt{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}$\blacksquare$\hss}\kern-3.87495pt}\joinrel{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rightarrow}}\mathcalx{F}(t^{\prime}\theta)$
wherever possible in $\mathcalx{F}(C\theta)$ and
$\mathcalx{F}(C^{\prime\prime}\theta)$, respectively. Since
$\mathcalx{F}(t\theta)$ is a subterm of $\mathcalx{F}(s\theta)$, now every
term in $C_{0}$ and $\tilde{C}_{0}$ is strictly smaller than
$\mathcalx{F}(s\theta)$.

We define $C_{1},C_{2},\dots$ inductively as follows: Given $C_{i}$, choose a
subterm of the form $\mathcalx{F}(\tilde{t}\theta\;\bar{u})$ where
$\tilde{t}\theta\;\bar{u}\succ\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u}$ or of the form $\mathcalx{F}(\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u})$ where $\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u}\succ\tilde{t}\theta\;\bar{u}$. Let $C_{i+1}$
be the clause resulting from rewriting that subterm
$\mathcalx{F}(\tilde{t}\theta\;\bar{u})$ to $\mathcalx{F}(\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u})$ or that subterm
$\mathcalx{F}(\tilde{t}\kern 0.83328pt^{\prime}\theta\;\bar{u})$ to
$\mathcalx{F}(\tilde{t}\theta\;\bar{u})$ in $C_{i}$, depending on which term
was chosen. Analogously, we define $\tilde{C}_{1},\tilde{C}_{2},\dots$ by
applying the same algorithm to $\tilde{C}_{0}$. In both cases, the process
terminates because $\succ$ is compatible with green contexts and well founded.
Let $C_{*}$ and $\tilde{C}_{*}$ be the respective final clauses.

The algorithm preserves the invariant that every term in $C_{i}$ and
$\tilde{C}_{i}$ is strictly smaller than $s\theta$. By congruence via (†),
applied at every step of the algorithm, we know that $C_{*}$ and
$\mathcalx{F}(C\theta)$ are equivalent in $\mathcal{I}$ and that
$\tilde{C}_{*}$ and $\mathcalx{F}(C^{\prime\prime}\theta)$ are equivalent in
$\mathcal{I}$ as well.

We show that $C_{*}=\tilde{C}_{*}$. Assume that $C_{*}\not=\tilde{C}_{*}$. The
algorithm preserves a second invariant, namely that $\mathcalx{F}^{-1}(C_{i})$
and $\mathcalx{F}^{-1}(\tilde{C}_{j})$ are equal except for positions where
one contains $\tilde{t}\theta$ and the other one contains $\tilde{t}\kern
0.83328pt^{\prime}\theta$. Consider a deepest position where
$\mathcalx{F}^{-1}(C_{*})$ and $\mathcalx{F}^{-1}(\tilde{C}_{*})$ are
different. The respective position in $C_{*}$ and $\tilde{C}_{*}$ then
contains $\mathcalx{F}(\tilde{t}\theta\;\bar{u})$ and
$\mathcalx{F}(\tilde{t}\kern 0.83328pt^{\prime}\theta\;\bar{u})$ or vice
versa. The arguments $\bar{u}$ must be equal because we consider a deepest
position. But then $\tilde{t}\theta\;\bar{u}\succ\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u}$ or
$\tilde{t}\theta\;\bar{u}\prec\tilde{t}\kern
0.83328pt^{\prime}\theta\;\bar{u}$, which is impossible since the algorithm
terminated in $C_{*}$ and $\tilde{C}_{*}$. This shows that
$C_{*}=\tilde{C}_{*}$. Hence $\mathcalx{F}(C\theta)$ and
$\mathcalx{F}(C^{\prime\prime}\theta)$ are equivalent, which proves
$\mathcal{I}\models\mathcalx{F}(C\theta)$.

Case 2.2.2: $s\theta$ is the maximal side of a selected literal of $C\theta$.
Then, by the selection restrictions, $x$ cannot be the head of a maximal
literal of $C.$

At every position where $x\;\bar{u}$ occurs in $C$ with some (or no) arguments
$\bar{u}$, we rewrite $(\tilde{t}\;\bar{u})\theta$ to $(\tilde{t}\kern
0.83328pt^{\prime}\>\bar{u})\theta$ in $C\theta$ if
$(\tilde{t}\;\bar{u})\theta\succ(\tilde{t}\kern
0.83328pt^{\prime}\>\bar{u})\theta$. We start with the innermost occurrences
of $x$, so that the order of the two terms at one step does not change by
later rewriting. Analogously, at every position where $x\;\bar{u}$ occurs in
$C$ with some (or no) arguments $\bar{u}$, we rewrite $(\tilde{t}\kern
0.83328pt^{\prime}\>\bar{u})\theta$ to $(\tilde{t}\;\bar{u})\theta$ in
$C^{\prime\prime}\theta$ if $(\tilde{t}\kern
0.83328pt^{\prime}\>\bar{u})\theta\succ(\tilde{t}\;\bar{u})\theta$, again
starting with the innermost occurrences.

We never rewrite at the top level of the maximal term of $C\theta$ or
$C^{\prime\prime}\theta$ because $x$ cannot be the head of a maximal literal
of $C.$ The two resulting clauses are identical because $C\theta$ and
$C^{\prime\prime}\theta$ only differ at positions where $x$ occurs in $C.$ The
rewritten terms are all smaller than the maximal term of $C\theta$. With
(19.3), this implies that $\mathcal{I}\models\mathcalx{F}(C\theta)$ by
congruence. ∎

With these properties of our inference systems in place, the saturation
framework’s lifting theorem (Theorem 19.3) guarantees static and dynamic
refutational completeness of $\mathit{HInf}$ w.r.t.
$\mathit{HRed}_{\mathrm{I}}$. However, this theorem gives us refutational
completeness w.r.t. the Herbrand entailment $\models{G}$, defined as
$N_{1}\models{G}N_{2}$ if $\mathcalx{G}(N_{1})\models\mathcalx{G}(N_{2})$,
whereas our semantics is Tarski entailment $\models$, defined as $N_{1}\models
N_{2}$ if any model of $N_{1}$ is a model of $N_{2}$. The following lemma
repairs this mismatch:

######  Lemma .

For $N\subseteq\mathcalx{C}_{\mathrm{H}}$, we have $N\models{G}\bot$ if and
only if $N\models\bot$.

###### Proof.

By Lemma 12.3, any model of $N$ is also a model of $\mathcalx{G}(N)$—i.e.,
$N\not\models\bot$ implies $N\not\models{G}\bot$. For the other direction, we
need to show that $N\not\models{G}\bot$ implies $N\not\models\bot$. Assume
that $N\not\models{G}\bot$—i.e., $\mathcalx{G}(N)\not\models\bot$. Then there
is a model $\mathcal{I}$ of $\mathcalx{G}(N)$. We must show that there exists
a model of $N$—i.e., $N\not\models\bot$. Let $\mathcal{I}^{\prime}$ be an
interpretation derived from $\mathcal{I}$ by removing all universes that are
not the denotation of a type in $\mathcalx{Ty}_{\mathrm{GH}}$ and removing all
domain elements that are not the denotation of a term in
$\mathcalx{T}_{\mathrm{GH}}$, making $\mathcal{I}^{\prime}$ term-generated.
Clearly, in our clausal logic, this leaves the denotations of terms and the
truth of ground clauses unchanged. Thus,
$\mathcal{I}^{\prime}\models\mathcalx{G}(N)$. We will show that
$\mathcal{I}^{\prime}\models N$. Let $C\in N$. We want to show that $C$ is
true in $\mathcal{I}^{\prime}$ for all valuations $\xi$. Fix a valuation
$\xi$. By construction, for each variable $x$, there exists a ground term
$s_{x}$ such that $\smash{\llbracket
s_{x}\rrbracket_{\mathcal{I}^{\prime}}^{\smash{}}}=\xi(x)$. Let $\rho$ be the
substitution that maps every free variable $x$ in $C$ to $s_{x}$. Then
$\xi(x)=\smash{\llbracket
s_{x}\rrbracket_{\mathcal{I}^{\prime}}^{\smash{}}}=\smash{\llbracket
x\rho\rrbracket_{\mathcal{I}^{\prime}}^{\smash{}}}$ for all $x$. By treating
the type variables of $C$ in the same way, we can also achieve that
$\xi(\alpha)=\smash{\llbracket\alpha\rho\rrbracket_{\mathcal{I}^{\prime}}^{\smash{}}}$
for all $x$. By Lemma 12.3, $\smash{\llbracket
t\rho\rrbracket_{\mathcal{I}^{\prime}}^{\smash{}}}=\smash{\llbracket
t\rrbracket_{\mathcal{I}^{\prime}}^{\smash{\xi}}}$ for all terms $t$ and
$\smash{\llbracket\tau\kern-0.83328pt\rho\rrbracket_{\mathcal{I}^{\prime}}^{\smash{}}}=\smash{\llbracket\tau\rrbracket_{\mathcal{I}^{\prime}}^{\smash{\xi}}}$
for all types $\tau$. Hence, $C\rho$ and $C$ have the same truth value in
$\mathcal{I}^{\prime}$ for $\xi$. Since
$\mathcal{I}^{\prime}\models\mathcalx{G}(N)$, $C\rho$ is true in
$\mathcal{I}^{\prime}$ and thus $C$ is true in $\mathcal{I}^{\prime}$ as well.
∎

######  Theorem  (Static refutational completeness).

The inference system $\mathit{HInf}$ is statically refutationally complete
w.r.t. $(\mathit{HRed}_{\mathrm{I}},{\mathit{HRed}_{\mathrm{C}}})$. That
means, if $N\subseteq\mathcalx{C}_{\mathrm{H}}$ is a clause set saturated
w.r.t. $\mathit{HInf}$ and $\mathit{HRed}_{\mathrm{I}}$, then we have
$N\models\bot$ if and only if $\bot\in N$.

###### Proof.

We apply Theorem 19.3. By Theorem 19.2, $\mathit{GHInf}^{\mathit{GHSel}}$ is
statically refutationally complete for all
$\mathit{GHSel}\in\mathcalx{G}(\mathit{HSel})$. By Lemmas 19.3, 19.3, and
19.3, for every saturated $N\subseteq\mathcalx{C}_{\mathrm{H}}$, there exists
a selection function $\mathit{GHSel}\in\mathcalx{G}(\mathit{HSel})$ such that
all inferences $\iota\in\mathit{GHInf}^{\mathit{GHSel}}$ with
$\mathit{prems}(\iota)\in\mathcalx{G}(N)$ either are
$\mathcalx{G}^{\mathit{GHSel}}$-ground instances of $\mathit{HInf}$-inferences
from $N$ or belong to
$\smash{\mathit{GHRed}_{\mathrm{I}}^{\mathit{GHSel}}(\mathcalx{G}(N))}$.

Theorem 19.3 implies that if $N\subseteq\mathcalx{C}_{\mathrm{H}}$ is a clause
set saturated w.r.t. $\mathit{HInf}$ and $\mathit{HRed}_{\mathrm{I}}$, then
$N\models{G}\bot$ if and only if $\bot\in N$. By Lemma 19.3, this also holds
for the Tarski entailment $\models$. That is, if
$N\subseteq\mathcalx{C}_{\mathrm{H}}$ is a clause set saturated w.r.t.
$\mathit{HInf}$ and $\mathit{HRed}_{\mathrm{I}}$, then $N\models\bot$ if and
only if $\bot\in N$. ∎

From static refutational completeness, we can easily derive dynamic
refutational completeness.

######  Theorem  (Dynamic refutational completeness).

The inference system $\mathit{HInf}$ is dynamically refutationally complete
w.r.t. $(\mathit{HRed}_{\mathrm{I}},{\mathit{HRed}_{\mathrm{C}}})$, as defined
in Definition 17.

###### Proof.

By Theorem 17 of Waldmann et al., this follows from Theorem 19.3 and Lemma
19.3. ∎

##  20\. Implementation

Zipperposition [Cru15, Cru17] is an open source superposition-based theorem
prover written in OCaml.111https://github.com/sneeuwballen/zipperposition It
was initially designed for polymorphic first-order logic with equality, as
embodied by TPTP TF1 [BP13]. We will refer to this implementation as
Zipperposition’s first-order mode. Later, Cruanes extended the prover with a
pragmatic higher-order mode with support for $\lambda$-abstractions and
extensionality, without any completeness guarantees. We have now also
implemented complete $\lambda$-free higher-order modes based on the four
calculi described in this article.

The pragmatic higher-order mode provided a convenient basis to implement our
calculi. It employs higher-order term and type representations and orders. Its
ad hoc calculus extensions are similar to our calculi. They include an
ArgCong-like rule and a PosExt-like rule, and Sup inferences are performed
only at green subterms. One of the bugs we found during our implementation
work occurred because argument positions shift when applied variables are
instantiated. We resolved this by numbering argument positions in terms from
right to left.

To implement the $\lambda$-free higher-order mode, we restricted the
unification algorithm to non-$\lambda$-abstractions. To satisfy the
requirements on selection, we avoid selecting literals that contain higher-
order variables. To comply with our redundancy notion, we disabled rewriting
of nongreen subterms. To improve term indexing of higher-order terms, we
replaced the imperfect discrimination trees by fingerprint indices [Sch12]. To
speed up the computation of the Sup conditions, we omit the condition
$C\sigma\not\preceq D\sigma$ in the implementation, at the cost of performing
some additional inferences.

For the purifying calculi, we implemented purification as a simplification
rule. This ensures that it is applied aggressively on all clauses, whether
initial clauses from the problem or clauses produced during saturation, before
any inferences are performed.

For the nonpurifying calculi, we added the possibility to perform Sup
inferences at variable positions. This means that variables must be indexed as
well. In addition, we modified the variable condition. Depending on the term
ordering, it may be expensive or even impossible to decide whether there
exists a grounding substitution $\theta$ with $t\sigma\theta\succ
t^{\prime}\sigma\theta$ and $C\sigma\theta\prec C^{\prime\prime}\sigma\theta$.
We overapproximate the condition as follows: (1) check whether $x$ appears
with different arguments in the clause $C$; (2) use a term-order-specific
algorithm to determine whether there might exist a grounding substitution
$\theta$ and terms $\bar{u}$ such that $t\sigma\theta\succ
t^{\prime}\sigma\theta$ and $t\sigma\theta\;\bar{u}\prec
t^{\prime}\sigma\theta\;\bar{u}$; and (3) check whether $C\sigma\not\succeq
C^{\prime\prime}\sigma$. If these three conditions apply, we conclude that
there might exist a ground substitution $\theta$ witnessing nonmonotonicity.

For the extensional calculi, we add axiom (Ext) to the clause set. To curb the
explosion associated with extensionality, this axiom and all clauses derived
from it are penalized by the clause selection heuristic. We also added the
NegExt rule described in Section 12.2, which resembles Vampire’s
extensionality resolution rule [GKKV14].

The ArgCong rule can have infinitely many conclusions on polymorphic clauses.
To capture this in the implementation, we store these infinite sequences of
conclusions in the form of finite instructions of how to obtain the actual
clauses. In addition to the usual active and passive set of the DISCOUNT loop
architecture [ADF95], we use a set of scheduled inferences that stores these
instructions. We visit the scheduled inferences in this additional set and the
clauses in the passive set fairly to achieve dynamic completeness of our
prover architecture. Waldmann et al. [WTRB20, Example 34] and Bentkamp et al.
[BBT+21, Section 6] describe this architecture in more detail.

Using Zipperposition, we can quantify the disadvantage of the applicative
encoding on Example 12.2. A well-chosen KBO instance with argument
coefficients allows Zipperposition to derive $\bot$ in 4 iterations of the
prover’s main loop and 0.03 s. KBO or LPO with default settings needs 203
iterations and 0.4 s, whereas KBO or LPO on the applicatively encoded problem
needs 203 iterations and more than 1 s due to the larger terms.

##  21\. Evaluation

We evaluated Zipperposition’s implementation of our four calculi on
Sledgehammer-generated Isabelle/HOL benchmarks [BN10] and on benchmarks from
the TPTP library [SSCB12, SBBT09]. Our experimental data is available
online.222https://doi.org/10.5281/zenodo.3992618 We used the development
version of Zipperposition, revision
2031e216.333https://github.com/sneeuwballen/zipperposition/tree/2031e216c1941acd76187882a073e8f1e533

The Sledgehammer benchmarks, corresponding to Isabelle’s Judgment Day suite,
were regenerated to target clausal $\lambda$-free higher-order logic. They
comprise 2506 problems in total, divided in two groups based on the number of
Isabelle facts (lemmas, definitions, etc.) selected for inclusion in each
problem: either 16 facts (SH16) or 256 facts (SH256). The problems were
generated by encoding $\lambda$-expressions as $\lambda$-lifted
supercombinators [MP08].

From the TPTP library, we collected 708 first-order problems in TFF format and
717 higher-order problems in THF format, both groups containing both
monomorphic and polymorphic problems. We excluded all problems that contain
interpreted arithmetic symbols, the symbols (@@+), (@@-), (@+), (@-), (&), or
tuples, as well as the SYN000 problems, which are only intended to test the
parser, and problems whose clausal normal form takes longer than 15 s to
compute or falls outside the $\lambda$-free fragment described in Section 9.

We want to answer the following questions:

  1. (1)

What is the overhead of our calculi on first-order benchmarks?

  2. (2)

Do the calculi outperform the applicative encoding?

  3. (3)

Do the purifying or the nonpurifying calculi achieve better results?

  4. (4)

What is the cost of nonmonotonicity?

Since the present work is only a stepping stone towards a prover for full
higher-order logic, it would be misleading to compare this prototype with
state-of-the-art higher-order provers that support a stronger logic. Many of
the higher-order problems in the TPTP library are in fact satisfiable for our
$\lambda$-free logic, even though they may be unsatisfiable for full higher-
order logic and labeled as such in the TPTP.

To answer question (1) and (3), we ran Zipperposition’s first-order mode on
the first-order benchmarks and the purifying and nonpurifying modes on all
benchmarks. To answer question (2), we implemented an applicative encoding
mode in Zipperposition, which performs the applicative encoding after the
clausal normal form transformation and then proceeds with Zipperposition’s
first-order mode. The encoding makes all function symbols nullary and replaces
all applications with a polymorphic binary ${\mathsf{app}}$ symbol.

We instantiated all four calculi with three term orders: LPO [BWW17], KBO
[BBWW17] (without argument coefficients), and EPO [Ben18]. Among these, LPO is
the only nonmonotonic order and therefore the most relevant option to evaluate
our calculi, which are designed to cope with nonmonotonicity. To answer
question (4), we also include the monotone orders KBO and EPO. EPO is an order
designed to resemble LPO while fulfilling the requirements of a ground-total
simplification order on $\lambda$-free terms. KBO and EPO serve as a yardstick
to assess the cost of nonmonotonicity. With these monotone orders, no
superposition inferences at variables are necessary and thus the nonpurifying
calculi become a straightforward generalization of the standard superposition
calculus with the caveat that it may be more efficient to superpose at
nongreen subterms directly instead of relying on the ArgCong rule. On first-
order benchmarks and in the applicative encoding mode, all three orders are
monotone because they are monotone on first-order terms.

Figure 2 summarizes, for the intensional calculi, the number of solved
satisfiable and unsatisfiable problems within 180 s, and the time taken to
show unsatisfiability. Figure 2 presents the corresponding data for the
extensional calculi. The average time is computed over the problems that all
configurations for the respective benchmark set and term order found to be
unsatisfiable within the time limit. For each combination of benchmark set and
term order, the best result is highlighted in bold. The evaluation was carried
out on StarExec Iowa [SST14] using Intel Xeon E5-2609 0 CPUs clocked at 2.40
GHz.

|  | # sat | # unsat | ⌀ time
---|---|---|---|---
|  | LPO | KBO | EPO | LPO | KBO | EPO | LPO | KBO | EPO
SH16 | applicative encoding | 111 | 189 | 65 | 373 | 382 | 157 | 0.9 | 1.2 | 10.7
| nonpurifying calculus | 136 | 165 | 133 | 383 | 385 | 381 | 0.4 | 0.3 | 0.0
| purifying calculus | 82 | 98 | 82 | 363 | 363 | 355 | 1.3 | 2.0 | 0.0
SH256 | applicative encoding | 1 | 1 | 1 | 471 | 488 | 36 | 9.4 | 8.7 | 63.8
| nonpurifying calculus | 1 | 1 | 1 | 543 | 554 | 498 | 2.3 | 2.3 | 0.1
| purifying calculus | 1 | 1 | 1 | 523 | 528 | 484 | 2.6 | 3.4 | 0.5
TFF | first-order mode | 0 | 0 | 0 | 212 | 229 | 107 | 1.9 | 2.3 | 1.5
| applicative encoding | 0 | 0 | 0 | 180 | 205 | 21 | 7.0 | 10.0 | 4.6
| nonpurifying calculus | 0 | 0 | 0 | 210 | 229 | 105 | 1.9 | 2.4 | 1.5
| purifying calculus | 0 | 0 | 0 | 211 | 229 | 105 | 2.1 | 2.6 | 1.6
THF | applicative encoding | 127 | 115 | 111 | 523 | 522 | 428 | 0.9 | 0.6 | 0.8
| nonpurifying calculus | 111 | 114 | 112 | 529 | 527 | 516 | 0.3 | 0.3 | 0.0
| purifying calculus | 108 | 109 | 108 | 528 | 526 | 514 | 0.3 | 0.5 | 0.0

Figure 1. Evaluation of the intensional calculi

|  | # sat | # unsat | ⌀ time
---|---|---|---|---
|  | LPO | KBO | EPO | LPO | KBO | EPO | LPO | KBO | EPO
SH16 | applicative encoding | 79 | 152 | 48 | 379 | 386 | 157 | 1.2 | 1.3 | 11.4
| nonpurifying calculus | 103 | 131 | 95 | 386 | 393 | 387 | 0.4 | 0.1 | 0.0
| purifying calculus | 32 | 57 | 32 | 367 | 365 | 363 | 2.0 | 1.7 | 0.0
SH256 | applicative encoding | 1 | 1 | 1 | 462 | 486 | 36 | 7.5 | 9.4 | 63.8
| nonpurifying calculus | 1 | 1 | 1 | 548 | 572 | 504 | 1.9 | 2.1 | 0.1
| purifying calculus | 1 | 1 | 1 | 512 | 529 | 482 | 2.2 | 5.0 | 0.1
TFF | first-order mode | 0 | 0 | 0 | 212 | 229 | 107 | 1.9 | 2.5 | 1.5
| applicative encoding | 0 | 0 | 0 | 178 | 202 | 21 | 7.9 | 11.7 | 4.7
| nonpurifying calculus | 0 | 0 | 0 | 207 | 229 | 106 | 2.1 | 3.0 | 1.5
| purifying calculus | 0 | 0 | 0 | 210 | 229 | 105 | 2.2 | 3.2 | 1.6
THF | applicative encoding | 108 | 109 | 105 | 526 | 527 | 436 | 0.9 | 0.6 | 1.1
| nonpurifying calculus | 106 | 108 | 107 | 539 | 535 | 526 | 0.3 | 0.3 | 0.0
| purifying calculus | 96 | 97 | 96 | 530 | 529 | 519 | 0.3 | 0.6 | 0.0

Figure 2. Evaluation of the extensional calculi

The experimental results on the TFF part of the TPTP library confirm that our
calculi handle the vast majority of problems that are solvable in first-order
mode gracefully, and thus that the overhead is minimal, answering question
(1). On first-order problems, the calculi are occasionally at variance with
the first-order mode, due to the interaction of ArgCong with polymorphic types
and due to the extensionality axiom (Ext). In contrast, the applicative
encoding is comparatively inefficient on problems that are already first-
order. For LPO, the success rate decreases by around 15%, and the average time
to show unsatisfiability triples.

The SH16 benchmarks consist mostly of small higher-order problems. The small
number of axioms benefits the applicative encoding enough to outperform the
purifying calculi but not the nonpurifying ones. The SH256 benchmarks are also
higher-order but much larger. Such problems are underrepresented in the TPTP
library. On these, our calculi clearly outperform the applicative encoding,
answering question (2) decisively. This is hardly surprising given that the
proving effort is dominated by first-order reasoning, which they can perform
gracefully.

The THF benchmarks generally require more sophisticated higher-order reasoning
than the Sledgehammer benchmarks, as observed by Sultana, Blanchette, and
Paulson [SBP13, Section 5]. On these benchmarks, the empirical results are
less clear; the applicative encoding and our calculi are roughly neck-and-
neck. The nonpurifying calculi detect unsatisfiability slightly more
frequently, whereas the applicative encoding tends to find more saturations.
It seems that, due to the large amount of higher-order reasoning necessary to
solve TPTP problems, the advantage of our calculi on the first-order parts of
the derivation is not a decisive factor on these benchmarks.

Concerning question (3), the nonpurifying calculi outperform their purifying
relatives across all benchmarks. The raw data show that on most benchmark
sets, the problems solved by the nonpurifying calculi are almost a superset of
the problems solved by the purifying calculi. Only on the SH256 benchmarks,
the purifying calculi can solve a fair number of problems that the
nonpurifying calculi cannot solve (11 problems for the intensional calculi
with LPO and 9 problems for the extensional calculi with LPO).

KBO tends to have a slight advantage over LPO on all benchmark sets. But the
gap between KBO and LPO is not larger on the higher-order benchmarks than on
TFF. Since LPO is monotonic on first-order terms but nonmonotonic on higher-
order terms, whereas KBO is monotonic on both, the best answer we can give to
question (4) is that no substantial cost seems to be associated with
nonmonotonicity. In particular, for the nonpurifying calculi, the additional
superposition inferences at variables necessary with LPO do not have a
negative impact on the overall performance. EPO generally performs worse than
the other two orders, with the exception of the nonpurifying calculus on SH16
benchmarks, where it is roughly neck-and-neck with LPO. This suggests that for
small, mildly higher-order problems, EPO can be a viable LPO-like complement
to KBO if one considers the effort to implement our calculi too high.

##  22\. Discussion and Related Work

Our calculi join a long list of extensions and refinements of superposition.
Among the most closely related is Peltier’s [Pel16] Isabelle/HOL formalization
of the refutational completeness of a superposition calculus that operates on
$\lambda$-free higher-order terms and that is parameterized by a monotonic
term order. Extensions with polymorphism and induction, independently
developed by Cruanes [Cru15, Cru17] and Wand [Wan17], contribute to increasing
the power of automatic provers. Detection of inconsistencies in axioms, as
suggested by Schulz et al. [SSUP17], is important for large axiomatizations.

Also of interest is Bofill and Rubio’s [BR13] integration of nonmonotonic
orders in ordered paramodulation, a precursor of superposition. Their work is
a veritable tour de force, but it is also highly complicated and restricted to
ordered paramodulation. Lack of compatibility with arguments being a mild form
of nonmonotonicity, it seemed preferable to start with superposition, enrich
it with an ArgCong rule, and tune the side conditions until we obtained a
complete calculus.

Most complications can be avoided by using a monotonic order such as KBO
without argument coefficients. However, coefficients can be useful to help
achieve compatibility with $\beta$-reduction. For example, the term $\lambda
x.\;x+x$ could be treated as a constant with a coefficient of 2 on its
argument and a heavy weight to ensure $(\lambda x.\;x+x)\;y\succ y+y$.
Although they do not use argument coefficients, the recently developed
$\lambda$-superposition calculus by Bentkamp et al. [BBT+21] and combinatory
superposition calculus by Bhayat and Reger [BR20] need a nonmonotonic order to
cope with $\beta$-reduction. They are modeled after our extensional
nonpurifying and intensional nonpurifying calculi, respectively.

Many researchers have proposed or used encodings of higher-order logic
constructs into first-order logic, including Robinson [Rob70], Kerber [Ker91],
Dougherty [Dou93], Dowek et al. [DHK95], Hurd [Hur03], Meng and Paulson
[MP08], Obermeyer [Obe09], and Czajka [Cza16]. Encodings of types, such as
those by Bobot and Paskevich [BP11] and Blanchette et al. [BBPS16], are also
crucial to obtain a sound encoding of higher-order logic. These ideas are
implemented in proof assistant tools such as HOLyHammer and Sledgehammer
[BKPU16].

In the term rewriting community, $\lambda$-free higher-order logic is known as
applicative first-order logic. First-order rewrite techniques can be applied
to this logic via the applicative encoding. However, there are similar
drawbacks as in theorem proving to having ${\mathsf{app}}$ as the only
nonnullary symbol. Hirokawa et al. [HMZ13] propose a technique that resembles
our mapping $\mathcalx{F}$ to avoid these drawbacks.

Another line of research has focused on the development of automated proof
procedures for higher-order logic. Robinson’s [Rob69], Andrews’s [And71], and
Huet’s [Hue73] pioneering work stands out. Andrews [And01] and Benzmüller and
Miller [BM14] provide excellent surveys. The competitive higher-order
automatic theorem provers include Leo-II [BPTF08] (based on RUE resolution),
Satallax [Bro12] (based on a tableau calculus and a SAT solver), agsyHOL
[Lin14] (based on a focused sequent calculus and a generic narrowing engine),
Leo-III [SB18] (based on a pragmatic higher-order version of ordered
paramodulation with no completeness guarantees), CVC4 and veriT [BREO+19]
(both based on satisfiability modulo theories), and Vampire [BR19, BR20]
(based on superposition and ${\mathsf{SK}}$-style combinators). The Isabelle
proof assistant [NPW02] (which includes a tableau reasoner and a rewriting
engine) and its Sledgehammer subsystem have also participated in the higher-
order division of the CADE ATP System Competition.

Zipperposition is a convenient vehicle for experimenting and prototyping
because it is easier to understand and modify than highly-optimized C or C++
provers. Our middle-term goal is to design higher-order superposition calculi,
implement them in state-of-the-art provers such as E [Sch13], SPASS [WDF+09],
and Vampire [KV13], and integrate these in proof assistants to provide a high
level of automation. With its stratified architecture, Otter-$\lambda$ [Bee04]
is perhaps the closest to what we are aiming at, but it is limited to second-
order logic and offers no completeness guarantees. As a first step,
Vukmirović, Blanchette, Cruanes, and Schulz [VBCS19] have generalized E’s data
structures and algorithms to clausal $\lambda$-free higher-order logic,
assuming a monotonic KBO [BBWW17].

##  23\. Conclusion

We presented four superposition calculi for intensional and extensional
clausal $\lambda$-free higher-order logic and proved them refutationally
complete. The calculi nicely generalize standard superposition and are
compatible with our $\lambda$-free higher-order LPO and KBO. Especially on
large problems, our experiments confirm what one would naturally expect: that
native support for partial application and applied variables outperforms the
applicative encoding.

The new calculi reduce the gap between proof assistants based on higher-order
logic and superposition provers. We can use them to reason about arbitrary
higher-order problems by axiomatizing suitable combinators. But perhaps more
importantly, they appear promising as a stepping stone towards complete,
highly efficient automatic theorem provers for full higher-order logic.
Indeed, the subsequent work by Bentkamp et al. [BBT+21], which introduces
support for $\lambda$-expressions, and Bhayat and Reger [BR20], which works
with ${\mathsf{SK}}$-style combinators, is largely based on our nonpurifying
calculi.

#### Acknowledgment.

We are grateful to the maintainers of StarExec for letting us use their
service. We want to thank Petar Vukmirović for his work on Zipperposition and
for his advice. We thank Christoph Benzmüller, Sander Dahmen, Johannes Hölzl,
Anders Schlichtkrull, Stephan Schulz, Alexander Steen, Geoff Sutcliffe, Andrei
Voronkov, Daniel Wand, Christoph Weidenbach, and the participants in the 2017
Dagstuhl Seminar on Deduction beyond First-Order Logic for stimulating
discussions. We also want to thank Christoph Benzmüller, Ahmed Bhayat, Wan
Fokkink, Alexander Steen, Mark Summerfield, Sophie Tourret, and the anonymous
reviewers for suggesting several textual improvements. Bentkamp and
Blanchette’s research has received funding from the European Research Council
(ERC) under the European Union’s Horizon 2020 research and innovation program
(grant agreement No. 713999, Matryoshka).

## References

  * [ADF95] Jürgen Avenhaus, Jörg Denzinger, and Matthias Fuchs.  DISCOUNT: A system for distributed equational deduction.  In Jieh Hsiang, editor, RTA-95, volume 914 of LNCS, pages 397–402. Springer, 1995.
  * [And71] Peter B. Andrews.  Resolution in type theory.  J. Symb. Log., 36(3):414–432, 1971.
  * [And01] Peter B. Andrews.  Classical type theory.  In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume II, pages 965–1007. Elsevier and MIT Press, 2001\.
  * [BBCW18] Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, and Uwe Waldmann.  Superposition for lambda-free higher-order logic.  In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, IJCAR 2018, volume 10900 of LNCS, pages 28–46. Springer, 2018.
  * [BBPS16] Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone.  Encoding monomorphic and polymorphic types.  Log. Meth. Comput. Sci., 12(4:13):1–52, 2016.
  * [BBT+21] Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann.  Superposition with lambdas.  J. Autom. Reason., 2021.
  * [BBWW17] Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand.  A transfinite Knuth–Bendix order for lambda-free higher-order terms.  In Leonardo de Moura, editor, CADE-26, volume 10395 of LNCS, pages 432–453. Springer, 2017.
  * [BC04] Yves Bertot and Pierre Castéran.  Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions.  Texts in Theoretical Computer Science. Springer, 2004.
  * [Bee04] Michael Beeson.  Lambda logic.  In David A. Basin and Michaël Rusinowitch, editors, IJCAR 2004, volume 3097 of LNCS, pages 460–474. Springer, 2004.
  * [Ben18] Alexander Bentkamp.  Formalization of the embedding path order for lambda-free higher-order terms.  Archive of Formal Proofs, 2018.  http://isa-afp.org/entries/Lambda_Free_EPO.html.
  * [BG94] Leo Bachmair and Harald Ganzinger.  Rewrite-based equational theorem proving with selection and simplification.  J. Log. Comput., 4(3):217–247, 1994.
  * [BG01] Leo Bachmair and Harald Ganzinger.  Resolution theorem proving.  In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 19–99. Elsevier and MIT Press, 2001.
  * [BKPU16] Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban.  Hammering towards QED.  J. Formaliz. Reas., 9(1):101–148, 2016.
  * [BM14] Christoph Benzmüller and Dale Miller.  Automation of higher-order logic.  In Jörg H. Siekmann, editor, Computational Logic, volume 9 of Handbook of the History of Logic, pages 215–254. Elsevier, 2014\.
  * [BN10] Sascha Böhme and Tobias Nipkow.  Sledgehammer: Judgement Day.  In Jürgen Giesl and Reiner Hähnle, editors, IJCAR 2010, volume 6173 of LNCS, pages 107–121. Springer, 2010.
  * [BP11] François Bobot and Andrei Paskevich.  Expressing polymorphic types in a many-sorted language.  In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, FroCoS 2011, volume 6989 of LNCS, pages 87–102. Springer, 2011.
  * [BP13] Jasmin Christian Blanchette and Andrei Paskevich.  TFF1: The TPTP typed first-order form with rank-1 polymorphism.  In Maria Paola Bonacina, editor, CADE-24, volume 7898 of LNCS, pages 414–420. Springer, 2013.
  * [BPTF08] Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, and Arnaud Fietzke.  LEO-II—A cooperative automatic theorem prover for higher-order logic.  In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, IJCAR 2008, volume 5195 of LNCS, pages 162–170. Springer, 2008\.
  * [BR13] Miquel Bofill and Albert Rubio.  Paramodulation with non-monotonic orderings and simplification.  J. Autom. Reason., 50(1):51–98, 2013.
  * [BR19] Ahmed Bhayat and Giles Reger.  Restricted combinatory unification.  In Pascal Fontaine, editor, CADE-27, volume 11716 of LNCS, pages 74–93. Springer, 2019.
  * [BR20] Ahmed Bhayat and Giles Reger.  A combinator-based superposition calculus for higher-order logic.  In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, IJCAR 2020, Part I, volume 12166 of LNCS, pages 278–296. Springer, 2020\.
  * [Bra75] D. Brand.  Proving theorems with the modification method.  SIAM J. Comput., 4:412–430, 1975.
  * [BREO+19] Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, and Clark Barrett.  Extending SMT solvers to higher-order logic.  In Pascal Fontaine, editor, CADE-27, volume 11716 of LNCS, pages 35–54. Springer, 2019.
  * [Bro12] Chad E. Brown.  Satallax: An automatic higher-order prover.  In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, IJCAR 2012, volume 7364 of LNCS, pages 111–117. Springer, 2012.
  * [BWW17] Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand.  A lambda-free higher-order recursive path order.  In Javier Esparza and Andrzej S. Murawski, editors, FoSSaCS 2017, volume 10203 of LNCS, pages 461–479. Springer, 2017.
  * [Chu40] Alonzo Church.  A formulation of the simple theory of types.  J. Symb. Log., 5(2):56–68, 1940.
  * [CP03] Iliano Cervesato and Frank Pfenning.  A linear spine calculus.  J. Log. Comput., 13(5):639–688, 2003.
  * [Cru15] Simon Cruanes.  Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond.  Ph.D. thesis, École polytechnique, 2015.
  * [Cru17] Simon Cruanes.  Superposition with structural induction.  In Clare Dixon and Marcelo Finger, editors, FroCoS 2017, volume 10483 of LNCS, pages 172–188. Springer, 2017.
  * [Cza16] Łukasz Czajka.  Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions.  In Jeremy Avigad and Adam Chlipala, editors, CPP 2016, pages 49–57. ACM, 2016.
  * [DH86] Vincent J. Digricoli and Malcolm C. Harrison.  Equality-based binary resolution.  J. ACM, 33(2):253–289, 1986.
  * [DHK95] Gilles Dowek, Thérèse Hardin, and Claude Kirchner.  Higher-order unification via explicit substitutions (extended abstract).  In LICS ’95, pages 366–374. IEEE Computer Society, 1995.
  * [Dou93] Daniel J. Dougherty.  Higher-order unification via combinators.  Theor. Comput. Sci., 114(2):273–298, 1993.
  * [Fit96] Melvin Fitting.  First-Order Logic and Automated Theorem Proving.  Springer-Verlag, 2nd edition, 1996.
  * [Fit02] Melvin Fitting.  Types, Tableaus, and Gödel’s God.  Kluwer, 2002.
  * [GKKV14] Ashutosh Gupta, Laura Kovács, Bernhard Kragl, and Andrei Voronkov.  Extensional crisis and proving identity.  In Franck Cassez and Jean-François Raskin, editors, ATVA 2014, volume 8837 of LNCS, pages 185–200. Springer, 2014.
  * [GM93] M. J. C. Gordon and T. F. Melham, editors.  Introduction to HOL: A Theorem Proving Environment for Higher Order Logic.  Cambridge University Press, 1993.
  * [Hen50] Leon Henkin.  Completeness in the theory of types.  J. Symb. Log., 15(2):81–91, 1950.
  * [HMZ13] Nao Hirokawa, Aart Middeldorp, and Harald Zankl.  Uncurrying for termination and complexity.  J. Autom. Reasoning, 50(3):279–315, 2013.
  * [Hue73] Gérard P. Huet.  A mechanization of type theory.  In Nils J. Nilsson, editor, IJCAI-73, pages 139–146. William Kaufmann, 1973.
  * [Hur03] Joe Hurd.  First-order proof tactics in higher-order logic theorem provers.  In Myla Archer, Ben Di Vito, and César Muñoz, editors, Design and Application of Strategies/Tactics in Higher Order Logics, NASA Technical Reports, pages 56–68, 2003.
  * [Ker91] Manfred Kerber.  How to prove higher order theorems in first order logic.  In John Mylopoulos and Raymond Reiter, editors, IJCAI-91, pages 137–142. Morgan Kaufmann, 1991.
  * [Kop12] Cynthia Kop.  Higher Order Termination: Automatable Techniques for Proving Termination of Higher-Order Term Rewriting Systems.  Ph.D. thesis, Vrije Universiteit Amsterdam, 2012.
  * [KV13] Laura Kovács and Andrei Voronkov.  First-order theorem proving and Vampire.  In Natasha Sharygina and Helmut Veith, editors, CAV 2013, volume 8044 of LNCS, pages 1–35. Springer, 2013.
  * [Lei94] Daniel Leivant.  Higher order logic.  In Dov M. Gabbay, Christopher J. Hogger, J. A. Robinson, and Jörg H. Siekmann, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 2, Deduction Methodologies, pages 229–322. Oxford University Press, 1994.
  * [Lin14] Fredrik Lindblad.  A focused sequent calculus for higher-order logic.  In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, IJCAR 2014, volume 8562 of LNCS, pages 61–75. Springer, 2014.
  * [Mil87] Dale A. Miller.  A compact representation of proofs.  Studia Logica, 46(4):347–370, 1987.
  * [MP08] Jia Meng and Lawrence C. Paulson.  Translating higher-order clauses to first-order clauses.  J. Autom. Reason., 40(1):35–60, 2008.
  * [NPW02] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel.  Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS.  Springer, 2002.
  * [Obe09] Fritz H. Obermeyer.  Automated Equational Reasoning in Nondeterministic $\lambda$-Calculi Modulo Theories $\mathcal{H}{}^{*}$.  Ph.D. thesis, Carnegie Mellon University, 2009.
  * [Pel16] Nicolas Peltier.  A variant of the superposition calculus.  Archive of Formal Proofs, 2016.
  * [Rob69] J.A. Robinson.  Mechanizing higher order logic.  In B. Meltzer and D. Michie, editors, Machine Intelligence, volume 4, pages 151–170. Edinburgh University Press, 1969.
  * [Rob70] J.A. Robinson.  A note on mechanizing higher order logic.  In B. Meltzer and D. Michie, editors, Machine Intelligence, volume 5, pages 121–135. Edinburgh University Press, 1970.
  * [SB18] Alexander Steen and Christoph Benzmüller.  The higher-order prover Leo-III.  In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, IJCAR 2018, volume 10900 of LNCS, pages 108–116. Springer, 2018\.
  * [SBBT09] Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, and Frank Theiss.  Progress in the development of automated theorem proving for higher-order logic.  In Renate A. Schmidt, editor, CADE-22, volume 5663 of LNCS, pages 116–130. Springer, 2009.
  * [SBP13] Nik Sultana, Jasmin Christian Blanchette, and Lawrence C. Paulson.  LEO-II and Satallax on the Sledgehammer test bench.  J. Applied Logic, 11(1):91–102, 2013.
  * [Sch02] Stephan Schulz.  E - a brainiac theorem prover.  AI Commun., 15(2-3):111–126, 2002.
  * [Sch12] Stephan Schulz.  Fingerprint indexing for paramodulation and rewriting.  In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, IJCAR 2012, volume 7364 of LNCS, pages 477–483. Springer, 2012.
  * [Sch13] Stephan Schulz.  System description: E 1.8.  In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov, editors, LPAR-19, volume 8312 of LNCS, pages 735–743. Springer, 2013\.
  * [SL91] Wayne Snyder and Christopher Lynch.  Goal directed strategies for paramodulation.  In Ronald V. Book, editor, RTA-91, volume 488 of LNCS, pages 150–161. Springer, 1991.
  * [SS89] Manfred Schmidt-Schauß.  Unification in a combination of arbitrary disjoint equational theories.  J. Symb. Comput., 8:51–99, 1989.
  * [SSCB12] Geoff Sutcliffe, Stephan Schulz, Koen Claessen, and Peter Baumgartner.  The TPTP typed first-order form with arithmetic.  In Nikolaj Bjørner and Andrei Voronkov, editors, LPAR-18, volume 7180 of LNCS, pages 406–419. Springer, 2012.
  * [SST14] Aaron Stump, Geoff Sutcliffe, and Cesare Tinelli.  StarExec: A cross-community infrastructure for logic solving.  In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, IJCAR 2014, volume 8562 of LNCS, pages 367–373. Springer, 2014.
  * [SSUP17] Stephan Schulz, Geoff Sutcliffe, Josef Urban, and Adam Pease.  Detecting inconsistencies in large first-order knowledge bases.  In Leonardo de Moura, editor, CADE-26, volume 10395 of LNCS, pages 310–325. Springer, 2017.
  * [Vää19] Jouko Väänänen.  Second-order and higher-order logic.  In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, fall 2019 edition, 2019.
  * [VBCS19] Petar Vukmirović, Jasmin Christian Blanchette, Simon Cruanes, and Stephan Schulz.  Extending a brainiac prover to lambda-free higher-order logic.  In Tomas Vojnar and Lijun Zhang, editors, TACAS 2019, volume 11427 of LNCS, pages 192–210. Springer, 2019.
  * [Wan17] Daniel Wand.  Superposition: Types and Polymorphism.  Ph.D. thesis, Universität des Saarlandes, 2017.
  * [WDF+09] Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, and Patrick Wischnewski.  SPASS version 3.5.  In Renate A. Schmidt, editor, CADE-22, volume 5663 of LNCS, pages 140–145. Springer, 2009.
  * [WTRB20] Uwe Waldmann, Sophie Tourret, Simon Robillard, and Jasmin Blanchette.  A comprehensive framework for saturation theorem proving.  In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, IJCAR 2020, Part I, volume 12166 of LNCS, pages 316–334. Springer, 2020\.


# Unsupervised Word Segmentation with Bi-directional
Neural Language Model

Lihao Wang, Zongyi Li, Xiaoqing Zheng
School of Computer Science, Fudan University, Shanghai, China
Shanghai Key Laboratory of Intelligent Information Processing
{wanglh19, zongyili19<EMAIL_ADDRESS>
###### Abstract

We present an unsupervised word segmentation model, in which the learning
objective is to maximize the generation probability of a sentence given its
all possible segmentation. Such generation probability can be factorized into
the likelihood of each possible segment given the context in a recursive way.
In order to better capture the long- and short-term dependencies, we propose
to use bi-directional neural language models to better capture the features of
segment’s context. Two decoding algorithms are also described to combine the
context features from both directions to generate the final segmentation,
which helps to reconcile word boundary ambiguities. Experimental results
showed that our context-sensitive unsupervised segmentation model achieved
state-of-the-art at different evaluation settings on various data sets for
Chinese, and the comparable result for Thai.

##  1 Introduction

Word segmentation aims to split a natural language sentence into its component
words. In English and many other Latin languages, whitespace is used as a
natural delimiter among words, while in character-based language such as
Chinese and Japanese, we usually need to recover implicit word boundaries
before further processing on language tasks. Previous psychological studies
Cattell (1886); Li et al. (2009) indicate that words are processed in a word-
level way instead of character-level way, which means word segmentation is an
essential step for further researches.

Table 1: Example sentences where the context features from both directions are required to reconcile the word boundary ambiguities. 我 / 从小 / 学 / 唱歌 |  I started learning to sing when I was young.
---|---
我 / 从 / 小学 / 毕业 |  I graduated from primary school.

There are two main learning paradigms for word segmentation: namely supervised
and unsupervised approaches. Although supervised methods have generally
achieved higher accuracy Huang and Zhao (2007), these models need a large
volume of manually labeled corpora to be trained, which requires expensive
human efforts. Furthermore, supervised approaches often train domain-specific
models, which may achieve accurate prediction on texts in the same domain as
the training texts, but significantly deteriorate performance when applied to
texts in other domains. Moreover, there is still no segmentation standard
widely accepted for some languages. For example, in Chinese, the meaning of a
multi-word phrase may vary greatly if the words are considered separately or
together. Unsupervised word segmentation approaches can deal with the three
issues mentioned above. The training with unlabeled dataset requires much less
human effort, and previous studies show that unsupervised learning has better
stability and adaptivity to novel domain, such as raw texts with unseen words
or in new languages. All these advantages over supervised learning makes
unsupervised approaches worth further investigation.

Traditional work on unsupervised word segmentation can be divided into two
categories: rule-based approaches and statistical approaches. The rule-based
approaches identify words by applying prior knowledge or morpho-lexical rules
governing the derivation of Sproat and Shih (1990); Jin and Tanaka-Ishii
(2006); Magistry and Sagot (2012), while the statistical approaches identify
words based on the distribution of their components in a larger corpus Teh
(2006); Goldwater et al. (2009); Mochihashi et al. (2009); Uchiumi et al.
(2015). The former is intrinsically context-free, so it could not deal with
the word boundary ambiguities (i.e. combination and overlap ambiguity). The
hyper-parameters of the latter need to be carefully tuned for a training
corpus, which might not be still work for others.

Recently, neural networks have been tried to address the problem of
unsupervised word segmentation. Wang et al. (2017) proposed the Sleep-WAke
Network (SWAN) for speech recognition and also apply it to text segmentation.
Sun and Deng (2018) extended SWAN model for Chinese word segmentation and
presented a Segmental language models (SLM). However, those models only
consider the context from a direction (left-to-right) and can not well resolve
the word boundary ambiguities that only can be reconciled by using the context
features from both directions (see example Chinese sentences listed in Table
1).

We propose an unsupervised word segmentation model based on a bi-directional
neural language model by maximizing the generation probability of sentences,
which can be recursively factorized into the likelihood of their all possible
segmentation, taking their rich-context features into consideration. Two
decoding algorithms were proposed to combine the context features from both
directions. One is to produce the segmentation by taking the average of
segment’s probabilities estimated by the forward and backward language models.
Another is to generate the segmentation by merging their results produced
separately by those two models. The former revealed better in word boundary
ambiguity reconciliation, while the latter achieved the higher overall
performance.

Our model can successfully split a sentence into words without any prior
knowledge or manually designed features. The bi-directional language models
are used to better capture the long- and short-term dependencies within
sentences. Experimental results on Chinese datasets showed that our model
performed better than SWAN Wang et al. (2017) and SLM Sun and Deng (2018) with
a significant margin. Our context-sensitive unsupervised model achieved state-
of-the-art on multiple Chinese benchmarks with different settings. We also
evaluated our model on Thai in which the words are formed by more characters
in average than those in Chinese, and achieved comparable result, comparing
with recent strong competitors.

##  2 Related Work

###  2.1 Traditional Methods

There are two main paradigms for the traditional works of unsupervised Chinese
word segmentation: one uses goodness measures to find boundaries between
words, while the other estimates the probability by nonparametric Bayesian
models.

Sproat and Shih (1990) first applied mutual information (MI) to word
segmentation, and then many methods have been proposed based on the variants
of goodness measures, including cohesion measure, separation measure and a
combination of two. Several goodness measures were compared by Zhao and Kit
(2008). They propose a unified framework, including description length gain
(DLG) Kitt and Wilks (1999), accessor variety (AV) Feng et al. (2004), and
branch entropy (BE) Jin and Tanaka-Ishii (2006). Magistry and Sagot (2012)
promoted on the branch entropy method, and proposed nVBE by adding
normalization and viterbi decoding which removed most hyper-parameters. Wang
et al. (2011) proposed ESA (Evaluation, Selection, Adjustment), which used
goodness measures to adopt a local maximum strategy without thresholds.

The other important paradigm used in unsupervised word segmentation is
nonparametric Bayesian model. Dirichlet process (DP) MacEachern and Müller
(1998), Pitman-Yor process (PYP) Pitman and Yor (1997), hierarchical DP (HDP)
Teh et al. (2005); Goldwater et al. (2006), hierarchical PYP (HPYP) Teh (2006)
have been introduced to word segmentation. Goldwater et al. (2009) proposed a
unigram and bigram model for unsupervised word segmentation, with the help of
DP and HDP. However, these approaches are computationally intensive.
Mochihashi et al. (2009) introduced a faster algorithm based on a nested
Pitman-Yor language model (NPYLM) by introducing a nested character model and
an efficient blocked Gibbs sampler combined with dynamic programming for
inference and Pitman-Yor Hidden Semi-Markov Model (PYHSMM) Uchiumi et al.
(2015) which was considered as a method to build a class n-gram language model
directly from strings while integrating character and word level information.
Their evaluation results outperformed the previous. Joint model of
hierarchical Dirichlet process model and character-based hidden Markov model
(Chen et al., 2014) and Bayesian model based on monolingual character (Teng et
al., 2014) achieved state-of-art performance in different datasets.

###  2.2 Neural Methods

Kong et al. (2015) introduced segmental recurrent neural networks (SRNNs)
which define a joint probability distribution over segmentations of the input
and labeling of the segments. This model can be partially training in which
segment boundaries are latent, but can not extend the task fully unsupervised
in the case of neither labels nor latent variable. Wang et al. (2017) proposed
the Sleep-WAke Network (SWAN) which sum over all valid segmentations to obtain
the final probability for the sequence. SWAN model present a sentence-level
loss function under unsupervised conditions. Aimed for speech recognition,
SWAN is a online segment to segment model which used beam search decoding
algorithm. Sun and Deng (2018) extended SWAN to Chinese word segmentation and
use dynamic decoding algorithm to get best segmentation path. Neither Wang nor
Sun consider the influence of backward context information on segmentation.

##  3 Methodology

We assume that the result of word segmentation can be determined by a latent
variable, and its prior distribution is a uniform distribution over all the
possible segmentations for a sentence. We require that a good segmentation
should contribute to increase the generation probability of a sentence, and
thus we can choose the segmentation with the highest generation probability
for the sentence as the final result. Our unsupervised segmentation model
learns to maximize the generation probability of each sentence given its all
the possible word segmentations. We show that such probability can be
factorize into the likelihood of each possible segment (or fragment) of a
sentence given its context in a recursive way. Bi-directional neural language
models are used to capture the context information for a segment and to
estimate the probabilities of the segment from the both sides. Two dynamic
decoding algorithms are proposed to combine the context information from the
both sizes to produce the best segmentation.

###  3.1 Unsupervised Framework

We introduce a latent variable $z$ that determines the result of segmentation.
If we have a sentence denoted as $d$, then the probability of $z$ given $d$
with parameters $\theta$ can be formalized as follows:

$p_{\theta}(z|d)=\frac{p_{\theta}(d|z)p_{\theta}(z)}{p_{\theta}(d)}$ (1)

Since $p_{\theta}(d)$ is a constant term, we can find the best segmentation by
finding the value of $z$ that maximizes $p_{\theta}(d|z)p_{\theta}(z)$. It is
usually easier to estimate $p_{\theta}(d|z)$ by proposing a model that can be
used to generate the observed data $d$. If we assume the prior of
$p_{\theta}(z)$ is a uniform distribution, then we can gain the best
segmentation $z^{*}$ via:

$z^{*}=\mathop{\arg\max}_{z}p_{\theta}(d|z)$ (2)

We optimize the model’s parameters $\theta$ by maximizing a log-likelihood
function $L$. If marginalizing all the segmentation $z$, we have:

$L(\theta)=\sum\limits_{d}\ln
p_{\theta}(d)=\sum\limits_{d}\ln\sum\limits_{z}p_{\theta}(d|z)$ (3)

In the above equation, we need to compute the sum of generation probabilities
for a sentence over all the possible segmentations. However, it is infeasible
to enumerate all the possible segmentations, and so we use dynamic programming
technique to compute such probability.

###  3.2 Generation Probability

A forward-backward algorithm is an inference algorithm used in hidden Markov
models, which computes the posterior marginals of all hidden state variables
given a sequence of observationsRabiner (1989). In our method, the algorithm
can be applied to calculate the sum probability of the sentences generated by
all possible segmentation.

We follow the symbol of Mochihashi et al. (2009). First, we define $\alpha$ as
forward variable, $t$ as the character sequence length, $k$ as the predicted
word length and abbreviated character sequence $c_{m}\cdots c_{n}$ to
$c_{m:n}$. Then, the forward variable $\alpha_{t}^{k}$ means the probability
of character sequence $c_{1:t}$ with final $k$ characters being a word. We
also use $q_{t}=k$ to represent the occurrence of a sequence of length $t$
whose final $k$ characters is a word. Then, we have the following deduction:

$\begin{split}\alpha_{t}^{k}&=p(c_{1:t},q_{t}=k)\\\
&=p(c_{1:t-k},c_{t-k+1:t},q_{t}=k)\\\
&=\sum\limits_{j=1}^{t-k}p(q_{t}=k,c_{t-k+1:t},c_{1:t-k},q_{t-k}=j)\\\
&=\sum\limits_{j=1}^{t-k}p(q_{t}=k|c_{t-k+1:t})p(c_{t-k+1:t}|c_{1:t-k})\alpha_{t-k}^{j}\end{split}$
(4)

Note that $p(c_{t-k+1:t}|c_{1:t-k})$ denotes the generated probability of
segment character sequence given the preceding context and
$p(q_{t}=k|c_{t-k-1:t})$ denotes the probability of the segment being a word.
These two kinds of probability will be modeled in next section. Now, we can
calculate the sum probability via forward variable :

$\sum\limits_{z}p_{\theta}(d|z)=\sum\limits_{k=0}^{N}\alpha_{N}^{k}$ (5)

where $N$ is the length of the sentence and $\alpha_{0}^{0}=1$

According to Markov property, the probabilities above are related to the
previous states(previous segmentations and preceding context). In order to
leverage the following context to segmentation, we define a backward variable
as $\beta_{t}^{k}$ and just reverse the sentences and apply the equation (4)
again to obtain another sum probability. The probabilities calculated by
forward variable $\alpha$ denote the generative probabilities with preceding
context , while the probability calculated by backward variable $\beta$
denotes the generative probability with following. We average the above two
probabilities to make full use of the context information of both sides. Now
we can obtain the objective function $J(\theta)$ according to equation
(4)-(6):

$\begin{split}J(\theta)&=-L(\theta)\\\
&=-\sum\limits_{d}\ln\sum\limits_{z}p_{\theta}(d|z)\\\
&=-\frac{1}{2}\sum\limits_{d}\ln(\sum\limits_{k=0}^{N_{d}}\alpha_{N_{d}}^{k}\sum\limits_{k=0}^{N_{d}}\beta_{N_{d}}^{k})\end{split}$
(6)

###  3.3 Model

In the previous two sections, we present an unsupervised framework to
inference the best segmentation $z$, and apply max-likelihood to estimate
model parameter $\theta$ as well. We also factorized the objective function
into the probability modeling of $p(q_{t}=k|c_{t-k+1:t})$ and
$p(c_{t-k+1:t}|c_{1:t-k})$. In this section, we will utilize neural language
model to generate these probabilities.

####  3.3.1 Neural Network-based Implementation

Now, we introduce a neural network architecture to implement the above
framework.

Firstly, $p(c_{t-k+1:t}|c_{1:t-k})$ can be further factorized and generated by
neural language models. We also denote the possible segment character sequence
$c_{t-k+1:t}$ as $s_{1:k}$ :

$p(c_{t-k+1:t}|c_{1:t-k})=\prod_{i=1}^{k}p(s_{i}|s_{1:i-1},c_{1:t-k})$ (7)

Recent work Bengio et al. (2003); Mikolov et al. (2010); Jozefowicz et al.
(2016) suggests that recurrent neural network (RNN), and its variants Long
short-term memory (LSTM) Hochreiter and Schmidhuber (1997), Gated Recurrent
Unit (GRU) Cho et al. (2014) have a good ability to model language models, as
they have the ability to capture the long- and short-term dependencies.
Therefore, we use four LSTMs to obtain the probabilities : two for generating
context representations, named as context LSTMs, two as neural language models
to generate above probabilities, named as language model LSTMs , each aspect
can be split into two directions, forward and backward.

We take the forward direction as an example, the forward context LSTM is used
to capture the preceding context information.Given a N-length character
embedding input sequence of sentences $(c_{1}\cdots c_{N})$, the context LSTM
$f^{C}$ produce the forward hidden sequence
$(\stackrel{{\scriptstyle\rightarrow}}{{\mathbf{h_{1}^{C}}}}\cdots\stackrel{{\scriptstyle\rightarrow}}{{\mathbf{h_{N}^{C}}}})$
as representations of the preceding context, which will also be used as
initial hidden state of a forward language model LSTM. At each time step $t$,
the hidden state $\mathbf{h_{t}^{C}}$ of the context LSTM is updated by:

$\mathbf{h}_{\mathbf{t}}^{\mathbf{C}}=f^{C}\left(\mathbf{h}_{\mathbf{t}-\mathbf{1}}^{\mathbf{C}},c_{t-1}\right)$
(8)

Then, the language model LSTM $f^{L}$ can learn a probability distribution
over a possible segment character sequence $s_{1:k}$ by being trained to
predict the next character in the sequence via softmax function. The initial
hidden state $\mathbf{h_{0}^{L}}$ of the language model LSTM obtains from
hidden sequence generated by the context LSTM at the time step $t-k+1$ , which
represents the preceding context of sequence $s_{1:k}$. :

$\mathbf{h}_{0}^{\mathbf{L}}=\mathbf{h}_{\mathbf{t}-\mathbf{k}+1}^{\mathbf{C}}$
(9)

$\mathbf{h}_{\mathbf{t}^{\prime}}^{\mathbf{L}}=f^{L}\left(\mathbf{h}_{\mathbf{t}^{\prime}-\mathbf{1}}^{\mathbf{L}},s_{t^{\prime}-1}\right)$
(10)

$p(s_{i}|s_{1:i-1},c_{1:t-k})=\frac{\exp\left(\mathbf{w}_{j}\mathbf{h}_{i}^{L}\right)}{\sum_{j^{\prime}=1}^{V}\exp\left(\mathbf{w}_{j^{\prime}}\mathbf{h}_{i}^{L}\right)}$
(11)

Finally, we combine these probability using equation (7) to obtain the segment
probability with preceding context. Similarly, the backward context LSTM
computes the backward hidden sequence
$(\stackrel{{\scriptstyle\leftarrow}}{{\mathbf{h_{1}^{C}}}}\cdots\stackrel{{\scriptstyle\leftarrow}}{{\mathbf{h_{N}^{C}}}})$
as the following context information and the backward language model LSTM
generates the probability.

$p(q_{t}=k|c_{t-k+1:t})$ can be modeled as the probability of an end-of-
segment symbol $EOS$, and the probability $p(q_{t}=k|c_{t-k+1:t})$ is
equivalent to $p(EOS|c_{t-k+1:t},c_{1:t-k})$. $EOS$ will compete with all
other meaningful characters when optimizing the candidate segment
probabilities and reduce the probability of wrong candidate sub-sequences
becoming a word. The architecture of our model is shown in Figure 1.

Figure 1: The neural network architecture. In this figure, we want to obtain
the probability of possible segment “从小”. Firstly, pick out preceding context
representation “我” and preceding context representation “学唱歌” from two context
LSTMs. Then we used these representations as the initial hidden states of two
Language model LSTMs and generate the character probability from both side (We
also input the “EOS” symbol to generate the first character probability). Next
, we multiply all the character probabilities to obtain two version of
possible segment probabilities. At Last, we average them to get a more
accurate probability or utilize them respectively.

####  3.3.2 Computational Complex and Optimization

Every candidate segment starting with the same position shares the same
forward context, and there is no need to compute it $N$ times. We store the
hidden states of context LSTMs to reduce the algorithm complexity from
$O(N^{4})$ to $O(N^{3})$, where $N$ stands for input sequence length.

Yee (1986) claimed that $69\%$ of Chinese articles consist of single character
word, while only $1\%$ consist of three or more character word. So it is
unnecessary to sum all the $k$ (last k character being one word), value from 1
to N. We set the maximum length of the words to $T(T\geq 3)$, reducing the
algorithm complexity to $O(NT^{2})$.

In addition, we can compute all the nested sub-sequence probabilities once the
generation probability of the entire sequence is obtained. Such probabilities
is produced by the softmax layers of our segments. Therefore, we just need to
compute the probability of longest segments, and meanwhile we can get the
nested candidate segments’ probabilities which share the start position with
the longest segments. We thus can reduce the algorithm complexity from
$O(NT^{2})$ to $O(NT)$.

###  3.4 Decoding Algorithms

In order to simplify the formulation, we denote the product of
$p(q_{t}=k|c_{t-k+1:t})$ and $p(c_{t-k+1:t}|c_{1:t-k})$ as the probability
$p_{\theta}(w_{i}|ctx(w_{i}))$ of the word $w_{i}$ made up by character
sequence $c_{t-k+1:t}$ given its context $ctx(w_{i})$. The backward version
one is symmetrically denoted as $p_{\theta}(w_{i}^{*}|ctx(w_{i}^{*}))$. Then,
we can compute the probability of a particular segmentation which segments the
character sequence $c_{1}\cdots c_{N}$ into the word sequence $w_{1}\cdots
w_{M}$ and the reversed character sequence $c_{N}\cdots c_{1}$ into
$w_{M}^{*}\cdots w_{1}^{*}$ by multiplying all the generated word
probabilities.

We denote $Z(d)$ as the set of all the possible segmentations for the sentence
$d$, then we are looking for:

$\mathop{\arg\max}_{W,W^{*}\in Z(d)}\prod_{w_{i}\in
W}p_{\theta}(w_{i}|ctx(w_{i}))\prod_{w_{i}^{*}\in
W^{*}}p_{\theta}(w_{i}^{*}|ctx(w_{i}^{*})$ (12)

However, it is a NP problem which can not be computed using dynamic
programming. We proposed two dynamic programming methods to approach the
solution as follows:

SGB-A  We can combine two probabilities (forward and backward) of a same word
by averaging them which is similar to the Figure 1 then use dynamic
programming algorithm to decode the best segmentation. We denote
$\hat{\alpha}_{t}^{k}$ as the best segmentation probability of character
sequence $c_{1:t}$ with final $k$ characters being a word and $\delta_{t}^{k}$
is used to trace back the decoding.

$\bar{p}(w_{j})=\sqrt{p_{\theta}(w_{j}|ctx(w_{j}))p_{\theta}(w_{j}^{*}|ctx(w_{j}^{*}))}$
(13) $\hat{\alpha}_{t}^{k}\ =\max\limits_{j=1}^{T}\ \bar{p}(w_{j})\
\hat{\alpha}_{t-k}^{j}$ (14)
$\delta_{t}^{k}=\arg\max_{j=1}^{T}\bar{p}(w_{j})\delta_{t-k}^{j}$ (15)

SGB-C  We can obtain the best segmentation separately using the two-side
probabilities by dynamic programming respectively and integrate all the word
boundaries to produce the final segmentation, resulting in a more fine-grained
result.

##  4 Experiments

###  4.1 Experimental Setting

Datasets  For Chinese word segmentation, we use the second SIGHAN Bakeoff
dataset to validate our model. The second SIGHAN Bakeoff Emerson (2005) have
four set of labeled data: AS, CITYU, MSR, PKU. AS and CITYU are written in
traditional Chinese, while MSR and PKU are written in simplified Chinese.In
similar to most of previous work, we combine the original training data with
test data as new training data, and only use test data for evaluation.For Thai
word segmentation, InterBest is a dataset in Thai used in the InterBest 2009
word segmentation contest Kosawat (2009).We use the “Novel” subset for
training and test data. The detail is shown in Table 2.

Table 2: Statistics of five corpora. Corpus | Word | Character
---|---|---
Types | Tokens | Types | Tokens
CITYU | 9001 | 40937 | 2953 | 66346
PKU | 13149 | 104373 | 3433 | 168975
MSR | 12923 | 106873 | 3341 | 180987
AS | 18811 | 122613 | 3884 | 196299
Novel | 22037 | 1522233 | 156 | 5426551

Preprocess  It is unfair to compare two unsupervised methods under different
preprocessing settings. Wang et al. (2011) proposed four kind of preprocessing
settings and we use setting 1, 3 and 4 to compare our model with previous
works:

  * •

Setting 1: Fully unsupervised condition.

  * •

Setting 3: All the punctuation marks are identified as delimiters in advance.

  * •

Setting 4: All the punctuation marks and other non-Chinese characters are
recognized and transformed into special symbols.

Set-up For our model, we choose LSTM as the language model component and set
the embedding size and the hidden size both 300. Adam algorithm is used for
the update rule with learning rate 0.001, and the number of iterates is to 10.
We set different batch sizes in consideration of size of each dataset. The
batch size of CITYU is 32, MSR is 64 , PKU is 16 , AS is 256 and Novel is 256.
The vocabulary sizes are equal to size of character set in each datasets. We
test the model with the maximum word length $T=3,4,5$ for Chinese word
segmentation and $T=12$ for Thai. We use F1-score on words for evaluation
which is the harmonic mean of precision and recall.

###  4.2 Result

We compare our model with some outstanding previous works on five datasets in
three settings. The detail information of all models is following:

  * •

nVBE: a variant method based on the branch entropy Magistry and Sagot (2012).

  * •

ESA: the model proposed by Wang et al. (2011) which choose the best value.

  * •

NPYLMT : $T$-gram Nested Pitman-Yor language model (Mochihashi et al., 2009).

  * •

PYHSMM: Pitman-Yor Hidden Semi-Markov Model (Uchiumi et al., 2015).

  * •

Joint: Joint model of hierarchical Dirichlet process model and character-based
hidden Markov model (Chen et al., 2014).

  * •

MCA: Bayesian model based on monolingual character (Teng et al., 2014).

  * •

SLMT: segmental language model proposed by Wang et al. (2017) and Sun and Deng
(2018) with maximum word length $T$.

Table 3: F1-score with setting 1 on Chinese word segmentation task. Models (%) | CITYU | MSR | PKU | AS
---|---|---|---|---
ESA | 72.3 | 76.4 | 75.0 | 76.4
SGB-A3 | 78.7 | 79.4 | 78.4 | 79.4
SGB-C3 | 77.4 | 80.2 | 79.6 | 78.6
SGB-A4 | 79.2 | 80.5 | 77.9 | 80.2
SGB-C4 | 80.0 | 74.0 | 80.0 | 81.0
SGB-A5 | 72.5 | 72.8 | 75.4 | 64.5
SGB-C5 | 78.5 | 80.4 | 78.4 | 82.4
Table 4: F1-score with setting 1 on Thai word segmentation task.  Models (%) | Novel
---|---
SGB-A12 | 80.1
SGB-C12 | 79.2
SLM12 | 79.6
PHYSMM | 82.1
nVBE | 82.1
Table 5: F1-score with setting 3 on Chinese word segmentation task Models (%) | CITYU | MSR | PKU | AS
---|---|---|---|---
nVBE | 77.5 | 78.2 | 77.9 | 72.9
ESA | 74.9 | 78.4 | 77.4 | 77.9
Joint | -/- | 81.7 | 81.1 | -/-
SGB-A3 | 79.5 | 80.6 | 80.4 | 81.9
SGB-C3 | 77.6 | 81.1 | 80.4 | 79.7
SGB-A4 | 80.3 | 80.6 | 80.3 | 82.7
SGB-C4 | 80.5 | 81.7 | 81.0 | 82.3
SGB-A5 | 78.3 | 80.1 | 79.1 | 82.8
SGB-C5 | 80.2 | 82.3 | 81.2 | 83.5
Table 6: F1-score with setting 4 on Chinese word segmentation task Models (%) | CITYU | MSR | PKU | AS
---|---|---|---|---
nVBE | 76.7 | 81.3 | 80.0 | 76.6
ESA | 76.0 | 80.1 | 77.8 | 78.5
NPY2 | 82.4 | 80.2 | -/- | -/-
NPY3 | 81.7 | 80.7 | -/- | -/-
PHYSMM | 82.6 | 82.9 | 81.6 | -/-
MCA | 77.9 | 82.4 | 80.7 | 80.6
SLM2 | 78.2 | 78.5 | 80.2 | 79.4
SLM3 | 80.5 | 79.4 | 79.8 | 80.3
SLM4 | 79.7 | 79.0 | 79.2 | 79.8
SGB-A3 | 79.5 | 82.7 | 80.9 | 81.7
SGB-C3 | 80.7 | 83.1 | 81.6 | 82.0
SGB-A4 | 80.5 | 81.7 | 79.4 | 83.0
SGB-C4 | 81.2 | 83.6 | 81.5 | 83.9
SGB-A5 | 78.7 | 82.6 | 79.9 | 82.3
SGB-C5 | 79.8 | 83.7 | 80.8 | 83.8

###  4.3 Disambiguation Analysis

Segmentation ambiguity is a very important factor influencing accuracy of word
segmentation systems (Huang and Zhao, 2007). We take Chinese word segmentation
as an example, there are two types of word boundary ambiguities: combination
ambiguity and overlap ambiguity.

Combination ambiguity  For any two character sequences in a sentence, denoted
by $x$ and $y$, if $xy$ can be combined together to form a word, yet at the
same time $x$ and $y$ also can function as a word respectively, then word
boundary ambiguity exists in these two character sequences.

Overlap ambiguity  If there is a word boundary ambiguity between $xy$ and
another character sequence that precedes or follows them, say $z$, and $xyz$
can be grouped into either $xy\,\,z$ or $x\,\,yz$, then there exists an
overlap ambiguity.

We counted two kinds of ambiguity error made by our models on MSR and PKU
datasets (the vocabulary is obtained from the gold test set) and compared
SGB-A3, SGB-C3 with SLM3 and nVBE. The result is shown in Figure 2.

Figure 2: Segmentation error analysis. (a) The errors of different models
caused by the combination ambiguity on MSR and PKU datasets. (b) The errors of
different models caused by the overlap ambiguity.

##  5 Discussion

###  5.1 Comparison

As shown in Table 3, 4, 5, and 6, our models outperform other approaches
almost with every setting across different datasets for Chinese word
segmentation. Under the setting 4, we surpassed state-of-the-art by $3.3\%$
increase in F1-score on AS and $0.8\%$ increase on MSR, and achieved the
compatible performance on PKU. We achieved new state-of-the-art under the
setting 3 on CITYU and the decent results under the setting 4. Under the fully
unsupervised situation (i.e. the setting 1), our models still perform well,
and achieved more than 80% accuracy on all the datasets. Our model is
evaluated on Thai that have longer word length in average than Chinese, and we
also achieved the comparable result comparing to others.

Because the concept of words is not well defined in Chinese, different
datasets were constructed following the different guidelines. Huang and Zhao
(2007) estimated the the lowest consistency rate $0.848$ between four datasets
which can be regarded as the upper bound for unsupervised Chinese word
segmentation models. The result of our model is very close to this ceiling.

We found that our combining model achieve higher F1-scores than the average
model on the most cases, while the averaging one show to be the better in word
disambiguation. Combining model leads to more fine-grained segmentation
results which helps to isolate the function words from the other words. When
the maximum length of words $T$ increases, the averaging model will suffer
from the problem of function word adhesion (the function words can not be
properly isolated). In contrast, the combining model always segments $xyz$
into $x\,\,y\,\,z$ rather than $xy\,\,z$ or $x\,\,yz$. Therefore, it makes the
combining model hard to deal with the problem of word disambiguation because
it tends to produce the results agreed by the both language models.

###  5.2 Error Analysis

The bidirectional nature of our models allows them leverage the post-text
information to determine the left boundary of the candidate segments. We take
two sentences as examples: “我从小学唱歌” (I started learning to sing when I was
young), and “我从小学毕业” (I graduated from primary school). The segment “从小学” can
be clearly split from both sides, but there is an overlap ambiguity inside.
Since segment ”从小学” in these sentences have the same preceding text (”我”), no
matter what the following word is (keep the boundary on right side), the one-
side model SLM will split the segment in the same way which is determined by
the result of comparing $p(\mbox{从小}|\mbox{我})p(\mbox{学}|\mbox{我从小})$ with
$p(\mbox{从}|\mbox{我})p(\mbox{小学}|\mbox{我从})$. However our two-side model will
refine the results by introducing the generation probability of segments given
the context from the right side. The occurrence of “唱歌” (sing) will increase
the probability of that “学” (learn) is identified as a single word while the
words “毕业” (graduate) and “小学” (primary school) are often occur together which
establishes the left word boundary of “小学”. It is in accordance with the idea
of branch entropy that uses the entropies from both sides to segment words. In
addition, although our combining model can not handle the overlap ambiguity,
the post contexts help to better segment the previous words.

We find that the error of function word recognition is one of the main
drawbacks of many existing approaches. Function words occur more frequently
than the common words, and could be assigned with a higher probability by the
language model, which causes these words easily to be attached with other
words. Our combining model is able to handle such problem thank to the bi-
directional language models. It can successfully establish the boundaries
between the function words and next words.

Thai has less character types and longer word length in average than Chinese,
which makes the models hard to accurately approximate the generation
probabilities. As to our combining model, it tends to get fine-grated results
that are not optimal for Thai. We leave it for future studies. Although our
models did not define new state-of-the-art on Thai, we still achieved the
comparable results on the Novel dataset.

##  6 Conclusion

We have described a novel unsupervised segmentation model augmented with bi-
directional neural language models. Assuming that a good segmentation
generally contributes to increase the generation possibility of sentences, the
model’s parameters are trained by maximizing such sentence generation
probability conditioned on all the possible segmentation. The bi-directional
nature of networks allows us to capture the semantic-rich context features for
each possible segment, aiming to better reconcile word boundary ambiguities.
Two decoding algorithms were also proposed to combine the context features
from both directions. One is to produce the segmentation by taking the average
of segment’s probabilities estimated by the forward and backward language
models. Another is to generate the segmentation by merging their results
produced separately by the two language models.The former revealed better in
word boundary ambiguity reconciliation, while the latter achieved the higher
overall performance. Experimental results demonstrated that our context-
sensitive unsupervised segmentation model achieved state-of-the-art on
multiple Chinese data sets, and the comparable result on Thai in which the
words are formed by more characters in average than those in Chinese.

## References

  * Bengio et al. (2003) Yoshua Bengio, Réjean Ducharme, Pascal Vincent, and Christian Jauvin. 2003.  A neural probabilistic language model.  _Journal of machine learning research_ , 3(Feb):1137–1155.
  * Cattell (1886) James McKeen Cattell. 1886.  The time it takes to see and name objects.  _Mind_ , 11(41):63–65.
  * Chen et al. (2014) Miaohong Chen, Baobao Chang, and Wenzhe Pei. 2014.  A joint model for unsupervised chinese word segmentation.  In _Proceedings of the 2014 Conference on Empirical Methods in Natural Language Processing (EMNLP)_ , pages 854–863.
  * Cho et al. (2014) Kyunghyun Cho, Bart Van Merriënboer, Caglar Gulcehre, Dzmitry Bahdanau, Fethi Bougares, Holger Schwenk, and Yoshua Bengio. 2014.  Learning phrase representations using rnn encoder-decoder for statistical machine translation.  _arXiv preprint arXiv:1406.1078_.
  * Emerson (2005) Thomas Emerson. 2005.  The second international chinese word segmentation bakeoff.  In _Proceedings of the fourth SIGHAN workshop on Chinese language Processing_.
  * Feng et al. (2004) Haodi Feng, Kang Chen, Xiaotie Deng, and Weimin Zheng. 2004.  Accessor variety criteria for chinese word extraction.  _Computational Linguistics_ , 30(1):75–93.
  * Goldwater et al. (2006) Sharon Goldwater, Thomas L Griffiths, and Mark Johnson. 2006.  Contextual dependencies in unsupervised word segmentation.  In _Proceedings of the 21st International Conference on Computational Linguistics and the 44th annual meeting of the Association for Computational Linguistics_ , pages 673–680. Association for Computational Linguistics.
  * Goldwater et al. (2009) Sharon Goldwater, Thomas L Griffiths, and Mark Johnson. 2009.  A bayesian framework for word segmentation: Exploring the effects of context.  _Cognition_ , 112(1):21–54.
  * Hochreiter and Schmidhuber (1997) Sepp Hochreiter and Jürgen Schmidhuber. 1997.  Long short-term memory.  _Neural computation_ , 9(8):1735–1780.
  * Huang and Zhao (2007) Changning Huang and Hai Zhao. 2007.  Chinese word segmentation: A decade review.  _Journal of Chinese Information Processing_ , 21(3):8–20.
  * Jin and Tanaka-Ishii (2006) Zhihui Jin and Kumiko Tanaka-Ishii. 2006.  Unsupervised segmentation of chinese text by use of branching entropy.  In _Proceedings of the COLING/ACL on Main conference poster sessions_ , pages 428–435. Association for Computational Linguistics.
  * Jozefowicz et al. (2016) Rafal Jozefowicz, Oriol Vinyals, Mike Schuster, Noam Shazeer, and Yonghui Wu. 2016\.  Exploring the limits of language modeling.  _arXiv preprint arXiv:1602.02410_.
  * Kitt and Wilks (1999) Chunyu Kitt and Yorick Wilks. 1999.  Unsupervised learning of word boundary with description length gain.  _EACL 1999: CoNLL-99 Computational Natural Language Learning_.
  * Kong et al. (2015) Lingpeng Kong, Chris Dyer, and Noah A Smith. 2015.  Segmental recurrent neural networks.  _arXiv preprint arXiv:1511.06018_.
  * Kosawat (2009) Krit Kosawat. 2009.  Interbest 2009: Thai word segmentation workshop.  In _Proceedings of 2009 Eighth International Symposium on Natural Language Processing (SNLP2009), Thailand_.
  * Li et al. (2009) Xingshan Li, Keith Rayner, and Kyle R Cave. 2009.  On the segmentation of chinese words during reading.  _Cognitive Psychology_ , 58(4):525–552.
  * MacEachern and Müller (1998) Steven N MacEachern and Peter Müller. 1998.  Estimating mixture of dirichlet process models.  _Journal of Computational and Graphical Statistics_ , 7(2):223–238.
  * Magistry and Sagot (2012) Pierre Magistry and Benoît Sagot. 2012.  Unsupervized word segmentation: the case for mandarin chinese.  In _Proceedings of the 50th Annual Meeting of the Association for Computational Linguistics: Short Papers-Volume 2_ , pages 383–387. Association for Computational Linguistics.
  * Mikolov et al. (2010) Tomáš Mikolov, Martin Karafiát, Lukáš Burget, Jan Černockỳ, and Sanjeev Khudanpur. 2010.  Recurrent neural network based language model.  In _Eleventh Annual Conference of the International Speech Communication Association_.
  * Mochihashi et al. (2009) Daichi Mochihashi, Takeshi Yamada, and Naonori Ueda. 2009.  Bayesian unsupervised word segmentation with nested pitman-yor language modeling.  In _Proceedings of the Joint Conference of the 47th Annual Meeting of the ACL and the 4th International Joint Conference on Natural Language Processing of the AFNLP: Volume 1-Volume 1_ , pages 100–108. Association for Computational Linguistics.
  * Pitman and Yor (1997) Jim Pitman and Marc Yor. 1997.  The two-parameter poisson-dirichlet distribution derived from a stable subordinator.  _The Annals of Probability_ , pages 855–900.
  * Rabiner (1989) Lawrence R Rabiner. 1989.  A tutorial on hidden markov models and selected applications in speech recognition.  _Proceedings of the IEEE_ , 77(2):257–286.
  * Sproat and Shih (1990) Richard Sproat and Chilin Shih. 1990.  A statistical method for finding word boundaries in chinese text.  _Computer Processing of Chinese and Oriental Languages_ , 4(4):336–351.
  * Sun and Deng (2018) Zhiqing Sun and Zhi-Hong Deng. 2018.  Unsupervised neural word segmentation for chinese via segmental language modeling.  _arXiv preprint arXiv:1810.03167_.
  * Teh et al. (2005) Yee W Teh, Michael I Jordan, Matthew J Beal, and David M Blei. 2005.  Sharing clusters among related groups: Hierarchical dirichlet processes.  In _Advances in neural information processing systems_ , pages 1385–1392.
  * Teh (2006) Yee Whye Teh. 2006.  A hierarchical bayesian language model based on pitman-yor processes.  In _Proceedings of the 21st International Conference on Computational Linguistics and the 44th annual meeting of the Association for Computational Linguistics_ , pages 985–992. Association for Computational Linguistics.
  * Teng et al. (2014) Zhiyang Teng, Hao Xiong, and Qun Liu. 2014.  Unsupervised joint monolingual character alignment and word segmentation.  In _Chinese Computational Linguistics and Natural Language Processing Based on Naturally Annotated Big Data_ , pages 1–12. Springer.
  * Uchiumi et al. (2015) Kei Uchiumi, Hiroshi Tsukahara, and Daichi Mochihashi. 2015.  Inducing word and part-of-speech with pitman-yor hidden semi-markov models.  In _Proceedings of the 53rd Annual Meeting of the Association for Computational Linguistics and the 7th International Joint Conference on Natural Language Processing (Volume 1: Long Papers)_ , volume 1, pages 1774–1782.
  * Wang et al. (2017) Chong Wang, Yining Wang, Po-Sen Huang, Abdelrahman Mohamed, Dengyong Zhou, and Li Deng. 2017.  Sequence modeling via segmentations.  _arXiv preprint arXiv:1702.07463_.
  * Wang et al. (2011) Hanshi Wang, Jian Zhu, Shiping Tang, and Xiaozhong Fan. 2011.  A new unsupervised approach to word segmentation.  _Computational Linguistics_ , 37(3):421–454.
  * Yee (1986) Suen Ching Yee. 1986.  _Computational studies of the most frequent Chinese words and sounds_ , volume 3.  World Scientific.
  * Zhao and Kit (2008) Hai Zhao and Chunyu Kit. 2008.  An empirical comparison of goodness measures for unsupervised chinese word segmentation with a unified framework.  In _Proceedings of the Third International Joint Conference on Natural Language Processing: Volume-I_.