\begin{slide}{Motivation}

Bisher: Typ-Deklarationspflicht für Variablen in Lambda.

scheint sachlich nicht nötig. In vielen Beispielen kann man
die Typen einfach rekonstruieren:
\begin{verbatim}
let { t = \ f x -> f (f x) 
    ; s = \ x -> x + 1
    } in t s 0
\end{verbatim}

\bigskip
Diesen Vorgang automatisieren!

(zunächst für einfaches (nicht polymorphes) Typsystem)

\end{slide}

\begin{slide}{Realisierung mit Constraints}

Inferenz für Aussagen der Form \( E \vdash X : (T, C) \)
\begin{itemize}
\item $E$: Umgebung (Name $\to$ Typ)
\item $X$: Ausdruck (Exp)
\item $T$: Typ
\item $C$: Menge von Typ-Constraints
\end{itemize}

wobei
\begin{itemize}
\item Menge der Typen $T$ erweitert um Variablen
\item Constraint: Paar von Typen $(T_1, T_2)$
\item Lösung eines Constraints: Substitution $\sigma$ mit
  $T_1 \sigma = T_2 \sigma$
\end{itemize}



\end{slide}
