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

Basic Information

• Paper ID: 2510.12300
• Title: On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions
• Author: Sebastián Urciuoli (Universidad ORT Uruguay, Uruguay)
• Classification: cs.LO (Logic in Computer Science)
• Conference: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2025)
• Paper Link: https://arxiv.org/abs/2510.12300
• Code Link: https://github.com/surciuoli/pts-metatheory

Abstract

This paper develops a formal theory of conversion for Church-style λ-terms with Π types using first-order syntax, one-sorted variable names, and Stoughton's multiple substitutions. It then formalizes Pure Type Systems (PTS) and establishes fundamental metatheoretic properties: weakening, syntactic validity, closure under α-conversion, and closure under substitution. Finally, it compares related formalization work. The entire development has been mechanically verified using the Agda proof assistant. The work demonstrates the feasibility of mechanizing dependent type theory using traditional syntax without identifying α-convertible λ-terms.

Research Background and Motivation

Problem Background

1. Formalization Challenges: Mechanical verification of dependent type theory has been challenging, particularly when handling variable binding and α-equivalence
2. Syntax Selection Dilemma: Existing approaches typically employ de Bruijn indices or dual-sorted variable names to avoid name capture issues, but these diverge from actual implementations
3. Substitution Operation Complexity: Traditional unary substitution definitions are non-structurally recursive, requiring complex induction methods in mechanized proofs

Research Motivation

1. Scalability Testing: Verify whether frameworks based on Stoughton's substitution theory can extend to more complex languages (such as PTS)
2. Bridging Theory and Practice: Use traditional one-sorted variable name syntax, closer to actual type checker implementations
3. Simplifying Proof Methods: Through improved α-conversion definitions, enable key lemmas to be proven using simpler structural induction

Core Contributions

1. Extended Stoughton Substitution Framework: Extended the original pure λ-calculus framework to support Church-style λ-abstraction and Π types
2. Improved α-Conversion Definition: Proposed a new α-conversion definition enabling key lemmas to be proven through structural induction
3. Formalized PTS Metatheory: Mechanically verified fundamental metatheoretic properties of PTS, including weakening, syntactic validity, α-conversion closure, and substitution closure
4. Equivalence Proofs: Established the equivalence between infinite rule systems using generalized induction and standard finite rule systems
5. Complete Agda Implementation: Provided a complete mechanized verification with approximately 3000 lines of code

Methodology Details

Syntax Definition

The paper uses traditional first-order syntax to define λ-terms:

data Λ : Set where
  c : C → Λ                    -- constants
  v : V → Λ                    -- variables
  λ[_:_]_ : V → Λ → Λ → Λ      -- Church-style λ-abstraction
  Π[_:_]_ : V → Λ → Λ → Λ      -- Π type
  _·_ : Λ → Λ → Λ              -- application

Choice Functions and Substitution

The core innovation lies in using Stoughton's multiple substitutions, avoiding name capture through choice functions:

X : Res → V
X (σ, xs) = X' (concat (map (fv ∘ σ) xs))

Substitution operations are defined as structural recursion:

λ[ x : A ] M • σ = λ[ y : A • σ ](M • σ , x := v y) 
  where y = X (σ , fv M - x)

Improved α-Conversion Definition

The new α-conversion definition uses syntactic equivalence rather than recursive definition:

∼λ : ∀ {x x' y A A' M M'} → A ∼α A' → y ∉ fv M - x → y ∉ fv M' - x'
   → M [ x := v y ] ≡ M' [ x' := v y ] → λ[ x : A ] M ∼α λ[ x' : A' ] M'

PTS Type System

PTS is defined using generalized induction, with key rules including:

⊢abs : Γ ⊢ A : s₁ → ∀z → z ∉ domΓ → Γ,z : A ⊢ B[y := z] : s₂
     → ∀z → z ∉ domΓ → Γ,z : A ⊢ M[x := z] : B[y := z]
     → R s₁ s₂ s₃
     → Γ ⊢ λ[x : A]M : Π[y : A]B

Technical Innovations

1. Redefinition of Restriction Types

Redefining restrictions from Sub × Λ to Sub × List V, providing greater flexibility:

Res = Sub × List V

2. Structured α-Conversion Proofs

The key lemma iotaAlpha can now be proven through structural induction:

iotaAlpha : ∀ {M M'} → M • ι ≡ M' • ι → M ∼α M'

3. Enhanced Premises in Application Rules

Adding type validity premises to application rules, simplifying subsequent proofs:

⊢app : Γ ⊢ M : Π[x : A]B → Γ ⊢ N : A → Γ ⊢ B[x := N] : s
     → Γ ⊢ M·N : B[x := N]

Experimental Setup

Formalization Environment

• Proof Assistant: Agda system
• Code Scale: Approximately 3000 lines of code
• Module Division: Framework and PTS metatheory each occupy roughly half

Verification Content

1. Foundational Theory: Properties of substitution operations, equivalence of α-conversion
2. PTS Metatheory: Weakening, syntactic validity, closure theorems
3. Equivalence: Equivalence between infinite and finite rule systems

Experimental Results

Main Achievements

1. Complete Mechanization: Successfully mechanized verification of core metatheoretic properties of PTS
2. Simplified Proofs: All results (except α-conversion completeness) proven through structural induction
3. Code Efficiency: 3000 lines of code implementing complete theory, more concise than comparable work

Key Theorems

• Lemma 4.1 (Weakening): thinning : ∀ {Γ Δ M A} → Γ ⊆ Δ → Δ ok → Γ ⊢ M : A → Δ ⊢ M : A
• Lemma 4.3 (Syntactic Validity): syntacticValidity : ∀ {Γ M A} → Γ ⊢ M : A → ∃ λ s → A ≡ c s ⊎ Γ ⊢ A : c s
• Lemma 4.4 (α-Conversion Closure): closAlphaAsg : ∀ {Γ Δ M N A} → Γ ≈α Δ → M ∼α N → Γ ⊢ M : A → Δ ⊢ N : A
• Lemma 4.6 (Substitution Closure): closureSub : ∀ {Γ Δ M A σ} → σ : Γ ⇀ Δ → Δ ok → Γ ⊢ M : A → Δ ⊢ M • σ : A • σ

Equivalence Results

• Theorem 4.9-4.11: Established bidirectional equivalence between infinite rule systems and standard finite rule systems

Related Work

Main Comparisons

1. McKinna & Pollack: Use dual-sorted variable names, avoiding α-conversion but requiring well-formedness predicates
2. Barras & Werner: Use de Bruijn notation, approximately 2600 lines of code for similar functionality
3. Urban et al.: Use Nominal Isabelle, approximately 15K lines of code, with 1800 lines for metatheory
4. Modern Developments: Larger-scale type theory formalizations by Abel, Adjedj, Sozeau, and others

Advantage Analysis

• Directness: Substitution closure of β-conversion can be directly proven through structural induction
• Conciseness: No need for additional equivalence proofs or renaming lemmas
• Practicality: Closer to actual type checker implementations

Conclusions and Discussion

Main Conclusions

1. Feasibility Verification: Demonstrated the feasibility of mechanizing dependent type theory using traditional syntax and one-sorted variable names
2. Method Advantages: Stoughton's substitution method remains effective when handling complex type systems
3. Theoretical Contribution: Improved α-conversion definition simplifies key proofs

Limitations

1. Scale Constraints: Currently addresses only basic metatheory of PTS, not more complex properties such as strong normalization
2. Performance Considerations: Computational complexity of multiple substitutions may impact practical applications
3. Extensibility: Extension to larger-scale type systems (such as those with universes, large elimination) requires further verification

Future Directions

1. Extension to More Complex Systems: Such as systems with inductive types and universe hierarchies
2. Performance Optimization: Research efficient implementations of substitution operations
3. Practical Applications: Apply theoretical results to actual type checker implementations

In-Depth Evaluation

Strengths

1. Theoretical Innovation: The improved α-conversion definition is an important theoretical contribution, simplifying proof complexity
2. Practical Value: Using traditional syntax narrows the gap between theory and practice
3. Completeness: Provides complete mechanized verification of PTS metatheory
4. Clarity: Clear paper writing with accurate technical detail descriptions
5. Reproducibility: Provides complete Agda code for verification and extension

Weaknesses

1. Coverage Scope: Compared to some large-scale formalization work, the theoretical content covered is relatively limited
2. Performance Analysis: Lacks in-depth analysis of computational complexity of substitution operations
3. Practical Verification: Lacks comparative verification with actual type checker implementations
4. Extensibility Discussion: Insufficient discussion of challenges in extending to more complex systems

Impact

1. Academic Contribution: Provides a new technical pathway for mechanizing dependent type theory
2. Practical Value: Provides theoretical foundation for type checker correctness verification
3. Methodology: Successful application of Stoughton's substitution method may inspire related work
4. Tool Value: Agda library can provide infrastructure for subsequent research

Applicable Scenarios

1. Type Checker Verification: Suitable for scenarios requiring verification of type checker correctness
2. Educational Research: Can serve as an excellent case study for learning formalized dependent type theory
3. Theoretical Research: Provides foundation for studying metatheory of more complex type systems
4. Tool Development: Can serve as reference implementation for developing formalized verification tools

References

The paper cites 31 important references, primarily including:

• Stoughton (1988): Original theory of multiple substitutions
• Barendregt (1992): Classical theory of PTS
• McKinna & Pollack (1993, 1999): PTS formalization in LEGO
• Barras & Werner: CC formalization in Coq
• Urban et al. (2011): LF metatheory using Nominal Isabelle
• Tasistro et al. (2015): Original work on Stoughton substitution framework

Overall Assessment: This is a high-quality theoretical computer science paper making important contributions to mechanized verification of dependent type theory. The paper's technical innovations are clear, the implementation is complete, and it provides valuable theoretical foundation and practical experience for subsequent research in this field.