普通视图

发现新文章,点击刷新页面。
昨天以前山楂片的博客

深度学习在语义分割中的应用(未完待续)

2021年10月10日 19:38

本篇笔记来自深度学习在语义分割中的应用的评论1一文。

介绍

本文剩余部分包括:

  1. 第二部分介绍了语义分割的问题、符号及一些背景
  2. 第三部分介绍了数据集、比赛和性能测试
  3. 第四部分评论现有模型
  4. 第五部分讨论上述模型的结果
  5. 最后总结全文

术语和背景介绍

通用深度网络架构

下面介绍当前最流行的几种架构:

AlexNet

AlextNet是深度CNN先驱,曾凭借84.6%的TOP5测试准确率获得ILSVRC-2012。它由五个卷积层、最大池化、ReLUs(Rectified Linear Units)、三个FC(fully-connected) layers以及dropout。

VGG(Visual Geometry Group)

该模型,也叫VGG16,因为其有16加权层。凭借92.7%的TOP5测试准确率获得ILSVRC-2013。VGG16和以前的模型的主要区别在于运用一堆卷积层和小的感受野(receptive fields),这使得参数变小,更加非线性,分辨能力更强,模型更加容易训练。

GoogLeNet

GoogLeNet以93.3%的TOP5测试准确率获得ILSVRC-2014,其特点是复杂、包含了22层、以及有一个最新介绍的inception模组。这种方法证明了CNN层不止能按照以前的方式排列,还可以通过别的方式堆积在一起。这些模组由一个NiN(Network in Network)层、一个池操作、一个大和一个小的卷积层组成。这些部分平行计算,然后通过卷积计算降维。因为这些模组的存在,网络可以减少参数数量和操作步骤。

ResNet

微软的ResNet以96.4%准确率赢得了ILSVRC-2016。其拥有152层和残差块(residual block)。在残差块中,每一层都可以将输入复制到下一层。这个方法基于,下一层总是学新的东西并且不同于已经编码的输入。此外,这种连接可以解决梯度消失问题。

ReNet

在ReNet中,他们一直用的序列RNNs,而不是多维RNNs。通过这种方式,RNNs的数量在每一层根据输入照片的维数d线性缩减,这样,每一个卷积层都会被四个垂直以及平行方向的RNNs代替。

迁移学习

不能直接应用迁移学习。一方面,必须要有预训练网络,通常会采用已有的网络架构;另一方面,使用微调(fine-tuning)而不是从头训练会有所不同。选择哪一层fine-tuning很重要,通常是网络的最上层————因为最下层会包含更多常见特征,也需要选择合适的学习率,通常会选择更小的,因为我们希望预训练的权重可以恰到好处,之后就可以不再大幅度改变。

数据预处理和增强

数据增强一般是将一系列转换应用于数据或者特征空间,或者两者皆有。常见的是应用于数据空间,将已有数据进行转换会生成新的样本。有很多转换可用:翻译、回转、扭曲、缩减、色彩空间变化、裁剪等。

数据集和比赛

2D数据集

  1. PASCAL Visual Object Classes (VOC):该比赛中的数据集包含ground-truth,并包含五种竞赛:分类、检测、分割、动作分类、人物布局。
  2. PASCAL Context:所有的照片包含像素点标签。包含540个类别。
  3. PASCAL Part:对象的每个部分都有像素点级别的分割。
  4. Semantic Boundaries Dataset(SBD):是PASCAL VOC的扩充,提供语义分割的ground-truth。
  5. Microsoft Common Object in Context(COCO):关于图片识别、分割和描述的大型数据集。
  6. SYNTHetic Collection of Imagery and Annotations:是一个关于虚拟城市的大型数据集。
  7. et al

2.5D 数据集

  1. NYUDv2:包含1449张室内RGB-D照片。
  2. SUN3D:大型RGB-D视频数据集,有8个标注序列。
  3. SUNRGBD:包含10000张RGB-D照片,适用于场景理解。
  4. et al

3D 数据集

  1. ShapeNet Part:ShapeNet的子集,包含细粒度的3D对象分割。原始数据集的16个类别中的31693个网格样本。
  2. Stanford 2D-3D-S:是一个多模型、大型室内空间数据集,有语义标注。
  3. et al

方法

解码变量(decoder variants)

解码或者map低分辨率的图片为分割做像素级处理是难题,这部分叫做decoder,也是FCN架构的divergence point。

整合上下文(Itegrating Context Knowledge)

语义分割既需要整合多个空间尺度的信息,又要平衡局部和整体信息。

  1. 有条件的随机区域(CRF):将低水平的照片信息和产生每个像素的类别分数的多类别推断系统结合起来,这种结合有助于抓取那些CNNs也没注意到的长期依赖并完善局部细节。
  2. 扩张的卷积:支持指数级扩张的感受野而不牺牲分辨率。
  3. 多尺度预测:运用有多种不同尺度的网络然后预测一个单一输出。
  4. 特征融合:将上层提取的整体特征和下层的局部特征合并。
  5. 循环神经网络:得益于特殊结构,循环神经网络可以同时适用长短序列。但问题是照片没有自然序列结构,标准vanilla RNNs集中在一维输入。

实例分割

区分同一类别的不同对象。

RGB-D数据

如果图片是RGB,深度数据就需要在每个像素用三种channels编码。RGB-D图片会抓取每个观点到FCN网络,然后得到关于每个图片的每个像素的40个类别的概率。

3D数据

视频序列

讨论

总结


  1. Garcia-Garcia, Alberto, et al. “A review on deep learning techniques applied to semantic segmentation.” arXiv preprint arXiv:1704.06857 (2017). ↩︎

语义分割论文概览

2021年9月26日 02:01

这篇文章是顺着一篇语义分割的综述1开始阅读相关论文。

介绍

早期的Object Detection多数采用尺度不变特征转换(SIFT)。深度学习应用到Object Detection,使得模型相较于传统算法能进行更复杂、精细地识别。这使得大家的研究方向着重于Generic Object Detection(而不是针对某个类别设计特殊的算法)。

目标

递进地来说,Object Detection的目标可以分为以下几种:

  1. 图像级别的分类:将图片标记为一个或多个类别
  2. 用边框围出事物并标类(边框有时会被叫做Axis-Aligned,因为它们是与坐标轴平齐的矩形)
  3. 语义分割:将图片的每个像素标类
  4. 事物实例分割:语义分割的基础上,对于同一类别的不同实例加以区分

挑战

  • 准确度相关的挑战
    • 类别内变化大
      • 内在因素:比如各种各样的椅子
      • 图像条件:背景、光照等
    • 类别数目多
  • 性能相关的挑战

SIFT2

⚠️警告: SIFT这个算法真的是复杂哭了。这里描述的是原论文里的方法。结合GitHub Repo rmislam/PythonSIFT的源码阅读可以极大地帮助理解原论文。当然这个源码似乎是原论文的改进版,里面用到了很多可怕的数学知识。 本文中的部分图片来源于这个Repo的教程。

该文提出了一种局部的图像特征,它不随缩放、平移、旋转的影响,并能部分地容忍光照、仿射、投影。它有生物学基础,即使是在杂乱、遮挡的情况下也能健壮地识别。

特征采用了分阶段过滤方案:首先寻找关键点。再对每个关键点会生成特征。然后匹配多张图的关键点,就可以寻找待识别的物体。

关键点定位

关键点定位:主要思想

(非人话版)通过高斯差分金字塔,从而尺度不变地选取关键点。其输入是一张图片,目标是选出图片中最有特点的点,类似下图(其中关键点用红点标出):

Example Input Image

高斯差分金字塔高斯差是将一张图片通过两个标准差不同的高斯模糊后,相互作差得到的一张新的图片。这张新的图片会包含某一层次的细节。通过采用标准差不断递增的高斯模糊图片,而后紧挨着的两个图片作差,就可以得到一系列变化由细致到粗糙的图片。这一系列的差值图片我们成为高斯差分金字塔。类似下图:

Example DoG Pyramid

极值点即关键点:差分金字塔某层上的极值点,通常是原图中某一尺度变化丰富的点。通过求解每层共享的极值点,就能得到在各个尺度下都变化显著的点,这些点就是我们想要寻找的关键点。

关键点定位:具体算法

我们用第$n$步指代算法的多个阶段,用第$n$步步骤$i$指代某个阶段的具体操作。

第一步:得到高斯差分金字塔。

  1. 对输入图片扩大到2倍(面积就4倍哦)使用双线性差值
  2. 选取$\sigma=\sqrt{2}$的高斯模糊处理先前的图片,得到图片A
  3. 再次使用$\sigma=\sqrt{2}$的高斯模糊处理图片A,得到图片B(此时相当于对步骤2输入图片直接做$\sigma=2$的高斯模糊)
  4. 产生一层高斯差分结果$A-B$
  5. 将图片B的大小是缩小为原来的$1/1.5$倍,采用双线性插值。如果得到的图片太小或完成一定次数,算法完成。否则将该图片作为步骤2的输入,执行步骤2

第二步:找到关键点。

  1. 从高斯差分金字的第1层开始,比较每个像素与其相邻的8个像素的大小,如果都大于或小于,则认为是极值点
  2. 接着计算这些极值点对应下一层的像素点(考虑第一步步骤5中的缩放),判断他们是否还为极值点,如果不是则筛去它们
  3. 重复第2步,直到遍历完所有层

由于极值点数目减少很快,所以第二步比第一步快很多。

Repo中的算法更加复杂,会对原图进行多次缩小,构成多个octave,然后对每个octave构建固定层的高斯差分金字塔。对于关键点选取,Repo是将某一像素所在的当前层连同前后层附近的点全挖去出来,形成了3x3x3的Cube,然后确保其中间点是其中最大的,从而粗略地定位斑点所在的位置和纵深(整数),作为下一步精确寻找的起始点。为了更精确地定位,Repo会用牛顿迭代法进一步寻找极值点的位置和纵深(实数),之后通过斑点的足够明/暗(响应的大小)和圆润与否进一步(Hessian矩阵特征值比值)筛选。

确认关键点的朝向

确认关键点的朝向:主要思想

(非人话版)通过寻找关键点的主要朝向,之后的特征提取可以在消去这个主要朝向后进行,从而使得特征提取不依赖于旋转方向。

像素$A_{ij}$梯度的模$M_{ij}$和朝向$R_{ij}$:对于第一步步骤2的图片A中的每个像素,我们定义其梯度的大小(模)和朝向:

$$M_{ij}=\sqrt{(A_{ij}-A_{i+1,j})^2+(A_{ij}-A_{i,j+1})^2}$$

$$R_{ij}=\mathrm{atan2}{(A_{ij}-A_{i+1,j},A_{i,j+1}-A_{ij})}$$

关键点的位置修正:之前得到关键点的位置是个整数,这里原论文没有细说怎么修正到sub-pixel,但可以想见是使用二次函数拟合局部点,然后找到极值位置。

对光照环境的健壮:设了个阈值,只考虑大于0.1倍最大可能光照的值。(嗯,我没看懂他在说啥)

关键点的主要朝向计算:挖取关键点周围的像素,计算它们的梯度方向,然后投放到36个桶里(每个桶宽度是$10^\circ$)。注意每个像素对桶的贡献是加权的,权重符合以关键点为中心,标准差为当前层$\sigma$ 3倍的高斯分布。之后,这个直方图会被平滑一下,然后选择最高点。关于“周围”的划分,由于是高斯分布,所以3倍标准差以外的点贡献很小,就可以不考虑算作“周围”。

确认关键点的朝向:具体算法

第三步:关键点的主要朝向计算。

  1. 初始化36个桶,以及一个标准差为关键点所在层$\sigma$ 3倍的高斯核
  2. 对于关键点所在层的图片$A$(而非$B$),挖取周围的像素(论文没说,我觉得再上面标准差基础上乘3倍就可以了,也就是所在层$\sigma$ 9倍),计算其梯度朝向,找到其对应的桶,往桶中加上该像素对应的高斯核值
  3. 用一个平滑函数卷积一下36个桶(Repo里用的卷积核是$[1,4,6,4,1]/16$)
  4. 找到数额最大的桶作为方向,这里当然也要使用包括最大桶及其左右的两个桶(共3个点),用二次函数插值找最大点

Repo中为了算法更稳定,它会寻找多个极值点,在极值点是最大值的0.8倍以上时,会创建多个位置相同,方向不同的关键点。

关键点特征提取

关键点特征提取:主要思想

文章扯了一大堆生物学。反正就是把关键点周围的像素,旋转一下,抵消掉主要朝向(这样图片旋转了,特征也不变)。然后统计不同位置(分成4x4个大致位置),不同朝向(分成8个大致方向)的像素点的梯度大小。

不过吧,论文里做的更加优雅点,有种双线性插值的感觉,然后有些数字对不太上,读得很困惑。

关键点特征提取:具体算法

第四步:

  1. 创建4x4x8的特征张量,前两个维度表示坐标(这里的每个桶代表4倍关键点大小的像素间距),后一个维度表示方向(这里每个桶代表梯度向量$45^\circ$夹角)
  2. 将关键点周围的点旋转抵消掉主要朝向,然后计算对应的特征张量的索引(这里索引是3个实数)即位置和方向,以及要存入的值即梯度大小
  3. 将这个梯度大小按索引小数部分对应的权重分配到相邻的8个整数索引上
  4. 特征张量归一(除以L2范数)

匹配图像

两幅图的关键点在特征的距离上彼此做个最近邻匹配,然后匹配的节点的坐标送进一个大的表示仿射变换的齐次线性方程组,最后来个最小二乘法。

深度学习模型分类

总的来说模型可以分为两类:

  1. 两阶段模型:先预处理选出候选区域
  2. 一阶段模型:无预处理阶段

两阶段模型

RCNN(Regions with CNN Features)3

  1. 与类别无关的候选区域选取,方案为Selective Search4
  2. 从图像中裁剪出相同大小的候选区域用于CNN模型预训练
  3. 用SVM对CNN模型中提取的特征进行分类
  4. 用边框对各类别的特征进行回归

SPPNet(Spatial Pyramid Pooling Net)

之前说到,在RCNN过程中,需要从一张图片中裁剪出的众多区域里提取CNN特征,导致RCNN的训练较慢。而SPP中可以输入不同大小的区域,将其应用于卷积层中,可以使RCNN显著提速。

Fast RCNN

Fast RCNN同时在softmax分类器和边框回归训练,还在CONV和FC layer之间添加了RoI(Region of Interest)池给每一个候选区域提取一个已修正长度的特征。相比RCNN和SPPNet,Fast RCNN更加高效。

Faster RCNN

Faster RCNN用更高效和精确的RPN(Region Proposal Network)来生成候选区域,RPN和Fast RCNN共享CONV特征,然后将其输入分类器或边框中训练,使得计算更高效。

RFCN(Region based Convolutional Network)

在RFCN中,没有隐藏的FC layer。RFCN和Faster RCNN的区别仅在于RoI,在Faster RCNN中,RoI之后的计算不能被分享;而在RFCN中,将一些特殊的CONV层作为FCN的输出来构造一套对位置敏感的地图,这些地图上的RoI不同于标准的,其精确度和Faster RCNN差不多,但速度更快。

Mask RCNN

Mask RCNN处理轴对象实例分割,分为两个阶段,第一个阶段是RPN,第二阶段则是在分类和边框训练的同时在CNN特征地图上进行FCN。

Light Head RCNN

为了提高RFCN的速度,尽可能减少RoI的计算,Li运用了一种大的核分裂卷积来产生更小的特征。

Selective Search

基于图(数据结构)的分割算法5

Selective Search的第一步是使用基于图(数据结构)的分割算法。具体来说,对于图像中的每个通道,我们将其看作由边和节点组成的带权无向图$G=(V,E)$,其中每个像素$p_i$对应于一个节点$v_i\in V$。而边,则是连接相邻的8个像素(论文指出可以采用其他的方法)。边的权重表示的是像素的不相似程度(越大越不相似),这里直接使用像素强度$I(p_i)$的差异作为权重:

$$w(v_i,v_j)=|I(p_i)-I(p_j)|$$

通常在进行这步之前,会使用$\sigma=0.8$的高斯模糊(模糊半径1.6)处理一下图片。

接下来,我们定义该图连通分量$C$的内部差异$Int(C)$。它被定义为其最小生成树$MSE$(Prim算法可以得到)最大的边权。

$$Int(C)=\max_{e\in MST(C)} w(e)$$

然后,我们定义两个连通分量$C_1,C_2$的最小内部差异$MInt(C_1,C_2)$:

$$MInt(C_1,C_2)=\min(Int(C_1)+\tau(C_1),Int(C_2)+\tau(C_2))$$

其中函数$\tau$可以调控差异,它越大象征着内部差异越大,相对地更能容忍连通区域之间的大差异,从而促使更大的连通区域形成。可能的设计包括使得细条形的$\tau$比较大,从而使得最终分割不太包含细条形的区域。这里我们使用:

$$\tau(C)=k/|C|$$

其中$|C|$表示连通分量节点的个数。这使得小的连通区域不太可能形成。$k$越大,算法更易形成越大的区域。对于128x128的图片,$k=150$是不错的选择;对于320x240及更大的图片,$k=300$是不错的选择。

算法的结果是一个分割$S$,它被定义为互不交且之间无空隙的连通分量的集合。

最后算法如下:

  1. 对边集$E$按权重递增排序$\pi=(o_1,\dots,o_m)$($m=|E|$)
  2. 初始化分割$S$,其中每个节点各自成一个连通分量。
  3. 对于$\pi$中的每个边$o_q=(v_i,v_j)$:
    1. 如果$v_i$和$v_j$分属于$S$中不同的两个连通分量$C_i$和$C_j$,且$w(o_q)\leq MInt(C_i,C_j)$:
      1. 合并$S$中的连通分量$C_i$和$C_j$

对于彩色的图片,这个算法在每个通道上运行,最终两个像素在同一个连通分量里当且仅当它们在各个通道上都在同一个连通分量里。

Selective Search剩余算法

一阶段模型

DetectorNet

DetectorNet将边框作为分类问题,给定一个图片,他们用一个网络预测一个大致的格子,然后用四个其余的网络预测出对象的上、下、左、右。Detector必须对每张图片采取重要的样本,然后用网络对每个样本的各部分训练。

OverFeat

OverFeat产生一组特征向量,每个都代表一个输入的图片中的位置以及可以预测物体的出现。一旦一个物体被识别,相同的特征就会被用来预测一个边框分类器。除此以外,OverFeat能通过处理原始图片六倍大小得到多规模的特征来提高整体表现,并将其整合到一起,得到一个最后的特征向量。OverFeat比RCNN速度更快,但精确度不足。

YOLO(You Only Look Once)

不同于其他基于区域的方法,YOLO从图片整体获得特征。YOLO将一张图片分为SS个格子,每个格子预测C类概率,B个边框和置信分数,这些预测都被编译成SS*(5B+C)张量。

YOLO容易忽略一些小的对象,因为格子分割是很粗糙的,而每一个格子又只能包含一个对象。

YOLOv2 and YOLO9000

YOLOv2是YOLO的增强版,用DarkNet19取代了GoogLeNet,优化了现有工作。

YOLO9000用联合优化的方法同时训练了ImageNet和带WordTree的COCO,可以观测9000多个对象类别。

SSD(Single Shot Detector)

SSD比YOLO更快,并与基于区域检测的检测器,如Faster RCNN有差不多的精确度。SSD高效地结合了Faster RCNN中的RPN、YOLO以及多规模CONV特征实现了更快更精确的检测。和YOLO类似,SSD检测一些修正过的边框,然后从中给对象打分,最后由NMS产生最后的检测结果。

基本子问题

基于DCNN的对象表示

特征表示已经转移成为了架构的设计问题。

提高对象表示的方法

检测对象通常需要处理大量数据,一个经典的策略是运行能处理大量图片的检测器,但是会受制于时间和内存;另一种是CNN可以一层一层地计算特征层次,子抽样的层会得到一个如金字塔般固定的规模。

三种多规模对象检测:

  1. 检测多CNN层的联合特征
  2. 检测多CNN层
  3. 上面两种方法的结合

上下文建模

上下文可以分为三类:

  1. 语义上下文:不同场景中对象被发现的可能性不一样
  2. 空间上下文:在不同位置发现对象的可能性不同
  3. 尺度上下文:对象有一部分限制的大小和其他场景中的规模相关

Global context

根据图片或场景,global context可以作为检测对象的线索。

Local context

Local context考虑到了对象和其周围的区域。一般来说,在对一些对象之间的关系建模时要求不同类、位置、规模的边框是有逻辑的。在深度学习领域,相关模型的研究很有限,具有代表性的有SMN(Spatial Memory Network)、Object Relation Network、SIN(Structure Inference Network)。

检测方法

一个好的检测建议应该有以下几种特点:

  1. 高召回,即只需一点建议就可以实现
  2. 建议尽可能精确地匹配对象
  3. 高效

边框建议法

对象分割建议法


  1. Liu, Li, et al. “Deep learning for generic object detection: A survey.” International journal of computer vision 128.2 (2020): 261-318. ↩︎

  2. Lowe, David G. “Object recognition from local scale-invariant features.” Proceedings of the seventh IEEE international conference on computer vision. Vol. 2. Ieee, 1999. ↩︎

  3. Girshick, Ross, et al. “Rich feature hierarchies for accurate object detection and semantic segmentation.” Proceedings of the IEEE conference on computer vision and pattern recognition. 2014. ↩︎

  4. Uijlings, Jasper RR, et al. “Selective search for object recognition.” International journal of computer vision 104.2 (2013): 154-171. ↩︎

  5. Felzenszwalb, Pedro F., and Daniel P. Huttenlocher. “Efficient graph-based image segmentation.” International journal of computer vision 59.2 (2004): 167-181. ↩︎

Coq学习笔记(未完待续)

2021年8月29日 23:33

这篇文章来自《Coq in a Hurry》1的总结。

表达式和逻辑公式

编写正确的公式

使用Check命令能查看公式的类型:

> Check True.
True : Prop

> Check 3.
3 : nat

a: A可以表示a的类型是A,或者aA的证明。它可以位于表达式中,显式指明表达式类型。

常见的类型有Prop表示命题,nat表示自然数。复杂的类型可以通过逻辑联结词(/\\/)和诸如加、乘、对(a, b)(其类型为A * B)等等创建。使用fun能创建λ表达式(其类型为A -> B,右结合)、forallexists创建量词:

> Check (fun x:nat => x = 3).
fun x : nat => x = 3 : nat -> Prop

> Check (forall x:nat, x < 3 \/ (exists y: nat, x = y + 3)).
forall x : nat, x < 3 \/ (exists y : nat, x = y + 3) : Prop

使用let .. in可以给表达式一个临时的名字,注意到函数应用不需要括号。

> Check (let f := fun x => (x * 3,x) in f 3).
(let f := fun x : nat => (x * 3, x) in f 3 : nat * nat

有些符号被重载了,比如*既表示数字的乘法,又表示笛卡尔积类型。使用Locate命令可以找到符号背后的函数。

> Locate "_ <= _".

项是合法的需要遵守:

  1. 语法正确
  2. 类型正确

Check命令不仅进行了上面的检查,还给出了表达式的类型。

对表达式求值

使用Compute可以对表达式求值。

用Coq编程

Coq中的程序用函数表示,简单的程序可以被Coq执行,复杂的可以用Extraction命令转换为其他编程语言的。

定义新的常量

使用Definition关键字可以定义常量:

> Definition example1 := fun x : nat => x*x+2*x+1.

上面的形式等价于:

> Definition example1 (x : nat) := x*x+2*x+1.

定义完后,就可以在诸如CheckCompute的命令中使用。使用Reset后面跟一个名字可以清除该名字。可以使用Print命令查看一个对象的定义。

布尔条件表达式

Coq内置了布尔(bool)值truefalse。为了使用它,你需要导入Bool库。

> Require Import Bool.

布尔值可以使用if ... then ... else ...。后者接受一个模式返回符合的;而后者接受一系列的模式,返回都符合的。

使用自然数计算

需要使用Arith库进行自然数的计算。自然数有两种形式,一种是0,另一种是S p,其中p是一个自然数。可以使用match ... with ... end进行模式匹配。第一个子句的|可省略。

Definition is_zero (n:nat) :=
    match n with
        0 => true
    | S p => false
    end.

如果要使用递归,可以使用Fixpoint关键字。Fixpoint必须遵守一个约束叫structural recursion,即递归只能作用在初始参数(上面的p)上。这个约束确保计算是可终止的。递归函数可以有多个参数,这时候structural recursion必须在一个参数上是成立的。

Coq还支持深模式匹配,Coq会检查是否所有的模式都匹配了:

Fixpoint evenb n :=
    match n with
            0 => true
    |       1 => false
    | S (S p) => evenb p
    end.

使用列表计算

需要导入List库。如果要将几个元素放入列表中,需要使用::,它将左边的元素添加到右边列表的头,用nil表示空列表:

Check 1::2::3::nil.

注意nil需要上下文确定其具体类型。可以使用类型注解表示其类型。

Check (nil : list nat)

有一些预定义的列表函数:

  • app,别名++:链接列表。
  • map:对列表的每个元素做映射。

列表也可以模式匹配为nila::tla是一个元素,tl是剩余的列表)。同样也可以递归,递归只能作用在剩余的列表上。

命题和证明

找到已有的证明

Search后面跟标识符可以搜索已有的证明。SearchPattern后面跟一个模式表达式(使用_表示一个不完整的子表达式)。SearchRewriteSearchPattern类似,只是寻找的一定是个相等的谓词。SearchAbout搜索所有的与某个符号相关的证明。

构建新的证明

构建证明的通常方式是“目标导向的证明”:

  1. 使用Theorem或者Lemma开始一个定理。
  2. Coq显示需要证明的命题,已经可以用于该证明的上下文(上下文在=====上方,目标在下方)。
  3. 用户输入命令,分解目标。
  4. Coq显示还需要证明的命题。
  5. 回到3。

步骤3称为tactics。某些tactics减少了目标的数量。当所有目标都解决,证明就完成了,这时候可以输入Qed.命令,该命令保存了证明。一个简单的证明如下:

Lemma example2 : forall a b: Prop, a /\ b -> b /\ a.
Proof.
    intros a b H.
    split.
        destruct H as [H1 H2].
            exact H2.
        intuition.
Qed.

上下文中的内容一般是a: type或者H: formula的形式,我们称为假设,它表示我们现在有的事实。destruct H as [H1 H2]H为两个命题的合取时可以使用。它的作用是创建两个新的假设,名字为H1H2。下表包含了常见的tactics。

Hypothesis H conclusion
$\Rightarrow$ apply H intros H
$\forall$ apply H intros H
$\land$ elim Hcase Hdestruct H as [H1 H2] intros H
$\neg$ elim Hcase H intros H
$\exists$ elim Hcase Hdestruct H as [x H] exists v
$\lor$ elim Hcase Hdestruct H as [H1 | H2] left或者right
$=$ rewrite Hrewrite <- H reflexivityring
False elim Hcase H

当你在处理假设时,可以用Hypothesis那一列;处理结论时用conclusion那列。

我们用exact H表示我们要证明的结论就在上下文中,assumption可以做到类似的效果。intuition可以用于自动证明。

当使用elim或者case,会将事实放在结论处,其目标会成为蕴含的前件。这些前件稍后可被intros引入。因此有destruct可以同时完成这两件事。

所有的以假设作为参数的tactics都可以以定理作为参数。

用基本tactics的另一个例子

(未完待续)


  1. Yves Bertot. Coq in a Hurry. 3rd cycle. Types Summer School, also used at the University of Goteborg, Nice,Ecole Jeunes Chercheurs en Programmation,Universite de Nice, France. 2016, pp.49. inria-00001173v6 ↩︎

区间分析

2021年5月20日 14:30

这篇文章的内容来自Allen的Control Flow Analysis1

基础概念

有向图$G=(B,E)$有节点(块)集合$\{b_1,b_2,\dots,b_n\}$和边集合$\{(b_i,b_j),(b_k,b_l),\dots\}$组成。每个有向边是一个节点有序对$(b_i,b_j)$(不一定互异),代表有向边从$b_i$出发到$b_j$。立即前驱函数$\Gamma^1_G:B\rightarrow P(B)$($P(B)$是$B$的幂集)被定义为$\Gamma^1_G(b_i)=\{b_j\mid(b_i,b_j)\in E\}$ ,可空。类似的可以定理立即后继函数$\Gamma^{-1}_G:B\rightarrow P(B)$被定义为$\Gamma^{-1}_G(b_j)=\{b_i\mid(b_i,b_j)\in E\}$,同样可空。

一个图是连通的,当且仅当任何一个节点可以通过不断使用$\Gamma^1_G$和/或$\Gamma^{-1}_G$得到。注意这里的连通是不讲求方向的。本文讨论的图是有向且连通的(这里的连通应该是指从$e_0$出发能够到达)。

基本块是有唯一入口和唯一出口的指令序列。它可能有多个立即前驱和立即后继,甚至立即前驱、立即后继是自己。控制流图是节点为基本块,边表示控制流路径的图。

图$G=(B,E)$的子图是$G’=(B’,E’)$,其中$B’\subseteq B,E’\subseteq E$,此外$E’\subseteq B’\times B’$。

一个路径$P$是可以一个节点序列$(b_1,b_2,\cdots,b_n)$,其中$b_{i+1}\in\Gamma^1_G(b_i)$(这里假定不存在重边)。边是隐含的$(b_i,b_{i+1})\in E$。节点和边都可以不是唯一的。

节点$q$是节点$p$的后继当且仅当存在路径$P=(p,\dots,q)$。类似可以定义前驱。一个节点可能既是另一个的前驱又是其后继。

一个闭路径,或者环路是一个$b_1=b_n$的路径$P$。如果除了$b_1$和$b_n$,这个路径上的节点没有重复,那称之为简单环路;否则称之为复合环路

路径$P$的长度$\delta(P)$是路径中边的数目。基于此可以定义两节点之间的最短路:$\delta_\text{min}(p,q)=\min\{\delta(P_i)\mid P_i=(p,\dots,q)\}$。

有向图的一个强连通分量是一个有向子图,其中从任意节点到任意节点。因而每个节点一定在一个闭路径上,且每个节点都是其本身的前驱和后继。闭环路所代表的子图是一种强连通分量的特例。我们可以观察到强连通分量之间有3种关系:

  1. 分离:没有共享的节点;
  2. 包含:一个强连通分量是另一个的子集;
  3. 其他:有部分节点共享,这时候可以合并成一个更大的强连通分量。

如果对于$G$中的任何一个强连通分量$R$,其他的(不是其子图的)强连通分量$R’$与其不共享节点,那么称这个强连通分量$R$为最大的。一个我认为没有太多用的基于强连通分量建立偏序关系的方案就省略了。

支配关系

在一个有向图内,一个没有后继的节点成为出口节点。类似的定义不太适合可能存在循环入边的入口节点,因而入口节点被认为是控制流图中包含程序入口的节点,它是唯一的。然后给这个有向图添加一个没有前驱的初始节点$e_0$作为入口节点的唯一前驱。

如果一个节点$b_i$出现在了每条从$e_0$到$b_k$的路径上,那么称$b_i$是前支配(back dominate;predominate)$b_k$。令$\mathcal{P}=\{P\mid P=(e_0,\dots,b_k)\}$,则其前支配者集合$BD(b_k)$为:

$$BD(b_k)=\{b_i\mid b_i\neq b_k\land b_i\in\cap\mathcal{P}\}$$

译注:这里的支配者把本身排除了,但实际上一般认为任何一个节点支配其本身 。$b_k$的立即前支配者$b_i$是前支配者集合中离$b_k$最近的。

$$b_i=\underset{b_j\in BD(b_k)}{\text{arg\,min}}\delta_\text{min}(b_j,b_k)$$

立即前支配者存在且唯一。由于$e_0$是所有节点的前支配者,所以一定存在。如果同时存在两个不同的立即前支配者,它们有相同的距离,必然在不同的路径上;但又由于立即前支配者必然出现在了每条路径上,因而矛盾,一定唯一。

一个有趣的发现是$BD(b_k)$可以通过$\delta_\text{min}$建立严格偏序关系。

$$BD(b_k)=(b_1,b_2,\dots,b_j)~~\text{where}~b_1=e_0$$

在上式中对任意$1\leq m<n\leq j$,有$\delta_\text{min}(b_m)>\delta_\text{min}(b_n)$。不仅如此,对任意的$1\leq m<j$,有$b_m$是$b_{m+1}$的立即前支配者;对任意的$1\leq m<n\leq j$,$b_m$是$b_n$的前支配者。

类似地我们可以定义节点$b_i$后支配节点$b_k$当且仅当$b_i$出现在了每条$b_k$前往任意出口的路径上。同样地,我们可以引入一个节点$x_0$作为所有出口节点的后继。后支配的相关概念和前支配类似,这里不重复表述了。

一个关节节点出现在了每条从入口到出口的路径上。对一有唯一入口$e_0$的图,关节节点就是$e_0$以及$e_0$的后支配者集合。

区间

给定一个节点$h$,区间$I(h)$是指最大的,以$h$为唯一入口的子图,并且该子图中的所有环路都包含$h$。$h$被称为区间头或者头节点。区间可以用其包含的节点表示,区间的边则可以被隐含地得到。

通过选取适当的节点作头节点集合的元素,一个图可以被唯一地划分为区间。以下是一个划分图的算法。

算法用到以下的数据结构:

  • $H$:存放处理过的和待处理的节点;
  • $I(h)$:$Map\langle B, Set\langle B\rangle\rangle$,以$h$作为区间头的节点集合。

过程A:

  1. 添加$e_0$到$H$中并标记为待处理。
  2. 如果$H$有待处理的$h$:
    1. 标记$h$为已处理。
    2. $I(h)\leftarrow\{h\}$
    3. 对所有的$b\in G$且$b\notin I(h)$且$\Gamma^{-1}_G(b)\subseteq I(h)$:(这一步不断重复,直到无法继续,实际实现需要一个工作队列)
      1. $I(h)\leftarrow I(h)\cup\{b\}$
    4. 对所有的$b\in G$且$b\notin H$且$b\notin I(h)$且$\Gamma^{-1}_G(b)\cap I(h)\neq\varnothing$:
      1. 添加$b$到$H$中并标记为待处理。

区间分析的例子1

区间分析的例子

上图包含以下区间:

区间 节点集合
$I(1)$ $1$
$I(2)$ $2$
$I(3)$ $3,4,5,6$
$I(7)$ $7,8$

首先我们证明所有的$I(h)$都是最大的、单入口的,且所有$I(h)$的环路都包含$h$,稍后我们会证明这是个划分。

论断1-3论证算法的正确性。

论断 1 $I(h)$只包含一个入口节点,$h$。

证明 假设还存在另一个节点$b\in I(h),b\neq h$是入口节点,那么$b$的立即前导节点中一定存在节点不在$I(h)$中,这与算法中$b$添加到$I(h)$的条件即步骤2.3矛盾。此外可以注意到,$h\neq e_0$有至少一个立即前导节点在$I(h)$外,这可以有步骤$2.3$推导出。

论断 2 $I(h)$中所有的闭环都包含$h$。

证明 假设存在一条环路$P=(b_1,b_2,\dots,b_n,b_1)$不包含$h$。我们知道$b_{i-1}$是$b_i$的立即前驱节点。因此只有$b_{i-1}$成为$I(h)$的成员后,$b_i$才能成为;此外,只有$b_n$成为了$I(h)$的成员后之后,$b_1$才能成为。结果就是没有一个能成为$I(h)$的成员。矛盾。

论断 3 $I(h)$是最大的。

证明 由步骤2.3可以得到,即不断执行知道无法有更多的节点添加的步骤。

区间具有一些性质,这里在下方给出,这些限制不限于过程A给出的区间,也不需要“最大”这个性质。

论断4-7寻找区间与支配的关系。

论断 4 区间头支配区间内的所有节点。

证明 论断1的推论。

对于区间$I(h)$内的任意一个节点$b_i$可以定义一个更加严格的局部后继函数$L^1_I$,将后继限制在区间内的非头节点中:

$$L^1_I(b_i)=\{b_j\mid b_j\in\Gamma^1_I(b_i)\land b_j\neq h\}$$

借助这个局部后继函数,可以定义局部前导函数$L^{-1}_I$。特别地我们有$L^{-1}_I(h)=\varnothing$。

使用局部后继函数,可以在区间内定义一种特殊的路径:前向路径$F=(b_1,b_2,\dots,b_n)$,其中$b_{i+1}\in L^1_I(b_i)$。可以注意到从$h$到$I(h)$内某节点的所有路径上的节点都在$I(h)$内(这是支配决定的)。

论断 5 可以通过局部后继函数在区间内的节点定义偏序关系。也就是对于给定的区间,可以表示为节点的序列$I(h)=(b_1=h,b_2,\dots,b_n)$,并且对于所有的$i<j$,要么$b_i$在某个前向路径上是$b_j$的前驱,要么$b_i$和$b_j$不同时出现在任何一个前向路径上。

证明 由过程A可以看出一个非$h$的节点在变成$I(h)$成员前,其立即前驱节点必须已经成为$I(h)$的成员。

其实这个区间序列就是过程A中添加到$I(h)$的先后顺序。

论断 6 前支配列表中序列的相对顺序和区间序列是一致的。

证明 在一个区间中,如果$b_i$是$b_j$的前支配者,那么$b_i$会出现在$h$到$b_j$的每个前向路径上。

这个定理是我非常关注的。它揭示了区间(归约)和支配的关系。我现在只想知道从区间序列中能否得到支配者树。

论断 7 对于区间成员$b_k$,它的前支配者序列为$BD(b_k)=(b_1=e_0,b_2,\dots,b_j)$。那么一定有一个$b_i\in BD(b_k)$满足$b_i=h$,且对于所有$b_i$之后的节点$b_l,i<l\leq j$,$b_l$一定是区间的成员。

证明 $b_l$出现在所有的从$h$到$b_k$的路径上,因而$b_l$一定是区间成员。

这个定理给出了一种基于区间的求解前支配者集合的思路。

论断8-9寻找区间和强连通分量的关系。

论断 8 区间中的任何强连通分量一定包含区间头。因此一个区间不可能包含分离的前连通分量。

证明 由任何闭路径都包含$h$可以得到。

论断 9 如果区间内部存在一个强连通分量,那么一定存在从这个强连通分量内的任意节点到区间内的任意节点的路径。

证明 一定存在从这个强连通分量内的任意节点到区间头的路径,也一定存在从区间头到区间内的任意节点的路径。

定义区间出口节点为没有立即后继(全图的出口节点)或者存在至少一个立即后继不在区间中的节点。论断10-11寻找求解区间关节节点的方案。

论断 10 对于区间而言,区间头是一个关节节点。

证明 真的很显然。

论断 11 所有区间头的区间内后支配者,以及区间头,就是区间的关节节点。

两终端子图有时也会是研究者感兴趣的。两终端子图是只有一个出口节点的区间。

接下来我们给出寻找区间内强连通分量、区间的关节节点以及区间内每个节点的前支配者的算法。这些算法可以嵌入过程A中,使得整个算法一步完成。

在具体实现上,为了快速地计算,这些算法可以使用位图以加速集合运算。

过程B: 计算出区间内每个节点的前支配者。

  1. $BD(h)\leftarrow\varnothing$
  2. 按照区间序列的顺序遍历节点$b_j$:
    1. $BD(b_j)\leftarrow\bigcap\limits_{b_i\in L^{-1}_I(b_j)}(b_i\cup BD(b_i))$

过程C: 求出区间的关节节点。

  1. $A\leftarrow\bigcap\limits_{b_i\in\text{IntervalExits}}(b_i\cup BD(b_i))$

过程D: 找到节点$b_i$的所有局部前驱$LP(b_i)$。

  1. $LP(h)\leftarrow\varnothing$
  2. 按照区间序列的顺序遍历节点$b_j$:
    1. $LP(b_j)\leftarrow\bigcup\limits_{b_i\in L^{-1}_I(b_j)}(b_i\cup LP(b_i))$

一个锁节点是区间中以区间头作为立即后继的节点。一个不存在锁节点的区间也就不存在强连通分量。 分

过程E: 求出包含锁节点的区间的强连通分量。

  1. $SCR\leftarrow\bigcup\limits_{b_i\in\text{IntervalLatchings}}(b_i\cup LP(b_i))$

另一种等价的算法是从锁节点出发,不断添加所有的立即前驱直到到达区间头。这种算法不需要求解$LP$。

使用区间划分图

接下来,我们证明过程A产生出来的区间集合$\Phi=\{I(h_1),I(h_2),\dots\}$组成了唯一的$G$的划分。所以我们要证明$\Phi$覆盖了$G$,任意两个区间的交为空,以及$\Phi$是唯一的。

论断 12 $\Phi$覆盖了$G$。

证明 如果$b\in G$且$b$不属于任何区间。由于$G$是个连通的图,那么$b$要么是$e_0$要么至少有一个立即前驱。如果$b=e_0$,那么$e_0\in I(e_0)$。如果它有至少一个立即前驱,那么它要么和立即前驱在同一区间内,要么它形成了新的区间头,要么立即前驱也不属于任何区间。对于最后一个情况不断递归就会得到$e_0$不属于任何区间,因而最后一个情况不成立。(其实这应该用数学归纳法)

论断 13 $\Phi$中的区间是分离的,也就是对于不同的$I(h)$和$I(h’)$,有$I(h)\cap I(h’)=\varnothing$。

证明 如下:

  1. 区间头一定是互异的,即$h\neq h’$,因为过程A中,每个节点成为循环头后,就会被标记为已处理,从而不可能再次成为循环头。

  2. 区间头不可能成为另一个区间的成员。假设区间头$h$是区间$I(h’)$的成员。故$h$的所有立即前驱也在$I(h’)$中。$h$要成为区间头,必然有一个但不是全部的前驱还在某个别的区间$I(h’’)$中(这里不能假设前驱只归属于一个区间)。我们将要证明$h’’$也是区间$I(h’)$的成员。

    假设立即前驱$b$既在区间$I(h’)$中,又在区间$I(h’’)$中,我们有$b$同时被$h’$和$h’’$前支配。由于前支配集合是严格偏序的,所以要么$h’$前支配$h’’$要么反过来。由于$h$有不在区间$I(h’’)$的前驱$c$,故而是$h’$前支配$h’’$(否则由区间最大会得到$h’$和$c$都在$I(h’’)$中),进而由论断7得$h’’$在$I(h’)$中。

    这样不断递归下去,只能得到没有区间头位在$I(h’)$中。

  3. 不同区间的交为空。假设存在$b\in I(h)\cap I(h’)$,由上面的讨论我们知道$b$不是任何区间头。如果$b$要同时出现在两个区间中,那么它的立即前驱也必须出现在两个区间中。不断递归下去就会得到两个区间头出现在两个区间中,从而矛盾。

论断 14 $\Phi=\{I(h),I(h’),\dots\}$是唯一的。

证明 实际上由于区间总归是最大的,所以当区间头确定完后,区间就确定了。由于区间之间是不会重叠的,所以区间的先后顺序是不会影响区间头的选取,只是区间头的顺序发生了变化。

接下来我们扩充区间的定义。先前的区间被称为一阶区间,区间所在的原图被称为一阶图。我们会构造高阶图和高阶区间,所以我们用上标表示阶。

二阶图是将每个一阶区间合并成一个节点之后形成的图。二阶图节点的立即前驱是原图中区间头的非区间内立即前驱;立即后继则是原图中区间出口节点的非区间立即后继。二阶区间是二阶图的区间。

不断如此就能构建高阶图和高阶区间。最后的高阶图要么只有一个节点组成,称原图为可归约图;否则,称原图为不可归约图(不再包含节点数不少于两个的区间)。

对于不可归约图,可以采用分裂节点的方式化为可归约图。假设$G^1$最终归约成了一个节点,可以观察到一下有趣的性质:

  1. $G^1$中的每个节点出现在有且仅有一个区间$I^1(h)\in\Phi^1$,而后成为了$G^2$的节点,并且出现在有且仅有一个区间$I^2(h)\in\Phi^2$,以此类推。
  2. 因而对于每个基本块而言,它们有唯一的成员关系链:$b_i\in I^1(h_1)\in I^2(h_2)\in\cdots\in I^n(h_n)$。
  3. 由于区间内的节点使用局部后继函数建立了偏序关系,所以整个图的节点都建立了偏序关系。

这里给出一般的适用于许多分析的框架(其实思路就是自底向上,在自上而下):

过程F:

  1. 处理程序中的每个基本块,收集感兴趣的基本块信息保存至基本块的入口和出口。令$k=1$
  2. 对于每个$k$阶区间:
    1. 按照区间序列处理成员,首先更新成员的状态作为对前导的反应,然后将修改传播至后继
    2. 如果锁节点传播给区间头的信息发生了更新,那就重新上一步
  3. 令$k=k+1$,重做上一步,直到归约成$n$阶图即一个节点
  4. 令$k=n-2$
  5. 将$k+1$阶图的信息关联到$k$阶图的区间头上
  6. 将区间头的信息传递给区间内的每个节点
  7. 令$k=k-1$,重做上两步,直到得到一阶图

总结

本文介绍的区间有很多性质,可以服务于全局分析。区间内节点间的偏序关系提供了一个自然的顺序;对图划分并组成层级的区间可以帮助我们快速地传递信息;图中的支配关系可以用区间挖掘;图中嵌套的强连通分量也可以用区间检测。


  1. Allen, Frances E. “Control flow analysis.” ACM Sigplan Notices 5.7 (1970): 1-19. ↩︎

检测流图的可归约性

2021年4月27日 14:25

这篇文章的主要内容来自于Tarjan的Testing Flow Graph Reducibility1。研究这篇文章的目的是为了得到求解归约序列的算法。依照规约序列分析可以很好的降低分析的复杂度,比如“从CFG直接构建GSA的算法”中的算法。

许多程序优化和分析都涉及到interval分析。而适合这类分析的流图是可归约的。本篇文章使用深度优先搜索和并查集测试流图的可规约性。本算法的复杂度为$O(E\log^* E)$,其中$\log^*x=\min\{i\mid\log^{(i)}x\leq 1\}$。

基础概念

引理 1 如果$ND(v)$是树$T$某节点$v$的子孙个数。如果$T$有$V$个节点,并且通过前序标号为$1$到$V$。那么树上有路径$v\xrightarrow{*}w$,当且仅当$v\leq w<v+ND(v)$。

这个定理给出了在前序遍历完毕后,$O(1)$复杂度判断两节点是否有祖先-子孙关系的方法。

令$(G,s)$为一流图(流图有一特殊的入口节点,且该入口节点可以到达所有节点),$T$是$G$的生成树且以$s$为根,并通过前序标号。$T$被称为深度优先生成树(DFST),如果$G$中不在$T$的边可以分为3个集合:

  1. 对于$G$的边$(v,w)$在$T$中存在路径$w\xrightarrow{*}v$,称为循环边
  2. 对于$G$的边$(v,w)$在$T$中存在路径$v\xrightarrow{*}w$,称为前向边
  3. 对于$G$的边$(v,w)$在$T$中即不存在路径$v\xrightarrow{*}w$也不存在路径$w\xrightarrow{*}v$,且此时$w<v$,称为交叉边

一个DFST之所以这么称呼,是因为它可以通过从$s$出发在$G$上进行深度优先遍历得到。因而可以在$O(V+E)$的时间复杂度里生成DFST、计算每个节点的序号和$ND(v)$、计算出循环边、前向边、交叉边的集合。

流图和可归约性

令$v$和$w\neq s$是流图$(G,s)$中的两个节点。定义一种操作“将$w$合并进$v$”,即删除$w$及其所有边,在不构成自环和重边的情况下,将$w$的边接到$v$上,构成新图$G’$。$G’$同样是流图。

如果$G’$是$G$通过几次合并操作形成的图,那么$G’$的每个节点$v’$都对应$G$中节点的集合。此外$G’$的每个边也会对应$G$的边,但反过来不一定有对应的。考虑下面的变换:

$T_2$:如果$(v,w)$是$w$唯一的入边,且$w\neq s$,将$w$合并进$v$。

一个流图如果是可归约的当且仅当不断使用$T_2$可以将流图转化为只包含$s$的图(这个定义中假定流图不包含自环)。如果$G’$由$G$通过几次$T_2$变换得到,则称$G’$是$G$的归约。一个唯一的图可以通过不断使用$T_2$变换得到,因此变换的顺序并不影响可归约性。

令$T$是流图$(G,s)$的一个DFST。

定理 2 (Hecht & Ullman) 如果$G$是可归约的当且仅当相对于$T$对于每个循环边$(v,w)$,$w$支配$v$。

对于$G$中的任何节点$w$。令$C(w)=\{v\mid (v,w)\text{是循环边}\}$,令$P(w)=\{v\mid\exists z\in C(w)\text{使得存在不经过$w$从$v$到$z$的路径}\}$。如果没有循环边$(v,w)$,那么$C(w)=\varnothing$、$P(w)=\varnothing$。形象地说,$C(w)$是循环头$w$对应的循环尾集合,$P(w)$是循环头$w$除去它本身外对应的循环体集合。对于有多个循环入口的情况下,即循环边终点不支配循环边起点的情况下,$s\in P(w)$。

引理 3 $G$是可归约的当且仅当对于所有的$w$和所有的$v\in P(w)$,$w\xrightarrow{*}v$在$T$中。

证明 “$\Rightarrow$”,反证法,如果存在$v\in P(w)$且$w\xrightarrow{*}v$不再$T$中,即$v$不是$w$的子孙。因而存在不经过$w$的$s$到$v$再到$C(w)$中某节点的一条路径,即$w$不支配$v$,也不支配$C(w)$中某节点,由定理$2$知$G$不可归约。“$\Leftarrow$”,反证法,$G$是不可归约的,由定理$2$,存在一个循环边$(v,w)$,满足$w$不支配$v$。因而存在$s$到$v$的不经过$w$的路径 ,故$s\in P(w)$,但$w\xrightarrow{*} s$不再$T$中。

令$w$是$G$中有循环边作为入边的节点中,编号最大的那个。并且假设对于所有的$v\in P(w)$,$w\xrightarrow{*}v$在$T$中。令$G’$是$G$在将所有$P(w)$中的节点合并进$w$后形成的图。

引理 4 $G’$中每个边$(v’,w’)$都对应于$G$中的某个边$(v,w’)$,且$v’\rightarrow v$在$T$中。

证明 令$(v,w’)$是$G$中的某条边。如果$w’\in P(w)$,那么$v\in P(w)\cup\{w\}$(因为$w’\in P(w)$等价于存在不经过$w$的从$w’$到$C(w)$某节点路径,将$(v,w’)$连街上这条路径,如果$v\neq w$就可以得到不经过$w$的$v$到$C(w)$某节点路径)。如果$v\in P(w)$,那么$w\xrightarrow{*}v$(题设)。因此,有以下情况:

  1. $w’\in P(w)\land(v\in P(w)\lor v=w)$:$(v,w’)$在$G’$中无对应的边;
  2. $v\notin P(w)\land v\neq w$:此时一定有$w’\notin P(w)$,$(v,w’)$在$G’$中对应于$(v,w’)$;
  3. $w’\notin P(w)\land(v\in P(w)\lor v=w)$:此时$v$一定被合进$w$(或者$v$就是$w$),由题设知道有$v’=w\xrightarrow{*}v$,$(v,w’)$在$G’$中对应于$(v’,w’)$。

令$T’$是$G’$的子图,其中的边由那些对应于原DFST $T$的边组成。

引理 5 $T’$,在和$T$有相同的编号下,是$G’$的DFST。$G’$的循环边对应于$G$的循环边,$G’$的前向边对应于$G$的前向边或交叉边,$G’$的交叉边对应于$G$的交叉边。

引理 6 对于任何节点$x<w$,令$P’(x)$和$C’(x)$根据$T’$定义在$G’$上,同时$P(x)$和$C(x)$根据$T$定义在$G$上。如果对于所有$y\in P’(x)$在$T’$中有$x\xrightarrow{*}y$当且仅当对于所有$y\in P(x)$在$T$中有$x\xrightarrow{*}y$

证明 “$\Leftarrow$”,反证法,如果存在$y\in P’(x)$且$T’$中没有$x\xrightarrow{*}y$,即$T’$中$y$不是$x$的子孙。那么同样可以得到在$T$中$y$不是$x$的子孙,需要证明的是$y\in P(x)$。进一步,在$G’$中存在不经过$x$的从$y$到某个点$z’$的路径$p’$,其中$(z’,x)$是$G’$的循环边。由引理5,可以知道$(z’,x)$对应于$G$中的某个循环边$(z,x)$。由于有$P(w)\cup\{w\}$导出的$G$的子图是强连通的,因而在$G$中存在一个不仅过$x$的从$y$到$z$的路径$p$,路径上的边由$p’$对应的边或者$P(w)\cup\{w\}$中节点之间的边组成。因而$y\in P(x)$。

反向的,“$\Rightarrow$”,反证法,如果存在$y\in P(x)$且在$T$中$y$不是$x$的子孙。如果$y\notin P(w)$,那么$y\in P’(x)$且在$T’$中$y$不是$x$的子孙。如果$y\in P(w)$,那么$T’$中$w$不是$x$的子孙,且$w\in P’(x)$。

引理3-6可以导出一个高效地测试图可归约性的算法。令$T$是流图$(G,s)$的一个DFST,并且令$w_1>w_2>\cdots>w_n$是$G$中有入边是循环边的节点。我们计算$P(w_1)$。如果$P(w_1)$中有非$w_1$的子孙节点,我们就停止;否则的话。我们将$P(w_1)$合并进$w_1$组成一个图$G’$,然后计算$G’$中的$P’(w_2)$。如果$P’(w_2)$中有非$w_2$的子孙节点,我们就停止;否则的话。我们将$P‘(w_2)$合并进$w_2$组成一个图$G’’$。不断这样直到我们知道$G$不可归约或者所有的循环边都处理完了,后者意味着$G$可归约。

合并节点从而组成$G’$和$G’’$可以使用并查集。初始的时候,有$V$个单元素集合,每个集合的代表元素都是那唯一的元素。我们定义以下操作:

  • $\text{FIND}(x)$,找到$x$所属集合的代表元;
  • $\text{UNION}(A,B,C)$,合并集合$A$和$B$(摧毁它们),并且给一个新的名字$C$。

下面给出归约算法。除了测试可归约性,这个算法还能给出每个节点首先合并进了哪个$w_i$。这个值被定义为$\text{HIGHPT}(x)$,如果$x$没被合并,那么定义为0。$\text{HIGHPT}(x)$被用于构建一个归约序列。

算法$\text{REDUCE}(G,s)$:

  1. 使用深度优先搜索构建$G$的DFST,节点通过前序遍历标号$1$到$V$,对每个节点$v$计算$ND(v)$
  2. 对于$v=1\dots V$:
    1. 构建进入$v$的循环边、前向边、交叉边
    2. 构建包含$v$的单元素并查集
    3. $\text{HIGHTPT}(v):=0$
  3. 对于$w=V\dots 1$:
    1. $P:=\varnothing$
    2. 对于每个进入$w$的循环边$(v,w)$:
      1. $P:=P\cup\{\text{FIND}(v)\}$
    3. $Q:=P$($Q$是一个待处理的工作队列)
    4. 当$Q\neq\varnothing$时不断循环:
      1. $x:=pop(Q)$
      2. 如果$w>x\lor w+ND(w)\leq x$:
        1. 终止,$G$不可归约
      3. 如果$\text{HIGHPT(x)}=0$:
        1. $\text{HIGHPT(x)}:=w$
      4. 对于每个进入$x$前向边、树边、交叉边$(y,x)$:
        1. $y’:=\text{FIND}(y)$
        2. 如果$y’\notin P$且$y’\neq w$:
          1. $P:=P\cup\{y’\}$
          2. $push(Q,y’)$
    5. 注释:现在$P=P(w)$
    6. 对于每个$x\in P$:
      1. $\text{UNION}(x,w,w)$
  4. $G$可归约

标鲜红色的代码被我从内层循环移了出来。原作者的伪代码似乎会漏给循环尾赋$\text{HIGHPT}$。要查看算法差异可以见页底引用的原论文。

归约一个可归约图

这个算法本身不是构造性的,但我们可以通过$\text{HIGHPT}(v)$构造归约序列。我们给每个$G$上的节点赋予一个数$\text{SNUMBER}$,使得对于树边$(v,w)$,$\text{SNUMBER}(v)<\text{SNUMBER}(w)$;对于交叉边$(v,w)$,$\text{SNUMBER}(v)<\text{SNUMBER}(w)$。这步可以通过深度优先搜索时,先遍历序号大的实现。再运行完算法后,我们就得到了一个二元组$(\text{HIGHPT}(v),\text{SNUMBER}(v))$,而后我们对节点按二元组字典序排序,其中二元组第一个元素降序,第二个元素升序。这个排序可以在$O(V)$的时间内通过两轮基数排序完成。

这里实际上就是对DAG进行了拓扑排序。

流图示例

流图示例,节点标签为$dfs (highpt, snumber)$

引理 7 如果$G$是可归约的,那么我们可以通过归约顺序合并$G$的节点。

证明 通过合并节点的数目进行归纳。假设$v$前面的节点都被合并了,这就创建了一个图$G$的归约$G’$。如果$v$不是根节点,那么$v$有一个树边作为入边。我们要证明的是,除了这条树边,$v$没有其他额外的边,这使得$T_2$变换能够继续进行。

假设$G$包含循环边$(u,v)$,那么所有的$x\in P(v)$已经被合并了。因为从代码中,我们可以知道$\text{HIGHTPT}(x)\geq v$,而另一方面由于$\text{HIGHTPT}(v)<v$(对于所有节点无条件成立)。故$\text{HIGHTPT}(x)>\text{HIGHTPT}(v)$。

假设$G$包含前向边$(u,v)$,那么所有的$u\xrightarrow{*}v$上路径除了$v$的节点$x$不晚于$v$被合并了。因为$\text{HIGHTPT}(x)\geq\text{HIGHTPT}(v)$(如何证明?,感觉上当$\text{HIGHTPT}(v)$被赋值时,所有逆着前向边、树边、交叉边能遍历到且没标上$\text{HIGHTPT}$的节点都会被标上同样的$\text{HIGHTPT}$)且$\text{SNUMBER}(x)\leq\text{SNUMBER}(v)$。

假设$G$包含交叉边$(u,v)$,那么令$w$是$u$和$v$的最近公共祖先。我们要证明$w\xrightarrow{*}u$和$w\xrightarrow{*}v$上路径除了$v$的节点$x$不晚于$v$被合并了。证明思路同前向边,这里用到了$\text{SNUMBER}$对于交叉边的性质。


  1. Tarjan, Robert. “Testing flow graph reducibility.” Proceedings of the fifth annual ACM symposium on Theory of computing. 1973. ↩︎

从CFG直接构建GSA的算法

2021年4月27日 02:14

本文来源于这篇Efficient building and placing of gating functions论文。该论文提供了一种算法,能够直接从CFG(控制流图)构建GSA(Gated单一赋值)形式。而之前的方法需要先插入phi节点即转换成SSA(静态单一赋值)形式,再进行构建。其核心思想是借助了他们提出的gating path这一概念。

内容主要来自这篇1论文。

背景及相关知识

支配

摘自“如何构建SSA形式的CFG”。

  • 支配:$x$支配$y \Leftrightarrow$ 从起始节点到$y$的每条路径都经过了$x$,记为$x\underline{\gg}y$;从定义来说$\forall x, x$支配$x$;这是一个偏序关系(满足自反、传递)。
  • 严格支配:$x$严格支配$y \Leftrightarrow x$支配$y \land x \neq y$,记为$x\gg y$;如果$x$不严格支配$y$,则记为$x\rlap{\hspace{.5em}/}\gg y$。
  • 支配边界:$y \in x$的支配边界$\Leftrightarrow x$支配了$y$的前驱节点,但$d$没有严格支配$y$;从定义来说$x$的支配边界可能包含$x$自己;直观理解支配边界就是支配从有到无的界线。记$DF(X)$为节点$X$的支配边界。$DF$也可以定义在集合$\mathcal{X}$上,$DF(\mathcal{X})=\bigcup_{x\in \mathcal{X}}DF(X)$。 $$DF(X) = {Y|\exists P\in Pred(Y)(X\underline{\gg}P\land X\rlap{\hspace{.6em}|}\gg Y)}$$
  • 立即支配者:$x$是$y$的立即支配者$\Leftrightarrow x$严格支配$y$且$\forall z$严格支配$y$,$x$不严格支配$z$;我们会用idom来表示立即支配者;直观理解$y$的idom就是离$y$最接近的严格支配$y$的节点;一个节点的idom是唯一的。
  • 支配者树:每个节点的立即支配者组成了一棵树(支配的偏序确保是有向无环的,idom的唯一进而确保是棵树)。

注意支配的概念是对于一个有起始节点的有向图的。在CFG中,支配者树的根是Entry。

可归约性与循环

可归约性

首先介绍两种变换,称为“归约”:

  1. T1变换:移除一个节点的自环;
  2. T2变换:对于一个有唯一前继$p$的节点$n$(可能有重边),移除$n$并让其后继成为$p$的后继。

可归约有很多等价的定义,现在给出其中的两种:

  • CFG中的边可以分为两个不重叠的集合:前向边和回边,并满足:
    • 前向边组成了DAG,且都能从入口节点到达;
    • 回边的终止节点支配了起始节点。
  • 反复使用T1和T2变换能将CFG转换为单一节点。

不可归约图主要是存在强连通分量有多个入口的情况。在结构化编程、不使用goto语句的情况下,创造出的CFG都是可归约图。

循环特指那些只有单一入口的强连通分量。在可归约图中识别循环将变得很简单,其切入点是回边检测:那些从被支配节点到支配节点的边就是回边,对应的支配节点是循环头,被支配节点是循环尾。下一小节会有更多关于循环的定义。

可归约图除了在识别循环上有帮助外,还能极大地简化程序分析复杂性。

对于不可归约图,可以通过复制分裂节点,转换成可归约图。

可归约图的逆图不一定是可归约图。

循环

以下是关于循环的一些概念,注意循环通常是可归约图的概念:

  • 循环:CFG上有唯一入口节点(循环头)的强连通子图;
  • 循环入边:起点在循环外,终点在循环内;
  • 循环出边:起点在循环内,终点在循环外;
  • 循环头:循环入边的终点。支配循环内所有节点;
  • 回边:终点是循环头,起点在循环内;
  • 某回边的自然循环:被循环头支配,并能到达该回边的节点集合;
  • 循环尾:回边的起点;
  • 循环出口:循环出边的终点;
  • 嵌套循环:循环头在另一循环内的的循环。

对于两个不同的自然循环,它们可能有3种关系:

  1. 互相分离:没有任何节点共享;
  2. 互相嵌套:一个的循环头严格支配另一个循环头;
  3. 共享循环头:循环头是共享的。

对于第3种情况,可以添加公共的循环尾合并为一个循环。进而循环只剩下两种关系:分离嵌套

SSA(静态单一赋值)形式

通过对CFG进行转化,确保每个变量只有一次定义(即一处赋值),可以极大地简化程序分析,这种转化的结果就是SSA形式。顺序执行的代码只需要给变量添加版本号,就能转化为SSA形式。而在CFG的交汇节点处,如果流入同一变量的不同版本,就需要插入一个选择函数来确保单一赋值。这种函数称为$\phi$函数,形如$x_{n+1}=\phi(x_1,x_2,\dots,x_n)$。它位于CFG节点的起始处(如果有多个变量的话,可能有多个$\phi$函数)。它的参数是那些流入的不同版本。语义上,根据控制流是从哪条边流入,$\phi$函数会返回对应的变量版本。

Cytron2给出了一个高效的转化SSA形式的算法。为了理解这篇论文的理论基础,首先定义支配边界闭包的$DF^+(\mathcal{X})$为下列序列的极限: $$\begin{cases} DF_1=DF(\mathcal{X})\newline DF_{i+1}=DF(\mathcal{X}\cup DF_i) \end{cases}$$ 也就是说$DF^+(\mathcal{X})$是$\mathcal{X}$的支配边界,并上支配边界的支配边界,等等。然后这篇论文给出了最重要的定理:令$\mathcal{X}$为某个变量所有赋值语句出现过的CFG节点集合,$DF^+(\mathcal{X})$是赋值语句交汇的点,也就是最少的需要为该变量插入$\phi$函数的地方。依据这个定理,Cytron给出了两步算法,先是放置$\phi$函数,再重命名变量(给变量加上版本号)。

GSA(Gated单一赋值)形式

虽然SSA形式的CFG更清楚的显示了def-use链,但它仍属于控制流的一种表示。Ottenstein3提出了GSA,它是一种更加易于分析的值流表示。在此工作基础上,Havlak4进一步简化了GSA为TGSA(T是Thinned,意为简化 )。在这篇论文里,他们给出的TGSA构造方法是以SSA结果为输入的。而本文则试图给出一个不依赖于SSA结果的算法。这里给出TGSA向传统SSA添加并用以替代$\phi$函数的3种新gating函数。

$\gamma$函数,含有谓词的合并

V1 := ...
if (P) then
    V2 := ...
endif
V3 := phi(V1, V2)
$$\Rightarrow$$
V1 = ...
if (P) then
    V2 := ...
endif
V3 := gamma(P, V2, V1)
在SSA的基础上,用$\gamma$函数替换$\phi$函数

$\gamma$试图表示条件分支语句的合并,它用于替换除循环头起始处的$\phi$函数。$\gamma$函数有如下的形式$V_3 := \gamma(P,V_1,V_2)$。含义是,如果$P$(谓词输入)为真,$V$的取值为$V_2$否则为$V_1$($V_1$、$V_2$统称为值输入)。注意到,$\phi$函数是依据流入控制流选取多个值,而$\gamma$则是根据条件选取多个值,后者便于值流分析。$\gamma$函数很容易被扩展为多分支用于switch,类似于$\gamma(P,V_1,V_2,\dots,V_n)$。

$\gamma$函数可能嵌套,构成DAG(嵌套表达式在合并公共子表达式后,就构成了DAG)。该合并节点CFG上的立即支配者为DAG的根$\gamma$函数提供谓词输入。而从DAG的根到末端经过的$\gamma$函数的顺序,应当与从合并节点CFG上的立即支配者到合并节点的前向CFG路径(除去循环回边的CFG)经过的分支顺序一致。

某些情况下,若某个分支条件不可能发生,用$\top$表示(译注:这里这个符号很困惑,它明明是底类型$\bot$)。这个记号和后文中$\varnothing$具有相同的意义,只是来源于不同的文章。

Nested gamma CFG

一个嵌套$\gamma$函数,并包含不可能发生条件$\top$的示例

考虑上图中的例子,在$A_3$处,将$\phi$函数替换为$\gamma$函数,结果应该为$\gamma(P,\gamma(Q,A_1,\top),A_2)$。

$\mu$函数,循环合并

$\mu$函数被插入在循环头起始处,并有如下的形式$V’:=\mu(V_{init},V_{iter})$。其中$V_{init}$是从循环外获得的初始输入,$V_{iter}$是从循环内回边获得的迭代输入。如果有多条循环外入边或有多条回边,相应的$V_{init}$和$V_{iter}$可能是一个$\gamma$ DAG。语义上,$\mu$函数产生了一个无穷的序列。而这个序列中的符合条件的第一个元素会被循环出口处的$\eta$函数选取。

一个循环头可能会被若干自然循环共享,即嵌套,或者除循环头外不共享节点。后者可以通过一个post-body节点合并多个回边化为一个自然循环。无论何种情况,$V_{iter}$应该是考虑了所有循环路径的结果。

这里使用了TGSA而不是GSA论文中的定义。

不可归约的CFG可能会有多个循环头。本文假定CFG都是可归约的,许多算法都是建立在这个假设上的。

TODO: 如何处理不可归约图?可能需要参照Tarjan的path sequence。

$\eta$函数,循环值选取

$\eta$函数被插入在循环出口的尾部,用于从$\mu$函数产生出来的序列中,选取符合某一条件的第一个值,其形式为$V’:=\eta(P,V_{final})$。其中$V_{final}$是一个由$\mu$函数产生的序列。而$P$则是断言,如果$P$依赖于循环内的变量,那么它也是序列。语义上,当$P$为真时,$V_{final}$的值被选取并赋值给$V’$。与$P$和$V_{final}$不同$V’$是序列中的一个值。

值得注意的是,与$\gamma$和$\mu$不同,$\eta$不表示合并。因此$\eta$的$P$和$V_{final}$一般不是$\gamma$ DAG。当然,如果从循环头到基本块有多个包含赋值的路径的话,那么$\eta$所处基本块的开始处会有$\gamma$节点。其插入的位置也有所不同。$\gamma$和$\mu$与$\phi$类似,都位于基本块的开头,而$\eta$插入在基本块的尾部。

此外,即使是在可归约图中,一个循环也可能存在多个循环出口。循环出口可能与循环头是同一个基本块(while),也有可能不同(do-while)。

A = 0;
do {
  if (P)
    A = A + 1;
  else
    A = A + 2;
} while (Q);
write(A);
$$\Rightarrow$$

eta GSA example

一个循环头与出口不位于同一基本块的循环插入$\mu$和$\eta$函数

讨论: 如何构建$\eta$函数?

以下内容是个人不成熟的想法,仅供参考。

上述的描述与论文中一笔带过的$\eta$函数有较大的差别。论文给出的算法无法处理循环出口与循环头不是同一个基本块的情况。论文中的$\eta$函数被放置在了循环头。如何构建$\eta$函数还需要进一步讨论。但进过一些思考,放置在循环出口更加合理。现在问题的难点在于:

  1. 循环出口:快速地从归约图和/或支配着树中找到循环出口,思路是识别出回边之后,反向遍历直到遇到循环头收集节点。而后找到这些节点集合不是到达本身集合中的出边。
  2. 重命名:论文并没有给出重命名这步的细节。重命名总是假设使用的变量来自最近一条该变量的定义语句。在循环出口末插入$\eta$节点会影响循环体内变量的重命名。解决方案是添加post-exit基本块在循环体出口和该出口的循环出边之间,并在其中放置$\eta$节点。
  3. 嵌套循环:一个节点可能是多个嵌套自然循环的出口,这时候我们可以插入多个包含$\eta$的基本块。这几个基本块串行。这种设计具有一致性,比如每个$\eta$都有唯一的$\mu$对应;每从$\mu$的$V_{init}$进入循环就$+1$,经过$\eta$就$-1$,就能记述循环深度。

最后,举个例子,$P\rightarrow{Clause_1,\dots,Clause_n}$表示$P$满足分支条件的析取;而$\gamma$函数采用了扩展表示,$\gamma(P,A_1,A_2,A_{default})$,表示$P$满足对应分支条件后,返回对应的值。

A = 0;
l1: A = A + 1;
l2: A = A + 2;
switch (P) {
    case 1:
      goto l1;
    case 2:
      goto l2;
    default:
      // pass through
}
write(A);
$$\Rightarrow$$

eta CFG example2

$$\Rightarrow$$

eta GSA CFG example2

一个包含`switch`和我所提出的$\eta$函数的例子。

算法思路

计算$\gamma$和$\mu$算法可以分为两部分,首先先放置$\gamma$,$\mu$函数并构造表达式,其中的变量没有标上版本号。之后再使用与SSA一样的重命名算法,给所有使用和被使用处的变量标上版本号。第2步算法在论文中并没有被提及,但可以参照Cytron2的论文。

$\gamma$和$\mu$就是原来$\phi$函数的变种,因而它们可以使用Cytron关于SSA的论断,即所有的$DF^+(\mathcal{X})$就是需要插入的位置($\mathcal{X}$为所有赋值语句的基本块)。但论文中并没有采取这个方法,他们找到了一种等价于$DF^+$的计算方法。相比于Cytron先计算$DF$,在用working list计算出$DF^+$的方法,这篇论文的方法更为直接。我们将在这一章讲解这篇论文提出的方法的理论基础。

但是$\gamma$和$\mu$表达式的内容就比较复杂了。它需要收集从某一个节点的支配者出发,到该节点所有路径组成的$\gamma$ DAG。论文采用了Tarjan5提出的用于解决图路径问题的通用算法“路径表达式”,我们将在这一节给出这个通用方案,以及这个方案是如何被运用到可归约图上的。

至于$\eta$函数,目前还需要探索。

路径表达式

核心思想是:使用正则表达式来表达一组路径具有同一起点和终点的路径,即路径表达式。路径表达式通过从最基本的元素(不可达、空路径和一个边)外加$\cup$(合并)、$\cdot$(拼接)和$*$(重复)构造出复杂的路径表达式,从而能表示一组复杂的路径。对于实际问题而言,通过赋予路径表达式不同的含义,并重新定义合并、拼接和重复运算,就能有通用的解法。如对于最短路问题,$x\cup y$相当于路径$\min\{x, y\}$,$x\cdot y$相当于$x + y$,$x^*$相当于$\begin{cases}0,&x\geq 0\newline-\infty,&x<0\end{cases}$。因而,绝大多数能划归为图论的问题,如最短路,线性方程组求解和控制流分析都能用路径表达式求解。本文所关注的$\gamma$和$\mu$函数参数的$\gamma$ DAG求解问题也能用这个通用的方案求解。问题的难点就在于如何快速、准确地构造出路径表达式。

路径表达式问题主要有两类:

  1. 单源路径表达式问题:求解从一个节点出发到其他所有节点的路径表达式;
  2. 任意两点路径表达式问题:求解任意节点到任意节点的路径表达式。

在接下来的文章中,我们主要关注可归约图的单源路径表达式问题。相比接下来所述的Tarjan的论文中给出了更多有趣的算法。他提出了路径序列作为快速计算路径表达式的方法,并给出了计算一般图、强连通分量分解图(特例DAG)、可归约图的路径序列方案。这些算法我还没来得及仔细看。下文只是一些相对简单,不涉及路径序列的概念和算法。

正则表达式

字母表$\Sigma$是一个既不包含$\Lambda$也不包含$\varnothing$的集合。$\Sigma$上的正则表达式是由以下规则组成的语言:

  1. “$\Lambda$"(空串)和”$\varnothing$"(空集合)以及对任意的$a\in\Sigma$,"$a$“都是原子正则表达式;
  2. 如果$R_1$和$R_2$是正则表达式,$(R_1\cup R_2)$(并)、$(R_1\cdot R_2)$(连接)以及$(R_1)^*$(重复)都是复合正则表达式。

我们使用$\sigma(R)$表示$R$对应的语言。具体计算规则可以递归定义,这里不再给出。

  • 如果$\sigma(R_1)=\sigma(R_2)$,则正则表达式$R_1$和$R_2$被称为等价的;
  • 如果$R=\varnothing$或者$R$不包含$\varnothing$,则正则表达式为简单的;

任何正则表达式都可以转化为简单的。可以重复使用以下的规则:

  1. 替换子表达式$\varnothing\cdot R_1$和$R_1\cdot\varnothing$为$\varnothing$;
  2. 替换子表达式$\varnothing\cup R_1$和$R_1\cup\varnothing$为$R_1$;
  3. 替换子表达式$\varnothing^*$为$\Lambda$。

如果正则表达式$R$能唯一地表示$\sigma(R)$中的每个字符串,则称$R$是不冗余的。也可以准确地递归定义不冗余,这里不再给出。

路径表达式(续)

令$G=(V,E)$为有向图。其中$G$上的任何路径都可以被认为是$E$上的字符串。一个类型为$(v,w)$的路径表达式$P$是$E$上的一个简单正则表达式,其中$\sigma(P)$中的所有路径都是从$v$到$w$的。

路径表达式$P$的类型也可以通过递归定义完成。这里注意到:

  • $\cup$:要求左右子表达式有相同的类型;
  • $\cdot$:要求左表达式的类型终点与右表达式的类型起点一样;
  • $*$:要求子表达式类型终点起点一样。

路径表达式有什么用? 你可能会发现,路径表达式的存储也需要用到树状的结构。在路径表达式上计算最短路等问题并没有降低复杂度,所以路径表达式有什么用?

其实,如果我们找到计算路径表达式的方法,再重新定义原子表达式和复合运算符,就能完成通用的图论问题求解算法。具体例子见本节首。

可归约控制流图的路径表达式计算

回顾可归约图的一种定义:通过下面两种归约操作能转化为单一节点:

  1. T1:移除自环;
  2. T2:单一前继的节点合并进前继。

随着归约的进行,归约图上的节点会代表原图的一个子图,称为区域。归约图的边是原图的边,归约图的区域是原图节点的划分。对于每个区域,都有唯一的,它是原图上所有进入区域的边的终点。你也可以认为头就是没有被合并进其他节点里的节点。

对图中的节点进行排序,构建一个归约序列$v_1,v_2,\dots,v_n$。使得依据这个序列可以通过下面的算法归约成单一节点:

  1. 对于$i=1\dots n-1$
    1. 对$v_i$来回使用T1变换,去除自环;
    2. 使用T2变换将$v_i$合并进$v_j,j>i$。

给出下面定义,其中$r$是可归约图的入口:

  • $header(v_i),v_i\neq r$:步骤1.2中$header(v_i)=v_j$,此外可以定义$\begin{cases}header^0(v)=v\newline header^1(v)=header(v)\newline header^i(v)=(header\circ header^{i-1})(v)\end{cases}$;
  • $cycle(v_i),v_i\neq r$:步骤1.1中$v_i$消去的自环;
  • $noncycle(v_i),v_i\neq r$:步骤1.2中删除的边。

有以下引理:

  1. 如果$v\neq r$,那么$header(v)>v$;
  2. 要么$h(e)=header(t(e))$(前向边),要么$h(e)\leq t(e)$(回边或自环),这里$h(e)$是边$e$的起始,$t(e)$是边$e$的终点;
  3. 如果$e\in cycle(t(e))$,那么存在$i\geq 0$满足$header^i(h(e))=t(e)$;
  4. 如果$e\in noncycle(t(e))$,那么对任意$i\geq 0$满足$header^i(h(e))\neq t(e)$,但存在$i\geq 0$满足$header^i(h(e))=header(t(e))$。

注意到可归约图的节点依据偏序关系最终形成了一棵树(一个节点只有一个$header$)。而支配者树也是一颗树。这两种树之间有怎么样的关联和差异?

暂时没有看到相关文献。但个人认为:

  1. 归约树不一定是支配者树。
  2. 可归约图的支配者树一定是一种归约树。如果想要将支配者树转换成排序好的序列,需要树上节点的直接孩子进行排序,方法是在原图上去除回边后对区域内节点进行拓扑排序。
  3. 不可归约图没有归约树(只有森林),但一定有支配者树。

其中第2点是后面算法的基础之一。

接下来,我们介绍可归约图构建单源路径表达式的方法。算法的输入是依据归约关系排序好的节点、每个节点的$header$、$cycle$和$noncycle$。

这个算法一边计算路径表达式,一边归约图。为了表示归约图,算法使用了一个森林,森林中每个节点$v$的父亲是$header(v)$。这样森林的每一个树都代表了区域,而区域的头则是树的根。森林中每个节点$v$都关联了一个不冗余的路径表达式$R(v)$,代表从$header(v)$到$v$的路径表达式。

算法通过以下四个函数操作树:

函数 描述
$INITIALIZE(v)$ 将$v$组成单一节点的一颗树,并另$R(v):=\Lambda$
$UPDATE(v,R)$ 如果$v$是根,那么$R(v):=R$
$LINK(v,w)$ 如果$v$和$w$是根,那么通过将$w$的父亲设为$v$合并树
$EVAL(v)$ 假设从$v$所属树的根$r$到$v$的树上路径为$r=v_0\rightarrow v_1\rightarrow\cdots\rightarrow v_k=v$,返回$R(v_0)\cdot R(v_1)\cdot\ldots\cdot R(v_k)$

算法如下:

  1. 对于所有的节点$v$
    1. $INITIALIZE(v)$
  2. 对于$v:=1\dots n-1$:
    1. $P:=\varnothing$;$Q:=\varnothing$
    2. 对于$e\in noncycle(v)$:
      1. $P:=[P\cup [EVAL(h(e))\cdot e]]$
    3. 对于$e\in cycle(v)$:
      1. $Q:=[Q\cup [EVAL(h(e))\cdot e]]$
    4. $UPDATE(v,[P\cdot[Q^*]])$
    5. $LINK(header(v),v)$
  3. $P(r,r):=\varnothing$*
  4. 对于$e\in cycle(r)$:
    1. $P(r,r):=[P(r,r)\cup[EVAL(h(e))\cdot e]]$
  5. $P(r,r):=[P(r,r)^*]$
  6. 对于$v:=1\dots n-1$
    1. $P(r,v):=[P(r,r)\cdot EVAL(v)]$

算法完成后,$P$就存放了从$r$到所有点的路径表达式。这里$[~\cdot~]$表示化简。

Gating Path

符号表

符号 含义 备注
$d\xrightarrow{+}v$ 从$d$到$v$的至少包含一条边的路径 可以是自环
$d\xrightarrow{*}v$ 从$d$到$v$的可空的路径 可以$d$就是$v$,路径无边
$d\rightarrow v$ 从$d$到$v$的有且只有一条边的路径  

Gating Path的定义

定义 1 CFG中的节点$v$的gating path被定义为,从$idom(v)$到$v$的一条CFG路径,且该路径上的每个节点都被$idom(v)$支配。

gating path CFG

用于演示gating path的CFG图

gating path dominator tree

用于演示gating path的支配者树
gating path的示例,展示了某些节点的gating path
节点 gating path
$b$ $a\rightarrow b$
$c$ $a\rightarrow c$
$d$ $a\rightarrow b\rightarrow d,~~a\rightarrow c\rightarrow d$
$e$ $d\rightarrow e$

Gating Path的存在性?存在

引理 1 对于任何CFG的路径$d\xrightarrow{+}v$,如果$d\gg v$且$d$在路径中出现了一次,那么$d$支配路径上的所有节点。

上述表述也就是路径除了起始节点,路径没有经过$d$。

引理 1 证明 反证法。如果路径上存在一个非$d$的节点$u$,满足$d\rlap{\hspace{.5em}/}\gg u$,那么路径$\text{Entry}\xrightarrow{*}u\xrightarrow{*}v$就没经过$d$,$v$不被$d$支配,矛盾。

推论 1 对任何节点$v$都存在gating path。

推论 1 证明 永远可以找到$idom(v)\xrightarrow{+}v$,移除这条路径上所有$idom(v)\xrightarrow{*}idom(v)$的环,就得到了符合引理1的路径。

支配边界闭包与支配树的兄弟子树的关系

接下来引理2和引理3将要论证:如果$v\in DF^+(X)$,那么$idom(v)\gg X$。从支配树的角度来说,$X$为$v$的兄弟子树上的某一个节点。

lemma 2&amp;3 CFG

引理2和3演示用的CFG图

lemma 2&amp;3 dominator tree

引理2和3演示用的支配者树
用于演示引理2和引理3的示例
节点 支配者树推断的可能支配闭包 实际支配闭包
2 7,exit 7,exit
3 7,exit 7,exit
4 5,6,7,exit 6,7,exit
6 4,5,7,exit 7,exit

注:这个论断可以用于寻找支配闭包包含$v$的那些节点$X$,也能寻找$X$的支配闭包可能包含的节点$v$。

接下来证明这个论断:

引理 2 如果$v\in DF(X)$,那么$idom(v)\gg X$。

引理 2 证明 反证法。假设$idom(v)\rlap{\hspace{.5em}/}\gg X$(不严格支配),由于$idom(v)$不是$X$,所以$idom(v)$不支配$X$。故存在路径$Entry\xrightarrow{+}X$避开了$idom(v)$。由于$v\in DF(X)$,所以存在$w\in Pred(v)$,使得$X\underline{\gg} w$。取路径$X\xrightarrow{*}w\rightarrow v$,移除路径中$X\xrightarrow{*}X$的环(使得$X$只出现在该路径的头)。此时由引理1,$X$支配$X\xrightarrow{*}v$上的所有节点,故$idom(X)$不在这条路径中(否则$X$将支配$idom(v)$和$v$)。将这条路径与$Entry\xrightarrow{+}X$,就得到了一条从$Entry$到$v$的避免$idom(v)$的路径,这与题设矛盾。

引理 3 如果$v\in DF^+(X)$,那么$idom(v)\gg X$。

引理 3 证明 数学归纳法。(初始情况)对于$DF^1(X)$,有引理2成立。(归纳)如果$v\in DF^{i-1}(X)$,那么$idom(v)\gg X$。任取$v\in DF(u),u\in DF^{i-1}(X)$。由归纳假设知$idom(u)\gg X$;由引理1,$idom(v)\gg u$,即$idom(v)\underline{\gg}idom(u)$。由传递性得$idom(v)\gg X$。

Gating Path与支配边界闭包的关系

首先,引理4和5论证支配边界(闭包)关系中可以得到一条特殊的gating path。

引理 4 如果$v\in DF(X)$,那么存在从$idom(v)$经过$X$到$v$的gating path。

引理 4 证明 由$DF$定义知道存在一个$w\in Pred(v)$,满足$X\underline{\gg}w$。又由推论1知,可以找到由gating path拼接的路径$X\xrightarrow{*}w$,满足路径上的每个节点都被$X$控制。由引理2知道$idom(v)\gg X$,类似地,又由推论1知,可以找到由gating path拼接的路径$idom(v)\gg X$,满足路径上的每个节点都被$idom(v)$控制。将这两条路径拼接成$idom(v)\xrightarrow{+}X\xrightarrow{*}w\rightarrow v$,注意到路径上的每个节点都被$idom(v)$控制,所以这是$v$的gating path。

引理 5 如果$v\in DF^+(X)$,那么存在从$idom(v)$经过$X$到$v$的gating path。

引理 5 证明 数学归纳法。

首先,引理6反过来,论证从一条特殊的gating path,可以得到支配边界闭包关系。

引理 6 如果存在一个$idom(v)$经过$X$到$v$的gating path,且$idom(v)\neq X$,那么$v\in DF^+(X)$。

$v$ $idom(v)$ $X$
6 3 4,5
7 1 2,3,4,5,6(注意,7不是4、5的直接支配边界,而是闭包)

引理 6 证明 依据gating path的子路径$X\xrightarrow{*}w\rightarrow v$上的合并节点(入边数目大于1)个数进行数学归纳法。$v$一定是个合并节点,否则$w$将成为$idom(v)$且由题设$idom(v)\neq X$知$idom(v)\neq w$矛盾。令$X\xrightarrow{+}v$上合并节点的个数为$n$。

  1. 如果$n=1$,那么$v$是唯一的合并节点,路径$X\xrightarrow{*}w\rightarrow v$上的每个中间节点只有一个前导,故$X\underline{\gg}w$,$v\in DF(X)$。
  2. 假设命题对于$n<i$成立,当$n=i$时,令$u$是$X\xrightarrow{*}w\rightarrow v$上倒数第2个合并节点,令$P_u$为$idom(u)\xrightarrow{+}u$是该gating path的一个子路径(译注:由于$idom(v)$支配$u$,故$idom(u)$也在该gating path上,这里$P_u$应该是移除了环的路径,因而是gating path)。如果$X$在$P_u$中且$X\neq idom(u)$,那么由归纳假设,$u\in DF^{k<i}(X)$;同时,由于$v\in DF(u)$,故$v\in DF^{k+1}(X)$。如果$X=idom(u)$或者$X$不在$P_u$上,那么$X\underline{\gg}idom(u)\gg u\underline{\gg} w$(这步证明存疑,$X$似乎不一定支配$idom(u)$),因而$v\in DF(X)$。

使用引理5和6,我们得到了下面的定理:

定理 1 给定初始的CFG节点集合$\mathcal{X}$,对于CFG上的任意节点$v$,$v\in DF^+(\mathcal{X})$当且仅当存在一个gating path满足$idom(v)\xrightarrow{+}X\xrightarrow{+}v,X\in\mathcal{X}$。

这个证明就是将引理5和6整合了,并且将$DF^+$应用到了集合上。

引理6红线部分证明的瑕疵

lemma 6 problem CFG

用于演示引理6证明瑕疵的CFG

lemma 6 problem dominator tree

用于演示引理6证明瑕疵的支配者树
用于演示引理6证明瑕疵的示例

红色路径为gating path,此时$n=3$,且$X$不位于$P_u$上。

GSA构建算法

用Gating函数代表路径表达式

我们使用路径表达式来表达两节点之间路径集合,最终目的是找到立即支配者到合并节点的路径集合,后者就是要插入$\gamma$和$\mu$的地方。重新定义路径表达式的原子表达式和运算规则,使之运算的结果就是表示路径成立的$\gamma$函数。这样路径表达式计算完毕,就自然得到了$\gamma$函数。

原子路径表达式

首先,我们使用$\Lambda$表示路径可达,$\varnothing$表示路径不可达。

然后,我们考虑对于一条边,它的路径表达式:

  1. 如果是if (B)then分支出边,该边的路径表达式为:$\gamma(B,\Lambda,\varnothing)$;
  2. 如果是if (B)else分支出边,该边的路径表达式为:$\gamma(B,\varnothing,\Lambda)$;
  3. 如果是唯一出边,该边的路径表达式为:$\Lambda$;

这里,$\gamma(B,\Lambda,\varnothing)$可以被理解为,当$B$为真时,路径可达;当$B$为假时,路径不可达。else分支类似理解。更多分支可以通过定义$\gamma(B,e_1,e_2,\dots,e_n)$来表示,其中$n$是分支数。

复合路径表达式

接下来,我们就需要定义路径表达式的$\cup$,$~\cdot~$运算。$*$运算不定义,因为之后用不到,但其实它也无法定义,这是被$\gamma$函数无法表达循环这件事本身所限制住的(主要是因为$B$可能会变)。

并集

对于路径表达式$R_1$和$R_2$,定义它们的并:

$$R_1\cup R_2:=\begin{cases} R_2, &\text{if}~R_1=\varnothing \newline R_1, &\text{if}~R_2=\varnothing \newline \gamma(B,(R_{1_t}\cup R_{2_t}),(R_{1_f}\cup R_{2_f})), &\text{if}~\begin{aligned}R_1=\gamma(B,R_{1_t},R_{1_f}) \newline R_2=\gamma(B,R_{2_t},R_{2_f})\end{aligned} \newline \end{cases}$$

前两个条件很容易理解,如果两个路径集合取并集,其中一个是不可达,留下另一个就可以了。关于最后一个情况,有三个疑问。

  1. 最后一条情况一定被满足么?是的,可以归纳证明类型相同的路径表达式,如果包含$\gamma$,其条件一定是相同的。
  2. 语义上如何理解?$B$为真的时候,两种情况中真的路径求并就可以了;else分支类似。
  3. 类型一致么?是的,可以归纳证明$R_1$、$R_{1_t}$、$R_{1_f}$以及$R_2$等6个路径表达式是同一类型,所以子表达式中的$\cup$没问题。
拼接

对于路径表达式$R_1$和$R_2$,定义它们的拼接:

$$R_1\cdot R_2:=\begin{cases} \varnothing, &\text{if}~R_1=\varnothing~\text{or}~R_2=\varnothing \newline R_2, &\text{if}~R_1=\Lambda \newline R_1, &\text{if}~R_2=\Lambda \newline \gamma(B,(R_{1_t}\cdot R_2),(R_{1_f}\cdot R_2)), &\text{if}~R_1=\gamma(B,R_{1_t},R_{1_f}) \newline \end{cases}$$

这里就讲解语义上的理解:前三条很直白,最后一条也就是$R_2$分配到thenelse分支。

从拼接的构造过程,我们就能得到$\gamma$函数,含有谓词的合并一节中的结论:(不考虑循环回边)在合并节点处的路径表达式的根$\gamma$函数的谓词输入就是合并节点的立即支配者的条件;其值输入则是(如果有)嵌套的$\gamma$函数,从外到里则与立即支配者到合并节点的路径对应。

需要注意到的是,反复运用合并和拼接后,路径表达式只有嵌套的$\gamma$、$\Lambda$和$\varnothing$组成(不包含$~\cdot~$和$\cup$)。

例子
1
2
3
4
5
if (P) then
    A := 1
else
    A := 2
endif

这里,我们把endif视作一个基本块,并用行号来表示CFG节点。我们的目标是求出立即支配者1(if)到被支配者5(endif)的路径表达式。

首先给出原子路径表达式:

原子路径表达式
$1\rightarrow 2$ $\gamma(P,\Lambda,\varnothing)$
$1\rightarrow 4$ $\gamma(P,\varnothing,\Lambda)$
$2\rightarrow 5$ $\Lambda$
$4\rightarrow 5$ $\Lambda$

再给出复合路径表达式:

路径 路径表达式
$1\rightarrow 2\rightarrow 5$ $\gamma(P,\Lambda,\varnothing)\cdot\Lambda=\gamma(P,\Lambda,\varnothing)$
$1\rightarrow 4\rightarrow 5$ $\gamma(P,\varnothing,\Lambda)\cdot\Lambda=\gamma(P,\varnothing,\Lambda)$
$\bigcup 1\xrightarrow{*}5$ $\gamma(P,\Lambda,\varnothing)\cup\gamma(P,\varnothing,\Lambda)=\gamma(P,\Lambda,\Lambda)$

那么对于复杂的可归约图,求解路径表达式就需要按照一个顺序。其计算方法就应当参见先前说的Tarjan的算法

有些人就有疑问了,对于绝大多数情况,路径表达式的值输入都是$\Lambda$,没有什么意义。其实,这里还缺最后一步,就是在合并节点处,依据流入边的顺序对$\Lambda$进行标号。这一步有点类似$\phi$函数的标号,方便之后重命名标上版本号(注意标号与版本号的区别)。

为什么给$\Lambda$标号?因为在消除死代码后,合并节点的每个$\Lambda$都代表着一种可能流入的值(假定entry包含对所有变量的默认初始化)。

标号

标号是很简单的操作。在合并节点求路径表达式时,会把所有流入的路径取个并。在取并之前,依据流入路径的顺序给$\Lambda$标号即可。

例如上例中,计算$\bigcup 1\xrightarrow{*}5$时,会合并两个路径,给它们标上号:

  1. $*\xrightarrow{*}2\rightarrow 5$:$\gamma(P,\Lambda^1,\varnothing)$;
  2. $*\xrightarrow{*}4\rightarrow 5$:$\gamma(P,\varnothing,\Lambda^2)$;

合并之后,就有最终的计算结果:$\gamma(P,\Lambda^1,\Lambda^2)$。经过重命名的步骤后,就能得到想要的gating函数了。再次强调这里的上标不是数据流上的版本号,而是控制流的入边,切勿搞混。

有时候,类似$\gamma(P,\Lambda,\Lambda)$并没有出现在我们感兴趣的合并节点上,这时候可直接改为$\Lambda$。对于不存在死循环的CFG,另合并节点为$u$,一般发生在$u=idom_{post}(idom_{pre}(u))$。这里通过下标区别前向立即支配者和反向立即支配者。

算法

这个算法输出以下3个数据结构:

  • $\Phi::Set\langle CFGNode\rangle$:需要放置$\gamma$或$\mu$函数的CFG节点;
  • $GP::Map\langle CFGNode,PathExpression\rangle$:从立即支配者到该节点的路径表达式(不考虑循环,即所有gating path);
  • $G^*::Map\langle CFGNode,PathExpression\rangle$:对于循环头,从该节点出发沿循环体回到该节点的路径表达式(如果有共享循环头的多个自然循环,这些自然循环全都会被考虑);其他情况为$\varnothing$。

算法的输出是:对任何$v\in\Phi$,如果$G^*[v]=\varnothing$,那么就在$v$处插入$\gamma$函数,其值即为$GP[v]$;否则插入$\mu$函数,其值为$\mu(GP[v],G^*[v])$。

算法还会用到临时变量:

  • $ListP::Array\langle(e = (w,v)::CFGEdge,p::PathExpression)\rangle$:数组的元素是二元组,其中$e$是边,以$w$为起点,$v$为终点。我们用$subroot(w)$代表一个CFG节点,在支配树上它即是$w$的祖先,又是$v$本身或$v$的兄弟节点。$p$是路径$subroot(w)\xrightarrow{*}w\rightarrow v$的路径表达式。之所以在这里引入一个临时数组,是为了分两次遍历,以确保遍历的顺序。

接下来,我给出算法的伪代码,算法的输入是包含某变量赋值节点的集合$\mathcal{X}::Set\langle CFGNode\rangle$:

  1. 初始化:对每个$v\in N$($N$是CFG节点的集合):
    1. $\Phi[v]\leftarrow false$
    2. $GP[v]\leftarrow\varnothing$
    3. $G^*[v]\leftarrow\varnothing$
  2. 对每个$u\in N$,以支配者树后序遍历(前序遍历的逆也行)的顺序遍历:
    1. $ListP = [~]$
    2. 对于$v\in children(u)$:
      1. 对于每个$e=(w,v)\in E$($E$是CFG边的集合)
        1. 如果$w=u$,那么:
          1. $GP[v]\leftarrow GP[v]\cup(e)$
        2. 否则:
          1. $(\phi,p)\leftarrow EVAL(e)$
          2. 如果$\phi$为真,$\Phi\leftarrow\Phi\cup\{v\}$
          3. $ListP\leftarrow[\dots ListP,(e,,p)]$
    3. 对$children(u)$拓扑排序
    4. 对于$v\in children(u)$,以拓扑顺序遍历:
      1. 对于每个$(e=(w,v),p)\in ListP$:
        1. 如果$subroot(w)=v$:
          1. $G^*[v]\leftarrow G^*[v]\cup p$
        2. 否则:
          1. $GP[v]\leftarrow GP[v]\cup (GP[subroot(w)]\cdot p)$
          2. 如果$subroot(w)\in\Phi$为真,$\Phi\leftarrow\Phi\cup\{v\}$
      2. $UPDATE(v,GP[v])$

红色的部分原论文似乎是错放到了内层循环中,这里已经更改。

接下来我们给出这里用到的3个函数,注意$EVAL()$的含义是有变化的。$UPDATE()$函数额外包含了一个简化的过程。由于支配者树是一种特殊的归约树,我们不必引入$LINK()$。

函数 描述
$EVAL(e)$ 令$e=(w,b)$,假设从$subroot(w)$到$v$的树上路径为$r=w_0=subroot(w)\rightarrow w_1\rightarrow\cdots\rightarrow w_k=w$,返回值的$p$为$(R(r)\cdot R(w_1)\cdot\ldots\cdot R(w)\cdot e)$,返回值的$\phi$在$\vee_{i=0}^k(w_i\in\Phi\lor w_i\in\mathcal{X})$时为真,否则为假
$UPDATE(v,R)$ $R(v):=R$,这里$R$中$\gamma$函数的值输入全部为$\Lambda$时,$\gamma$函数会被替换成$\Lambda$,因为之后的标号将给值输入同样的标号,没必要使用$\gamma$函数

算法解释

以后序遍历或前序遍历的逆的顺序遍历支配者树,可以确保孩子在父亲节点遍历之前被遍历到。对于$e=(w,v)\in E$,可以分为以下几种情况。

  1. $e$来自$v$的立即支配者(即$w=u=idom(v)$),那么这条边就是$v$的gating path,将其直接存入$GP[v]$;
  2. 其他情况下一定会有$u\gg w$,也就是$w$在$u$支配子树中处在非根的位置,这时有两种情况:
    1. $e$来自$v$支配树上的兄弟节点的子树($subroot(w)\neq v$),即$e\in cycle(v)$。此时路径$u\xrightarrow{+}subroot(w)\xrightarrow{*} w\rightarrow v$是$v$的gating path,应当被并到$GP[v]$中。
    2. $e$来自$v$支配子树($subroot(w)=v$),即$e\in cycle(v)$。此时路径$v=subroot(w)\xrightarrow{*} w\rightarrow v$是循环,应当被并到$G^*[v]$中。

注意到2.1情形,$u\xrightarrow{+}subroot(w)$这个子路径需要引用到正在计算中的其他$GP[v],v\in children(u)$。所以这就需要引入拓扑排序。而$subroot(w)\xrightarrow{*} w\rightarrow v$部分的路径则是使用Tarjan的算法由$EVAL()$给出的。

拓扑排序细节

拓扑排序是在以$children(u)$为节点,以这些节点对应的子图之间的边为边的图上进行的。解释一下这样做的原因。在把所有的$v\in children(u)$对应的子图归约成一个点后,可能存在3类边:

  1. $v\rightarrow u$这就是未来的$cycle(u)$,这种边是不会影响当前处理的先后顺序的
  2. $v$离开$u$控制区域的边,未来某些节点的$noncycle(\dots)$。同样这种边是不会影响顺序的
  3. $v$到其他$children(u)$子图的边,这类边的前驱需要先算其$GP$,而后继计算的时候就需要引用前驱的$GP$,这类边决定了运算的顺序。

这个拓扑排序的顺序,其实就是前面的归约序列顺序。

标号细节

其实所有$GP[v]\leftarrow GP[v]\cup(\dots)$的地方,就需要对$\dots$进行标号,也就是在算法2.2.1.1.1和2.4.1.2.2都需要标号。

算法的拆解

这个算法其实是可以被拆解的成3部分:

  1. 归约序列的计算:这部分采用了在支配者树上进行拓扑排序的算法来做的。这部分可以被替换。
  2. 路径表达式的计算:计算$GP$和$G^*$,这两个都是不依赖于输入$\mathcal{X}$的,是图的内在性质,因而对于多个变量,这部分是不需要重复计算的。
  3. $\gamma$和$\mu$插入位置的计算:这部分是原论文gating path性质的实践,可以在计算路径表达式的同时计算出来。实际上这部分算法可以被替换成Cytron的算法。对于多个变量,这部分是需要重复计算的,之后的重命名算法也需要重复计算。

完整的例子

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
read(A)
if (P) then goto 5
if (Q) then
    A := 5
    while (R) do
        A := A + 1
    enddo
else
    if (T) then
        A := A * 3
    else
        A := A + 6
    endif
endif
write(A)

example CFG

用于演示的CFG

example dominator tree

用于演示的支配者树,那些在CFG中有但支配者树没的边,用虚线添加了进来
算法的完整示例

loop: $u=10$

derive:$v$ edge:$(w,v)$ 影响
$11$ $(10,11)$ $GP(11)=\gamma(T,\Lambda,\varnothing)$
$12$ $(10,12)$ $GP(12)=\gamma(T,\varnothing,\Lambda)$
$13$ $(11,13)$ $subroot(w)=11,~~p(subroot(w),v)=\Lambda^1,~~\phi=\texttt{true},~~\Phi(13)=\texttt{true},~~ListP(13)={(11,13,\Lambda^1)}$
^ $(12,13)$ $subroot(w)=12,~~p(subroot(w),v)=\Lambda^2,~~\phi=\texttt{true},~~\Phi(13)=\texttt{true},~~ListP(13)={(11,13,\Lambda^1),(12,13,\Lambda^2)}$

sequence: $11\rightarrow 13,12\rightarrow 13\Rightarrow11,12,13$

merge:$v$ $subroot(w),v,p(subroot(w),v)$ 影响
$13$ $11,13,\Lambda^1$ $GP(13)=\gamma(T,\Lambda^1,\varnothing)$
^ $12,13,\Lambda^2$ $GP(13)=\gamma(T,\Lambda^1,\Lambda^2)$

此时树的样子为:

interval tree 1

$u=10$时构建的树。

loop: $u=8$

derive:$v$ edge:$(w,v)$ 影响
$9$ $(8,9)$ $GP(9)=\gamma(Q,\Lambda,\varnothing)$
$10$ $(8,10)$ $GP(10)=\gamma(Q,\varnothing,\Lambda)$

interval tree 2

$u=8$时构建的树。

loop: $u=6$

derive:$v$ edge:$(w,v)$ 影响
$7$ $(6,7)$ $GP(7)=\Lambda$

interval tree 3

$u=6$时构建的树。

loop: $u=4$

derive:$v$ edge:$(w,v)$ 影响
$5$ $(4,5)$ $GP(5)=\Lambda$

interval tree 4

$u=4$时构建的树。

loop: $u=3$

derive:$v$ edge:$(w,v)$ 影响
$4$ $(3,4)$ $GP(4)=\gamma(R,\Lambda,\varnothing)$

interval tree 5

$u=3$时构建的树。

loop: $u=2$

derive:$v$ edge:$(w,v)$ 影响
$3$ $(2,3)$ $GP(3)=\gamma(P,\Lambda^1,\varnothing)$
^ $(5,3)$ $subroot(w)=3,~~p(subroot(w),v)=\gamma(R,\Lambda^2,\varnothing),~~\phi=\texttt{true},~~\Phi(3)=\texttt{true},~~ListP(3)={(3,3,\gamma(R,\Lambda^2,\varnothing))}$
^ $(9,3)$ $subroot(w)=8,~~p(subroot(w),v)=\gamma(Q,\Lambda^3,\varnothing),~~\phi=\texttt{true},~~\Phi(3)=\texttt{true},~~ListP(3)={(3,3,\gamma(R,\Lambda^2,\varnothing)),(8,3,\gamma(Q,\Lambda^3,\varnothing))}$
$6$ $(3,6)$ $subroot(w)=3,~~p(subroot(w),v)=\gamma(R,\varnothing,\Lambda^1),~~\phi=\texttt{true},~~\Phi(6)=\texttt{true},~~ListP(6)={(3,6,\gamma(R,\varnothing,\Lambda^1))}$
^ $(13,6)$ $subroot(w)=8,~~p(subroot(w),v)=\gamma(Q,\varnothing,\Lambda^2),~~\phi=\texttt{true},~~\Phi(6)=\texttt{true},~~ListP(6)={(3,6,\gamma(R,\varnothing,\Lambda^1)),(8,6,\gamma(Q,\varnothing,\Lambda^2))}$
$8$ $(2,8)$ $GP(2)=\gamma(P,\varnothing,\Lambda)$

sequence: $8\rightarrow 6,8\rightarrow 3,3\rightarrow 6\Rightarrow 8,3,6$

merge:$v$ $subroot(w),v,p(subroot(w),v)$ 影响
$3$ $3,3,\gamma(R,\Lambda^2,\varnothing)$ $G^*(3)=\gamma(R,\Lambda^2,\varnothing)$
^ $8,3,\gamma(Q,\Lambda^3,\varnothing)$ $GP(3)=\gamma(P,\Lambda^1,\gamma(Q,\Lambda^3,\varnothing))$
$6$ $3,6,\gamma(R,\varnothing,\Lambda^1)$ $GP(6)=\gamma(P,\gamma(R,\varnothing,\Lambda^1),\gamma(Q,\gamma(R,\varnothing,\Lambda^1),\varnothing)),\Phi(6)=\texttt{true}$
^ $8,6,\gamma(Q,\varnothing,\Lambda^2)$ $GP(6)=\gamma(P,\gamma(R,\varnothing,\Lambda^1),\gamma(Q,\gamma(R,\varnothing,\Lambda^1),\Lambda^2))$

原论文给的$GP(6)$似乎求错了。此时树的样子为:

interval tree 6

$u=2$时构建的树。

loop: $u=1$

derive:$v$ edge:$(w,v)$ 影响
$1$ $(1,2)$ $GP(2)=\Lambda$

interval tree 7

$u=1$时构建的树。

  1. P. Tu and D. Padua, “Efficient building and placing of gating functions,” in Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation - PLDI ’95, 1995. ↩︎

  2. R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck, “Efficiently computing static single assignment form and the control dependence graph,” ACM Trans. Program. Lang. Syst., vol. 13, no. 4, pp. 451–490, 1991. ↩︎ ↩︎

  3. K. J. Ottenstein, R. A. Ballance, and A. B. MacCabe, “The program dependence web: a representation supporting control-, data-, and demand-driven interpretation of imperative languages,” in Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation - PLDI ’90, 1990. ↩︎

  4. P. Havlak, “Construction of thinned gated single-assignment form,” in Languages and Compilers for Parallel Computing, Berlin, Heidelberg: Springer Berlin Heidelberg, 1994, pp. 477–499. ↩︎

  5. R. E. Tarjan, “Fast algorithms for solving path problems,” J. ACM, vol. 28, no. 3, pp. 594–614, 1981. ↩︎

最优化理论与算法第3章:单纯形方法

2020年9月27日 06:00

本文的内容主要来自陈宝林的《最优化理论与算法(第2版)》第3章《单纯形方法》和老师的PPT。

单纯形方法原理

基本可行解的转换

考虑问题:

$$\begin{aligned} \min \;\;\;\;&f\stackrel{\text{def}}{=}\vec{c}^T\vec{x} \\ \text{s. t.} \;\;\;\;&\mathbf{A}\vec{x}=\vec{b} \\ \;\;\;\;&\vec{x}\geq\vec{0} \end{aligned}$$

同时记:

$$\begin{aligned} &\mathbf{A}=[\vec{p}_1,\vec{p}_2,\cdots,\vec{p}_n]=[\mathbf{B}\mid\mathbf{N}]\\ &\vec{x}^{(0)}=\begin{bmatrix} \mathbf{B}^{-1}\vec{b}\\ \vec{0} \end{bmatrix} \end{aligned}$$

其中$\mathbf{B}$和$\mathbf{N}$分别是基本可行解$\vec{x}^{(0)}$的基矩阵和非基矩阵。则$\vec{x}^{(0)}$处的目标函数值为:

$$f_0=\vec{c}^T\vec{x}^{(0)}=\vec{c}_B^T\mathbf{B}^{-1}\vec{b}$$

我们的目标是从这个基本可行解出发,得到另一个目标函数值更小的。考虑任意可行解:

$$\vec{x}=\begin{bmatrix} \vec{x}_B\\ \vec{x}_N \end{bmatrix}$$

注意,这里的$\vec{x}_B$和$\vec{x}_N$的基矩阵和非基矩阵是相对$\vec{x}^{(0)}$说的。这时候目标函数值为:

$$\begin{aligned} f&=\vec{c}_B^T(\mathbf{B}^{-1}\vec{b}-\mathbf{B}^{-1}\mathbf{N}\vec{x}_N)+\vec{c}_N^T\vec{x}_N\\ &=f_0-(\vec{c}_B^T\mathbf{B}^{-1}\mathbf{N}-\vec{c}_N^T)\vec{x}_N\\ &=f_0-\sum_{j=m+1}^n(\vec{c}_B^T\mathbf{B}^{-1}\vec{p}_j-c_j)x_j\\ &=f_0-\sum_{j=m+1}^n(z_j-c_j)x_j\;\;\;\;\text{其中}z_j=\vec{c}_B^T\mathbf{B}^{-1}\vec{p}_j \end{aligned}$$

注意到$\vec{x}\geq 0$,所以此时若$z_j-c_j\leq 0, j=m+1,\cdots,n$,则达到最优解条件。若此时存在$z_j-c_j>0$,为了让$f$下降得更快,所以我们会添加一个基$x_k, m<k\leq n$,这个基对应的$z_j-c_j$应当是最最大的。所以有:

$$z_k-c_k=\max_{m<j\leq n} z_j-c_j$$

则此时:

$$\begin{aligned} \vec{x}_B&=\mathbf{B}^{-1}\vec{b}-\mathbf{B}^{-1}\vec{p}_kx_k\\ &=\vec{x}_B^{(0)}-\vec{y}_kx_k\\ &\text{其中}\vec{x}_B^{(0)}=\mathbf{B}^{-1}\vec{b},\vec{y}_k=\mathbf{B}^{-1}\vec{p}_k \end{aligned}$$

为了保证新的解是可行解,我们需要确保$\vec{x}_B\geq 0$,即$\vec{x}_B^{(0)}-\vec{y}_kx_k\geq 0$,所以我们应当取:

$$x_k=\min\left\{\frac{x_{Bi}^{(0)}}{y_{ki}}\mid y_{ki}>0\right\}=\frac{x_{Br}^{(0)}}{y_{kr}}$$

若$\vec{y}_k\leq 0$,则问题无界。如果找到了,这时候$x_r=0$,得到了一个新的可行解,接下来我们证明这是基本可行解,方法是证明$\vec{p}_1,\cdots,\vec{p}_{r-1},\vec{p}_k,\vec{p}_{r+1},\vec{p}_m$线性无关。注意到$\vec{p}_1,\cdots,\vec{p}_{r-1},\vec{p}_r,\vec{p}_{r+1},\vec{p}_m$是线性无关的,而$\vec{p}_k=\mathbf{B}\vec{y}_k=\sum\limits_{i=1}^m y_{ki}\vec{p}_i$,而$y_{kr}\neq 0$,故$\vec{p}_r$可被$\vec{p}_1,\cdots,\vec{p}_{r-1},\vec{p}_k,\vec{p}_{r+1},\vec{p}_m$线性标出,故$\vec{p}_1,\cdots,\vec{p}_{r-1},\vec{p}_k,\vec{p}_{r+1},\vec{p}_m$线性无关。故:

$$\vec{x}=[x_0^{(0)},\cdots,x_{r-1}^{(0)},0,x_{r+1}^{(0)},\cdots,x_m^{(0)},0,\cdots,0,x_k,0,\cdots,0]^T$$

是新的更优的基本可行解。

定理 3.1.1 若在极小化问题中,对于某个基本可行解,所有$z_j-c_j\leq 0$,则这个基本可行解是最优解,这里:

$$z_j-c_j=\vec{c}_B^T\mathbf{B}^{-1}\vec{p}_j-c_j, j=1,\cdots,n$$

称为判别数检验数。注:如果$j$是基的下标,则判别数为$0$。

单纯形方法计算步骤

首先要给定一个初始的基本可行解,假设初始基矩阵为$\mathbf{B}$,执行以下步骤:

  1. 求$\vec{x}_B=\mathbf{B}^{-1}\vec{b}$;

  2. 求单纯形子$\vec{w}^T=\vec{c}_B\mathbf{B}^{-1}$,对于所有非基变量,计算判别数$z_j-c_j=\vec{w}^T\vec{p}_j-c_j$,令:

    $$z_k-c_k=\max_{j\in\text{非基变量下标集}} z_j-c_j$$

    若$z_k-c_k\leq 0$,则找到最优解,退出。否则进入下一步;

  3. 求$\vec{y}_k=\mathbf{B}^{-1}\vec{p}_k$,若$\vec{y}_k\leq 0$,则不存在有限最优解,退出,否则进入下一步;

  4. 确定下标$r$,使:

    $$\frac{\vec{x}_{Br}}{y_{kr}}=\min\left\{\frac{\vec{x}_{Bi}}{y_{ki}}\mid y_{ki}>0\right\}$$

    $x_r$为离基变量,$x_k$为进基变量,用$\vec{p}_k$替换$\vec{p}_r$得到新的基矩阵,返回步骤1。

对于最大化问题,步骤2的$\max$改$\min$即可。

收敛性

所有迭代会出现下列情况:

  1. $z_k-c_k\leq 0$,当前解为最优解;
  2. $z_k-c_k>0$且$\vec{y}_k\leq 0$,问题无界;
  3. $z_k-c_k>0$且$\vec{y}_k\nleq 0$,找到新基本可行解,非退化情况下目标函数下降。

定理 3.1.2 对于非退化问题,单纯形方法经过有限次迭代要么达到最优基本可行解,要么无界。

使用表格形式的单纯形方法

首先,对标准形式作变换可以得到:

$$\begin{aligned} \min \;\;\;\;&f \\ \text{s. t.} \;\;\;\;&f-\vec{c}_B^T\vec{x}_B-\vec{c}_N^T\vec{x}_N=0 \\ \;\;\;\;&\mathbf{B}\vec{x}_B+\mathbf{N}\vec{x}_N=\vec{b} \\ \;\;\;\;&\vec{x}_B\geq\vec{0},\vec{x}_N\geq\vec{0} \end{aligned}$$

消去第一个等式中的$\vec{x}_B$,得到:

$$\begin{aligned} \min \;\;\;\;&f \\ \text{s. t.} \;\;\;\;&\mathbf{B}\vec{x}_B+\mathbf{N}\vec{x}_N=\vec{b} \\ \;\;\;\;&f+(\vec{c}_B^T\mathbf{B}^{-1}\mathbf{N}-\vec{c}_N^T)\vec{x}_N=0 \\ \;\;\;\;&\vec{x}_B\geq\vec{0},\vec{x}_N\geq\vec{0} \end{aligned}$$

将上式写在表格中就有了单纯形表

$f$ $\vec{x}_B$ $\vec{x}_N$ 右端
$\vec{x}_B$ $\vec{0}$ $\mathbf{I}_m$ $\mathbf{B}^{-1}\mathbf{N}$ $\mathbf{B}^{-1}\vec{b}$
$f$ $1$ $0$ $\vec{c}_B\mathbf{B}^{-1}\mathbf{N}-\vec{c}_N$ $\vec{c}_B\mathbf{B}^{-1}\vec{b}$

其中,$\vec{c}_B\mathbf{B}^{-1}\mathbf{N}-\vec{c}_N$的每一个分量即为判别数$z_j-c_j$,$\mathbf{B}^{-1}\mathbf{N}$的列分量就是$\vec{y}_k$。第一列通常省略。

初始的时候。我们已经有了一个可行解$\vec{x}_N=\vec{0}$。

若$\vec{c}_B\mathbf{B}^{-1}\mathbf{N}-\vec{c}_N\leq 0$,则找到了最优解。

若$\vec{c}_B\mathbf{B}^{-1}\mathbf{N}-\vec{c}_N\nleq 0$,则需要用主元消去法。在表的最后一行中,寻找除右端外的最大值,它所在的一行称主列,从而确定了离基变量。这时候寻找主列上除最后一列外大于0的元素,且右端除以该元素值最小的,找到的该元素称为主元,它所在的行称为主行,再用主行加上初等行变换,消去主元所在列,并使主元为$1$。循环此操作。

最优化理论与算法第1章:引言

2020年9月18日 00:38

本文的内容主要来自陈宝林的《最优化理论与算法(第2版)》第1章《引言》。

学科简述

(略)

线性与非线性规划问题

目标函数和约束函数都是线性的,称为线性规划问题,若含有非线性函数,称为非线性规划问题

满足约束条件的点称为可行点,全体可行点组成的集合称为可行集可行域。如果可行域是整个空间称为无约束问题

定义1.2.1 $f:\mathbb{R}^n\rightarrow\mathbb{R}$为目标函数,$S$为可行域,$\vec{x}’\in S$,若$\forall \vec{x}(\vec{x}\in S\rightarrow f(\vec{x})\geq f(\vec{x}’))$,则称$\vec{x}’$为$f$在$S$上的全局极小点

定义1.2.2 $f:\mathbb{R}^n\rightarrow\mathbb{R}$为目标函数,$S$为可行域,$\vec{x}’\in S$,若$\exists\epsilon(\epsilon\in\mathbb{R}^+\land\forall \vec{x}(\vec{x}\in N(\vec{x}’,\epsilon)\rightarrow f(\vec{x})\geq f(\vec{x}’)))$,则称$\vec{x}’$为$f$在$S$上的局部极小点。其中$N(\vec{x}’,\epsilon)={\vec{x}\mid|\vec{x}-\vec{x}’|<\epsilon}$为邻域。

注:全局极小点不需要用到距离和范数,它和函数的最值定义几乎是一样的,只是定义域成了可行域。而局部极小点用到了邻域,需要距离也就是范数,它和函数的极小值定义也几乎是一样的。

几个数学概念

向量范数和矩阵范数

定义1.3.1 实值函数$|\cdot|:\mathbb{R}^n\rightarrow\mathbb{R}$称为向量范数,若满足$\forall\alpha,\vec{x},\vec{y}(\alpha\in\mathbf{R}\land \vec{x},\vec{y}\in\mathbf{R}^n)$:

  1. 严格正定性:$|\vec{x}|\geq 0\land(|\vec{x}|=0\leftrightarrow\vec{x}=\vec{0})$;
  2. 齐次性(线性形):$|\alpha\vec{x}|=|\alpha|\cdot|\vec{x}|$
  3. 三角不等式:$|\vec{x}+\vec{y}|\leq|\vec{x}|+|\vec{y}|$

常见的向量范数有:

  1. $L_1$范数:$|\vec{x}|_1=\sum\limits_{j=1}^n |x_j|$
  2. $L_2$范数:$|\vec{x}|_2=(\sum\limits_{j=1}^n x_j^2)^\frac{1}{2}$
  3. $L_\infty$范数:$|\vec{x}|_\infty=\max\limits_j |x_j|$

注:这里的范数都称为$L_p$-范数,来源于$|\vec{x}|_p=(\sum\limits_{j=1}^n |x_j|^p)^\frac{1}{p}$。其中$|\vec{x}|_\infty=\lim\limits_{p\rightarrow+\infty}(\sum\limits_{j=1}^n |x_j|^p)^\frac{1}{p}$。

定义1.3.2 $|\cdot|_\alpha,|\cdot|_\beta$为$\mathbb{R}^n$上的范数,若$\exists c_1, c_2(c_1, c_2\in\mathbb{R}^+\land\forall\vec{x}(\vec{x}\in\mathbb{R}^n\rightarrow c_1|\vec{x}|_\alpha\leq |\vec{x}|_\beta\leq c_2|\vec{x}|_\alpha))$,则称这两个范数等价

$\mathbb{R}^n$中任何两个范数等价(这里必须是有限维,这个定理的证明我尚不能掌握,需要参考泛函分析)。

定义1.3.3 $\mathbf{A}\in\mathbb{R}^{m\times n}$为矩阵,$|\cdot|_\alpha$为$\mathbb{R}^m$上的向量范数,$|\cdot|_\beta$为$\mathbb{R}^n$上的向量范数,定义矩阵范数$|\mathbf{A}|=\max\limits_{|\vec{x}|_\beta=1}|\mathbf{A}\vec{x}|_\alpha$。

注:这里可以想像成矩阵的范数,是其对应的线性映射,能够将一个向量拉长的最大倍数。

定理1.3.1 矩阵范数的性质:

  1. $|\mathbf{A}\vec{x}|_\alpha\leq|\mathbf{A}|\cdot|\vec{x}|_\beta$;
  2. $|\lambda\mathbf{A}|=|\lambda|\cdot|\mathbf{A}|$;
  3. $|\mathbf{A}+\mathbf{B}|\leq|\mathbf{A}|+|\mathbf{B}|$;
  4. $|\mathbf{A}\mathbf{D}|\leq|\mathbf{A}|\cdot|\mathbf{D}|$。

定理1.3.1 (1) 证:

$$ \begin{aligned} &|\mathbf{A}|=\max\limits_{|\vec{x}|_\beta=1}|\mathbf{A}\vec{x}|_\alpha \\ \Rightarrow &|\mathbf{A}|=\max\limits_{|\frac{\vec{x}}{|\vec{x}|}_\beta|_\beta=1}|\mathbf{A}\frac{\vec{x}}{|\vec{x}|}_\beta|_\alpha;(\text{变量代换}) \\ \Rightarrow &|\mathbf{A}|=\max\frac{|\mathbf{A}\vec{x}|_\alpha}{|\vec{x}|_\beta};(\text{利用齐次性,并去掉了恒成立的max条}) \\ \Rightarrow &|\mathbf{A}|\geq\frac{|\mathbf{A}\vec{x}|_\alpha}{|\vec{x}|_\beta} \end{aligned} $$

定理1.3.1 (3) 证:

$$ \begin{aligned} |\mathbf{A}+\mathbf{B}|&=\max\limits_{|\vec{x}|_\beta=1}|(\mathbf{A}+\mathbf{B})\vec{x}|_\alpha \\ &\leq\max\limits_{|\vec{x}|_\beta=1}|\mathbf{A}\vec{x}|_\alpha + |\mathbf{B}\vec{x}|_\alpha;(\text{三角不等式}) \\ &=|\mathbf{A}|+|\mathbf{B}| \end{aligned} $$

定理1.3.1 (4) 证:

$$ \begin{aligned} |\mathbf{A}\mathbf{D}|&=\max\limits_{|\vec{x}|_\beta=1}|\mathbf{A}\mathbf{D}\vec{x}|_\alpha \\ &\leq\max\limits_{|\vec{x}|_\beta=1}|\mathbf{A}|\cdot|\mathbf{D}\vec{x}|_\gamma;(\text{性质1}) \\ &=|\mathbf{A}|\cdot|\mathbf{D}| \end{aligned} $$

常见的矩阵范数有:

  1. $|\mathbf{A}|_1=\max_j\sum\limits_{i=1}^m |a_{ij}|$;
  2. $|\mathbf{A}|_2=\sqrt[]{\lambda_{\mathbf{A}^T\mathbf{A}}}$,($\lambda$是最大特征值,这被称为谱范数);
  3. $|\mathbf{A}|_\infty=\max_i\sum\limits_{j=1}^n |a_{ij}|$。

注:这里$p$矩阵范数就是$L_p$向量范数的组合,我采用形象化的方式来解释这3种范数。先考虑第2个范数,它将球拉伸成椭球,长径拉伸最大值也就是其最大的奇异值;再考虑第1个范数,它将一个立方体拉伸成长方体,其中立方体的顶点是$[0,\dots,0,1,0,\dots,0]^T$,映射完后,相当于挨个取出列向量,求他们的$L_1$范数(求和),再取出最大的;最后考虑第3个范数,它同样将一个立方体拉伸成长方体,其中立方体的顶点是$[1,\dots,1]^T$,映射完后,相当于将行向量求和,最后取出最大的。

序列的极限

定义1.3.4 ${\vec{x}^{(k)}}$是$\mathbb{R}^n$中的向量序列,$\vec{x}’\in\mathbb{R}^n$,若:

$$\forall\epsilon(\epsilon\in\mathbb{R}^+\rightarrow\exists N(N\in\mathbb{N}^+\land\forall n(n\in\mathbb{N}^+\land n>N\rightarrow |\vec{x}^{(n)}-\vec{x}’|<\epsilon))$$

则称序列收敛到$\vec{x}’$,或序列以$\vec{x}’$为极限,记作$\lim\limits_{k\to\infty}\vec{x}^{(k)}=\vec{x}’$。

序列若存在极限,则任何子序列有相同的极限(选取适当的$N$即可证明),序列的极限是唯一的。

序列的极限是唯一的 证:

反证法,若存在两极限,则$\lim\limits_{k\to\infty}\vec{x}^{(k)}=\vec{a}$同时$\lim\limits_{k\to\infty}\vec{x}^{(k)}=\vec{b}$,且$\vec{a}\neq\vec{b}$。取$\epsilon_0=\frac{|\vec{b}-\vec{a}|}{2}$,由假设知道:

$$ \begin{aligned} &\begin{aligned} &\exists N_1(N_1\in\mathbf{N}^+\land\forall n(n\in\mathbb{N}^+\land n>N_1\rightarrow |\vec{x}^{(n)}-\vec{a}|<\epsilon_0))) \\ \land &\exists N_2(N_2\in\mathbf{N}^+\land\forall n(n\in\mathbb{N}^+\land n>N_2\rightarrow |\vec{x}^{(n)}-\vec{b}|<\epsilon_0))) \end{aligned} \\ \Rightarrow & \exists N_1,N_2(N_1,N_2\in\mathbf{N}^+\land \forall n (n\in\mathbb{N}^+\land n>N_1\land n>N_2\rightarrow |\vec{x}^{(n)}-\vec{a}|<\epsilon_0 \land |\vec{x}^{(n)}-\vec{b}|<\epsilon_0)) \\ \Rightarrow & \exists N_1,N_2(N_1,N_2\in\mathbf{N}^+\land \forall n (n\in\mathbb{N}^+\land n>\max(N_1,N_2)\rightarrow |\vec{x}^{(n)}-\vec{a}| + |\vec{x}^{(n)}-\vec{b}|<|\vec{b}-\vec{a}|)) \\ \Rightarrow & \bot ;(\text{违反三角不等式}) \end{aligned} $$

定义1.3.5 ${\vec{x}^{(k)}}$是$\mathbb{R}^n$中的向量序列,若存在子序列${\vec{x}^{(k_j)}}$,$\lim\limits_{k_j\to\infty}\vec{x}^{(k_j)}=\hat{\vec{x}}$,则称$\hat{\vec{x}}$是${\vec{x}^{(k)}}$的一个聚点

Bolzano–Weierstrass定理:$\mathbb{R}^n$中有界序列必有聚点,即有界序列必有收敛子列,证明详见波尔查诺-魏尔斯特拉斯定理 - 维基百科,自由的百科全书。这只在有限维实向量赋范空间成立。

定义1.3.6 ${\vec{x}^{(k)}}$是$\mathbb{R}^n$中的向量序列,若:

$$\forall\epsilon(\epsilon\in\mathbb{R}^+\rightarrow\exists N(N\in\mathbb{N}^+\land\forall n_1,n_2(n_1,n_2\in\mathbb{N}^+\land n_1,n_2>N\rightarrow|\vec{x}^{n_1}-\vec{x}^{n_2}|<\epsilon)))$$

则称${\vec{x}^{(k)}}$为柯西序列。$\mathbb{R}^n$中,柯西序列和收敛数学互为充要条件。

注:柯西序列的定义没有涉及到极限值,这便于完成一些对收敛性的证明。那些所有柯西序列收敛到空间中某点的空间,称为完备空间,比如实数是完备的,有理数是不完备的。完备空间中,柯西序列和收敛序列互为充要条件。不完备空间中,柯西序列是收敛序列的必要条件。

定理1.3.2 ${\vec{x}^{(k)}}$是$\mathbb{R}^n$中的柯西序列,则其聚点为极限点。

注:$\mathbb{R}^n$中,收敛序列(即柯西序列)必有唯一聚点,且该聚点为极限点。一个序列可能有多个聚点。

设$S\subseteq\mathbb{R}^n$:

  1. 若$S$中每个收敛序列的极限均在$S$,则称$S$为闭集
  2. 若$\forall\hat{\vec{x}}(\hat{\vec{x}}\in S\rightarrow\exists\epsilon(\epsilon\in\mathbb{R}^+\land N(\hat{\vec{x}},\epsilon)\subseteq S))$,则称$S$为开集,这样的$\hat{\vec{x}}$称为内点
  3. 若$S$是有界闭集,则称$S$为紧集

闭集的另一个定义是:一个补集是开集的集合称为闭集。这里集合$S$的补集定义为$S^C={x\mid x\notin S,x\in\mathbb{N}}$。

紧集的一个等价定义是:集合中的序列都有收敛子序列。由Bolzano–Weierstrass定理可证$S\subseteq\mathbb{R}^n$紧致,当且仅当,$S$为有界闭集。

梯度、海森矩阵、泰勒展开式

设$f:S\to\mathbb{R}$,其中$S\subseteq\mathbb{R}^n$。如果$f$在$S$中的每一点连续,则称$f$在$S$上连续,记作$f\in C(S)$。若$f$在每一点$\vec{x}\in S$,一阶导数$\frac{\partial f(\vec{x})}{\partial x_i}$存在且连续,则称$f$在$S$上连续可微,记作$f\in C^1(S)$。若$f$在每一点$\vec{x}\in S$,二阶导数$\frac{\partial^2 f(\vec{x})}{\partial x_i\partial x_j}$存在且连续,则称$f$在$S$上二次连续可微,记作$f\in C^2(S)$。

函数$f\in C^1(S)$在$\vec{x}$的梯度为:

$$\nabla f(\vec{x})=\begin{bmatrix} \frac{\partial f(\vec{x})}{\partial x_1},\frac{\partial f(\vec{x})}{\partial x_2},\cdots,\frac{\partial f(\vec{x})}{\partial x_n} \end{bmatrix}^T$$

函数$f\in C^2(S)$在$\vec{x}$的海森矩阵为对称矩阵,如下:

$$[\nabla^2 f(\vec{x})]_{ij}=\frac{\partial^2 f(\vec{x})}{\partial x_i\partial x_j}$$

对于二次函数$f(\vec{x})=\frac{1}{2}\vec{x}^T\mathbf{A}\vec{x}+\vec{b}^T\vec{x}+c$:

  1. 其梯度:$\nabla f(\vec{x})=\mathbf{A}\vec{x} + \vec{b}$;
  2. 其海森矩阵:$\nabla^2 f(\vec{x})=\mathbf{A}$。

对$S\in\mathbb{R}^n$上的函数$f:S\to\mathbb{R}$:

  1. 若$f\in C^1(S)$,则对任意$\vec{x}_0\in\mathbb{R}^n$,有一阶泰勒展式: $$f(\vec{x})=f(\vec{x_0})+\nabla f(\vec{x}_0)^T(\vec{x}-\vec{x}_0)+o(|\vec{x}-\vec{x}_0|)$$
  2. 若$f\in C^2(S)$,则对任意$\vec{x}_0\in\mathbb{R}^n$,有二阶泰勒展式: $$f(\vec{x})=f(\vec{x_0})+\nabla f(\vec{x}_0)^T(\vec{x}-\vec{x}_0)+\frac{1}{2}(\vec{x}-\vec{x}_0)^T\nabla^2 f(\vec{x}_0)(\vec{x}-\vec{x}_0)+o(|\vec{x}-\vec{x}_0|^2)$$

雅可比矩阵、链式法则和隐函数存在定理

雅可比矩阵

考虑向量值函数$\vec{h}:\mathbb{R}^n\to\mathbb{R}^m$:

$$\vec{h}(\vec{x})=(h_1(\vec{x}),h_2(\vec{x}),\cdots,h_m(\vec{x}))^T$$

若对任意$i,j$,$\frac{\partial h_i(\vec{x})}{\partial x_j}$存在,则其雅可比矩阵为:

$$[\vec{h}’(\vec{x})]_{ij}=\frac{\partial h_i(\vec{x})}{\partial x_j}$$

也可记作$\nabla\vec{h}(\vec{x})^T$。

链式法则

对于实数空间上的复合向量值函数$\vec{h}(\vec{x})=\vec{f}(\vec{g}(\vec{x}))$,若$f,g$均可微,则有:

$$\vec{h}’(\vec{x})=\vec{h}’(\vec{g}(\vec{x}))\vec{g}’(\vec{x})$$

隐函数定理

定理 1.3.3 对于$\vec{h}:\mathbb{R}^m\times\mathbb{R}^n\to\mathbb{R}^m$,定点向量$\vec{a}^{(0)}\in\mathbb{R}^m,\vec{b}^{(0)}\in\mathbb{R}^n$,令$\vec{x}^{(0)}=[\vec{a}^{(0)},|,\vec{b}^{(0)}]$,满足:

  1. $\vec{h}(\vec{x}^{(0)})=\vec{0}$;
  2. 在$\vec{x}^{(0)}$的某一个邻域中,$h_i\in C^1 (i=1,\cdots,m)$;
  3. $\begin{vmatrix}\begin{bmatrix}\frac{\partial h_i}{\partial a_j}(\vec{x})\end{bmatrix}_{m\times m}\end{vmatrix}\neq 0$

则存在$\vec{b}^{(0)}\in\mathbb{R}^n$的一个邻域,使得对于邻域中的点$\vec{b}\in\mathbb{R}^n$,唯一存在函数$\vec{\phi}:\mathbb{R}^n\to\mathbb{R}^m$,满足:

  1. $\phi_i\in C^1;(i=1,\cdots,m)$;
  2. $\vec{a}^{(0)}=\phi(\vec{b}^{(0)})$;
  3. $\vec{h}([\vec{\phi}(\vec{b}^{(0)}),|,\vec{b}^{(0)}])=\vec{0}$。

二次型的正定性与半正定性

正定二次型的定义 对实二次型$f(\vec{x})=\vec{x}^T\mathbf{A}\vec{x}$,若:

$$\forall\vec{x}(\vec{x}\in\mathbb{R}^n\land\vec{x}\neq\vec{0}\rightarrow f(\vec{x})\geq 0)$$

则称$f(x)$为正定二次型,$\mathbf{A}$为正定矩阵

正定二次型的判断 对于$\mathbf{A}\in\mathbb{R}^{n\times n}$,下列命题等价:

  1. $\vec{x}^T\mathbf{A}\vec{x}$是正定二次型;
  2. $\mathbf{A}$是正定矩阵;
  3. $\mathbf{A}$的$n$个顺序主子式都大于零;
  4. $\mathbf{A}$的$n$个特征值都大于零;
  5. 存在可逆矩阵$\mathbf{P}$,使得$A=P^TP$。

半正定二次型的定义 对实二次型$f(\vec{x})=\vec{x}^T\mathbf{A}\vec{x}$,若:

$$\forall\vec{x}(\vec{x}\in\mathbb{R}^n\land\vec{x}\neq\vec{0}\rightarrow f(\vec{x})\geq 0)\land\exists\vec{x}(\vec{x}\in\mathbb{R}^n\land\vec{x}\neq\vec{0}\land f(\vec{x})=0)$$

则称$f(x)$为半正定二次型,$\mathbf{A}$为半正定矩阵

半正定二次型的判断 对于$\mathbf{A}\in\mathbb{R}^{n\times n}$,下列命题等价:

  1. $\vec{x}^T\mathbf{A}\vec{x}$是半正定二次型;
  2. $\mathbf{A}$是半正定矩阵;
  3. $\mathbf{A}$的所有主子式都大于等于零,且至少有一个等于零;
  4. $\mathbf{A}$的$n$个特征值都大于等于零,且至少有一个等于零。

凸集和凸函数

凸集

定义1.4.1 设$S\subseteq\mathbb{R}^n$,若$\forall\vec{x}_1,\vec{x}_2,\lambda(x_1,x_2\in S\land\lambda\in[0,1]\rightarrow\lambda\vec{x}_1+(1-\lambda)\vec{x}_2\in S)$,则称$S$为凸集。其中$\lambda\vec{x}_1+(1-\lambda)\vec{x}_2$称为凸组合

常见的凸集有超平面${\vec{x}\mid\vec{p}^T\vec{x}=\alpha}$、半空间${\vec{x}\mid\vec{p}^T\vec{x}\leq\alpha}$、射线${\vec{x}\mid\vec{x}_0+\lambda\vec{d},\lambda\geq 0}$(其中$\vec{x}_0$为顶点,$\vec{d}$为方向向量)。

设$S_1,S_2\subseteq\mathbb{R}^n$为凸集,$\beta\in\mathbb{R}$,则:

  1. $\beta S_1={\beta\vec{x}\mid\vec{x}\in S_1}$为凸集;
  2. $S_1\cap S_2$为凸集;
  3. $S_1+S_2={\vec{x}_1+\vec{x}_2\mid\vec{x}_1\in S_1,\vec{x}_2\in S_2}$为凸集;
  4. $S_1-S_2={\vec{x}_1-\vec{x}_2\mid\vec{x}_1\in S_1,\vec{x}_2\in S_2}$为凸集。

凸集的线性组合也是凸集,但凸集的并不是凸集。

定义1.4.2 设$C\subseteq\mathbb{R}^n$,若$\forall\vec{x},\lambda(\vec{x}\in C\land\lambda\in\mathbb{R}^*\rightarrow\lambda\vec{x}\in C)$,则称$C$为。若$C$又为凸集,则称$C$为凸锥

向量集${\vec{x}_1,\vec{x}_2,\cdots,\vec{x}_n}$的非负线性组合${\sum\limits_{i=1}^n\lambda_i\vec{x}_i\mid\lambda_i\geq 0,i=1,\cdots,n}$。

定义1.4.3 有限个半空间的交${\vec{x}\mid\mathbf{A}\vec{x}\leq\vec{b}}$称为多面集,若$\vec{b}=\vec{0}$,则多面集成为凸锥。

定义1.4.4 设$S$为非空凸集,$\vec{x}\in S$,若$\forall\vec{x}_1,\vec{x}_2,\lambda(\vec{x}_1,\vec{x}_2\in S\land\lambda\in(0,1)\land\vec{x}=\lambda\vec{x}_1+(1-\lambda)\vec{x}_2\rightarrow\vec{x}=\vec{x}_1=\vec{x}_2)$,则称$\vec{x}$为凸集$S$的极点

紧凸集中的点可以表示为极点的线性组合,但对无界集并不成立。

定义1.4.5 设$S\subseteq\mathbb{R}^n$为闭凸集,$\vec{d}\in\mathbb{R}^n$非零,若$\forall\vec{x}(\vec{x}\in S\rightarrow{\vec{x}+\lambda\vec{d}\mid\lambda\in\mathbb{R}^+}\subseteq S)$,则称$\vec{d}$为$S$的方向。又设$\vec{d}_1,\vec{d}_2$是$S$的两个方向,若$\forall\lambda(\lambda\in\mathbb{R}^+\rightarrow\vec{d}_1\neq\lambda\vec{d}_2)$,则称$\vec{d}_1,\vec{d}_2$是不同的方向。若$S$的方向$\vec{d}$不能表示成两个不同方向的正的线性组合,则称$\vec{d}$是$S$的极方向。

有界集不存在方向和极方向。

考虑平面直角坐标系中的半平面$x\geq \alpha$,可以发现有3个极方向,分别是$(0, \lambda_+)^T,(0, \lambda_-)^T,(\lambda_+, \lambda)^T$,且不存在极点。

特别地,对于$S={x\mid\mathbf{A}\vec{x}=\vec{b},\vec{x}\geq\vec{0}}$,$\vec{d}$为$S$的方向等价于$\vec{d}\geq\vec{0}\land\mathbf{A}\vec{d}=\vec{0}$。

定理1.4.1 表示定理:设$S={x\mid\mathbf{A}\vec{x}=\vec{b},\vec{x}\geq\vec{0}}$为非空多面集(它一定是多面集),则:

  1. 极点集非空且为有限个$\vec{x}_1,\cdots,\vec{x}_k$;
  2. 极方向为空当且仅当$S$有界,$S$无界,则有有限个极方向$\vec{d}_1,\cdots,\vec{d}_l$;
  3. $\vec{x}\in S$当且仅当: $$\begin{aligned}&\vec{x}=\sum_{j=1}^k\lambda_j\vec{x}_{j}+\sum_{j=1}^l\mu_j\vec{d}_j,\\ &\sum_{j=1}^k\lambda_j=1,\\ &\lambda_j\geq 0, j=1,\cdots,k,\\ &\mu_j\geq 0, j=1,\cdots,l. \end{aligned}$$

凸集分离定理

(暂不收录)

凸函数

(暂不收录)

凸函数的判别

(暂不收录)

凸规划

(暂不收录)

❌
❌