Vereinfachung der Lambda-Rechnung

Unten ist der Lambda-Ausdruck, den ich nur schwer reduzieren kann, dh ich kann nicht verstehen, wie ich dieses Problem lösen soll.

$$(\lambda mn.(\lambda sz.ms(nsz)))(\lambda sz.sz)(\lambda sz.sz)$$

Ich bin damit verloren.

Wenn mich jemand in die richtige Richtung führen könnte, wäre das sehr dankbar

Lambda-Terme werden durch die β-Reduktionsregel vereinfacht :

$$(\lambda x.M)N\,\rightarrow_\beta\,M[x:=N]$$

Es bedeutet, wenn Sie ein Subterm haben, das aussieht $(\lambda x.M)N$( Redex genannt ) Sie können es durch ersetzen$M[x:=N]$, welches ist $M$ mit $N$ Ersetzt durch $x$. Der Ersatz$M[x:=N]$wird oft Contractum genannt . (Großbuchstaben mögen$M$ und $N$ werden verwendet, um Begriffe zu bezeichnen.)

In Ihrem Fall wäre die erste Ermäßigung:

$$(\underbrace{(\lambda mn.(\lambda sz.ms(nsz)))(\lambda sz.sz)}_{\mbox{redex}})(\lambda sz.sz) \rightarrow_\beta \underbrace{(\lambda n.(\lambda sz.(\lambda sz.sz)s(nsz)))}_{\mbox{contractum}}(\lambda sz.sz)$$ wo wir ersetzt haben $m$ mit $\lambda sz.sz$. Beachten Sie, dass wir jetzt haben$\lambda sz$ Innerhalb $\lambda sz$was nicht sehr praktisch ist (noch erlaubt). Es ist besser, gebundene Variablen umzubenennen ($\alpha$-Umwandlung) zu unterscheiden, zum Beispiel zu:

$$(\lambda n.(\lambda uv.(\lambda sz.sz)u(nuv)))(\lambda sz.sz)$$

Einige Notizen:

• Die Substitution gilt nur für freie Variablen. Gebundene Variablen bleiben immer intakt.
• Manchmal ist eine Substitution nicht direkt möglich. Zum Beispiel können Sie nicht ersetzen$x:=y$ in $\lambda y.xy$ da $y$ ist gebunden unter $\lambda$. Du würdest bekommen$\lambda y.yy$was die Bedeutung des Begriffs ändern würde. Sie müssen also zuerst die gebundene Variable umbenennen, zum Beispiel in$\lambda z.xz$ und dann können Sie sicher ersetzen $x:=y$ bekommen $\lambda z.yz$. Der Wikipedia-Artikel enthält eine formale Definition der Substitution und zeigt, wann gebundene Variablen umbenannt werden müssen.
• Lambda assoziiert also rechts $\lambda sz.sz$ ist $\lambda s.(\lambda z.sz)$.
• Anwendungsassoziierte auf der linken Seite, also $xyz$ ist $(xy)z$.

Eine alternative Art, eine Lambda-Abstraktion und -Reduktion auszudrücken. Indizes werden anstelle von mit Buchstaben versehenen Begriffen verwendet, die auf der Reihenfolge der Eingabe basieren. Abstraktionen sind von [] umgeben

(λmn.(λsz.ms(nsz)))(λsz.sz)(λsz.sz)
m -> 1, n -> 2, s -> 3, z -> 4
(λmn.(λsz.ms(nsz))) = [1 3 (2 3 4)]
(λsz.sz) = [1 2]
[1 3 (2 3 4)][1 2][1 2]  
[[1 2] 2 (1 2 3)][1 2]   ;1 was replaced with [1 2], remaining terms decremented
[[1 2] 1 ([1 2] 1 2)]    ;1 was replaced with [1 2], remaining terms decremented
[1 ([1 2] 1 2)]          ;1 2 was replaced by 1 ([1 2] 1 2)]
[1 (1 2)]                ;1 2 was replaced by 1 2
(λmn.m(mn))

Die obige Notation ist nur eine kompaktere und eindeutigere Art, Lambda-Abstraktionen auszudrücken. Zusammengesetzte Abstraktionen werden automatisch auf eine einzige Normalform reduziert, eine Alpha-Reduktion ist nicht erforderlich.

Einzelne positive Indizes werden für gebundene Begriffe verwendet. Negative Indizes werden für Kill-Begriffe verwendet. Negative Indizes werden zuletzt in abnehmender Reihenfolge platziert.

I = λx.x = [1]
K = λxy.x = [1 -2]
KI = λyx.x = [2 -1]
S = λxyz.xz(yz) = [1 3 (2 3)]

Anwenden von S auf K:

[1 3 (2 3)][1 -2]
[[1 -2] 2 (1 2)]  ;1 was replaced with [1 -2], remaining terms decremented
[[.2 -1] (1 2)]   ;reducing: 1 replaced by .2*, -2 decremented (in magnitude) 
[2 -2 -1]         ;(1 2) bound terms become kill terms due to -1.
[2 -1] = KI       ;-2 kill term is void due to surviving 2 term

* the . notation signifies the bound term is from the outer abstraction 
  and must be used to prevent decrementing and double replacement of the
  term until the substitution of all terms in the abstraction is complete.

[2 -1][anything] ;applying KI to anything
[1] = I          ;yeilds I, therefor SK[anything] = [1] = I

Anwenden von K auf K:

[1 -2][1 -2]
[[1 -2] -1]  ;kill terms are absorbed and also increase the magnitude of bound terms
[2 -3 -1]    ;applying this result to anything yields K.
[2 -3 -1][anything]
[2 -1]