A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
复制标题
通过机械化语法分析在 Isabelle/HOL 中充分充分浅嵌入 π 演算
DOI：
--
复制
发表时间：
2003
影响因子：
1.1
通讯作者：
D. Hirschkoff
中科院分区：
文献类型：
--
作者：
C. Röckl;D. Hirschkoff
本文讨论了高阶抽象语法技术在通用定理证明中的应用，产生形式化语言绑定器的浅嵌入。高阶抽象语法已成功应用于满足封闭世界假设的专用逻辑框架中。由于更通用的环境（如 Isabelle/HOL 或 Coq）不支持这种封闭世界假设，高阶抽象语法可能会产生外来术语，也就是说，数据类型可能会产生比语言中实际应有的术语更多的术语。手头的工作演示了如何通过两级格式良好的谓词来消除这些外来术语，进一步为规则归纳方面的结构归纳的实现奠定基础，从而提供成熟的语法分析。为了应用和证明格式良好的谓词，本文开发了一种基于高阶项的实例化和重新抽象相结合的证明技术。作为一种应用，诸如上下文理论（由 Honsell、Miculan 和 Scagnetto 引入）之类的句法原则被推导出来，并显示了谓词的充分性，两者都在 Isabelle/HOL 中 π 演算的形式化中。
This paper discusses an application of the higher-order abstract syntax technique to general-purpose theorem proving, yielding shallow embeddings of the binders of formalized languages. Higher-order abstract syntax has been applied with success in specialized logical frameworks which satisfy a closed-world assumption. As more general environments (like Isabelle/HOL or Coq) do not support this closed-world assumption, higher-order abstract syntax may yield exotic terms, that is, datatypes may produce more terms than there should actually be in the language. The work at hand demonstrates how such exotic terms can be eliminated by means of a two-level well-formedness predicate, further preparing the ground for an implementation of structural induction in terms of rule induction, and hence providing fully-fledged syntax analysis. In order to apply and justify well-formedness predicates, the paper develops a proof technique based on a combination of instantiations and reabstractions of higher-order terms. As an application, syntactic principles like the theory of contexts (as introduced by Honsell, Miculan, and Scagnetto) are derived, and adequacy of the predicates is shown, both within a formalization of the π-calculus in Isabelle/HOL.