用户: Ice1000/CMU 特有 PL 记号

在 CMU, 你会学到很多难以和非 CMU 的讨论环境兼容的术语和记号. 本文记录一些这样的符号.

本文目前还在建设中!

1术语

•	Dynamics 的意思是操作语义 (Operational semantics)
•	Statics 的意思是用于描述类型的推理规则 (Typing rules)

2记号

•	$x.e$ 表示表达式 $e$ 中可以使用到 $x$ 这个自由变量. 例如自然数类型的消去子是使用了一个函数类型的实例, 而使用 CMU 记号的话应该会写作$$\frac{a:An:\mathbb{N}x:\mathbb{N},y:A⊢b:A}{{\mathrm{rec}}_{\mathbb{N}}(a,x.y.b,n)}$$
•	构造子的调用, 无交并类型传统的构造子可以记作函数应用, 但记号 CMU 会记作$$\mathrm{inl}\cdot n$$