返回介绍

9.1 抽象解释

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

抽象解释给了我们一种着手处理难处理问题的方法,这些难处理的问题或许过于庞大,过于复杂,或者有太多的未知东西难以直接处理。抽象解释的主要思想就是使用抽象,或者通过让它更小,更简单,或者通过去掉未知的东西,但这样做还能保留足够的细节,以便让它的解决方案与原始问题相关。

为了让这个模糊的想法更具体,让我们看一个抽象解释的简单应用。

9.1.1 路线规划

假设你是一个身处陌生国家的旅行者,想要做到另一个镇的公路旅行计划。你怎么决定要走哪条路线呢?一个直接的解决方案就是跳上你租来的汽车,然后朝看起来最有希望到达目的地的方向行驶。取决于你的幸运程度和外国路标对你的帮助程度,这种对未知道路的暴力探索可能最终让你到达目的地。但这是一个昂贵的策略,而且很可能在完全放弃之前,你会越来越迷路。

使用地图来规划你的旅行是极理性的想法。印在纸上的公路地图是牺牲现实公路网络大量细节之后的一个抽象。它不会告诉你交通是什么样,哪条公路当前关闭了,某个建筑物在哪儿,或者关于第三维的任何东西。至关重要的是,它比真实的东西更小更平。但一张地图确实保留了旅行规划所需要的最重要的信息:所有镇的相对位置,哪条路通向哪个镇,以及哪些路彼此之间如何连接。

尽管丢掉了一些细节,但一个准确的地图仍然是有用的,因为它指定的路线很可能在现实中是有效的。地图制作人员已经完成了创建现实模型的昂贵工作,这让你能只查看简化的公路网络并规划路线。然后当你驾车驶向目的地时,你可以把计算的结果转换回现实世界中。按照地图这个抽象世界指定的路线,可以避免试错的昂贵代价。

近似的地图让行驶计算更容易,又不会损失结果的准确性。在很多情况下,用地图做决策可能会是错的——无法保证地图告诉你旅行需要的所有信息——但预先规划路线可以让你排除一些错误,让从一个地方到另一个地方容易控制得多。

9.1.2 抽象:乘法的符号

用印刷地图规划路线是抽象解释的现实应用,也非常随意。如果要举一个更正式的例子,我们可以看一下数字的乘法。尽管这仍然是个小例子,但乘法让我们有机会开始写代码研究这些思想。

假设两个数相乘是一个困难或者昂贵的运算,而我们对不实际执行乘法就查明它结果的某些信息很感兴趣。特别地:结果的符号是什么?它是一个负数、零,还是一个整数呢?

理论上的难点是在具体的世界中进行计算,使用乘法的标准解释:真的把数字乘起来,看结果的数,然后决定结果是否为负的,零,或者是正的。例如,在 Ruby 中:

>> 6 * -9
=> -54

-54 是负数,所以我们知道了 6 和 -9 的乘积是一个负数。任务完成了。 尽管如此,通过在抽象世界中进行计算,使用乘法的抽象解释,也可能发现同样的信息。就像一个地图使用平面纸上的线来表示现实世界中的道路一样,我们使用抽象的值来表示数字;我们可以在地图上设计一条路线,而不必在真实道路上通过试错来找到路。可以在抽象值上定义一个抽象的乘法运算,而不必使用具体数之上的具体乘法。

为此,我们需要设计抽象的值让计算在结果仍为有用答案的同时,变得更简单。可以利用两个乘数的绝对值 2 不影响结果符号的事实:

2一个数的绝对值是把符号去掉时候的值。例如,-10 的绝对值是 10。

>> (6 * -9) < 0
=> true
>> (1000 * -5) < 0
=> true
>> (1 * -1) < 0
=> true

小时候,我们就知道关键要看乘数的符号:两个正数的乘积,或者两个负数的乘积,总是一个正数;一个正数和一个负数的乘积总是负数;而零与任何数的乘积都是零。

因此使用“负数”、“零”和“正数”作为抽象值,可以用 Ruby 定义一个 Sign 类然后创建它的三个实例:

class Sign < Struct.new(:name)
  NEGATIVE, ZERO, POSITIVE = [:negative, :zero, :positive].map { |name| new(name) }

  def inspect
    "#<Sign #{name}>"
  end
end

这给了我们可以用作抽象值的 Ruby 对象:Sign::NEGATIVE 代表“任何负数”,Sign::ZERO代表“数字零”,而 Sign::POSITIVE 代表“任意正数”。这三个 Sign 对象组成了这个小的抽象世界,在这个世界里,我们将执行抽象运算。而与此同时,具体的世界里包含着事实上无限个 Ruby 的正数。3我们可以通过实现符号相关的乘法来定义 Sign 值的抽象乘法:

3Ruby 的 Bignum 对象可以表示任意大小的正数,它只受可用内存的限制。

class Sign
  def *(other_sign)
    if [self, other_sign].include?(ZERO)
      ZERO
    elsif self == other_sign
      POSITIVE
    else
      NEGATIVE
    end
  end
end

Sign 的实例现在可以像数字那样“乘”到一起了,并且 Sign#* 的实现产生的答案与实际数字乘法的一致:

>> Sign::POSITIVE * Sign::POSITIVE
=> #<Sign positive>
>> Sign::NEGATIVE * Sign::ZERO
=> #<Sign zero>
>> Sign::POSITIVE * Sign::NEGATIVE
=> #<Sign negative>

例如,上面的最后一行问的问题是:我们把任意的正数乘以任意的负数得到的结果是什么?答案是:一个负数。这仍然是一种乘法,但比我们习惯的那种要简单,它只对几乎已经去掉所有识别信息的“数字”起作用。如果把真实的乘法想象成是昂贵的,那这个缩减的乘法版本就是廉价的。

有了数字的抽象世界和对这些数字乘法的抽象解释之后,我们可以用不同的方式处理最初的问题了。我们不是把两个数字直接相乘来找到它们结果的符号,而是把数字转换成它们的抽象表示再把它们相乘。首先,需要一种把具体数转换成抽象数的方法:

class Numeric
  def sign
    if self < 0
      Sign::NEGATIVE
    elsif zero?
      Sign::ZERO
    else
      Sign::POSITIVE
    end
  end
end

现在,可以转换两个数然后在抽象世界中做乘法了:

>> 6.sign
=> #<Sign positive>
>> -9.sign
=> #<Sign negative>
>> 6.sign * -9.sign
=> #<Sign negative>

我们又计算出了 6 * -9会得到一个负数,但这次没进行任何实际数字的乘法。步入抽象世界让我们有了执行计算的另一种方式,更重要的是,这个抽象结果能转换回具体的世界,这样就能搞清它的意思,尽管抽象时牺牲细节只得到了一个近似的答案。在这个场景下,抽象结果Sign::NEGATIVE 表明任何具体的数-1、-2、-3 等都可能是6 * -9 的答案,但答案肯定不是 0 或者任何像 1 或 500 这样的正数。

注意,因为 Ruby 的值都是对象(带有操作的数据结构),所以可以根据提供的是具体的(Fixnum)还是抽象的(Sign)对象,我们可以使用同样的 Ruby 表达式为参数执行具体或抽象的计算。用 #calculate 方法把三个数用特别的方式乘起来:

def calculate(x, y, z)
  (x * y) * (x * z)
end

如果使用 Fixnum 对象调用 #calculate,这个计算将由 Fixnum#* 完成,从而得到一个具体的Fixnum 结果。相反,如果我们用 Sign 对象调用它,Sign#* 操作将会调用并生成一个 Sign结果。

>> calculate(3, -5, 0)
=> 0
>> calculate(Sign::POSITIVE, Sign::NEGATIVE, Sign::ZERO)
=> #<Sign zero>

这给了我们在真正的 Ruby 程序中执行抽象解释的有限机会,可以把具体的参数替换成它们对应的抽象相对物,然后无需修改就可以运行其他代码了。

这个技术让人联想到自动化单元测试中打桩测试(test doubles)的方法(如存根和模拟对象)。桩是插到代码中的一个特别的占位对象,使用这种方法可以控制和校验代码的行为。在使用更现实的对象作为测试数据特别不方便或者特别昂贵的条件下,它们特别有用。

9.1.3 安全和近似:增加符号

目前为止可以看到,抽象世界中的计算比具体世界中的对应计算在准确性上要差一些,因为抽象会丢掉细节:在地图上规划的路线会表明在哪条路转弯,但不会说在哪条车道行驶,两个 Sign 对象的乘法会表明结果在零的哪一边,但不会告知实际结果值。

很多时候,结果不准确是没问题的,但对一个需要有用的抽象,很重要的是这个不准确是安全的。安全意味着这个抽象总是能给出真相:抽象计算的结果一定要与它对应的具体结果一致。如果不一致,抽象给我们的信息就不可靠,这可能比无用还要差。

Sign 抽象是安全的,因为把数字转换成Sign,并把它们乘在一起所给出的结果总是与计算数字本身然后把最终结果转成 Sign 一样:

>> (6 * -9).sign == (6.sign * -9.sign)
=> true
>> (100 * 0).sign == (100.sign * 0.sign)
=> true
>> calculate(1, -2, -3).sign == calculate(1.sign, -2.sign, -3.sign)
=> true

在这方面,Sign 抽象实际上是非常准确的。它准确保留了合适数量的信息并通过抽象计算把它们完美保留下来。在抽象与想要执行的计算不是那么匹配的时候,安全性问题变得更重要了,通过抽象加法实验我们将看到这一点。

两个数的符号如何确定它们加到一起得到的数字的符号,有一些规则,但它们并不是对所有可能的符号组合都有作用。我们知道两个正数的和一定是正数,而一个负数和零的和一定是负数,但如果把一个负数和一个正数加到一起会怎么样呢?在这种情况下,结果的符号取决于两个数绝对值的关系:如果正数的绝对值比负数的绝对值大,我们得到的答案就是正的(-20+30=10),如果负数的绝对值更大,那就会得到负数的答案(-30+20=-10),而如果它们的绝对值恰好相等,会得到零。但当然,每个数的绝对值正好是我们的抽象已经丢弃的信息,因此不可能在抽象世界中做出这种符号的判定。

对我们的抽象这是一个问题,因为它太抽象了,不能在每种情况下都准确地进行计算。如何处理这种情况呢?我们可以添加抽象加法的定义让它返回同样的结果——比如说只要不知道正确答案的时候就返回 Sign::ZERO——但那会不安全,因为那意味着抽象计算给出的答案可能与通过具体计算得到的答案不一致。

解决方案就是扩展抽象以适应这个不确定性。就像 Sign 值意思是“任何正数”和“任何负数”一样,我们可以引入一个新的,它只表示“任何数”。这实际上是最实在的答案,在遇到问题但没有足够细节的时候我们可以给出这个答案来:结果可能是负数、零,或者正数,不保证到底是哪种。让我们管这个新值叫作 Sign::UNKNOWN:

class Sign
  UNKNOWN = new(:unknown)
end

这给了我们安全实现抽象加法所需要的东西。计算两个数x和y之和的符号的规则是:

· 如果 x和 y 符号相同(同为正、同为负,或者都是零),那这个符号就是它们和的符号;

· 如果x 是零,它们的和与 y 的符号相同,反过来也是这样;

· 否则,它们和的符号未知。

很容易把这些规则转换成 Sign#+:

class Sign
  def +(other_sign)
    if self == other_sign || other_sign == ZERO
      self
    elsif self == ZERO
      other_sign
    else
      UNKNOWN
    end
  end
end

这样给出的行为正是我们想要的:

>> Sign::POSITIVE + Sign::POSITIVE
=> #<Sign positive>
>> Sign::NEGATIVE + Sign::ZERO
=> #<Sign negative>
>> Sign::NEGATIVE + Sign::POSITIVE
=> #<Sign unknown>

事实上,在输入中有一个符号未知的时候这个实现恰好做了正确的事情:

>> Sign::POSITIVE + Sign::UNKNOWN
=> #<Sign unknown>
>> Sign::UNKNOWN + Sign::ZERO
=> #<Sign unknown>
>> Sign::POSITIVE + Sign::NEGATIVE + Sign::NEGATIVE
=> #<Sign unknown>

但是我们确实需要回去修改 Sign#*的实现,以便它能正确地处理 Sign::UNKNOWN:

class Sign
  def *(other_sign)
    if [self, other_sign].include?(ZERO)
      ZERO
    elsif [self, other_sign].include?(UNKNOWN)
      UNKNOWN
    elsif self == other_sign
      POSITIVE
    else
      NEGATIVE
    end
  end
end

这样我们就有了两个可以使用的抽象操作。注意,Sign::UNKNOWN 是不传染的,即使一个未知数乘以零也仍然是零,因此任何中间存在的不确定性都可能在结束时被消化掉:

>> (Sign::POSITIVE + Sign::NEGATIVE) * Sign::ZERO + Sign::POSITIVE
=> #<Sign positive>

为了处理 Sign::UNKNOWN 引入的不准确性,我们还需要调整对正确性的认识。因为抽象有时候没有足够的信息给出准确答案,一个计算的抽象和具体版本也不总是能给出互相准确匹配的结果了:

>> (10 + 3).sign == (10.sign + 3.sign)
=> true
>> (-5 + 0).sign == (-5.sign + 0.sign)
=> true
>> (6 + -9).sign == (6.sign + -9.sign)
=> false
>> (6 + -9).sign
=> #<Sign negative>
>> 6.sign + -9.sign
=> #<Sign unknown>

怎么回事呢?抽象还安全吗?是的,因为在失去准确度返回Sign::UNKNOWN 的时候,抽象计算告诉我们的仍然是某种事实:“结果是一个负数、零,或者正数。”它没有执行具体计算所得到的结果有用,但它没错,并且它好在没有往抽象值中添加更多信息从而让抽象计算变复杂。

我们在代码中可以用一种比#== 更好的方式来比较符号,#== 现在太不利于安全检查了。这里想要知道的是:具体计算的结果在抽象计算所预测的结果范围内吗?如果抽象计算声称可能有几个不同的结果,那具体计算是实际产生了这个结果中的一个,还是完全是另外的结果呢?

在 Sign 上定义一个操作,它可以告诉我们两个抽象值是否用这种方式彼此关联。既然我们在测试一个 Sign 的值是否“落在”另一个里,那么叫它 #<= 方法吧:

class Sign
  def <=(other_sign)
    self == other_sign || other_sign == UNKNOWN
  end
end

这样我们就可以做测试了:

>> Sign::POSITIVE <= Sign::POSITIVE
=> true
>> Sign::POSITIVE <= Sign::UNKNOWN
=> true
>> Sign::POSITIVE <= Sign::NEGATIVE
=> false

现在可以检查安全性了,看一下是否每个具体计算的结果都落在了抽象计算预测的范围里:

>> (6 * -9).sign <= (6.sign * -9.sign)
=> true
>> (-5 + 0).sign <= (-5.sign + 0.sign)
=> true
>> (6 + -9).sign <= (6.sign + -9.sign)
=> true

安全性对包括加法和乘法在内的任何计算都能保持,因为当抽象计算无法给出准确答案的时候,我们已经设计了一个能进行安全近似的抽象。顺便说一下,能访问这个抽象让我们能对进行数的加和乘的 Ruby 代码做简单的分析。作为一个实例,下面是一个计算平方和的方法:

def sum_of_squares(x, y)
  (x * x) + (y * y)
end

如果想要自动分析这个方法以了解它的某些行为,我们可以把它处理成黑盒,用所有可能的参数运行它,这可能会造成永久运行;也可以检查它的源代码并尝试使用数学推理来推导出它的属性,这样很复杂。(而在一般情况下,由于 Rice 定理这注定失败。)抽象解释给了我们第三个选项,可以用抽象值调用这个方法,看这个计算的抽象版本会产生什么输出,因为抽象值的组合数只是一个很小的数字,所以为所有的可能输入这么做也 是可行的。

每个参数 x 和 y 都可能是负数、零或者正数,因此让我们看看输出都有哪些可能:

>> inputs = Sign::NEGATIVE, Sign::ZERO, Sign::POSITIVE
=> [#<Sign negative>, #<Sign zero>, #<Sign positive>]
>> outputs = inputs.product(inputs).map { |x, y| sum_of_squares(x, y) }
=> [
  #<Sign positive>, #<Sign positive>, #<Sign positive>,
  #<Sign positive>, #<Sign zero>, #<Sign positive>,
  #<Sign positive>, #<Sign positive>, #<Sign positive>
]
>> outputs.uniq
=> [#<Sign positive>, #<Sign zero>]

不必经过任何智能分析,这就能告诉我们 #sum_of_squares 只能产生零或者正数,从来不会有负数——对于读过代码的人来说,这是一个相当无聊的特性,但对机器来说,这都无所谓。当然,这种小技巧只对非常简单的代码起作用,但尽管是个小玩具,它还是展示了抽象如何能让一个难题变得更容易处理。

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

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

发布评论

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