AI 中文总结
研究证明助手中表层语法隐含问题，引入依赖类型单子领域特定语言，通过浅嵌入表示双向类型表层语言，实现正确转换，提取具体精细化算法，提升语法处理可靠性与可预测性。
AI 中文摘要
在诸如Rocq、Lean、Agda和Idris等证明助手的表层语法高度隐含，缺乏用户编写代码精确表示定义明确的数学对象所需的许多细节。精细化是一种通过将表层语法转换为足够明确的核心语法来处理这些细节的算法。其可靠性和可预测性依赖于核心类型系统的几个关键属性。我们引入一种依赖类型的单子领域特定语言，用于可构造正确的精细化算法的可执行规范，它从范式的任何特定表示或转换检查算法中抽象出来。我们通过浅嵌入这种DSL来表示Martin-Löf类型理论的双向类型表层语言，使得表层项到核心项的转换相当于基本等式计算。这种转换在构造上是正确的，在核心项的判断相等甚至替换下自动稳定，由此获得了精细化问题暂停的新表示解释。最后，通过代数方法从基于Martin-Löf类型理论的双初始自然模型构建的DSL的预层模型中提取了一个具体的精细化算法。
英文摘要
Surface syntax in proof assistants like Rocq, Lean, Agda, and Idris is highly implicit, lacking many details that are needed for user-written code to denote precisely defined mathematical objects. Elaboration is an algorithm that accounts for these details by translating surface syntax to an explicit enough core syntax. The reliability and predictability of elaboration relies on several critical properties of the core type system, including decidability of judgemental equality and the injectivity of type constructors; these dependencies are witnessed in a concrete system by explicit calls to conversion checking and weak-head reduction subroutines. We introduce a dependently typed monadic domain specific language for the executable specification of correct-by-construction elaboration algorithms that is abstracted from any particular representation of normal forms or algorithm for conversion checking. In particular, we represent a bidirectionally typed surface language for Martin-Löf type theory by shallow embedding in this DSL so that the translation of surface terms into core terms amounts to elementary equational calculation. This translation is correct by construction in the sense that it cannot produce ill-typed terms, and is automatically stable under judgemental equality of core terms and even under substitution; from the latter property, we obtain a new denotational interpretation of the suspension of elaboration problems. Finally, a concrete elaboration algorithm is extracted by algebraic means from a presheaf model of the DSL built out of the bi-initial natural model of Martin-Löf type theory.
