返回介绍

6.2 实现 lambda 演算

发布于 2023-05-18 19:12:04 字数 9455 浏览 0 评论 0 收藏 0

FizzBuzz 实现已经让我们对用无类型的lambda 演算写程序有了一些感觉。这些限制迫使我们从零开始实现大量的基本功能而不是依赖语言的特性,但我们确实成功构建了解决这个问题所需要的数据结构和算法。

因为还没有lambda演算的解释器,所以还没有真正写演算的程序呢。我们只是在用lambda 演算的形式写Ruby 程序,以此获得这样一个小语言能工作的感觉。但我们已经有了构建lambda 演算解释器并用其对实际的lambda 演算表达式求值的所有知识,那来尝试一下吧。

6.2.1 语法

无类型的lambda 表达式是一种编程语言,它只有三种表达式:变量、函数定义以及调用。我们不再引入一种新的lambda 表达式语法,而是还遵守Ruby 的习惯(变量看起来像x,函数看起来像->x{x},而调用看起来像是x[y]),并尽量不让两种语言混淆。

为什么是“lambda 演算”?

在这个上下文中,单词演算(calculus)的意思是一个操纵符号字符串的规则系统。7 lambda 演算的原始语法用的是希腊字母lambda(λ)代替Ruby 中的-> 符号。例如,ONE会写成λp.λx.p x。

7大多数人把它与微积分学联系起来,这是一个数学函数中关于改变率和数量累加率的系统。

我们可以用常见的方式实现LCVariable、LCFunction和LCCall类:

class LCVariable < Struct.new(:name)
  def to_s
    name.to_s
  end

  def inspect
    to_s
  end
end

class LCFunction < Struct.new(:parameter, :body)
  def to_s
    "-> #{parameter} { #{body} }"
  end

  def inspect
    to_s
  end
end

class LCCall < Struct.new(:left, :right)
  def to_s
    "#{left}[#{right}]"
  end

  def inspect
    to_s
  end
end

这些类可以让我们构建lambda演算表达式的抽象语法树,就像第2章的Simple和第3章的正则表达式那样:

>> one =
    LCFunction.new(:p,
      LCFunction.new(:x,
        LCCall.new(LCVariable.new(:p), LCVariable.new(:x))
      )
    )
=> -> p { -> x { p[x] } }
>> increment =
    LCFunction.new(:n,
      LCFunction.new(:p,
        LCFunction.new(:x,
          LCCall.new(
            LCVariable.new(:p),
            LCCall.new(
              LCCall.new(LCVariable.new(:n), LCVariable.new(:p)),
              LCVariable.new(:x)
            )
          )
        )
      )
    )
=> -> n { -> p { -> x { p[n[p][x]] } } }
>> add =
    LCFunction.new(:m,
      LCFunction.new(:n,
        LCCall.new(LCCall.new(LCVariable.new(:n), increment), LCVariable.new(:m))
      )
    )
=> -> m { -> n { n[-> n { -> p { -> x { p[n[p][x]] } } }][m] } }

因为这种语言有这样小的语法,所以那三个类足以表示任意的lambda 演算的程序了。

6.2.2 语义

现在通过为每个语法类实现一个#reduce方法来为lambda演算赋予一个小步操作语义。小步操作语义是一个很有吸引力的选择,因为它能让我们看到求值的每一步,这在Ruby表达式中是没法轻易做到的。

1. 替换变量

在实现#reduce之前,我们需要另一个叫作#replace的操作,它能找到一个表达式里的一个特定变量并用另一个表达式替换它:

class LCVariable
  def replace(name, replacement)
    if self.name == name
      replacement
    else
      self
    end
  end
end

class LCFunction
  def replace(name, replacement)
    if parameter == name
      self
    else
      LCFunction.new(parameter, body.replace(name, replacement))
    end
  end
end

class LCCall
  def replace(name, replacement)
    LCCall.new(left.replace(name, replacement), right.replace(name, replacement))
  end
end

对于变量和调用,它的工作方式很明显:

>> expression = LCVariable.new(:x)
=> x
>> expression.replace(:x, LCFunction.new(:y, LCVariable.new(:y)))
=> -> y { y }
>> expression.replace(:z, LCFunction.new(:y, LCVariable.new(:y)))
=> x
>> expression =
  LCCall.new(
    LCCall.new(
      LCCall.new(
        LCVariable.new(:a),
        LCVariable.new(:b)
      ),
      LCVariable.new(:c)
    ),
    LCVariable.new(:b)
  )
=> a[b][c][b]
>> expression.replace(:a, LCVariable.new(:x))
=> x[b][c][b]
>> expression.replace(:b, LCFunction.new(:x, LCVariable.new(:x)))
=> a[-> x { x }][c][-> x { x }]

对于函数,情况会更复杂。#replace只能对一个函数的函数体起作用,而且它只能替换自由变量——自由变量就是在函数范围内但是没有被声明为函数参数的变量:

>> expression =
  LCFunction.new(:y,
    LCCall.new(LCVariable.new(:x), LCVariable.new(:y))
  )
=> -> y { x[y] }
>> expression.replace(:x, LCVariable.new(:z))
=> -> y { z[y] }
>> expression.replace(:y, LCVariable.new(:z))
=> -> y { x[y] }

这让我们可以替换掉整个表达式中的同一个变量,而不会不小心改变正好有相同名字的无关变量:

>> expression =
  LCCall.new(
    LCCall.new(LCVariable.new(:x), LCVariable.new(:y)),
      LCFunction.new(:y, LCCall.new(LCVariable.new(:y), LCVariable.new(:x)))
  )
=> x[y][-> y { y[x] }]
>> expression.replace(:x, LCVariable.new(:z))
=> z[y][-> y { y[z] }] ➊
>> expression.replace(:y, LCVariable.new(:z))
=> x[z][-> y { y[x] }] ➋

➊ 在原始表达式中x都是自由的,所以它们都被替换掉了。 ➋ 只有第一次出现的y才是自由变量,因此只有它被替换掉了。第二个y 是个函数参数,不是变量,而第三个y是一个属于那个函数的变量,所以不应该碰它。

简单的#replace实现在某些输入下不能工作。它无法正确地处理含有自由变量的替换:

> expression =
  LCFunction.new(:x,
    LCCall.new(LCVariable.new(:x), LCVariable.new(:y))
)
=> -> x { x[y] }
> replacement = LCCall.new(LCVariable.new(:z), LCVariable.new(:x))
=> z[x]
> expression.replace(:y, replacement)
=> -> x{ x[z[x]] }

像那样只是把z[x]粘贴进-> x { ... }的函数体内是不行的,因为z[x]中的x 是一个自由变量,在处理完之后应该保持不变,但在这里,它恰好被同名的函数参数捕获了。8

我们可以忽略这个缺陷,因为我们将只对不含任何自由变量的表达式求值,因此实际上它不会产生任何问题,但是要注意,一般情况下,需要一种更为复杂的实现。

8正确的行为是自动改掉函数参数的名字,这样就避免与任何自由变量冲突了:->x{ x[y] }改写为等价的表达式->w { w[y] },然后再安全地执行替换,得到->w { w[z[x]] },而x 仍然是自由变量。

2. 调用函数

方法#replace的作用就是给我们一种实现函数调用语义的方式。在Ruby 中,在用一个或者多个参数调用proc 的时候,proc 的主体会得到求值,在这个环境下每个参数都被赋值给了一个本地变量,因此每次使用变量时都像用参数本身一样。这暗示着,用参数1和2调用proc->x, y {x + y}会产生中间表达式1+2,它是为了产生最终结果所要求值的表达式。

在lambda 演算中我们可以应用同样的思想,在对一个调用求值的时候替换一个函数体内的变量。为此,我们可以定义一个LCFunction#call方法,这个方法进行替换并返回结果:

class LCFunction
  def call(argument)
    body.replace(parameter, argument)
  end
end

这让我们可以模拟一个函数被调用的时刻:

>> function =
  LCFunction.new(:x,
    LCFunction.new(:y,
      LCCall.new(LCVariable.new(:x), LCVariable.new(:y))
    )
  )
=> -> x { -> y { x[y] } }
>> argument = LCFunction.new(:z, LCVariable.new(:z))
=> -> z { z }
>> function.call(argument)
=> -> y { -> z { z }[y] }

3. 规约表达式

在对一个lambda 演算程序求值的时候,函数调用是唯一实际发生的事情,因此现在我们准备实现#replace。它会找到表达式中函数调用能发生的地方,然后使用#call 方法使函数调用发生。我们只需要能识别哪些表达式是实际能调用的……

class LCVariable
  def callable?
    false
  end
end

class LCFunction
  def callable?
    true
  end
end

class LCCall
  def callable?
    false
  end
end

……然后就可以写#reduce了:

class LCVariable
  def reducible?
    false
  end
end

class LCFunction
  def reducible?
    false
  end
end

class LCCall
  def reducible?
    left.reducible? || right.reducible? || left.callable?
  end

  def reduce
    if left.reducible?
      LCCall.new(left.reduce, right)
    elsif right.reducible?
      LCCall.new(left, right.reduce)
    else
      left.call(right)
    end
  end
end

在这个实现中,函数调用是唯一一种能被规约的语法。规约LCCall有点像规约SIMPLE 里的Add或Multiply:如果其中有一个子表达式可以规约,我们就对其规约;如果都不能规约,我们就通过以右边的子表达式作为左边子表达式(应该是一个LCFunction)的参数调用左边的子表达式来实际执行调用。这个策略称为值调用求值——首先我们把参数规约成一个不可规约的值,然后再执行调用。

使用lambda 演算来计算一下“一加一”,以此来测试我们的实现:

>> expression = LCCall.new(LCCall.new(add, one), one)
=> -> m { -> n { n[-> n { -> p { -> x { p[n[p][x]] } } }][m] } }[-> p { -> x { p[x] }
}][-> p { -> x { p[x] } }]
>> while expression.reducible?
    puts expression
    expression = expression.reduce
  end; puts expression
-> m { -> n { n[-> n { -> p { -> x { p[n[p][x]] } } }][m] } }[-> p { -> x { p[x] } }]
[-> p { -> x { p[x] } }]
-> n { n[-> n { -> p { -> x { p[n[p][x]] } } }][-> p { -> x { p[x] } }] }[-> p { -> x
{ p[x] } }]
-> p { -> x { p[x] } }[-> n { -> p { -> x { p[n[p][x]] } } }][-> p { -> x { p[x] } }]
-> x { -> n { -> p { -> x { p[n[p][x]] } } }[x] }[-> p { -> x { p[x] } }]
-> n { -> p { -> x { p[n[p][x]] } } }[-> p { -> x { p[x] } }]
-> p { -> x { p[-> p { -> x { p[x] } }[p][x]] } }
=> nil

好吧,有些事情确实发生了,不过我们没得到想要的结果:最终的表达式是-> p { -> x{ p[-> p { -> x { p[x] } }[p][x]] } },但数字“二”的lambda 演算表示应该是-> p{ -> x{ p[p[x]] } })]。哪里错了呢?

错误是由我们使用的求值策略引起的。结果里还有可规约的函数调用——例如调用-> p{ -> x { p[x] } }[p]可以被规约成-> x { p[x] }——但#reduce没有接触到它们,因为它们是在一个函数体内出现的,而我们的语义不会把函数处理成可规约的。9

9为了修正这个问题,我们可以重新实现#reduce方法,使用更激进的求值策略(如应用序求值或者正则序求值)对函数体执行规约,但处理单一函数体时通常都包含自由变量,所以需要一个#replace的更健壮的实现。

但是,就像前面6.1.1 节中“相等”部分讨论的一样,两个具有不同语法的表达式如果有同样的行为仍然被认为是相等的。我们知道数字“二”的lambda 演算表达式应该是:如果我们给它两个参数,它会对第二个参数调用第一个参数两次。让我们试着用两个改造过的变量inc和zero10 调用表达式,然后看一下它实际在做什么:

10我们对含有自由变量inc和zero的表达式求值是在冒险,但幸运的是,表达式中没有一个函数含有这些名字的参数,因此在这个特例中,不管哪个变量被意外捕获都不会有危险。

>> inc, zero = LCVariable.new(:inc), LCVariable.new(:zero)
=> [inc, zero]
>> expression = LCCall.new(LCCall.new(expression, inc), zero)
=> -> p { -> x { p[-> p { -> x { p[x] } }[p][x]] } }[inc][zero]
>> while expression.reducible?
    puts expression
    expression = expression.reduce
  end; puts expression
-> p { -> x { p[-> p { -> x { p[x] } }[p][x]] } }[inc][zero]
-> x { inc[-> p { -> x { p[x] } }[inc][x]] }[zero]
inc[-> p { -> x { p[x] } }[inc][zero]]
inc[-> x { inc[x] }[zero]]
inc[inc[zero]]
=> nil

这恰好是我们希望数字“二”所要表现的行为,因此尽管-> p { -> x { p[-> p { -> x{ p[x] } }[p][x]] } }看起来与期望的不同,但毕竟是正确的结果。

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。
列表为空,暂无数据
    我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
    原文