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.
Typisierungsregeln - wie kommt man auf alpha?
Hi, mir ist nicht ganz klar wie man beim einfach getypten λ-Kalkül in beiden Ergebnissen auf α kommt? Hab mal einen Screenshot angehängt.
Wird das aus dem Kontext ersichtlich?
Attachment:
Bildschirmfoto 2019-09-30 um 14.22.08.png: https://fsi.cs.fau.de/unb-attachments/post_161544/Bildschirmfoto 2019-09-30 um 14.22.08.png
Genauso wie du auf den Typen von \beta kommst: indem du die Typisierungsregeln anwendest.s ist ja auch einfach
nur ein Term von dem du den Typen wissen willst. Nachdem du dann \alpha ausgerechnet hast kannst du den Typen
dann auf der linken Seite einsetzen. In der Praxis machts dann Sinn (falls \alpha nicht offensichtlich ist), dass du erstmal
etwas Platz auf deinem Blatt laesst, erst alles durchrechnest und erst falls die Rechnung geklappt hast alles einsetzt.
Tatsächlich glaube ich, dass das hier asymmetricher ist als so gesagt. Das sieht an auch am Prinzipaltypen PT-Algorithmus, dass genau an dieser Stelle eine frische Variable eingeführt wird und erst durch in späteren Schritten aufgedeckte Unifikationsgleichungen genauer bestimmt wird.
Genau wie auf dem Blatt Papier muss hier erstmal (im nicht offensichtlichen Fall) ein Platzhalter hergenommen werden.
1 „Gefällt mir“