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