Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Probeklausur/2.1
Heya,
hat jemand eine Idee, was kaputt gegangen ist?
https://wwwcip.cs.fau.de/~av37umic/thprog/pk-2.1.pdf
- Warum bekomme ich für c nichts raus
- Wieso widersprechen sich die zwei Varianten von a (je nachdem ob aufgelöst oder nicht), wenn man die erwartete Lösung als gegeben betrachtet?
Hey nudelsalat,
Paste aus meinen Kommentaren in #faui2k15:
Erstmal für’s Archiv, falls das CIP-Bild verloren geht 
Das Bild zeigt den PT-Algorithmus für λ→ auf Aufgabe 2.1 angewandt. Beachte schon hier, dass die Aufgabe explizit Elemente von System F (den Allquantor in N) nutzt, wir also von vornherein keine Garantien haben, dass der PT-Algorithmus funktioniert (der Typcheck in System F ist dazu auch unentscheidbar).
Der berechnete Prinzipaltyp ist ((N → N) → N → c) → c. c ist hier eine freie Variable, d. h. der Term hat unendlich viele Typen, die alle durch Substitution in diesem Prinzipaltypen hervorgehen.
Der zu zeigende Typ für den Term ist: N → N.
Der Widerspruch (N->N)->N->c = N->N ist nur scheinbar, da N einen Allquantor in seiner Definition besitzt. Also ist diese Gleichung nicht so einfach syntaktisch zu betrachten.
Nehmen wir mal c = N, d.h. στ mit τ = [N/c], was auch eine Lösung des Typproblems ist.
Dann haben wir ((N->N) → N → N) → N als möglichen Typen seitens des PT-Algorithmus.
Betrachten wir die Defintion N = ∀a. (a->a) → a → a, dann sehen wir, dass insbesondere (N->N) → N → N für [N/a] eine Instanz ist.
“Substituieren” wir das im Typen oben, erhalten wir: ((N->N) → N → N) → N = N → N. Voilà, dasselbe Ergebnis wie gefordert.
Fazit
Nur “λ→” => PT-Algorithmus geht.
“System F” => PT-Algorithmus geht nicht, nutze die “Baumherleitung”.
“ML Polymorphie” => Modifizierter PT-Algorithmus geht.
Hier auch nochmal vielen Dank! 