[LOS] normal-order reduction sequenz Seite 95
2005-08-13 14:22
Johannes
Die ersten beide Schritte bis zu
(<l>w. <l>y. (<l>z. <l>w. z)yy)(<l>z. <l>w. z) (1)
verstehe ich.
Allerdings ist mir denn der Schritt zu
<l>y. (<l>z. <l>w. z)yy (2)
unklar.
Ich würde denken, das in (1) zuerst (weil normal-order) <l>w bearbeitet wird. Ergibt sich (2) dann einfach dadurch, das keine Variable w in "<l>y. (<l>z. <l>w. z)yy" enthalten ist?
Was genau sagt mir der (*), also warum ist hier die Reduktion eigentlich beendet, und warum wird dann trotzdem weiter reduziert?
Ist die Reduktion bei (*) (eigentlich) beendet, weil hier das erste mal eine Kanonische Form = Abstraktion = <l><var>. <exp> auftritt?
(<l>w. <l>y. (<l>z. <l>w. z)yy)(<l>z. <l>w. z) (1)
verstehe ich.
Allerdings ist mir denn der Schritt zu
<l>y. (<l>z. <l>w. z)yy (2)
unklar.
Ich würde denken, das in (1) zuerst (weil normal-order) <l>w bearbeitet wird. Ergibt sich (2) dann einfach dadurch, das keine Variable w in "<l>y. (<l>z. <l>w. z)yy" enthalten ist?
Was genau sagt mir der (*), also warum ist hier die Reduktion eigentlich beendet, und warum wird dann trotzdem weiter reduziert?
Ist die Reduktion bei (*) (eigentlich) beendet, weil hier das erste mal eine Kanonische Form = Abstraktion = <l><var>. <exp> auftritt?