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.
Alpha Äquivalenz
Muss man bei der Alpha Äquivalenz wenn man zwei geschachtelte Terme hat die Variablen in beiden ersetzen oder geht es auch nur im inneren? Bsp. λabc.(λa.aa)ab
Kann ich das zu λabc.(λb.bb)ab machen oder muss ich die anderen a auch umbenennen/substituieren?
Die beiden von dir angegebenen Terme sind tatsächlich alpha-äquivalent. Wenn ich mich recht erinnere, sollte alpha-Äquivalenz auch die folgende Eigenschaft habe:
Wenn t und t’ alpha-äquivalent, dann auch C(t) und C(t’), wobei C(.) ein Kontext ist.
Ich würde gerne noch eine zweite Meinung dazu hören 
Möglicherweise stand das im ThProg Skript irgendwo.
Das heißt ich subsituiere für jedes Lambda separat?
Mein Verständnis: Bei der α-Äquivalenz geht es allgemein darum das nur verschiedene (gebundene) Symbole verwendet werden, für die gleiche “Berechnung”. Dh. λx.x und λy.y sind beides Identitätsfunktionen, denn (λx.x)a = (λy.y)b, ⇔ a = b. Dieses muss natürlich nicht auf globaler eben stattfinden, sondern auch in einem beliebigem Kontex (“geschachtelt”), insofert es von den gebundenen Variablen zugelassen wird, bzw. diese korrekt geschattet werden.
Ich verstehe nicht, was du formal ausdrücken willst.
Naja ob ich λabc.(λa.aa)ab zu λabc.(λb.bb)ab machen kann oder es bei einer Substitution zu λbbc.(λb.bb)bb wird, da man alle a durch b ersetzen muss. Verständlicher???
[quote=elias007]
Naja ob ich λabc.(λa.aa)ab zu λabc.(λb.bb)ab machen kann[/quote]
Das hatte ich oben schon beantwortet: ja, die beiden sind alpha-äquivalent 
Nein, das wäre falsch! Der Teil der Definition von Substitutionen auf Lambda-Termen, der dagegen spricht, ist imo sehr wesentlich. Ich empfehle dir, das Skript an der Stelle nochmal zu lesen. Bei uns gab es früher auch eine Übungsaufgabe dazu.
Nein, das macht keinen Sinn wenn du dir den Sinn hinter dem Begriff der α-Äquivalenz überlegst.
Wie meinst du das? So wie ich es verstanden habe wird Alpha-Äquivalenz auf einen Lambda-Terme angewandt. Hat dieser wieder innere Lambda Terme sind diese Separat zu betrachten. Stimmt das?
α-Äquivalenz ist ja eher eine Relation zwischen zwei syntaktisch-unterschiedlichen Termen, als ein Operator oder eine Funktion. Wenn man zwei Terme hat, von denen man sagen kann dass sie α-äquivalent sind, weiß man wie bereits oben gesagt, das sie das gleiche „Berechnen“. Die Wahl der Symbole hat grundsätzlich keine Bedeutung für die Semantik eines Lamba-Terms, bis auf die Ausname mit Namenskollisionen (denk an λx.xy und λy.yy).
Stell dir z.b. in Python (mir bewusst, nicht perfekt) vor was
map(lambda x: x*x, [1, 2, 3, 4])und
map(lambda y: y*y, [1, 2, 3, 4])ergeben? Genau das gleiche, da [m]lambda y: yy[/m] für alle eingaben, das gleiche wie [m]lambda x: xx[/m] auswertet, wo jeweils [m]y[/m] und [m]x[/m] ein Wert gebunden bekommt.
Vergleiche das dann mit
y = -1
map(lambda x: x*y, [1, 2, 3, 4])und
y = -1
map(lambda y: y*y, [1, 2, 3, 4])wo man sich daran erinnert das das zweite [m]y[/m] das globale schattet. Das eine mal hat man [m][-1, -2, -3, -4][/m] und das andere [m][1, 4, 9, 16][/m] da jeweils das zweite [m]y[/m] eine andere Bedeutung hatte, dh. anders ausgewertet wurde, dh. die beiden [m]lambda[/m]s sind nicht α-äquivalent.
1 „Gefällt mir“
Verstehe ich das richtig, dass du u.a. damit sagen willst, dass man Lambdas immer verschieden auswertet, egal ob sie ineinander geschachtelt sind?
Wie meinst du “verschieden auswertet”?
“Auswertung” wird mittels Reduktion gemacht, zumindest im Lambda-Kalkül, da haben wir ja verschiedene Mechanismen kennengelernt wie man da vorgehen kann, da ist ja nichts gesagt worden von “verschiedener” Auswertung (abgesehen von nicht -determinismus der beta-reduktion, afair).
Ich hab gemeint, dass man zuerst das innere Lambda auswertet und dabei Variablen ersetzen kann. Wenn man das äußere Lambda auswertet, dann kann man die Variablen wieder anders ersetzen, auch wenn es z.B: zweimal y hieß. Stimmt doch so?
Was heißt für dich “auswerten”? Ich verstehe leider die Frage nicht. Kannst du die Frage eventuell mit mehr Formalität stellen?
Ich habe das Gefühl, dass du möglicherweise ganz konkrete Dinge vor Augen hast/Dinge, die du auf dem Papier tun möchtest, die ein bisschen schwierig sind, über ein Forum zu kommunizieren.
Mir geht es eigentlich nur darum, ob man bei einem inneren Lambda die Variablen anders ersetzen kann wie bei einem äußeren (auch wenn die Variablennamen gleich sind).
Ja, das innere und äußere a sind andere, das ist ja das was ich die ganze zeit mit überschatten sage.
Passt. Dann habe ich bisher alles richtig gemacht