如何对嵌套Lambda抽象执行Beta归约？Haskell示例解析

背景示例 #

Will Kurt的Haskell相关书籍中，先给出了一个变量覆盖的let表达式示例：

overwrite x = let x = 2
              in
              let x = 3
              in
              let x = 4
              in
              x

对应的纯Lambda抽象版本为（不建议实操）：

(\x -> (\x -> (\x -> x) 4) 3) 2

通过GHCi执行会得到结果4，但手动归约时容易因混淆变量作用域出错，以下是正确的分步Beta归约过程。

核心规则：作用域优先 #

Beta归约的关键是变量的作用域绑定：每个\x -> ...中的x仅在其右侧的表达式内有效，内层Lambda绑定的x会覆盖外层同名变量，二者是不同的绑定，名字相同只是巧合。

分步归约过程 #

• 第一步：归约最外层Lambda
  初始表达式：

  (\x -> (\x -> (\x -> x) 4) 3) 2
  

  最外层(\x -> 内层表达式) 2中的x被内层Lambda完全覆盖，因此2没有可替换的目标变量，归约后得到：

  (\x -> (\x -> x) 4) 3
  

• 第二步：归约第二层Lambda
  当前表达式(\x -> 内层表达式) 3中的x同样被最内层Lambda绑定的x覆盖，3也无对应的替换位置，归约后得到：

  (\x -> x) 4
  

• 第三步：归约恒等函数
  (\x -> x)是恒等函数，输入值会被直接返回，因此归约后得到最终结果：

  4
  

错误归约的问题分析 #

错误步骤尝试将最外层的2替换最内层的x：

(\x -> (\x -> (\x -> x) 4) 3) 2 => (\x -> (\x -> 2) 4) 3)

这个错误的根源是混淆了不同作用域的同名变量：最内层的x是由(\x -> x)绑定的局部变量，和最外层Lambda的x属于完全独立的作用域，因此不能被外层的2替换。

内容的提问来源于stack exchange，提问作者ezyman