\newcommand{\mt}[1]{\text{#1}} \newcommand{\mE}{\mathcal{E}} \newcommand{\tup}[1]{\left<{#1}\right>}

环境类似于其他语言（C++、JAVA等）的“符号表”。 所谓符号表，是一张将变量名与变量代表的内容联系起来的一张表。 不过这里我们抛弃符号表的观点，单纯地从算法角度上引入环境这一概念。

引入环境

通过修改解释器求值过程的算法，可以很自然的引入环境这个概念。

在前面基于文本替换的解释器里可以看到，所谓的“计算”，其实不过是一堆符号根据某种规则替换来替换去最终得到一个不能再归约的结果的过程。 这个替换过程需要遍历表达式。 比如计算表达式(\lambda X.M \; V)(λX.MV)<script id="MathJax-Element-2" type="math/tex">(\lambda X.M \; V)</script>，需要进行替换M[X \leftarrow V]M[X←V]<script id="MathJax-Element-3" type="math/tex">M[X \leftarrow V]</script>。 这个替换过程需要遍历表达式MM<script id="MathJax-Element-4" type="math/tex">M</script>。 而求值过程本身也需要遍历表达式MM<script id="MathJax-Element-5" type="math/tex">M</script>。 这样就至少需要遍历两次表达式MM<script id="MathJax-Element-6" type="math/tex">M</script>。 另外，替换过程本身也很麻烦，其中有这么一条规则： \begin{equation*}\begin{array}{lcl}   (\lambda X_1.M)[X_2 \leftarrow N] &=& (\lambda X_3.M[X_1 \leftarrow X_3][X_2 \leftarrow N]) \\   &&   \begin{array}{ll}     \text{其中} & X_1 \neq X_2, X_3 \notin FV(N), \\     & X_3 \notin FV(M)\backslash\{X_1\}   \end{array} \end{array}\end{equation*}

  (λX1.M)[X2←N]  =(λX3.M[X1←X3][X2←N])      其中    X1≠X2,X3?FV(N),X3?FV(M)?{X1}  

M

这样一来，在原来的算法里，由于直接使用替换，计算一个表达式需要一遍遍地遍历这个表达式的子表达式们。 这是一个效率很低的方法。 为了避免这些多余的遍历过程，我们可以延后替换过程，等到遍历到需要替换的变量时再对这个变量做替换。 这样只需要一次遍历就够了。 为了延后替换过程，需要一个保存这些“延后的替换”的数据结构。 这个数据结构叫做环境。 我们用字母\mE<script id="MathJax-Element-9" type="math/tex">\mE</script>表示环境。

下面举个例子来粗略地说明如何用环境来进行计算（粗略的展示，不代表实际的计算步骤）： \begin{equation*}\begin{array}{lcl}   && (\underline{(\lambda x.\lambda y.(+ \; x \; y) \; 11)} \; 22) \\   &\rightarrow& \underline{(\tup{\lambda y.(+ \; x \; y), \tup{(x \leftarrow 11)}} \; 22)} \\   &\rightarrow& \underline{\tup{(+ \; x \; y), \tup{(y \leftarrow 22), (x \leftarrow 11)}}} \\   &\rightarrow& \tup{\underline{(+ \; 11 \; 22)}, \tup{(y \leftarrow 22), (x \leftarrow 11)}} \\   &\rightarrow& \tup{\underline{33}, \tup{(y \leftarrow 22), (x \leftarrow 11)}} \\   &\rightarrow& 33 \end{array}\end{equation*}

引入环境后，一个表达式就可能不是一个“完整的表达式”了。 因为这个表达式可能有些自由变量应该被替换，只是替换被延后了，所以它看起来仍保持还没被替换的样子。 所以，一个“完整的表达式”，应该包括表达式和“延后的替换”的信息——也就是环境。 表达式和环境这个二元组叫做闭包，记为\tup{M, \mE}<script id="MathJax-Element-11" type="math/tex">\tup{M, \mE}</script>。

我一直故意没有描述环境的具体定义。 有了闭包这个概念后，现在可以说说环境的定义了。 从用途上看，环境可以理解成一个函数，它的输入是一个变量，它的输出是这个变量应该被替换成的东西。 这个“被替换成的东西”是什么东西呢？ 一个直接的想法是表达式。 但这是不正确的！ 因为一个表达式可能不是一个“完整的表达式”。 所以这个“被替换成的东西”应该是一个闭包。 也就是说，环境是一个将变量映射成闭包的函数： \mE: X \rightarrow \tup{M, \mE}

构造环境

考虑表达式(\mt{let} \; a \; 1 \; (\mt{let} \; a \; 2 \; a))<script id="MathJax-Element-13" type="math/tex">(\mt{let} \; a \; 1 \; (\mt{let} \; a \; 2 \; a))</script>。 这个表达式共有两次替换，第一次将变量a<script id="MathJax-Element-14" type="math/tex">a</script>替换成1<script id="MathJax-Element-15" type="math/tex">1</script>，第二次将变量a<script id="MathJax-Element-16" type="math/tex">a</script>替换成2<script id="MathJax-Element-17" type="math/tex">2</script>，而表达式最终的值是2<script id="MathJax-Element-18" type="math/tex">2</script>。 可以看到，当遇到同名变量时，后替换的变量有效。 用于保存替换信息的环境应该具有后进入先找到（栈！）的性质。 环境可以用链表的形式保存。 每次保存替换信息时，将要替换的变量和应该替换成的闭包插入到链表的头部； 而查找是从头部开始查找。

构造环境的方法如下面公式所示： \begin{equation*}\begin{array}{lcl}   \mE &=& \mt{empty-env} \\       &|& \tup{\mt{extend-env}, \mE, X, \tup{M, \mE‘}} \end{array}\end{equation*}

当输入变量X<script id="MathJax-Element-28" type="math/tex">X</script>时，从链表的头部开始搜索，返回第一次找到变量X<script id="MathJax-Element-29" type="math/tex">X</script>时对应的闭包。 用\mE(X)<script id="MathJax-Element-30" type="math/tex">\mE(X)</script>表示在环境\mE<script id="MathJax-Element-31" type="math/tex">\mE</script>中查找X<script id="MathJax-Element-32" type="math/tex">X</script>的过程，这个过程如下： \begin{equation*}\begin{array}{lcl}   \mt{empty-env}(X) &=& \tup{X, \mt{empty-env}} \\   \tup{\mt{extend-env}, \mE, X, \tup{M, \mE‘}}(X) &=& \tup{M, \mE‘} \\   \tup{\mt{extend-env}, \mE, X‘, \tup{M, \mE‘}}(X) &=& \mE(X) \\   && \text{其中} X‘ \neq X \end{array}\end{equation*}

CEK machine

还记得CK machine吗？ CEK machine指的是加入环境后的CK machine。

为了简化问题，暂时先不考虑递归表达式(\mt{fix} \; X_1 \; X_2 \; M)<script id="MathJax-Element-34" type="math/tex">(\mt{fix} \; X_1 \; X_2 \; M)</script>。 无fix表达式的Alligator的语法（我真的没在凑字数）： \begin{equation*}\begin{array}{lcl}   M, N, L &=& X \\           &|& b \\           &|& \lambda X.M \\           &|& (+ \; M \; N) \\           &|& (- \; M \; N) \\           &|& (\mt{iszero} \; M) \\           &|& (M \; N) \\ \end{array}\end{equation*}

CEK machine的求值过程从CK machine的求值过程稍微改改得到。 无fix表达式的Alligator的语法中只有函数调用(M \; N)<script id="MathJax-Element-36" type="math/tex">(M \; N)</script>会用到替换。 现在我们不使用替换，取而代之的是扩展环境。 其他的改动还有：原来的表达式M<script id="MathJax-Element-37" type="math/tex">M</script>改成闭包\tup{M, \mE}<script id="MathJax-Element-38" type="math/tex">\tup{M, \mE}</script>； 而变量X<script id="MathJax-Element-39" type="math/tex">X</script>现在要到环境查找对应的闭包\mE(X)<script id="MathJax-Element-40" type="math/tex">\mE(X)</script>。 另外，Alligator使用call-by-value的调用顺序，所以要求环境值域的闭包里的表达式是一个值。 也就是说，CEK machine里用到的环境应该是这样的函数： \mE: X \rightarrow \tup{V, \mE}

递归的处理

fix表达式的求值过程需要特别的处理。 按照上面的技巧修改fix表达式的求值过程，这个求值过程有如下形式： \tup{\tup{(\mt{fix} \; X_1 \; X_2 \; M), \mE}, \kappa}_v \rightarrow_v   \tup{\tup{\lambda X_2.M, \mE^{fix}}, \kappa}_c

增加了构造环境方法后，fix表达式的求值过程如下： \tup{\tup{(\mt{fix} \; X_1 \; X_2 \; M), \mE}, \kappa}_v \rightarrow_v   \tup{\tup{\lambda X_2.M, \tup{\mt{extendrec-env}, \mE, X_1, X_2, M}}, \kappa}_c

代码实现

写代码咯，首先，用Racket的结构来表示闭包：

环境的代码，同样用结构来表示环境：

函数\mt{apply-env}<script id="MathJax-Element-58" type="math/tex">\mt{apply-env}</script>是在环境中查找变量的过程：

最后是求值过程的代码：

简化CEK machine

CEK machine里环境的值域只有三种类型的闭包： 包含变量的闭包\tup{X, \mt{empty-env}}<script id="MathJax-Element-59" type="math/tex">\tup{X, \mt{empty-env}}</script>、 包含常数的闭包\tup{b, \mE}<script id="MathJax-Element-60" type="math/tex">\tup{b, \mE}</script> 以及包含函数的闭包\tup{\lambda X.M, \mE}<script id="MathJax-Element-61" type="math/tex">\tup{\lambda X.M, \mE}</script>。 这三种闭包只有函数的情况需要环境。 而变量和常数的情况下不需要环境。 修改值类型为： \begin{equation*}\begin{array}{lcl}   V &=& X \\     &|& b \\     &|& \tup{\lambda X.M, \mE} \end{array}\end{equation*}

修改环境的定义，将环境的定义改为变量到值的映射： \mE: X \rightarrow V

思考

1. 用函数表示环境。
2. 关于递归的处理，\mt{extendrec-env}<script id="MathJax-Element-66" type="math/tex">\mt{extendrec-env}</script> 的扩展方式可能看起来有点违和感。 使用带有“副作用”的方法可以避免这种扩展方式的使用。修改环境为带有存储的环境（方括号表示这个是一个引用，这个引用指向的存储里的值是V<script id="MathJax-Element-67" type="math/tex">V</script> ）： \begin{equation*}\begin{array}{lcl}   \mE &=& \mt{empty-env} \\       &|& \tup{\mt{extend-env}, \mE, X, [V]} \end{array}\end{equation*}
   <script id="MathJax-Element-68" type="math/tex; mode=display">\begin{equation*}\begin{array}{lcl} \mE &=& \mt{empty-env} \\ &|& \tup{\mt{extend-env}, \mE, X, [V]} \end{array}\end{equation*}</script> 另外增加一个修改存储的方法(\mt{set-value-env!} \; \mE \; V‘)<script id="MathJax-Element-69" type="math/tex">(\mt{set-value-env!} \; \mE \; V‘)</script> ， 其中这里的\mE=\tup{\mt{extend-env}, \mE, X, [V]}<script id="MathJax-Element-70" type="math/tex">\mE=\tup{\mt{extend-env}, \mE, X, [V]}</script> 。 这个方法修改环境\mE<script id="MathJax-Element-71" type="math/tex">\mE</script> 为\tup{\mt{extend-env}, \mE, X, [V‘]}<script id="MathJax-Element-72" type="math/tex">\tup{\mt{extend-env}, \mE, X, [V‘]}</script> 。为了计算fix表达式(\mt{fix} \; X_1 \; X_2 \; M)<script id="MathJax-Element-73" type="math/tex">(\mt{fix} \; X_1 \; X_2 \; M)</script> 扩展的环境\mE^{fix}<script id="MathJax-Element-74" type="math/tex">\mE^{fix}</script> ， 先将X_1<script id="MathJax-Element-75" type="math/tex">X_1</script> 绑定到一个未初始化的值： \mE^{fix} = \tup{\mt{extend-env}, \mE, X_1, [uninitialized]}
   <script id="MathJax-Element-76" type="math/tex; mode=display"> \mE^{fix} = \tup{\mt{extend-env}, \mE, X_1, [uninitialized]} </script> 其中uninitialized<script id="MathJax-Element-77" type="math/tex">uninitialized</script> 表示未初始化。 然后修改\mE^{fix}<script id="MathJax-Element-78" type="math/tex">\mE^{fix}</script> ： (\mt{set-value-env!} \; \mE^{fix} \; \tup{\lambda X_2.M, \mE^{fix}})
   <script id="MathJax-Element-79" type="math/tex; mode=display"> (\mt{set-value-env!} \; \mE^{fix} \; \tup{\lambda X_2.M, \mE^{fix}}) </script> 这样就能得了\mE^{fix}<script id="MathJax-Element-80" type="math/tex">\mE^{fix}</script> 。
3. 这是一个算法练习。 在一些代码分析过程中，知道代码中所有变量的使用次数是很有用的。 我们希望统计所有变量的使用次数，并标记在变量声明的位置。 例如输入一段代码：
   ?

   1 2 3 4 5 6 7

   (((lambda x     (lambda y       (+ ((lambda x x)           33)          (+ y (+ x x)))))    11)  22)

   输出： 
   ?

   1 2 3 4 5 6 7

   (((lambda (x 2)     (lambda (y 1)       (+ ((lambda (x 1) x)           33)          (+ y (+ x x)))))   11)  22)

   如何实现这个算法？要求只遍历代码一次。