2025-11-15T20:46:11.945579

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

Urciuoli

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.

academic

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

基本信息

论文ID: 2510.12300
标题: On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions
作者: Sebastián Urciuoli (Universidad ORT Uruguay, Uruguay)
分类: cs.LO (Logic in Computer Science)
发表会议: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2025)
论文链接: https://arxiv.org/abs/2510.12300
代码链接: https://github.com/surciuoli/pts-metatheory

形式化挑战: 依赖类型理论的机械化验证一直是一个挑战，特别是在处理变量绑定和α等价时
语法选择困境: 现有方法通常采用de Bruijn索引或双排序变量名来避免名称捕获问题，但这些方法与实际实现存在差距
替换操作复杂性: 传统的一元替换定义是非结构递归的，在机械化证明中需要复杂的归纳方法

研究动机

测试可扩展性: 验证基于Stoughton替换理论的框架能否扩展到更复杂的语言(如PTS)
缩小理论与实践差距: 使用传统的单一排序变量名语法，更接近实际的类型检查器实现
简化证明方法: 通过改进α转换定义，使用更简单的结构归纳方法证明关键引理

核心贡献

扩展了Stoughton替换框架: 将原有的纯λ演算框架扩展到支持Church风格λ抽象和Π类型
改进的α转换定义: 提出了新的α转换定义，使得关键引理可以通过结构归纳证明
PTS元理论形式化: 机械化验证了PTS的基本元理论性质，包括弱化、语法有效性、α转换封闭性和替换封闭性
等价性证明: 证明了使用广义归纳的无穷规则系统与标准有限规则系统的等价性
完整的Agda实现: 提供了约3000行代码的完整机械化验证

方法详解

语法定义

论文使用传统的一阶语法定义λ项：

data Λ : Set where
  c : C → Λ                    -- 常量
  v : V → Λ                    -- 变量  
  λ[_:_]_ : V → Λ → Λ → Λ      -- Church风格λ抽象
  Π[_:_]_ : V → Λ → Λ → Λ      -- Π类型
  _·_ : Λ → Λ → Λ              -- 应用

选择函数与替换

核心创新在于使用Stoughton的多重替换，通过选择函数避免名称捕获：

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

替换操作定义为结构递归：

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

改进的α转换定义

新的α转换定义使用语法等价而非递归定义：

∼λ : ∀ {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类型系统

使用广义归纳定义PTS，关键规则包括：

⊢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

技术创新点

1. 限制类型的重新定义

将限制从Sub × Λ重新定义为Sub × List V，提供更大的灵活性：

Res = Sub × List V

2. 结构化的α转换证明

关键引理iotaAlpha现在可以通过结构归纳证明：

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

3. 应用规则的增强前提

在应用规则中添加类型有效性前提，简化后续证明：

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

实验设置

形式化环境

证明助手: Agda系统
代码规模: 约3000行代码
模块划分: 框架和PTS元理论各占一半

验证内容

基础理论: 替换操作的性质、α转换的等价性
PTS元理论: 弱化、语法有效性、封闭性定理
等价性: 无穷规则系统与有限规则系统的等价性

实验结果

主要成果

完整机械化: 成功机械化验证了PTS的核心元理论性质
简化证明: 所有结果(除α转换的完备性外)都通过结构归纳证明
代码效率: 3000行代码实现完整理论，相比其他工作更加简洁

关键定理

Lemma 4.1 (弱化): thinning : ∀ {Γ Δ M A} → Γ ⊆ Δ → Δ ok → Γ ⊢ M : A → Δ ⊢ M : A
Lemma 4.3 (语法有效性): syntacticValidity : ∀ {Γ M A} → Γ ⊢ M : A → ∃ λ s → A ≡ c s ⊎ Γ ⊢ A : c s
Lemma 4.4 (α转换封闭性): closAlphaAsg : ∀ {Γ Δ M N A} → Γ ≈α Δ → M ∼α N → Γ ⊢ M : A → Δ ⊢ N : A
Lemma 4.6 (替换封闭性): closureSub : ∀ {Γ Δ M A σ} → σ : Γ ⇀ Δ → Δ ok → Γ ⊢ M : A → Δ ⊢ M • σ : A • σ