HOL轻型QE
HOL Light QE
摘要：
我们感兴趣的是以数学上有意义的方式处理数学表达式的算法。表达式是语法的，但大多数逻辑不允许讨论语法。${\rm CTT}_{\rm qe}$是Church类型论的一个版本，它包含了引用和求值运算符，类似于Lisp程序设计语言中的引用和求值。由于HOL逻辑也是Church类型论的一个版本，我们决定将引用和评估添加到HOL Light中，以演示${\rm CTT}_{\rm qe}$的可实现性以及在证明助手中使用引用和评估的好处。由此产生的系统被称为HOL Light QE。在这里，我们记录了HOL Light QE的设计以及需要克服的挑战。由此产生的实现是免费提供的。
英文摘要：
We are interested in algorithms that manipulate mathematical expressions in mathematically meaningful ways. Expressions are syntactic, but most logics do not allow one to discuss syntax. ${\rm CTT}_{\rm qe}$ is a version of Church's type theory that includes quotation and evaluation operators, akin to quote and eval in the Lisp programming language. Since the HOL logic is also a version of Church's type theory, we decided to add quotation and evaluation to HOL Light to demonstrate the implementability of ${\rm CTT}_{\rm qe}$ and the benefits of having quotation and evaluation in a proof assistant. The resulting system is called HOL Light QE. Here we document the design of HOL Light QE and the challenges that needed to be overcome. The resulting implementation is freely available.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
