\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}