理论证明 Theoretical Properties

结构上的操作语义 Structural Operational Semantics

理论分析需要借助结构归纳法，所以我们要先将代码描述成结构。由于我们不再记录每一步操作后的变量值，所以我们只记录最初值和变量名

v用来表示value值 ρ表示变量组

v要记录所在语句，变量组。所以我们可以列出这样的表达式：v ::= c | close t in ρ

相对的ρ要记录变量名和值 ： ρ ::= [] | ρ[x -> v]

也就有fn x => e_0可以表示为 close(fn x => e_0) in ρ

由于控制流分析不记录过程中变量的变化，所以会出现中间变量，也就是调用一个函数时，会有一个初始值，而整个程序也有一个初始值，函数的初始值就是中间变量，也就是局部变量。

我们用ie表示中间出现的表达式，it表示中间出现的项

表达式就是经过标签处理的代码，而项就是表达式中除去标签的部分。因为局部变量作用域需要记录，所以it会出现bind ρ in ie来实现记录作用域。相对的其值也需要记录，所以it又会有close t in ρ的情况

例子 Examples

上述式子中包括let in 结构，fn结构以及fun f结构，首先对两个fn结构进行处理：fn y => y ^2 |- close(fn y => y ^2) 我们用id_y表示 fn z => z ^7 |- close(fn z => z ^7) 我们用id_z表示。然后是fun f 结构fun f x => (f ^1 (fn y => y ^2)) |- close(fun f x => (f ^1 (fn y => y ^2)))，我们用f表示。

对fn和fun f结构的处理主要是将函数转化为返回值形式作为参数实现控制流分析，也就是将操作当作参数。

let in结构则处理成控制流程图的形式：由于fun f 我们以f作为返回值，所以原结构变成 let g = f ^5 in (g ^6 (fn z => z ^7) ^8) ^9。而g = f ^5则是in部分的处理方式，我们记录g与f的转化关系记为bind[g -> f]。后续in部分g ^6由于g与f的转化关系我们将原结构处理成(f ^6 (fn z => z ^7) ^8) ^9。最后将fn z记为 id _z。

最终的表达方式是bind[g -> f] in (f ^6 id_z ^8) ^9。也就是先进行f操作再进行z操作得到的最终结果：(bind [ g -> f] in (bind [ f-> f] [x -> id_z] in (f ^1(fn y => y ^2) ^3) ^4) ^9) ^10)

由于上述例子处于递归循环结构当中，我们要进行一定的处理，在这个处理过程中，我们不改变g和f的对应关系，也不改变z的操作，只是在函数循环过程中多次执行y操作实现循环，也就是(bind [ g -> f] in (bind [ f-> f] [x -> id_z] in (bind [ f-> f] [x -> id_y] (f ^1(fn y => y ^2) ^3) ^4) ^4) ^9) ^10)

语义正确Semantic Correctness

我们要证明控制流分析的语义是正确的，首先我们证明过程间的操作语义是合理的：也就是要证明close t in p是合理的，即一个函数抽象t使用的参数一定包含于p中。除此之外，我们还要保证 t 的子语句中的ie一定是小于母语句中的ie的。这一点的证明我们只需要说明对于每一次调用都只使用本地环境，即任意参数被调用都在本地环境中存在，同时由于只使用本地环境，随着语句的不断更细的分析，ie一定是递减的。

所以对于语义分析，存在一定条件使得上述等式成立：

对于x -> v一定满足x在参数表p中，v一定在参数表p的x的可能性中。

对于 fn x => e_0 -> close(fn x => e_0) in p_0 一定满足 p_0包含于p中，且 fn x => e_0为待定量。fun f 同理

对于语句ie_1 ie_2 -> ie'_1 ie_2一定满足ie_1 -> ie'\_1

因此我们做出定义：p和关于p的操作满足包含关系的情况下 ie -> ie' 如果关于代码的结果包含于ie中，那么结果一定也包含于ie‘中，也就是对于一个环境变量更精确的条件，执行结果更精确。也就是说对于控制流分析存在一个最小的最优解。

我们如何判断当前结果为最小最优解。这就用到了完全格，摩尔集的知识，这些知识在前面的文章都已经提到了，在这里简单描述。

一个完全格的子集任意元素基于完全格规则的衍生元素依旧包含于当前子集，该子集为摩尔集。

那么我们只要证明{(C,p) | (C,p) |= ie}的集合Y包含所有满足条件的元素即可。

根据 p(x) = close t_x in p_x需要满足t_x 属于 p(x) 并且 p_x 和 p满足关系。由于控制流分析结构满足单调递减的规则。所以t_x 属于 最小p(x) 并且 p_x 和 最小p满足关系。所以当p属于全部环境变量，{p' | p' R p}的集合是摩尔集。

所以对于{(C,p) | (C,p) |= ie}，由于在程序过程中的任意的 i 满足(C_i,p_i) |= ie 所以{(C,p) | (C,p) |= ie}是摩尔集。

最小不动点和最大不动点

在上面的分析中，我们选取的 |= 关系是寻找最大不动点，也就是向最小单元分析包含其环境变量。接下来我们改变其关系为寻找最小不动点，也就是向最大单元分析。来证明我们确实需要利用最大不动点构造摩尔集使得分析成立。

由于我们改变了|=的定义，所以分析方法要重新定义。

e = t ^l

t = (fn x => (x ^l x ^l) ^l) ^l (fn x => (x ^l x ^l) ^l) ^l

lab = {l}

var = {x}

term = {t , fn x => (x ^l x ^l) ^l ,x ^l x ^l ,x}

IEXP = {t ^l | t ∈ Term}

val = P({fn x => (x ^l x ^l) ^l}) = {空集 , {fn x => (x ^l x ^l) ^l }}

和之前一样，我们通过(C,p) |= t来证明最小不动点的{(C,p) | (C,p) |= ie}不是摩尔集

我们先对各种情况满足的条件进行罗列。

对于(C,p) |= x ^l 需要满足 p(x) 包含于 C(l)

(C,p) |= fn x => (x ^l x ^l) ^l 需要满足 {fn x => (x ^l x ^l) ^l} 包含于 C(l)

(C,p) |= (x ^l x ^l) ^l 需要满足 (C,p) |= x ^l 的条件，且如果C(l)不为空，需要满足(C,p) |= (x ^l x ^l) ^l的条件 C(l) = p(x)

也就是说(C,p) 和 (x ^l x ^l) ^l 的关系有三种情况，C(l) = p(x) = 空 ，C(l) = p(x) 不等于空 ， 不成立。

由于摩尔集不能为空，所以当出现第二种情况时，最小不动点的{(C,p) | (C,p) |= ie}不是摩尔集。