环境分类器的逻辑基础

中文速览

多阶段编程需要同时支持开放代码、代码执行和跨阶段嵌入，又要在编译时保证生成的代码封闭且安全，但原有环境分类器系统的类型规则缺少清晰的逻辑基础。作者借助 Curry–Howard 对应，设计了带环境分类器的类型化 λ 演算 λ^▷，把分类器解释为可能世界之间带标签的转换序列，并将 run 和跨阶段持久化统一为分类器应用。该演算满足类型保持、合流性、强正规化和按阶段进行的正规化，还证明良类型程序能安全地分阶段执行，并建立了相应经典逻辑与 Kripke 语义之间的可靠性和完备性。其重要性在于，它把多阶段语言中原本零散、复杂的安全机制统一到一个有逻辑语义支撑的框架里，为 MetaOCaml 一类语言的设计、证明和实现提供了更简洁的基础。

摘要

Taha 和 Nielsen 基于环境分类器的概念，构建了一个具有可靠类型系统的多阶段演算 $\lambda^{\alpha}$。环境分类器是特殊的标识符，代码片段和变量声明均使用它们进行注释，并利用其作用域机制在静态上确保某些代码片段是闭合代码且能够安全运行。

Taha and Nielsen have developed a multi-stage calculus $\lambda^{\alpha}$ with a sound type system using the notion of environment classifiers. They are special identifiers, with which code fragments and variable declarations are annotated, and their scoping mechanism is used to ensure statically that certain code fragments are closed and safely runnable.

术语表

multi-stage calculus

多阶段演算

environment classifier

环境分类器

classifier

分类器

Curry-Howard isomorphism

Curry–Howard 同构

typed λ-calculus

带类型 λ 演算

multi-modal logic

多模态逻辑

transition variable

迁移变量

labeled transition

带标签迁移

possible world

可能世界

quasiquotation

准引用

code fragment

代码片段

closed code

闭合代码

open code

开放代码

run construct

run 构造

cross-stage persistence (CSP)

跨阶段持久化（CSP）

modal operator

模态算子

necessity operator

必然算子

next operator

next 算子

linear-time temporal logic (LTL)

线性时序逻辑（LTL）

Kripke semantics

Kripke 语义

subject reduction

类型保持

confluence

合流性

strong normalization

强规范化

time-ordered normalization

按时间顺序规范化

big-step evaluation semantics

大步求值语义

erasure semantics

擦除语义

type inference

类型推断

MetaOCaml

MetaOCaml