文章目录
1.5 上下文中的赋值
如何减少表达式 ((f • t) • f) ？根据 r 关系或者 ↝↝r 关系，这个表达式并不能规约！
直观上看，通过将第一个子表达式根据 (f • t) r t 的规则， ((f • t) • f) 应该被规约到 (t•f) 。但是在r关系的定义中，没有一项是满足 ((f • t) • f) 的。我们只能将类似于 (f • B) 或 (t • B) 格式的表达式规约。换句话说，在 • 右边的表达式是任意的，但是在左边的表达式必须是 f 或者 t 。
现在我们将 r关系 用 -->r 扩张，从而支持子表达式的规约：
–>r 关系被称为 r关系 的 兼容闭合（compatible closure）译者注：从这篇开始，我找到了一个更合适的词“闭合”来翻译closure，以及更合适的词“规约”来翻译reduction
和r一样， -->r 是一个单步规约的关系，但是它允许任何一个子表达式自身规约。用r关系规约后的子表达式被称为 redex ，包裹redex的文本被称为上下文（context）。
–>r 关系包括 ((f • t) • f) -->r (t • f) ，我们可以用下述的证明树来演示这条结论。
并且，继续规约这个表达式，我们最终可以得到 t ：
最后，如果我们定义 ->->r 作为 –>r 的自反-传递闭合，我们可以得到 ((f • t) • f) ->->r t，因此，->->r 是由r生成的自然规约关系（natural reduction relation）。
总结：
单纯的自反闭合 ≍r，等价闭合 ≈r，或是自反-传递闭合 ↝↝r 关系将是无趣的。相反，我们最近感兴趣的将会是兼容闭合 -->r 和它的自反-传递闭合 ->->r ， 因为他们对应了典型的赋值概念。另外，–>r 的等价闭合 =r 关联了会产生相同结果的表达式，因此它也很有趣。
练习 1.3
请你解释为什么 (f • ((t • f) • f)) !↝↝r** r t** .
题解：
(f • ((t • f) • f)) r ((t • f) • f) 无法继续规约。
练习 1.4
请你用 -->r 进行规约，证明 (f • ((t • f) • f)) →→r t
题解：
(f • ((t • f) • f)) -->r ((t • f) • f) -->r (t • f) -->r t
1.6 赋值函数
→→r 将我们与赋值的概念拉得更近了。由于 ((f • t) • f) →→r t，我们发现 ((f • t) • f)→→r (t • f) 以及 ((f • t) • f)→→r ((f • t) • f) 同样成立。
在赋值中，我们感兴趣的是 B表达式 到底是 f 还是 t ，任何其他的映射关系都是无关紧要的。为了捕捉到这种赋值的概念，我们将 evalr 关系定义如下：
这里，我们使用了另一个符号来定义关系，这个特殊的符号是具有暗示性的函数的一种关系，即把每一个元素最多映射到一个元素的关系。我们使用函数表示法，因为 evalr 必须是一个函数，才能让它作为一个求值器而有意义。
练习 1.5
在这些关系中：哪一个是函数？在非函数关系中，找到它关联的两个表达式。
题解：
r 和 evalr 是函数。
- ≍r 不是函数
(t • B1) ≍r B1
(t • B1) ≍r (t • B1)
- ≈r 不是函数
(t • B1) ≈r B1
(t • B1) ≈r (t • B1)
- ↝↝r 不是函数
(t • B1) ↝↝r (t • B1)
(t • B1) ↝↝r t
- →r 不是函数
((t • B1) • (t • B1)) →r (t • (t • B1))
((t • B1) • (t • B1)) →r ((t • B1) • t)
- →→r 不是函数
(t • B1) ↠r (t • B1)
(t • B1) ↠r t
- =r 不是函数
(t • B1) =r (t • B1)
(t • B1) =r t
1.7 符号摘要
| 名字 | 定义 | 直观定义 |
|---|---|---|
| _ | 表达式语法成员的基础关系 | 一个单步的没有上下文的规约步骤 |
| →_ | _ 关系 关于表达式语法的兼容闭合关系 | 上下文中的单步 |
| →→_ | →_关系 的自反-传递闭合 | 多数赋值步骤（0或多） |
| =_ | →→_关系 的对称-传递闭合 | 产出相同结果的同等表达式 |
| eval_ | =_关系 严格限定结果的范围 | 全面完整的赋值函数 |
第一章 完