\begin{slide}{Unifikation höherer Ordnung}

Satz: Typrekonstruktion für System F (beliebiger Rang)
ist unentscheidbar.

Beweis: Reduktion von Unifikation höherer Ordnung.

Def HO-Unifikation: 
\begin{itemize}
\item Eingabe: einfach getypte Lambda-Terme $s,t$,
\item Ausgabe: getypte Substitution $\sigma$ mit $s\sigma \leftrightarrow^* t\sigma$
\end{itemize}

Satz: HO-Unifikation ist unentscheidbar.

Beweis: Reduktion von Hilberts 10. Problem
(ganzzahlige Lösungen polynomieller Gleichungssysteme),
Codierung mit Church-Zahlen.

Gilles Dowek: \url{http://www.lix.polytechnique.fr/~dowek/Publi/unification.ps}

\end{slide}
