Lambda-Kalkül Beta Reduktion spezifische Schritte und warum

Question

Von einem Buch, das ich vor kurzem gerade lese:

Erstens:

.(..)()((.)) Die äußerste Lambda-Bindung ist, an dieser Stelle, nicht reduzierbar, weil es kein Argument hat anzuwenden zu. Was bleibt, ist, in die Begriffe Schicht für Schicht zu gehen, bis wir etwas Reduzierbares finden.

Next:

.(.)((.)) Wir können das Lambda gelten für das Argument verbindlich. Wir suchen weiter nach Begriffen, die wir anwenden können. Das nächste, was wir anwenden können, ist die Lambda-Bindung an den Lambda-Term ((.)).

Ich verstehe es nicht. Im ersten Abschnitt heißt es hat kein Argument zu gelten, das kann ich wahrscheinlich verstehen, aber dann im nächsten Abschnitt denke ich, die z kann an ((.)) gebunden werden, weil, wie Sie sehen können, .(.), der Körper von eindeutig hat ein z Argument, das gebunden werden kann. Aber das Buch ignoriert nur den Kopf und direkt n an ((.)) gebunden. Ich meine . hat kein n Argument, warum wird es gebunden werden?

Kann mir jemand das erklären?

Answer 1

normale Reihenfolge Auswertung verwenden, können Sie die Antwort in zwei Beta-Reduktionen

// beta reduction 1 
λz.(λm.λn.m)(z)((λp.p)z) →β (λn.m) [m := z] 
λz.(λm.λn.z)(z)((λp.p)z) 

// beta reduction 2 
λz.(λn.z)((λp.p)z)  →β z  [n := ((λp.p)z)] 
λz.(λn.z)((λp.p)z) 

// result 
λz.z 

Die zweite Reduktion heikel erscheinen mag, weil n-((λp.p)z) gebunden ist, sondern der Ausdruck ist nur z, so n sind weggeworfen.

---

applicative um die Auswertung mit, dauert es einen zusätzlichen Schritt

// beta reduction 1 
λz.(λm.λn.m)(z)((λp.p)z) →β p  [p := z] 
λz.(λm.λn.m)(z)((λp.z)z) 

// beta reduction 2 
λz.(λm.λn.m)(z)(z)  →β (λn.m) [m := z] 
λz.(λm.λn.z)(z)(z) 

// beta reduction 3 
λz.(λn.z)(z)    →β z  [n := z] 
λz.(λn.z)(z) 

// result 
λz.z 

---

In diesem Szenario ob wir normale Ordnung Auswertung oder applicative um die Auswertung zu verwenden, das Ergebnis ist das gleiche. Unterschiedliche Evaluierungsstrategien bewerten manchmal unterschiedliche Ergebnisse.

Ein wichtiger Hinweis, die oben genannten Reduzierungsschritte werden nicht ausgeführt bisλz angewendet wird (je nach Implementierung). In dem von Ihnen bereitgestellten Beispielcode wird λz nie angewendet, daher vereinfacht sich in diesem Fall der Begriff λz nur für die Übung.

Alles, was wir getan haben, ist Lambda Äquivalenz (unter zwei verschiedenen Auswertungsstrategien)

λz.(λm.λn.m)(z)((λp.p)z) <=> λz.z 

Answer 2

Lambda-Notation ist ein bisschen seltsam zu analysieren. IMO Haskell Syntax ist klarer:

\z -> (\m -> \n -> m) z ((\p -> p) z) 

oder, noch deutlicher

\z -> (
     (
      (\m -> (\n -> m)) 
      z 
     ) 
     ((\p -> p) z) 
    ) 

Der erste Reduktionsschritt ist

\z -> (
     (
      (\n -> z) 
     ) 
     ((\p -> p) z) 
    ) 

oder

\z -> (
     (\n -> z) 
     ((\p -> p) z) 
    ) 

dann können Sie in der Tat binden ((\p -> p) z) - nicht zu z sondern zu n! (Das ist eigentlich gar nicht, obwohl verwendet.)

\z -> (
     (z) 
    ) 

oder einfach \z -> z. Also, wir immer noch haben, dass z Lambda, die wie das Buch sagte, irredicible ist. Wir haben einfach nichts anderes!

---

... Ich bin mir nicht sicher, ob das tatsächlich deine Frage war. Wenn es eher war: Warum müssen wir nicht zuerst sehen, wenn wir ((\p -> p) z) reduzieren können, dann ist die Antwort, ich denke, Lambda-Kalkül als solche definiert dies überhaupt nicht (es definiert nur, welche Transformation Sie kann gelten, nicht in welcher Reihenfolge du sollte es tun. ^{Eigentlich bin ich mir nicht sicher, korrigieren Sie mich, wenn ich falsch liege}). In einer strengen Sprache wie Scheme würden Sie zuerst ((\p -> p) z) reduzieren; Haskell würde das nicht tun, da es keine Notwendigkeit gibt. In jedem Fall spielt es keine Rolle, denn das Ergebnis wird sowieso verworfen.

(\z -> (\n -> z) ((\p -> p) z)) 
≡ (\z -> (\n -> z) z) 
≡ (\z -> (\n -> z) foo) 
≡ (\z -> z) 

Answer 3

Der Schlüssel ist, dass n nie in der Abstraktion verwendet wird. n ist immer noch an ((λp.p)z) gebunden, aber es wird sofort verworfen.

λz.(λm.λn.m)(z)((λp.p)z) = λz.(λn.z)((λp.p)z) Replacing m with z 
         = λz.z    Replacing n with ((λp.p)z)