第3章 控制流分析 内容概述 -定义一个函数式编程语言，变量可以指称函数 以dynamic dispatch problemi为例（作为参数的 函数被调用时，究竟执行的是哪个函数) 规范该控制流分析问题，定义什么是可接受的控 制流分析 -定义可接受分析在语义模型上的可靠性 一讨论分析算法（语法制导、集合约束求解） -加上数据流分析 -加上上下文信息
第3章 控制流分析 • 内容概述 – 定义一个函数式编程语言，变量可以指称函数 – 以dynamic dispatch problem为例（作为参数的 函数被调用时，究竟执行的是哪个函数） – 规范该控制流分析问题，定义什么是可接受的控 制流分析 – 定义可接受分析在语义模型上的可靠性 – 讨论分析算法（语法制导、集合约束求解） – 加上数据流分析 – 加上上下文信息
第3章 控制流分析 函数的不动点 若x)=x,则x是函数f的不动点 -求解含函数变量f的方程 f=An.if n=0 then 1 else n x fn -1)end 看成找下面函数的不动点 F 入f入n.ifn=0then1 else n×fn-1)end F(阶乘函数)=阶乘函数 该函数只有唯一的不动点 阶乘函数
第3章 控制流分析 • 函数的不动点 – 若f(x) = x，则x是函数f 的不动点 – 求解含函数变量f 的方程 f = n. if n=0 then 1 else n f(n − 1) end – 看成找下面函数的不动点 F f. n. if n=0 then 1 else n f(n − 1) end F(阶乘函数) = 阶乘函数 – 该函数只有唯一的不动点 阶乘函数
第3章 控制流分析 函数的最小不动点 求解含函数变量f的方程 f=入n.ifn=0then1 else if n 1 then f3) else fn -2)end 一相应高阶函数有无数个不动点 当n是偶数时，结果是1 当n是奇数时，结果是a(a可以任取) 最小不动点 n为偶数时，结果是1；n为奇数时，结果未定义
第3章 控制流分析 • 函数的最小不动点 – 求解含函数变量f 的方程 f = n. if n=0 then 1 else if n = 1 then f(3) else f(n − 2) end – 相应高阶函数有无数个不动点 当n是偶数时，结果是1 当n是奇数时，结果是a（ a可以任取 ） – 最小不动点 n为偶数时, 结果是1; n为奇数时, 结果未定义
第3章 控制流分析 函数最小不动点的计算 -例：F 入fn.ifn=0then1 else n×fn-1) end -lfp(F)= FnL)(n=0,1,…) -0(L)=⊥（表示处处无定义的函数） -F1(L)=F(L) =(入fn.ifn=0then1 else n×fn-l)end)L =入n.ifn=0then1 else n×L(n-l)end ={K0,0)
第3章 控制流分析 • 函数最小不动点的计算 – 例：F f. n. if n=0 then 1 else n f(n − 1) end – lfp(F) = Fn (⊥) (n = 0, 1, …) – F0 (⊥) = ⊥ (表示处处无定义的函数) – F1 (⊥) = F(F0 (⊥)) = ( f. n. if n = 0 then 1 else n f(n − 1) end ) ⊥ = n. if n = 0 then 1 else n ⊥(n − 1) end = {0, 0!}
第3章 控制流分析 函数最小不动点的计算 -例：F 入f入n.ifn=0then1 else n×fn-l)〉 end -lfp(F)= Fm(L)(n=0,1,… -F2(L=F(F(L =(入f入n.ifn=0then1 else n×n-l)end)F(L) =入n.ifn=0then1 else n×F(L)(n-l)end ={K0,0),〈1,1} 依次逐步计算可得：⊥，{K0,0)},{《0,0),〈1,1}， {K0,0),〈1,1，〈2,2}，.（构成一个上升链
第3章 控制流分析 • 函数最小不动点的计算 – 例：F f. n. if n=0 then 1 else n f(n − 1) end – lfp(F) = Fn (⊥) (n = 0, 1, …) – F2 (⊥) = F(F1 (⊥)) =( f. n. if n=0 then 1 else n f(n −1)end)F1 (⊥) =n. if n = 0 then 1 else n F1 (⊥) (n − 1) end = {0, 0!, 1, 1!} – 依次逐步计算可得：⊥,{0, 0!}, {0, 0!, 1, 1!}, {0, 0!, 1, 1!, 2, 2!}, … (构成一个上升链) – lfp(F) = Fn (⊥) = {0, 0!, 1, 1!, 2, 2!, …}
第3章 控制流分析 。Tarski定理 令F:P(U)→P(U)是单调函数 其中U是集合，P(U)表示U的幂集 集合XSU是F封闭的 当且仅当F)SX 集合XSU是F致密的 当且仅当XsF) -定义X.F)和vX.F X.F)= XFXX vX.F(X)= XIX≤FX)}
第3章 控制流分析 • Tarski定理 – 令F : P(U) → P(U)是单调函数 其中U是集合，P(U)表示U的幂集 – 集合XU是F封闭的 当且仅当F(X) X – 集合XU是F致密的 当且仅当X F(X) – 定义X.F(X)和X.F(X) X.F(X) = {X | F(X) X} X.F(X) = {X | X F(X)}
第3章 控制流分析 。Tarski定理 -集合XcU是F封闭的 当且仅当F)二X 集合XSV是F致密的 当且仅当XsFX 定义X.FX)和vX.FX LX.F(X)= XFXEX vX.F(X)= XXE FX 引理 XF)是最小的F封闭集合 vX.F)是最大的F致密集合
第3章 控制流分析 • Tarski定理 – 集合XU是F封闭的 当且仅当F(X) X – 集合XU是F致密的 当且仅当X F(X) – 定义X.F(X)和X.F(X) X.F(X) = {X | F(X) X} X.F(X) = {X | X F(X)} – 引理 X.F(X)是最小的F封闭集合 X.F(X)是最大的F致密集合
第3章 控制流分析 ·Tarski定理 根据对偶性，只证明一种情况。首先证明引理： vX.F(X)= {XXEFX)}是最大F致密集合 一最大是明显的 证明每个X都致密，则 :X也F致密则可 因为对每个有XSFX),则：X;s:FX 因为F单调，则对每个有FX)SF(:X) 由此可得F)c(:X) 由传递性， X,SF(X),即：X是F致密 的
第3章 控制流分析 • Tarski定理 根据对偶性，只证明一种情况。首先证明引理： X.F(X) = {X | X F(X)}是最大F致密集合 – 最大是明显的 – 证明每个Xi都F致密，则 iXi也F致密则可 因为对每个i有Xi F(Xi )，则 i Xi i F(Xi ) 因为F单调，则对每个i有F(Xi ) F( i Xi ) 由此可得 iF(Xi ) F( i Xi ) 由传递性， iXi F( i Xi )，即 iXi是F致密 的
第3章 控制流分析 ·Tarski定理 再证明本定理（仍只证明一种情况）： 1、XF)是F的最小不动点 2、X.F)是F的最大不动点 令y=X.FX,则y是致密的，v∈F() 由单调性，F()sF(F(),则F(y)也致密 -由v的定义知道F()sv 由v和F()之间的这两个不等式得y=F(y) 不动点都是致密的，因而都包含在中，所以y是 最大不动点
第3章 控制流分析 • Tarski定理 再证明本定理（仍只证明 一种情况）： 1、X.F(X)是F的最小不动点 2、X.F(X)是F的最大不动点 – 令 = X.F(X)，则是致密的， F() – 由单调性，F() F(F())，则F()也致密 – 由的定义知道F() – 由和F()之间的这两个不等式得 = F() – 不动点都是致密的，因而都包含在中，所以是 最大不动点
第3章 控制流分析 归纳和余归纳(coinduction) 归纳法 -初始条件、迭代规则、最小化条件 字母表A上的串集A*归纳定义如下 (1)ε∈A*;(2)若a∈A且x∈A*,则ax∈A*;3)除此以 外，A*不含其它元素 余归纳法 迭代规则（循环条件），最大化条件 -流可以通过余归纳法来定义 (1)若t是A上的流且a∈A,则(a,t)也是A上的流； (②)A上的流集是满足上述规则的最大集合
第3章 控制流分析 • 归纳和余归纳(coinduction) 归纳法 – 初始条件、迭代规则、最小化条件 – 字母表A上的串集A归纳定义如下 (1) A ; (2)若aA且xA , 则axA ;(3)除此以 外， A不含其它元素 余归纳法 – 迭代规则(循环条件)，最大化条件 – 流可以通过余归纳法来定义 (1) 若t是A上的流且aA，则(a,t)也是A上的流； (2) A上的流集是满足上述规则的最大集合
