haskell - Lambda Calculus 变量变化及应用题

Question

我正在学习 Haskell，我正在学习什么是抽象、替换(beta 等价)、应用程序、自由和绑定(bind)变量(alpha 等价)，但我对解决这些练习有一些疑问，我不知道我的解决方案是否正确。
进行以下替换

1. (λ x → y x x) [x:= f z] 
Sol. (\x -> y x x) =>α (\w -> y w w) =>α (\w -> x w w) =>β (\w -> f z w w)

2. ((λ x → y x x) x) [y:= x]
Sol. ((\x -> y x x)x) =>α (\w -> y w w)[y:= x] = (\w -> x w w)     

3. ((λ x → y x) (λ y → y x) y) [x:= f y]
Sol. aproximation, i don't know how to do it:  ((\x -> y x)(\y -> y x) y) =>β 
(\x -> y x)y x)[x:= f y] =>β  y x [x:= f y] = y f y

4. ((λ x → λ y → y x x) y) [y:= f z]
Sol aproximation, ((\x -> (\y -> (y x x))) y) =>β ((\y -> (y x x)) y) =>α ((\y -> (y x x)) f z)

我的另一个疑问是我是否可以在 this website 上运行这些表达式。 ?它是一个 Lambda 微积分计算器，但我不知道如何运行这些测试。

Answer 1

1. (λ x → y x x) [x:= f z]
Sol. (\x -> y x x) =>α (\w -> y w w) =>α (\w -> x w w) =>β (\w -> f z w w)

不，您不能重命名 y ，在 (λ x → y x x) 中是免费的.只有绑定(bind)变量可以(一致地)α重命名。但是只能替换自由变量，没有自由的 x在那个 lambda 项中。

2. ((λ x → y x x) x) [y:= x]
Sol. ((\x -> y x x)x) =>α (\w -> y w w)[y:= x] = (\w -> x w w)

是的，替换 x对于 y将允许它被 λ x 捕获，所以你确实必须α重命名 x在 (λ x → y x x)首先像您一样使用一些新的唯一名称，但您已将应用程序放到免费的 x由于某些原因。您不能只省略部分术语，所以它是 ((\w -> y w w) x)[y:= x] .现在执行替换。请注意，您不需要执行结果项的 β 减少，只是替换。
剩下的两个我就不说了。只要仔细遵守规则。如果您首先将所有绑定(bind)名称重命名为唯一名称，则很容易，即使重命名不是严格要求，例如

((λ x → y x) (λ y → y x) y) [x:= f y]   -->
((λ w → y w) (λ z → z x) y) [x:= f y]

“唯一”部分还包括替换术语中使用的自由变量，这些自由变量可能会在被替换后被捕获(即没有首先执行重命名，在它们被替换的术语中)。这就是为什么我们不得不重命名绑定(bind) y在上述术语中， -- 因为 y在替代项中出现自由。我们不必重命名绑定(bind) x但这样就更容易了。