一种用于λ演算与强规范化的模块化Lean 4框架
A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums
AI总结：
本文提出了一种模块化Lean 4框架，用于证明λ演算及其扩展的连通性和强规范性，通过三种经典证明技术实现，并展示了完整的机械证明。
摘要：
我们介绍了Metatheory，这是一个用于编程语言基础的Lean 4综合性库。该库提供了一个模块化框架，用于通过三种经典证明技术证明抽象重写系统的连通性：钻石性质、Newman引理和Hindley-Rosen引理。这些技术在六个案例研究中得到实例化，包括未类型λ演算、组合逻辑、术语重写、单纯类型λ演算以及带有产品和求和的STLC。所有定理都完全机械化，不使用任何公理或sorry声明。我们提供了de Bruijn替换基础设施的完整证明，并通过逻辑关系展示了强规范性。据我们所知，这是第一个针对Lean 4的综合性连通性和规范性框架。
英文摘要：
We present Metatheory, a comprehensive library for programming language foundations in Lean 4. The library features a modular framework for proving confluence of abstract rewriting systems using three classical proof techniques: the diamond property, Newmans lemma, and the Hindley-Rosen lemma. These are instantiated across six case studies including untyped lambda calculus, combinatory logic, term rewriting, simply typed lambda calculus, and STLC with products and sums. All theorems are fully mechanized with zero axioms or sorry statements. We provide complete proofs of de Bruijn substitution infrastructure and demonstrate strong normalization via logical relations. To our knowledge, this is the first comprehensive confluence and normalization framework for Lean 4.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
