带有未定义性、引用和求值的简单类型论

本文提出了一个简单类型论的版本，称为${\cal Q}^{\rm uqe}_{0}$，它基于${\cal Q}_0$，即由Peter B. Andrews创建并广泛研究的Church类型论的优雅表述。${\cal Q}^{\rm uqe}_{0}$直接形式化了处理未定义性的传统方法，其中未定义表达式被视为合法的、无所指的表达式，可以成为有意义陈述的组成部分。${\cal Q}^{\rm uqe}_{0}$还配备了基于引用和求值对表达式语法进行推理的设施。引用用于指代表示表达式语法结构的语法值，求值用于指代语法值所代表的表达式的值。通过引用和求值，可以在${\cal Q}^{\rm uqe}_{0}$中推理表达式的语法和语义的相互作用，从而在${\cal Q}^{\rm uqe}_{0}$中形式化基于语法的数学算法。本文给出了${\cal Q}^{\rm uqe}_{0}$的语法和语义，以及${\cal Q}^{\rm uqe}_{0}$的证明系统。该证明系统对所有公式是可靠的，对不包含求值的公式是完备的。本文还展示了${\cal Q}^{\rm uqe}_{0}$的一些应用。