函数的 Lambda 演算约简

Question

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

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

现在如果我们应用另一个术语，比如说 F (YF)，那么我们如何减少它。如果我根据 beta 减少是正确的，我们可以替换 中的所有 f >(ƛx.f(xx)) by (ƛ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) )这个术语，我们用f'替换ƛx.f(xx)
这意味着(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)