标签：关系 1.5 1.7 函数 规约 Programming B1 表达式 赋值
文章目录
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_ | =_关系 严格限定结果的范围 | 全面完整的赋值函数 |
第一章 完
标签：关系,1.5,1.7,函数,规约,Programming,B1,表达式,赋值 来源： https://blog.csdn.net/qq_35714301/article/details/113777330
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。