论文部分内容阅读
在直觉主义逻辑和兰贝克演算之间,各演算的区别由结构规则的去留决定,于是形成了“结构层级”和“子结构逻辑”.在这些层级系统和类型化的兰姆达演算之间建立对应关系,便可实现句法范畴和语义表达式的并行推演,从而得到自然语言表达式的语义解释.直觉主义逻辑与简单类型兰姆达演算具有同构关系;相干逻辑、线性逻辑和兰贝克演算都与简单类型兰姆达演算具有对应关系,它们都对应了简单类型兰姆达演算的某一片段.