背景

为了更好的理解后续内容，我们需要理解如下内容。

我们总结一下就是：

1. lambda abstraction：表示函数，形式就是$\lambda X.E$，X是变量，E是表达式，是对X应用的表达式
2. lambda application：是函数的应用，E1 E2，就是将E2应用到E1这个lambda抽象

(本章节的内容看不懂应该问题不大！其本意是通过$\lambda$ 演算的数学方式来介绍 调用图分析的理论基础）

    控制流分析在其最纯粹的形式下最好可以通过经典的 λ-演算（lambda calculus）来进行阐释。演算的抽象语法定义如下：

在第10.3节中，我们在TIP语言上演示了这种分析技术。具体的语法也允许括号。为简单起见，我们假设所有λ-绑定的变量都是不同的。为了构建这种演算中术语的控制流图（CFG），我们需要近似地确定每个表达式E可能求值的闭包集合。闭包可以由类似λX的符号来表示，它标识了一个具体的λ-抽象。这个问题被称为闭包分析，可以使用第4章和第5章中的技术来解决。然而，由于这种语言中的过程内控制流非常简单，因此我们可以直接在AST上执行分析。

    对于每一个AST节点v，我们引入一个约束变量[[v]]表示闭包集合的结果（也就是v这个节点，可能的函数调动的集合）。对于一个抽象$\\lambda X.E$，我们有如下约束：其含义是这个点的函数调用可能就是它自己

对于一个应用$E_1 ~ E_2$（注意有空格），那么对于每一个抽象$\lambda X.E$，我们有如下条件约束

其含义说明，（如果函数$\lambda X$是E1这个表达式应用的函数之一，那么）实参E2可能流入形参X，并且函数体E应该是这个函数调用E1 E2的可能结果之一。（这里面参数和返回值的包含关系式不同的！很奇怪）

    举个例子，带有7个函数抽象（7个函数）和3个应用（3个函数调用）的一个小程序：

$$ (\lambda s.\lambda z.sz)(\lambda n.\lambda t.\lambda e.e)(\lambda r.\lambda p.r) $$

$$ (_2(_1\lambda s.\lambda z.s ~ z)_1(\lambda n.\lambda t.\lambda e.e))_2(\lambda r.\lambda p.r) $$