lambda-calculus - 函数的 Lambda 演算约简

Question

我对 lambda 演算非常陌生，在阅读教程时遇到了这个问题。这是我的方程式。

Y = ƛf.( ƛx.f(xx)) ( ƛx.f(xx))

现在如果我们应用另一个术语，比如说 F (YF)，那么我们如何才能减少它。如果我根据 beta 减少是正确的，我们可以将(ƛx.f(xx))中 的所有f替换为(ƛx. f(xx))，这是正确的，如果是，我们该怎么做。

谢谢

Answer 1

还原步骤：

Y = ƛf.( ƛx.f(xx)) ( ƛx.f(xx)) = ƛf.( f ( ƛx.f(xx) ƛx.f(xx) ) ) 
  = ƛf.( f ( f (ƛx.f(xx) ƛx.f(xx)))) 
  = ƛf.( f ( f ( f (ƛx.f(xx) ƛx.f(xx)))) 
  = ƛf.( f ( f ( f ( f (ƛx.f(xx) ƛx.f(xx))))) = ...

所以这个 Lambda 项进入了一个无限循环......

解释：
让我们看看( ƛx.f(xx) ƛx.f(xx) )我们ƛx.f(xx)用f'
它替换的术语(f' f')=> 激活术语f'本身。
这样看可能更容易：
( ƛy.f(yy) ƛx.f(xx) )现在当您激活ƛy.f(yy)并提供输入（用 替换y）ƛx.f(xx)时，结果是：f(ƛx.f(xx) ƛx.f(xx))反过来，它可以一次又一次地遍历相同的过程，而 lambda 表达式只会消耗。 ..

备注：
写错了：
Y = ƛf.( ƛx.f(xx)) ( ƛx.f(xx)) 它实际上应该是： 和Y = ƛf.(ƛx.f(xx) ƛx.f(xx))
的区别在于后者是一个激活- 像这样激活它是没有意义的，因为我们需要一个（输入）来激活它。最后：意思：ƛx.f(xx)(ƛx.f(xx))ƛx.f(xx)(ƛx.f(xx))x


Y = ƛf.( ƛx.f(xx)) ( ƛx.f(xx)) = ƛf.( f ( ƛx.f(xx) ƛx.f(xx) ) )

YF = ( ƛx.F(xx)) ( ƛx.F(xx)) = F(ƛx.F(xx)) ( ƛx.F(xx)) = F(YF)