Skip to content

PCF 的归约和符号解释程序

:material-circle-edit-outline: 约 605 个字 :material-clock-time-two-outline: 预计阅读时间 2 分钟

12 PCF 的归约.pdf 编程语言原理（本）2024-12-04 第 7-8 节

不确定性规约

PCF 的规约是不确定的，但是规约流程可以不同

PCF 规约是汇聚的，路径不同但结果是一定一样

image-20241228203717580

  • 单个箭头是指 单步规约
  • 双箭头是指 0 次 或 2 次及以上，反正不是 1 次
    • \(\alpha\) 规约（换名）并不是规约，就得用双箭头
  • 加一个斜杠意思是这个箭头是不成立的

image-20241228203439065

规约或停机

任意 PCF 项最多只有 ⼀ 个范式

例题 1

image-20241228204422030

image-20241228204426520

例题 2

image-20241228204433423

image-20241228204439518

例题 3

image-20241228204506983

例题 4

image-20241228204529565

看 PPT 吧，12 PCF 的归约.pdf 13 页

PCF 是从左往右规约

例题 1

image-20241228205137254

image-20241228205142056

image-20241228205149308

例题 2

image-20241228205156992

12 PCF 的归约.pdf 24 页

PCF 的规约策略

⼀ 个归约策略是某个规约的路径

PCF ⼀ 个重要的性质是: 能以 ⼀ 种有效的 ⽅ 式确定地实现理想化的不确定性解释程序

更明确地说，存在 ⼀ 种有效可计算的归约策略 F，使得只要 M 归约到范式 N，就有 \(eval_F(M)=N\)

这种归约策略称为最左优先归约，或简称为最左优先归约

image-20241228205650016

最左优先归约

image-20241228205708410

例题 1

image-20241228205752847

12 PCF 的归约.pdf 37 页

例题 2

image-20241228205827491

12 PCF 的归约.pdf 43 页

懒归约（Lazy Evaluation / Reduction）

懒归约 的基本思想是，只有当 ⼀ 个表达式的结果真的需要时，才会进 ⾏ 计算

懒归约并不 ⽴ 即 求值函数应 ⽤ 中的参数，⽽ 是仅在必要时才“触发”求值

这种策略与最左优先归约不 同，它并不是按顺序逐步归约所有部分，⽽ 是推迟某些部分的求值

在懒归约中，函数的参数通常不会 ⽴ 即被求值，⽽ 是会“保持未求值状态”，直到需要其 值时才进 ⾏ 计算

例题 1

image-20241228210038786

12 PCF 的归约.pdf 46 页

懒归约的核 ⼼ 在于，它推迟了计算，直到表达式的值确实被需要时才进 ⾏ 求值。

与此相 反，最左优先归约会 ⽴ 即对最左侧的表达式进 ⾏ 归约。

积极规约

积极归约中，⼀ 个重要的思想就是值的概念，值就是不能通过积极归约进 ⼀ 步归约的项

image-20241228210739728

12 PCF 的归约.pdf 55 页

这节课前面有一些规约的例题：编程语言原理（本）2024-12-11 第 7-8 节