静态与动态语义

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

5 静态和动态语义.pdf 编程语言原理（本）2024-10-16第7-8节

E 语言语法表（syntax chart）

类型系统

类型系统的作用是对短语（phrase）的形成加以约束，使得短语上下文敏感

例如，表达式 plus(x; num[n]) 是否合理，要去上下文检查 x 类型是否是 num

E 语言的静态语义

E 的静态语义由如下形式的泛型假言判断的归纳定义组成：

$\vec{x}$ 是变量组成的向量，

$\Tau$ 是定型上下文，是类型组成的向量

$\vec{x}|\Tau $ 即，给每个变量确定其类型，这就是一个上下文（目前定义了什么变量，都是什么类型的）

基于这个上下文，我们可以推导表达式 $e$ 的类型是 $\tau$

E 的静态语义规则

P29 的 4.1a⾄4.1h

引理

类型唯⼀性（unicity of typing），表达式的类型是唯一的
定型反转（inversion for typing），废话
- 规则运用： plus 我们能确定其参数和输出均为 num 类型
弱化（weakening），根据 $\Tau$ 我们能确定 e 类型，那根据 $\Tau,x$ 依旧能确定
- $x$ 不属于 $\Tau$，且类型与 $e$ 一致
- 表达式结果与变量一致，则可将变量换成表达式
- 即，$\beta$ 代换不改类型
- 可将表达式换成变量

语言的结构

引入（introduction）：确定类型的值或范式（canonical form）
消去（elimination）：确定如何操作该类型的值以形成另⼀种类型的计算

[!EXAMPLE]

在 E 语言中，num 类型的引入形式是 num，消去形式是 plus 和 times

前者使得这种类型的变量更多，后者使得这种类型的变量更少

动态语义

转换系统

一个无法转换的状态是 stuck 的

所有的终结状态都是卡住的，但也可能存在卡住的非终结状态

一个转换系统是确定性的，如果每个状态最多只有一条出路，不用选择

类比计算模型的确定性与非确定性

转换序列

结构化动态语义

P34 5.4a⾄5.4g

[!EXAMPLE]

即，改了类型后输出也会相应的改变类型

需要 $e_1$ 已经被化简为值了，才能开始化简第二个参数 e_2

[!EXAMPLE]
let(plus(num[1];num[2]);x.plus(plus(x;num[3]);num[4])) 
牢记规则中的条件是需要严格遵守的，例如上面的 $e_1val$

先用规则 5.4g，进行 let 运算

引理

值的终结性（finality of values），值无法再转换（化简）
确定性（determinacy），同一个表达式推出的任何东西都是 $\alpha$ 等价的