Coq 中替换引理的形式化扩展
计算机科学中的逻辑
2023-09-26 v1
摘要
替换引理是 λ 演算理论中著名的定理，关注元替换操作的交互行为。在本工作中，我们为 λ 演算的文法增补一个未解释的指名替换（explicit substitution）算子，使得我们的框架可用于多种带指名替换的演算。我们的主要贡献在于验证了即便经过这些修改，替换引理依然成立。该结论是使用 Coq 证明助手得到的。我们的形式化方法采用名义（nominal）方法，其对 α 等价概念提供了直接实现。证明中变量重命名的策略带来挑战，尤其是在确保对我们向 λ 演算文法所作扩展之含义的探究方面。
引用
@article{arxiv.2309.13801,
title = {A Formalized Extension of the Substitution Lemma in Coq},
author = {Maria J. D. Lima and Flávio L. C. de Moura},
journal= {arXiv preprint arXiv:2309.13801},
year = {2023}
}
备注
In Proceedings FROM 2023, arXiv:2309.12959