常量传播

2018-05-28

遇到这个问题是这样的,select * from t where a < 5 and a > 5 我期望它能直接推导出来,这是一个空集,因为 a < 5 and a > 5 恒为假。结果呢?它给我搞出来了一个全表扫!这不就傻逼了。

嗯,扫了一眼我们的代码,开始没看太懂。于是决定自己想想怎么做。比如我们有下面这一系列的条件:

[= a 1] [= a c] [> b c] [= b d] [> c d] [= d f]

那么我们需要做的是,把 a = 1 这个常量表达式,不停地拿到集合里面去做替换,替换过程中,如果有新的常量表达式生成,可以记录下来。[= a c] 这个替换掉之后,就会生成一个 c = 1,继续用它执行下去,可以得出 [> b 1][> 1 d],像 [= d f] 这种消除不掉的,就继续保留下来。

那么这个算法的基本框架是这样子的,已知的常量表达式 [= a 1] 这种,放到一个叫做 Rules 的集合里面,而未知的待替换的集合,我们叫 Input,拿 Rules 里面的每一条,去 Input 里面做替换,过程中如果有新的 Rule 生成,则放到 Rules 集合里面。直到 Rules 集合的所有规则都使用过了,没有更多的替换时,算法结束。

为了体现 lisp 的优越性,我决定用 shen 语言写写这段代码(装个逼)。

(define constant-propagate0
        [] Input -> Input
        [Rule | Rules] Input -> (let Pair (apply-subst Rule Input [] Rules)
                                    Output (hd Pair)
                                    Rules (tl Pair)
                                    (constant-propagate0 Rules Output)))

这是一个递归函数。第一行,如果 Rules 为空了,算法就结束了。第二行,取第一条 Rule,将它应用到 Input 集合所有成员 (apply-subst Rule Input [] Rules),它会生成新的 Rules 和新的输入(这里叫 Output 了),递归继续做 constant-propagate0

(define apply-subst
    Rule [] Output Rules ->  (cons [Rule | Output] Rules)
    [= Var Const] [[= Var Var2] | Input] Output Rules ->
          (apply-subst [= Var Const] Input Output [[= Var2 Const] | Rules])
    [= Var Const] [[= Var1 Var] | Input] Output Rules ->
          (apply-subst [= Var Const] Input Output [[= Var1 Const] | Rules])
    [= Var Const] [[OP Var Var2] | Input] Output Rules ->
          (apply-subst [= Var Const] Input [[OP Const Var2] | Output] Rules)
    [= Var Const] [[OP Var1 Var] | Input] Output Rules ->
          (apply-subst [= Var Const] Input [[OP Var1 Const] | Output] Rules)
    Rule [H | Input] Output Rules -> (apply-subst Rule Input [H | Output] Rules))

apply-subst Rule Input 函数,第三个第四个参数,OutputRules 是为了尾递归才写成这样的,它做的事情就是用 Rule 去跟 Input 里面的各个比较,新的结果会放到 Output,如果有新规则生成会放到 Rules

好了,在 shen 语言 里面(随便找个实现,比如 shen-go),敲进去这两函数,然而执行

(constant-propagate0 [[= a 1]] [[= a c] [> b c] [= b d] [> c d] [= d f]])

会得到

[[= c 1] [> b 1] [= b d] [> 1 d] [= d f] [= a 1]]

其实这个算法是借鉴类型推导里面,一个叫做算法W 的做法,简化的版本(好吧,我根本不知道常量传播标准做法应该是怎么做的)。

有几个问题,这里只处理了 var = const 这种表达式的推导,这是最简单的情况。其实归纳下来有好几种更复杂的场景。

var1 = var2var > const

这种情况其实不难,继续套用上面的算法框架仍然是能够处理的。比如我们只把 var > const 这一类,作为 Rules 集合,把 var1 = var2 当作 Input 集合,拿规则集里面每条规则,过一遍 Input,就可以推导出更准确的 var 范围。

像之前的 [= a b] [= b c] [> a 5] [< c 3] ,先从 Rules 里面取出 [> a 5],将它应用到 [= a b] 上面,推出 [> b 5],新的 [> b 5] 被加到 Rules 里面,再应用它到 [= b c] 时,会推出 [> c 5],丢到 Rules 里面... 最后规则里面会出现矛盾 [< c 3] [> c 5],这种场景我们就可以判定 false 了。

比较难处理的,是 var1 > var2 这种场景的推导。当 var > const 作用于它时,结果不那么直观。比如 a > b并且 a > 3 ,这个得不出啥信息。但 a > b b > 3,这个可以推出 a > 3。也是可以丢到规则集里面继续利用的。主要麻烦在场景复杂了一些。

目前就想到这些吧。说说一个同事的脑洞。

  1. 如果把所有等号两边的点,都当做图上面的节点,然而 a < b 就构造一条从 a 到 b 的有向边。比如 [< a b] [> a 5] [< b 4],会构造出 a -> b b -> 4 5 -> a,如果我们再手动用 [< 4 5] 构造一条,4 -> 5,那么这个图就会成环了。也就是说,通过这样子构造一个图,然后检测成环,可以判断表达式是否是恒假的。

  2. 如果出现更复杂的 a - b < 3 b - c < 5 这种表达式,两者相加可以推出 a - c < 8。继续假想一个图,从 a 到 b 画一条出边,边的权值为 3,含义就是 a 到 b 节点的距离最少是 3。然后 b 到 c 画一条出边,边的权值为 5。把所有这种表达式都构造成图,那么求任意两节点之间的最短路径,就是两个变量的差值。比如 a 到 c 最短路径是 8,就是 a - c < 8。如果再把常量引入,有可能把各变量的一些范围信息推出来。

暂时还没有更多的想法,这哥们好喜欢图。好晚,不知道自己在想啥了,明天先好好改代码 bug 吧,不脑洞,实用为主。

constant propagate