45/87
\begin{frame}[t]
\frametitle{Transfinite Reductions}

\vspace{-2ex}
\begin{definition}
Let $\alpha$ be an ordinal,
and $\tau : (t_\beta \to t_{\beta+1})_{\beta < \alpha}$ a sequence of reduction steps.
\medskip\pause

We use $d_\beta$ to denote the depth of the rewrite step $t_\beta \to t_{\beta+1}$.
\bigskip\pause

Then $\tau$ is an \alert{infinite reduction} of length $\alpha$ if for every limit ordinal $\lambda < \alpha$:
\begin{enumerate}
\item
the distance $d(t_\beta,t_\lambda)$ tends to $0$,
\hfill\textcolor{gray}{$\forall \epsilon > 0. \; \exists \beta < \lambda. \; \forall \beta < \gamma < \lambda.\; d(t_{\gamma},t_\lambda) \le \epsilon$}
\item
the depth $d_\beta$ tends to infinity
\hfill\textcolor{gray}{$\forall n. \; \exists \beta < \lambda. \; \forall \beta < \gamma < \lambda.\; d_\gamma \ge n$}
\end{enumerate}
as $\beta$ approaches $\lambda$ from below.
\end{definition}
\pause

\alt<5>{
\begin{example}[We want more than Cauchy-convergence\ldots]
Let $R = \{f(x) \to f(c(x))\}$. Condition (2) excludes sequences like:
$$f(a) \to_\epsilon f(c(a)) \to_\epsilon f(c(c(a))) \to_\epsilon \ldots \to^\omega_\epsilon f(c^\omega) \to \ldots$$
where the \alert{activity does not move downwards}.
\end{example}
}{
\begin{example}
Let $R = \{a \to a,\; b\to b\}$. Condition (1) excludes \alert{jumps in the limit}:
$$a\to a \to a \to \ldots \underbrace{b}_{t_\omega} \to b \to \ldots$$
\end{example}
}
\end{frame}