On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions

TL;DR

The paper tackles formalizing the metatheory of Pure Type Systems using one-sorted variable names and Stoughton’s substitutions, implemented and machine-checked in Agda. It develops a framework with a first-order syntax for $\lambda$-terms and $\Pi$-types, a robust substitution mechanism, and a rigorous treatment of $\alpha$- and $\beta$-conversion, culminating in key metatheoretic results such as thinning, syntactic validity, and closure under $\alpha$-conversion and substitution. A new, more workable notion of $\alpha$-conversion and a finitary alternative presentation are established, along with proofs of soundness and completeness relative to standard formulations. The work demonstrates that dependent type theory can be mechanized using conventional syntax without naming identifications, producing a compact ~3kLOC-scale formalization and offering a practical benchmark against larger mechanizations in the literature.

Abstract

We develop formal theories of conversion for Church-style lambda-terms with Pi-types in first-order syntax using one-sorted variables names and Stoughton's multiple substitutions. We then formalize the Pure Type Systems along some fundamental metatheoretic properties: weakening, syntactic validity, closure under alpha-conversion and substitution. Finally, we compare our formalization with others related. The whole development has been machine-checked using the Agda system. Our work demonstrates that the mechanization of dependent type theory by using conventional syntax and without identifying alpha-convertible lambda-terms is feasible.

Figures (3)

• Figure 1: $\lambda$-terms
• Figure 2: Pure Type Systems
• Figure 3: Standard (Finitary) PTS

Theorems & Definitions (42)

• Lemma 2.1
• Lemma 2.2
• Lemma 2.3
• proof
• Lemma 2.4
• proof
• Lemma 2.5
• Lemma 2.6
• Lemma 2.7
• proof