Was kann weggelassen werden?
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.
Hindley/Milner: Prinzipialtyp
Wenn wir den PT-Algorithmus fertig ausgewertet haben erhalten wir ja eine Menge mit meist mehreren Gleichungen und Variablen die uns letztendlich auf den Typ des gesamten Terms führen. Können wir nun von dieser Menge direkt auf den Typ des gesamten Terms a schließen (reicht also {a=…, …}) oder müssen wir die ganze Menge nach den Umformungen (also {a=…, b=…, c =…}) noch einmal hinschreiben? Beim mgu das selbe, reicht […/a, …] oder müssen wir den Typ jeder vorkommenden Variable erwähnen?
Das kommt ganz darauf an, was gefragt ist. 
Vielleicht verstehe ich aber auch die Frage gerade nicht ganz. Wenn man sowieso Umformungen durch den Unifikationsalgorithmus durchgeführt hat, steht doch am Schluss sowieso nochmal das ganze System da?
Aber kann man sich den Unifikationsalgorithmus (wenn ich das richtig verstehe ist das der mit dem elim, dec und orient) auch sparen und gleich den Typ des Termes hinschreiben nachdem mann die vollständige PT-Menge berechnet hat? Hier ein Bild wie ich es dann machen würde für PT(Γ;s;a): https://cl.ly/mzj7
Ich verstehe zwar das es bestimmt sinnvoll ist den Unifikationsalgorithmus zu machen, letztendlich kann man bei den einfachen Mengen die wir haben aber finde ich einfach so sehen was der Typ ist. Auch wurde der Unifikationsalgorithmus (von dem ja letztendlich die finale Menge für alle vorkommenden Typvariablen abhängt) nur am Rande in den Übungen erwähnt (die Regeln stehen ja auch nicht im Skript so weit ich weis, in GLoIn eventuell aber das hatte ich noch nicht).
Deswegen sage ich ja, es kommt darauf an, was gefragt ist. Wenn die Aufgabe lautet, den Unifikationsalgorithmus durchzuführen (was allerdings wie du schon sagst Stoff von GLoIn ist), dann muss man es machen (man würde es bei einer Implementierung des Algorithmus ja auch nicht weglassen, weil es “offensichtlich” ist), aber ich verweise da einfach mal auf die Probeklausur, Aufgabe 2. In dem unten angegebenen Hinweis steht ja schon, was du wissen willst.
1 „Gefällt mir“