简化 Lambda-Mu 演算的指称语义与经典类型论的新演绎系统

经典（或布尔）类型论是允许类型推导 $\sigma \to \bot) \to \bot => \sigma$（双重否定消去的类型对应物）的类型论，其中 $\sigma$ 是任意类型，$\bot$ 是荒谬类型。本文首先为 Parigot 的 lambda-mu 演算的一个简化版本提出了指称语义，该演算是经典类型论的首要示例。在此语义中，每个类型的论域被划分为无穷多个秩，不仅包含该类型在秩 0 处的通常成员，还包含其在更高秩处的否定、合取和析取阴影，这些阴影构成了一个无穷嵌套的布尔结构。荒谬类型 $\bot$ 被等同于真值类型。随后，本文提出了经典类型论的一个新演绎系统，即称为经典类型系统（CTS）的矢列演算，它包含标准的逻辑算子（如否定、合取和析取），从而以更直接的方式反映了所讨论的语义结构。