Unifikation höherer Ordnung

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

Beweis: Reduktion von Unifikation höherer Ordnung.

Def HO-Unifikation:

• Eingabe: einfach getypte Lambda-Terme s, t,
• Ausgabe: getypte Substitution $\sigma$ mit s$\sigma$ $\leftrightarrow^{*}_{}$ t$\sigma$

Satz: HO-Unifikation ist unentscheidbar.

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

Gilles Dowek: http://www.lix.polytechnique.fr/~dowek/Publi/unification.ps