lambda Pi演算模重写中嵌入的保守性（长版本）
Conservativity of embeddings in the lambda Pi calculus modulo rewriting (long version)
摘要：
lambda Pi演算可以通过重写规则来扩展，以嵌入任何函数式纯类型系统。在本文中，我们证明了嵌入是保守的，通过证明一个相对形式的规范化，从而证明使用的lambda Pi演算模重写作为一个逻辑框架的逻辑基于纯类型系统。这个结果以前只在目标系统是标准化的条件下得到证明。我们的方法不依赖于这个条件，因此在源系统未归一化时也有效。
英文摘要：
The lambda Pi calculus can be extended with rewrite rules to embed any functional pure type system. In this paper, we show that the embedding is conservative by proving a relative form of normalization, thus justifying the use of the lambda Pi calculus modulo rewriting as a logical framework for logics based on pure type systems. This result was previously only proved under the condition that the target system is normalizing. Our approach does not depend on this condition and therefore also works when the source system is not normalizing.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
