为支持重写的逻辑框架形式化表示定理
Formalizing Representation Theorems for a Logical Framework with Rewriting
AI总结：
本文提出在支持理论同态与逻辑关系的逻辑框架中，通过归纳翻译规则形式化和验证表示定理，特别针对排序消除翻译等挑战性转换提供优雅的新形式化方法。
摘要：
形式系统中的表示定理通常以归纳翻译形式出现，满足某些不变量，这些不变量通过归纳法证明。理论同态和逻辑关系是此类归纳构造的常见模式。它们允许将翻译和不变量的证明表示为翻译规则集，对应归纳的各个情况。重要的是，建立不变量被简化为检查有限集，通常可判定的陈述。因此，在支持理论同态和逻辑关系的框架中，符合这些模式的翻译更容易形式化和验证。lambdaPi-calculus modulo rewriting是一种用于表示和翻译正式系统的逻辑框架，此前未系统支持此类模式。本文将其扩展以支持理论同态和逻辑关系。我们应用这些来定义和验证多个正式系统之间的翻译不变量。在此过程中，我们识别了一些最佳实践，使我们能够获得一些挑战性翻译的优雅新形式化，特别是从排序到无序语言的排序消除翻译。
英文摘要：
Representation theorems for formal systems often take the form of an inductive translation that satisfies certain invariants, which are proved inductively. Theory morphisms and logical relations are common patterns of such inductive constructions. They allow representing the translation and the proofs of the invariants as a set of translation rules, corresponding to the cases of the inductions. Importantly, establishing the invariants is reduced to checking a finite set of, typically decidable, statements. Therefore, in a framework supporting theory morphisms and logical relations, translations that fit one of these patterns become much easier to formalize and to verify. The lambdaPi-calculus modulo rewriting is a logical framework designed for representing and translating between formal systems that has previously not systematically supported such patterns. In this paper, we extend it with theory morphisms and logical relations. We apply these to define and verify invariants for a number of translations between formal systems. In doing so, we identify some best practices that enable us to obtain elegant novel formalizations of some challenging translations, in particular sort-erasure translations from sorted to unsorted languages.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
