\newcommand{\dom}{\operatorname{dom}}
\newcommand{\img}{\operatorname{img}}
\newcommand{\Term}{\operatorname{Term}}

\begin{slide}{Substitutionen (Definition)}

\begin{itemize}
\item Signatur $\Sigma=\Sigma_0\cup\ldots\Sigma_k$,
\item $\Term(\Sigma,V)$ ist kleinste Menge $T$ mit
  $V\subseteq T$ und $\forall 0\le i\le k, f\in\Sigma_i, t_1\in
  T,\ldots,t_i\in T: f(t_1,\ldots,t_i)\in T$.

 (hier Anwendung für Terme, die Typen beschreiben)

\item Substitution: 
  partielle Abbildung $\sigma:V\to\Term(\Sigma,V)$,

  Definitionsbereich: $\dom \sigma$, 
  Bildbereich: $\img \sigma$.

\item Substitution $\sigma$ auf Term $t$ anwenden: $t\sigma$

\item $\sigma$ heißt \emph{pur}, 
  wenn  kein $v\in\dom \sigma$ 
    als Teilterm in  $\img\sigma$ vorkommt.

\end{itemize}
\end{slide}

\newcommand{\lesim}{\raisebox{-8pt}[0pt][0pt]{$\stackrel{\displaystyle <}{\sim}$}}

\begin{slide}{Substitutionen: Produkt}
Produkt von Substitutionen: 
$t (\sigma_1 \circ \sigma_2) = (t \sigma_1) \sigma_2$

\bigskip

Beispiel 1:

$\sigma_1=\{X\mapsto Y\}, \sigma_2 = \{Y\mapsto a\},
\sigma_1 \circ \sigma_2 = \{ X\mapsto a, Y\mapsto a\}$.

Beispiel 2 (nachrechnen!):

$\sigma_1 = \{X\mapsto Y\}, \sigma_2=\{Y \mapsto X\},
\sigma_1\circ\sigma_2 = \sigma_2$

Eigenschaften:
\begin{itemize}\itemsep 0pt
\item $\sigma$ pur $\Rightarrow$ $\sigma$ idempotent: 
$ \sigma \circ \sigma= \sigma$
\item
  $\sigma_1$ pur $\wedge$ $\sigma_2$ pur 
  impliziert nicht $\sigma_1\circ \sigma_2$ pur
\end{itemize}

Implementierung:
\begin{verbatim}
import Data.Map 
type Substitution = Map Identifier Term
times :: Substitution -> Substitution -> Substition
\end{verbatim}




\end{slide}

\begin{slide}{Substitutionen: Ordnung}

Substitution $\sigma_1$ ist \emph{allgemeiner als}
Substitution $\sigma_2$:

$\sigma_1 \lesim \sigma_2 \iff 
\exists \tau : \sigma_1 \circ \tau = \sigma_2$


Beispiele: 
\begin{itemize}
\item
$\{X\mapsto Y\} \lesim \{X\mapsto a,Y\mapsto a\}$,
\item
$\{X\mapsto Y\}\lesim\{Y\mapsto X\}$,
\item $\{Y\mapsto X\}\lesim\{X\mapsto Y\}.$
\end{itemize}

Eigenschaften
\begin{itemize}
\item 
Relation $\lesim$ ist Prä-Ordnung 
(\dots, \dots, aber nicht \dots)
\item
Die durch $\lesim$ erzeugte Äquivalenzrelation
ist die \dots
\end{itemize}

\end{slide}

\newcommand{\mgu}{\operatorname{mgu}}

\begin{slide}{Unifikation---Definition}

Unifikationsproblem 
\begin{itemize}\itemsep 1pt
\item Eingabe: Terme $t_1,t_2\in\Term(\Sigma,V)$
\item Ausgabe: ein allgemeinster Unifikator (mgu): 
  Substitution $\sigma$ mit $t_1\sigma = t_2\sigma$.
\end{itemize}

(allgemeinst: infimum bzgl. $\lesim$)


Satz: jedes Unifikationsproblem ist 
\begin{itemize}\itemsep 1pt
\item entweder gar nicht 
\item oder bis auf Umbenennung eindeutig 
\end{itemize}
lösbar.


\end{slide}

\begin{slide}{Unifikation---Algorithmus}

  $\mgu(s, t)$ nach Fallunterscheidung
  \begin{itemize}\itemsep 1pt
  \item $s$ ist Variable: \dots
  \item $t$ ist Variable: symmetrisch
  \item $s=(s_1 \to s_2)$ und $t=(t_1 \to t_2)$: \dots
  \end{itemize}

\begin{verbatim}
mgu :: Term -> Term -> Maybe Substitution
\end{verbatim}
  

\end{slide}

\begin{slide}{Unifikation---Komplexität}
Bemerkungen:
\begin{itemize}\itemsep 1pt
\item gegebene Implementierung ist korrekt, 
  übersichtlich, aber nicht effizient,
\item (Ü) es gibt Unif.-Probl. mit exponentiell großer Lösung,
\item eine komprimierte Darstellung davon 
  kann man aber in Polynomialzeit ausrechnen.
\end{itemize}
  
\end{slide}
