Lambda微积分变量的变化和应用问题

问题描述

我正在研究Haskell，并且正在学习什么是抽象，替代（β等价），应用程序，自由变量和绑定变量（α等价），但是我对解决这些练习有一些疑问，我不知道我的解决方案是否可行是正确的。

进行以下替换

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微积分计算器，但我不知道如何运行这些测试。

解决方法

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

否，您无法重命名y，它在(λ x → y x x)中是免费的。只有 bound 变量可以（一致地）重命名。但是只能替换 free 变量，并且在该lambda术语中没有免费的x。

2. ((λ x → y x x) x) [y:= x]
索尔((\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]。现在执行替换。请注意，系统不会要求您对结果项进行β归约，而只是要求进行取代。

我将其他两个排除在外。只需仔细遵守规则即可。例如，即使不严格要求重命名，也可以先将所有绑定名称重命名为唯一名称，这很容易

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

“唯一”部分还包括在替换项中使用的自由变量，这些自由变量可能在被替换后被捕获（即，在被替换的术语中，没有先执行重命名）。这就是为什么我们在上一条款中不得不重命名绑定的y的原因，因为y在替代条款中似乎是自由的。我们不必重命名绑定的x，但是这样更容易。