在逻辑框架中使用高阶抽象语法进行推理

基于直觉主义逻辑或线性逻辑并具备高阶类型量化的逻辑框架，已成功用于对编程语言和推理系统中许多重要判决给出高层次、模块化且正式的规范。给定一个此类规范，自然会考虑在框架中对指定系统进行属性证明：例如，给定一个函数式编程语言的评估规范，证明该语言是确定的或评估保持类型。在发展用于此类推理框架的一个挑战是，高阶抽象语法（HOAS），即一种优雅且声明性的对对象级抽象和替换的处理方式，在涉及归纳的证明中难以处理。本文提出了一种可用于推理使用 HOAS 编码的判决的元逻辑；该元逻辑是一种扩展简单直觉主义逻辑的系统，允许对 simply typed lambda 项（HOAS 的关键要素）进行高阶量化，同时包含归纳和一种定义概念。我们通过考虑直觉主义逻辑和线性逻辑的编码，探讨了对 HOAS 编码进行形式元理论分析的困难；随后形式推导这些逻辑的重要子集的 cut 合法性。我们然后提出一种方法，以避免更高阶抽象语法的优势与对结果编码进行分析能力之间的明显权衡。我们通过涉及简单函数式和命令式编程语言 PCF 和 PCF:= 的例子来说明这种方法。我们形式化推导了诸如类型唯一性、主语归约、评估确定性以及评估的自然语义演示与过渡语义演示等属性。