Not logged in. · Lost password · Register

RaspberryPie
Avatar
Member since Nov 2017
92 posts
Subject: 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?
So ist das in der Welt. Der eine hat den Beutel, der andre hat das Geld.
The author has attached one file to this post:
Bildschirmfoto 2019-09-30 um 14.22.08.png | Save   31.1 kBytes, downloaded 88 times
Jonas S
Member since Jul 2016
101 posts
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.
Marcel[Inf]
#faui2k15, GTI-Tutor a. D.
Member since Nov 2015
619 posts
+1 Jonas S
Quote by Jonas S:
Genauso wie du auf den Typen von \beta kommst
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.
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