\begin{frame}[t]
  \frametitle{Constructing Reduction Orders}
  
  Idea: give semantics to terms by interpreting them into an algebra.
  \pause
  
  \begin{definition}%[$\Sigma$-algebra $(A,\lbrack \cdot \rbrack)$]
  A $\Sigma$-algebra $(A,\interpret{\cdot})$ consists of:
  \begin{itemize}
    \item a non-empty set $A$,
    \item and for every $f \in \Sigma$ an \emph{interpretation function} $\interpret{f}{:}\ A^{\xar(f)} \to A$.
  \end{itemize}
  \end{definition}
  \pause
  
  \begin{example}[We use the $\Sigma$-algebra $(\nat,\interpret{\cdot})$ with]
  \vspace{-1.5em}
  \begin{align*}
    \interpret{0} &= 1 & \interpret{{\rm s}}(x) &= x+1 & \interpret{{\rm A}}(x,y) &= x + 2\cdot y
  \end{align*}
  \vspace{-2.2em}
  \begin{center}
    \only<3->{\includegraphics{../graphics/pstricks/reduction_semantic}}
  \end{center}
  \vspace{-.5em}
  \end{example}
\end{frame}