Ableitungen (Ansatz)

Absicht: Relation $\to$ auf $\Lambda$ (Ein-Schritt-Ersetzung):

• ($\lambda$x.B)A$\to$B[x : = A] (Vorsicht)
• F$\to$F' $\Rightarrow$ (FA)$\to$(F'A)
• A$\to$A' $\Rightarrow$ (FA)$\to$(FA')
• B$\to$B' $\Rightarrow$ $\lambda$x.B$\to$$\lambda$x.B'

was soll ($\lambda$x.B)[x : = 3 + 4] bedeuten?

ist das sinnvoll: ($\lambda$x.($\lambda$y.xyx))(yy)$\to$($\lambda$y.yx)[x : = (yy)] = $\lambda$y.y(yy)

das freie y wird fälschlich gebunden