Not logged in. · Lost password · Register

nudelsalat
Avatar
Member since Apr 2014
13 posts
Subject: Probeklausur/2.1
Heya,

hat jemand eine Idee, was kaputt gegangen ist?
https://wwwcip.cs.fau.de/~av37umic/thprog/pk-2.1.pdf

1. Warum bekomme ich für c nichts raus
2. Wieso widersprechen sich die zwei Varianten von a (je nachdem ob aufgelöst oder nicht), wenn man die erwartete Lösung als gegeben betrachtet?
Marcel[Inf]
#faui2k15, GTI-Tutor a. D.
Member since Nov 2015
622 posts
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.
This post was edited on 2017-10-07, 17:18 by Marcel[Inf].
nudelsalat
Avatar
Member since Apr 2014
13 posts
Hier auch nochmal vielen Dank! :)
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen